Fix CNF and DNF transformations

razor-chase/src/chase.rs

@@ -43,7 +43,7 @@
 //! [the chase]: https://en.wikipedia.org/wiki/Chase_(algorithm)
 //! [geometric theories]: https://www.cs.bham.ac.uk/~sjv/GLiCS.pdf
 //! [run of the chase]: self#chase_all
-//! [standard syntactic manipulation]: razor_fol::transform::CNF::gnf()
+//! [standard syntactic manipulation]: razor_fol::transform::Gnf
 //! [godel]: https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theorems
 //!
 //! ## The Chase
@@ -149,7 +149,7 @@ impl fmt::Display for E {
 
 impl fmt::Debug for E {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "{}", self.to_string())
+        write!(f, "{}", self)
     }
 }
 
@@ -261,7 +261,7 @@ impl fmt::Display for Rel {
 
 impl fmt::Debug for Rel {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "{}", self.to_string())
+        write!(f, "{}", self)
     }
 }
 
@@ -293,7 +293,7 @@ impl<T: WitnessTerm> fmt::Display for Observation<T> {
 
 impl<T: WitnessTerm> fmt::Debug for Observation<T> {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "{}", self.to_string())
+        write!(f, "{}", self)
     }
 }
 
@@ -340,18 +340,18 @@ pub trait Model: Clone {
 /// [bg]: self#background
 pub trait Sequent: Clone {
     /// Returns the *body* (premise) of the sequent as a formula.
-    fn body(&self) -> FOF;
+    fn body(&self) -> Fof;
 
     /// Returns the *head* (consequence) of the sequent as a formula.
-    fn head(&self) -> FOF;
+    fn head(&self) -> Fof;
 }
 
 impl<S: Sequent> Sequent for &S {
-    fn body(&self) -> FOF {
+    fn body(&self) -> Fof {
         (*self).body()
     }
 
-    fn head(&self) -> FOF {
+    fn head(&self) -> Fof {
         (*self).head()
     }
 }
@@ -367,7 +367,7 @@ pub trait PreProcessor {
 
     /// Given a theory, returns an iterator of [sequents][Sequent] and an initial
     /// [model][Model] by applying the necessary pre-processing.
-    fn pre_process(&self, theory: &Theory<FOF>) -> (Vec<Self::Sequent>, Self::Model);
+    fn pre_process(&self, theory: &Theory<Fof>) -> (Vec<Self::Sequent>, Self::Model);
 }
 
 /// Strategy is the trait of algorithms for choosing sequents in the context of an
@@ -527,7 +527,7 @@ pub trait Scheduler<S: Sequent, M: Model, Stg: Strategy<S>> {
 /// [the chase]: self#the-chase
 ///
 /// ```rust
-/// use razor_fol::syntax::{FOF, Theory};
+/// use razor_fol::syntax::{Fof, Theory};
 /// use razor_chase::chase::{
 ///     PreProcessor, Scheduler, Strategy, chase_all,
 ///     r#impl::basic,
@@ -537,7 +537,7 @@ pub trait Scheduler<S: Sequent, M: Model, Stg: Strategy<S>> {
 /// };
 ///
 /// // parse the theory:
-/// let theory: Theory<FOF> = r#"
+/// let theory: Theory<Fof> = r#"
 ///   exists x . P(x);
 ///   P(x) implies Q(x) | R(x);
 ///   R(x) -> exists y . S(x, y);
@@ -596,7 +596,7 @@ where
 /// [chase-step]: self#chase-step
 ///
 /// ```rust
-/// use razor_fol::syntax::{FOF, Theory};
+/// use razor_fol::syntax::{Fof, Theory};
 /// use razor_chase::chase::{
 ///     PreProcessor, Scheduler, Strategy, chase_step,
 ///     r#impl::basic,
@@ -607,7 +607,7 @@ where
 /// use std::convert::TryInto;
 ///
 /// // parse the theory:
-/// let theory: Theory<FOF> = r#"
+/// let theory: Theory<Fof> = r#"
 ///   exists x . P(x);
 ///   P(x) implies Q(x) | R(x);
 ///   R(x) -> exists y . S(x, y);

razor-chase/src/chase/bounder.rs

@@ -3,7 +3,7 @@
 //! The bounders are instances of [`Bounder`].
 //!
 //! [`Bounder`]: crate::chase::Bounder
-use crate::chase::{Bounder, Model, Observation, WitnessTerm};
+use crate::chase::{Bounder, Model, Observation};
 
 /// Bounds the size of a [model] by the number of elements in its [domain].
 ///
@@ -29,13 +29,11 @@ impl Bounder for DomainSize {
         match observation {
             Observation::Fact { relation: _, terms } => {
                 let model_size = model.domain().len();
-                let terms: Vec<Option<<<M as Model>::TermType as WitnessTerm>::ElementType>> =
-                    terms
-                        .iter()
-                        .map(|t| model.element(t))
-                        .filter(|t| t.is_none())
-                        .collect();
-                let size = terms.len();
+                let size = terms
+                    .iter()
+                    .map(|t| model.element(t))
+                    .filter(|t| t.is_none())
+                    .count();
                 model_size + size > self.max_domain_size
             }
             Observation::Identity { left, right } => {

razor-chase/src/chase/impl/basic.rs

@@ -11,8 +11,8 @@ use crate::chase::*;
 use either::Either;
 use itertools::Itertools;
 use razor_fol::{
-    syntax::{formula::Atomic, term::Complex, Formula, FOF},
-    transform::GNF,
+    syntax::{formula::Atomic, term::Complex, Fof, Formula},
+    transform::Gnf,
 };
 use std::{
     collections::{HashMap, HashSet},
@@ -89,7 +89,7 @@ impl fmt::Display for BasicWitnessTerm {
 
 impl fmt::Debug for BasicWitnessTerm {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "{}", self.to_string())
+        write!(f, "{}", self)
     }
 }
 
@@ -465,9 +465,7 @@ impl fmt::Debug for BasicModel {
             .sorted()
             .iter()
             .map(|e| {
-                let witnesses: Vec<String> =
-                    self.witness(e).iter().map(|w| w.to_string()).collect();
-                let witnesses = witnesses.into_iter().sorted();
+                let witnesses = self.witness(e).iter().map(|w| w.to_string()).sorted();
                 format!("{} -> {}", witnesses.into_iter().sorted().join(", "), e)
             })
             .collect();
@@ -505,12 +503,12 @@ pub struct BasicSequent {
     pub head: Vec<Vec<Literal>>,
 
     // other fields:
-    body_fof: FOF,
-    head_fof: FOF,
+    body_fof: Fof,
+    head_fof: Fof,
 }
 
-impl From<GNF> for BasicSequent {
-    fn from(gnf: GNF) -> Self {
+impl From<Gnf> for BasicSequent {
+    fn from(gnf: Gnf) -> Self {
         let gnf_body = gnf.body();
         let gnf_head = gnf.head();
         let free_vars = gnf.free_vars().into_iter().cloned().collect();
@@ -547,11 +545,11 @@ impl fmt::Display for BasicSequent {
 }
 
 impl Sequent for BasicSequent {
-    fn body(&self) -> FOF {
+    fn body(&self) -> Fof {
         self.body_fof.clone()
     }
 
-    fn head(&self) -> FOF {
+    fn head(&self) -> Fof {
         self.head_fof.clone()
     }
 }
@@ -566,9 +564,9 @@ impl PreProcessor for BasicPreProcessor {
     type Sequent = BasicSequent;
     type Model = BasicModel;
 
-    fn pre_process(&self, theory: &Theory<FOF>) -> (Vec<Self::Sequent>, Self::Model) {
-        use razor_fol::transform::ToGNF;
-        use razor_fol::transform::ToSNF;
+    fn pre_process(&self, theory: &Theory<Fof>) -> (Vec<Self::Sequent>, Self::Model) {
+        use razor_fol::transform::ToGnf;
+        use razor_fol::transform::ToSnf;
 
         let mut c_counter: u32 = 0;
         let mut f_counter: u32 = 0;
@@ -751,7 +749,7 @@ fn make_observe_literal(
 // variables of a sequent. It mutates the given a list of indices, corresponding to mapping of each
 // position to an element of a domain to the next assignment. Returns true if a next assignment
 // exists and false otherwise.
-fn next_assignment(vec: &mut Vec<usize>, last: usize) -> bool {
+fn next_assignment(vec: &mut [usize], last: usize) -> bool {
     for item in vec.iter_mut() {
         if *item != last {
             *item += 1;
@@ -770,7 +768,7 @@ mod test_basic {
         bounder::DomainSize, chase_all, scheduler::FIFO, strategy::Linear, Scheduler,
     };
     use crate::test_prelude::*;
-    use razor_fol::transform::ToGNF;
+    use razor_fol::transform::ToGnf;
     use std::iter::FromIterator;
 
     // Witness Elements
@@ -1022,55 +1020,55 @@ mod test_basic {
     }
 
     // Assumes that `fof` is in GNF, so it converts to a single GNF
-    fn sequents(gnfs: Vec<GNF>) -> Vec<BasicSequent> {
+    fn sequents(gnfs: Vec<Gnf>) -> Vec<BasicSequent> {
         gnfs.into_iter().map(BasicSequent::from).collect()
     }
 
     #[test]
     fn test_build_sequent() {
-        assert_debug_string("[]", sequents("true -> true".parse::<FOF>().unwrap().gnf()));
+        assert_debug_string("[]", sequents("true -> true".parse::<Fof>().unwrap().gnf()));
         assert_debug_string(
             "[]",
-            sequents("true -> true & true".parse::<FOF>().unwrap().gnf()),
+            sequents("true -> true & true".parse::<Fof>().unwrap().gnf()),
         );
         assert_debug_string(
             "[]",
-            sequents("true -> true | true".parse::<FOF>().unwrap().gnf()),
+            sequents("true -> true | true".parse::<Fof>().unwrap().gnf()),
         );
         assert_debug_string(
             "[[] -> []]",
-            sequents("true -> false".parse::<FOF>().unwrap().gnf()),
+            sequents("true -> false".parse::<Fof>().unwrap().gnf()),
         );
         assert_debug_string(
             "[[] -> []]",
-            sequents("true -> false & true".parse::<FOF>().unwrap().gnf()),
+            sequents("true -> false & true".parse::<Fof>().unwrap().gnf()),
         );
         assert_debug_string(
             "[[] -> []]",
-            sequents("true -> true & false".parse::<FOF>().unwrap().gnf()),
+            sequents("true -> true & false".parse::<Fof>().unwrap().gnf()),
         );
         assert_debug_string(
             "[]",
-            sequents("true -> true | false".parse::<FOF>().unwrap().gnf()),
+            sequents("true -> true | false".parse::<Fof>().unwrap().gnf()),
         );
         assert_debug_string(
             "[]",
-            sequents("true -> false | true".parse::<FOF>().unwrap().gnf()),
+            sequents("true -> false | true".parse::<Fof>().unwrap().gnf()),
         );
         assert_debug_string(
             "[[P(x)] -> [[Q(x)]]]",
-            sequents("P(x) -> Q(x)".parse::<FOF>().unwrap().gnf()),
+            sequents("P(x) -> Q(x)".parse::<Fof>().unwrap().gnf()),
         );
         assert_debug_string(
             // Note: only range restricted geometric formulae get contracted
             "[[P(x), Q(x)] -> [[Q(y)]]]",
-            sequents("P(x) & Q(x) -> Q(y)".parse::<FOF>().unwrap().gnf()),
+            sequents("P(x) & Q(x) -> Q(y)".parse::<Fof>().unwrap().gnf()),
         );
         assert_debug_string(
             "[[P(x, z), Q(x)] -> [[Q(x)], [R(z)]], [P(x, z), Q(x)] -> [[Q(x)], [S(z)]]]",
             sequents(
                 "P(x, z) & Q(x) -> Q(x) | (R(z) & S(z))"
-                    .parse::<FOF>()
+                    .parse::<Fof>()
                     .unwrap()
                     .gnf(),
             ),
@@ -1079,14 +1077,14 @@ mod test_basic {
 "[[D(x, y, z)] -> [[P(x)], [P(y)], [P(z)]], [D(x, y, z)] -> [[P(x)], [P(y)], [Q(z)]], [D(x, y, z)] -> [[P(x)], [P(z)], [Q(y)]], [D(x, y, z)] -> [[P(x)], [Q(y)], [Q(z)]], [D(x, y, z)] -> [[P(y)], [P(z)], [Q(x)]], [D(x, y, z)] -> [[P(y)], [Q(x)], [Q(z)]], [D(x, y, z)] -> [[P(z)], [Q(x)], [Q(y)]], [D(x, y, z)] -> [[Q(x)], [Q(y)], [Q(z)]]]",
             sequents(
                 "D(x, y, z) -> (P(x) & Q(x)) | (P(y) & Q(y)) | (P(z) & Q(z))"
-                    .parse::<FOF>()
+                    .parse::<Fof>()
                     .unwrap()
                     .gnf(),
             ),
         );
     }
 
-    fn run(theory: &Theory<FOF>) -> Vec<BasicModel> {
+    fn run(theory: &Theory<Fof>) -> Vec<BasicModel> {
         let pre_processor = BasicPreProcessor;
         let (sequents, init_model) = pre_processor.pre_process(theory);
 
@@ -1099,7 +1097,7 @@ mod test_basic {
         chase_all(&mut scheduler, &evaluator, bounder)
     }
 
-    fn run_domain_bounded(theory: &Theory<FOF>, bound: usize) -> Vec<BasicModel> {
+    fn run_domain_bounded(theory: &Theory<Fof>, bound: usize) -> Vec<BasicModel> {
         let pre_processor = BasicPreProcessor;
         let (sequents, init_model) = pre_processor.pre_process(theory);
         let evaluator = BasicEvaluator;

razor-chase/src/chase/impl/batch.rs

@@ -186,7 +186,7 @@ fn make_observe_literal(
 // variables of a sequent. It mutates the given a list of indices, corresponding to mapping of each
 // position to an element of a domain to the next assignment. Returns true if a next assignment
 // exists and false otherwise.
-fn next_assignment(vec: &mut Vec<usize>, last: usize) -> bool {
+fn next_assignment(vec: &mut [usize], last: usize) -> bool {
     for item in vec.iter_mut() {
         if *item != last {
             *item += 1;
@@ -211,7 +211,7 @@ mod test_batch {
         bounder::DomainSize, chase_all, scheduler::FIFO, strategy::Linear, Scheduler,
     };
     use crate::test_prelude::*;
-    use razor_fol::syntax::{Theory, FOF};
+    use razor_fol::syntax::{Fof, Theory};
     use std::collections::HashSet;
 
     static IGNORE_TEST: [&'static str; 1] = ["thy24.raz"];
@@ -263,7 +263,7 @@ mod test_batch {
         }
     }
 
-    fn run(theory: &Theory<FOF>) -> Vec<ColModel> {
+    fn run(theory: &Theory<Fof>) -> Vec<ColModel> {
         use crate::chase::r#impl::collapse::ColPreProcessor;
         use crate::chase::PreProcessor;