Polysat: minor fixes (#5364)

* update include paths

* bdd fixes

* update/fix some tests

* work around assertion failure when constraint from clause becomes unit

* Remove old code

* use clause_builder

* Verify model when returning SAT

* log

* fix

src/math/dd/dd_bdd.cpp

@@ -1037,7 +1037,8 @@ namespace dd {
             std::function<bdd(unsigned)> get_a = [&](unsigned k) {
                 if (k < i)
                     return mk_false();
-                return a[i - k] && b[i];
+                else
+                    return a[k - i] && b[i];
             };
             result = mk_add(result, get_a);
         }
@@ -1056,11 +1057,10 @@ namespace dd {
         SASSERT(a.size() == b.size());
         bddv result = mk_zero(a.size());
 
-       
         // use identity (bvmul a b) == (bvneg (bvmul (bvneg a) b))
         unsigned cnt = 0;
         for (auto v : b) if (v) cnt++; 
-        if (cnt*2 > b.size()) 
+        if (cnt*2 > b.size()+1)
             return mk_usub(mk_mul(a, mk_usub(b)));
 
         for (unsigned i = 0; i < a.size(); ++i) {

src/math/dd/dd_pdd.h

@@ -452,6 +452,7 @@ namespace dd {
     inline pdd operator-(rational const& r, pdd const& b) { return b.rev_sub(r); }
     inline pdd operator-(int x, pdd const& b) { return rational(x) - b; }
     inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); }
+    inline pdd operator-(pdd const& b, rational const& r) { return b + (-r); }
 
     inline pdd& operator&=(pdd & p, pdd const& q) { p = p & q; return p; }
     inline pdd& operator^=(pdd & p, pdd const& q) { p = p ^ q; return p; }

src/math/polysat/constraint.cpp

@@ -66,7 +66,10 @@ namespace polysat {
         for (unsigned l = m_constraints.size(); l-- > lvl; ) {
             for (auto const& c : m_constraints[l]) {
                 LOG_V("Removing constraint: " << show_deref(c));
-                SASSERT_EQ(c->m_ref_count, 1);  // otherwise there is a leftover reference somewhere
+                if (c->m_ref_count > 2) {
+                    // NOTE: ref count could be two if the constraint was added twice (once as part of clause, and later as unit constraint)
+                    LOG_H1("Expected ref_count 1 or 2, got " << c->m_ref_count << " for " << *c);
+                }
                 if (c->dep() && c->dep()->is_leaf()) {
                     unsigned dep = c->dep()->leaf_value();
                     SASSERT(m_external_constraints.contains(dep));

src/math/polysat/eq_constraint.cpp

@@ -191,9 +191,9 @@ namespace polysat {
 
         // Concrete values of evaluable terms
         auto e1s = e1.subst_val(s.assignment());
-        auto e2s = m.zero();
+        if (!e1s.is_val())
+            return false;
         SASSERT(e1s.is_val());
-        SASSERT(e2s.is_val());
 
         // e1 + t <= 0, with t = 2^j1*y
         // condition for empty/full: 0 == -1, never satisfied, so we always have a proper interval!

src/math/polysat/search_state.cpp

@@ -27,6 +27,10 @@ namespace polysat {
         return out;
     }
 
+    std::ostream& search_state::display(std::ostream& out) const {
+        return out << m_items;
+    }
+
     void search_state::push_assignment(pvar p, rational const& r) {
         m_items.push_back(search_item::assignment(p));
         m_assignment.push_back({p, r});

src/math/polysat/solver.cpp

@@ -71,7 +71,7 @@ namespace polysat {
             else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
             else if (is_conflict()) resolve_conflict();
             else if (can_propagate()) propagate();
-            else if (!can_decide()) { LOG_H2("SAT"); return l_true; }
+            else if (!can_decide()) { LOG_H2("SAT"); SASSERT(verify_sat()); return l_true; }
             else decide();
         }
         LOG_H2("UNDEF (resource limit)");
@@ -442,7 +442,8 @@ namespace polysat {
     void solver::resolve_conflict() {
         IF_VERBOSE(1, verbose_stream() << "resolve conflict\n");
         LOG_H2("Resolve conflict");
-        LOG_H2(*this);
+        LOG(*this);
+        LOG("search state: " << m_search);
         ++m_stats.m_num_conflicts;
 
         SASSERT(is_conflict());
@@ -485,11 +486,9 @@ namespace polysat {
                 set_marks(*lemma.get());
             }
             else {
-                // lemma = resolve(conflict_var);
                 conflict_explainer cx(*this, m_conflict);
                 lemma = cx.resolve(conflict_var, {});
                 LOG("resolved: " << show_deref(lemma));
-                // std::abort();
             }
         }
 
@@ -512,7 +511,9 @@ namespace polysat {
                     return;
                 }
                 SASSERT(j.is_propagation());
+                LOG("Lemma: " << show_deref(lemma));
                 clause_ref new_lemma = resolve(v);
+                LOG("New Lemma: " << show_deref(new_lemma));
                 if (!new_lemma) {
                     backtrack(i, lemma);
                     return;
@@ -554,6 +555,7 @@ namespace polysat {
                     return;
                 }
                 SASSERT(m_bvars.is_propagation(var));
+                LOG("Lemma: " << show_deref(lemma));
                 clause_ref new_lemma = resolve_bool(lit);
                 if (!new_lemma) {
                     backtrack(i, lemma);
@@ -695,9 +697,16 @@ namespace polysat {
         LOG("Learning: " << show_deref(lemma));
         SASSERT(m_conflict_level <= m_justification[v].level());
         if (lemma->size() == 1) {
-            constraint_ref c = lemma->new_constraints()[0];  // TODO: probably wrong
+            constraint_ref c;
+            if (lemma->new_constraints().size() > 0) {
+                SASSERT_EQ(lemma->new_constraints().size(), 1);
+                c = lemma->new_constraints()[0];
+            }
+            else {
+                c = m_constraints.lookup(lemma->literals()[0].var());
+            }
             SASSERT_EQ(lemma->literals()[0].var(), c->bvar());
-            SASSERT(!lemma->literals()[0].sign()); // that case is handled incorrectly atm
+            SASSERT(!lemma->literals()[0].sign()); // TODO: that case is handled incorrectly atm
             learn_lemma_unit(v, std::move(c));
         }
         else
@@ -715,6 +724,7 @@ namespace polysat {
     void solver::learn_lemma_clause(pvar v, clause_ref lemma) {
         SASSERT(lemma);
         sat::literal lit = decide_bool(*lemma);
+        SASSERT(lit != sat::null_literal);
         constraint* c = m_constraints.lookup(lit.var());
         push_cjust(v, c);
         add_lemma_clause(std::move(lemma));
@@ -725,6 +735,7 @@ namespace polysat {
         LOG_H3("Guessing literal in lemma: " << lemma);
         IF_LOGGING(m_viable.log());
         LOG("Boolean assignment: " << m_bvars);
+        SASSERT(lemma.size() >= 2);
 
         // To make a guess, we need to find an unassigned literal that is not false in the current model.
         auto is_suitable = [this](sat::literal lit) -> bool {
@@ -741,15 +752,6 @@ namespace polysat {
         unsigned num_choices = 0;  // TODO: should probably cache this?
 
         for (sat::literal lit : lemma) {
-            // IF_LOGGING({
-            //     auto value = m_bvars.value(lit);
-            //     auto c = m_constraints.lookup(lit.var());
-            //     bool is_false;
-            //     LOG_V("Checking: lit=" << lit << ", value=" << value << ", constraint=" << show_deref(c));
-            //     tmp_assign _t(c, lit);
-            //     is_false = c->is_currently_false(*this);
-            //     LOG_V("Checking: lit=" << lit << ", value=" << value << ", constraint=" << show_deref(c) << ", currently_false=" << is_false);
-            // });
             if (is_suitable(lit)) {
                 num_choices++;
                 if (choice == sat::null_literal)
@@ -767,33 +769,6 @@ namespace polysat {
         else
             decide_bool(choice, lemma);
         return choice;
-
-        // constraint* c = nullptr;
-        // while (true) {
-        //     unsigned next_idx = lemma.next_guess();
-        //     SASSERT(next_idx < lemma.size());  // must succeed for at least one
-        //     sat::literal lit = lemma[next_idx];
-        //     // LOG_V("trying: "
-        //     if (m_bvars.value(lit) == l_false)
-        //         continue;
-        //     SASSERT(m_bvars.value(lit) != l_true);  // cannot happen in a valid lemma
-        //     c = m_constraints.lookup(lit.var());
-        //     c->assign(!lit.sign());
-        //     if (c->is_currently_false(*this))
-        //         continue;
-        //     // Choose c as next literal
-        //     break;
-        // }
-        // sat::literal const new_lit{c->bvar()};
-        // TODO: this will not be needed once we add boolean watchlists; alternatively replace with an incremental counter on the clause
-        // unsigned const unassigned_count =
-        //     std::count_if(lemma.begin(), lemma.end(),
-        //     [this](sat::literal lit) { return !m_bvars.is_assigned(lit); });
-        // if (unassigned_count == 1)
-        //     propagate_bool(new_lit, &lemma);
-        // else
-        //     decide_bool(new_lit, lemma);
-        // return c;
     }
 
     /**
@@ -886,12 +861,11 @@ namespace polysat {
             // TODO: what to do when reason is NULL?
             // * this means we were unable to build a lemma for the current conflict.
             // * the reason for reverting this decision then needs to be the (negation of the) conflicting literals. Or we give up on resolving this lemma?
-            // TODO: do not include 'base' unit constraints (only in dependencies)
             SASSERT(m_conflict.clauses().empty());  // not sure how to handle otherwise
+            clause_builder clause(*this);
             unsigned reason_lvl = m_constraints.lookup(lit.var())->level();
             p_dependency_ref reason_dep(m_constraints.lookup(lit.var())->dep(), m_dm);
-            sat::literal_vector reason_lits;
+            clause.push_literal(~lit);  // propagated literal
-            reason_lits.push_back(~lit);  // propagated literal
             for (auto c : m_conflict.units()) {
                 if (c->bvar() == var)
                     continue;
@@ -899,9 +873,9 @@ namespace polysat {
                     continue;
                 reason_lvl = std::max(reason_lvl, c->level());
                 reason_dep = m_dm.mk_join(reason_dep, c->dep());
-                reason_lits.push_back(c->blit());
+                clause.push_literal(c->blit());
             }
-            reason = clause::from_literals(reason_lvl, reason_dep, reason_lits, {});
+            reason = clause.build(reason_lvl, reason_dep);
             LOG("Made-up reason: " << show_deref(reason));
         }
 
@@ -969,11 +943,7 @@ namespace polysat {
         assign_bool_core(sat::literal(c->bvar()), nullptr, nullptr);
         activate_constraint(*c, true);
         // c must be in m_original or m_redundant so it can be deactivated properly when popping the base level
-        SASSERT(
+        SASSERT_EQ(std::count(m_original.begin(), m_original.end(), c) + std::count(m_redundant.begin(), m_redundant.end(), c), 1);
-            std::count(m_original.begin(), m_original.end(), c) + std::count(m_redundant.begin(), m_redundant.end(), c) == 1
-            // std::any_of(m_original.begin(), m_original.end(), [c](constraint* d) { return c == d; })
-            // || std::any_of(m_redundant.begin(), m_redundant.end(), [c](constraint* d) { return c == d; })
-        );
     }
 
     /// Assign a boolean literal and activate the corresponding constraint
@@ -1021,21 +991,7 @@ namespace polysat {
         conflict_explainer cx(*this, m_conflict);
         clause_ref res = cx.resolve(v, m_cjust[v]);
         LOG("resolved: " << show_deref(res));
-        // std::abort();
         return res;
-/*
-            if (m_cjust[v].size() != 1)
-            return nullptr;
-        constraint* d = m_cjust[v].back();
-        constraint_ref res = d->resolve(*this, v);
-        LOG("resolved: " << show_deref(res));
-        if (res) {
-            res->assign(true);
-            return clause::from_unit(res);
-        }
-        else
-            return nullptr;
-*/
     }
 
     /**
@@ -1059,11 +1015,11 @@ namespace polysat {
         if (!lemma)
             return;
         LOG("Lemma: " << show_deref(lemma));
-        // SASSERT(lemma->size() > 1);
         if (lemma->size() < 2) {
             LOG_H1("TODO: this should be treated as unit constraint and asserted at the base level!");
         }
-        clause* cl = m_constraints.insert(lemma);
+        SASSERT(lemma->size() > 1);
+        clause* cl = m_constraints.insert(std::move(lemma));
         m_redundant_clauses.push_back(cl);
     }
 
@@ -1211,6 +1167,18 @@ namespace polysat {
         return true;
     }
 
+    /// Check that all original constraints are satisfied by the current model.
+    bool solver::verify_sat() {
+        LOG_H1("Checking current model...");
+        LOG("Assignment: " << assignments_pp(*this));
+        for (auto* c : m_original) {
+            bool ok = c->is_currently_true(*this);
+            LOG((ok ? "PASS" : "FAIL") << ": " << show_deref(c));
+            if (!ok) return false;
+        }
+        LOG("All good!");
+        return true;
+    }
 }
 
 

src/math/polysat/solver.h

@@ -243,6 +243,7 @@ namespace polysat {
         bool invariant();
         static bool invariant(ptr_vector<constraint> const& cs);
         bool wlist_invariant();
+        bool verify_sat();
 
     public:
 

src/test/bdd.cpp

@@ -119,6 +119,8 @@ public:
                 eq = m.mk_eq(nv, kr);
                 SASSERT(eq.is_const() && (eq.is_true() == (n == k)));
 
+                SASSERT(m.mk_usub(nv).to_val() == (m.mk_zero(num_bits) - nv).to_val());
+
                 bdd cmp = nv <= kv;
                 SASSERT(cmp.is_const() && (cmp.is_true() == (nr <= kr)));
                 cmp = nv >= kv;

src/test/ddnf.cpp

@@ -4,7 +4,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #include "muz/ddnf/ddnf.h"
-#include "muz/rel/tbv.h"
+#include "util/tbv.h"
 #include <iostream>
 #include <fstream>
 #include <list>

src/test/polysat.cpp

@@ -517,13 +517,12 @@ namespace polysat {
      * 
      * We do overflow checks by doubling the base bitwidth here.
      */
-    static void test_fixed_point_arith_div_mul_inverse() {
+    static void test_fixed_point_arith_div_mul_inverse(unsigned base_bw = 5) {
         scoped_solver s(__func__);
 
-        auto baseBw = 5;
+        auto max_int_const = rational::power_of_two(base_bw) - 1;
-        auto max_int_const = 31; // (2^5 - 1) -- change this when you change baseBw
 
-        auto bw = 2 * baseBw;
+        auto bw = 2 * base_bw;
         auto max_int = s.var(s.add_var(bw));
         s.add_eq(max_int - max_int_const);
 
@@ -538,7 +537,7 @@ namespace polysat {
 
         // scaling factor (setting it, somewhat arbitrarily, to max_int/3)
         auto sf = s.var(s.add_var(bw));
-        s.add_eq(sf - (max_int_const/3));
+        s.add_eq(sf - floor(max_int_const/3));
 
         // (a * sf) / b = quot1 <=> quot1 * b + rem1 - (a * sf) = 0
         auto quot1 = s.var(s.add_var(bw));
@@ -642,30 +641,29 @@ namespace polysat {
      *
      * We do overflow checks by doubling the base bitwidth here.
      */
-    static void test_monot_bounds_full() {
+    static void test_monot_bounds_full(unsigned base_bw = 5) {
         scoped_solver s(__func__);
 
-        auto baseBw = 5;
+        auto const max_int_const = rational::power_of_two(base_bw) - 1;
-        auto max_int_const = 31; // (2^5 - 1) -- change this when you change baseBw
 
-        auto bw = 2 * baseBw;
+        auto const bw = 2 * base_bw;
-        auto max_int = s.var(s.add_var(bw));
+        auto const max_int = s.var(s.add_var(bw));
         s.add_eq(max_int - max_int_const);
 
-        auto zero = max_int - max_int;
+        auto const zero = max_int - max_int;
 
-        auto first = s.var(s.add_var(bw));
+        auto const first = s.var(s.add_var(bw));
         s.add_ule(first, max_int);
-        auto second = s.var(s.add_var(bw));
+        auto const second = s.var(s.add_var(bw));
         s.add_ule(second, max_int);
-        auto idx = s.var(s.add_var(bw));
+        auto const idx = s.var(s.add_var(bw));
         s.add_ule(idx, max_int);
-        auto r = s.var(s.add_var(bw));
+        auto const q = s.var(s.add_var(bw));
+        s.add_ule(q, max_int);
+        auto const r = s.var(s.add_var(bw));
         s.add_ule(r, max_int);
 
         // q = max_int / idx <=> q * idx + r - max_int = 0
-        auto q = s.var(s.add_var(bw));
-        r = s.var(s.add_var(bw));
         s.add_eq((q * idx) + r - max_int);
         s.add_ult(r, idx);
         s.add_ule(q * idx, max_int);
@@ -683,8 +681,9 @@ namespace polysat {
 
         // (bvugt second first)
         s.add_ult(first, second);
-        // (bvumul_noovfl (bvsub second first) idx)
+        // (not (bvumul_noovfl (bvsub second first) idx))
-        s.add_ule((second - first) * idx, max_int);
+        s.add_ult(max_int, (second - first) * idx);
+        // s.add_ule((second - first) * idx, max_int);
 
         // resolving disjunction via push/pop
 

src/test/tbv.cpp

@@ -4,7 +4,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#include "muz/rel/tbv.h"
+#include "util/tbv.h"
 
 static void tst1(unsigned num_bits) {
     tbv_manager m(num_bits);