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

tinker with bound atom (#80)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-08-27 20:48:11 -07:00 • committed by Lev Nachmanson
parent 89d086fff0
commit 64ecefdf07
1 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_lra.cpp
View file

@ -2075,7 +2075,6 @@ public:
niil::lemma m_lemma; niil::lemma m_lemma;
lbool check_aftermath_niil(lbool r) { lbool check_aftermath_niil(lbool r) {
TRACE("arith", tout << "niil: " << r << "\n";);
switch (r) { switch (r) {
case l_false: { case l_false: {
literal_vector core; literal_vector core;
@ -2083,14 +2082,15 @@ public:
bool is_lower = true, pos = true, is_eq = false; bool is_lower = true, pos = true, is_eq = false;
switch (ineq.m_cmp) { switch (ineq.m_cmp) {
case lp::LE: is_lower = false; pos = true; break; case lp::LE: is_lower = false; pos = false; break;
case lp::LT: is_lower = true; pos = false; break; case lp::LT: is_lower = true; pos = true; break;
case lp::GE: is_lower = true; pos = true; break; case lp::GE: is_lower = true; pos = false; break;
case lp::GT: is_lower = true; pos = false; break; case lp::GT: is_lower = false; pos = true; break;
case lp::EQ: is_eq = true; pos = true; break; case lp::EQ: is_eq = true; pos = true; break;
case lp::NE: is_eq = true; pos = false; break; case lp::NE: is_eq = true; pos = false; break;
default: UNREACHABLE(); default: UNREACHABLE();
} }
TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
app_ref atom(m); app_ref atom(m);
if (is_eq) { if (is_eq) {
atom = mk_eq(ineq.m_term); atom = mk_eq(ineq.m_term);
@ -3205,9 +3205,11 @@ public:
for (auto const& eq : m_eqs) { for (auto const& eq : m_eqs) {
m_core.push_back(th.mk_eq(eq.first->get_owner(), eq.second->get_owner(), false)); m_core.push_back(th.mk_eq(eq.first->get_owner(), eq.second->get_owner(), false));
} }
for (auto & c : m_core) { for (literal & c : m_core) {
c.neg(); c.neg();
ctx().mark_as_relevant(c);
} }
TRACE("arith", ctx().display_literals_verbose(tout, m_core););
ctx().mk_th_axiom(get_id(), m_core.size(), m_core.c_ptr()); ctx().mk_th_axiom(get_id(), m_core.size(), m_core.c_ptr());
} }
} }