From 737913b67e145a340c60093ca3669257f9811834 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Dec 2023 14:00:28 -0800 Subject: [PATCH] bugfixes Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_bv_plugin.cpp | 3 ++- src/ast/euf/euf_egraph.cpp | 2 -- src/sat/smt/polysat/constraints.cpp | 2 +- src/sat/smt/polysat/core.cpp | 30 ++++++++++++++++++-------- src/sat/smt/polysat/core.h | 4 ++-- src/sat/smt/polysat/ule_constraint.cpp | 13 +++++------ src/sat/smt/polysat/viable.cpp | 3 ++- src/sat/smt/polysat_internalize.cpp | 10 ++++----- src/sat/smt/polysat_solver.cpp | 15 +++++++++++-- src/sat/smt/polysat_solver.h | 2 +- 10 files changed, 54 insertions(+), 30 deletions(-) diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index bb595b386..87bd4c434 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -531,7 +531,8 @@ namespace euf { out << "bv\n"; for (auto const& i : m_info) if (i.lo) - out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n"; + out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n"; + return out; } } diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 6f6b6a7e8..779bedc55 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -110,7 +110,6 @@ namespace euf { for (enode* child : enode_args(n)) SASSERT(child->get_root()->m_parents.back() == n); m_updates.push_back(update_record(n, update_record::update_children())); - TRACE("euf", tout << "update children " << bpp(n) << "\n"; display(tout)); } enode* egraph::mk(expr* f, unsigned generation, unsigned num_args, enode *const* args) { @@ -444,7 +443,6 @@ namespace euf { p.r1->set_relevant(false); break; case update_record::tag_t::is_update_children: - TRACE("euf", tout << "reverse update children " << bpp(p.r1) << "\n"; display(tout)); for (unsigned i = 0; i < p.r1->num_args(); ++i) { CTRACE("euf", (p.r1->m_args[i]->get_root()->m_parents.back() != p.r1), display(tout << bpp(p.r1->m_args[i]) << " " << bpp(p.r1->m_args[i]->get_root()) << " ");); diff --git a/src/sat/smt/polysat/constraints.cpp b/src/sat/smt/polysat/constraints.cpp index c96b43d6a..e7a204295 100644 --- a/src/sat/smt/polysat/constraints.cpp +++ b/src/sat/smt/polysat/constraints.cpp @@ -25,7 +25,7 @@ namespace polysat { pdd lhs = p, rhs = q; bool is_positive = true; ule_constraint::simplify(is_positive, lhs, rhs); - auto* cnstr = alloc(ule_constraint, p, q); + auto* cnstr = alloc(ule_constraint, lhs, rhs); c.trail().push(new_obj_trail(cnstr)); auto sc = signed_constraint(ckind_t::ule_t, cnstr); return is_positive ? sc : ~sc; diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 04f0ae857..f0024fdd9 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -39,7 +39,7 @@ namespace polysat { public: mk_assign_var(pvar v, core& c) : m_var(v), c(c) {} void undo() { - c.m_justification[m_var] = constraint_id::null(); + c.m_justification[m_var] = null_dependency; c.m_assignment.pop(); } }; @@ -124,7 +124,7 @@ namespace polysat { unsigned v = m_vars.size(); m_vars.push_back(sz2pdd(sz).mk_var(v)); m_activity.push_back({ sz, 0 }); - m_justification.push_back(constraint_id::null()); + m_justification.push_back(null_dependency); m_watch.push_back({}); m_var_queue.mk_var_eh(v); m_viable.ensure_var(v); @@ -173,18 +173,25 @@ namespace polysat { return final_check(); m_var = m_var_queue.next_var(); s.trail().push(mk_dqueue_var(m_var, *this)); + switch (m_viable.find_viable(m_var, m_value)) { case find_t::empty: + TRACE("bv", tout << "check-conflict v" << m_var << "\n"); s.set_conflict(m_viable.explain()); // propagate_unsat_core(); return sat::check_result::CR_CONTINUE; - case find_t::singleton: - s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain()); + case find_t::singleton: { + TRACE("bv", tout << "check-propagate v" << m_var << " := " << m_value << "\n"); + auto d = s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain()); + propagate_assignment(m_var, m_value, d); return sat::check_result::CR_CONTINUE; + } case find_t::multiple: + TRACE("bv", tout << "check-multiple v" << m_var << " := " << m_value << "\n"); s.add_eq_literal(m_var, m_value); return sat::check_result::CR_CONTINUE; case find_t::resource_out: + TRACE("bv", tout << "check-resource out v" << m_var << "\n"); m_var_queue.unassign_var_eh(m_var); return sat::check_result::CR_GIVEUP; } @@ -199,6 +206,8 @@ namespace polysat { auto [sc, d, value] = m_constraint_index[idx.id]; SASSERT(value != l_undef); lbool eval_value = eval(sc); + sc.display(verbose_stream()) << " eval: " << eval_value << "\n"; + CTRACE("bv", eval_value == l_undef, sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n"); SASSERT(eval_value != l_undef); if (eval_value == value) continue; @@ -233,7 +242,7 @@ namespace polysat { for (auto v : sc.vars()) { if (!is_assigned(v)) continue; - auto new_level = s.level(get_dependency(m_justification[v])); + auto new_level = s.level(m_justification[v]); if (new_level < lvl) continue; if (new_level > lvl) @@ -260,8 +269,9 @@ namespace polysat { SASSERT(value != l_undef); if (value == l_false) sc = ~sc; + TRACE("bv", tout << "propagate " << sc << " using " << dep << " := " << value << "\n"); if (sc.is_eq(m_var, m_value)) - propagate_assignment(m_var, m_value, idx); + propagate_assignment(m_var, m_value, dep); else sc.activate(*this, dep); } @@ -270,13 +280,15 @@ namespace polysat { m_watch[var].push_back(idx); } - void core::propagate_assignment(pvar v, rational const& value, constraint_id dep) { + void core::propagate_assignment(pvar v, rational const& value, dependency dep) { + TRACE("bv", tout << "propagate assignment v" << v << " := " << value << " " << is_assigned(v) << "\n"); if (is_assigned(v)) return; if (m_var_queue.contains(v)) { m_var_queue.del_var_eh(v); s.trail().push(mk_dqueue_var(v, *this)); } + m_values[v] = value; m_justification[v] = dep; m_assignment.push(v , value); @@ -417,7 +429,7 @@ namespace polysat { dependency_vector deps; for (auto v : sc.vars()) if (is_assigned(v)) - deps.push_back(get_dependency(m_justification[v])); + deps.push_back(m_justification[v]); return deps; } @@ -448,7 +460,7 @@ namespace polysat { for (auto const& [sc, d, value] : m_constraint_index) out << sc << " " << d << " := " << value << "\n"; for (unsigned i = 0; i < m_vars.size(); ++i) { - out << m_vars[i] << " := " << m_values[i] << " " << get_dependency(m_justification[i]) << "\n"; + out << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n"; } m_var_queue.display(out << "vars ") << "\n"; return out; diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index 7c8466b92..8a6a0bced 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -63,7 +63,7 @@ namespace polysat { // attributes associated with variables vector m_vars; // for each variable a pdd vector m_values; // current value of assigned variable - constraint_id_vector m_justification; // justification for assignment + dependency_vector m_justification; // justification for assignment activity m_activity; // activity of variables var_queue m_var_queue; // priority queue of variables to assign vector m_watch; // watch lists for variables for constraints on m_prop_queue where they occur @@ -80,7 +80,7 @@ namespace polysat { bool is_assigned(pvar v) { return !m_justification[v].is_null(); } void propagate_assignment(constraint_id idx); void propagate_eval(constraint_id idx); - void propagate_assignment(pvar v, rational const& value, constraint_id dep); + void propagate_assignment(pvar v, rational const& value, dependency dep); void propagate_unsat_core(); void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d); diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp index 1c21fdf25..c39120ec3 100644 --- a/src/sat/smt/polysat/ule_constraint.cpp +++ b/src/sat/smt/polysat/ule_constraint.cpp @@ -86,6 +86,8 @@ namespace polysat { SASSERT_EQ(lhs.power_of_2(), rhs.power_of_2()); unsigned const N = lhs.power_of_2(); + // verbose_stream() << "simplify " << lhs << " <= " << rhs << "\n"; + // 0 <= p --> 0 <= 0 if (lhs.is_zero()) { rhs = 0; @@ -139,13 +141,11 @@ namespace polysat { } } - // -p + k <= k --> p <= k if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs.val()) { LOG("-p + k <= k --> p <= k"); lhs = rhs - lhs; } - // k <= p + k --> p <= -k-1 if (lhs.is_val() && !lhs.is_zero() && lhs.val() == rhs.offset()) { LOG("k <= p + k --> p <= -k-1"); pdd k = lhs; @@ -153,7 +153,6 @@ namespace polysat { rhs = -k - 1; } - // k <= -p --> p-1 <= -k-1 if (lhs.is_val() && rhs.leading_coefficient().get_bit(N - 1) && !rhs.offset().is_zero()) { LOG("k <= -p --> p-1 <= -k-1"); pdd k = lhs; @@ -161,8 +160,6 @@ namespace polysat { rhs = -k - 1; } - // -p <= k --> -k-1 <= p-1 - // if (rhs.is_val() && lhs.leading_coefficient() > rational::power_of_two(N - 1) && !lhs.offset().is_zero()) { if (rhs.is_val() && lhs.leading_coefficient().get_bit(N - 1) && !lhs.offset().is_zero()) { LOG("-p <= k --> -k-1 <= p-1"); pdd k = rhs; @@ -170,6 +167,10 @@ namespace polysat { lhs = -k - 1; } + if (rhs.is_zero() && lhs.leading_coefficient().get_bit(N - 1) && !lhs.offset().is_zero()) { + LOG("-p <= 0 --> p <= 0"); + lhs = -lhs; + } // NOTE: do not use pdd operations in conditions when comparing pdd values. // e.g.: "lhs.offset() == (rhs + 1).val()" is problematic with the following evaluation: // 1. return reference into pdd_manager::m_values from lhs.offset() @@ -177,7 +178,6 @@ namespace polysat { // 3. now the reference returned from lhs.offset() may be invalid pdd const rhs_plus_one = rhs + 1; - // p - k <= -k - 1 --> k <= p // TODO: potential bug here: first call offset(), then rhs+1 has to reallocate pdd_manager::m_values, then the reference to offset is broken. if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs_plus_one.val()) { LOG("p - k <= -k - 1 --> k <= p"); @@ -231,6 +231,7 @@ namespace polysat { lhs *= x; SASSERT(lhs.leading_coefficient().is_power_of_two()); } + // verbose_stream() << "simplified " << lhs << " <= " << rhs << "\n"; } // simplify_impl } diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 1578dc443..a7b5111f6 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -84,7 +84,6 @@ namespace polysat { } find_t viable::find_viable(pvar v, rational& lo) { - display(verbose_stream() << "find viable for v" << v << "\n"); rational hi; switch (find_viable(v, lo, hi)) { case l_true: @@ -193,6 +192,8 @@ namespace polysat { * - set k := l + v.width - w.width, lo' := 2^{v.width-w.width} lo, hi' := 2^{v.width-w.width} hi. */ lbool viable::next_viable_layer(pvar w, layer& layer, rational& val) { + if (!layer.entries) + return l_true; unsigned v_width = m_num_bits; unsigned w_width = c.size(w); unsigned l = w_width - layer.bit_width; diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 942538334..1147f5fc5 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -106,9 +106,9 @@ namespace polysat { case OP_UGT: internalize_le(a); break; case OP_SGT: internalize_le(a); break; - case OP_BUMUL_NO_OVFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.umul_ovfl(p, q); }); break; - case OP_BSMUL_NO_OVFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.smul_ovfl(p, q); }); break; - case OP_BSMUL_NO_UDFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.smul_udfl(p, q); }); break; + case OP_BUMUL_NO_OVFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.umul_ovfl(p, q); }); break; + case OP_BSMUL_NO_OVFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.smul_ovfl(p, q); }); break; + case OP_BSMUL_NO_UDFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.smul_udfl(p, q); }); break; case OP_BUMUL_OVFL: case OP_BSMUL_OVFL: @@ -187,10 +187,10 @@ namespace polysat { ctx.push(mk_atom_trail(bv, *this)); } - void solver::internalize_binaryc(app* e, std::function const& fn) { + void solver::internalize_binary_predicate(app* e, std::function const& fn) { auto p = expr2pdd(e->get_arg(0)); auto q = expr2pdd(e->get_arg(1)); - auto sc = ~fn(p, q); + auto sc = fn(p, q); sat::literal lit = expr2literal(e); if (lit.sign()) sc = ~sc; diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 599fadd87..17589fc61 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -167,6 +167,7 @@ namespace polysat { auto n = var2enode(v); auto eq = eq_internalize(n->get_expr(), bv.mk_numeral(val, get_bv_size(v))); s().set_phase(eq); + ctx.mark_relevant(eq); } void solver::new_eq_eh(euf::th_eq const& eq) { @@ -205,6 +206,7 @@ namespace polysat { // Everything goes over expressions/literals. polysat::core is not responsible for replaying expressions. dependency solver::propagate(signed_constraint sc, dependency_vector const& deps) { + TRACE("bv", sc.display(tout << "propagate ") << "\n"); sat::literal lit = ctx.mk_literal(constraint2expr(sc)); if (s().value(lit) == l_true) return dependency(lit.var()); @@ -257,7 +259,9 @@ namespace polysat { } void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps) { + TRACE("bv", tout << "propagate " << d << " " << sign << "\n"); auto [core, eqs] = explain_deps(deps); + SASSERT(d.is_bool_var() || d.is_eq()); if (d.is_bool_var()) { auto bv = d.bool_var(); auto lit = sat::literal(bv, sign); @@ -335,16 +339,23 @@ namespace polysat { } expr_ref solver::constraint2expr(signed_constraint const& sc) { + expr_ref result(m); switch (sc.op()) { case ckind_t::ule_t: { auto l = pdd2expr(sc.to_ule().lhs()); auto h = pdd2expr(sc.to_ule().rhs()); - return expr_ref(bv.mk_ule(l, h), m); + result = bv.mk_ule(l, h); + if (sc.sign()) + result = m.mk_not(result); + return result; } case ckind_t::umul_ovfl_t: { auto l = pdd2expr(sc.to_umul_ovfl().p()); auto r = pdd2expr(sc.to_umul_ovfl().q()); - return expr_ref(m.mk_not(bv.mk_bvumul_no_ovfl(l, r)), m); + result = bv.mk_bvumul_no_ovfl(l, r); + if (!sc.sign()) + result = m.mk_not(result); + return result; } case ckind_t::smul_fl_t: case ckind_t::op_t: diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index 32bb7a65c..e1e35cc5c 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -105,7 +105,7 @@ namespace polysat { void internalize_unary(app* e, std::function const& fn); void internalize_binary(app* e, std::function const& fn); void internalize_binary(app* e, std::function const& fn); - void internalize_binaryc(app* e, std::function const& fn); + void internalize_binary_predicate(app* e, std::function const& fn); void internalize_par_unary(app* e, std::function const& fn); void internalize_novfl(app* n, std::function& fn); void internalize_interp(app* n, std::function& ibin, std::function& un);