From ace8fb6d95761ec35d7fd8fce6ca818b380d02ad Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 18 Dec 2018 16:22:47 -0800 Subject: [PATCH] improve printouts and diagnostics Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 277 ++++++++++++++++++++++++++++--------- src/util/lp/nla_solver.h | 10 ++ 2 files changed, 221 insertions(+), 66 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 62949c318..529b5c634 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -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& 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(-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; diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h index f9f0f42eb..edd6101a2 100644 --- a/src/util/lp/nla_solver.h +++ b/src/util/lp/nla_solver.h @@ -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 lemma;