mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
parent
f2449df06e
commit
6f6c8d76eb
|
@ -100,6 +100,14 @@ namespace smt {
|
|||
|
||||
void context::justify(literal lit, index_set& s) {
|
||||
(void)m;
|
||||
auto add_antecedent = [&](literal l) {
|
||||
CTRACE("context", !m_antecedents.contains(l.var()),
|
||||
tout << "untracked literal: " << l << " "
|
||||
<< mk_pp(bool_var2expr(l.var()), m) << "\n";);
|
||||
if (m_antecedents.contains(l.var())) {
|
||||
s |= m_antecedents[l.var()];
|
||||
}
|
||||
};
|
||||
b_justification js = get_justification(lit.var());
|
||||
switch (js.get_kind()) {
|
||||
case b_justification::CLAUSE: {
|
||||
|
@ -107,13 +115,13 @@ namespace smt {
|
|||
if (!cls) break;
|
||||
for (literal lit2 : *cls) {
|
||||
if (lit2.var() != lit.var()) {
|
||||
s |= m_antecedents.find(lit2.var());
|
||||
add_antecedent(lit2);
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
case b_justification::BIN_CLAUSE: {
|
||||
s |= m_antecedents.find(js.get_literal().var());
|
||||
add_antecedent(js.get_literal());
|
||||
break;
|
||||
}
|
||||
case b_justification::AXIOM: {
|
||||
|
@ -123,10 +131,7 @@ namespace smt {
|
|||
literal_vector literals;
|
||||
m_conflict_resolution->justification2literals(js.get_justification(), literals);
|
||||
for (unsigned j = 0; j < literals.size(); ++j) {
|
||||
if (!m_antecedents.contains(literals[j].var())) {
|
||||
TRACE("context", tout << literals[j] << " " << mk_pp(bool_var2expr(literals[j].var()), m) << "\n";);
|
||||
}
|
||||
s |= m_antecedents.find(literals[j].var());
|
||||
add_antecedent(literals[j]);
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
|
|
@ -248,7 +248,7 @@ namespace smt {
|
|||
//
|
||||
// x1 <= k1 x1 >= k1, x2 <= x1 + k2 x2 >= x1 + k2
|
||||
//
|
||||
TRACE("arith_eq_propagation", tout << "fixed\n";);
|
||||
TRACE("arith_eq", tout << "fixed\n";);
|
||||
lower(x2)->push_justification(ante, numeral::zero(), proofs_enabled());
|
||||
upper(x2)->push_justification(ante, numeral::zero(), proofs_enabled());
|
||||
m_stats.m_fixed_eqs++;
|
||||
|
@ -350,14 +350,13 @@ namespace smt {
|
|||
antecedents.num_params(), antecedents.params("eq-propagate")));
|
||||
TRACE("arith_eq", tout << "detected equality: #" << _x->get_owner_id() << " = #" << _y->get_owner_id() << "\n";
|
||||
display_var(tout, x);
|
||||
display_var(tout, y););
|
||||
TRACE("arith_eq_propagation",
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
ctx.display_detailed_literal(tout, lits[i]);
|
||||
display_var(tout, y);
|
||||
for (literal lit : lits) {
|
||||
ctx.display_detailed_literal(tout, lit);
|
||||
tout << "\n";
|
||||
}
|
||||
for (unsigned i = 0; i < eqs.size(); ++i) {
|
||||
tout << mk_pp(eqs[i].first->get_owner(), m) << " = " << mk_pp(eqs[i].second->get_owner(), m) << "\n";
|
||||
for (auto const& p : eqs) {
|
||||
tout << mk_pp(p.first->get_owner(), m) << " = " << mk_pp(p.second->get_owner(), m) << "\n";
|
||||
}
|
||||
tout << " ==> ";
|
||||
tout << mk_pp(_x->get_owner(), m) << " = " << mk_pp(_y->get_owner(), m) << "\n";
|
||||
|
|
Loading…
Reference in a new issue