mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

improve printouts and diagnostics

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-18 16:22:47 -08:00 committed by Lev Nachmanson
parent 3192db64a1
commit ace8fb6d95
2 changed files with 221 additions and 66 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -25,12 +25,12 @@
#include "util/lp/factorization.h"
#include "util/lp/rooted_mons.h"
namespace nla {
struct solver::imp {
typedef lp::lconstraint_kind llc;
struct solver::imp {
typedef lp::lar_base_constraint lpcon;
//fields
vars_equivalence m_vars_equivalence;
@ -55,9 +55,45 @@ struct solver::imp {
{
}
bool compare_holds(const rational& ls, llc cmp, const rational& rs) const {
switch(cmp) {
case llc::LE: return ls <= rs;
case llc::LT: return ls < rs;
case llc::GE: return ls >= rs;
case llc::GT: return ls > rs;
case llc::EQ: return ls == rs;
case llc::NE: return ls != rs;
default: SASSERT(false);
};
return false;
}
rational value(const lp::lar_term& r) const {
rational ret(0);
for (const auto & t : r.coeffs()) {
ret += t.second * vvr(t.first);
}
return ret;
}
bool ineq_holds(const ineq& n) const {
return compare_holds(value(n.term()), n.cmp(), n.rs());
}
bool lemma_holds() const {
for(auto &i : *m_lemma) {
if (!ineq_holds(i))
return false;
}
return true;
}
rational vvr(lpvar j) const { return m_lar_solver.get_column_value_rational(j); }
rational vvr(const monomial& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
lp::impq vv(lpvar j) const { return m_lar_solver.get_column_value(j); }
lpvar var(const rooted_mon& rm) const {return m_monomials[rm.m_orig.m_i].var(); }
@ -205,8 +241,10 @@ struct solver::imp {
}
std::ostream& print_monomial(const monomial& m, std::ostream& out) const {
out << m_lar_solver.get_variable_name(m.var()) << " = ";
return print_product(m.vars(), out);
out << "( [" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << vvr(m.var()) << " = ";
print_product(m.vars(), out);
out << ")\n";
return out;
}
std::ostream& print_monomial(unsigned i, std::ostream& out) const {
@ -229,8 +267,10 @@ struct solver::imp {
}
std::ostream& print_monomial_with_vars(const monomial& m, std::ostream& out) const {
out << m_lar_solver.get_variable_name(m.var()) << " = ";
return print_product_with_vars(m, out);
out << "( [" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << vvr(m.var()) << " = ";
print_product_with_vars(m.vars(), out);
out << ")\n";
return out;
}
std::ostream& print_rooted_monomial(const rooted_mon& rm, std::ostream& out) const {
@ -258,57 +298,146 @@ struct solver::imp {
return out;
}
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, lp::lconstraint_kind cmp, const rational& rs) {
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs) {
lp::lar_term t;
t.add_coeff_var(a, j);
t.add_coeff_var(b, k);
if (t.is_empty() && rs.is_zero() &&
(cmp == lp::lconstraint_kind::LT || cmp == lp::lconstraint_kind::GT || cmp == lp::lconstraint_kind::NE))
(cmp == llc::LT || cmp == llc::GT || cmp == llc::NE))
return; // otherwise we get something like 0 < 0, which is always false and can be removed from the lemma
m_lemma->push_back(ineq(cmp, t, rs));
}
void mk_ineq(lpvar j, const rational& b, lpvar k, lp::lconstraint_kind cmp, const rational& rs) {
void mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs) {
mk_ineq(rational(1), j, b, k, cmp, rs);
}
void mk_ineq(lpvar j, const rational& b, lpvar k, lp::lconstraint_kind cmp) {
void mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp) {
mk_ineq(j, b, k, cmp, rational::zero());
}
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, lp::lconstraint_kind cmp) {
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp) {
mk_ineq(a, j, b, k, cmp, rational::zero());
}
void mk_ineq(const rational& a ,lpvar j, lpvar k, lp::lconstraint_kind cmp, const rational& rs) {
void mk_ineq(const rational& a ,lpvar j, lpvar k, llc cmp, const rational& rs) {
mk_ineq(a, j, rational(1), k, cmp, rs);
}
void mk_ineq(lpvar j, lpvar k, lp::lconstraint_kind cmp, const rational& rs) {
void mk_ineq(lpvar j, lpvar k, llc cmp, const rational& rs) {
mk_ineq(j, rational(1), k, cmp, rs);
}
void mk_ineq(lpvar j, lp::lconstraint_kind cmp, const rational& rs) {
void mk_ineq(lpvar j, llc cmp, const rational& rs) {
lp::lar_term t;
t.add_coeff_var(j);
m_lemma->push_back(ineq(cmp, t, rs));
}
void mk_ineq(const rational& a, lpvar j, lp::lconstraint_kind cmp, const rational& rs) {
void mk_ineq(const rational& a, lpvar j, llc cmp, const rational& rs) {
lp::lar_term t;
t.add_coeff_var(a, j);
m_lemma->push_back(ineq(cmp, t, rs));
}
void mk_ineq(const rational& a, lpvar j, lp::lconstraint_kind cmp) {
llc negate(llc cmp) {
switch(cmp) {
case llc::LE: return llc::GE;
case llc::LT: return llc::GT;
case llc::GE: return llc::LE;
case llc::GT: return llc::LT;
case llc::EQ: return llc::NE;
case llc::NE: return llc::EQ;
default: SASSERT(false);
};
return cmp; // not reachable
}
llc apply_minus(llc cmp) {
switch(cmp) {
case llc::LE: return llc::GE;
case llc::LT: return llc::GT;
case llc::GE: return llc::LE;
case llc::GT: return llc::LT;
default: break;
}
return cmp;
}
bool explain(const rational& a, lpvar j, llc cmp, const rational& rs) {
cmp = negate(cmp);
if (a == rational(1))
return explain(j, cmp, rs);
if (a == -rational(1))
return explain(j, apply_minus(cmp), -rs);
return false;
}
bool explain(lpvar j, llc cmp, const rational& rs) {
unsigned lc, uc; // indices for the lower and upper bounds
m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
switch(cmp) {
case llc::LE: {
if (uc + 1 == 0 || m_lar_solver.column_upper_bound(j) > rs)
return false;
m_expl->add(uc);
return true;
}
case llc::LT: {
if (uc + 1 == 0 || m_lar_solver.column_upper_bound(j) >= rs)
return false;
m_expl->add(uc);
return true;
}
case llc::GE: {
if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) < rs)
return false;
m_expl->add(lc);
return true;
}
case llc::GT: {
if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) <= rs)
return false;
m_expl->add(lc);
return true;
}
case llc::EQ:
{
if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) < rs
||
uc + 1 == 0 || m_lar_solver.column_upper_bound(j) > rs)
return false;
m_expl->add(lc);
m_expl->add(uc);
return true;
}
case llc::NE: {
if (uc + 1 && m_lar_solver.column_upper_bound(j) < rs) {
m_expl->add(uc);
return true;
}
if (lc + 1 && m_lar_solver.column_lower_bound(j) > rs) {
m_expl->add(lc);
return true;
}
return false;
};
default:
SASSERT(false);
};
SASSERT(false);
return false;
}
void mk_ineq(const rational& a, lpvar j, llc cmp) {
mk_ineq(a, j, cmp, rational::zero());
}
void mk_ineq(lpvar j, lpvar k, lp::lconstraint_kind cmp) {
void mk_ineq(lpvar j, lpvar k, llc cmp) {
mk_ineq(rational(1), j, rational(1), k, cmp, rational::zero());
}
void mk_ineq(lpvar j, lp::lconstraint_kind cmp) {
void mk_ineq(lpvar j, llc cmp) {
mk_ineq(j, cmp, rational::zero());
}
@ -323,7 +452,7 @@ struct solver::imp {
m_lar_solver.print_constraint(p.second, tout); tout << "\n";
);
SASSERT(m_lemma->size() == 0);
mk_ineq(rational(1), a.var(), -sign, b.var(), lp::lconstraint_kind::EQ, rational::zero());
mk_ineq(rational(1), a.var(), -sign, b.var(), llc::EQ, rational::zero());
TRACE("nla_solver", print_lemma(tout););
}
@ -405,12 +534,12 @@ struct solver::imp {
index_with_sign & ins = it->second.back();
if (j != ins.m_i) {
s *= ins.m_sign;
mk_ineq(j, -s, ins.m_i, lp::lconstraint_kind::NE);
mk_ineq(j, -s, ins.m_i, llc::NE);
}
it->second.pop_back();
}
mk_ineq(m_monomials[i].var(), -sign, m_monomials[k].var(), lp::lconstraint_kind::EQ);
mk_ineq(m_monomials[i].var(), -sign, m_monomials[k].var(), llc::EQ);
TRACE("nla_solver", print_lemma(tout););
}
@ -430,6 +559,12 @@ struct solver::imp {
}
bool basic_sign_lemma_on_a_bucket_of_abs_vals(const vector<rational>& abs_vals, const unsigned_vector& list){
TRACE("nla_solver",
tout << "key = ";
print_vector(abs_vals, tout);
tout << "m0 = ";
print_monomial_with_vars(m_monomials[list[0]], tout);
);
rational val = vvr(m_monomials[list[0]].var());
int sign = vars_sign(m_monomials[list[0]].vars());
if (sign == 0) {
@ -470,13 +605,13 @@ struct solver::imp {
std::ostream & print_ineq(const ineq & in, std::ostream & out) const {
m_lar_solver.print_term(in.m_term, out);
out << " " << lp::lconstraint_kind_string(in.m_cmp) << " " << in.m_rs;
out << " " << llc_string(in.m_cmp) << " " << in.m_rs;
return out;
}
std::ostream & print_var(lpvar j, std::ostream & out) const {
bool is_monomial = false;
out << j << " ";
out << "[" << j << "] = ";
for (const monomial & m : m_monomials) {
if (j == m.var()) {
is_monomial = true;
@ -489,6 +624,13 @@ struct solver::imp {
out << m_lar_solver.get_variable_name(j) << " = " << vvr(j);
out <<";";
return out;
}
std::ostream & print_monomials(std::ostream & out) const {
for (auto &m : m_monomials) {
print_monomial_with_vars(m, out);
}
return out;
}
std::ostream & print_lemma(std::ostream & out) const {
@ -559,9 +701,9 @@ struct solver::imp {
SASSERT(m_lemma->empty());
mk_ineq(var(rm), lp::lconstraint_kind::NE);
mk_ineq(var(rm), llc::NE);
for (auto j : f) {
mk_ineq(var(j), lp::lconstraint_kind::EQ);
mk_ineq(var(j), llc::EQ);
}
explain(rm);
@ -596,8 +738,8 @@ struct solver::imp {
return false;
}
mk_ineq(zero_j, lp::lconstraint_kind::NE);
mk_ineq(var(rm), lp::lconstraint_kind::EQ);
mk_ineq(zero_j, llc::NE);
mk_ineq(var(rm), llc::EQ);
explain(rm);
TRACE("nla_solver", print_lemma(tout););
@ -643,19 +785,19 @@ struct solver::imp {
}
// mon_var = 0
mk_ineq(mon_var, lp::lconstraint_kind::EQ);
mk_ineq(mon_var, llc::EQ);
// negate abs(jl) == abs()
if (vvr(jl) == - vvr(mon_var))
mk_ineq(jl, mon_var, lp::lconstraint_kind::NE);
mk_ineq(jl, mon_var, llc::NE);
else // jl == mon_var
mk_ineq(jl, -rational(1), mon_var, lp::lconstraint_kind::NE);
mk_ineq(jl, -rational(1), mon_var, llc::NE);
// not_one_j = 1
mk_ineq(not_one_j, lp::lconstraint_kind::EQ, rational(1));
mk_ineq(not_one_j, llc::EQ, rational(1));
// not_one_j = -1
mk_ineq(not_one_j, lp::lconstraint_kind::EQ, -rational(1));
mk_ineq(not_one_j, llc::EQ, -rational(1));
explain(rm);
TRACE("nla_solver", print_lemma(tout); );
return true;
@ -694,13 +836,13 @@ struct solver::imp {
for (auto j : f){
lpvar var_j = var(j);
if (not_one == var_j) continue;
mk_ineq(var_j, lp::lconstraint_kind::NE, j.is_var()? vvr(j) : flip_sign(j) * vvr(j) );
mk_ineq(var_j, llc::NE, j.is_var()? vvr(j) : flip_sign(j) * vvr(j) );
}
if (not_one == static_cast<lpvar>(-1)) {
mk_ineq(m_monomials[rm.orig_index()].var(), lp::lconstraint_kind::EQ, sign);
mk_ineq(m_monomials[rm.orig_index()].var(), llc::EQ, sign);
} else {
mk_ineq(m_monomials[rm.orig_index()].var(), -sign, not_one, lp::lconstraint_kind::EQ);
mk_ineq(m_monomials[rm.orig_index()].var(), -sign, not_one, llc::EQ);
}
TRACE("nla_solver",
tout << "rm = "; print_rooted_monomial_with_vars(rm, tout);
@ -995,16 +1137,16 @@ struct solver::imp {
auto iv = vvr(i), jv = vvr(j);
SASSERT(abs(iv) == abs(jv));
if (iv == jv) {
mk_ineq(i, -rational(1), j, lp::lconstraint_kind::NE);
mk_ineq(i, -rational(1), j, llc::NE);
} else { // iv == -jv
mk_ineq(i, j, lp::lconstraint_kind::NE);
mk_ineq(i, j, llc::NE);
}
}
void negate_factor_relation(const rational& a_sign, const factor& a, const rational& b_sign, const factor& b) {
rational a_fs = flip_sign(a);
rational b_fs = flip_sign(b);
lp::lconstraint_kind cmp = a_sign*vvr(a) < b_sign*vvr(b)? lp::lconstraint_kind::GE : lp::lconstraint_kind::LE;
llc cmp = a_sign*vvr(a) < b_sign*vvr(b)? llc::GE : llc::LE;
mk_ineq(a_fs*a_sign, var(a), - b_fs*b_sign, var(b), cmp);
}
@ -1019,8 +1161,8 @@ struct solver::imp {
const factor& b,
int d_sign,
const factor& d,
lp::lconstraint_kind ab_cmp) {
mk_ineq(rational(c_sign) * flip_sign(c), var(c), lp::lconstraint_kind::LE);
llc ab_cmp) {
mk_ineq(rational(c_sign) * flip_sign(c), var(c), llc::LE);
negate_factor_equality(c, d);
negate_factor_relation(rational(c_sign), a, rational(d_sign), b);
mk_ineq(flip_sign(ac), var(ac), -flip_sign(bd), var(bd), ab_cmp);
@ -1090,12 +1232,12 @@ struct solver::imp {
if (av < bv){
if(!(acv < bdv)) {
generate_ol(ac, a, c_sign, c, bd, b, d_sign, d, lp::lconstraint_kind::LT);
generate_ol(ac, a, c_sign, c, bd, b, d_sign, d, llc::LT);
return true;
}
} else if (av > bv){
if(!(acv > bdv)) {
generate_ol(ac, a, c_sign, c, bd, b, d_sign, d, lp::lconstraint_kind::GT);
generate_ol(ac, a, c_sign, c, bd, b, d_sign, d, llc::GT);
return true;
}
}
@ -1286,7 +1428,8 @@ struct solver::imp {
}
init_search();
for (int search_level = 0; search_level < 3; search_level++) {
lbool ret = l_undef;
for (int search_level = 0; search_level < 3 && ret == l_undef; search_level++) {
if (search_level == 0) {
if (basic_lemma()) {
return l_false;
@ -1305,8 +1448,10 @@ struct solver::imp {
}
}
}
return l_undef;
CTRACE("nla_solver", ret == l_undef, tout << "Monomials\n"; print_monomials(tout););
SASSERT(ret != l_false || ((!m_lemma->empty()) && (!lemma_holds())));
return ret;
}
void test_factorization(unsigned mon_index, unsigned number_of_factorizations) {
@ -1508,12 +1653,12 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
ineq i0(lp::lconstraint_kind::NE, lp::lar_term(), rational(1));
ineq i0(llc::NE, lp::lar_term(), rational(1));
i0.m_term.add_coeff_var(lp_ac);
ineq i1(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
ineq i1(llc::EQ, lp::lar_term(), rational(0));
i1.m_term.add_coeff_var(lp_bde);
i1.m_term.add_coeff_var(-rational(1), lp_abcde);
ineq i2(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
ineq i2(llc::EQ, lp::lar_term(), rational(0));
i2.m_term.add_coeff_var(lp_abcde);
i2.m_term.add_coeff_var(-rational(1), lp_bde);
bool found0 = false;
@ -1567,13 +1712,13 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
SASSERT(lemma.size() == 4);
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
ineq i0(lp::lconstraint_kind::NE, lp::lar_term(), rational(1));
ineq i0(llc::NE, lp::lar_term(), rational(1));
i0.m_term.add_coeff_var(lp_b);
ineq i1(lp::lconstraint_kind::NE, lp::lar_term(), rational(1));
ineq i1(llc::NE, lp::lar_term(), rational(1));
i1.m_term.add_coeff_var(lp_d);
ineq i2(lp::lconstraint_kind::NE, lp::lar_term(), rational(1));
ineq i2(llc::NE, lp::lar_term(), rational(1));
i2.m_term.add_coeff_var(lp_e);
ineq i3(lp::lconstraint_kind::EQ, lp::lar_term(), rational(1));
ineq i3(llc::EQ, lp::lar_term(), rational(1));
i3.m_term.add_coeff_var(lp_bde);
bool found0 = false;
bool found1 = false;
@ -1646,9 +1791,9 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
SASSERT(lemma.size() == 2);
ineq i0(lp::lconstraint_kind::NE, lp::lar_term(), rational(0));
ineq i0(llc::NE, lp::lar_term(), rational(0));
i0.m_term.add_coeff_var(lp_b);
ineq i1(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
ineq i1(llc::EQ, lp::lar_term(), rational(0));
i1.m_term.add_coeff_var(lp_be);
bool found0 = false;
bool found1 = false;
@ -1710,11 +1855,11 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
ineq i0(llc::EQ, lp::lar_term(), rational(0));
i0.m_term.add_coeff_var(lp_b);
ineq i1(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
ineq i1(llc::EQ, lp::lar_term(), rational(0));
i1.m_term.add_coeff_var(lp_d);
ineq i2(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
ineq i2(llc::EQ, lp::lar_term(), rational(0));
i2.m_term.add_coeff_var(lp_e);
bool found0 = false;
bool found1 = false;
@ -1787,9 +1932,9 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(1));
ineq i0(llc::EQ, lp::lar_term(), rational(1));
i0.m_term.add_coeff_var(lp_b);
ineq i1(lp::lconstraint_kind::EQ, lp::lar_term(), -rational(1));
ineq i1(llc::EQ, lp::lar_term(), -rational(1));
i1.m_term.add_coeff_var(lp_b);
bool found0 = false;
bool found1 = false;
@ -1860,11 +2005,11 @@ void solver::test_basic_sign_lemma() {
lp::lar_term t;
t.add_coeff_var(lp_bde);
t.add_coeff_var(lp_acd);
ineq q(lp::lconstraint_kind::EQ, t, rational(0));
ineq q(llc::EQ, t, rational(0));
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
SASSERT(q == lemma.back());
ineq i0(lp::lconstraint_kind::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(rational(1), lp_acd);
bool found = false;
@ -1938,8 +2083,8 @@ void solver::test_order_lemma_params(bool var_equiv, int sign) {
t.add_coeff_var(lp_k);
t.add_coeff_var(-rational(1), lp_j);
lpvar kj = s.add_term(t.coeffs_as_vector());
s.add_var_bound(kj, lp::lconstraint_kind::LE, rational(0));
s.add_var_bound(kj, lp::lconstraint_kind::GE, rational(0));
s.add_var_bound(kj, llc::LE, rational(0));
s.add_var_bound(kj, llc::GE, rational(0));
}
//create monomial (ab)(ef)
@ -1997,11 +2142,11 @@ void solver::test_order_lemma_params(bool var_equiv, int sign) {
// lp::lar_term t;
// t.add_coeff_var(lp_bde);
// t.add_coeff_var(lp_acd);
// ineq q(lp::lconstraint_kind::EQ, t, rational(0));
// ineq q(llc::EQ, t, rational(0));
nla.m_imp->print_lemma(std::cout << "lemma: ");
// SASSERT(q == lemma.back());
// ineq i0(lp::lconstraint_kind::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(rational(1), lp_acd);
// bool found = false;

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

@ -35,6 +35,16 @@ struct ineq {
bool operator==(const ineq& a) const {
return m_cmp == a.m_cmp && m_term == a.m_term && m_rs == a.m_rs;
}
const lp::lar_term& term() const {
return m_term;
};
const lp::lconstraint_kind& cmp() const {
return m_cmp;
};
const rational& rs() const {
return m_rs;
};
};
typedef vector<ineq> lemma;