mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

check delayed eqs before nla

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-26 11:48:26 -07:00
parent fb78a9e3a5
commit 646eacd2aa
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/arith_solver.cpp
View file

@ -1037,6 +1037,9 @@ namespace arith {
break; break;
} }
if (!check_delayed_eqs())
return sat::check_result::CR_CONTINUE;
switch (check_nla()) { switch (check_nla()) {
case l_true: case l_true:
break; break;
@ -1052,8 +1055,6 @@ namespace arith {
++m_stats.m_assume_eqs; ++m_stats.m_assume_eqs;
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
} }
if (!check_delayed_eqs())
return sat::check_result::CR_CONTINUE;
if (!int_undef && !check_bv_terms()) if (!int_undef && !check_bv_terms())
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
@ -1250,7 +1251,7 @@ namespace arith {
TRACE("arith_conflict", TRACE("arith_conflict",
tout << "Lemma - " << (is_conflict ? "conflict" : "propagation") << "\n"; tout << "Lemma - " << (is_conflict ? "conflict" : "propagation") << "\n";
for (literal c : m_core) tout << c << ": " << literal2expr(c) << "\n"; for (literal c : m_core) tout << c << ": " << literal2expr(c) << " := " << s().value(c) << "\n";
for (auto p : m_eqs) tout << ctx.bpp(p.first) << " == " << ctx.bpp(p.second) << "\n";); for (auto p : m_eqs) tout << ctx.bpp(p.first) << " == " << ctx.bpp(p.second) << "\n";);
if (ctx.get_config().m_arith_validate) if (ctx.get_config().m_arith_validate)
@ -1525,7 +1526,7 @@ namespace arith {
continue; continue;
ctx.mark_relevant(lit); ctx.mark_relevant(lit);
s().set_phase(lit); s().set_phase(lit);
verbose_stream() << lit << ":= " << s().value(lit) << "\n"; // verbose_stream() << lit << ":= " << s().value(lit) << "\n";
// force trichotomy axiom for equality literals // force trichotomy axiom for equality literals
if (ineq.cmp() == lp::EQ && false) { if (ineq.cmp() == lp::EQ && false) {
nla::lemma l; nla::lemma l;