From d91820fe5120ec4b0498dd1fbcdd9c4dace82b76 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jan 2024 16:24:15 -0800 Subject: [PATCH] bug fixes Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.h | 1 + src/sat/smt/polysat/core.cpp | 3 ++ src/sat/smt/polysat/core.h | 2 +- src/sat/smt/polysat/monomials.cpp | 45 ++++++++-------------- src/sat/smt/polysat/monomials.h | 2 +- src/sat/smt/polysat/ule_constraint.cpp | 2 +- src/sat/smt/polysat/ule_constraint.h | 2 +- src/sat/smt/polysat/umul_ovfl_constraint.h | 2 +- src/sat/smt/polysat/viable.cpp | 5 +-- src/sat/smt/polysat_internalize.cpp | 16 +++++++- src/sat/smt/polysat_solver.cpp | 8 +++- src/util/debug.h | 1 + 12 files changed, 48 insertions(+), 41 deletions(-) diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index fa545c06e..f589f4b70 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -432,6 +432,7 @@ namespace dd { bool is_one() const { return m->is_one(root); } bool is_zero() const { return m->is_zero(root); } bool is_linear() const { return m->is_linear(root); } + bool is_linear_or_value() const { return is_linear() || is_val(); } bool is_var() const { return m->is_var(root); } bool is_max() const { return m->is_max(root); } /** Polynomial is of the form a * x + b for some numerals a, b. */ diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index fb49e59c8..c2241b6bf 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -217,6 +217,7 @@ namespace polysat { case l_true: break; case l_false: + TRACE("bv", tout << "refine\n"); return sat::check_result::CR_CONTINUE; case l_undef: r = l_undef; @@ -228,6 +229,7 @@ namespace polysat { case l_true: break; case l_false: + TRACE("bv", tout << "saturate\n"); return sat::check_result::CR_CONTINUE; case l_undef: r = l_undef; @@ -238,6 +240,7 @@ namespace polysat { case l_true: break; case l_false: + TRACE("bv", tout << "blast\n"); return sat::check_result::CR_CONTINUE; case l_undef: r = l_undef; diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index ee26fe639..acebceee5 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -130,7 +130,7 @@ namespace polysat { void band(pdd const& a, pdd const& b, pdd const& r) { add_opdef(m_constraints.band(a, b, r)); } pdd bnot(pdd p) { return -p - 1; } - pdd mul(unsigned n, pdd const* args) { return m_monomials.mk(n, args); } + pvar mul(unsigned n, pdd const* args) { return m_monomials.mk(n, args); } /* diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp index b785a7f5c..0709e22db 100644 --- a/src/sat/smt/polysat/monomials.cpp +++ b/src/sat/smt/polysat/monomials.cpp @@ -26,40 +26,24 @@ namespace polysat { m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq) {} - pdd monomials::mk(unsigned n, pdd const* args) { - SASSERT(n > 0); - if (n == 1) - return args[0]; - if (n == 2 && args[0].is_val()) - return args[0]*args[1]; - if (n == 2 && args[1].is_val()) - return args[0]*args[1]; + pvar monomials::mk(unsigned n, pdd const* args) { + SASSERT(n > 1); auto& m = args[0].manager(); unsigned sz = m.power_of_2(); m_tmp.reset(); - pdd offset = c.value(rational(1), sz); - for (unsigned i = 0; i < n; ++i) { - pdd const& p = args[i]; - if (p.is_val()) - offset *= p; - else - m_tmp.push_back(p); - } - if (m_tmp.empty()) - return offset; - if (m_tmp.size() == 1) - return offset * m_tmp[0]; - - std::stable_sort(m_tmp.begin(), m_tmp.end(), - [&](pdd const& a, pdd const& b) { return a.index() < b.index(); }); + for (unsigned i = 0; i < n; ++i) + m_tmp.push_back(args[i]); + std::stable_sort(m_tmp.begin(), m_tmp.end(), + [&](pdd const& a, pdd const& b) { return a.index() < b.index(); }); + pdd offset = c.value(rational(0), sz); unsigned index = m_monomials.size(); m_monomials.push_back({m_tmp, offset, offset, {}, rational(0) }); unsigned j; if (m_table.find(index, j)) { m_monomials.pop_back(); - return offset * m_monomials[j].var; + return m_monomials[j].var.var(); } struct del_monomial : public trail { @@ -73,7 +57,7 @@ namespace polysat { }; auto & mon = m_monomials.back(); - mon.var = c.add_var(sz); + mon.var = c.var(c.add_var(sz)); mon.def = c.value(rational(1), sz); for (auto p : m_tmp) { mon.arg_vals.push_back(rational(0)); @@ -81,13 +65,15 @@ namespace polysat { } m_table.insert(index); c.trail().push(del_monomial(*this)); - return offset * mon.var; + return mon.var.var(); } pdd monomials::subst(pdd const& p) { pdd r = p; - for (unsigned i = m_monomials.size(); i-- > 0;) - r = r.subst_pdd(m_monomials[i].var.var(), m_monomials[i].def); + for (unsigned i = m_monomials.size(); i-- > 0;) { + if (&r.manager() == &m_monomials[i].var.manager()) + r = r.subst_pdd(m_monomials[i].var.var(), m_monomials[i].def); + } return r; } @@ -201,8 +187,7 @@ namespace polysat { else cs.push_back(C.eq(mon.var, offset * mon.args[free_index])); - c.add_axiom("p = k => p * q = k * q", cs, true); - return true; + return c.add_axiom("p = k => p * q = k * q", cs, true); } // parity p >= i => parity p * q >= i diff --git a/src/sat/smt/polysat/monomials.h b/src/sat/smt/polysat/monomials.h index 04798e3b9..f2599cdda 100644 --- a/src/sat/smt/polysat/monomials.h +++ b/src/sat/smt/polysat/monomials.h @@ -87,7 +87,7 @@ namespace polysat { monomials(core& c); - pdd mk(unsigned n, pdd const* args); + pvar mk(unsigned n, pdd const* args); pdd subst(pdd const& p); diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp index 802cea772..6e4b1e9f5 100644 --- a/src/sat/smt/polysat/ule_constraint.cpp +++ b/src/sat/smt/polysat/ule_constraint.cpp @@ -319,7 +319,7 @@ namespace polysat { std::ostream& ule_constraint::display(std::ostream& out) const { display(out, l_true, m_lhs, m_rhs); if (m_lhs != m_unfold_lhs || m_rhs != m_unfold_rhs) - display(out << " alias ( ", l_true, m_unfold_lhs, m_unfold_rhs) << ")"; + display(out << " alias (", l_true, m_unfold_lhs, m_unfold_rhs) << ")"; return out; } diff --git a/src/sat/smt/polysat/ule_constraint.h b/src/sat/smt/polysat/ule_constraint.h index 8b838bcbf..fbe1cc6df 100644 --- a/src/sat/smt/polysat/ule_constraint.h +++ b/src/sat/smt/polysat/ule_constraint.h @@ -40,7 +40,7 @@ namespace polysat { lbool eval() const override; lbool eval(assignment const& a) const override; lbool eval_unfold(assignment const& a) const override; - bool is_linear() const override { return lhs().is_linear() && rhs().is_linear(); } + bool is_linear() const override { return lhs().is_linear_or_value() && rhs().is_linear_or_value(); } void activate(core& c, bool sign, dependency const& dep); void propagate(core& c, lbool value, dependency const& dep) {} bool is_eq() const { return m_rhs.is_zero(); } diff --git a/src/sat/smt/polysat/umul_ovfl_constraint.h b/src/sat/smt/polysat/umul_ovfl_constraint.h index f87a10f2f..5d7f09bce 100644 --- a/src/sat/smt/polysat/umul_ovfl_constraint.h +++ b/src/sat/smt/polysat/umul_ovfl_constraint.h @@ -38,7 +38,7 @@ namespace polysat { lbool eval(assignment const& a) const override; void activate(core& c, bool sign, dependency const& dep) override; void propagate(core& c, lbool value, dependency const& dep) override; - bool is_linear() const override { return p().is_linear() && q().is_linear(); } + bool is_linear() const override { return p().is_linear_or_value() && q().is_linear_or_value(); } }; diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 4f51529ce..f8d0767d1 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -550,9 +550,8 @@ namespace polysat { if (value == l_false) sc = ~sc; - if (!sc.is_linear()) { - return true; - } + if (!sc.is_linear()) + return true; entry* ne = alloc_entry(v, idx); if (!m_forbidden_intervals.get_interval(sc, v, *ne)) { diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 617d6c161..3720c04f2 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -608,7 +608,21 @@ namespace polysat { vector args; for (expr* arg : *to_app(a)) args.push_back(expr2pdd(arg)); - internalize_set(a, m_core.mul(args.size(), args.data())); + if (args.size() == 1) { + internalize_set(a, args[0]); + return; + } + if (args.size() == 2 && args[0].is_val()) { + internalize_set(a, args[0] * args[1]); + return; + } + if (args.size() == 2 && args[1].is_val()) { + internalize_set(a, args[0] * args[1]); + return; + } + auto pv = m_core.mul(args.size(), args.data()); + m_pddvar2var.setx(pv, get_th_var(a), UINT_MAX); + internalize_set(a, m_core.var(pv)); } // TODO - test that internalize works with recursive call on bit2bool diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index a63d6ea6c..696816c79 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -74,7 +74,8 @@ namespace polysat { case sat::check_result::CR_CONTINUE: return sat::check_result::CR_CONTINUE; case sat::check_result::CR_GIVEUP: - return intblast(); + return sat::check_result::CR_GIVEUP; + // return intblast(); } UNREACHABLE(); return sat::check_result::CR_GIVEUP; @@ -315,6 +316,7 @@ namespace polysat { } bool solver::add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant) { + TRACE("bv", tout << "add " << name << "\n"); sat::literal_vector lits; euf::enode_pair_vector eqs; for (auto it = begin; it != end; ++it) { @@ -335,8 +337,10 @@ namespace polysat { for (auto& lit : lits) lit.neg(); for (auto lit : lits) - if (s().value(lit) == l_true) + if (s().value(lit) == l_true) { + TRACE("bv", tout << "literal is true " << ctx.literal2expr(lit) << "\n"); return false; + } validate_axiom(lits); s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint)); return true; diff --git a/src/util/debug.h b/src/util/debug.h index 5f092b181..42e7f3e70 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -103,6 +103,7 @@ bool is_debug_enabled(const char * tag); if (!((LHS) == (RHS))) { \ notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #LHS " == " #RHS "\n"); \ std::cerr << "LHS value: " << (LHS) << "\nRHS value: " << (RHS) << "\n"; \ + DEBUG_CODE(INVOKE_DEBUGGER();); \ exit(ERR_UNREACHABLE); \ }