From bd377bfd63d72fd4cfe2b0935061730c3ad56c3c Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 16 Oct 2024 12:00:01 +0200 Subject: [PATCH 1/8] Lto does not seem to work anyway --- libraries/mcrl2-sys/build.rs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/libraries/mcrl2-sys/build.rs b/libraries/mcrl2-sys/build.rs index d3a3f37..2db64aa 100644 --- a/libraries/mcrl2-sys/build.rs +++ b/libraries/mcrl2-sys/build.rs @@ -48,10 +48,6 @@ fn add_cpp_flags(build: &mut Build) { #[cfg(unix)] { build.flag_if_supported("-std=c++17"); - // build.flag_if_supported("-flto=auto"); - // build.flag_if_supported("-fno-fat-lto-objects"); - // build.flag_if_supported("-fuse-linker-plugin"); - // build.flag_if_supported("-fuse-ld=lld"); } } From a9b50fefa1a00fc554e3fc65101b3fbf535cd0d4 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 16 Oct 2024 21:22:47 +0200 Subject: [PATCH 2/8] Replaced semi compressed trees by a stack construction --- libraries/sabre/src/utilities/term_stack.rs | 418 ++++++++++++++++++++ 1 file changed, 418 insertions(+) create mode 100644 libraries/sabre/src/utilities/term_stack.rs diff --git a/libraries/sabre/src/utilities/term_stack.rs b/libraries/sabre/src/utilities/term_stack.rs new file mode 100644 index 0000000..b45969f --- /dev/null +++ b/libraries/sabre/src/utilities/term_stack.rs @@ -0,0 +1,418 @@ +use std::fmt; + +use ahash::{HashMap, HashMapExt}; +use log::trace; +use mcrl2::{aterm::{ATermRef, Markable, Protected, TermPool, Todo}, data::{is_data_expression, is_data_machine_number, is_data_variable, DataApplication, DataExpression, DataExpressionRef, DataFunctionSymbolRef, DataVariable}}; + +use crate::{utilities::InnermostStack, Rule}; + +use super::{ExplicitPosition, PositionIterator}; + + +/// A stack used to represent a term with free variables that can be constructed +/// efficiently. +/// +/// It stores as much as possible in the term pool. Due to variables it cannot +/// be fully compressed. For variables it stores the position in the lhs of a +/// rewrite rule where the concrete term can be found that will replace the +/// variable. +/// +#[derive(Hash, Debug, PartialEq, Eq, PartialOrd, Ord)] +pub struct TermStack { + /// The innermost rewrite stack for the right hand side and the positions that must be added to the stack. + pub(crate) innermost_stack: Protected>, + pub(crate) variables: Vec<(ExplicitPosition, usize)>, + pub(crate) stack_size: usize, +} + +#[derive(Hash, Eq, PartialEq, Ord, PartialOrd, Debug)] +pub enum Config { + /// Rewrite the top of the stack and put result at the given index. + Rewrite(usize), + /// Constructs function symbol with given arity at the given index. + Construct(DataFunctionSymbolRef<'static>, usize, usize), + /// A concrete term to be placed at the current position in the stack. + Term(DataExpressionRef<'static>, usize), + /// Yields the given index as returned term. + Return(), +} + +impl Markable for Config { + fn mark(&self, todo: Todo<'_>) { + if let Config::Construct(t, _, _) = self { + let t: ATermRef<'_> = t.copy().into(); + t.mark(todo); + } + } + + fn contains_term(&self, term: &ATermRef<'_>) -> bool { + if let Config::Construct(t, _, _) = self { + term == &>::into(t.copy()) + } else { + false + } + } + + fn len(&self) -> usize { + if let Config::Construct(_, _, _) = self { + 1 + } else { + 0 + } + } +} + +impl fmt::Display for Config { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Config::Rewrite(result) => write!(f, "Rewrite({})", result), + Config::Construct(symbol, arity, result) => { + write!(f, "Construct({}, {}, {})", symbol, arity, result) + } + Config::Term(term, result) => { + write!(f, "Term({}, {})", term, result) + } + Config::Return() => write!(f, "Return()"), + } + } +} + +impl TermStack { + /// Construct a new right-hand stack for a given equation/rewrite rule. + pub fn new(rule: &Rule) -> TermStack { + Self::from_term(&rule.rhs.copy(), &create_var_map(&rule.lhs.copy().into())) + } + + /// + pub fn from_term(term: &DataExpressionRef, var_map: &HashMap) -> TermStack { + // Compute the extra information for the InnermostRewriter. + let mut innermost_stack: Protected> = Protected::new(vec![]); + let mut variables = vec![]; + let mut stack_size = 0; + + for (term, position) in PositionIterator::new(term.copy().into()) { + if let Some(index) = position.indices.last() { + if *index == 1 { + continue; // Skip the function symbol. + } + } + + if is_data_variable(&term) { + variables.push(( + var_map + .get(&term.protect()) + .expect( + "All variables in the right hand side must occur in the left hand side", + ) + .clone(), + stack_size, + )); + stack_size += 1; + } else if is_data_machine_number(&term) { + // Skip SortId(@NoValue) and OpId + } else if is_data_expression(&term) { + let t: DataExpressionRef = term.into(); + let arity = t.data_arguments().len(); + let mut write = innermost_stack.write(); + let symbol = write.protect(&t.data_function_symbol().into()); + write.push(Config::Construct(symbol.into(), arity, stack_size)); + stack_size += 1; + } else { + // Skip intermediate terms such as UntypeSortUnknown. + } + } + + TermStack { + innermost_stack, + stack_size, + variables, + } + } + + pub fn evaluate(&self, tp: &mut TermPool, term: &ATermRef) -> DataExpression { + let mut builder = TermStackBuilder::new(); + self.evaluate_with(tp, term, &mut builder) + } + + /// Evaluate the rhs stack for the given term and returns the result. + pub fn evaluate_with(&self, tp: &mut TermPool, term: &ATermRef, builder: &mut TermStackBuilder) -> DataExpression { + let stack = &mut builder.stack; + { + let mut write = stack.terms.write(); + write.clear(); + write.push(DataExpressionRef::default()); + } + + InnermostStack::integrate( + &mut stack.configs.write(), + &mut stack.terms.write(), + self, + &DataExpressionRef::from(term.copy()), + 0, + ); + loop { + trace!("{}", stack); + + let mut write_configs = stack.configs.write(); + if let Some(config) = write_configs.pop() { + match config { + Config::Construct(symbol, arity, index) => { + // Take the last arity arguments. + let mut write_terms = stack.terms.write(); + let length = write_terms.len(); + + let arguments = &write_terms[length - arity..]; + + let term: DataExpression = if arguments.is_empty() { + symbol.protect().into() + } else { + DataApplication::new(tp, &symbol.copy(), arguments).into() + }; + + // Add the term on the stack. + write_terms.drain(length - arity..); + let t = write_terms.protect(&term); + write_terms[index] = t.into(); + }, + Config::Term(term, index) => { + let mut write_terms = stack.terms.write(); + let t = write_terms.protect(&term); + write_terms[index] = t.into(); + } + Config::Rewrite(_) => { + unreachable!("This case should not happen"); + } + Config::Return() => { + unreachable!("This case should not happen"); + } + } + } else { + break; + } + } + + debug_assert!( + stack.terms.read().len() == 1, + "Expect exactly one term on the result stack" + ); + + let mut write_terms = stack.terms.write(); + + write_terms + .pop() + .expect("The result should be the last element on the stack") + .protect() + } + + /// Used to check if a subterm is duplicated, for example "times(s(x), y) = + /// plus(y, times(x,y))" is duplicating. + pub(crate) fn contains_duplicate_var_references(&self) -> bool { + let mut variables = self.variables.clone(); + variables.sort_by_key(|(pos, _)| pos.clone()); + let len = variables.len(); + variables.dedup(); + + len == variables.len() + } +} + +impl Clone for TermStack { + fn clone(&self) -> Self { + // TODO: It would make sense if Protected could implement Clone. + let mut innermost_stack: Protected> = Protected::new(vec![]); + + let mut write = innermost_stack.write(); + for t in self.innermost_stack.read().iter() { + match t { + Config::Rewrite(x) => write.push(Config::Rewrite(*x)), + Config::Construct(f, x, y) => { + let f = write.protect(&f.copy().into()); + write.push(Config::Construct(f.into(), *x, *y)); + } + Config::Term(t, y) => { + let f = write.protect(&t.copy().into()); + write.push(Config::Term(f.into(), *y)); + } + Config::Return() => write.push(Config::Return()), + } + } + drop(write); + + Self { + variables: self.variables.clone(), + stack_size: self.stack_size, + innermost_stack, + } + } +} + + +pub struct TermStackBuilder { + stack: InnermostStack, + +} + +impl TermStackBuilder { + pub fn new() -> Self { + Self { + stack: InnermostStack::default(), + } + } +} + +/// Create a mapping of variables to their position in the given term +pub fn create_var_map(t: &ATermRef) -> HashMap { + let mut result = HashMap::new(); + + for (term, position) in PositionIterator::new(t.copy()) { + if is_data_variable(&term) { + result.insert(term.protect().into(), position.clone()); + } + } + result +} + +#[cfg(test)] +mod tests { + use super::*; + use ahash::AHashSet; + use mcrl2::aterm::{apply, ATerm, TermPool}; + use mcrl2::data::DataFunctionSymbol; + + use crate::test_utility::create_rewrite_rule; + use crate::utilities::to_untyped_data_expression; + + use test_log::test; + + /// Converts a slice of static strings into a set of owned strings + /// + /// example: + /// make_var_map(["x"]) + fn var_map(vars: &[&str]) -> AHashSet { + AHashSet::from_iter(vars.iter().map(|x| String::from(*x))) + } + + /// Convert terms in variables to a [DataVariable]. + pub fn convert_variables(tp: &mut TermPool, t: &ATerm, variables: &AHashSet) -> ATerm { + apply(tp, t, &|tp, arg| { + if variables.contains(arg.get_head_symbol().name()) { + // Convert a constant variable, for example 'x', into an untyped variable. + Some(DataVariable::new(tp, &arg.get_head_symbol().name()).into()) + } else { + None + } + }) + } + + #[test] + fn test_rhs_stack() { + let mut tp = TermPool::new(); + + let rhs_stack = TermStack::new( + &create_rewrite_rule(&mut tp, "fact(s(N))", "times(s(N), fact(N))", &["N"]).unwrap(), + ); + let mut expected = Protected::new(vec![]); + + let mut write = expected.write(); + let t = write.protect(&DataFunctionSymbol::new(&mut tp, "times").copy().into()); + write.push(Config::Construct(t.into(), 2, 0)); + + let t = write.protect(&DataFunctionSymbol::new(&mut tp, "s").copy().into()); + write.push(Config::Construct(t.into(), 1, 1)); + + let t = write.protect(&DataFunctionSymbol::new(&mut tp, "fact").copy().into()); + write.push(Config::Construct(t.into(), 1, 2)); + drop(write); + + // Check if the resulting construction succeeded. + assert_eq!( + rhs_stack.innermost_stack, expected, + "The resulting config stack is not as expected" + ); + + assert_eq!(rhs_stack.stack_size, 5, "The stack size does not match"); + + // Test the evaluation + let lhs = tp.from_string("fact(s(a))").unwrap(); + let lhs_expression = to_untyped_data_expression(&mut tp, &lhs, &AHashSet::new()); + + let rhs = tp.from_string("times(s(a), fact(a))").unwrap(); + let rhs_expression = to_untyped_data_expression(&mut tp, &rhs, &AHashSet::new()); + + assert_eq!( + rhs_stack.evaluate(&mut tp, &lhs_expression), + rhs_expression, + "The rhs stack does not evaluate to the expected term" + ); + } + + #[test] + fn test_rhs_stack_variable() { + let mut tp = TermPool::new(); + + let rhs = TermStack::new(&create_rewrite_rule(&mut tp, "f(x)", "x", &["x"]).unwrap()); + + // Check if the resulting construction succeeded. + assert!( + rhs.innermost_stack.read().is_empty(), + "The resulting config stack is not as expected" + ); + + assert_eq!(rhs.stack_size, 1, "The stack size does not match"); + } + + #[test] + fn test_evaluation() { + let mut tp = TermPool::new(); + let t_rhs = { + let tmp = tp.from_string("f(f(a,a),x)").unwrap(); + to_untyped_data_expression(&mut tp, &tmp, &AHashSet::from([String::from("x")])) + }; + + let t = tp.from_string("g(b)").unwrap(); + let t_lhs = to_untyped_data_expression(&mut tp, &t, &AHashSet::new()); + + // Make a variable map with only x@1. + let mut map = HashMap::new(); + map.insert(DataVariable::new(&mut tp, "x"), ExplicitPosition::new(&[1])); + + let sctt = TermStack::from_term(&t_rhs.copy(), &map); + + let t = tp.from_string("f(f(a,a),b)").unwrap(); + let t_expected = to_untyped_data_expression(&mut tp, &t, &AHashSet::new()); + + assert_eq!(sctt.evaluate(&mut tp, &t_lhs), t_expected); + } + + #[test] + fn test_create_varmap() { + let mut tp = TermPool::new(); + let t = { + let tmp = tp.from_string("f(x,x)").unwrap(); + convert_variables(&mut tp, &tmp, &AHashSet::from([String::from("x")])) + }; + let x = DataVariable::new(&mut tp, "x"); + + let map = create_var_map(&t); + assert!(map.contains_key(&x)); + } + + #[test] + fn test_is_duplicating() { + let mut tp = TermPool::new(); + let t_rhs = { + let tmp = tp.from_string("f(x,x)").unwrap(); + to_untyped_data_expression(&mut tp, &tmp, &AHashSet::from([String::from("x")])) + }; + + // Make a variable map with only x@1. + let mut map = HashMap::new(); + map.insert(DataVariable::new(&mut tp, "x"), ExplicitPosition::new(&[1])); + + let sctt = TermStack::from_term(&t_rhs.copy(), &map); + assert!( + sctt.contains_duplicate_var_references(), + "This sctt is duplicating" + ); + } +} From e040d3746480be206741cd4f68c47f9d5fd30c1a Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 16 Oct 2024 21:23:55 +0200 Subject: [PATCH 3/8] Used the term stack in the innermost rewriter. --- libraries/sabre/src/innermost_rewriter.rs | 28 +++++---- .../sabre/src/utilities/innermost_stack.rs | 61 ++++--------------- 2 files changed, 28 insertions(+), 61 deletions(-) diff --git a/libraries/sabre/src/innermost_rewriter.rs b/libraries/sabre/src/innermost_rewriter.rs index 3d093fa..8bce979 100644 --- a/libraries/sabre/src/innermost_rewriter.rs +++ b/libraries/sabre/src/innermost_rewriter.rs @@ -19,8 +19,8 @@ use crate::set_automaton::SetAutomaton; use crate::utilities::Config; use crate::utilities::InnermostStack; use crate::utilities::PositionIndexed; -use crate::utilities::RHSStack; -use crate::utilities::SCCTBuilder; +use crate::utilities::TermStack; +use crate::utilities::TermStackBuilder; use crate::RewriteEngine; use crate::RewriteSpecification; use crate::RewritingStatistics; @@ -57,7 +57,7 @@ impl InnermostRewriter { apma, tp: tp.clone(), stack: InnermostStack::default(), - builder: SCCTBuilder::new(), + builder: TermStackBuilder::new(), } } @@ -78,7 +78,7 @@ impl InnermostRewriter { pub(crate) fn rewrite_aux( tp: &mut TermPool, stack: &mut InnermostStack, - builder: &mut SCCTBuilder, + builder: &mut TermStackBuilder, stats: &mut RewritingStatistics, automaton: &SetAutomaton, input_term: DataExpression, @@ -162,7 +162,7 @@ impl InnermostRewriter { &mut write_configs, &mut write_terms, &annotation.rhs_stack, - &term, + &term.copy(), index, ); stats.rewrite_steps += 1; @@ -174,6 +174,9 @@ impl InnermostRewriter { write_terms[index] = t.into(); } } + }, + Config::Term(_, _) => { + unreachable!("This case should not happen"); } Config::Return() => { let mut write_terms = stack.terms.write(); @@ -193,6 +196,7 @@ impl InnermostRewriter { match x { Config::Construct(_, _, result) => index == *result, Config::Rewrite(result) => index == *result, + Config::Term(_, result) => index == *result, Config::Return() => true, } }), @@ -208,7 +212,7 @@ impl InnermostRewriter { fn find_match<'a>( tp: &mut TermPool, stack: &mut InnermostStack, - builder: &mut SCCTBuilder, + builder: &mut TermStackBuilder, stats: &mut RewritingStatistics, automaton: &'a SetAutomaton, t: &ATermRef<'_>, @@ -252,15 +256,15 @@ impl InnermostRewriter { fn check_conditions( tp: &mut TermPool, stack: &mut InnermostStack, - builder: &mut SCCTBuilder, + builder: &mut TermStackBuilder, stats: &mut RewritingStatistics, automaton: &SetAutomaton, announcement: &AnnouncementInnermost, t: &ATermRef<'_>, ) -> bool { for c in &announcement.conditions { - let rhs: DataExpression = c.semi_compressed_rhs.evaluate_with(builder, t, tp).into(); - let lhs: DataExpression = c.semi_compressed_lhs.evaluate_with(builder, t, tp).into(); + let rhs: DataExpression = c.semi_compressed_rhs.evaluate_with(tp, t, builder).into(); + let lhs: DataExpression = c.semi_compressed_lhs.evaluate_with(tp, t, builder).into(); let rhs_normal = InnermostRewriter::rewrite_aux(tp, stack, builder, stats, automaton, rhs); let lhs_normal = if &lhs == tp.true_term() { @@ -284,7 +288,7 @@ pub struct InnermostRewriter { tp: Rc>, apma: SetAutomaton, stack: InnermostStack, - builder: SCCTBuilder, + builder: TermStackBuilder, } pub(crate) struct AnnouncementInnermost { @@ -295,7 +299,7 @@ pub(crate) struct AnnouncementInnermost { conditions: Vec, /// The innermost stack for the right hand side of the rewrite rule. - rhs_stack: RHSStack, + rhs_stack: TermStack, } impl AnnouncementInnermost { @@ -303,7 +307,7 @@ impl AnnouncementInnermost { AnnouncementInnermost { conditions: extend_conditions(rule), equivalence_classes: derive_equivalence_classes(rule), - rhs_stack: RHSStack::new(rule), + rhs_stack: TermStack::new(rule), } } } diff --git a/libraries/sabre/src/utilities/innermost_stack.rs b/libraries/sabre/src/utilities/innermost_stack.rs index fe4a0b8..e541bec 100644 --- a/libraries/sabre/src/utilities/innermost_stack.rs +++ b/libraries/sabre/src/utilities/innermost_stack.rs @@ -2,25 +2,15 @@ use std::fmt; use itertools::Itertools; use mcrl2::aterm::ATermRef; -use mcrl2::aterm::Markable; use mcrl2::aterm::Protected; use mcrl2::aterm::Protector; -use mcrl2::aterm::TermPool; -use mcrl2::aterm::Todo; -use mcrl2::data::is_data_expression; -use mcrl2::data::is_data_machine_number; -use mcrl2::data::is_data_variable; -use mcrl2::data::DataApplication; -use mcrl2::data::DataExpression; use mcrl2::data::DataExpressionRef; use mcrl2::data::DataFunctionSymbolRef; use crate::utilities::PositionIndexed; -use crate::Rule; -use super::create_var_map; -use super::ExplicitPosition; -use super::PositionIterator; +use super::Config; +use super::TermStack; use log::trace; @@ -38,8 +28,8 @@ impl InnermostStack { pub fn integrate( write_configs: &mut Protector>, write_terms: &mut Protector>>, - rhs_stack: &RHSStack, - term: &DataExpression, + rhs_stack: &TermStack, + term: &DataExpressionRef, result_index: usize, ) { // TODO: This ignores the first element of the stack, but that is kind of difficult to deal with. @@ -61,6 +51,10 @@ impl InnermostStack { InnermostStack::add_result(write_configs, symbol.copy(), *arity, top_of_stack + offset - 1); } } + Config::Term(term, index) => { + let term = write_configs.protect(term); + write_configs.push(Config::Term(term.into(), *index)); + } Config::Rewrite(_) => { unreachable!("This case should not happen"); } @@ -121,41 +115,6 @@ impl InnermostStack { } } -#[derive(Hash, Eq, PartialEq, Ord, PartialOrd, Debug)] -pub enum Config { - /// Rewrite the top of the stack and put result at the given index. - Rewrite(usize), - /// Constructs function symbol with given arity at the given index. - Construct(DataFunctionSymbolRef<'static>, usize, usize), - /// Yields the given index as returned term. - Return(), -} - -impl Markable for Config { - fn mark(&self, todo: Todo<'_>) { - if let Config::Construct(t, _, _) = self { - let t: ATermRef<'_> = t.copy().into(); - t.mark(todo); - } - } - - fn contains_term(&self, term: &ATermRef<'_>) -> bool { - if let Config::Construct(t, _, _) = self { - term == &>::into(t.copy()) - } else { - false - } - } - - fn len(&self) -> usize { - if let Config::Construct(_, _, _) = self { - 1 - } else { - 0 - } - } -} - impl fmt::Display for InnermostStack { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { writeln!(f, "Terms: [")?; @@ -174,6 +133,7 @@ impl fmt::Display for InnermostStack { } write!(f, "]") } +<<<<<<< HEAD } impl fmt::Display for Config { @@ -393,3 +353,6 @@ mod tests { assert_eq!(rhs.stack_size, 1, "The stack size does not match"); } } +======= +} +>>>>>>> c86ebbb (Used the term stack in the innermost rewriter.) From e40e741bcf976d6557da31506410547329fe9519 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 16 Oct 2024 21:24:10 +0200 Subject: [PATCH 4/8] Replaced conditions by the term stack --- libraries/sabre/src/matching/conditions.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/libraries/sabre/src/matching/conditions.rs b/libraries/sabre/src/matching/conditions.rs index 3c1c07f..740c91a 100644 --- a/libraries/sabre/src/matching/conditions.rs +++ b/libraries/sabre/src/matching/conditions.rs @@ -1,5 +1,5 @@ use crate::utilities::create_var_map; -use crate::utilities::SemiCompressedTermTree; +use crate::utilities::TermStack; use crate::Rule; /// This is a [Rule] condition stored as semi compressed trees such that they can be @@ -7,8 +7,8 @@ use crate::Rule; #[derive(Hash, Clone, Eq, PartialEq, Ord, PartialOrd, Debug)] pub struct EMACondition { /// Conditions lhs and rhs are stored in the term pool as much as possible with a SemiCompressedTermTree - pub semi_compressed_lhs: SemiCompressedTermTree, - pub semi_compressed_rhs: SemiCompressedTermTree, + pub semi_compressed_lhs: TermStack, + pub semi_compressed_rhs: TermStack, /// whether the lhs and rhs should be equal or different pub equality: bool, @@ -16,13 +16,13 @@ pub struct EMACondition { /// Computes the extended condition from a given rewrite rule. pub fn extend_conditions(rule: &Rule) -> Vec { - let var_map = create_var_map(&rule.lhs.clone().into()); + let var_map = create_var_map(&rule.lhs.copy().into()); let mut conditions = vec![]; for c in &rule.conditions { let ema_condition = EMACondition { - semi_compressed_lhs: SemiCompressedTermTree::from_term(&c.lhs.copy().into(), &var_map), - semi_compressed_rhs: SemiCompressedTermTree::from_term(&c.rhs.copy().into(), &var_map), + semi_compressed_lhs: TermStack::from_term(&c.lhs.copy().into(), &var_map), + semi_compressed_rhs: TermStack::from_term(&c.rhs.copy().into(), &var_map), equality: c.equality, }; conditions.push(ema_condition); From d0eba98a46a22e4590f690528c62a7cc0d948e35 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Thu, 28 Nov 2024 15:49:35 +0100 Subject: [PATCH 5/8] Added the TermStack to the modules --- libraries/sabre/src/utilities/mod.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/libraries/sabre/src/utilities/mod.rs b/libraries/sabre/src/utilities/mod.rs index 16bb246..f4a5a4a 100644 --- a/libraries/sabre/src/utilities/mod.rs +++ b/libraries/sabre/src/utilities/mod.rs @@ -1,11 +1,11 @@ mod configuration_stack; mod innermost_stack; mod position; -mod semi_compressed_tree; mod substitution; +mod term_stack; -pub(crate) use configuration_stack::*; -pub(crate) use innermost_stack::*; pub use position::*; -pub use semi_compressed_tree::*; pub use substitution::*; +pub(crate) use configuration_stack::*; +pub(crate) use innermost_stack::*; +pub(crate) use term_stack::*; From 119cb646fb1eaadfb3f3b491989de22126ff4652 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 2 Dec 2024 15:42:07 +0100 Subject: [PATCH 6/8] Replaced the semi compressed trees by a term stack. --- libraries/sabre/src/sabre_rewriter.rs | 6 +- .../src/utilities/configuration_stack.rs | 13 +- .../sabre/src/utilities/innermost_stack.rs | 222 ------------ .../src/utilities/semi_compressed_tree.rs | 321 ------------------ libraries/sabre/src/utilities/term_stack.rs | 8 - 5 files changed, 8 insertions(+), 562 deletions(-) delete mode 100644 libraries/sabre/src/utilities/semi_compressed_tree.rs diff --git a/libraries/sabre/src/sabre_rewriter.rs b/libraries/sabre/src/sabre_rewriter.rs index f1cb108..01ca8b2 100644 --- a/libraries/sabre/src/sabre_rewriter.rs +++ b/libraries/sabre/src/sabre_rewriter.rs @@ -237,7 +237,7 @@ impl SabreRewriter { // Computes the new subterm of the configuration let new_subterm = annotation .semi_compressed_rhs - .evaluate(&leaf_subterm.get_position(&announcement.position), tp) + .evaluate(tp, &leaf_subterm.get_position(&announcement.position)) .into(); trace!( @@ -264,8 +264,8 @@ impl SabreRewriter { for c in &annotation.conditions { let subterm = subterm.get_position(&announcement.position); - let rhs: DataExpression = c.semi_compressed_rhs.evaluate(&subterm, tp).into(); - let lhs: DataExpression = c.semi_compressed_lhs.evaluate(&subterm, tp).into(); + let rhs: DataExpression = c.semi_compressed_rhs.evaluate(tp, &subterm).into(); + let lhs: DataExpression = c.semi_compressed_lhs.evaluate(tp, &subterm).into(); // Equality => lhs == rhs. if !c.equality || lhs != rhs { diff --git a/libraries/sabre/src/utilities/configuration_stack.rs b/libraries/sabre/src/utilities/configuration_stack.rs index 4071213..b07fcb9 100644 --- a/libraries/sabre/src/utilities/configuration_stack.rs +++ b/libraries/sabre/src/utilities/configuration_stack.rs @@ -18,8 +18,8 @@ use mcrl2::data::DataExpressionRef; use super::create_var_map; use super::substitute_with; use super::PositionIndexed; -use super::SemiCompressedTermTree; use super::SubstitutionBuilder; +use super::TermStack; /// This is the announcement for Sabre, which stores additional information about the rewrite rules. #[derive(Hash, Eq, PartialEq, Ord, PartialOrd, Debug)] @@ -31,19 +31,16 @@ pub struct AnnouncementSabre { pub conditions: Vec, /// Right hand side is stored in the term pool as much as possible with a SemiCompressedTermTree - pub semi_compressed_rhs: SemiCompressedTermTree, + pub semi_compressed_rhs: TermStack, + /// Whether the rewrite rule duplicates subterms, e.g. times(s(x), y) = plus(y, times(x, y)) pub is_duplicating: bool, } impl AnnouncementSabre { pub fn new(rule: &Rule) -> AnnouncementSabre { - // Compute the extra information for the InnermostRewriter. - // Create a mapping of where the variables are and derive SemiCompressedTermTrees for the - // rhs of the rewrite rule and for lhs and rhs of each condition. - // Also see the documentation of SemiCompressedTermTree - let var_map = create_var_map(&rule.lhs.clone().into()); - let sctt_rhs = SemiCompressedTermTree::from_term(&rule.rhs.copy().into(), &var_map); + let var_map = create_var_map(&rule.lhs); + let sctt_rhs = TermStack::from_term(&rule.rhs.copy().into(), &var_map); let is_duplicating = sctt_rhs.contains_duplicate_var_references(); diff --git a/libraries/sabre/src/utilities/innermost_stack.rs b/libraries/sabre/src/utilities/innermost_stack.rs index e541bec..ceb0b3a 100644 --- a/libraries/sabre/src/utilities/innermost_stack.rs +++ b/libraries/sabre/src/utilities/innermost_stack.rs @@ -133,226 +133,4 @@ impl fmt::Display for InnermostStack { } write!(f, "]") } -<<<<<<< HEAD } - -impl fmt::Display for Config { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - match self { - Config::Rewrite(result) => write!(f, "Rewrite({})", result), - Config::Construct(symbol, arity, result) => { - write!(f, "Construct({}, {}, {})", symbol, arity, result) - } - Config::Return() => write!(f, "Return()"), - } - } -} - -/// A stack for the right-hand side. -pub struct RHSStack { - /// The innermost rewrite stack for the right hand side and the positions that must be added to the stack. - innermost_stack: Protected>, - variables: Vec<(ExplicitPosition, usize)>, - stack_size: usize, -} - -impl RHSStack { - /// Construct a new right-hand stack for a given equation/rewrite rule. - pub fn new(rule: &Rule) -> RHSStack { - let var_map = create_var_map(&rule.lhs.clone().into()); - - // Compute the extra information for the InnermostRewriter. - let mut innermost_stack: Protected> = Protected::new(vec![]); - let mut variables = vec![]; - let mut stack_size = 0; - - for (term, position) in PositionIterator::new(rule.rhs.copy().into()) { - if let Some(index) = position.indices.last() { - if *index == 1 { - continue; // Skip the function symbol. - } - } - - if is_data_variable(&term) { - variables.push(( - var_map - .get(&term.protect()) - .expect("All variables in the right hand side must occur in the left hand side") - .clone(), - stack_size, - )); - stack_size += 1; - } else if is_data_machine_number(&term) { - // Skip SortId(@NoValue) and OpId - } else if is_data_expression(&term) { - let t: DataExpressionRef = term.into(); - let arity = t.data_arguments().len(); - let mut write = innermost_stack.write(); - let symbol = write.protect(&t.data_function_symbol().into()); - write.push(Config::Construct(symbol.into(), arity, stack_size)); - stack_size += 1; - } else { - // Skip intermediate terms such as UntypeSortUnknown. - } - } - - RHSStack { - innermost_stack, - stack_size, - variables, - } - } - - /// Evaluate the rhs stack for the given term and returns the result. - pub fn evaluate(&self, tp: &mut TermPool, term: &DataExpression) -> DataExpression { - let mut stack = InnermostStack::default(); - stack.terms.write().push(DataExpressionRef::default()); - - InnermostStack::integrate(&mut stack.configs.write(), &mut stack.terms.write(), self, term, 0); - loop { - trace!("{}", stack); - - let mut write_configs = stack.configs.write(); - if let Some(config) = write_configs.pop() { - match config { - Config::Construct(symbol, arity, index) => { - // Take the last arity arguments. - let mut write_terms = stack.terms.write(); - let length = write_terms.len(); - - let arguments = &write_terms[length - arity..]; - - let term: DataExpression = if arguments.is_empty() { - symbol.protect().into() - } else { - DataApplication::new(tp, &symbol.copy(), arguments).into() - }; - - // Add the term on the stack. - write_terms.drain(length - arity..); - let t = write_terms.protect(&term); - write_terms[index] = t.into(); - } - Config::Rewrite(_) => { - unreachable!("This case should not happen"); - } - Config::Return() => { - unreachable!("This case should not happen"); - } - } - } else { - break; - } - } - - debug_assert!( - stack.terms.read().len() == 1, - "Expect exactly one term on the result stack" - ); - - let mut write_terms = stack.terms.write(); - - write_terms - .pop() - .expect("The result should be the last element on the stack") - .protect() - } -} - -impl Clone for RHSStack { - fn clone(&self) -> Self { - // TODO: It would make sense if Protected could implement Clone. - let mut innermost_stack: Protected> = Protected::new(vec![]); - - let mut write = innermost_stack.write(); - for t in self.innermost_stack.read().iter() { - match t { - Config::Rewrite(x) => write.push(Config::Rewrite(*x)), - Config::Construct(f, x, y) => { - let f = write.protect(&f.copy().into()); - write.push(Config::Construct(f.into(), *x, *y)); - } - Config::Return() => write.push(Config::Return()), - } - } - drop(write); - - Self { - variables: self.variables.clone(), - stack_size: self.stack_size, - innermost_stack, - } - } -} - -#[cfg(test)] -mod tests { - use super::*; - use ahash::AHashSet; - use mcrl2::aterm::TermPool; - use mcrl2::data::DataFunctionSymbol; - - use crate::test_utility::create_rewrite_rule; - use crate::utilities::to_untyped_data_expression; - - use test_log::test; - - #[test] - fn test_rhs_stack() { - let mut tp = TermPool::new(); - - let rhs_stack = - RHSStack::new(&create_rewrite_rule(&mut tp, "fact(s(N))", "times(s(N), fact(N))", &["N"]).unwrap()); - let mut expected = Protected::new(vec![]); - - let mut write = expected.write(); - let t = write.protect(&DataFunctionSymbol::new(&mut tp, "times").copy().into()); - write.push(Config::Construct(t.into(), 2, 0)); - - let t = write.protect(&DataFunctionSymbol::new(&mut tp, "s").copy().into()); - write.push(Config::Construct(t.into(), 1, 1)); - - let t = write.protect(&DataFunctionSymbol::new(&mut tp, "fact").copy().into()); - write.push(Config::Construct(t.into(), 1, 2)); - drop(write); - - // Check if the resulting construction succeeded. - assert_eq!( - rhs_stack.innermost_stack, expected, - "The resulting config stack is not as expected" - ); - - assert_eq!(rhs_stack.stack_size, 5, "The stack size does not match"); - - // Test the evaluation - let lhs = tp.from_string("fact(s(a))").unwrap(); - let lhs_expression = to_untyped_data_expression(&mut tp, &lhs, &AHashSet::new()); - - let rhs = tp.from_string("times(s(a), fact(a))").unwrap(); - let rhs_expression = to_untyped_data_expression(&mut tp, &rhs, &AHashSet::new()); - - assert_eq!( - rhs_stack.evaluate(&mut tp, &lhs_expression), - rhs_expression, - "The rhs stack does not evaluate to the expected term" - ); - } - - #[test] - fn test_rhs_stack_variable() { - let mut tp = TermPool::new(); - - let rhs = RHSStack::new(&create_rewrite_rule(&mut tp, "f(x)", "x", &["x"]).unwrap()); - - // Check if the resulting construction succeeded. - assert!( - rhs.innermost_stack.read().is_empty(), - "The resulting config stack is not as expected" - ); - - assert_eq!(rhs.stack_size, 1, "The stack size does not match"); - } -} -======= -} ->>>>>>> c86ebbb (Used the term stack in the innermost rewriter.) diff --git a/libraries/sabre/src/utilities/semi_compressed_tree.rs b/libraries/sabre/src/utilities/semi_compressed_tree.rs deleted file mode 100644 index 6717829..0000000 --- a/libraries/sabre/src/utilities/semi_compressed_tree.rs +++ /dev/null @@ -1,321 +0,0 @@ -// Author(s): Mark Bouwman - -use std::collections::HashMap; -use std::collections::HashSet; - -use crate::utilities::ExplicitPosition; -use mcrl2::aterm::ATerm; -use mcrl2::aterm::ATermRef; -use mcrl2::aterm::Symbol; -use mcrl2::aterm::TermBuilder; -use mcrl2::aterm::TermPool; -use mcrl2::aterm::Yield; -use mcrl2::data::is_data_variable; -use mcrl2::data::DataVariable; - -/// A SemiCompressedTermTree (SCTT) is a mix between a [ATerm] and a syntax tree and is used -/// to represent the rhs of rewrite rules and the lhs and rhs of conditions. -/// -/// It stores as much as possible in the term pool. Due to variables it cannot be fully compressed. -/// For variables it stores the position in the lhs of a rewrite rule where the concrete term can be -/// found that will replace the variable. -/// -/// # Examples -/// For the rewrite rule and(true, true) = true, the SCTT of the rhs will be of type Compressed, with -/// a pointer to the term true. -/// -/// For the rewrite rule minus(x, 0) = x, the SCTT of the rhs will be of type Variable, storing position -/// 1, the position of x in the lhs. -/// -/// For the rewrite rule minus(s(x), s(y)) = minus(x, y), the SCTT of the rhs will be of type -/// Explicit, which will stored the head symbol 'minus' and two child SCTTs of type Variable. -#[derive(Debug, Clone, PartialEq, Eq, Hash, Ord, PartialOrd)] -pub enum SemiCompressedTermTree { - Explicit(ExplicitNode), - Compressed(ATerm), - Variable(ExplicitPosition), -} - -/// Stores the head symbol and a SCTT for every argument explicitly. -#[derive(Debug, Clone, PartialEq, Eq, Hash, Ord, PartialOrd)] -pub struct ExplicitNode { - pub head: Symbol, - pub children: Vec, -} - -use SemiCompressedTermTree::*; - -use super::PositionIndexed; -use super::PositionIterator; - -pub type SCCTBuilder = TermBuilder<&'static SemiCompressedTermTree, &'static Symbol>; - -impl SemiCompressedTermTree { - /// Given an [ATerm] and a term pool this function instantiates the SCTT and computes a [ATerm]. - /// - /// # Example - /// For the SCTT belonging to the rewrite rule minus(s(x), s(y)) = minus(x, y) - /// and the concrete lhs minus(s(0), s(0)) the evaluation will go as follows. - /// evaluate will encounter an ExplicitNode and make two recursive calls to get the subterms. - /// Both these recursive calls will return the term '0'. - /// The term pool will be used to construct the term minus(0, 0). - pub fn evaluate_with<'a>(&'a self, builder: &mut SCCTBuilder, t: &ATermRef<'_>, tp: &mut TermPool) -> ATerm { - // TODO: Figure out if this can be done properly. This is safe because evaluate will always leave the - // underlying vectors empty. - let builder: &mut TermBuilder<&'a SemiCompressedTermTree, &'a Symbol> = unsafe { std::mem::transmute(builder) }; - - builder - .evaluate( - tp, - self, - |_tp, args, node| { - match node { - Explicit(node) => { - // Create an ATerm with as arguments all the evaluated semi compressed term trees. - for i in 0..node.children.len() { - args.push(&node.children[i]); - } - - Ok(Yield::Construct(&node.head)) - } - Compressed(ct) => Ok(Yield::Term(ct.clone())), - Variable(p) => Ok(Yield::Term(t.get_position(p).protect())), - } - }, - |tp, symbol, args| Ok(tp.create(symbol, args)), - ) - .unwrap() - } - - /// The same as [evaluate_with], but allocates a [SCCTBuilder] internally. - pub fn evaluate(&self, t: &ATermRef<'_>, tp: &mut TermPool) -> ATerm { - let mut builder = TermBuilder::<&SemiCompressedTermTree, &Symbol>::new(); - - self.evaluate_with(&mut builder, t, tp) - } - - /// Creates a SCTT from a term. The var_map parameter should specify where the variable can be - /// found in the lhs of the rewrite rule. - pub(crate) fn from_term( - t: &ATermRef<'_>, - var_map: &HashMap, - ) -> SemiCompressedTermTree { - if is_data_variable(t) { - Variable( - var_map - .get(&t.protect()) - .unwrap_or_else(|| panic!("{t} not contained in variable mapping var_map")) - .clone(), - ) - } else if t.arguments().is_empty() { - Compressed(t.protect()) - } else { - let children = t - .arguments() - .map(|c| SemiCompressedTermTree::from_term(&c, var_map)) - .collect(); - let node = ExplicitNode { - head: t.get_head_symbol().protect(), - children, - }; - - if node.children.iter().all(|c| c.is_compressed()) { - Compressed(t.protect()) - } else { - Explicit(node) - } - } - } - - /// Used to check if a subterm is duplicated, for example "times(s(x), y) = - /// plus(y, times(x,y))" is duplicating. - pub(crate) fn contains_duplicate_var_references(&self) -> bool { - let references = self.get_all_var_references(); - let mut seen = HashSet::new(); - - for r in references { - if seen.contains(&r) { - return true; - } - seen.insert(r); - } - - false - } - - /// Get all positions to variables in the left hand side. - fn get_all_var_references(&self) -> Vec { - let mut result = vec![]; - match self { - Explicit(en) => { - for n in &en.children { - result.extend_from_slice(&n.get_all_var_references()); - } - } - Compressed(_) => {} - Variable(ep) => { - result.push(ep.clone()); - } - } - - result - } - - /// Returns true iff this tree is compressed. - fn is_compressed(&self) -> bool { - matches!(self, Compressed(_)) - } -} - -/// Create a mapping of variables to their position in the given term -pub fn create_var_map(t: &ATerm) -> HashMap { - let mut result = HashMap::new(); - - for (term, position) in PositionIterator::new(t.copy()) { - if is_data_variable(&term) { - result.insert(term.protect().into(), position.clone()); - } - } - result -} - -#[cfg(test)] -mod tests { - use super::*; - use ahash::AHashSet; - use mcrl2::aterm::apply; - use mcrl2::aterm::TermPool; - - /// Converts a slice of static strings into a set of owned strings - /// - /// example: - /// make_var_map(["x"]) - fn var_map(vars: &[&str]) -> AHashSet { - AHashSet::from_iter(vars.iter().map(|x| String::from(*x))) - } - - /// Convert terms in variables to a [DataVariable]. - pub fn convert_variables(tp: &mut TermPool, t: &ATerm, variables: &AHashSet) -> ATerm { - apply(tp, t, &|tp, arg| { - if variables.contains(arg.get_head_symbol().name()) { - // Convert a constant variable, for example 'x', into an untyped variable. - Some(DataVariable::new(tp, &arg.get_head_symbol().name()).into()) - } else { - None - } - }) - } - - #[test] - fn test_constant() { - let mut tp = TermPool::new(); - let t = tp.from_string("a").unwrap(); - - let map = HashMap::new(); - let sctt = SemiCompressedTermTree::from_term(&t, &map); - assert_eq!(sctt, Compressed(t)); - } - - #[test] - fn test_compressible() { - let mut tp = TermPool::new(); - let t = tp.from_string("f(a,a)").unwrap(); - - let map = HashMap::new(); - let sctt = SemiCompressedTermTree::from_term(&t, &&map); - assert_eq!(sctt, Compressed(t)); - } - - #[test] - fn test_not_compressible() { - let mut tp = TermPool::new(); - let t = { - let tmp = tp.from_string("f(x,x)").unwrap(); - convert_variables(&mut tp, &tmp, &var_map(&["x"])) - }; - - let mut map = HashMap::new(); - map.insert(DataVariable::new(&mut tp, "x"), ExplicitPosition::new(&[2])); - - let sctt = SemiCompressedTermTree::from_term(&t, &map); - - let en = Explicit(ExplicitNode { - head: tp.create_symbol("f", 2), - children: vec![ - Variable(ExplicitPosition::new(&[2])), // Note that both point to the second occurence of x. - Variable(ExplicitPosition::new(&[2])), - ], - }); - - assert_eq!(sctt, en); - } - - #[test] - fn test_partly_compressible() { - let mut tp = TermPool::new(); - let t = { - let tmp = tp.from_string("f(f(a,a),x)").unwrap(); - convert_variables(&mut tp, &tmp, &var_map(&["x"])) - }; - let compressible = tp.from_string("f(a,a)").unwrap(); - - // Make a variable map with only x@2. - let mut map = HashMap::new(); - map.insert(DataVariable::new(&mut tp, "x"), ExplicitPosition::new(&[2])); - - let sctt = SemiCompressedTermTree::from_term(&t, &map); - let en = Explicit(ExplicitNode { - head: tp.create_symbol("f", 2), - children: vec![Compressed(compressible), Variable(ExplicitPosition::new(&[2]))], - }); - assert_eq!(sctt, en); - } - - #[test] - fn test_evaluation() { - let mut tp = TermPool::new(); - let t_rhs = { - let tmp = tp.from_string("f(f(a,a),x)").unwrap(); - convert_variables(&mut tp, &tmp, &var_map(&["x"])) - }; - let t_lhs = tp.from_string("g(b)").unwrap(); - - // Make a variable map with only x@1. - let mut map = HashMap::new(); - map.insert(DataVariable::new(&mut tp, "x"), ExplicitPosition::new(&[1])); - - let sctt = SemiCompressedTermTree::from_term(&t_rhs, &map); - - let t_expected = tp.from_string("f(f(a,a),b)").unwrap(); - assert_eq!(sctt.evaluate(&t_lhs, &mut tp), t_expected); - } - - #[test] - fn test_create_varmap() { - let mut tp = TermPool::new(); - let t = { - let tmp = tp.from_string("f(x,x)").unwrap(); - convert_variables(&mut tp, &tmp, &AHashSet::from([String::from("x")])) - }; - let x = DataVariable::new(&mut tp, "x"); - - let map = create_var_map(&t); - assert!(map.contains_key(&x)); - } - - #[test] - fn test_is_duplicating() { - let mut tp = TermPool::new(); - let t_rhs = { - let tmp = tp.from_string("f(x,x)").unwrap(); - convert_variables(&mut tp, &tmp, &AHashSet::from([String::from("x")])) - }; - - // Make a variable map with only x@1. - let mut map = HashMap::new(); - map.insert(DataVariable::new(&mut tp, "x"), ExplicitPosition::new(&[1])); - - let sctt = SemiCompressedTermTree::from_term(&t_rhs, &map); - assert!(sctt.contains_duplicate_var_references(), "This sctt is duplicating"); - } -} diff --git a/libraries/sabre/src/utilities/term_stack.rs b/libraries/sabre/src/utilities/term_stack.rs index b45969f..9f002cb 100644 --- a/libraries/sabre/src/utilities/term_stack.rs +++ b/libraries/sabre/src/utilities/term_stack.rs @@ -284,14 +284,6 @@ mod tests { use test_log::test; - /// Converts a slice of static strings into a set of owned strings - /// - /// example: - /// make_var_map(["x"]) - fn var_map(vars: &[&str]) -> AHashSet { - AHashSet::from_iter(vars.iter().map(|x| String::from(*x))) - } - /// Convert terms in variables to a [DataVariable]. pub fn convert_variables(tp: &mut TermPool, t: &ATerm, variables: &AHashSet) -> ATerm { apply(tp, t, &|tp, arg| { From 368db399ba6ddb6b7d8ceb2585275da81f3e3347 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 2 Dec 2024 15:59:51 +0100 Subject: [PATCH 7/8] Fixed an issue with contains_duplicate_var_references --- libraries/sabre/src/innermost_rewriter.rs | 4 +- libraries/sabre/src/matching/conditions.rs | 8 ++-- libraries/sabre/src/sabre_rewriter.rs | 4 +- libraries/sabre/src/utilities/term_stack.rs | 42 ++++++++++----------- 4 files changed, 29 insertions(+), 29 deletions(-) diff --git a/libraries/sabre/src/innermost_rewriter.rs b/libraries/sabre/src/innermost_rewriter.rs index 8bce979..86ad9cf 100644 --- a/libraries/sabre/src/innermost_rewriter.rs +++ b/libraries/sabre/src/innermost_rewriter.rs @@ -263,8 +263,8 @@ impl InnermostRewriter { t: &ATermRef<'_>, ) -> bool { for c in &announcement.conditions { - let rhs: DataExpression = c.semi_compressed_rhs.evaluate_with(tp, t, builder).into(); - let lhs: DataExpression = c.semi_compressed_lhs.evaluate_with(tp, t, builder).into(); + let rhs: DataExpression = c.stack_rhs.evaluate_with(tp, t, builder).into(); + let lhs: DataExpression = c.stack_lhs.evaluate_with(tp, t, builder).into(); let rhs_normal = InnermostRewriter::rewrite_aux(tp, stack, builder, stats, automaton, rhs); let lhs_normal = if &lhs == tp.true_term() { diff --git a/libraries/sabre/src/matching/conditions.rs b/libraries/sabre/src/matching/conditions.rs index 740c91a..59e25c6 100644 --- a/libraries/sabre/src/matching/conditions.rs +++ b/libraries/sabre/src/matching/conditions.rs @@ -7,8 +7,8 @@ use crate::Rule; #[derive(Hash, Clone, Eq, PartialEq, Ord, PartialOrd, Debug)] pub struct EMACondition { /// Conditions lhs and rhs are stored in the term pool as much as possible with a SemiCompressedTermTree - pub semi_compressed_lhs: TermStack, - pub semi_compressed_rhs: TermStack, + pub stack_lhs: TermStack, + pub stack_rhs: TermStack, /// whether the lhs and rhs should be equal or different pub equality: bool, @@ -21,8 +21,8 @@ pub fn extend_conditions(rule: &Rule) -> Vec { for c in &rule.conditions { let ema_condition = EMACondition { - semi_compressed_lhs: TermStack::from_term(&c.lhs.copy().into(), &var_map), - semi_compressed_rhs: TermStack::from_term(&c.rhs.copy().into(), &var_map), + stack_lhs: TermStack::from_term(&c.lhs.copy().into(), &var_map), + stack_rhs: TermStack::from_term(&c.rhs.copy().into(), &var_map), equality: c.equality, }; conditions.push(ema_condition); diff --git a/libraries/sabre/src/sabre_rewriter.rs b/libraries/sabre/src/sabre_rewriter.rs index 01ca8b2..fc66a11 100644 --- a/libraries/sabre/src/sabre_rewriter.rs +++ b/libraries/sabre/src/sabre_rewriter.rs @@ -264,8 +264,8 @@ impl SabreRewriter { for c in &annotation.conditions { let subterm = subterm.get_position(&announcement.position); - let rhs: DataExpression = c.semi_compressed_rhs.evaluate(tp, &subterm).into(); - let lhs: DataExpression = c.semi_compressed_lhs.evaluate(tp, &subterm).into(); + let rhs: DataExpression = c.stack_rhs.evaluate(tp, &subterm).into(); + let lhs: DataExpression = c.stack_lhs.evaluate(tp, &subterm).into(); // Equality => lhs == rhs. if !c.equality || lhs != rhs { diff --git a/libraries/sabre/src/utilities/term_stack.rs b/libraries/sabre/src/utilities/term_stack.rs index 9f002cb..fcd261c 100644 --- a/libraries/sabre/src/utilities/term_stack.rs +++ b/libraries/sabre/src/utilities/term_stack.rs @@ -2,13 +2,18 @@ use std::fmt; use ahash::{HashMap, HashMapExt}; use log::trace; -use mcrl2::{aterm::{ATermRef, Markable, Protected, TermPool, Todo}, data::{is_data_expression, is_data_machine_number, is_data_variable, DataApplication, DataExpression, DataExpressionRef, DataFunctionSymbolRef, DataVariable}}; +use mcrl2::{ + aterm::{ATermRef, Markable, Protected, TermPool, Todo}, + data::{ + is_data_expression, is_data_machine_number, is_data_variable, DataApplication, DataExpression, + DataExpressionRef, DataFunctionSymbolRef, DataVariable, + }, +}; use crate::{utilities::InnermostStack, Rule}; use super::{ExplicitPosition, PositionIterator}; - /// A stack used to represent a term with free variables that can be constructed /// efficiently. /// @@ -83,7 +88,7 @@ impl TermStack { Self::from_term(&rule.rhs.copy(), &create_var_map(&rule.lhs.copy().into())) } - /// + /// Construct a term stack from a data expression where variables are taken from a specific position of the left hand side. pub fn from_term(term: &DataExpressionRef, var_map: &HashMap) -> TermStack { // Compute the extra information for the InnermostRewriter. let mut innermost_stack: Protected> = Protected::new(vec![]); @@ -101,9 +106,7 @@ impl TermStack { variables.push(( var_map .get(&term.protect()) - .expect( - "All variables in the right hand side must occur in the left hand side", - ) + .expect("All variables in the right hand side must occur in the left hand side") .clone(), stack_size, )); @@ -139,7 +142,7 @@ impl TermStack { let stack = &mut builder.stack; { let mut write = stack.terms.write(); - write.clear(); + write.clear(); write.push(DataExpressionRef::default()); } @@ -173,7 +176,7 @@ impl TermStack { write_terms.drain(length - arity..); let t = write_terms.protect(&term); write_terms[index] = t.into(); - }, + } Config::Term(term, index) => { let mut write_terms = stack.terms.write(); let t = write_terms.protect(&term); @@ -203,16 +206,18 @@ impl TermStack { .expect("The result should be the last element on the stack") .protect() } - + /// Used to check if a subterm is duplicated, for example "times(s(x), y) = /// plus(y, times(x,y))" is duplicating. pub(crate) fn contains_duplicate_var_references(&self) -> bool { - let mut variables = self.variables.clone(); - variables.sort_by_key(|(pos, _)| pos.clone()); + let mut variables: Vec<&ExplicitPosition> = self.variables.iter().map(|(v, _)| v).collect(); + + // Check if there are duplicates. + variables.sort_unstable(); let len = variables.len(); variables.dedup(); - len == variables.len() + len != variables.len() } } @@ -246,10 +251,8 @@ impl Clone for TermStack { } } - pub struct TermStackBuilder { stack: InnermostStack, - } impl TermStackBuilder { @@ -269,6 +272,7 @@ pub fn create_var_map(t: &ATermRef) -> HashMap { result.insert(term.protect().into(), position.clone()); } } + result } @@ -300,9 +304,8 @@ mod tests { fn test_rhs_stack() { let mut tp = TermPool::new(); - let rhs_stack = TermStack::new( - &create_rewrite_rule(&mut tp, "fact(s(N))", "times(s(N), fact(N))", &["N"]).unwrap(), - ); + let rhs_stack = + TermStack::new(&create_rewrite_rule(&mut tp, "fact(s(N))", "times(s(N), fact(N))", &["N"]).unwrap()); let mut expected = Protected::new(vec![]); let mut write = expected.write(); @@ -402,9 +405,6 @@ mod tests { map.insert(DataVariable::new(&mut tp, "x"), ExplicitPosition::new(&[1])); let sctt = TermStack::from_term(&t_rhs.copy(), &map); - assert!( - sctt.contains_duplicate_var_references(), - "This sctt is duplicating" - ); + assert!(sctt.contains_duplicate_var_references(), "This sctt is duplicating"); } } From 5f94c7c5577f4b369a041e64087ca60c9a2a9589 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 3 Dec 2024 11:30:08 +0100 Subject: [PATCH 8/8] Fixed a off-by-one of a term position in a test --- libraries/sabre/src/utilities/innermost_stack.rs | 2 ++ libraries/sabre/src/utilities/term_stack.rs | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/libraries/sabre/src/utilities/innermost_stack.rs b/libraries/sabre/src/utilities/innermost_stack.rs index ceb0b3a..1c4e872 100644 --- a/libraries/sabre/src/utilities/innermost_stack.rs +++ b/libraries/sabre/src/utilities/innermost_stack.rs @@ -64,6 +64,7 @@ impl InnermostStack { } first = false; } + trace!( "\t applied stack size: {}, substitution: {}, stack: [{}]", rhs_stack.stack_size, @@ -77,6 +78,7 @@ impl InnermostStack { rhs_stack.stack_size != 1 || rhs_stack.variables.len() <= 1, "There can only be a single variable in the right hand side" ); + if rhs_stack.stack_size == 1 && rhs_stack.variables.len() == 1 { // This is a special case where we place the result on the correct position immediately. // The right hand side is only a variable diff --git a/libraries/sabre/src/utilities/term_stack.rs b/libraries/sabre/src/utilities/term_stack.rs index fcd261c..e0b1695 100644 --- a/libraries/sabre/src/utilities/term_stack.rs +++ b/libraries/sabre/src/utilities/term_stack.rs @@ -369,7 +369,7 @@ mod tests { // Make a variable map with only x@1. let mut map = HashMap::new(); - map.insert(DataVariable::new(&mut tp, "x"), ExplicitPosition::new(&[1])); + map.insert(DataVariable::new(&mut tp, "x"), ExplicitPosition::new(&[2])); let sctt = TermStack::from_term(&t_rhs.copy(), &map);