From f0b056d8593f5ac71ab5ece6dbf5acc151ad22bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jan 2024 11:29:48 -0800 Subject: [PATCH] add ad-hoc debug output, add rule for incremental linearization Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/core.cpp | 14 +++++++++++--- src/sat/smt/polysat/core.h | 14 +++++++++++++- src/sat/smt/polysat/monomials.cpp | 19 +++++++++++++++++++ src/sat/smt/polysat/monomials.h | 1 + src/sat/smt/polysat/viable.cpp | 29 ++++++++++++++++++++++++++--- src/sat/smt/polysat_solver.cpp | 3 +++ 6 files changed, 73 insertions(+), 7 deletions(-) diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 34614476f..5adf7001e 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -311,8 +311,13 @@ namespace polysat { } void core::viable_conflict(pvar v) { + if (s.inconsistent()) + return; TRACE("bv", tout << "viable-conflict v" << v << "\n"); - s.set_conflict(m_viable.explain(), "viable-conflict"); + auto exp = m_viable.explain(); + if (s.inconsistent()) + verbose_stream() << "inconsistent " << exp << "\n"; + s.set_conflict(exp, "viable-conflict"); decay_activity(); } @@ -371,6 +376,7 @@ namespace polysat { else if (v == null_var && weak_eval(sc) == l_false) { auto ex = explain_weak_eval(sc); ex.push_back(dep); + verbose_stream() << "infeasible propagation " << ~sc << " <- " << ex << "\n"; s.set_conflict(ex, "infeasible propagation"); } } @@ -381,6 +387,7 @@ namespace polysat { if (!m_viable.assign(v, value)) { auto deps = m_viable.explain(); deps.push_back(dep); + verbose_stream() << "non-viable assignment v" << v << " == " << value << " <- " << deps << "\n"; s.set_conflict(deps, "non-viable assignment"); return; } @@ -489,6 +496,7 @@ namespace polysat { else if (value != eval_value) { m_unsat_core = explain_weak_eval(sc); m_unsat_core.push_back(m_constraint_index[id.id].d); + verbose_stream() << "infeasible propagation " << m_unsat_core << "\n"; s.set_conflict(m_unsat_core, "polysat-constraint-core"); decay_activity(); } @@ -645,7 +653,7 @@ namespace polysat { } void core::inc_activity(pvar v) { - unsigned& act = m_activity[v].second; + unsigned& act = m_activity[v].act; act += m_activity_inc; m_var_queue.activity_increased_eh(v); if (act > (1 << 24)) @@ -654,7 +662,7 @@ namespace polysat { void core::rescale_activity() { for (auto& act : m_activity) - act.second >>= 14; + act.act >>= 14; m_activity_inc >>= 14; } diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index 2d2944741..50c98b8b9 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -35,11 +35,23 @@ namespace polysat { class core { + struct var_activity { + unsigned sz; + unsigned act; + bool operator<(var_activity const& other) const { + if (other.sz != sz) + return sz > other.sz; + return act < other.act; + }; + bool operator>(var_activity const& other) const { + return other < *this; + } + }; class mk_add_var; class mk_dqueue_var; class mk_assign_var; class mk_add_watch; - typedef svector> activity; + typedef svector activity; friend class viable; friend class constraints; friend class assignment; diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp index e8e79ec6a..ee0bec436 100644 --- a/src/sat/smt/polysat/monomials.cpp +++ b/src/sat/smt/polysat/monomials.cpp @@ -66,6 +66,8 @@ namespace polysat { return l_false; if (any_of(m_to_refine, [&](auto i) { return mul1(m_monomials[i]); })) return l_false; + if (any_of(m_to_refine, [&](auto i) { return mul1_inverse(m_monomials[i]); })) + return l_false; if (any_of(m_to_refine, [&](auto i) { return non_overflow_unit(m_monomials[i]); })) return l_false; @@ -169,6 +171,23 @@ namespace polysat { return c.add_axiom("p = k => p * q = k * q", cs, true); } + // p * q = p => q = 1 or p = 0 + bool monomials::mul1_inverse(monomial const& mon) { + for (unsigned j = mon.size(); j-- > 0; ) { + auto const& arg_val = mon.arg_vals[j]; + if (arg_val == mon.val) { + auto const& p = mon.args[j]; + pdd qs = c.value(rational(1), mon.num_bits()); + for (unsigned k = mon.size(); k-- > 0; ) + if (k != j) + qs *= mon.arg_vals[k]; + c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), C.eq(qs, 1), C.eq(p) }, true); + return true; + } + } + return false; + } + // parity p >= i => parity p * q >= i bool monomials::parity(monomial const& mon) { unsigned parity_val = get_parity(mon.val, mon.num_bits()); diff --git a/src/sat/smt/polysat/monomials.h b/src/sat/smt/polysat/monomials.h index 25bf4de96..779def053 100644 --- a/src/sat/smt/polysat/monomials.h +++ b/src/sat/smt/polysat/monomials.h @@ -49,6 +49,7 @@ namespace polysat { bool mul0(monomial const& mon); bool mul1(monomial const& mon); bool mulp2(monomial const& mon); + bool mul1_inverse(monomial const& mon); bool mul(monomial const& mon, std::function const& p); bool parity(monomial const& mon); bool non_overflow_monotone(monomial const& mon); diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index c3c663d1d..fd79cc72f 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -555,6 +555,8 @@ namespace polysat { auto last = m_explain.back(); auto after = last; + if (c.inconsistent()) + verbose_stream() << "inconistent explain\n"; TRACE("bv", display_explain(tout)); auto unmark = [&]() { @@ -564,13 +566,20 @@ namespace polysat { auto explain_entry = [&](entry* e) { auto index = e->constraint_index; + if (c.inconsistent()) + return; if (e->marked) return; e->marked = true; if (m_var != e->var) result.push_back(offset_claim(m_var, { e->var, 0 })); - for (auto const& sc : e->side_cond) - result.push_back(c.propagate(sc, c.explain_weak_eval(sc))); + for (auto const& sc : e->side_cond) { + auto d = c.propagate(sc, c.explain_weak_eval(sc)); + if (c.inconsistent()) { + verbose_stream() << "inconsistent " << d << " " << sc << "\n"; + } + result.push_back(d); + } result.append(e->deps); if (!index.is_null()) result.push_back(c.get_dependency(index)); @@ -600,7 +609,11 @@ namespace polysat { explain_entry(first.e); // add constraint that there is only a single viable value. auto sc = cs.eq(last.e->interval.hi() + 1, first.e->interval.lo()); - result.push_back(c.propagate(sc, c.explain_weak_eval(sc))); + auto exp = c.propagate(sc, c.explain_weak_eval(sc)); + if (c.inconsistent()) { + verbose_stream() << "inconsistent " << sc << " " << exp << "\n"; + } + result.push_back(exp); } if (m_explain_kind == explain_t::assignment) { // there is just one entry @@ -608,6 +621,8 @@ namespace polysat { explain_entry(last.e); } unmark(); + if (c.inconsistent()) + verbose_stream() << "inconistent after explain\n"; return result; } @@ -691,6 +706,8 @@ namespace polysat { t.reset(lo.manager()); t = c.value(mod(e.value, rational::power_of_two(aw)), aw); // verbose_stream() << "after " << t << "\n"; + if (c.inconsistent()) + verbose_stream() << "inconsistent overlap " << sc << " " << "\n"; } if (abw < aw) @@ -700,6 +717,12 @@ namespace polysat { SASSERT(!sc.is_always_false()); if (!sc.is_always_true()) deps.push_back(c.propagate(sc, c.explain_weak_eval(sc))); + if (c.inconsistent()) { + verbose_stream() << "inconsistent ult " << sc << " " << "\n"; + verbose_stream() << "before bw " << ebw << " " << bw << " " << *e.e << "\nafter bw " << abw << " " << aw << " " << *after.e << "\n"; + display(verbose_stream()); + // UNREACHABLE(); + } } /* diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 244e90b41..8cfd9dba4 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -260,6 +260,9 @@ namespace polysat { hint = mk_proof_hint(hint_info, core, eqs); core.pop_back(); } + if (s().value(lit) == l_false) { + verbose_stream() << "contradictory propagation " << sc << " <- " << deps << "\n"; + } auto ex = euf::th_explain::propagate(*this, core, eqs, lit, hint); validate_propagate(lit, core, eqs); ctx.propagate(lit, ex);