diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp index 95647e0b1..34816966e 100644 --- a/src/math/dd/dd_bdd.cpp +++ b/src/math/dd/dd_bdd.cpp @@ -1037,7 +1037,8 @@ namespace dd { std::function 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) { diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 553ad004b..a9a45fb46 100644 --- a/src/math/dd/dd_pdd.h +++ b/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; } diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index b772ba26d..7c5f4642e 100644 --- a/src/math/polysat/constraint.cpp +++ b/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)); diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp index 2ebffb5cb..377978670 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/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! diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp index 551d35c52..243fbdb14 100644 --- a/src/math/polysat/search_state.cpp +++ b/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}); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index e32ed2ee6..d4ef01329 100644 --- a/src/math/polysat/solver.cpp +++ b/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; - reason_lits.push_back(~lit); // propagated literal + clause.push_literal(~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( - 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; }) - ); + SASSERT_EQ(std::count(m_original.begin(), m_original.end(), c) + std::count(m_redundant.begin(), m_redundant.end(), c), 1); } /// 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; + } } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index ca8ea652b..e2aa0b1ca 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -243,6 +243,7 @@ namespace polysat { bool invariant(); static bool invariant(ptr_vector const& cs); bool wlist_invariant(); + bool verify_sat(); public: diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index 71553f261..d66acc960 100644 --- a/src/test/bdd.cpp +++ b/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; diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp index b1bb624a2..c62adb4f9 100644 --- a/src/test/ddnf.cpp +++ b/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 #include #include diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 2adc1f00e..17a131946 100644 --- a/src/test/polysat.cpp +++ b/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 = 31; // (2^5 - 1) -- change this when you change baseBw + auto max_int_const = rational::power_of_two(base_bw) - 1; - 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 max_int_const = 31; // (2^5 - 1) -- change this when you change baseBw + auto const max_int_const = rational::power_of_two(base_bw) - 1; - auto bw = 2 * baseBw; - auto max_int = s.var(s.add_var(bw)); + auto const bw = 2 * base_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) - s.add_ule((second - first) * idx, max_int); + // (not (bvumul_noovfl (bvsub second first) idx)) + s.add_ult(max_int, (second - first) * idx); + // s.add_ule((second - first) * idx, max_int); // resolving disjunction via push/pop diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp index c921551bd..b707f91d5 100644 --- a/src/test/tbv.cpp +++ b/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);