bugfixes

src/sat/smt/polysat/core.cpp

@@ -62,11 +62,6 @@ namespace polysat {
             auto& [sc, lit, val] = c.m_constraint_index.back();
             auto& vars = sc.vars();
             auto idx = c.m_constraint_index.size() - 1;
-            IF_VERBOSE(10,
-                verbose_stream() << "undo add watch " << sc << " ";
-            if (vars.size() > 0) verbose_stream() << "(" << idx << ": " << c.m_watch[vars[0]] << ") ";
-            if (vars.size() > 1) verbose_stream() << "(" << idx << ": " << c.m_watch[vars[1]] << ") ";
-            verbose_stream() << "\n");
             unsigned n = sc.num_watch();
             SASSERT(n <= vars.size());
             auto del_watch = [&](unsigned i) {
@@ -147,10 +142,6 @@ namespace polysat {
             add_watch(idx, vars[0]);
         if (j > 1)
             add_watch(idx, vars[1]);
-        IF_VERBOSE(10, verbose_stream() << "add watch " << sc << " " << vars << "  ";
-        if (j > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") ";
-        if (j > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") ";
-        verbose_stream() << "\n");
         s.trail().push(mk_add_watch(*this));
         return { idx };
     }
@@ -166,38 +157,36 @@ namespace polysat {
         CTRACE("bv", is_assigned(m_var), display(tout << "v" << m_var << " is assigned\n"););
         SASSERT(!is_assigned(m_var));
         
-        switch (m_viable.find_viable(m_var, m_value)) {
+        auto& var_value = m_values[m_var];
+        switch (m_viable.find_viable(m_var, var_value)) {
         case find_t::empty:
             viable_conflict(m_var);
             return sat::check_result::CR_CONTINUE;
         case find_t::singleton: {
             auto p = var2pdd(m_var).mk_var(m_var);
-            auto sc = m_constraints.eq(p, m_value);
+            auto sc = m_constraints.eq(p, var_value);
-            TRACE("bv", tout << "check-propagate v" << m_var << " := " << m_value << " " << sc << "\n");
+            TRACE("bv", tout << "check-propagate v" << m_var << " := " << var_value << " " << sc << "\n");
             auto d = s.propagate(sc, m_viable.explain(), "viable-propagate");
-            propagate_assignment(m_var, m_value, d);
+            propagate_assignment(m_var, var_value, d);
             return sat::check_result::CR_CONTINUE;
         }
         case find_t::multiple: {
-            do {
+            dependency d = null_dependency;
-                try_again:
+            lbool value = s.add_eq_literal(m_var, var_value, d);
-                dependency d = null_dependency;
+            TRACE("bv", tout << "check-multiple v" << m_var << " := " << var_value << " " << value << "\n");
-                lbool value = s.add_eq_literal(m_var, m_value, d);
+            switch (value) {
-                TRACE("bv", tout << "check-multiple v" << m_var << " := " << m_value << " " << value << "\n");
+            case l_true:
-                switch (value) {
+                propagate_assignment(m_var, var_value, d);
-                case l_true:
+                break;
-                    propagate_assignment(m_var, m_value, d);
+            case l_false:
-                    break;
+                // disequality is forced into propagation queue.
-                case l_false:   
+                var_value = mod(var_value + 1, rational::power_of_two(size(m_var)));
-                    // add m_var != m_value to m_viable but need a constraint index for that.
+                propagate();
-                    m_value = mod(m_value + 1, rational::power_of_two(size(m_var)));
+                break;
-                    goto try_again;
+            default:
-                default:
+                // let core assign equality.                    
-                    // let core assign equality.                    
+                break;
-                    break;
+            }
-                }
-            } 
-            while (false);
             return sat::check_result::CR_CONTINUE;
         }
         case find_t::resource_out:
@@ -211,14 +200,17 @@ namespace polysat {
     sat::check_result core::final_check() {
         unsigned n = 0;
         constraint_id conflict_idx = { UINT_MAX };
+        // verbose_stream() << "final-check\n";
         for (auto idx : m_prop_queue) {
             auto [sc, d, value] = m_constraint_index[idx.id];
             SASSERT(value != l_undef);
+            // verbose_stream() << "constraint " << (value == l_true ? sc : ~sc) << "\n";
             lbool eval_value = eval(sc);
             CTRACE("bv", eval_value == l_undef, sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n"; display(tout););
             SASSERT(eval_value != l_undef);
             if (eval_value == value)
                 continue;
+            // verbose_stream() << "violated " << sc << " " << d << " " << eval_value << "\n";
             if (0 == (m_rand() % (++n)))
                 conflict_idx = idx;
 
@@ -288,8 +280,9 @@ namespace polysat {
             s.set_conflict({dep}, "infeasible assignment");
             return;
         }
-        if (sc.is_eq(m_var, m_value))
+        rational var_value;
-            propagate_assignment(m_var, m_value, dep);
+        if (sc.is_eq(m_var, var_value))
+            propagate_assignment(m_var, var_value, dep);
         else
             propagate_activation(idx, sc, dep);
     }
@@ -424,7 +417,7 @@ namespace polysat {
         return s.inconsistent();
     }
 
-    void core::assign_eh(constraint_id index, bool sign, unsigned level) { 
+    void core::assign_eh(constraint_id index, bool sign) { 
         struct unassign : public trail {
             core& c;
             unsigned m_index;
@@ -434,6 +427,8 @@ namespace polysat {
                 c.m_prop_queue.pop_back();
             }
         };
+        if (m_constraint_index[index.id].value != l_undef)
+            return;
         m_prop_queue.push_back(index);
         m_constraint_index[index.id].value = to_lbool(!sign);
         s.trail().push(unassign(*this, index.id));
@@ -494,7 +489,7 @@ namespace polysat {
 
     void core::add_axiom(signed_constraint sc) {
         auto idx = register_constraint(sc, dependency::axiom());
-        assign_eh(idx, false, 0);
+        assign_eh(idx, false);
     }
 
     signed_constraint core::get_constraint(constraint_id idx) {

src/sat/smt/polysat/core.h

@@ -69,7 +69,6 @@ namespace polysat {
         vector<unsigned_vector> m_watch;                      // watch lists for variables for constraints on m_prop_queue where they occur
 
         // values to split on
-        rational    m_value;
         pvar        m_var = 0;
 
         dd::pdd_manager& sz2pdd(unsigned sz) const;
@@ -99,7 +98,7 @@ namespace polysat {
         sat::check_result check();        
         constraint_id register_constraint(signed_constraint& sc, dependency d);
         bool propagate();
-        void assign_eh(constraint_id idx, bool sign, unsigned level);
+        void assign_eh(constraint_id idx, bool sign);
         pvar next_var() { return m_var_queue.next_var(); }
 
         pdd value(rational const& v, unsigned sz);

src/sat/smt/polysat/viable.cpp

@@ -107,20 +107,28 @@ namespace polysat {
         m_num_bits = c.size(v);
         m_fixed_bits.reset(v);
         init_overlaps(v);
-
+        bool start_at0 = val1 == 0;
-        rational const& max_value = c.var2pdd(v).max_value();
+        
-
+        
-        val1 = 0;
         lbool r = next_viable(val1);
         TRACE("bv", display_state(tout); display(tout << "next viable v" << v << " " << val1 << " " << r << "\n"));
+        if (r == l_false && !start_at0) {
+            val1 = 0;
+            r = next_viable(val1);
+        }
         if (r != l_true)
             return r;
 
-        if (val1 == max_value) {
+        if (val1 == c.var2pdd(v).max_value()) {
-            val2 = val1;
+            if (start_at0) {
-            return l_true;
+                val2 = val1;
+                return l_true;
+            }
+            else
+                val2 = 0;
         }
-        val2 = val1 + 1;
+        else 
+            val2 = val1 + 1;
         
         r = next_viable(val2);
 

src/sat/smt/polysat_internalize.cpp

@@ -178,13 +178,15 @@ namespace polysat {
         }
     };
 
-    void solver::mk_atom(sat::bool_var bv, signed_constraint& sc) {
+    solver::atom* solver::mk_atom(sat::bool_var bv, signed_constraint& sc) {
-        if (get_bv2a(bv))
+        auto a = get_bv2a(bv);
-            return;
+        if (a)
+            return a;            
         auto index = m_core.register_constraint(sc, dependency(bv));
-        auto a = new (get_region()) atom(bv, index);
+        a = new (get_region()) atom(bv, index);
         insert_bv2a(bv, a);
         ctx.push(mk_atom_trail(bv, *this));
+        return a;
     }
 
     void solver::internalize_binary_predicate(app* e, std::function<polysat::signed_constraint(pdd, pdd)> const& fn) {
@@ -759,6 +761,7 @@ namespace polysat {
     public:
         undo_add_eq(solver& s, unsigned i) : s(s), index(i) {}
         void undo() override {
+            SASSERT(index == s.m_eqs.back().index());
             s.m_eq2constraint.remove(index);
             s.m_eqs.pop_back();
         }
@@ -769,10 +772,8 @@ namespace polysat {
         constraint_id idx;
         if (m_eq2constraint.find(r.index(), idx))
             return idx;
-        auto sc = m_core.eq(p, q);
+        auto sc = m_core.eq(p, q);       
-        TRACE("bv", tout << "new eq " << sc << "\n");
         idx = m_core.register_constraint(sc, d);
-
         m_eq2constraint.insert(r.index(), idx);
         m_eqs.push_back(r);
         ctx.push(undo_add_eq(*this, r.index()));

src/sat/smt/polysat_solver.cpp

@@ -114,7 +114,7 @@ namespace polysat {
         if (!a)
             return;
         force_push();
-        m_core.assign_eh(a->m_index, l.sign(), s().lvl(l));
+        m_core.assign_eh(a->m_index, l.sign());
     }
 
     void solver::set_conflict(dependency_vector const& deps, char const* hint_info) {
@@ -193,10 +193,15 @@ namespace polysat {
         pdd p = m_core.var(pvar);
         pdd q = m_core.value(val, m_core.size(pvar));
         auto sc = m_core.eq(p, q);
-        mk_atom(eq.var(), sc);
         s().set_phase(eq);
         ctx.mark_relevant(eq);
         d = dependency(eq.var());
+        auto value = s().value(eq);
+        if (!get_bv2a(eq.var())) {
+            auto a = mk_atom(eq.var(), sc);
+            if (value == l_false)
+                m_core.assign_eh(a->m_index, true);
+        }
         return s().value(eq);
     }
 
@@ -213,7 +218,7 @@ namespace polysat {
         pdd q = var2pdd(v2);
         auto d = dependency(v1, v2);
         constraint_id id = eq_constraint(p, q, d);
-        m_core.assign_eh(id, false, s().scope_lvl()); 
+        m_core.assign_eh(id, false); 
 
     }
 
@@ -228,7 +233,7 @@ namespace polysat {
         auto d = dependency(eq.var());
         auto id = eq_constraint(p, q, d);
         TRACE("bv", tout << eq << " := " << s().value(eq) << " @" << s().scope_lvl() << "\n");
-        m_core.assign_eh(id, true, s().lvl(eq));
+        m_core.assign_eh(id, true);
     }
 
     // Core uses the propagate callback to add unit propagations to the trail.

src/sat/smt/polysat_solver.h

@@ -103,7 +103,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;
-        void  mk_atom(sat::bool_var bv, signed_constraint& sc);
+        atom* 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);