razor_chase/chase/impl/
batch.rs

1//! Improves `chase::impl::reference` by evaluating the sequent provided by the strategy
2//! against all assignments from the free variables of the sequent to the elements of the
3//! model in which it is being evaluated.
4//!
5//! [`chase::impl::reference::Evaluator`] extends the [`Model`] that it processes in a
6//! [chase-step] only for one assignment from the free variables of the [`Sequent`] that it is
7//! evaluating to the elements of the [`Model`]. [`chase::impl::batch::Evaluator`] is the only
8//! different component between [`chase::impl::reference`] and [`chase::impl::batch`].
9//!
10//! [`chase::impl::reference`]: ../reference/index.html
11//! [`Sequent`]: ../basic/struct.Sequent.html
12//! [chase-step]: ../../index.html#chase-step
13//! [`chase::impl::reference::Evaluator`]: ../reference/struct.Evaluator.html
14//! [`Model`]: ../reference/struct.Model.html
15//! [`chase::impl::batch::Evaluator`]: ./struct.Evaluator.html
16//! [`chase::impl::reference`]: ../reference/index.html
17//! [`chase::impl::batch`]: ./index.html
18
19use std::{
20    collections::HashMap,
21    iter,
22};
23use razor_fol::syntax::V;
24use crate::chase::{
25    r#impl::{
26        basic, reference,
27        reference::{WitnessTerm, Element},
28    },
29    Rel, Observation, EvaluateResult,
30    ModelTrait, StrategyTrait, EvaluatorTrait, BounderTrait,
31};
32use itertools::{Itertools, Either};
33
34/// Simple evaluator that evaluates a Sequnet in a Model.
35pub struct Evaluator {}
36
37impl<'s, Stg: StrategyTrait<Item=&'s Sequent>, B: BounderTrait> EvaluatorTrait<'s, Stg, B> for Evaluator {
38    type Sequent = Sequent;
39    type Model = Model;
40    fn evaluate(
41        &self,
42        initial_model: &Model,
43        strategy: &mut Stg,
44        bounder: Option<&B>,
45    ) -> Option<EvaluateResult<Model>> {
46        let mut result = EvaluateResult::new();
47
48        let domain: Vec<&Element> = initial_model.domain();
49        let domain_size = domain.len();
50        for sequent in strategy {
51            let vars = &sequent.free_vars;
52            let vars_size = vars.len();
53            if domain_size == 0 && vars_size > 0 {
54                continue; // empty models can only be extended with sequents with no free variables.
55            }
56
57            // maintain a list of indices into the model elements to which variables are mapped
58            let mut assignment: Vec<usize> = iter::repeat(0).take(vars_size).collect();
59
60            // try all the variable assignments to the elements of the model
61            // (notice the do-while pattern)
62            while {
63                // construct a map from variables to elements
64                let mut assignment_map: HashMap<&V, Element> = HashMap::new();
65                for i in 0..vars_size {
66                    assignment_map.insert(vars.get(i).unwrap(), (*domain.get(assignment[i]).unwrap()).clone());
67                }
68                // construct a "characteristic function" for the assignment map
69                let assignment_func = |v: &V| assignment_map.get(v).unwrap().clone();
70
71                // lift the variable assignments to literals (used to make observations)
72                let observe_literal = make_observe_literal(assignment_func);
73
74                // build body and head observations
75                let body: Vec<Observation<WitnessTerm>> = sequent.body_literals
76                    .iter().map(&observe_literal).collect();
77                let head: Vec<Vec<Observation<WitnessTerm>>> = sequent.head_literals
78                    .iter().map(|l| l.iter().map(&observe_literal).collect()).collect();
79
80                // if all body observations are true in the model but not all the head observations
81                // are true, extend the model:
82                if body.iter().all(|o| initial_model.is_observed(o))
83                    && !head.iter().any(|os| os.iter().all(|o| initial_model.is_observed(o))) {
84                    if head.is_empty() {
85                        return None; // the chase fails if the head is empty (FALSE)
86                    } else {
87                        if result.open_models.is_empty() {
88                            result.open_models.push(initial_model.clone());
89                        }
90
91                        // extending all extensions of this model with the new observations:
92                        let models: Vec<Either<Model, Model>> = result.open_models.iter().flat_map(|m| {
93                            let ms: Vec<Either<Model, Model>> = if let Some(bounder) = bounder {
94                                let extend = make_bounded_extend(bounder, m);
95                                head.iter().map(extend).collect()
96                            } else {
97                                let extend = make_extend(m);
98                                head.iter().map(extend).collect()
99                            };
100                            ms
101                        }).collect();
102
103                        // all previous extensions are now extended further. so remove them from
104                        // the result:
105                        result.open_models.clear();
106                        models.into_iter().for_each(|m| result.append(m));
107                    }
108                }
109
110                // try the next variable assignment
111                domain_size > 0 && next_assignment(&mut assignment, domain_size - 1)
112            } {}
113        }
114
115        return Some(result);
116    }
117}
118
119// Returns a closure that returns a cloned extension of the given model, extended by a given set of
120// observations.
121fn make_extend<'m>(
122    model: &'m Model
123) -> impl FnMut(&'m Vec<Observation<WitnessTerm>>) -> Either<Model, Model>
124{
125    move |os: &'m Vec<Observation<WitnessTerm>>| {
126        let mut model = model.clone();
127        os.iter().foreach(|o| model.observe(o));
128        Either::Left(model)
129    }
130}
131
132// Returns a closure that returns a cloned extension of the given model, extended by a given set of
133// observations. Unlike `make_extend`, `make_bounded_extend` extends the model with respect to a
134// bounder: a model wrapped in `Either::Right` has not reached the bounds while a model wrapped in
135// `Either::Left` has reached the bounds provided by `bounder`.
136fn make_bounded_extend<'m, B: BounderTrait>(
137    bounder: &'m B,
138    model: &'m Model,
139) -> impl FnMut(&'m Vec<Observation<WitnessTerm>>) -> Either<Model, Model>
140{
141    move |os: &Vec<Observation<WitnessTerm>>| {
142        let mut model = model.clone();
143        let mut modified = false;
144        os.iter().foreach(|o| {
145            if bounder.bound(&model, o) {
146                if !model.is_observed(o) {
147                    modified = true;
148                }
149            } else {
150                if !model.is_observed(o) {
151                    model.observe(o);
152                }
153            }
154        });
155        if modified {
156            Either::Right(model)
157        } else {
158            Either::Left(model)
159        }
160    }
161}
162
163// Given an function from variables to elements of a model, returns a closure that lift the variable
164// assignments to literals of a sequent, returning observations.
165fn make_observe_literal(assignment_func: impl Fn(&V) -> Element)
166                        -> impl Fn(&Literal) -> Observation<WitnessTerm> {
167    move |lit: &Literal| {
168        match lit {
169            basic::Literal::Atm { predicate, terms } => {
170                let terms = terms
171                    .into_iter()
172                    .map(|t| WitnessTerm::witness(t, &assignment_func))
173                    .collect();
174                Observation::Fact { relation: Rel(predicate.0.clone()), terms }
175            }
176            basic::Literal::Eql { left, right } => {
177                let left = WitnessTerm::witness(left, &assignment_func);
178                let right = WitnessTerm::witness(right, &assignment_func);
179                Observation::Identity { left, right }
180            }
181        }
182    }
183}
184
185// Implements a counter to enumerate all the possible assignments of a domain of elements to free
186// variables of a sequent. It mutates the given a list of indices, corresponding to mapping of each
187// position to an element of a domain to the next assignment. Returns true if a next assignment
188// exists and false otherwise.
189fn next_assignment(vec: &mut Vec<usize>, last: usize) -> bool {
190    let len = vec.len();
191    for i in 0..len {
192        if vec[i] != last {
193            vec[i] += 1;
194            return true;
195        } else {
196            vec[i] = 0;
197        }
198    }
199    false
200}
201
202pub type Sequent = basic::Sequent;
203pub type Literal = basic::Literal;
204pub type Model = reference::Model;
205
206#[cfg(test)]
207mod test_batch {
208    use super::{Evaluator, next_assignment};
209    use crate::chase::r#impl::reference::Model;
210    use crate::chase::r#impl::basic::Sequent;
211    use razor_fol::syntax::Theory;
212    use crate::chase::{
213        SchedulerTrait, StrategyTrait, strategy::{Bootstrap, Fair},
214        scheduler::FIFO, bounder::DomainSize, chase_all,
215    };
216    use crate::test_prelude::*;
217    use std::collections::HashSet;
218    use std::fs;
219
220    #[test]
221    fn test_next_assignment() {
222        {
223            let mut assignment = vec![];
224            assert_eq!(false, next_assignment(&mut assignment, 1));
225            assert!(assignment.is_empty());
226        }
227        {
228            let mut assignment = vec![0];
229            assert_eq!(true, next_assignment(&mut assignment, 1));
230            assert_eq!(vec![1], assignment);
231        }
232        {
233            let mut assignment = vec![1];
234            assert_eq!(false, next_assignment(&mut assignment, 1));
235            assert_eq!(vec![0], assignment);
236        }
237        {
238            let mut assignment = vec![0, 1];
239            assert_eq!(true, next_assignment(&mut assignment, 1));
240            assert_eq!(vec![1, 1], assignment);
241        }
242        {
243            let mut assignment = vec![1, 1];
244            assert_eq!(true, next_assignment(&mut assignment, 2));
245            assert_eq!(vec![2, 1], assignment);
246        }
247        {
248            let mut assignment = vec![2, 1];
249            assert_eq!(true, next_assignment(&mut assignment, 2));
250            assert_eq!(vec![0, 2], assignment);
251        }
252        {
253            let mut assignment = vec![2, 2];
254            assert_eq!(false, next_assignment(&mut assignment, 2));
255            assert_eq!(vec![0, 0], assignment);
256        }
257        {
258            let mut counter = 1;
259            let mut vec = vec![0, 0, 0, 0, 0];
260            while next_assignment(&mut vec, 4) {
261                counter += 1;
262            }
263            assert_eq!(3125, counter);
264        }
265    }
266
267    fn run_test(theory: &Theory) -> Vec<Model> {
268        let geometric_theory = theory.gnf();
269        let sequents: Vec<Sequent> = geometric_theory
270            .formulae
271            .iter()
272            .map(|f| f.into()).collect();
273
274        let evaluator = Evaluator {};
275        let strategy: Bootstrap<Sequent, Fair<Sequent>> = Bootstrap::new(sequents.iter().collect());
276        let mut scheduler = FIFO::new();
277        let bounder: Option<&DomainSize> = None;
278        scheduler.add(Model::new(), strategy);
279        chase_all(&mut scheduler, &evaluator, bounder)
280    }
281
282    #[test]
283    fn test() {
284        println!("{}", std::env::current_dir().unwrap().to_str().unwrap());
285        for item in fs::read_dir("../theories/core").unwrap() {
286            let theory = read_theory_from_file(item.unwrap().path().to_str().unwrap());
287            let basic_models = solve_basic(&theory);
288            let test_models = run_test(&theory);
289            let basic_models: HashSet<String> = basic_models.into_iter().map(|m| print_basic_model(m)).collect();
290            let test_models: HashSet<String> = test_models.into_iter().map(|m| print_reference_model(m)).collect();
291            assert_eq!(basic_models, test_models);
292        }
293    }
294}
razor_chase/chase/impl/batch.rs

razor_chase/chase/impl/
batch.rs
