construct sequent branches before equality expansion of the rhs

this change removes unnecessary atoms from branches to improve performance
creating a new sequent now returns a result type instead of panicking immediately

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

@@ -181,6 +181,12 @@ pub enum Error {
         source: codd::Error,
     },
 
+    #[error("syntactic transformation error")]
+    TransformError {
+        #[from]
+        source: razor_fol::transform::Error,
+    },
+
     #[error("cannot create witness term for symbol `{symbol:?}`")]
     BadWitnessTerm { symbol: String },
 
@@ -193,7 +199,7 @@ pub enum Error {
     #[error("cannot build sequent from formula `{}`", .formula.to_string())]
     BadSequentFormula { formula: razor_fol::syntax::Formula },
 
-    #[error("cannot build sequent from formula `{name:?}`")]
+    #[error("invalid attribute name `{name:?}`")]
     BadAttributeName { name: String },
 }
 

razor-chase/src/chase/impl/relational/preprocessor.rs

@@ -1,10 +1,7 @@
-use super::{constants::*, memo::ViewMemo, model::Model, sequent::Sequent};
+use super::{memo::ViewMemo, model::Model, sequent::Sequent};
 use crate::chase::PreProcessorEx;
 use itertools::Itertools;
-use razor_fol::{
-    syntax::{symbol::Generator, Formula, Sig, Term, Theory, V},
-    transform::relationalize,
-};
+use razor_fol::syntax::{Formula, Sig, Term, Theory, V};
 
 /// Is a [`PreProcessorEx`] instance that converts the input theory to a vector of [`Sequent`].
 /// This is done by the standard conversion to geometric normal form followed by relationalization.
@@ -38,57 +35,25 @@ impl PreProcessorEx for PreProcessor {
 
         let mut model = Model::new(&theory.signature());
 
-        let relationalized = theory
-            .formulae()
-            .into_iter()
-            .map(|f| match f {
-                Formula::Implies { left, right } => {
-                    let left = relationalizer().relationalize(&left).expect(&format!(
-                        "internal error: failed to relationalize formula: {}",
-                        left
-                    ));
-                    let right = relationalizer().relationalize(&right).expect(&format!(
-                        "internal error: failed to relationalize formula: {}",
-                        right
-                    ));
-                    (left, right)
-                }
-                _ => panic!(format!("internal error: unexpected formula: {}", f)),
-            })
-            .collect_vec();
-
         let sequents = if self.memoize {
             let mut memo = ViewMemo::new(model.database_mut());
-            relationalized
+            theory
+                .formulae()
                 .into_iter()
-                .map(|(left, right)| Sequent::new(&Formula::implies(left, right), Some(&mut memo)))
+                .map(|fmla| Sequent::new(&fmla, Some(&mut memo)).unwrap())
                 .collect()
         } else {
-            relationalized
+            theory
+                .formulae()
                 .into_iter()
-                .map(|(left, right)| Sequent::new(&Formula::implies(left, right), None))
+                .map(|fmla| Sequent::new(&fmla, None).unwrap())
                 .collect()
         };
 
         (sequents, model)
     }
 }
 
-// Create consistent `Relationalizer` instances:
-fn relationalizer() -> relationalize::Relationalizer {
-    let mut result = relationalize::Relationalizer::new();
-    result.set_equality_symbol(EQUALITY);
-    result.set_flattening_generator(Generator::new().set_prefix(EXISTENTIAL_PREFIX));
-    result.set_equality_generator(
-        Generator::new()
-            .set_prefix(EQUATIONAL_PREFIX)
-            .set_delimiter(SEPERATOR),
-    );
-    result.set_predicate_generator(Generator::new().set_prefix(FUNCTIONAL_PREDICATE_PREFIX));
-
-    result
-}
-
 // Equality axioms:
 fn equality_axioms() -> Vec<Formula> {
     use razor_fol::formula;

razor-chase/src/chase/impl/relational/sequent.rs

@@ -8,7 +8,7 @@ use super::{
 use crate::chase::SequentTrait;
 use codd::expression as rel_exp;
 use razor_fol::{
-    syntax::{Formula, Pred, Term, C, F, V},
+    syntax::{symbol::Generator, Formula, Pred, Term, C, F},
     transform::relationalize,
 };
 
@@ -88,91 +88,78 @@ impl Sequent {
         &self.attributes
     }
 
-    pub(super) fn new(formula: &Formula, memo: Option<&mut ViewMemo>) -> Self {
+    pub(super) fn new(formula: &Formula, memo: Option<&mut ViewMemo>) -> Result<Self, Error> {
         use itertools::Itertools;
 
-        if let Formula::Implies { left, right } = formula {
-            let right_universals: AttributeList = AttributeList::try_from_formula(right)
-                .expect(&format!(
-                    "internal error: failed to compute attributes for formula: {}",
-                    right
-                ))
-                .universals();
-
-            let range: Vec<V> = (&right_universals).into();
-
-            let rr_left = relationalize::range_restrict(left, &range, DOMAIN).expect(&format!(
-                "internal error: failed to apply range restriction on formula: {}",
-                left
-            ));
-            let rr_right = relationalize::range_restrict(right, &range, DOMAIN).expect(&format!(
-                "internal error: failed to apply range restriction on formula: {}",
-                right
-            ));
-
-            let left_attrs = AttributeList::try_from_formula(&rr_left)
-                .expect(&format!(
-                    "internal error: failed to compute attributes for formula: {}",
-                    rr_left
-                ))
-                .intersect(&right_universals);
-
-            // Removing duplicate atoms is necessary for correctness:
-            let branches: Vec<Branch> = build_branches(&rr_right)
-                .expect("internal error: failed to process sequent")
-                .into_iter()
-                .map(|branch| branch.into_iter().unique().collect())
-                .collect();
-
-            // Is it a sequent with `true` in the head:
-            let branches = if branches.iter().any(|branch| branch.is_empty()) {
-                vec![vec![]]
+        #[inline]
+        fn implies_parts(formula: &Formula) -> Result<(&Formula, &Formula), Error> {
+            if let Formula::Implies { left, right } = formula {
+                Ok((left, right))
             } else {
-                branches
-            };
+                Err(Error::BadSequentFormula {
+                    formula: formula.clone(),
+                })
+            }
+        }
 
-            let (left_expr, right_expr) = if let Some(memo) = memo {
-                (
-                    memo.make_expression(&rr_left, &left_attrs),
-                    memo.make_expression(&rr_right, &left_attrs),
-                )
-            } else {
-                (
-                    make_expression(&rr_left, &left_attrs),
-                    make_expression(&rr_right, &left_attrs),
-                )
-            };
+        let (left, right) = implies_parts(formula)?;
 
-            let left_expression = left_expr.expect(&format!(
-                "internal error: failed to compute relational expression for formula: {}",
-                rr_left
-            ));
-            let right_expression = right_expr.expect(&format!(
-                "internal error: failed to compute relational expression for formula: {}",
-                rr_right
-            ));
-
-            let expression = match &branches[..] {
-                [] => left_expression,
-                _ => match &branches[0][..] {
-                    [] => rel_exp::Mono::Empty(rel_exp::Empty::new()),
-                    _ => rel_exp::Mono::Difference(rel_exp::Difference::new(
-                        left_expression.boxed(),
-                        right_expression.boxed(),
-                    )),
-                },
-            };
+        // relationalize and expand equalities of `left` and `right`:
+        let left_er = expand_equality(&relationalize(left)?)?;
+        let right_r = relationalize(right)?;
+        let branches = build_branches(right_r.formula())?; // relationalized right is enough for building branches
+        let right_er = expand_equality(&right_r)?;
 
-            Self {
-                branches,
-                attributes: left_attrs,
-                expression,
-                body_formula: rr_left.clone(),
-                head_formula: rr_right.clone(),
-            }
+        let right_attrs = AttributeList::try_from_formula(right_er.formula())?.universals();
+        let range = Vec::from(&right_attrs);
+
+        // apply range restriction:
+        let left_rr = relationalize::range_restrict(&left_er, &range, DOMAIN)?;
+        let right_rr = relationalize::range_restrict(&right_er, &range, DOMAIN)?;
+
+        let left_attrs =
+            AttributeList::try_from_formula(left_rr.formula())?.intersect(&right_attrs);
+
+        let branches = if branches.iter().any(|branch| branch.is_empty()) {
+            vec![vec![]] // logically the right is true
         } else {
-            panic!("something is wrong: expecting a geometric sequent in standard form")
-        }
+            // Remove duplicate atoms is necessary for correctness:
+            branches
+                .into_iter()
+                .map(|branch| branch.into_iter().unique().collect())
+                .collect()
+        };
+
+        let (left_expr, right_expr) = if let Some(memo) = memo {
+            (
+                memo.make_expression(left_rr.formula(), &left_attrs)?,
+                memo.make_expression(right_rr.formula(), &left_attrs)?,
+            )
+        } else {
+            (
+                make_expression(left_rr.formula(), &left_attrs)?,
+                make_expression(right_rr.formula(), &left_attrs)?,
+            )
+        };
+
+        let expression = match &branches[..] {
+            [] => left_expr,
+            _ => match &branches[0][..] {
+                [] => rel_exp::Mono::Empty(rel_exp::Empty::new()),
+                _ => rel_exp::Mono::Difference(rel_exp::Difference::new(
+                    left_expr.boxed(),
+                    right_expr.boxed(),
+                )),
+            },
+        };
+
+        Ok(Self {
+            branches,
+            attributes: left_attrs,
+            expression,
+            body_formula: left.clone(),
+            head_formula: right.clone(),
+        })
     }
 }
 
@@ -186,6 +173,32 @@ impl SequentTrait for Sequent {
     }
 }
 
+// Create consistent `Relationalizer` instances:
+fn relationalize(formula: &Formula) -> Result<relationalize::Relational, Error> {
+    let mut relationalizer = relationalize::Relationalizer::new();
+    relationalizer.set_equality_symbol(EQUALITY);
+    relationalizer.set_flattening_generator(Generator::new().set_prefix(EXISTENTIAL_PREFIX));
+    relationalizer
+        .set_predicate_generator(Generator::new().set_prefix(FUNCTIONAL_PREDICATE_PREFIX));
+
+    relationalizer.transform(formula).map_err(|e| e.into())
+}
+
+// Create consistent `EqualityExpander` instances:
+fn expand_equality(
+    formula: &relationalize::Relational,
+) -> Result<relationalize::Relational, Error> {
+    let mut equality_expander = relationalize::EqualityExpander::new();
+    equality_expander.set_equality_symbol(EQUALITY);
+    equality_expander.set_equality_generator(
+        Generator::new()
+            .set_prefix(EQUATIONAL_PREFIX)
+            .set_delimiter(SEPERATOR),
+    );
+
+    equality_expander.transform(formula).map_err(|e| e.into())
+}
+
 fn build_branches(formula: &Formula) -> Result<Vec<Vec<Atom>>, Error> {
     use std::convert::TryFrom;