tidy'

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

src/sat/smt/polysat_constraints.h

@@ -73,8 +73,6 @@ namespace polysat {
         bool is_eq(pvar& v, rational& val) { throw default_exception("nyi"); }
     };
 
-    using dependent_constraint = std::pair<signed_constraint, stacked_dependency*>;
-
     class constraints {
         trail_stack& m_trail;
     public:

src/sat/smt/polysat_core.cpp

@@ -40,7 +40,7 @@ namespace polysat {
     public:
         mk_assign_var(pvar v, core& c) : m_var(v), c(c) {}
         void undo() {
-            c.m_justification[m_var] = nullptr;
+            c.m_justification[m_var] = dependency::null_dependency();
             c.m_assignment.pop();
         }
     };
@@ -84,7 +84,6 @@ namespace polysat {
         m_viable(*this),
         m_constraints(s.get_trail_stack()),
         m_assignment(*this),
-        m_dep(s.get_region()),
         m_var_queue(m_activity)
     {}
 
@@ -107,7 +106,7 @@ namespace polysat {
         unsigned v = m_vars.size();
         m_vars.push_back(sz2pdd(sz).mk_var(v));
         m_activity.push_back({ sz, 0 });
-        m_justification.push_back(nullptr);
+        m_justification.push_back(dependency::null_dependency());
         m_watch.push_back({});
         m_var_queue.mk_var_eh(v);
         s.ctx.push(mk_add_var(*this));
@@ -123,9 +122,9 @@ namespace polysat {
         m_var_queue.del_var_eh(v);
     }
 
-    unsigned core::register_constraint(signed_constraint& sc, solver_assertion as) {
+    unsigned core::register_constraint(signed_constraint& sc, dependency d) {
         unsigned idx = m_constraint_trail.size();
-        m_constraint_trail.push_back({ sc, as });
+        m_constraint_trail.push_back({ sc, d });
         auto& vars = sc.vars();
         unsigned i = 0, j = 0, sz = vars.size();
         for (; i < sz && j < 2; ++i)
@@ -172,15 +171,24 @@ namespace polysat {
             return false;
         s.ctx.push(value_trail(m_qhead));
         for (; m_qhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_qhead)
-            propagate_constraint(m_prop_queue[m_qhead]);        
+            propagate_assignment(m_prop_queue[m_qhead]);        
         s.ctx.push(value_trail(m_vqhead));
         for (; m_vqhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_vqhead) 
             propagate_value(m_prop_queue[m_vqhead]);        
         return true;
     }
 
-    void core::propagate_constraint(prop_item& dc) { 
+    signed_constraint core::get_constraint(unsigned idx, bool sign) {
-        auto [idx, sc, dep] = dc;
+        auto sc = m_constraint_trail[idx].sc;
+        if (sign)
+            sc = ~sc;
+        return sc;
+    }
+
+
+    void core::propagate_assignment(prop_item& dc) { 
+        auto [idx, sign, dep] = dc;
+        auto sc = get_constraint(idx, sign);
         if (sc.is_eq(m_var, m_value))
             propagate_assignment(m_var, m_value, dep);
     }
@@ -189,7 +197,7 @@ namespace polysat {
         m_watch[var].push_back(idx);
     }
 
-    void core::propagate_assignment(pvar v, rational const& value, stacked_dependency* dep) {
+    void core::propagate_assignment(pvar v, rational const& value, dependency dep) {
         if (is_assigned(v))
             return;
         if (m_var_queue.contains(v)) {
@@ -238,13 +246,15 @@ namespace polysat {
     }
 
     void core::propagate_value(prop_item const& dc) {
-        auto [idx, sc, dep] = dc;
+        auto [idx, sign, dep] = dc;
+        auto sc = get_constraint(idx, sign);
         // check if sc evaluates to false
         switch (eval(sc)) {
         case l_true:
-            return;
+            break;
         case l_false:
-            m_unsat_core = explain_eval({ sc, dep });
+            m_unsat_core = explain_eval(sc);
+            m_unsat_core.push_back(dep);
             propagate_unsat_core();
             return;
         default:
@@ -253,15 +263,13 @@ namespace polysat {
         // if sc is v == value, then check the watch list for v to propagate truth assignments
         if (sc.is_eq(m_var, m_value)) {
             for (auto idx : m_watch[m_var]) {
-                auto [sc, as] = m_constraint_trail[idx];
+                auto [sc, d] = m_constraint_trail[idx];
                 switch (eval(sc)) {
                 case l_false:
-                    m_unsat_core = explain_eval({ sc, nullptr });
+                    s.propagate(d, true, explain_eval(sc));
-                    s.propagate(as, true, m_unsat_core);
                     break;
                 case l_true:
-                    m_unsat_core = explain_eval({ sc, nullptr });
+                    s.propagate(d, false, explain_eval(sc));
-                    s.propagate(as, false, m_unsat_core);
                     break;
                 default:
                     break;
@@ -272,12 +280,13 @@ namespace polysat {
 
     void core::propagate_unsat_core() { 
         // default is to use unsat core:
-        s.set_conflict(m_unsat_core);
         // if core is based on viable, use s.set_lemma();
+
+        s.set_conflict(m_unsat_core);
     }
 
-    void core::assign_eh(unsigned index, signed_constraint const& sc, dependency const& dep) { 
+    void core::assign_eh(unsigned index, bool sign, dependency const& dep) { 
-        m_prop_queue.push_back({ index, sc, m_dep.mk_leaf(dep) });
+        m_prop_queue.push_back({ index, sign, dep });
         s.ctx.push(push_back_vector(m_prop_queue));
     }
 

src/sat/smt/polysat_core.h

@@ -30,45 +30,36 @@ namespace polysat {
     class core;
     class solver;
 
-    struct solver_assertion {
-        unsigned m_var1;
-        unsigned m_var2 = 0;
-    public:
-        solver_assertion(sat::literal lit) : m_var1(2*lit.index()) {}
-        solver_assertion(unsigned v1, unsigned v2) : m_var1(1 + 2*v1), m_var2(v2) {}
-        bool is_literal() const { return m_var1 % 2 == 0; }
-        sat::literal get_literal() const { SASSERT(is_literal()); return sat::to_literal(m_var1 / 2); }
-        unsigned var1() const { SASSERT(!is_literal()); return (m_var1 - 1) / 2; }
-        unsigned var2() const { SASSERT(!is_literal()); return m_var2; }
-    };
-
     class core {
         class mk_add_var;
         class mk_dqueue_var;
         class mk_assign_var;
         class mk_add_watch;
         typedef svector<std::pair<unsigned, unsigned>> activity;
-        typedef std::tuple<unsigned, signed_constraint, stacked_dependency*> prop_item;
+        typedef std::tuple<unsigned, bool, dependency> prop_item;
         friend class viable;
         friend class constraints;
         friend class assignment;
 
+        struct constraint_info {
+            signed_constraint sc;
+            dependency d;
+        };
         solver& s;
         viable m_viable;
         constraints m_constraints;
         assignment m_assignment;
         unsigned m_qhead = 0, m_vqhead = 0;
         svector<prop_item> m_prop_queue;
-        svector<std::tuple<signed_constraint, solver_assertion>> m_constraint_trail;  // 
+        svector<constraint_info> m_constraint_trail;  // index of constraints
-        stacked_dependency_manager<dependency>     m_dep;
         mutable scoped_ptr_vector<dd::pdd_manager> m_pdd;
         dependency_vector m_unsat_core;
 
 
         // attributes associated with variables
-        vector<pdd>            m_vars;                       // for each variable a pdd
+        vector<pdd>             m_vars;                       // for each variable a pdd
-        vector<rational>       m_values;                     // current value of assigned variable
+        vector<rational>        m_values;                     // current value of assigned variable
-        ptr_vector<stacked_dependency>     m_justification;  // justification for assignment
+        svector<dependency>     m_justification;  // justification for assignment
         activity                m_activity;                  // activity of variables
         var_queue<activity>     m_var_queue;                 // priority queue of variables to assign
         vector<unsigned_vector> m_watch;                     // watch lists for variables for constraints on m_prop_queue where they occur
@@ -82,25 +73,27 @@ namespace polysat {
         unsigned size(pvar v) const { return var2pdd(v).power_of_2(); }
         void del_var();
 
-        bool is_assigned(pvar v) { return nullptr != m_justification[v]; }
+        bool is_assigned(pvar v) { return !m_justification[v].is_null(); }
-        void propagate_constraint(prop_item& dc);
         void propagate_value(prop_item const& dc);
-        void propagate_assignment(pvar v, rational const& value, stacked_dependency* dep);
+        void propagate_assignment(prop_item& dc);
+        void propagate_assignment(pvar v, rational const& value, dependency dep);
         void propagate_unsat_core();
 
         void add_watch(unsigned idx, unsigned var);
 
+        signed_constraint get_constraint(unsigned idx, bool sign);
+
         lbool eval(signed_constraint sc) { throw default_exception("nyi"); }
-        dependency_vector explain_eval(dependent_constraint const& dc) { throw default_exception("nyi"); }
+        dependency_vector explain_eval(signed_constraint const& dc) { throw default_exception("nyi"); }
 
     public:
         core(solver& s);
 
         sat::check_result check();
 
-        unsigned register_constraint(signed_constraint& sc, solver_assertion sa);
+        unsigned register_constraint(signed_constraint& sc, dependency d);
         bool propagate();
-        void assign_eh(unsigned idx, signed_constraint const& sc, dependency const& dep);
+        void assign_eh(unsigned idx, bool sign, dependency const& d);
 
         pdd value(rational const& v, unsigned sz);
 

src/sat/smt/polysat_internalize.cpp

@@ -163,23 +163,18 @@ namespace polysat {
     public:
         mk_atom_trail(sat::bool_var v, solver& th) : th(th), m_var(v) {}
         void undo() override {
-            solver::atom* a = th.get_bv2a(m_var);
-            a->~atom();
             th.erase_bv2a(m_var);
         }
     };
 
-    solver::atom* solver::mk_atom(sat::literal lit, signed_constraint& sc) {
+    void solver::mk_atom(sat::bool_var bv, signed_constraint& sc) {
-        auto bv = lit.var();
+        if (get_bv2a(bv))
-        atom* a = get_bv2a(bv);
+            return;
-        if (a)
+        sat::literal lit(bv, false);
-            return a;
+        auto index = m_core.register_constraint(sc, dependency(lit, 0));
-        a = new (get_region()) atom(bv);
+        auto a = new (get_region()) atom(bv, index);
         insert_bv2a(bv, a);
-        a->m_sc = sc;
-        a->m_index = m_core.register_constraint(sc, lit);
         ctx.push(mk_atom_trail(bv, *this));
-        return a;
     }
 
     void solver::internalize_binaryc(app* e, std::function<polysat::signed_constraint(pdd, pdd)> const& fn) {
@@ -187,7 +182,9 @@ namespace polysat {
         auto q = expr2pdd(e->get_arg(1));
         auto sc = ~fn(p, q);
         sat::literal lit = expr2literal(e);
-        auto* a = mk_atom(lit, sc);
+        if (lit.sign())
+            sc = ~sc;
+        mk_atom(lit.var(), sc);
     }
 
     void solver::internalize_div_rem_i(app* e, bool is_div) {
@@ -290,12 +287,9 @@ namespace polysat {
             sc = ~sc;
         
         sat::literal lit = expr2literal(e);
-        atom* a = mk_atom(lit, sc);
+        if (lit.sign())
-    }
+            sc = ~sc;
-
+        mk_atom(lit.var(), sc);
-    void solver::internalize_bit2bool(atom* a, expr* e, unsigned idx) {
-        pdd p = expr2pdd(e);
-        a->m_sc = m_core.bit(p, idx);
     }
 
     dd::pdd solver::expr2pdd(expr* e) {

src/sat/smt/polysat_solver.cpp

@@ -58,15 +58,12 @@ namespace polysat {
     }
 
     void solver::asserted(literal l) {
-        atom* a = get_bv2a(l.var());
         TRACE("bv", tout << "asserted: " << l << "\n";);
+        atom* a = get_bv2a(l.var());
         if (!a)
             return;
         force_push();
-        auto sc = a->m_sc;
+        m_core.assign_eh(a->m_index, l.sign(), dependency(l, s().lvl(l)));
-        if (l.sign())
-            sc = ~sc;
-        m_core.assign_eh(a->m_index, sc, dependency(l, s().lvl(l)));
     }
 
     void solver::set_conflict(dependency_vector const& core) {
@@ -150,10 +147,11 @@ namespace polysat {
         pdd p = var2pdd(v1);
         pdd q = var2pdd(v2);
         auto sc = m_core.eq(p, q);        
-        m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2));
+        m_var_eqs.setx(m_var_eqs_head, {v1, v2}, {v1, v2});
         ctx.push(value_trail<unsigned>(m_var_eqs_head));    
-        unsigned index = m_core.register_constraint(sc, solver_assertion(v1, v2));
+        auto d = dependency(m_var_eqs_head, s().scope_lvl());
-        m_core.assign_eh(index, sc, dependency(m_var_eqs_head, s().scope_lvl())); 
+        unsigned index = m_core.register_constraint(sc, d);
+        m_core.assign_eh(index, false, d); 
         m_var_eqs_head++;
     }
 
@@ -163,9 +161,10 @@ namespace polysat {
         pdd q = var2pdd(v2);
         auto sc = ~m_core.eq(p, q);
         sat::literal neq = ~expr2literal(ne.eq());
-        auto index = m_core.register_constraint(sc, neq);
+        auto d = dependency(neq, s().lvl(neq));
+        auto index = m_core.register_constraint(sc, d);
         TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n");
-        m_core.assign_eh(index, sc, dependency(neq, s().lvl(neq)));
+        m_core.assign_eh(index, false, d);
     }
 
     // Core uses the propagate callback to add unit propagations to the trail.
@@ -178,19 +177,22 @@ namespace polysat {
         ctx.propagate(lit, ex);
     }
 
-    void solver::propagate(solver_assertion as, bool sign, dependency_vector const& deps) {
+    void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps) {
         auto [core, eqs] = explain_deps(deps);
-        if (as.is_literal()) {
+        if (d.is_literal()) {
-            auto lit = as.get_literal();
+            auto lit = d.literal();
             if (sign)
                 lit.neg();
+            if (s().value(lit) == l_true)
+                return;
             auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);
             ctx.propagate(lit, ex);
         }
-        else if (sign) {           
+        else if (sign) {  
+            auto const [v1, v2] = m_var_eqs[d.index()];
             // equalities are always asserted so a negative propagation is a conflict.
-            auto n1 = var2enode(as.var1());
+            auto n1 = var2enode(v1);
-            auto n2 = var2enode(as.var2());
+            auto n2 = var2enode(v2);
             eqs.push_back({ n1, n2 });
             auto ex = euf::th_explain::conflict(*this, core, eqs, nullptr);
             ctx.set_conflict(ex);
@@ -223,6 +225,7 @@ namespace polysat {
         }
         case ckind_t::smul_fl_t:
         case ckind_t::op_t:
+            NOT_IMPLEMENTED_YET();
             break;
         }
         throw default_exception("nyi"); 

src/sat/smt/polysat_solver.h

@@ -42,9 +42,8 @@ namespace polysat {
 
         struct atom {
             bool_var                m_bv;
-            unsigned                m_index = 0;
+            unsigned                m_index;
-            signed_constraint       m_sc;
+            atom(bool_var b, unsigned index) :m_bv(b), m_index(index) {}
-            atom(bool_var b) :m_bv(b) {}
             ~atom() { }
         };
 
@@ -92,7 +91,7 @@ namespace polysat {
         void erase_bv2a(bool_var bv) { m_bool_var2atom[bv] = nullptr; }
         atom* get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, nullptr); }
         class mk_atom_trail;
-        atom* mk_atom(sat::literal lit, signed_constraint& sc);
+        void  mk_atom(sat::bool_var bv, signed_constraint& sc);
         void set_bit_eh(theory_var v, literal l, unsigned idx);
         void init_bits(expr* e, expr_ref_vector const & bits);
         void mk_bits(theory_var v);
@@ -122,7 +121,6 @@ namespace polysat {
         void internalize_polysat(app* a);
         void assert_bv2int_axiom(app * n);
         void assert_int2bv_axiom(app* n);
-        void internalize_bit2bool(atom* a, expr* e, unsigned idx);
 
         pdd expr2pdd(expr* e);
         pdd var2pdd(euf::theory_var v);
@@ -134,7 +132,7 @@ namespace polysat {
         void set_conflict(dependency_vector const& core);
         void set_lemma(vector<signed_constraint> const& lemma, unsigned level, dependency_vector const& core);
         void propagate(signed_constraint sc, dependency_vector const& deps);
-        void propagate(solver_assertion as, bool sign, dependency_vector const& deps);
+        void propagate(dependency const& d, bool sign, dependency_vector const& deps);
         
         void add_lemma(vector<signed_constraint> const& lemma);
 

src/sat/smt/polysat_types.h

@@ -11,28 +11,26 @@ Author:
 
 #include "math/dd/dd_pdd.h"
 #include "util/sat_literal.h"
-#include "util/dependency.h"
 
 namespace polysat {
 
     using pdd = dd::pdd;
     using pvar = unsigned;
 
-
     class dependency {
         unsigned m_index;
         unsigned m_level;
     public:
         dependency(sat::literal lit, unsigned level) : m_index(2 * lit.index()), m_level(level) {}
         dependency(unsigned var_idx, unsigned level) : m_index(1 + 2 * var_idx), m_level(level) {} 
+        static dependency null_dependency() { return dependency(0, UINT_MAX); }
+        bool is_null() const { return m_level == UINT_MAX; }
         bool is_literal() const { return m_index % 2 == 0; }
         sat::literal literal() const { SASSERT(is_literal());  return sat::to_literal(m_index / 2); }
         unsigned index() const { SASSERT(!is_literal()); return (m_index - 1) / 2; }
         unsigned level() const { return m_level; }
     };
 
-    using stacked_dependency = stacked_dependency_manager<dependency>::dependency;
-
     inline std::ostream& operator<<(std::ostream& out, dependency d) {
         if (d.is_literal())
             return out << d.literal() << "@" << d.level();