diff --git a/razor-chase/src/chase/impl/relational.rs b/razor-chase/src/chase/impl/relational.rs index 5630c6a..a567686 100644 --- a/razor-chase/src/chase/impl/relational.rs +++ b/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 }, } diff --git a/razor-chase/src/chase/impl/relational/preprocessor.rs b/razor-chase/src/chase/impl/relational/preprocessor.rs index 4dcefc0..02c625c 100644 --- a/razor-chase/src/chase/impl/relational/preprocessor.rs +++ b/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,35 +35,18 @@ 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() }; @@ -74,21 +54,6 @@ impl PreProcessorEx for PreProcessor { } } -// 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 { use razor_fol::formula; diff --git a/razor-chase/src/chase/impl/relational/sequent.rs b/razor-chase/src/chase/impl/relational/sequent.rs index 39f2086..befda41 100644 --- a/razor-chase/src/chase/impl/relational/sequent.rs +++ b/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 { 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 = (&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 = 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 { + 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 { + 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>, Error> { use std::convert::TryFrom;