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

generate explanations inside of a lemma if possible

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-11 17:07:08 -08:00
parent 3987cc5f1b
commit c9a6d23897
2 changed files with 164 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/util/lp/explanation.h
View file

@ -36,10 +36,11 @@ public:
} }
template <typename A> template <typename A>
void add(const A& a) { for (auto j : a) push_justification(j); } void add(const A& a) { for (auto j : a) add(j); }
void add(const std::pair<mpq, constraint_index>& j) { push_justification(j.second, j.first); }
void add(unsigned j) { push_justification(j); } void add(unsigned j) { push_justification(j); }
bool empty() const { return m_explanation.empty(); } bool empty() const { return m_explanation.empty(); }
size_t size() const { return m_explanation.size(); } size_t size() const { return m_explanation.size(); }
}; };

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

@ -379,27 +379,124 @@ struct solver::imp {
return out; return out;
} }
bool explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const {
rational b(0); // the bound
for (const auto& p : t) {
rational pb;
if (explain_coeff_upper_bound(p, pb, e)) {
b += pb;
} else {
e.clear();
return false;
}
}
if (b > rs ) {
e.clear();
return false;
}
return true;
}
bool explain_lower_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const {
rational b(0); // the bound
for (const auto& p : t) {
rational pb;
if (explain_coeff_lower_bound(p, pb, e)) {
b += pb;
} else {
e.clear();
return false;
}
}
if (b < rs ) {
e.clear();
return false;
}
return true;
}
bool explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const {
const rational& a = p.coeff();
SASSERT(!a.is_zero());
unsigned c; // the index for the lower or the upper bound
if (a.is_pos()) {
unsigned c = m_lar_solver.get_column_lower_bound_witness(p.var());
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_lower_bound(p.var()).x;
e.add(c);
return true;
}
// a.is_neg()
c = m_lar_solver.get_column_upper_bound_witness(p.var());
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_upper_bound(p.var()).x;
e.add(c);
return true;
}
bool explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const {
const rational& a = p.coeff();
SASSERT(!a.is_zero());
unsigned c; // the index for the lower or the upper bound
if (a.is_neg()) {
unsigned c = m_lar_solver.get_column_lower_bound_witness(p.var());
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_lower_bound(p.var()).x;
e.add(c);
return true;
}
// a.is_pos()
c = m_lar_solver.get_column_upper_bound_witness(p.var());
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_upper_bound(p.var()).x;
e.add(c);
return true;
}
// return true iff the negation of the ineq can be derived from the constraints
bool explain_ineq(const lp::lar_term& t, llc cmp, const rational& rs) { 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 // check that we have something like 0 < 0, which is always false and can be safely
// removed from the lemma // 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)) return true; (cmp == llc::LT || cmp == llc::GT || cmp == llc::NE)) return true;
/*
lp::explanation exp; lp::explanation exp;
bool r; bool r;
switch(negate(cmp)) { switch(negate(cmp)) {
case llc::LE: case llc::LE:
r = explain_upper_bound(t, rs, exp);
case llc::LT: return llc::GE; break;
case llc::GE: return llc::LT; case llc::LT:
case llc::GT: return llc::LE; r = explain_upper_bound(t, rs - rational(1), exp);
case llc::EQ: return llc::NE; break;
case llc::NE: return llc::EQ; case llc::GE:
}*/ r = explain_lower_bound(t, rs, exp);
break;
case llc::GT:
r = explain_lower_bound(t, rs + rational(1), exp);
break;
case llc::EQ:
r = explain_lower_bound(t, rs, exp) && explain_upper_bound(t, rs, exp);
break;
case llc::NE:
r = explain_lower_bound(t, rs + rational(1), exp) || explain_upper_bound(t, rs - rational(1), exp);
break;
default:
SASSERT(false);
r = false;
}
if (r) {
current_expl().add(exp);
return true;
}
return false; return false;
} }
void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs, lemma& l) { void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs, lemma& l) {
TRACE("nla_solver", m_lar_solver.print_term(t, tout << "t = "););
if (explain_ineq(t, cmp, rs)) if (explain_ineq(t, cmp, rs))
return; return;
m_lar_solver.subs_term_columns(t); m_lar_solver.subs_term_columns(t);
@ -466,61 +563,61 @@ struct solver::imp {
return cmp; return cmp;
} }
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);
switch(cmp) { // switch(cmp) {
case llc::LE: { // case llc::LE: {
if (uc + 1 == 0 || m_lar_solver.column_upper_bound(j) > rs) // if (uc + 1 == 0 || m_lar_solver.column_upper_bound(j) > rs)
return false; // return false;
exp.add(uc); // exp.add(uc);
return true; // return true;
} // }
case llc::LT: { // case llc::LT: {
if (uc + 1 == 0 || m_lar_solver.column_upper_bound(j) >= rs) // if (uc + 1 == 0 || m_lar_solver.column_upper_bound(j) >= rs)
return false; // return false;
exp.add(uc); // exp.add(uc);
return true; // return true;
} // }
case llc::GE: { // case llc::GE: {
if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) < rs) // if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) < rs)
return false; // return false;
exp.add(lc); // exp.add(lc);
return true; // return true;
} // }
case llc::GT: { // case llc::GT: {
if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) <= rs) // if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) <= rs)
return false; // return false;
exp.add(lc); // exp.add(lc);
return true; // return true;
} // }
case llc::EQ: // case llc::EQ:
{ // {
if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) < rs // if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) < rs
|| // ||
uc + 1 == 0 || m_lar_solver.column_upper_bound(j) > rs) // uc + 1 == 0 || m_lar_solver.column_upper_bound(j) > rs)
return false; // return false;
exp.add(lc); // exp.add(lc);
exp.add(uc); // exp.add(uc);
return true; // return true;
} // }
case llc::NE: { // case llc::NE: {
if (uc + 1 && m_lar_solver.column_upper_bound(j) < rs) { // if (uc + 1 && m_lar_solver.column_upper_bound(j) < rs) {
exp.add(uc); // exp.add(uc);
return true; // return true;
} // }
if (lc + 1 && m_lar_solver.column_lower_bound(j) > rs) { // if (lc + 1 && m_lar_solver.column_lower_bound(j) > rs) {
exp.add(lc); // exp.add(lc);
return true; // return true;
} // }
return false; // return false;
}; // };
default: // default:
SASSERT(false); // SASSERT(false);
}; // };
SASSERT(false); // SASSERT(false);
return false; // return false;
} // }
void mk_ineq(const rational& a, lpvar j, llc cmp, lemma& l) { void mk_ineq(const rational& a, lpvar j, llc cmp, lemma& l) {
mk_ineq(a, j, cmp, rational::zero(), l); mk_ineq(a, j, cmp, rational::zero(), l);
@ -2413,7 +2510,7 @@ struct solver::imp {
else { else {
mk_ineq(j, llc::LE, a, l); mk_ineq(j, llc::LE, a, l);
} }
TRACE("nla_solver", print_ineq(l.ineqs().back(), tout);); TRACE("nla_solver", print_lemma(tout););
} }
void generate_two_tang_lines(const bfc & bf, const point& xy, const rational& sign, lpvar j) { void generate_two_tang_lines(const bfc & bf, const point& xy, const rational& sign, lpvar j) {