change gc strategy for user-push/pop

src/sat/sat_extension.h

@@ -117,7 +117,6 @@ namespace sat {
         virtual void init_use_list(ext_use_list& ul) {}
         virtual bool is_blocked(literal l, ext_constraint_idx) { return false; }
         virtual bool check_model(model const& m) const { return true; }
-        virtual unsigned max_var(unsigned w) const { return w; }
 
         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) {                                

src/sat/smt/ba_solver.cpp

@@ -1863,16 +1863,6 @@ namespace sat {
         c.set_psm(r);
     }
 
-    unsigned ba_solver::max_var(unsigned w) const {
-        for (constraint* cp : m_constraints) {
-            w = cp->fold_max_var(w);
-        }
-        for (constraint* cp : m_learned) {
-            w = cp->fold_max_var(w);
-        }
-        return w;
-    }
-
     void ba_solver::gc() {
         if (m_learned.size() >= 2 * m_constraints.size() && 
             (s().at_search_lvl() || s().at_base_lvl())) {

src/sat/smt/ba_solver.h

@@ -424,7 +424,6 @@ namespace sat {
         void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override;
         void pop_reinit() override;
         void gc() override;
-        unsigned max_var(unsigned w) const override;
         bool is_extended_binary(ext_justification_idx idx, literal_vector & r) override;
         void init_use_list(ext_use_list& ul) override;
         bool is_blocked(literal l, ext_constraint_idx idx) override;

src/sat/smt/bv_solver.cpp

@@ -710,7 +710,6 @@ namespace bv {
     bool solver::is_blocked(literal l, sat::ext_constraint_idx) { return false; }
     bool solver::check_model(sat::model const& m) const { return true; }
     void solver::finalize_model(model& mdl) {}
-    unsigned solver::max_var(unsigned w) const { return w; }
 
     void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
         SASSERT(bv.is_bv(n->get_expr()));

src/sat/smt/bv_solver.h

@@ -335,7 +335,6 @@ namespace bv {
         bool is_blocked(literal l, sat::ext_constraint_idx) override;
         bool check_model(sat::model const& m) const override;
         void finalize_model(model& mdl) override;
-        unsigned max_var(unsigned w) const override;
 
         void new_eq_eh(euf::th_eq const& eq) override;
         void new_diseq_eh(euf::th_eq const& ne) override;

src/sat/smt/euf_solver.cpp

@@ -464,10 +464,13 @@ namespace euf {
             e->pop(n);
         si.pop(n);
         m_egraph.pop(n);
-        scope const & s = m_scopes[m_scopes.size() - n];
-        for (unsigned i = m_var_trail.size(); i-- > s.m_var_lim; )
-            m_bool_var2expr[m_var_trail[i]] = nullptr;
-        m_var_trail.shrink(s.m_var_lim);        
+        scope const & sc = m_scopes[m_scopes.size() - n];
+        for (unsigned i = m_var_trail.size(); i-- > sc.m_var_lim; ) {
+            bool_var v = m_var_trail[i];
+            m_bool_var2expr[v] = nullptr;
+            s().set_non_external(v);
+        }
+        m_var_trail.shrink(sc.m_var_lim);        
         m_scopes.shrink(m_scopes.size() - n);
         SASSERT(m_egraph.num_scopes() == m_scopes.size());
         TRACE("euf_verbose", display(tout << "pop to: " << m_scopes.size() << "\n"););
@@ -476,7 +479,7 @@ namespace euf {
     void solver::user_push() {
         push();
         if (m_dual_solver)
-            m_dual_solver->push();
+            m_dual_solver->push();        
     }
 
     void solver::user_pop(unsigned n) {
@@ -725,20 +728,7 @@ namespace euf {
                 return false;
         return true;
     }
-
-    unsigned solver::max_var(unsigned w) const { 
-        for (auto* e : m_solvers)
-            w = e->max_var(w);
-        for (unsigned sz = m_bool_var2expr.size(); sz > w && sz-- > 0; ) {
-            expr* n = m_bool_var2expr[sz];
-            if (n && m.is_bool(n)) {
-                w = std::max(w, sz);
-                break;
-            }           
-        }
-        return w; 
-    }
-
+
     double solver::get_reward(literal l, ext_constraint_idx idx, sat::literal_occs_fun& occs) const {
         auto* ext = sat::constraint_base::to_extension(idx);
         SASSERT(ext);        

src/sat/smt/euf_solver.h

@@ -304,7 +304,6 @@ namespace euf {
         void init_use_list(sat::ext_use_list& ul) override;
         bool is_blocked(literal l, ext_constraint_idx) override;
         bool check_model(sat::model const& m) const override;
-        unsigned max_var(unsigned w) const override;
 
         // proof
         bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }