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

fix order for inequalities in arithmetic justifications such that implied bound literal is last. The self-checker uses this property to identify the implied bound

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-26 10:06:41 -07:00
parent c6aab89662
commit 249f0de80b
1 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/sat/smt/arith_diagnostics.cpp
View file

@ -209,12 +209,6 @@ namespace arith {
rational lc(1); rational lc(1);
for (unsigned i = m_lit_head; i < m_lit_tail; ++i) for (unsigned i = m_lit_head; i < m_lit_tail; ++i)
lc = lcm(lc, denominator(a.m_arith_hint.lit(i).first)); lc = lcm(lc, denominator(a.m_arith_hint.lit(i).first));
for (unsigned i = m_lit_head; i < m_lit_tail; ++i) {
auto const& [coeff, lit] = a.m_arith_hint.lit(i);
args.push_back(arith.mk_int(abs(coeff*lc)));
args.push_back(s.literal2expr(lit));
}
for (unsigned i = m_eq_head; i < m_eq_tail; ++i) { for (unsigned i = m_eq_head; i < m_eq_tail; ++i) {
auto [x, y, is_eq] = a.m_arith_hint.eq(i); auto [x, y, is_eq] = a.m_arith_hint.eq(i);
if (x->get_id() > y->get_id()) if (x->get_id() > y->get_id())
@ -224,6 +218,11 @@ namespace arith {
args.push_back(arith.mk_int(1)); args.push_back(arith.mk_int(1));
args.push_back(eq); args.push_back(eq);
} }
for (unsigned i = m_lit_head; i < m_lit_tail; ++i) {
auto const& [coeff, lit] = a.m_arith_hint.lit(i);
args.push_back(arith.mk_int(abs(coeff*lc)));
args.push_back(s.literal2expr(lit));
}
return m.mk_app(symbol(name), args.size(), args.data(), m.mk_proof_sort()); return m.mk_app(symbol(name), args.size(), args.data(), m.mk_proof_sort());
} }
} }