remove lazy push from theory_lra

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

src/sat/sat_solver/inc_sat_solver.cpp

@@ -666,21 +666,21 @@ class inc_sat_solver : public solver {
             return l_undef;
         }
         g = m_subgoals[0];
-        expr_ref_vector atoms(m);
+        func_decl_ref_vector funs(m);
         m_pc = g->pc();
         m_mcs.set(m_mcs.size()-1, concat(m_mcs.back(), g->mc()));
         TRACE("sat", g->display_with_dependencies(tout););
 
         // ensure that if goal is already internalized, then import mc from m_solver.
 
         m_goal2sat(*g, m_params, m_solver, m_map, m_dep2asm, is_incremental());
-        m_goal2sat.get_interpreted_atoms(atoms);
+        m_goal2sat.get_interpreted_funs(funs);
         if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
         m_sat_mc->flush_smc(m_solver, m_map);
-        if (!atoms.empty()) {
+        if (!funs.empty()) {
             m_has_uninterpreted = true;
             std::stringstream strm;
-            strm << "(sat.giveup interpreted atoms sent to SAT solver " << atoms <<")";
+            strm << "(sat.giveup interpreted functions sent to SAT solver " << funs <<")";
             TRACE("sat", tout << strm.str() << "\n";);
             IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
             set_reason_unknown(strm.str());

src/sat/smt/euf_solver.cpp

@@ -79,6 +79,7 @@ namespace euf {
     }
 
     bool solver::propagate(literal l, ext_constraint_idx idx) { 
+		force_push();
         auto* ext = sat::constraint_base::to_extension(idx);
         SASSERT(ext != this);
         return ext->propagate(l, idx);
@@ -101,17 +102,17 @@ namespace euf {
         // init_ackerman();
 
         switch (j.kind()) {
-        case constraint::conflict:
+        case constraint::kind_t::conflict:
             SASSERT(m_egraph.inconsistent());
             m_egraph.explain<unsigned>(m_explain);
             break;
-        case constraint::eq:
+        case constraint::kind_t::eq:
             n = m_var2node[l.var()].first;
             SASSERT(n);
             SASSERT(m_egraph.is_equality(n));
             m_egraph.explain_eq<unsigned>(m_explain, n->get_arg(0), n->get_arg(1), n->commutative());
             break;
-        case constraint::lit:
+        case constraint::kind_t::lit:
             p = m_var2node[l.var()];
             n = p.first;
             sign = l.sign() != p.second;
@@ -127,15 +128,18 @@ namespace euf {
     }
 
     void solver::asserted(literal l) {
+
         auto* ext = get_solver(l.var());
         if (ext) {
+			force_push();
             ext->asserted(l);
             return;
         }
 
         auto p = m_var2node.get(l.var(), enode_bool_pair(nullptr, false));
         if (!p.first)
             return;
+		force_push();
         bool sign = p.second != l.sign();
         euf::enode* n = p.first;
         expr* e = n->get_owner();
@@ -152,7 +156,7 @@ namespace euf {
         propagate();
     }
 
-    void solver::propagate() {        
+    void solver::propagate() {     
         m_egraph.propagate();
         if (m_egraph.inconsistent()) {       
             s().set_conflict(sat::justification::mk_ext_justification(s().scope_lvl(), conflict_constraint().to_index()));
@@ -196,6 +200,7 @@ namespace euf {
     }
 
     sat::check_result solver::check() { 
+		force_push();
         bool give_up = false;
         bool cont = false;
         for (auto* e : m_solvers)
@@ -212,27 +217,40 @@ namespace euf {
     }
 
     void solver::push() {
-        for (auto* e : m_solvers)
-            e->push();
-        m_egraph.push();
         ++m_num_scopes;
     }
 
+	void solver::force_push() {
+		for (; m_num_scopes > 0; --m_num_scopes) {
+			scope s;
+			s.m_bool_var_lim = m_bool_var_trail.size();
+			s.m_trail_lim = m_trail.size();
+			m_scopes.push_back(s);
+			for (auto* e : m_solvers)
+				e->push();
+			m_egraph.push();
+		}
+	}
+
     void solver::pop(unsigned n) {
-        m_egraph.pop(n);
-        for (auto* e : m_solvers)
-            e->pop(n);
         if (n <= m_num_scopes) {
             m_num_scopes -= n;
             return;
         }
         n -= m_num_scopes;
-        unsigned old_lim = m_bool_var_lim.size() - n;
-        unsigned old_sz = m_bool_var_lim[old_lim];
-        for (unsigned i = m_bool_var_trail.size(); i-- > old_sz; )
+        m_egraph.pop(n);
+        for (auto* e : m_solvers)
+            e->pop(n);
+
+		scope & s = m_scopes[m_scopes.size() - n];
+
+        for (unsigned i = m_bool_var_trail.size(); i-- > s.m_bool_var_lim; )
             m_var2node[m_bool_var_trail[i]] = enode_bool_pair(nullptr, false);
-        m_bool_var_trail.shrink(old_sz);
-        m_bool_var_lim.shrink(old_lim);
+        m_bool_var_trail.shrink(s.m_bool_var_lim);
+
+		undo_trail_stack(*this, m_trail, s.m_trail_lim);
+
+        m_scopes.shrink(m_scopes.size() - n);
     }
 
     void solver::pre_simplify() {
@@ -312,6 +330,7 @@ namespace euf {
     }
 
     void solver::pop_reinit() {
+		force_push();
         for (auto* e : m_solvers)
             e->pop_reinit();
     }
@@ -390,6 +409,7 @@ namespace euf {
     }
 
     sat::literal solver::internalize(expr* e, bool sign, bool root) {
+		force_push();
         auto* ext = get_solver(e);
         if (ext)
             return ext->internalize(e, sign, root);
@@ -463,8 +483,6 @@ namespace euf {
 
     void solver::attach_bool_var(sat::bool_var v, bool sign, euf::enode* n) {
         m_var2node.reserve(v + 1, enode_bool_pair(nullptr, false));
-        for (; m_num_scopes > 0; --m_num_scopes) 
-            m_bool_var_lim.push_back(m_bool_var_trail.size());   
         SASSERT(m_var2node[v].first == nullptr);
         m_var2node[v] = euf::enode_bool_pair(n, sign);
         m_bool_var_trail.push_back(v);

src/sat/smt/euf_solver.h

@@ -17,6 +17,7 @@ Module Name:
 #pragma once
 
 #include "util/scoped_ptr_vector.h"
+#include "util/trail.h"
 #include "ast/ast_translation.h"
 #include "ast/euf/euf_egraph.h"
 #include "smt/params/smt_params.h"
@@ -35,12 +36,12 @@ namespace euf {
 
     class constraint {
     public:
-        enum kind_t { conflict, eq, lit};
+        enum class kind_t { conflict, eq, lit};
     private:
         kind_t m_kind;
     public:
         constraint(kind_t k) : m_kind(k) {}
-        unsigned kind() const { return m_kind; }
+        kind_t kind() const { return m_kind; }
         static constraint* from_idx(size_t z) { return reinterpret_cast<constraint*>(z); }
         size_t to_index() const { return sat::constraint_base::mem2base(this); }
     };
@@ -53,15 +54,23 @@ namespace euf {
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
         };
+		struct scope {
+			unsigned m_bool_var_lim;
+			unsigned m_trail_lim;
+		};
+		typedef ptr_vector<trail<solver> > trail_stack;
 
         ast_manager&          m;
         atom2bool_var&        m_expr2var;
         sat::sat_internalizer& si;
         smt_params            m_config;
         euf::egraph           m_egraph;
         stats                 m_stats;
-        sat::solver*          m_solver { nullptr };
-        sat::lookahead*       m_lookahead { nullptr };
+
+		trail_stack           m_trail;
+
+        sat::solver*           m_solver { nullptr };
+        sat::lookahead*        m_lookahead { nullptr };
         ast_manager*           m_to_m;
         atom2bool_var*         m_to_expr2var;
         sat::sat_internalizer* m_to_si;
@@ -73,7 +82,7 @@ namespace euf {
         svector<sat::frame>                             m_stack;
         unsigned                                        m_num_scopes { 0 };
         unsigned_vector                                 m_bool_var_trail;
-        unsigned_vector                                 m_bool_var_lim;
+		svector<scope>                                  m_scopes;
         scoped_ptr_vector<sat::th_solver>               m_solvers;
         ptr_vector<sat::th_solver>                      m_id2solver;
 
@@ -109,11 +118,12 @@ namespace euf {
         // solving
         void propagate();
         void get_antecedents(literal l, constraint& j, literal_vector& r);
+		void force_push();
 
         constraint& mk_constraint(constraint*& c, constraint::kind_t k);
-        constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::conflict); }
-        constraint& eq_constraint() { return mk_constraint(m_eq, constraint::eq); }
-        constraint& lit_constraint() { return mk_constraint(m_lit, constraint::lit); }
+        constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
+        constraint& eq_constraint() { return mk_constraint(m_eq, constraint::kind_t::eq); }
+        constraint& lit_constraint() { return mk_constraint(m_lit, constraint::kind_t::lit); }
 
     public:
        solver(ast_manager& m, atom2bool_var& expr2var, sat::sat_internalizer& si, params_ref const& p = params_ref()):

src/sat/tactic/goal2sat.cpp

@@ -66,11 +66,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
     bool                        m_ite_extra;
     unsigned long long          m_max_memory;
     expr_ref_vector             m_trail;
-    expr_ref_vector             m_interpreted_atoms;
+    func_decl_ref_vector        m_interpreted_funs;
     bool                        m_default_external;
     bool                        m_xor_solver;
     bool                        m_euf;
-
+    sat::literal_vector         aig_lits;
 
     imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
         m(_m),
@@ -80,7 +80,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_map(map),
         m_dep2asm(dep2asm),
         m_trail(m),
-        m_interpreted_atoms(m),
+        m_interpreted_funs(m),
         m_default_external(default_external) {
         updt_params(p);
         m_true = sat::null_literal;
@@ -174,7 +174,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                         return;
                     }
                     else
-                        m_interpreted_atoms.push_back(t);
+                        m_interpreted_funs.push_back(to_app(t)->get_decl());
                 }
             }
         }
@@ -257,8 +257,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
-    sat::literal_vector aig_lits;
-
     void convert_or(app * t, bool root, bool sign) {
         TRACE("goal2sat", tout << "convert_or:\n" << mk_bounded_pp(t, m, 2) << "\n";);
         unsigned num = t->get_num_args();
@@ -775,8 +773,7 @@ bool goal2sat::has_unsupported_bool(goal const & g) {
 }
 
 goal2sat::goal2sat():
-    m_imp(nullptr), 
-    m_interpreted_atoms(nullptr) {
+    m_imp(nullptr) {
 }
 
 goal2sat::~goal2sat() {
@@ -795,23 +792,21 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core
 
     (*m_imp)(g);
 
-    m_interpreted_atoms = alloc(expr_ref_vector, g.m());
-    m_interpreted_atoms->append(m_imp->m_interpreted_atoms);
-    if (!t.get_extension()) {
+    if (!t.get_extension() && m_imp->m_interpreted_funs.empty()) {
         dealloc(m_imp);
         m_imp = nullptr;
     }
 
 }
 
-void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) {
-    if (m_interpreted_atoms) {
-        atoms.append(*m_interpreted_atoms);
+void goal2sat::get_interpreted_funs(func_decl_ref_vector& atoms) {
+    if (m_imp) {
+        atoms.append(m_imp->m_interpreted_funs);
     }
 }
 
-bool goal2sat::has_interpreted_atoms() const {
-    return m_interpreted_atoms && !m_interpreted_atoms->empty();
+bool goal2sat::has_interpreted_funs() const {
+    return m_imp && !m_imp->m_interpreted_funs.empty(); 
 }
 
 

src/sat/tactic/goal2sat.h

@@ -38,7 +38,6 @@ Module Name:
 class goal2sat {
     struct imp;
     imp *  m_imp;
-    scoped_ptr<expr_ref_vector> m_interpreted_atoms;
 
 public:
     goal2sat();
@@ -62,9 +61,9 @@ class goal2sat {
     */
     void operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
 
-    void get_interpreted_atoms(expr_ref_vector& atoms);
+    void get_interpreted_funs(func_decl_ref_vector& atoms);
 
-    bool has_interpreted_atoms() const;
+    bool has_interpreted_funs() const;
 
     sat::sat_internalizer& si(ast_manager& m, params_ref const& p, sat::solver_core& t, atom2bool_var& a2b, dep2asm_map& dep2asm, bool default_external = false);
 

src/sat/tactic/sat_tactic.cpp

@@ -112,7 +112,7 @@ class sat_tactic : public tactic {
                 ref<sat2goal::mc> mc;
                 m_sat2goal(*m_solver, map, m_params, *(g.get()), mc);
                 g->add(mc.get());
-                if (produce_core || m_goal2sat.has_interpreted_atoms()) {
+                if (produce_core || m_goal2sat.has_interpreted_funs()) {
                     // sat2goal does not preseve assumptions or assignments to interpreted atoms
                     g->updt_prec(goal::OVER);
                 }