add sat-euf

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

scripts/mk_project.py

@@ -39,6 +39,7 @@ def init_project_def():
     add_lib('solver', ['model', 'tactic', 'proofs'])
     add_lib('cmd_context', ['solver', 'rewriter'])    
     add_lib('sat_tactic', ['tactic', 'sat', 'solver'], 'sat/tactic')
+    add_lib('sat_euf', ['sat_tactic', 'sat', 'euf'], 'sat/euf')    
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
     add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
     add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
@@ -80,7 +81,7 @@ def init_project_def():
             includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
     add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'arith_tactics'], 'cmd_context/extra_cmds')
     add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
-    add_exe('test', ['api', 'fuzzing', 'simplex', 'euf'], exe_name='test-z3', install=False)
+    add_exe('test', ['api', 'fuzzing', 'simplex', 'sat_euf'], exe_name='test-z3', install=False)
     _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
                               reexports=['api'],
                               dll_name='libz3',

src/CMakeLists.txt

@@ -60,6 +60,7 @@ add_subdirectory(math/subpaving/tactic)
 add_subdirectory(tactic/aig)
 add_subdirectory(solver)
 add_subdirectory(sat/tactic)
+add_subdirectory(sat/euf)
 add_subdirectory(tactic/arith)
 add_subdirectory(nlsat/tactic)
 add_subdirectory(ackermannization)

src/ast/euf/euf_egraph.cpp

@@ -35,8 +35,7 @@ namespace euf {
         unmerge_justification(n1);
     }
 
-    enode* egraph::mk_enode(expr* f, enode * const* args) {
-        unsigned num_args = is_app(f) ? to_app(f)->get_num_args() : 0;
+    enode* egraph::mk_enode(expr* f, unsigned num_args, enode * const* args) {
         enode* n = enode::mk(m_region, f, num_args, args);
         m_nodes.push_back(n);
         m_exprs.push_back(f);
@@ -98,15 +97,15 @@ namespace euf {
         n->set_update_children();            
     }
 
-    enode* egraph::mk(expr* f, enode *const* args) {
+    enode* egraph::mk(expr* f, unsigned num_args, enode *const* args) {
         SASSERT(!find(f));
         force_push();
-        enode *n = mk_enode(f, args);
+        enode *n = mk_enode(f, num_args, args);
         SASSERT(n->class_size() == 1);
         m_expr2enode.setx(f->get_id(), n, nullptr);
-        if (n->num_args() == 0 && m.is_unique_value(f))
+        if (num_args == 0 && m.is_unique_value(f))
             n->mark_interpreted();
-        if (n->num_args() == 0) 
+        if (num_args == 0) 
             return n;
         if (is_equality(n)) {
             update_children(n);
@@ -171,6 +170,8 @@ namespace euf {
             std::swap(r1, r2);
             std::swap(n1, n2);
         }
+        if ((m.is_true(r2->get_owner()) || m.is_false(r2->get_owner())) && j.is_congruence())
+            m_new_lits.push_back(n1);
         for (enode* p : enode_parents(n1)) 
             m_table.erase(p);            
         for (enode* p : enode_parents(n2)) 
@@ -187,6 +188,7 @@ namespace euf {
 
     void egraph::propagate() {
         m_new_eqs.reset();
+        m_new_lits.reset();
         SASSERT(m_num_scopes == 0 || m_worklist.empty());
         unsigned head = 0, tail = m_worklist.size();
         while (head < tail && m.limit().inc() && !inconsistent()) {
@@ -239,6 +241,88 @@ namespace euf {
         SASSERT(n1->get_root()->m_target == nullptr);
     }
 
+    /**
+       \brief generate an explanation for a congruence.
+       Each pair of children under a congruence have the same roots
+       and therefore have a least common ancestor. We only need
+       explanations up to the least common ancestors.
+     */
+    void egraph::push_congruence(enode* n1, enode* n2, bool comm) {
+        SASSERT(n1->get_decl() == n2->get_decl());
+        if (comm && 
+            n1->get_arg(0)->get_root() == n2->get_arg(1)->get_root() &&
+            n1->get_arg(1)->get_root() == n2->get_arg(0)->get_root()) {
+            push_lca(n1->get_arg(0), n2->get_arg(1));
+            push_lca(n1->get_arg(1), n2->get_arg(0));
+            return;
+        }
+
+        for (unsigned i = 0; i < n1->num_args(); ++i) 
+            push_lca(n1->get_arg(i), n2->get_arg(i));
+    }
+
+    void egraph::push_lca(enode* a, enode* b) {
+        SASSERT(a->get_root() == b->get_root());
+        enode* n = a;
+        while (n) {
+            n->mark2();
+            n = n->m_target;
+        }
+        n = b;
+        while (n) {
+            if (n->is_marked2()) 
+                n->unmark2();   
+            else if (!n->is_marked1()) 
+                m_todo.push_back(n);
+            n = n->m_target;
+        }
+        n = a;
+        while (n->is_marked2()) {            
+            n->unmark2();
+            if (!n->is_marked1())
+                m_todo.push_back(n);
+            n = n->m_target;
+        }
+    }
+
+    void egraph::push_todo(enode* n) {
+        while (n) {
+            m_todo.push_back(n);
+            n = n->m_target;
+        }
+    }
+
+    template <typename T>
+    void egraph::explain(ptr_vector<T>& justifications) {
+        SASSERT(m_inconsistent);
+        SASSERT(m_todo.empty());
+        push_todo(m_n1);
+        push_todo(m_n2);
+        explain_eq(justifications, m_n1, m_n2, m_justification);
+        explain_todo(justifications);
+    }
+
+    template <typename T>
+    void egraph::explain_eq(ptr_vector<T>& justifications, enode* a, enode* b, bool comm) {
+        SASSERT(m_todo.empty());
+        push_congruence(a, b, comm);
+        explain_todo(justifications);
+    }
+
+    template <typename T>
+    void egraph::explain_todo(ptr_vector<T>& justifications) {
+        for (unsigned i = 0; i < m_todo.size(); ++i) {
+            enode* n = m_todo[i];
+            if (n->m_target && !n->is_marked1()) {
+                n->mark1();
+                explain_eq(justifications, n, n->m_target, n->m_justification);
+            }
+        }
+        for (enode* n : m_todo) 
+            n->unmark1();
+        m_todo.reset();        
+    }
+
     void egraph::invariant() {
         for (enode* n : m_nodes)
             n->invariant();
@@ -267,3 +351,12 @@ namespace euf {
         return out;
     }
 }
+
+template void euf::egraph::explain(ptr_vector<int>& justifications);
+template void euf::egraph::explain_todo(ptr_vector<int>& justifications);
+template void euf::egraph::explain_eq(ptr_vector<int>& justifications, enode* a, enode* b, bool comm);
+
+template void euf::egraph::explain(ptr_vector<unsigned>& justifications);
+template void euf::egraph::explain_todo(ptr_vector<unsigned>& justifications);
+template void euf::egraph::explain_eq(ptr_vector<unsigned>& justifications, enode* a, enode* b, bool comm);
+

src/ast/euf/euf_egraph.h

@@ -58,29 +58,45 @@ namespace euf {
         enode                  *m_n2 { nullptr };
         justification          m_justification;
         enode_vector           m_new_eqs;
+        enode_vector           m_new_lits;
         enode_vector           m_todo;
 
         void push_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
             m_eqs.push_back(add_eq_record(r1, n1, r2_num_parents));
         }
         void undo_eq(enode* r1, enode* n1, unsigned r2_num_parents);
-        enode* mk_enode(expr* f, enode * const* args);
+        enode* mk_enode(expr* f, unsigned num_args, enode * const* args);
         void reinsert(enode* n);
         void force_push();
         void set_conflict(enode* n1, enode* n2, justification j);
         void merge(enode* n1, enode* n2, justification j);
         void merge_justification(enode* n1, enode* n2, justification j);
         void unmerge_justification(enode* n1);
         void dedup_equalities();
-        bool is_equality(enode* n) const;
         void reinsert_equality(enode* p);
         void update_children(enode* n);
+        void push_lca(enode* a, enode* b);
+        void push_congruence(enode* n1, enode* n2, bool commutative);
+        void push_todo(enode* n);
+        template <typename T>
+        void explain_eq(ptr_vector<T>& justifications, enode* a, enode* b, justification const& j) {
+            if (j.is_external())
+                justifications.push_back(j.ext<T>());
+            else if (j.is_congruence()) 
+                push_congruence(a, b, j.is_commutative());
+        }
+        template <typename T>
+        void explain_todo(ptr_vector<T>& justifications);
+
     public:
         egraph(ast_manager& m): m(m), m_table(m), m_exprs(m) {}
         enode* find(expr* f) { return m_expr2enode.get(f->get_id(), nullptr); }
-        enode* mk(expr* f, enode *const* args);
+        enode* mk(expr* f, unsigned n, enode *const* args);
         void push() { ++m_num_scopes; }
         void pop(unsigned num_scopes);
+
+        bool is_equality(enode* n) const;
+
         /**
            \brief merge nodes, all effects are deferred to the propagation step.
          */
@@ -98,45 +114,11 @@ namespace euf {
         void propagate();
         bool inconsistent() const { return m_inconsistent; }
         enode_vector const& new_eqs() const { return m_new_eqs; }
+        enode_vector const& new_lits() const { return m_new_lits; }
         template <typename T>
-        void explain(ptr_vector<T>& justifications) {
-            SASSERT(m_inconsistent);
-            SASSERT(m_todo.empty());
-            auto push_congruence = [&](enode* p, enode* q) {
-                SASSERT(p->get_decl() == q->get_decl());
-                for (enode* arg : enode_args(p))
-                    m_todo.push_back(arg);
-                for (enode* arg : enode_args(q))
-                    m_todo.push_back(arg);
-            };
-            auto explain_node = [&](enode* n) {
-                if (!n->m_target)
-                    return;
-                if (n->is_marked1())
-                    return;
-                n->mark1();
-                if (n->m_justification.is_external())
-                    justifications.push_back(n->m_justification.ext<T>());
-                else if (n->m_justification.is_congruence()) 
-                    push_congruence(n, n->m_target);
-                n = n->m_target;
-                if (!n->is_marked1())
-                    m_todo.push_back(n);
-            };
-            m_todo.push_back(m_n1);
-            m_todo.push_back(m_n2);
-            if (m_justification.is_external())
-                justifications.push_back(m_justification.ext<T>());
-            else if (m_justification.is_congruence())
-                push_congruence(m_n1, m_n2);
-            for (unsigned i = 0; i < m_todo.size(); ++i) 
-                explain_node(m_todo[i]);
-            for (enode* n : m_todo) 
-                n->unmark1();
-            m_todo.reset();
-        }
-
-
+        void explain(ptr_vector<T>& justifications);
+        template <typename T>
+        void explain_eq(ptr_vector<T>& justifications, enode* a, enode* b, bool comm);
         void invariant();
         std::ostream& display(std::ostream& out) const;        
     };

src/ast/euf/euf_enode.h

@@ -43,6 +43,7 @@ namespace euf {
         enode*        m_root;
         enode*        m_target { nullptr };
         justification m_justification;
+        unsigned      m_num_args;
         enode*        m_args[0];        
 
         friend class enode_args;
@@ -56,12 +57,14 @@ namespace euf {
         }
 
         static enode* mk(region& r, expr* f, unsigned num_args, enode* const* args) {
+            SASSERT(num_args <= (is_app(f) ? to_app(f)->get_num_args() : 0));
             void* mem = r.allocate(get_enode_size(num_args));
             enode* n = new (mem) enode();
             n->m_owner = f;
             n->m_next = n;
             n->m_root = n;
             n->m_commutative = num_args == 2 && is_app(f) && to_app(f)->get_decl()->is_commutative();
+            n->m_num_args = num_args;
             for (unsigned i = 0; i < num_args; ++i) {
                 SASSERT(to_app(f)->get_arg(i) == args[i]->get_owner());
                 n->m_args[i] = args[i];
@@ -83,9 +86,10 @@ namespace euf {
         }
 
         enode* const* args() const { return m_args; }
-        unsigned num_args() const { return is_app(m_owner) ? to_app(m_owner)->get_num_args() : 0; }                
+        unsigned num_args() const { return m_num_args; }
         unsigned num_parents() const { return m_parents.size(); }
         bool interpreted() const { return m_interpreted; }
+        bool commutative() const { return m_commutative; }
         void mark_interpreted() { SASSERT(num_args() == 0); m_interpreted = true; }
 
         enode* get_arg(unsigned i) const { SASSERT(i < num_args()); return m_args[i]; }        
@@ -97,6 +101,9 @@ namespace euf {
         void mark1() { m_mark1 = true; }
         void unmark1() { m_mark1 = false; }
         bool is_marked1() { return m_mark1; }
+        void mark2() { m_mark2 = true; }
+        void unmark2() { m_mark2 = false; }
+        bool is_marked2() { return m_mark2; }
         void add_parent(enode* p) { m_parents.push_back(p); }
         unsigned class_size() const { return m_class_size; }
         enode* get_root() const { return m_root; }

src/sat/euf/CMakeLists.txt

@@ -0,0 +1,8 @@
+z3_add_component(sat_euf
+  SOURCES
+    euf_solver.cpp
+  COMPONENT_DEPENDENCIES
+    sat
+    sat_tactic
+    euf
+)