updates to euf-completion to

src/ast/simplifiers/euf_completion.cpp

@@ -38,15 +38,10 @@ Algorithm for extracting canonical form from an E-graph:
 Conditional saturation:
 - forall X . Body => Head
 - propagate when (all assertions in) Body is merged with True
-- Possible efficient approaches:
-    - use on_merge? 
-    - or bit set in nodes with Body?
-    - register Boolean reduction rules to EUF?
-    - register function "body_of" and monitor merges based on function?
+- insert expressions from Body into a watch list.
+  When elements of the watch list are merged by true/false
+  trigger rep-propagation with respect to body.
 
-Delayed solver invocation
-- So far default code for checking rules 
-  - EUF check should be on demand, see note on conditional saturation
 
 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.
@@ -59,10 +54,11 @@ Mam optimization?
 #include "ast/rewriter/var_subst.h"
 #include "ast/simplifiers/euf_completion.h"
 #include "ast/shared_occs.h"
+#include "params/tactic_params.hpp"
 
 namespace euf {
 
-    completion::completion(ast_manager& m, dependent_expr_state& fmls):
+    completion::completion(ast_manager& m, dependent_expr_state& fmls) :
         dependent_expr_simplifier(m, fmls),
         m_egraph(m),
         m_mam(mam::mk(*this, *this)),
@@ -78,6 +74,7 @@ namespace euf {
         std::function<void(euf::enode*, euf::enode*)> _on_merge =
             [&](euf::enode* root, euf::enode* other) {
             m_mam->on_merge(root, other);
+            watch_rule(root, other);
             };
 
         std::function<void(euf::enode*)> _on_make =
@@ -92,9 +89,76 @@ namespace euf {
     completion::~completion() {
     }
 
+    bool completion::should_stop() {
+        return
+            !m.inc() ||
+            m_egraph.inconsistent() ||
+            m_fmls.inconsistent() ||
+            resource_limits_exceeded();
+    }
+
+    void completion::updt_params(params_ref const& p) {
+        tactic_params tp(p);
+        m_max_instantiations = tp.completion_max_instantiations();
+    }
+
+    struct completion::push_watch_rule : public trail {
+        vector<ptr_vector<conditional_rule>>& m_rules;
+        unsigned idx;
+        push_watch_rule(vector<ptr_vector<conditional_rule>>& r, unsigned i) : m_rules(r), idx(i) {}
+        void undo() override {
+            m_rules[idx].pop_back();
+        }
+    };
+
+    void completion::push() {
+        if (m_side_condition_solver)
+            m_side_condition_solver->push();
+        m_egraph.push();
+        dependent_expr_simplifier::push();
+    }
+
+    void completion::pop(unsigned n) {
+        clear_propagation_queue();
+        dependent_expr_simplifier::pop(n);
+        m_egraph.pop(n);
+        if (m_side_condition_solver)
+            m_side_condition_solver->pop(n);
+    }
+
+    void completion::clear_propagation_queue() {
+        for (auto r : m_propagation_queue)
+            r->m_in_queue = false;
+        m_propagation_queue.reset();
+    }
+
+    void completion::watch_rule(enode* root, enode* other) {
+        auto oid = other->get_id();
+        if (oid >= m_rule_watch.size())
+            return;
+        if (m_rule_watch[oid].empty())
+            return;
+        auto is_true_or_false = m.is_true(root->get_expr()) || m.is_false(root->get_expr());
+        if (is_true_or_false) {
+            for (auto r : m_rule_watch[oid])
+                if (!r->m_in_queue)
+                    r->m_in_queue = true,
+                    m_propagation_queue.push_back(r);
+        }
+        else {
+            // root is not true or false, use root to watch rules
+            auto rid = root->get_id();
+            m_rule_watch.reserve(rid + 1);
+            for (auto r : m_rule_watch[oid]) {
+                m_rule_watch[rid].push_back(r);
+                get_trail().push(push_watch_rule(m_rule_watch, rid));
+            }
+        }
+    }
+
     void completion::reduce() {
         m_has_new_eq = true;
-        for (unsigned rounds = 0; m_has_new_eq && rounds <= 3 && !m_fmls.inconsistent(); ++rounds) {
+        for (unsigned rounds = 0; m_has_new_eq && rounds <= 3 && !should_stop(); ++rounds) {
             ++m_epoch;
             m_has_new_eq = false;
             add_egraph();
@@ -113,13 +177,14 @@ namespace euf {
             add_constraint(f, d);
         }
         m_should_propagate = true;
-        while (m_should_propagate && m.inc() && !m_egraph.inconsistent()) {
+        while (m_should_propagate && !should_stop()) {
             m_should_propagate = false;
             m_egraph.propagate();
             m_mam->propagate();
+            propagate_rules();
             IF_VERBOSE(11, verbose_stream() << "propagate " << m_stats.m_num_instances << "\n");
             if (!m_should_propagate)
-                check_rules();
+                propagate_all_rules();
         }
     }
 
@@ -184,6 +249,8 @@ namespace euf {
                 d = m.mk_join(d, explain_eq(n, n->get_root()));
                 return l_true;
             }
+            if (m.is_true(n->get_root()->get_expr()))
+                return l_false;
         }
         if (m_side_condition_solver) {
             expr_dependency* sd = nullptr;
@@ -220,48 +287,63 @@ namespace euf {
         if (body.empty())
             add_constraint(head, d);
         else {
-            m_rules.push_back(alloc(ground_rule, body, head, d));
+            // create a new rule. 
+            // add all (one is actually enough) parts of the body to watch list.
+            auto r = alloc(conditional_rule, body, head, d);
+            m_rules.push_back(r);
+            get_trail().push(new_obj_trail(r));
             get_trail().push(push_back_vector(m_rules));
-        }
-    }
-
-    void completion::check_rules() {
-        for (auto& r : m_rules) {
-            if (!r->m_active)
-                continue;
-            switch (check_rule(*r)) {
-            case l_true:
-                get_trail().push(value_trail(r->m_active));
-                r->m_active = false;
-                break; // remove rule, it is activated
-            case l_false:
-                get_trail().push(value_trail(r->m_active));
-                r->m_active = false;               
-                break; // remove rule, premise is false
-            case l_undef:                
-                break;
+            for (auto f : body) {
+                auto n = m_egraph.find(f)->get_root();
+                if (m.is_not(n->get_expr()))
+                    n = n->get_arg(0)->get_root();
+                m_rule_watch.reserve(n->get_id() + 1);
+                m_rule_watch[n->get_id()].push_back(r);
+                get_trail().push(push_watch_rule(m_rule_watch, n->get_id()));
             }
         }
     }
 
-     lbool completion::check_rule(ground_rule& r) {
+    void completion::propagate_all_rules() {
+        for (auto* r : m_rules)
+            if (!r->m_in_queue)
+                r->m_in_queue = true,
+                m_propagation_queue.push_back(r);
+        propagate_rules();
+    }
+
+    void completion::propagate_rules() {
+        for (unsigned i = 0; i < m_propagation_queue.size() && !should_stop(); ++i) {
+            auto r = m_propagation_queue[i];
+            r->m_in_queue = false;
+            propagate_rule(*r);
+        }
+        clear_propagation_queue();
+    }
+
+    void completion::propagate_rule(conditional_rule& r) {
+        if (!r.m_active)
+            return;
         for (auto* f : r.m_body) {
             switch (eval_cond(f, r.m_dep)) {
             case l_true:
                 break;
             case l_false:
-                return l_false;
+                get_trail().push(value_trail(r.m_active));
+                r.m_active = false;
+                return;
             default:
                 break;
             }
         }
         if (r.m_body.empty()) {
             add_constraint(r.m_head, r.m_dep);
-            return l_true;
+            get_trail().push(value_trail(r.m_active));
+            r.m_active = false;
         }
-        return l_undef;
     }
 
+    // callback when mam finds a binding
     void completion::on_binding(quantifier* q, app* pat, enode* const* binding, unsigned mg, unsigned ming, unsigned mx) {
         if (m_egraph.inconsistent())
             return;
@@ -272,6 +354,7 @@ namespace euf {
         expr_ref r = subst(q->get_expr(), _binding);
         IF_VERBOSE(12, verbose_stream() << "add " << r << "\n");
         add_constraint(r, get_dependency(q));
+        propagate_rules();
         m_should_propagate = true;
         ++m_stats.m_num_instances;
     }
@@ -636,5 +719,4 @@ namespace euf {
             }
         }
     }
-   
 }

src/ast/simplifiers/euf_completion.h

@@ -7,7 +7,10 @@ Module Name:
 
 Abstract:
 
-    Ground completion for equalities
+    Completion for (conditional) equalities.
+    This transforms expressions into a normal form by perorming equality saturation modulo 
+    ground equations and E-matching on quantified axioms.
+    It supports conditional equations in terms of implications.
 
 Author:
 
@@ -27,11 +30,17 @@ namespace euf {
 
     class side_condition_solver {
     public:
+        struct solution {
+            expr* var;
+            expr_ref term;
+            expr_ref guard;
+        };
         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;
+        virtual void solve_for(vector<solution>& sol) = 0;
     };
 
     class completion : public dependent_expr_simplifier, public on_binding_callback, public mam_solver {
@@ -42,12 +51,13 @@ namespace euf {
             void reset() { memset(this, 0, sizeof(*this)); }
         };
 
-        struct ground_rule {
+        struct conditional_rule {
             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) :
+            bool m_in_queue = false;
+            conditional_rule(expr_ref_vector& b, expr_ref& h, expr_dependency* d) :
                 m_body(b), m_head(h), m_dep(d) {}
         };
 
@@ -64,9 +74,11 @@ namespace euf {
         th_rewriter            m_rewriter;
         stats                  m_stats;
         scoped_ptr<side_condition_solver> m_side_condition_solver;
-        ptr_vector<ground_rule>    m_rules;
+        ptr_vector<conditional_rule>    m_rules;
         bool                   m_has_new_eq = false;
         bool                   m_should_propagate = false;
+        unsigned               m_max_instantiations = std::numeric_limits<unsigned>::max();
+        vector<ptr_vector<conditional_rule>> m_rule_watch;
             
         enode* mk_enode(expr* e);
         bool is_new_eq(expr* a, expr* b);
@@ -87,32 +99,38 @@ namespace euf {
 
         lbool eval_cond(expr* f, expr_dependency*& d);
         
-        lbool check_rule(ground_rule& rule);
-        void check_rules();
+
+        bool should_stop();
+
         void add_rule(expr* f, expr_dependency* d);
+        void watch_rule(enode* root, enode* other);
+        void propagate_rule(conditional_rule& r);
+        void propagate_rules();
+        void propagate_all_rules();
+        void clear_propagation_queue();
+        ptr_vector<conditional_rule> m_propagation_queue;
+        struct push_watch_rule;
 
         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-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 push() override;
+        void pop(unsigned n) override;
         void reduce() override;
         void collect_statistics(statistics& st) const override;
         void reset_statistics() override { m_stats.reset(); }
+        void updt_params(params_ref const& p) override;
 
         trail_stack& get_trail() override { return m_trail;}
         region& get_region() override { return m_trail.get_region(); }
         egraph& get_egraph() override { return m_egraph; }
         bool is_relevant(enode* n) const override { return true; }
-        bool resource_limits_exceeded() const override { return false; }
+        bool resource_limits_exceeded() const override { return m_stats.m_num_instances > m_max_instantiations; }
         ast_manager& get_manager() override { return m; }
 
         void on_binding(quantifier* q, app* pat, enode* const* binding, unsigned mg, unsigned ming, unsigned mx) override;
-
         void set_solver(side_condition_solver* s) { m_side_condition_solver = s; }
-
     };
 }

src/tactic/portfolio/euf_completion_tactic.cpp

@@ -18,6 +18,7 @@ Author:
 #include "tactic/tactic.h"
 #include "tactic/portfolio/euf_completion_tactic.h"
 #include "solver/solver.h"
+#include "smt/smt_solver.h"
 
 class euf_side_condition_solver : public euf::side_condition_solver {
     ast_manager& m;
@@ -25,55 +26,81 @@ class euf_side_condition_solver : public euf::side_condition_solver {
     scoped_ptr<solver> m_solver;
     expr_ref_vector m_deps;
     obj_map<expr, expr_dependency*> m_e2d;
+    expr_ref_vector m_fmls;
+    obj_hashtable<expr> m_seen;
+    trail_stack m_trail;
+
     void init_solver() {
         if (m_solver.get())
             return;
         m_params.set_uint("smt.max_conflicts", 100);
-        scoped_ptr<solver_factory> f = mk_smt_strategic_solver_factory();
+        scoped_ptr<solver_factory> f = mk_smt_solver_factory();
         m_solver = (*f)(m, m_params, false, false, true, symbol::null);
     }
+
 public:
-    euf_side_condition_solver(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_deps(m) {}
+
+    euf_side_condition_solver(ast_manager& m, params_ref const& p) : 
+        m(m), m_params(p), m_deps(m), m_fmls(m) {}
 
     void push() override {
         init_solver();
         m_solver->push();
+        m_trail.pop_scope(1);
     }
 
     void pop(unsigned n) override {
+        m_trail.push_scope();
         SASSERT(m_solver.get());
         m_solver->pop(n);
     }
 
     void add_constraint(expr* f, expr_dependency* d) override {
+        if (m_seen.contains(f))
+            return;
+        m_seen.insert(f);
+        m_trail.push(insert_obj_trail(m_seen, f));
         if (!is_ground(f))
             return;
+        if (m.is_implies(f))
+            return;
         init_solver();
-        expr* e_dep = nullptr;
         if (d) {
-            e_dep = m.mk_fresh_const("dep", m.mk_bool_sort());
+            expr* e_dep = m.mk_fresh_const("dep", m.mk_bool_sort());
             m_deps.push_back(e_dep);
             m_e2d.insert(e_dep, d);
-        }
+            m_trail.push(insert_obj_map(m_e2d, e_dep));
             m_solver->assert_expr(f, e_dep);
         }
+        else
+            m_solver->assert_expr(f);        
+    }
 
     bool is_true(expr* f, expr_dependency*& d) override {
         d = nullptr;
-        m_solver->push();
-        expr_ref_vector fmls(m);
-        fmls.push_back(m.mk_not(f));
+        solver::scoped_push _sp(*m_solver);
+        m_fmls.reset();
+        m_fmls.push_back(m.mk_not(f));
         expr_ref nf(m.mk_not(f), m);
-        lbool r = m_solver->check_sat(fmls);
+        lbool r = m_solver->check_sat(m_fmls);
         if (r == l_false) {
             expr_ref_vector core(m);
             m_solver->get_unsat_core(core);
             for (auto c : core)
                 d = m.mk_join(d, m_e2d[c]);
         }
-        m_solver->pop(1);
         return r == l_false;
     }
+
+    void solve_for(vector<solution>& sol) override {
+        vector<solver::solution> ss;
+        for (auto [v, t, g] : sol)
+            ss.push_back({ v, t, g });
+        sol.reset();
+        m_solver->solve_for(ss);
+        for (auto [v, t, g] : ss)
+            sol.push_back({ v, t, g });
+    }
 };
 
 dependent_expr_simplifier* mk_euf_completion_simplifier(ast_manager& m, dependent_expr_state& s, params_ref const& p) {