make rule processing fully incremental

NikolajBjorner · NikolajBjorner · commit 1cd162203d3b · 2025-06-06T20:45:54.000+02:00
diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
@@ -51,10 +51,6 @@ Delayed solver invocation
 Mam optimization?
    match(p, t, S) = suppose all variables in p are bound in S, check equality using canonization of p[S], otherwise prune instances from S.
 
-
-
-
-
 --*/
 
 #include "ast/ast_pp.h"
@@ -94,13 +90,6 @@ namespace euf {
     }
 
     completion::~completion() {
-        reset_rules();
-    }
-
-    void completion::reset_rules() {
-        for (auto r : m_rules)
-            dealloc(r);
-        m_rules.reset();
     }
 
     void completion::reduce() {
@@ -113,7 +102,6 @@ namespace euf {
             read_egraph();
             IF_VERBOSE(11, verbose_stream() << "(euf.completion :rounds " << rounds << ")\n");
         }
-        reset_rules();
     }
 
     void completion::add_egraph() {
@@ -229,45 +217,44 @@ namespace euf {
             }
         }
         body.shrink(j);
-        if (body.empty()) {
-            add_constraint(head, d);
-            return;
+        if (body.empty()) 
+            add_constraint(head, d);        
+        else {
+            m_rules.push_back(alloc(ground_rule, body, head, d));
+            get_trail().push(push_back_vector(m_rules));
         }
-        m_rules.push_back(alloc(ground_rule, body, head, d));
     }
 
     void completion::check_rules() {
-        unsigned j = 0;
         for (auto& r : m_rules) {
+            if (!r->m_active)
+                continue;
             switch (check_rule(*r)) {
             case l_true:
-                dealloc(r);
+                get_trail().push(value_trail(r->m_active));
+                r->m_active = false;
                 break; // remove rule, it is activated
             case l_false:
-                dealloc(r);
+                get_trail().push(value_trail(r->m_active));
+                r->m_active = false;               
                 break; // remove rule, premise is false
             case l_undef:                
-                m_rules[j++] = r;
                 break;
             }
         }
-        m_rules.shrink(j);
     }
 
      lbool completion::check_rule(ground_rule& r) {
-        unsigned j = 0;
         for (auto* f : r.m_body) {
             switch (eval_cond(f, r.m_dep)) {
             case l_true:
                 break;
             case l_false:
                 return l_false;
             default:
-                r.m_body[j++] = f;
                 break;
             }            
         }
-        r.m_body.shrink(j);
         if (r.m_body.empty()) {
             add_constraint(r.m_head, r.m_dep);
             return l_true;
@@ -650,6 +637,4 @@ namespace euf {
         }
     }    
    
-}
-
-
+}
diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h
@@ -30,6 +30,8 @@ namespace euf {
         virtual ~side_condition_solver() = default;
         virtual void add_constraint(expr* f, expr_dependency* d) = 0;
         virtual bool is_true(expr* f, expr_dependency*& d) = 0;
+        virtual void push() = 0;
+        virtual void pop(unsigned n) = 0;
     };
 
     class completion : public dependent_expr_simplifier, public on_binding_callback, public mam_solver {
@@ -44,6 +46,7 @@ namespace euf {
             expr_ref_vector m_body;
             expr_ref m_head;
             expr_dependency* m_dep;
+            bool m_active = true;
             ground_rule(expr_ref_vector& b, expr_ref& h, expr_dependency* d) :
                 m_body(b), m_head(h), m_dep(d) {}
         };
@@ -87,15 +90,15 @@ namespace euf {
         lbool check_rule(ground_rule& rule);
         void check_rules();
         void add_rule(expr* f, expr_dependency* d);
-        void reset_rules();
 
         bool is_gt(expr* a, expr* b) const;
     public:
         completion(ast_manager& m, dependent_expr_state& fmls);
         ~completion() override;
-        char const* name() const override { return "euf-reduce"; }
-        void push() override { m_egraph.push(); dependent_expr_simplifier::push(); }
-        void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_egraph.pop(n); }
+        char const* name() const override { return "euf-completion"; }
+        void push() override { if (m_side_condition_solver) m_side_condition_solver->push();  m_egraph.push(); dependent_expr_simplifier::push(); }
+        void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_egraph.pop(n); if (m_side_condition_solver) m_side_condition_solver->pop(1);
+        }
         void reduce() override;
         void collect_statistics(statistics& st) const override;
         void reset_statistics() override { m_stats.reset(); }
