adding ack/model

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

scripts/mk_project.py

@@ -39,9 +39,7 @@ def init_project_def():
     add_lib('solver', ['model', 'tactic', 'proofs'])
     add_lib('cmd_context', ['solver', 'rewriter'])
     add_lib('sat_smt', ['sat', 'euf', 'tactic'], 'sat/smt')
-    add_lib('sat_ba',  ['sat', 'sat_smt'], 'sat/ba')    
-    add_lib('sat_euf', ['sat', 'euf', 'sat_ba'], 'sat/euf')    
-    add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_euf'], 'sat/tactic')        
+    add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')        
     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')
@@ -83,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', 'sat_euf'], exe_name='test-z3', install=False)
+    add_exe('test', ['api', 'fuzzing', 'simplex', 'sat_smt'], 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,8 +60,6 @@ add_subdirectory(math/subpaving/tactic)
 add_subdirectory(tactic/aig)
 add_subdirectory(solver)
 add_subdirectory(sat/smt)
-add_subdirectory(sat/ba)
-add_subdirectory(sat/euf)
 add_subdirectory(sat/tactic)
 add_subdirectory(tactic/arith)
 add_subdirectory(nlsat/tactic)

src/ast/euf/euf_egraph.cpp

@@ -255,7 +255,10 @@ namespace euf {
        explanations up to the least common ancestors.
      */
     void egraph::push_congruence(enode* n1, enode* n2, bool comm) {
+        SASSERT(is_app(n1->get_owner()));
         SASSERT(n1->get_decl() == n2->get_decl());
+        if (m_used_cc) 
+            m_used_cc(to_app(n1->get_owner()), to_app(n2->get_owner()));
         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()) {
@@ -268,30 +271,28 @@ namespace euf {
             push_lca(n1->get_arg(i), n2->get_arg(i));
     }
 
-    void egraph::push_lca(enode* a, enode* b) {
+    enode* egraph::find_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);
+        a->mark2_targets<true>();
+        while (!b->is_marked2()) 
+            b = b->m_target;
+        a->mark2_targets<false>();
+        return b;
+    }
+
+    void egraph::push_to_lca(enode* n, enode* lca) {
+        while (n != lca) {
+            m_todo.push_back(n);
             n = n->m_target;
         }
     }
 
+    void egraph::push_lca(enode* a, enode* b) {
+        enode* lca = find_lca(a, b);
+        push_to_lca(a, lca);
+        push_to_lca(b, lca);
+    }
+
     void egraph::push_todo(enode* n) {
         while (n) {
             m_todo.push_back(n);
@@ -313,7 +314,11 @@ namespace euf {
     void egraph::explain_eq(ptr_vector<T>& justifications, enode* a, enode* b, bool comm) {
         SASSERT(m_todo.empty());
         SASSERT(a->get_root() == b->get_root());
-        push_lca(a, b);
+        enode* lca = find_lca(a, b);
+        push_to_lca(a, lca);
+        push_to_lca(b, lca);
+        if (m_used_eq)
+            m_used_eq(a->get_owner(), b->get_owner(), lca->get_owner());
         explain_todo(justifications);
     }
 

src/ast/euf/euf_egraph.h

@@ -70,7 +70,8 @@ namespace euf {
         enode_vector           m_new_lits;
         enode_vector           m_todo;
         stats                  m_stats;
-
+        std::function<void(expr*,expr*,expr*)> m_used_eq;
+        std::function<void(app*,app*)>        m_used_cc;            
 
         void push_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
             m_eqs.push_back(add_eq_record(r1, n1, r2_num_parents));
@@ -87,6 +88,8 @@ namespace euf {
         void reinsert_equality(enode* p);
         void update_children(enode* n);
         void push_lca(enode* a, enode* b);
+        enode* find_lca(enode* a, enode* b);
+        void push_to_lca(enode* a, enode* lca);
         void push_congruence(enode* n1, enode* n2, bool commutative);
         void push_todo(enode* n);
         template <typename T>
@@ -126,6 +129,10 @@ namespace euf {
         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; }
+
+        void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
+        void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }
+
         template <typename T>
         void explain(ptr_vector<T>& justifications);
         template <typename T>

src/ast/euf/euf_enode.h

@@ -104,11 +104,29 @@ namespace euf {
         void mark2() { m_mark2 = true; }
         void unmark2() { m_mark2 = false; }
         bool is_marked2() { return m_mark2; }
+
+        template<bool m> void mark1_targets() {
+            enode* n = this;
+            while (n) {
+                if (m) n->mark1(); else n->unmark1();
+                n = n->m_target;
+            }
+        }
+        template<bool m> void mark2_targets() {
+            enode* n = this;
+            while (n) {
+                if (m) n->mark2(); else n->unmark2();
+                n = n->m_target;
+            }
+        }
+
         void add_parent(enode* p) { m_parents.push_back(p); }
         unsigned class_size() const { return m_class_size; }
+        bool is_root() const { return m_root == this; }
         enode* get_root() const { return m_root; }
         expr*  get_owner() const { return m_owner; }
         unsigned get_owner_id() const { return m_owner->get_id(); }
+        unsigned get_root_id() const { return m_root->m_owner->get_id(); }
         void inc_class_size(unsigned n) { m_class_size += n; }
         void dec_class_size(unsigned n) { m_class_size -= n; }
 

src/sat/sat_extension.h

@@ -86,7 +86,7 @@ namespace sat {
         virtual unsigned max_var(unsigned w) const = 0;
 
         virtual bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
-                                std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {
+                                std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {                                
             return false;
         }
     };

src/sat/sat_solver.h

@@ -454,6 +454,8 @@ namespace sat {
 
         void display_lookahead_scores(std::ostream& out);
 
+        stats const& stats() const { return m_stats; }
+
     protected:
 
         unsigned m_conflicts_since_init;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -615,7 +615,7 @@ class inc_sat_solver : public solver {
 
 private:
 
-    lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
+    lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) {
         m_solver.pop_to_base_level();
         if (m_solver.inconsistent()) 
             return l_false;
@@ -662,7 +662,7 @@ class inc_sat_solver : public solver {
 
         // ensure that if goal is already internalized, then import mc from m_solver.
 
-        m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, is_incremental(), is_lemma);
+        m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, is_incremental());
         m_goal2sat.get_interpreted_atoms(atoms);
         if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
         m_sat_mc->flush_smc(m_solver, m_map);
@@ -690,7 +690,7 @@ class inc_sat_solver : public solver {
         for (unsigned i = 0; i < get_num_assumptions(); ++i) {
             g->assert_expr(get_assumption(i), m.mk_leaf(get_assumption(i)));
         }
-        lbool res = internalize_goal(g, dep2asm, false);
+        lbool res = internalize_goal(g, dep2asm);
         if (res == l_true) {
             extract_assumptions(sz, asms, dep2asm);
         }
@@ -831,7 +831,7 @@ class inc_sat_solver : public solver {
             expr* fml = m_fmls.get(i);
             g->assert_expr(fml);
         }
-        lbool res = internalize_goal(g, dep2asm, false);
+        lbool res = internalize_goal(g, dep2asm);
         if (res != l_undef) {
             m_fmls_head = m_fmls.size();
         }

src/sat/smt/CMakeLists.txt

@@ -1,7 +1,12 @@
 z3_add_component(sat_smt
   SOURCES
     atom2bool_var.cpp
-    sat_th.cpp
+    ba_solver.cpp
+    xor_solver.cpp
+    ba_internalize.cpp
+    euf_ackerman.cpp
+    euf_solver.cpp
+    euf_model.cpp
   COMPONENT_DEPENDENCIES
     sat
     ast