mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

create class lemma

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-10 21:40:47 -08:00
parent 4243bd3e2a
commit b2943c34f1
4 changed files with 119 additions and 131 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_lra.cpp
View file

@ -2153,7 +2153,7 @@ public:
void false_case_of_check_nla() { void false_case_of_check_nla() {
literal_vector core; literal_vector core;
for (auto const& ineq : m_lemma) { for (auto const& ineq : m_lemma.ineqs()) {
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 = false; break; case lp::LE: is_lower = false; pos = false; break;
@ -2181,14 +2181,12 @@ public:
set_conflict_or_lemma(core, false); set_conflict_or_lemma(core, false);
} }
lbool check_aftermath_nla(lbool r, const vector<nla::lemma>& l, lbool check_aftermath_nla(lbool r, const vector<nla::lemma>& lv) {
const vector<lp::explanation>& e) {
switch (r) { switch (r) {
case l_false: { case l_false: {
SASSERT(l.size() == e.size()); for(const nla::lemma & l : lv) {
for(unsigned i = 0; i < l.size(); i++) { m_lemma = l; //todo avoit the copy
m_lemma = l[i]; m_explanation = l.expl();
m_explanation = e[i];
false_case_of_check_nla(); false_case_of_check_nla();
} }
break; break;
@ -2217,9 +2215,8 @@ public:
m_explanation.clear(); m_explanation.clear();
return check_aftermath_nra(m_nra->check(m_explanation)); return check_aftermath_nra(m_nra->check(m_explanation));
} }
vector<nla::lemma> l; vector<nla::lemma> lv;
vector<lp::explanation> e; return check_aftermath_nla(m_nla->check(lv), lv);
return check_aftermath_nla(m_nla->check(e, l), l, e);
} }
/** /**

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

@ -41,5 +41,6 @@ public:
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(); }
}; };
} }

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

@ -96,7 +96,6 @@ struct solver::imp {
// m_var_to_its_monomial[m_monomials[i].var()] = i // m_var_to_its_monomial[m_monomials[i].var()] = i
std::unordered_map<lpvar, unsigned> m_var_to_its_monomial; std::unordered_map<lpvar, unsigned> m_var_to_its_monomial;
vector<lp::explanation> * m_expl_vec;
vector<lemma> * m_lemma_vec; vector<lemma> * m_lemma_vec;
unsigned_vector m_to_refine; unsigned_vector m_to_refine;
std::unordered_map<unsigned_vector, unsigned, hash_svector> m_mkeys; // the key is the sorted vars of a monomial std::unordered_map<unsigned_vector, unsigned, hash_svector> m_mkeys; // the key is the sorted vars of a monomial
@ -147,12 +146,12 @@ struct solver::imp {
return compare_holds(value(n.term()), n.cmp(), n.rs()); return compare_holds(value(n.term()), n.cmp(), n.rs());
} }
bool lemma_holds(const lemma& l) const { bool an_ineq_holds(const lemma& l) const {
for(auto &i : l) { for(const ineq &i : l.ineqs()) {
if (!ineq_holds(i)) if (!ineq_holds(i))
return false; return false;
} }
return true; return false;
} }
rational vvr(lpvar j) const { return m_lar_solver.get_column_value_rational(j); } rational vvr(lpvar j) const { return m_lar_solver.get_column_value_rational(j); }
@ -540,16 +539,16 @@ struct solver::imp {
// the monomials should be equal by modulo sign but this is not so in the model // the monomials should be equal by modulo sign but this is not so in the model
void fill_explanation_and_lemma_sign(const monomial& a, const monomial & b, rational const& sign) { void fill_explanation_and_lemma_sign(const monomial& a, const monomial & b, rational const& sign) {
SASSERT(sign == 1 || sign == -1); SASSERT(sign == 1 || sign == -1);
explain(a, m_expl_vec->back()); explain(a, current_expl());
explain(b, m_expl_vec->back()); explain(b, current_expl());
TRACE("nla_solver", TRACE("nla_solver",
tout << "used constraints: "; tout << "used constraints: ";
for (auto &p : m_expl_vec->back()) for (auto &p : current_expl())
m_lar_solver.print_constraint(p.second, tout); tout << "\n"; m_lar_solver.print_constraint(p.second, tout); tout << "\n";
); );
SASSERT(m_lemma_vec->back().size() == 0); SASSERT(current_ineqs().size() == 0);
mk_ineq(rational(1), a.var(), -sign, b.var(), llc::EQ, rational::zero(), m_lemma_vec->back()); mk_ineq(rational(1), a.var(), -sign, b.var(), llc::EQ, rational::zero(), current_lemma());
TRACE("nla_solver", print_lemma(m_lemma_vec->back(), tout);); TRACE("nla_solver", print_lemma(tout););
} }
// Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus. // Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus.
@ -586,7 +585,7 @@ struct solver::imp {
// the value of the i-th monomial has to be equal to the value of the k-th monomial modulo sign // the value of the i-th monomial has to be equal to the value of the k-th monomial modulo sign
// but it is not the case in the model // but it is not the case in the model
void generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign) { void generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign) {
add_empty_lemma_and_explanation(); add_empty_lemma();
TRACE("nla_solver", TRACE("nla_solver",
tout << "m = "; print_monomial_with_vars(m, tout); tout << "m = "; print_monomial_with_vars(m, tout);
tout << "n = "; print_monomial_with_vars(n, tout); tout << "n = "; print_monomial_with_vars(n, tout);
@ -594,7 +593,7 @@ struct solver::imp {
mk_ineq(m.var(), -sign, n.var(), llc::EQ, current_lemma()); mk_ineq(m.var(), -sign, n.var(), llc::EQ, current_lemma());
explain(m, current_expl()); explain(m, current_expl());
explain(n, current_expl()); explain(n, current_expl());
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
} }
// the value of the i-th monomial has to be equal to the value of the k-th monomial modulo sign // the value of the i-th monomial has to be equal to the value of the k-th monomial modulo sign
@ -602,7 +601,7 @@ struct solver::imp {
// abs_vars_key is formed by m_vars_equivalence.get_abs_root_for_var(k), where // abs_vars_key is formed by m_vars_equivalence.get_abs_root_for_var(k), where
// k runs over m. // k runs over m.
void generate_sign_lemma_model_based(const monomial& m, const monomial& n, const rational& sign) { void generate_sign_lemma_model_based(const monomial& m, const monomial& n, const rational& sign) {
add_empty_lemma_and_explanation(); add_empty_lemma();
if (sign.is_zero()) { if (sign.is_zero()) {
// either m or n has to be equal zero, but it is not the case // either m or n has to be equal zero, but it is not the case
SASSERT(!vvr(m).is_zero() || !vvr(n).is_zero()); SASSERT(!vvr(m).is_zero() || !vvr(n).is_zero());
@ -610,7 +609,7 @@ struct solver::imp {
generate_zero_lemma(m); generate_zero_lemma(m);
if (!vvr(n).is_zero()) if (!vvr(n).is_zero())
generate_zero_lemma(n); generate_zero_lemma(n);
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
return; return;
} }
unsigned_vector mvars(m.vars()); unsigned_vector mvars(m.vars());
@ -647,11 +646,12 @@ struct solver::imp {
} }
mk_ineq(m.var(), -sign, n.var(), llc::EQ, current_lemma()); mk_ineq(m.var(), -sign, n.var(), llc::EQ, current_lemma());
TRACE("nla_solver", print_lemma(current_lemma(), tout);); TRACE("nla_solver", print_lemma(tout););
} }
lemma& current_lemma() { return m_lemma_vec->back(); } lemma& current_lemma() { return m_lemma_vec->back(); }
lp::explanation& current_expl() {return m_expl_vec->back();} vector<ineq>& current_ineqs() { return current_lemma().ineqs(); }
lp::explanation& current_expl() { return current_lemma().expl(); }
static int rat_sign(const rational& r) { static int rat_sign(const rational& r) {
return r.is_pos()? 1 : ( r.is_neg()? -1 : 0); return r.is_pos()? 1 : ( r.is_neg()? -1 : 0);
@ -881,18 +881,17 @@ struct solver::imp {
return out; return out;
} }
std::ostream & print_lemma(const lemma& l, std::ostream & out) const { std::ostream & print_ineqs(const lemma& l, std::ostream & out) const {
out << "lemma: ";
for (unsigned i = 0; i < l.size(); i++) {
print_ineq(l[i], out);
if (i + 1 < l.size()) out << " or ";
}
out << std::endl;
std::unordered_set<lpvar> vars; std::unordered_set<lpvar> vars;
for (auto & in: l) { out << "lemma: ";
for (unsigned i = 0; i < l.ineqs().size(); i++) {
auto & in = l.ineqs()[i];
print_ineq(in, out);
if (i + 1 < l.size()) out << " or ";
for (const auto & p: in.m_term) for (const auto & p: in.m_term)
vars.insert(p.var()); vars.insert(p.var());
} }
out << std::endl;
for (lpvar j : vars) { for (lpvar j : vars) {
print_var(j, out); print_var(j, out);
} }
@ -950,7 +949,7 @@ struct solver::imp {
} }
} }
add_empty_lemma_and_explanation(); add_empty_lemma();
if (derived) if (derived)
mk_ineq(var(rm), llc::NE, current_lemma()); mk_ineq(var(rm), llc::NE, current_lemma());
for (auto j : f) { for (auto j : f) {
@ -958,7 +957,7 @@ struct solver::imp {
} }
explain(rm, current_expl()); explain(rm, current_expl());
TRACE("nla_solver", print_lemma(current_lemma(), tout);); TRACE("nla_solver", print_lemma(tout););
return true; return true;
} }
@ -967,7 +966,7 @@ struct solver::imp {
// xy = 0 -> x = 0 or y = 0 // xy = 0 -> x = 0 or y = 0
bool basic_lemma_for_mon_zero_derived(const rooted_mon& rm, const factorization& f) { bool basic_lemma_for_mon_zero_derived(const rooted_mon& rm, const factorization& f) {
TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout););
add_empty_lemma_and_explanation(); add_empty_lemma();
explain_fixed_var(var(rm)); explain_fixed_var(var(rm));
std::unordered_set<lpvar> processed; std::unordered_set<lpvar> processed;
for (auto j : f) { for (auto j : f) {
@ -975,7 +974,7 @@ struct solver::imp {
mk_ineq(var(j), llc::EQ, current_lemma()); mk_ineq(var(j), llc::EQ, current_lemma());
} }
explain(rm, current_expl()); explain(rm, current_expl());
TRACE("nla_solver", print_lemma(current_lemma(), tout);); TRACE("nla_solver", print_lemma(tout););
return true; return true;
} }
@ -983,13 +982,13 @@ struct solver::imp {
bool basic_lemma_for_mon_zero_model_based(const rooted_mon& rm, const factorization& f) { bool basic_lemma_for_mon_zero_model_based(const rooted_mon& rm, const factorization& f) {
TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout););
SASSERT(vvr(rm).is_zero()); SASSERT(vvr(rm).is_zero());
add_empty_lemma_and_explanation(); add_empty_lemma();
mk_ineq(var(rm), llc::NE, current_lemma()); mk_ineq(var(rm), llc::NE, current_lemma());
for (auto j : f) { for (auto j : f) {
mk_ineq(var(j), llc::EQ, current_lemma()); mk_ineq(var(j), llc::EQ, current_lemma());
} }
explain(rm, current_expl()); explain(rm, current_expl());
TRACE("nla_solver", print_lemma(current_lemma(), tout);); TRACE("nla_solver", print_lemma(tout););
return true; return true;
} }
@ -1031,12 +1030,12 @@ struct solver::imp {
if (zero_j == -1) { if (zero_j == -1) {
return false; return false;
} }
add_empty_lemma_and_explanation(); add_empty_lemma();
mk_ineq(zero_j, llc::NE, current_lemma()); mk_ineq(zero_j, llc::NE, current_lemma());
mk_ineq(var(rm), llc::EQ, current_lemma()); mk_ineq(var(rm), llc::EQ, current_lemma());
explain(rm, current_expl()); explain(rm, current_expl());
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
return true; return true;
} }
@ -1062,11 +1061,11 @@ struct solver::imp {
if (zero_j == -1) { if (zero_j == -1) {
return false; return false;
} }
add_empty_lemma_and_explanation(); add_empty_lemma();
explain_fixed_var(zero_j); explain_fixed_var(zero_j);
explain_var_separated_from_zero(var(rm)); explain_var_separated_from_zero(var(rm));
explain(rm, current_expl()); explain(rm, current_expl());
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
return true; return true;
} }
@ -1108,7 +1107,7 @@ struct solver::imp {
return false; return false;
} }
add_empty_lemma_and_explanation(); add_empty_lemma();
// mon_var = 0 // mon_var = 0
mk_ineq(mon_var, llc::EQ, current_lemma()); mk_ineq(mon_var, llc::EQ, current_lemma());
@ -1124,7 +1123,7 @@ struct solver::imp {
// not_one_j = -1 // not_one_j = -1
mk_ineq(not_one_j, llc::EQ, -rational(1), current_lemma()); mk_ineq(not_one_j, llc::EQ, -rational(1), current_lemma());
explain(rm, current_expl()); explain(rm, current_expl());
TRACE("nla_solver", print_lemma(current_lemma(), tout); ); TRACE("nla_solver", print_lemma(tout); );
return true; return true;
} }
@ -1186,7 +1185,7 @@ struct solver::imp {
return false; return false;
} }
add_empty_lemma_and_explanation(); add_empty_lemma();
// mon_var = 0 // mon_var = 0
if (mon_var_is_sep_from_zero) if (mon_var_is_sep_from_zero)
explain_var_separated_from_zero(mon_var); explain_var_separated_from_zero(mon_var);
@ -1201,7 +1200,7 @@ struct solver::imp {
// not_one_j = -1 // not_one_j = -1
mk_ineq(not_one_j, llc::EQ, -rational(1), current_lemma()); mk_ineq(not_one_j, llc::EQ, -rational(1), current_lemma());
explain(rm, current_expl()); explain(rm, current_expl());
TRACE("nla_solver", print_lemma_and_expl(tout); ); TRACE("nla_solver", print_lemma(tout); );
return true; return true;
} }
@ -1241,7 +1240,7 @@ struct solver::imp {
} }
} }
add_empty_lemma_and_explanation(); add_empty_lemma();
explain(rm, current_expl()); explain(rm, current_expl());
for (auto j : f){ for (auto j : f){
@ -1257,7 +1256,7 @@ struct solver::imp {
} }
TRACE("nla_solver", TRACE("nla_solver",
tout << "rm = "; print_rooted_monomial_with_vars(rm, tout); tout << "rm = "; print_rooted_monomial_with_vars(rm, tout);
print_lemma_and_expl(tout);); print_lemma(tout););
return true; return true;
} }
// use the fact // use the fact
@ -1289,7 +1288,7 @@ struct solver::imp {
return false; return false;
} }
add_empty_lemma_and_explanation(); add_empty_lemma();
explain(rm, current_expl()); explain(rm, current_expl());
for (auto j : f){ for (auto j : f){
@ -1305,7 +1304,7 @@ struct solver::imp {
} }
TRACE("nla_solver", TRACE("nla_solver",
tout << "rm = "; print_rooted_monomial_with_vars(rm, tout); tout << "rm = "; print_rooted_monomial_with_vars(rm, tout);
print_lemma(current_lemma(), tout);); print_lemma(tout););
return true; return true;
} }
@ -1343,7 +1342,7 @@ struct solver::imp {
print_rooted_monomial_with_vars(rm, tout); print_rooted_monomial_with_vars(rm, tout);
tout << "fc = "; print_factorization(fc, tout); tout << "fc = "; print_factorization(fc, tout);
tout << "orig mon = "; print_monomial(m_monomials[rm.orig_index()], tout);); tout << "orig mon = "; print_monomial(m_monomials[rm.orig_index()], tout););
add_empty_lemma_and_explanation(); add_empty_lemma();
int fi = 0; int fi = 0;
for (factor f : fc) { for (factor f : fc) {
if (fi++ != factor_index) { if (fi++ != factor_index) {
@ -1364,7 +1363,7 @@ struct solver::imp {
} }
explain(fc, current_expl()); explain(fc, current_expl());
explain(rm, current_expl()); explain(rm, current_expl());
TRACE("nla_solver", print_lemma(current_lemma(), tout); print_explanation(current_expl(), tout);); TRACE("nla_solver", print_lemma(tout); );
} }
template <typename T> template <typename T>
@ -1661,7 +1660,6 @@ struct solver::imp {
m_vars_equivalence.clear(); m_vars_equivalence.clear();
m_rm_table.clear(); m_rm_table.clear();
m_monomials_containing_var.clear(); m_monomials_containing_var.clear();
m_expl_vec->clear();
m_lemma_vec->clear(); m_lemma_vec->clear();
} }
@ -1743,7 +1741,7 @@ struct solver::imp {
llc ab_cmp, llc ab_cmp,
bool derived bool derived
) { ) {
add_empty_lemma_and_explanation(); add_empty_lemma();
mk_ineq(rational(c_sign) * flip_sign(c), var(c), llc::LE, current_lemma()); mk_ineq(rational(c_sign) * flip_sign(c), var(c), llc::LE, current_lemma());
negate_factor_equality(c, d); negate_factor_equality(c, d);
negate_factor_relation(rational(c_sign), a, rational(d_sign), b); negate_factor_relation(rational(c_sign), a, rational(d_sign), b);
@ -1756,11 +1754,11 @@ struct solver::imp {
explain(c, current_expl()); explain(c, current_expl());
explain(d, current_expl()); // todo: double check that these explanations are enough, too much!? explain(d, current_expl()); // todo: double check that these explanations are enough, too much!?
} }
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
} }
void print_lemma_and_expl(std::ostream& out) { void print_lemma(std::ostream& out) {
print_lemma(current_lemma(), out); print_ineqs(current_lemma(), out);
print_explanation(current_expl(), out); print_explanation(current_expl(), out);
} }
@ -2124,7 +2122,7 @@ struct solver::imp {
void generate_monl_strict(const rooted_mon& a, void generate_monl_strict(const rooted_mon& a,
const rooted_mon& b, const rooted_mon& b,
unsigned strict) { unsigned strict) {
add_empty_lemma_and_explanation(); add_empty_lemma();
auto akey = get_sorted_key_with_vars(a); auto akey = get_sorted_key_with_vars(a);
auto bkey = get_sorted_key_with_vars(b); auto bkey = get_sorted_key_with_vars(b);
SASSERT(akey.size() == bkey.size()); SASSERT(akey.size() == bkey.size());
@ -2139,13 +2137,13 @@ struct solver::imp {
assert_abs_val_a_le_abs_var_b(a, b, true); assert_abs_val_a_le_abs_var_b(a, b, true);
explain(a, current_expl()); explain(a, current_expl());
explain(b, current_expl()); explain(b, current_expl());
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
} }
// not a strict version // not a strict version
void generate_monl(const rooted_mon& a, void generate_monl(const rooted_mon& a,
const rooted_mon& b) { const rooted_mon& b) {
add_empty_lemma_and_explanation(); add_empty_lemma();
auto akey = get_sorted_key_with_vars(a); auto akey = get_sorted_key_with_vars(a);
auto bkey = get_sorted_key_with_vars(b); auto bkey = get_sorted_key_with_vars(b);
SASSERT(akey.size() == bkey.size()); SASSERT(akey.size() == bkey.size());
@ -2155,7 +2153,7 @@ struct solver::imp {
assert_abs_val_a_le_abs_var_b(a, b, false); assert_abs_val_a_le_abs_var_b(a, b, false);
explain(a, current_expl()); explain(a, current_expl());
explain(b, current_expl()); explain(b, current_expl());
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
} }
bool monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const rooted_mon& rm) { bool monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const rooted_mon& rm) {
@ -2312,11 +2310,11 @@ struct solver::imp {
} }
} }
mk_ineq(m.var(), (sign.is_pos()? llc::GT : llc ::LT), current_lemma()); mk_ineq(m.var(), (sign.is_pos()? llc::GT : llc ::LT), current_lemma());
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
} }
bool generate_simple_tangent_lemma(const rooted_mon* rm) { bool generate_simple_tangent_lemma(const rooted_mon* rm) {
add_empty_lemma_and_explanation(); add_empty_lemma();
unsigned i_mon = rm->orig_index(); unsigned i_mon = rm->orig_index();
const monomial & m = m_monomials[i_mon]; const monomial & m = m_monomials[i_mon];
const rational v = product_value(m); const rational v = product_value(m);
@ -2348,7 +2346,7 @@ struct solver::imp {
mk_ineq(sign, m.var(), llc::LT, current_lemma()); mk_ineq(sign, m.var(), llc::LT, current_lemma());
mk_ineq(sign, m.var(), llc::GE, v, current_lemma()); mk_ineq(sign, m.var(), llc::GE, v, current_lemma());
} }
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
return true; return true;
} }
@ -2390,13 +2388,12 @@ struct solver::imp {
generate_explanations_of_tang_lemma(rm, bf); generate_explanations_of_tang_lemma(rm, bf);
} }
void add_empty_lemma_and_explanation() { void add_empty_lemma() {
m_lemma_vec->push_back(lemma()); m_lemma_vec->push_back(lemma());
m_expl_vec->push_back(lp::explanation());
} }
void generate_tang_plane(const rational & a, const rational& b, lpvar jx, lpvar jy, bool below, lpvar j, const rational& j_sign) { void generate_tang_plane(const rational & a, const rational& b, lpvar jx, lpvar jy, bool below, lpvar j, const rational& j_sign) {
add_empty_lemma_and_explanation(); add_empty_lemma();
lemma& l = m_lemma_vec->back(); lemma& l = m_lemma_vec->back();
negate_relation(jx, a, l); negate_relation(jx, a, l);
negate_relation(jy, b, l); negate_relation(jy, b, l);
@ -2407,7 +2404,7 @@ struct solver::imp {
t.add_coeff_var(b, jx); t.add_coeff_var(b, jx);
t.add_coeff_var( -j_sign, j); t.add_coeff_var( -j_sign, j);
l.push_back(ineq(below? llc::LT : llc::GT, t, a*b)); l.push_back(ineq(below? llc::LT : llc::GT, t, a*b));
TRACE("nla_solver", print_lemma(l, tout);); TRACE("nla_solver", print_lemma(tout););
} }
void negate_relation(unsigned j, const rational& a, lemma& l) { void negate_relation(unsigned j, const rational& a, lemma& l) {
@ -2418,18 +2415,18 @@ 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.back(), tout);); TRACE("nla_solver", print_ineq(l.ineqs().back(), 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) {
add_empty_lemma_and_explanation(); add_empty_lemma();
mk_ineq(bf.m_x, llc::NE, xy.x, current_lemma()); mk_ineq(bf.m_x, llc::NE, xy.x, current_lemma());
mk_ineq(sign, j, - xy.x, bf.m_y, llc::EQ, current_lemma()); mk_ineq(sign, j, - xy.x, bf.m_y, llc::EQ, current_lemma());
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
add_empty_lemma_and_explanation(); add_empty_lemma();
mk_ineq(bf.m_y, llc::NE, xy.y, current_lemma()); mk_ineq(bf.m_y, llc::NE, xy.y, current_lemma());
mk_ineq(sign, j, - xy.y, bf.m_x, llc::EQ, current_lemma()); mk_ineq(sign, j, - xy.y, bf.m_x, llc::EQ, current_lemma());
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma(tout););
} }
// Get two planes tangent to surface z = xy, one at point a, and another at point b. // Get two planes tangent to surface z = xy, one at point a, and another at point b.
// One can show that these planes still create a cut. // One can show that these planes still create a cut.
@ -2527,9 +2524,8 @@ struct solver::imp {
lbool check(vector<lp::explanation> & expl_vec, vector<lemma>& l_vec) { lbool check(vector<lemma>& l_vec) {
TRACE("nla_solver", tout << "check of nla";); TRACE("nla_solver", tout << "check of nla";);
m_expl_vec = &expl_vec;
m_lemma_vec = &l_vec; m_lemma_vec = &l_vec;
if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE )) { if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE )) {
TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << lp_status_to_string(m_lar_solver.get_status()) << "\n";); TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << lp_status_to_string(m_lar_solver.get_status()) << "\n";);
@ -2554,7 +2550,7 @@ struct solver::imp {
bool no_lemmas_hold() const { bool no_lemmas_hold() const {
for (auto & l : * m_lemma_vec) { for (auto & l : * m_lemma_vec) {
if ((!l.empty()) && lemma_holds(l)) if (an_ineq_holds(l))
return false; return false;
} }
return true; return true;
@ -2581,11 +2577,10 @@ struct solver::imp {
} }
lbool test_check( lbool test_check(
vector<vector<ineq>>& lemma, vector<lemma>& l)
vector<lp::explanation>& exp )
{ {
m_lar_solver.set_status(lp::lp_status::OPTIMAL); m_lar_solver.set_status(lp::lp_status::OPTIMAL);
return check(exp, lemma); return check(l);
} }
}; // end of imp }; // end of imp
@ -2596,8 +2591,8 @@ unsigned solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
bool solver::need_check() { return true; } bool solver::need_check() { return true; }
lbool solver::check(vector<lp::explanation> & ex, vector<lemma>& l) { lbool solver::check(vector<lemma>& l) {
return m_imp->check(ex, l); return m_imp->check(l);
} }
void solver::push(){ void solver::push(){
@ -2734,8 +2729,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
v.push_back(lp_a);v.push_back(lp_c); v.push_back(lp_a);v.push_back(lp_c);
nla.add_monomial(lp_ac, v.size(), v.begin()); nla.add_monomial(lp_ac, v.size(), v.begin());
vector<lemma> lemma; vector<lemma> lv;
vector<lp::explanation> exp;
// set abcde = ac * bde // set abcde = ac * bde
// ac = 1 then abcde = bde, but we have abcde < bde // ac = 1 then abcde = bde, but we have abcde < bde
@ -2749,9 +2743,9 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
s.set_column_value(lp_bde, rational(16)); s.set_column_value(lp_bde, rational(16));
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lv) == l_false);
nla.m_imp->print_lemma(lemma.back(), std::cout << "expl & lemma: "); nla.m_imp->print_lemma(std::cout);
ineq i0(llc::NE, lp::lar_term(), rational(1)); ineq i0(llc::NE, lp::lar_term(), rational(1));
i0.m_term.add_var(lp_ac); i0.m_term.add_var(lp_ac);
@ -2764,7 +2758,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
bool found0 = false; bool found0 = false;
bool found1 = false; bool found1 = false;
bool found2 = false; bool found2 = false;
for (const auto& k : lemma[0]){ for (const auto& k : lv[0].ineqs()){
if (k == i0) { if (k == i0) {
found0 = true; found0 = true;
} else if (k == i1) { } else if (k == i1) {
@ -2799,7 +2793,6 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
nla.add_monomial(lp_bde, v.size(), v.begin()); nla.add_monomial(lp_bde, v.size(), v.begin());
vector<lemma> lemma; vector<lemma> lemma;
vector<lp::explanation> exp;
s.set_column_value(lp_a, rational(1)); s.set_column_value(lp_a, rational(1));
s.set_column_value(lp_b, rational(1)); s.set_column_value(lp_b, rational(1));
@ -2808,9 +2801,9 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
s.set_column_value(lp_e, rational(1)); s.set_column_value(lp_e, rational(1));
s.set_column_value(lp_bde, rational(3)); s.set_column_value(lp_bde, rational(3));
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma) == l_false);
SASSERT(lemma[0].size() == 4); SASSERT(lemma[0].size() == 4);
nla.m_imp->print_lemma(lemma.back(), std::cout << "expl & lemma: "); nla.m_imp->print_lemma(std::cout);
ineq i0(llc::NE, lp::lar_term(), rational(1)); ineq i0(llc::NE, lp::lar_term(), rational(1));
i0.m_term.add_var(lp_b); i0.m_term.add_var(lp_b);
@ -2824,7 +2817,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
bool found1 = false; bool found1 = false;
bool found2 = false; bool found2 = false;
bool found3 = false; bool found3 = false;
for (const auto& k : lemma[0]){ for (const auto& k : lemma[0].ineqs()){
if (k == i0) { if (k == i0) {
found0 = true; found0 = true;
} else if (k == i1) { } else if (k == i1) {
@ -2874,8 +2867,6 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
lp_acd, lp_acd,
lp_be); lp_be);
vector<lemma> lemma; vector<lemma> lemma;
vector<lp::explanation> exp;
// set vars // set vars
s.set_column_value(lp_a, rational(1)); s.set_column_value(lp_a, rational(1));
@ -2889,8 +2880,8 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
s.set_column_value(lp_acd, rational(1)); s.set_column_value(lp_acd, rational(1));
s.set_column_value(lp_be, rational(1)); s.set_column_value(lp_be, rational(1));
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma) == l_false);
nla.m_imp->print_lemma_and_expl(std::cout); nla.m_imp->print_lemma(std::cout);
SASSERT(lemma.size() == 1 && lemma[0].size() == 2); SASSERT(lemma.size() == 1 && lemma[0].size() == 2);
ineq i0(llc::NE, lp::lar_term(), rational(0)); ineq i0(llc::NE, lp::lar_term(), rational(0));
i0.m_term.add_var(lp_b); i0.m_term.add_var(lp_b);
@ -2899,7 +2890,7 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
bool found0 = false; bool found0 = false;
bool found1 = false; bool found1 = false;
for (const auto& k : lemma[0]){ for (const auto& k : lemma[0].ineqs()){
if (k == i0) { if (k == i0) {
found0 = true; found0 = true;
} else if (k == i1) { } else if (k == i1) {
@ -2933,18 +2924,14 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
nla.add_monomial(lp_acd, vec.size(), vec.begin()); nla.add_monomial(lp_acd, vec.size(), vec.begin());
vector<lemma> lemma; vector<lemma> lemma;
vector<lp::explanation> exp;
s.set_column_value(lp_a, rational(1)); s.set_column_value(lp_a, rational(1));
s.set_column_value(lp_c, rational(1)); s.set_column_value(lp_c, rational(1));
s.set_column_value(lp_d, rational(1)); s.set_column_value(lp_d, rational(1));
s.set_column_value(lp_acd, rational(0)); s.set_column_value(lp_acd, rational(0));
SASSERT(nla.m_imp->test_check(lemma) == l_false);
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); nla.m_imp->print_lemma(std::cout);
nla.m_imp->print_lemma_and_expl(std::cout);
ineq i0(llc::EQ, lp::lar_term(), rational(0)); ineq i0(llc::EQ, lp::lar_term(), rational(0));
i0.m_term.add_var(lp_a); i0.m_term.add_var(lp_a);
@ -2956,7 +2943,7 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
bool found1 = false; bool found1 = false;
bool found2 = false; bool found2 = false;
for (const auto& k : lemma[0]){ for (const auto& k : lemma[0].ineqs()){
if (k == i0) { if (k == i0) {
found0 = true; found0 = true;
} else if (k == i1) { } else if (k == i1) {
@ -3003,7 +2990,6 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
lp_acd, lp_acd,
lp_be); lp_be);
vector<lemma> lemma; vector<lemma> lemma;
vector<lp::explanation> exp;
// set all vars to 1 // set all vars to 1
s.set_column_value(lp_a, rational(1)); s.set_column_value(lp_a, rational(1));
@ -3022,10 +3008,10 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
s.set_column_value(lp_b, - rational(2)); s.set_column_value(lp_b, - rational(2));
// we have bde = -b, therefore d = +-1 and e = +-1 // we have bde = -b, therefore d = +-1 and e = +-1
s.set_column_value(lp_d, rational(3)); s.set_column_value(lp_d, rational(3));
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma) == l_false);
nla.m_imp->print_lemma_and_expl(std::cout); nla.m_imp->print_lemma(std::cout);
ineq i0(llc::EQ, lp::lar_term(), rational(1)); ineq i0(llc::EQ, lp::lar_term(), rational(1));
i0.m_term.add_var(lp_d); i0.m_term.add_var(lp_d);
ineq i1(llc::EQ, lp::lar_term(), -rational(1)); ineq i1(llc::EQ, lp::lar_term(), -rational(1));
@ -3033,7 +3019,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
bool found0 = false; bool found0 = false;
bool found1 = false; bool found1 = false;
for (const auto& k : lemma[0]){ for (const auto& k : lemma[0].ineqs()){
if (k == i0) { if (k == i0) {
found0 = true; found0 = true;
} else if (k == i1) { } else if (k == i1) {
@ -3093,22 +3079,20 @@ void solver::test_basic_sign_lemma() {
s.set_column_value(lp_acd, lp::impq(rational(3))); s.set_column_value(lp_acd, lp::impq(rational(3)));
vector<lemma> lemma; vector<lemma> lemma;
vector<lp::explanation> exp; SASSERT(nla.m_imp->test_check(lemma) == l_false);
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
lp::lar_term t; lp::lar_term t;
t.add_var(lp_bde); t.add_var(lp_bde);
t.add_var(lp_acd); t.add_var(lp_acd);
ineq q(llc::EQ, t, rational(0)); ineq q(llc::EQ, t, rational(0));
nla.m_imp->print_lemma_and_expl(std::cout); nla.m_imp->print_lemma(std::cout);
SASSERT(q == lemma[0].back()); SASSERT(q == lemma[0].ineqs().back());
ineq i0(llc::EQ, lp::lar_term(), rational(0)); ineq i0(llc::EQ, lp::lar_term(), rational(0));
i0.m_term.add_var(lp_bde); i0.m_term.add_var(lp_bde);
i0.m_term.add_var(lp_acd); i0.m_term.add_var(lp_acd);
bool found = false; bool found = false;
for (const auto& k : lemma[0]){ for (const auto& k : lemma[0].ineqs()){
if (k == i0) { if (k == i0) {
found = true; found = true;
} }
@ -3230,16 +3214,15 @@ void solver::test_order_lemma_params(bool var_equiv, int sign) {
+ rational(1)); + rational(1));
} }
vector<lemma> lemma; vector<lemma> lemma;
vector<lp::explanation> exp;
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma) == l_false);
SASSERT(!var_equiv || !exp.empty()); SASSERT(!var_equiv || !nla.m_imp->current_expl().empty());
// lp::lar_term t; // lp::lar_term t;
// t.add_coeff_var(lp_bde); // t.add_coeff_var(lp_bde);
// t.add_coeff_var(lp_acd); // t.add_coeff_var(lp_acd);
// ineq q(llc::EQ, t, rational(0)); // ineq q(llc::EQ, t, rational(0));
nla.m_imp->print_lemma(lemma.back(), std::cout << "lemma: "); nla.m_imp->print_lemma(std::cout);
// SASSERT(q == lemma.back()); // SASSERT(q == lemma.back());
// ineq i0(llc::EQ, lp::lar_term(), rational(0)); // ineq i0(llc::EQ, lp::lar_term(), rational(0));
// i0.m_term.add_coeff_var(lp_bde); // i0.m_term.add_coeff_var(lp_bde);
@ -3315,9 +3298,8 @@ void solver::test_monotone_lemma() {
s.set_column_value(lp_ef, s.get_column_value(lp_ij)); s.set_column_value(lp_ef, s.get_column_value(lp_ij));
vector<lemma> lemma; vector<lemma> lemma;
vector<lp::explanation> exp; SASSERT(nla.m_imp->test_check(lemma) == l_false);
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); nla.m_imp->print_lemma(std::cout);
nla.m_imp->print_lemma(lemma.back(), std::cout << "lemma: ");
} }
void solver::test_tangent_lemma_reg() { void solver::test_tangent_lemma_reg() {
@ -3351,10 +3333,8 @@ void solver::test_tangent_lemma_reg() {
s.set_column_value(lp_ab, nla.m_imp->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value s.set_column_value(lp_ab, nla.m_imp->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
vector<lemma> lemma; vector<lemma> lemma;
vector<lp::explanation> exp; SASSERT(nla.m_imp->test_check(lemma) == l_false);
nla.m_imp->print_lemma(std::cout);
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
nla.m_imp->print_lemma(lemma.back(), std::cout << "lemma: ");
} }
void solver::test_tangent_lemma_equiv() { void solver::test_tangent_lemma_equiv() {
@ -3397,10 +3377,9 @@ void solver::test_tangent_lemma_equiv() {
s.set_column_value(lp_ab, nla.m_imp->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value s.set_column_value(lp_ab, nla.m_imp->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
vector<lemma> lemma; vector<lemma> lemma;
vector<lp::explanation> exp;
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma) == l_false);
nla.m_imp->print_lemma(lemma.back(), std::cout << "lemma: "); nla.m_imp->print_lemma(std::cout);
} }

15
src/util/lp/nla_solver.h
View file

@ -47,7 +47,18 @@ struct ineq {
}; };
typedef vector<ineq> lemma; class lemma {
vector<ineq> m_ineqs;
lp::explanation m_expl;
public:
void push_back(const ineq& i) { m_ineqs.push_back(i);}
size_t size() const { return m_ineqs.size() + m_expl.size(); }
const vector<ineq>& ineqs() const { return m_ineqs; }
vector<ineq>& ineqs() { return m_ineqs; }
lp::explanation& expl() { return m_expl; }
const lp::explanation& expl() const { return m_expl; }
};
typedef vector<monomial> polynomial; typedef vector<monomial> polynomial;
// nonlinear integer incremental linear solver // nonlinear integer incremental linear solver
class solver { class solver {
@ -62,7 +73,7 @@ public:
void push(); void push();
void pop(unsigned scopes); void pop(unsigned scopes);
bool need_check(); bool need_check();
lbool check(vector<lp::explanation>&, vector<lemma>&); lbool check(vector<lemma>&);
static void test_factorization(); static void test_factorization();
static void test_basic_sign_lemma(); static void test_basic_sign_lemma();
static void test_basic_lemma_for_mon_zero_from_monomial_to_factors(); static void test_basic_lemma_for_mon_zero_from_monomial_to_factors();