mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 16:38:45 +00:00
Code Activity

substitute the term columns in nla_solver before returning a term to theory_nra

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-11 14:34:40 -08:00
parent b2943c34f1
commit 3987cc5f1b
1 changed files with 28 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

58
src/util/lp/nla_solver.cpp
View file

@ -378,24 +378,31 @@ struct solver::imp {
out << "\n"; out << "\n";
return out; return out;
} }
void mk_ineq(const lp::lar_term& t, llc cmp, const rational& rs, lemma& l) {
bool explain_ineq(const lp::lar_term& t, llc cmp, const rational& rs) {
// check that we have something like 0 < 0, which is always false and can be safely
// removed from the lemma
if (t.is_empty() && rs.is_zero() && if (t.is_empty() && rs.is_zero() &&
(cmp == llc::LT || cmp == llc::GT || cmp == llc::NE)) (cmp == llc::LT || cmp == llc::GT || cmp == llc::NE)) return true;
return; // otherwise we get something like 0 < 0, which is always false and can be removed from the lemma /*
switch(cmp){ lp::explanation exp;
case llc::NE: bool r;
if (t.size() == 1) { switch(negate(cmp)) {
const auto & p = t.coeffs().begin(); case llc::LE:
auto r = rs/p->second;
lpvar j = p->first; case llc::LT: return llc::GE;
if (vvr(j) == r && var_is_fixed_to_val(j, r)) { case llc::GE: return llc::LT;
explain_fixed_var(j); // instead of adding the inequality case llc::GT: return llc::LE;
return; case llc::EQ: return llc::NE;
} case llc::NE: return llc::EQ;
} }*/
default: return false;
break; }
}
void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs, lemma& l) {
if (explain_ineq(t, cmp, rs))
return;
m_lar_solver.subs_term_columns(t);
l.push_back(ineq(cmp, t, rs)); l.push_back(ineq(cmp, t, rs));
} }
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs, lemma& l) { void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs, lemma& l) {
@ -437,10 +444,10 @@ struct solver::imp {
llc negate(llc cmp) { llc negate(llc cmp) {
switch(cmp) { switch(cmp) {
case llc::LE: return llc::GE; case llc::LE: return llc::GT;
case llc::LT: return llc::GT; case llc::LT: return llc::GE;
case llc::GE: return llc::LE; case llc::GE: return llc::LT;
case llc::GT: return llc::LT; case llc::GT: return llc::LE;
case llc::EQ: return llc::NE; case llc::EQ: return llc::NE;
case llc::NE: return llc::EQ; case llc::NE: return llc::EQ;
default: SASSERT(false); default: SASSERT(false);
@ -459,15 +466,6 @@ struct solver::imp {
return cmp; return cmp;
} }
bool explain(const rational& a, lpvar j, llc cmp, const rational& rs, lp::explanation & exp) {
cmp = negate(cmp);
if (a == rational(1))
return explain(j, cmp, rs, exp);
if (a == -rational(1))
return explain(j, apply_minus(cmp), -rs, exp);
return false;
}
bool explain(lpvar j, llc cmp, const rational& rs, lp::explanation & exp) { bool explain(lpvar j, llc cmp, const rational& rs, lp::explanation & exp) {
unsigned lc, uc; // indices for the lower and upper bounds unsigned lc, uc; // indices for the lower and upper bounds
m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc); m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);