na

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/ast/euf/euf_egraph.h

@@ -39,6 +39,13 @@ namespace euf {
             r1(r1), n1(n1), r2_num_parents(r2_num_parents) {}
     };
 
+    /***
+      \brief store derived theory equalities.
+      Theory 'id' is notified with the equality of theory variables v1, v2
+      that are merged into the common root of child and root (their roots may
+      have been updated since the equality was derived, but the explanation for
+      v1 == v2 is provided by explaining the equality child == root.
+    */
     struct th_eq {
         theory_id  m_id;
         theory_var m_v1;

src/sat/sat_solver.cpp

@@ -1602,7 +1602,6 @@ namespace sat {
     }
 
     lbool solver::bounded_search() {
-#if 1
         lbool is_sat = l_undef;
         while (is_sat == l_undef && !should_cancel()) {
             if (inconsistent()) is_sat = resolve_conflict_core();
@@ -1614,57 +1613,13 @@ namespace sat {
             else if (!decide()) is_sat = final_check();
         }
         return is_sat;
-#else
-        while (true) {
-            checkpoint();
-            bool done = false;
-            while (!done) {
-                lbool is_sat = propagate_and_backjump_step(done);
-                if (is_sat != l_true) return is_sat;
-            }
-
-            SASSERT(!inconsistent());
-            do_gc();
-
-            if (!decide()) {
-                lbool is_sat = final_check();
-                if (is_sat != l_undef) {
-                    return is_sat;
-                }
-            }
-        }
-#endif
     }
 
     bool solver::should_propagate() const {        
         return !inconsistent() && m_qhead < m_trail.size();
     }
 
 
-    lbool solver::propagate_and_backjump_step(bool& done) {
-        done = true;
-        propagate(true);
-        if (!inconsistent()) {
-            return should_restart() ? l_undef : l_true; 
-        }
-        if (!resolve_conflict())
-            return l_false;
-        if (reached_max_conflicts()) 
-            return l_undef;
-        if (should_rephase()) 
-            do_rephase();
-        if (at_base_lvl()) {
-            do_cleanup(false); // cleaner may propagate frozen clauses
-            if (inconsistent()) {
-                TRACE("sat", tout << "conflict at level 0\n";);
-                return l_false;
-            }
-            do_gc();
-        }
-        done = false;
-        return l_true;
-    }
-
     lbool solver::final_check() {
         if (m_ext) {
             switch (m_ext->check()) {

src/sat/sat_solver.h

@@ -459,29 +459,28 @@ namespace sat {
 
     protected:
 
-        unsigned m_conflicts_since_init;
-        unsigned m_restarts;
-        unsigned m_restart_next_out;
-        unsigned m_conflicts_since_restart;
-        bool     m_force_conflict_analysis;
-        unsigned m_simplifications;
-        unsigned m_restart_threshold;
-        unsigned m_luby_idx;
-        unsigned m_conflicts_since_gc;
-        unsigned m_gc_threshold;
-        unsigned m_defrag_threshold;
-        unsigned m_num_checkpoints;
-        double   m_min_d_tk;
-        unsigned m_next_simplify;
+        unsigned m_conflicts_since_init { 0 };
+        unsigned m_restarts { 0 };
+        unsigned m_restart_next_out { 0 };
+        unsigned m_conflicts_since_restart { 0 };
+        bool     m_force_conflict_analysis { false };
+        unsigned m_simplifications { 0 };
+        unsigned m_restart_threshold { 0 };
+        unsigned m_luby_idx { 0 };
+        unsigned m_conflicts_since_gc { 0 };
+        unsigned m_gc_threshold { 0 };
+        unsigned m_defrag_threshold { 0 };
+        unsigned m_num_checkpoints { 0 };
+        double   m_min_d_tk { 0 } ;
+        unsigned m_next_simplify { 0 };
         bool decide();
         bool_var next_var();
         lbool bounded_search();
         lbool final_check();
-        lbool propagate_and_backjump_step(bool& done);
         void init_search();
 
         literal_vector m_min_core;
-        bool           m_min_core_valid;
+        bool           m_min_core_valid { false };
         void init_reason_unknown() { m_reason_unknown = "no reason given"; }
         void init_assumptions(unsigned num_lits, literal const* lits);
         void reassert_min_core();

src/sat/smt/euf_solver.cpp

@@ -190,6 +190,8 @@ namespace euf {
             if (s().value(lit) == l_true)
                 continue;
             s().assign(literal(v, false), sat::justification::mk_ext_justification(lvl, eq_constraint().to_index()));
+            if (s().inconsistent())
+                return;
         }
         for (euf::enode* p : m_egraph.new_lits()) {
             expr* e = p->get_owner();
@@ -203,6 +205,11 @@ namespace euf {
             if (s().value(lit) == l_false && m_ackerman) 
                 m_ackerman->cg_conflict_eh(p->get_owner(), p->get_root()->get_owner());
             s().assign(lit, sat::justification::mk_ext_justification(lvl, lit_constraint().to_index()));
+            if (s().inconsistent())
+                return;
+        }
+        for (euf::th_eq const& eq : m_egraph.new_th_eqs()) {
+            // m_id2solver[eq.m_id]->new_eq_eh(eq);
         }
     }
 

src/sat/smt/sat_th.h

@@ -18,7 +18,7 @@ Module Name:
 
 #include "util/top_sort.h"
 #include "sat/smt/sat_smt.h"
-#include "ast/euf/euf_enode.h"
+#include "ast/euf/euf_egraph.h"
 
 namespace sat {
 
@@ -63,6 +63,8 @@ namespace sat {
         virtual ~th_solver() {}
 
         virtual th_solver* fresh(solver* s, ast_manager& m, sat_internalizer& si) = 0;        
+
+        virtual void new_eq_eh(euf::th_eq const& eq) {}
     };
 
 

src/util/id_var_list.h

@@ -21,6 +21,7 @@ Revision History:
 #pragma once
 
 #include "util/region.h"
+#include "util/debug.h"
 
 template <int null_id = -1, int null_var = -1>
 class id_var_list {