Replace the semi compressed trees by a term stack construction

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");
     }
 }
 

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<AnnouncementInnermost>,
         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<AnnouncementInnermost>,
         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<AnnouncementInnermost>,
         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.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() {
@@ -284,7 +288,7 @@ pub struct InnermostRewriter {
     tp: Rc<RefCell<TermPool>>,
     apma: SetAutomaton<AnnouncementInnermost>,
     stack: InnermostStack,
-    builder: SCCTBuilder,
+    builder: TermStackBuilder,
 }
 
 pub(crate) struct AnnouncementInnermost {
@@ -295,15 +299,15 @@ pub(crate) struct AnnouncementInnermost {
     conditions: Vec<EMACondition>,
 
     /// The innermost stack for the right hand side of the rewrite rule.
-    rhs_stack: RHSStack,
+    rhs_stack: TermStack,
 }
 
 impl AnnouncementInnermost {
     fn new(rule: &Rule) -> AnnouncementInnermost {
         AnnouncementInnermost {
             conditions: extend_conditions(rule),
             equivalence_classes: derive_equivalence_classes(rule),
-            rhs_stack: RHSStack::new(rule),
+            rhs_stack: TermStack::new(rule),
         }
     }
 }

libraries/sabre/src/matching/conditions.rs

@@ -1,28 +1,28 @@
 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
 /// subsituted efficiently.
 #[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 stack_lhs: TermStack,
+    pub stack_rhs: TermStack,
 
     /// whether the lhs and rhs should be equal or different
     pub equality: bool,
 }
 
 /// Computes the extended condition from a given rewrite rule.
 pub fn extend_conditions(rule: &Rule) -> Vec<EMACondition> {
-    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),
+            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);

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.stack_rhs.evaluate(tp, &subterm).into();
+            let lhs: DataExpression = c.stack_lhs.evaluate(tp, &subterm).into();
 
             // Equality => lhs == rhs.
             if !c.equality || lhs != rhs {

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<EMACondition>,
 
     /// 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();