mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

Also print original exprs for polysat unsat core

Browse source
This commit is contained in:
Jakob Rath 2023-08-07 14:39:45 +02:00
parent 2a2015f61d
commit 3fe591e5bb
2 changed files with 33 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/math/polysat/solver.cpp
View file

@ -1532,9 +1532,24 @@ namespace polysat {
if (!found) if (!found)
verbose_stream() << " " << d << ": <no constraint in polysat>\n"; verbose_stream() << " " << d << ": <no constraint in polysat>\n";
} }
for (pvar v : vars) for (pvar v : vars) {
if (signed_constraint c = m_constraints.find_op_by_result_var(v)) switch (m_kind[v]) {
case pvar_kind::external:
break;
case pvar_kind::name:
break;
case pvar_kind::op: {
signed_constraint c = m_constraints.find_op_by_result_var(v);
verbose_stream() << " op: " << lit_pp(*this, c) << "\n"; verbose_stream() << " op: " << lit_pp(*this, c) << "\n";
break;
}
case pvar_kind::internal:
verbose_stream() << " internal: v" << v << "\n";
break;
default:
UNREACHABLE();
}
}
}); });
#if ENABLE_LEMMA_VALIDITY_CHECK #if ENABLE_LEMMA_VALIDITY_CHECK
clause_builder cb(*this, "unsat core check"); clause_builder cb(*this, "unsat core check");

25
src/sat/smt/bv_polysat.cpp
View file

@ -309,22 +309,29 @@ namespace bv {
sat::literal_vector core; sat::literal_vector core;
euf::enode_pair_vector eqs; euf::enode_pair_vector eqs;
m_polysat.unsat_core(deps); m_polysat.unsat_core(deps);
for (auto n : deps) { IF_VERBOSE(10, verbose_stream() << "polysat_core:\n");
if (0 != (n.val() & 1)) for (auto d : deps) {
core.push_back(sat::to_literal(n.val() / 2)); if (0 != (d.val() & 1)) {
sat::literal const lit = sat::to_literal(d.val() / 2);
core.push_back(lit);
IF_VERBOSE(10, verbose_stream() << " " << d << ": " << mk_ismt2_pp(literal2expr(lit), m) << "\n");
}
else { else {
auto [v1, v2] = m_var_eqs[n.val() / 2]; VERIFY(d.val() <= 2 * m_var_eqs_head);
VERIFY(var2enode(v1)->get_root() == var2enode(v2)->get_root()); auto const [v1, v2] = m_var_eqs[d.val() / 2];
VERIFY(n.val() <= 2 * m_var_eqs_head); euf::enode* const n1 = var2enode(v1);
eqs.push_back(euf::enode_pair(var2enode(v1), var2enode(v2))); euf::enode* const n2 = var2enode(v2);
VERIFY(n1->get_root() == n2->get_root());
eqs.push_back(euf::enode_pair(n1, n2));
IF_VERBOSE(10, verbose_stream() << " " << d << ": " << mk_ismt2_pp(n1->get_expr(), m) << " == " << mk_ismt2_pp(n2->get_expr(), m) << "\n");
} }
} }
DEBUG_CODE( DEBUG_CODE({
for (auto lit : core) for (auto lit : core)
VERIFY(s().value(lit) == l_true); VERIFY(s().value(lit) == l_true);
for (auto const& [n1, n2] : eqs) for (auto const& [n1, n2] : eqs)
VERIFY(n1->get_root() == n2->get_root()); VERIFY(n1->get_root() == n2->get_root());
); });
auto ex = mk_bv2ext_justification(core, eqs); auto ex = mk_bv2ext_justification(core, eqs);
ctx.set_conflict(ex); ctx.set_conflict(ex);
} }