add variable replay, remove MacOS from Travis (#4681)

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* dbg

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

* bv

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

* drat and fresh

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

* move ackerman functionality

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

* na

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

* debugability

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

* towards debugability

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

* missing file

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

* na

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

* na

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

* remove csp

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

* replay variables created by solver

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

* remove old function

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

* fix scoped-limit

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

src/sat/sat_solver.cpp

@@ -38,6 +38,7 @@ Revision History:
 #endif
 
 #define ENABLE_TERNARY true
+#define DYNAMIC_VARS true
 
 namespace sat {
 
@@ -243,10 +244,45 @@ namespace sat {
     //
     // -----------------------
 
+    void solver::reset_var(bool_var v, bool ext, bool dvar) {
+        m_watches[2*v].reset();
+        m_watches[2*v+1].reset();
+        m_assignment[2*v] = l_undef;
+        m_assignment[2*v+1] = l_undef;
+        m_justification[2*v] = justification(UINT_MAX);
+        m_decision[v] = dvar;
+        m_eliminated[v] = false;
+        m_external[v] = ext;
+        m_touched[v] = 0;
+        m_activity[v] = 0;
+        m_mark[v] = false;
+        m_lit_mark[2*v] = false;
+        m_lit_mark[2*v+1] = false;
+        m_phase[v] = false;
+        m_best_phase[v] = false;
+        m_prev_phase[v] = false;
+        m_assigned_since_gc[v] = false;
+        m_last_conflict[v] = 0;        
+        m_last_propagation[v] = 0;
+        m_participated[v] = 0;
+        m_canceled[v] = 0;
+        m_reasoned[v] = 0;
+        m_case_split_queue.mk_var_eh(v);
+        m_simplifier.insert_elim_todo(v);
+    }
+
     bool_var solver::mk_var(bool ext, bool dvar) {
         m_model_is_current = false;
         m_stats.m_mk_var++;
         bool_var v = m_justification.size();
+        if (!m_free_vars.empty()) {
+            v = m_free_vars.back();
+            m_free_vars.pop_back();
+            m_active_vars.push_back(v);
+            reset_var(v, ext, dvar);
+            return v;
+        }
+        m_active_vars.push_back(v);
         m_watches.push_back(watch_list());
         m_watches.push_back(watch_list());
         m_assignment.push_back(l_undef);
@@ -3212,7 +3248,7 @@ namespace sat {
         for (unsigned i = 0; i < num; i++) {
             SASSERT(value(lits[i]) != l_undef);
             unsigned lit_lvl = lvl(lits[i]);
-            if (m_diff_levels[lit_lvl] == false) {
+            if (!m_diff_levels[lit_lvl]) {
                 m_diff_levels[lit_lvl] = true;
                 r++;
             }
@@ -3230,14 +3266,13 @@ namespace sat {
         for (; i < num && glue < max_glue; i++) {
             SASSERT(value(lits[i]) != l_undef);
             unsigned lit_lvl = lvl(lits[i]);
-            if (m_diff_levels[lit_lvl] == false) {
+            if (!m_diff_levels[lit_lvl]) {
                 m_diff_levels[lit_lvl] = true;
                 glue++;
             }
-        }
+        }       
-        num = i;
         // reset m_diff_levels.
-        for (i = 0; i < num; i++)
+        for (; i-- > 0; )
             m_diff_levels[lvl(lits[i])] = false;
         return glue < max_glue;        
     }
@@ -3249,15 +3284,14 @@ namespace sat {
         for (; i < num && glue < max_glue; i++) {
             if (value(lits[i]) == l_false) {
                 unsigned lit_lvl = lvl(lits[i]);
-                if (m_diff_levels[lit_lvl] == false) {
+                if (!m_diff_levels[lit_lvl]) {
                     m_diff_levels[lit_lvl] = true;
                     glue++;
                 }
             }
         }
-        num = i;
         // reset m_diff_levels.
-        for (i = 0; i < num; i++) {
+        for (; i-- > 0;) {
             literal lit = lits[i];
             if (value(lit) == l_false) {
                 VERIFY(lvl(lit) < m_diff_levels.size());
@@ -3653,9 +3687,12 @@ namespace sat {
         s.m_trail_lim = m_trail.size();
         s.m_clauses_to_reinit_lim = m_clauses_to_reinit.size();
         s.m_inconsistent = m_inconsistent;
-        // m_vars_lim.push(num_vars());
+        if (m_ext) {
-        if (m_ext)
+#if DYNAMIC_VARS
+            m_vars_lim.push(m_active_vars.size());
+#endif
             m_ext->push();
+        }
     }
 
     void solver::pop_reinit(unsigned num_scopes) {
@@ -3666,13 +3703,35 @@ namespace sat {
     }
 
     void solver::pop_vars(unsigned num_scopes) {
+        m_vars_to_reinit.reset();
         unsigned old_num_vars = m_vars_lim.pop(num_scopes);
-        if (old_num_vars == num_vars()) 
+        if (old_num_vars == m_active_vars.size())
             return;
-        IF_VERBOSE(0, verbose_stream() << "new variables created under scope\n";);
+        init_visited();
-        for (unsigned v = old_num_vars; v < num_vars(); ++v) {
+        unsigned new_lvl = scope_lvl() - num_scopes;
-            
+        unsigned old_sz = m_scopes[new_lvl].m_clauses_to_reinit_lim;
+        for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; ) {
+            clause_wrapper const& cw = m_clauses_to_reinit[i];
+            for (unsigned j = cw.size(); j-- > 0; )
+                mark_visited(cw[j]);
         }
+        for (literal lit : m_lemma)
+            mark_visited(lit);
+               
+        unsigned sz = m_active_vars.size(), j = old_num_vars;
+        for (unsigned i = old_num_vars; i < sz; ++i) {
+            bool_var v = m_active_vars[i];
+            if (is_visited(v)) {
+                m_vars_to_reinit.push_back(v);
+                m_active_vars[j++] = v;
+            }
+            else {
+                set_eliminated(v, true);
+                m_free_vars.push_back(v);
+            }
+        }
+        m_active_vars.shrink(j);
+        IF_VERBOSE(0, verbose_stream() << "vars to reinit: " << m_vars_to_reinit << " free vars " << m_free_vars << "\n");
     }
 
     void solver::shrink_vars(unsigned v) {
@@ -3702,7 +3761,9 @@ namespace sat {
         if (num_scopes == 0)
             return;
         if (m_ext) {
-            // pop_vars(num_scopes);
+#if DYNAMIC_VARS
+            pop_vars(num_scopes);
+#endif
             m_ext->pop(num_scopes);
         }
         SASSERT(num_scopes <= scope_lvl());
@@ -3713,7 +3774,7 @@ namespace sat {
         m_scope_lvl -= num_scopes;
         m_scopes.shrink(new_lvl);
         reinit_clauses(s.m_clauses_to_reinit_lim);
-        if (m_ext)
+        if (m_ext) 
             m_ext->pop_reinit();
     }
 
@@ -3750,18 +3811,6 @@ namespace sat {
         m_replay_assign.reset();
     }
 
-    void solver::get_reinit_literals(unsigned n, literal_vector& r) {
-        unsigned new_lvl = scope_lvl() - n;
-        unsigned old_sz = m_scopes[new_lvl].m_clauses_to_reinit_lim;
-        for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; ) {
-            clause_wrapper cw = m_clauses_to_reinit[i];
-            for (unsigned j = cw.size(); j-- > 0; )
-                r.push_back(cw[j]);
-        }
-        for (literal lit : m_lemma)
-            r.push_back(lit);
-    }
-
     void solver::reinit_clauses(unsigned old_sz) {
         unsigned sz = m_clauses_to_reinit.size();
         SASSERT(old_sz <= sz);

src/sat/sat_solver.h

@@ -115,6 +115,7 @@ namespace sat {
         clause_vector           m_clauses;
         clause_vector           m_learned;
         unsigned                m_num_frozen;
+        unsigned_vector         m_active_vars, m_free_vars, m_vars_to_reinit;
         vector<watch_list>      m_watches;
         svector<lbool>          m_assignment;
         svector<justification>  m_justification; 
@@ -264,6 +265,8 @@ namespace sat {
         random_gen& rand() { return m_rand; }
 
     protected:
+        void reset_var(bool_var v, bool ext, bool dvar);
+
         inline clause_allocator& cls_allocator() { return m_cls_allocator[m_cls_allocator_idx]; }
         inline clause_allocator const& cls_allocator() const { return m_cls_allocator[m_cls_allocator_idx]; }
         inline clause * alloc_clause(unsigned num_lits, literal const * lits, bool learned) { return cls_allocator().mk_clause(num_lits, lits, learned); }
@@ -645,7 +648,8 @@ namespace sat {
         // -----------------------
     public:
         void set_should_simplify() { m_next_simplify = m_conflicts_since_init; }
-        void get_reinit_literals(unsigned num_scopes, literal_vector& r);
+        bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit;  }
+
     public:
         void user_push() override;
         void user_pop(unsigned num_scopes) override;

src/sat/smt/bv_ackerman.h

@@ -52,7 +52,8 @@ namespace bv {
         table_t       m_table;
         vv*           m_queue { nullptr };
         vv*           m_tmp_vv { nullptr };
-        unsigned      m_gc_threshold { 1 };
+
+        unsigned      m_gc_threshold { 100 };
         unsigned      m_propagate_high_watermark { 10000 };
         unsigned      m_propagate_low_watermark { 10 };
         unsigned      m_num_propagations_since_last_gc { 0 };

src/sat/smt/euf_ackerman.cpp

@@ -47,6 +47,7 @@ namespace euf {
         inf.b = b;
         inf.c = lca;
         inf.is_cc = false;
+        inf.m_count = 0;
         insert();
     }
 

src/sat/smt/euf_ackerman.h

@@ -57,7 +57,7 @@ namespace euf {
         table_t       m_table;
         inference*    m_queue { nullptr };
         inference*    m_tmp_inference { nullptr };
-        unsigned      m_gc_threshold { 1 };
+        unsigned      m_gc_threshold { 100 };
         unsigned      m_high_watermark { 1000 };
         unsigned      m_num_propagations_since_last_gc { 0 };
  

src/sat/smt/euf_solver.cpp

@@ -315,6 +315,7 @@ namespace euf {
     }
 
     void solver::pop(unsigned n) {
+        start_reinit(n);
         m_egraph.pop(n);
         for (auto* e : m_solvers)
             e->pop(n);
@@ -328,28 +329,32 @@ namespace euf {
     }
 
     void solver::start_reinit(unsigned n) {
-        sat::literal_vector lits;
-        m_reinit_vars.reset();
         m_reinit_exprs.reset();
-        s().get_reinit_literals(n, lits);
+        for (sat::bool_var v : s().get_vars_to_reinit()) {
-        for (sat::literal lit : lits) {
-            sat::bool_var v = lit.var();
             expr* e = bool_var2expr(v);
-            if (m_reinit_vars.contains(v) || !e)
-                continue;
-            m_reinit_vars.push_back(v);
             m_reinit_exprs.push_back(e);
         }
     }
 
     void solver::finish_reinit() {
-        unsigned sz = m_reinit_vars.size();
-        for (unsigned i = 0; i < sz; ++i) {
-            euf::enode* n = get_enode(m_reinit_exprs.get(i));
-            if (n)
-                continue;
 
+        SASSERT(s().get_vars_to_reinit().size() == m_reinit_exprs.size());
+        if (s().get_vars_to_reinit().empty())
+            return;
+        unsigned i = 0;
+        obj_map<expr, sat::bool_var> expr2var_replay;
+        for (sat::bool_var v : s().get_vars_to_reinit()) {
+            expr* e = m_reinit_exprs.get(i++);
+            if (!e)
+                continue;
+            expr2var_replay.insert(e, v);
         }
+        if (expr2var_replay.empty())
+            return;
+        si.set_expr2var_replay(&expr2var_replay);
+        for (auto const& kv : expr2var_replay)
+            si.internalize(kv.m_key, true);
+        si.set_expr2var_replay(nullptr);        
     }
 
     void solver::pre_simplify() {
@@ -461,6 +466,7 @@ namespace euf {
     }
 
     void solver::pop_reinit() {
+        finish_reinit();
         for (auto* e : m_solvers)
             e->pop_reinit();
     }

src/sat/smt/euf_solver.h

@@ -118,7 +118,6 @@ namespace euf {
 
         // replay
         expr_ref_vector      m_reinit_exprs;
-        sat::bool_var_vector m_reinit_vars;
         
         void start_reinit(unsigned num_scopes);
         void finish_reinit();

src/sat/smt/sat_smt.h

@@ -44,6 +44,7 @@ namespace sat {
         virtual void cache(app* t, literal l) = 0;
         virtual void push() = 0;
         virtual void pop(unsigned n) = 0;
+        virtual void set_expr2var_replay(obj_map<expr, sat::bool_var>* r) = 0;
     };
     
     class constraint_base {

src/sat/tactic/goal2sat.cpp

@@ -66,6 +66,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     sat::solver_core &          m_solver;
     atom2bool_var &             m_map;
     dep2asm_map &               m_dep2asm;
+    obj_map<expr, sat::bool_var>* m_expr2var_replay { nullptr };
     sat::literal                m_true;
     bool                        m_ite_extra;
     unsigned long long          m_max_memory;
@@ -189,16 +190,26 @@ struct goal2sat::imp : public sat::sat_internalizer {
         return m_map.to_bool_var(e);
     }
 
+
+    void set_expr2var_replay(obj_map<expr, sat::bool_var>* r) override {
+        m_expr2var_replay = r;
+    }
+
+    sat::bool_var mk_bool_var(expr* t) {
+        force_push();
+        sat::bool_var v;
+        if (!m_expr2var_replay || !m_expr2var_replay->find(t, v))  
+            v = add_var(true, t);
+        m_map.insert(t, v);
+        return v;
+    }
+
     sat::bool_var add_bool_var(expr* t) override {
         sat::bool_var v = m_map.to_bool_var(t);
-        if (v == sat::null_bool_var) {
+        if (v == sat::null_bool_var) 
-            v = add_var(true, t);
+            v = mk_bool_var(t);
-            force_push();
+        else 
-            m_map.insert(t, v);
-        }
-        else {
             m_solver.set_external(v);
-        }
         return v;
     }
 
@@ -254,9 +265,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                         m_unhandled_funs.push_back(to_app(t)->get_decl());
                 }
                 bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
-                v = add_var(ext, t);
+                v = mk_bool_var(t);
-                force_push();
-                m_map.insert(t, v);
                 l = sat::literal(v, sign);
                 TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";);
             }

src/shell/drat_frontend.cpp

@@ -102,7 +102,7 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
     dimacs::drat_parser drat(ins, std::cerr);
     std::function<int(char const* read_theory)> read_theory = [&](char const* r) {
         if (strcmp(r, "euf") == 0)
-            return 0;
+            return ctx.m().get_basic_family_id();
         return ctx.m().mk_family_id(symbol(r));
     };
     drat.set_read_theory(read_theory);

src/util/dlist.h

@@ -171,7 +171,10 @@ public:
             elem->m_prev = elem;            
         }
         else if (list != elem) {
-            remove_from(list, elem);
+            auto* next = elem->m_next;
+            auto* prev = elem->m_prev;
+            prev->m_next = next;
+            next->m_prev = prev;        
             list->m_prev->m_next = elem;
             elem->m_prev = list->m_prev;
             elem->m_next = list;

src/util/scoped_limit_trail.h

@@ -15,6 +15,7 @@ class scoped_limit_trail {
         else {
             for (; m_scopes > 0; --m_scopes)
                 m_lim.push_back(m_last);
+            m_lim.push_back(n);
             m_last = n;
         }
     }