mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-21 10:41:35 +00:00
Code Activity

handle output from niil_solver (#77)

Browse source 
* handle output from niil_solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add proper equality handling

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-08-17 18:52:52 -07:00 • committed by Lev Nachmanson
parent 49ae42cebd
commit 88ea90fbb9
1 changed files with 66 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

67
src/smt/theory_lra.cpp
View file

@ -1678,6 +1678,22 @@ public:
return FC_GIVEUP; return FC_GIVEUP;
} }
// create a eq atom representing "term = 0"
app_ref mk_eq(lp::lar_term const& term) {
rational offset(0);
u_map<rational> coeffs;
term2coeffs(term, coeffs, rational::one(), offset);
offset.neg();
bool isint = offset.is_int();
for (auto const& kv : coeffs) isint &= is_int(kv.m_key) && kv.m_value.is_int();
app_ref atom(m);
app_ref t = coeffs2app(coeffs, rational::zero(), isint);
atom = m.mk_eq(t, a.mk_numeral(offset, isint));
ctx().internalize(atom, true);
ctx().mark_as_relevant(atom.get());
return atom;
}
// create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false // create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false
app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) { app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) {
bool is_int = k.is_int(); bool is_int = k.is_int();
@ -2059,6 +2075,47 @@ 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) {
case l_false: {
literal_vector core;
for (auto const& ineq : m_lemma) {
bool is_lower = true, pos = true, is_eq = false;
switch (ineq.m_cmp) {
case lp::LE: is_lower = false; pos = true; break;
case lp::LT: is_lower = true; pos = false; break;
case lp::GE: is_lower = true; pos = true; break;
case lp::GT: is_lower = true; pos = false; break;
case lp::EQ: is_eq = true; pos = true; break;
case lp::NE: is_eq = true; pos = false; break;
default: UNREACHABLE();
}
app_ref atom(m);
if (is_eq) {
atom = mk_eq(ineq.m_term);
}
else {
// create term >= 0 (or term <= 0)
atom = mk_bound(ineq.m_term, rational::zero(), is_lower);
}
literal lit(ctx().get_bool_var(atom), pos);
core.push_back(~lit);
}
std::cout << "the following conjunction should be unsat:\n";
ctx().display_literals_verbose(std::cout << "core ", core) << "\n";
display_evidence(std::cout, m_explanation); std::cout << "\n";
set_conflict(core);
break;
}
case l_true:
if (assume_eqs()) {
return l_false;
}
break;
case l_undef:
break;
}
return r; return r;
} }
@ -3116,9 +3173,17 @@ public:
} }
void set_conflict1() { void set_conflict1() {
literal_vector core;
set_conflict(core);
}
void set_conflict(literal_vector const& core) {
m_eqs.reset(); m_eqs.reset();
m_core.reset(); m_core.reset();
m_params.reset(); m_params.reset();
for (literal lit : core) {
m_core.push_back(lit);
}
// m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed // m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
/* /*
static unsigned cn = 0; static unsigned cn = 0;
@ -3135,7 +3200,7 @@ public:
set_evidence(ev.second); set_evidence(ev.second);
} }
} }
// SASSERT(validate_conflict()); // SASSERT(validate_conflict());
dump_conflict(); dump_conflict();
ctx().set_conflict( ctx().set_conflict(
ctx().mk_justification( ctx().mk_justification(