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

fix #4230

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-09 18:49:00 -07:00
parent f044071f5e
commit 4890c3ce31
7 changed files with 61 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/math/lp/nla_basics_lemmas.cpp
View file

@ -91,7 +91,7 @@ void basics::basic_sign_lemma_model_based_one_mon(const monic& m, int product_si
TRACE("nla_solver_bl", tout << "zero product sign: " << pp_mon(_(), m)<< "\n"; ); TRACE("nla_solver_bl", tout << "zero product sign: " << pp_mon(_(), m)<< "\n"; );
generate_zero_lemmas(m); generate_zero_lemmas(m);
} else { } else {
new_lemma lemma(c()); new_lemma lemma(c(), __FUNCTION__);
for(lpvar j: m.vars()) { for(lpvar j: m.vars()) {
negate_strict_sign(j); negate_strict_sign(j);
} }
@ -157,7 +157,7 @@ bool basics::basic_sign_lemma(bool derived) {
// the value of the i-th monic has to be equal to the value of the k-th monic modulo sign // the value of the i-th monic has to be equal to the value of the k-th monic modulo sign
// but it is not the case in the model // but it is not the case in the model
void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& sign) { void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& sign) {
new_lemma lemma(c()); new_lemma lemma(c(), "sign lemma");
TRACE("nla_solver", TRACE("nla_solver",
tout << "m = " << pp_mon_with_vars(_(), m); tout << "m = " << pp_mon_with_vars(_(), m);
tout << "n = " << pp_mon_with_vars(_(), n); tout << "n = " << pp_mon_with_vars(_(), n);
@ -184,14 +184,14 @@ lpvar basics::find_best_zero(const monic& m, unsigned_vector & fixed_zeros) cons
return zero_j; return zero_j;
} }
void basics::add_trival_zero_lemma(lpvar zero_j, const monic& m) { void basics::add_trival_zero_lemma(lpvar zero_j, const monic& m) {
new_lemma lemma(c()); new_lemma lemma(c(), "x = 0 or x != 0");
c().mk_ineq(zero_j, llc::NE); c().mk_ineq(zero_j, llc::NE);
c().mk_ineq(m.var(), llc::EQ); c().mk_ineq(m.var(), llc::EQ);
} }
void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj) { void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj) {
TRACE("nla_solver_bl", tout << "sign_of_zj = " << sign_of_zj << "\n";); TRACE("nla_solver_bl", tout << "sign_of_zj = " << sign_of_zj << "\n";);
// we know all the signs // we know all the signs
new_lemma lemma(c()); new_lemma lemma(c(), "strict case 0");
c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT)); c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT));
for (unsigned j : m.vars()){ for (unsigned j : m.vars()){
if (j != zero_j) { if (j != zero_j) {
@ -201,7 +201,7 @@ void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, in
negate_strict_sign(m.var()); negate_strict_sign(m.var());
} }
void basics::add_fixed_zero_lemma(const monic& m, lpvar j) { void basics::add_fixed_zero_lemma(const monic& m, lpvar j) {
new_lemma lemma(c()); new_lemma lemma(c(), "fixed zero");
c().explain_fixed_var(j); c().explain_fixed_var(j);
c().mk_ineq(m.var(), llc::EQ); c().mk_ineq(m.var(), llc::EQ);
} }
@ -229,7 +229,7 @@ bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) {
return true; return true;
#if 0 #if 0
TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout););
new_lemma lemma(c()); new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0");
c().explain_fixed_var(var(rm)); c().explain_fixed_var(var(rm));
std::unordered_set<lpvar> processed; std::unordered_set<lpvar> processed;
for (auto j : f) { for (auto j : f) {
@ -247,7 +247,7 @@ bool basics::basic_lemma(bool derived) {
if (derived) if (derived)
return false; return false;
const auto& mon_inds_to_ref = c().m_to_refine; const auto& mon_inds_to_ref = c().m_to_refine;
TRACE("nla_solver", tout << "mon_inds_to_ref = "; print_vector(mon_inds_to_ref, tout);); TRACE("nla_solver", tout << "mon_inds_to_ref = "; print_vector(mon_inds_to_ref, tout) << "\n";);
unsigned start = c().random(); unsigned start = c().random();
unsigned sz = mon_inds_to_ref.size(); unsigned sz = mon_inds_to_ref.size();
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
@ -309,7 +309,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori
if (zero_j == null_lpvar) { if (zero_j == null_lpvar) {
return false; return false;
} }
new_lemma lemma(c()); new_lemma lemma(c(), "x = 0 or y = 0 -> xy = 0");
c().explain_fixed_var(zero_j); c().explain_fixed_var(zero_j);
c().explain_var_separated_from_zero(var(rm)); c().explain_var_separated_from_zero(var(rm));
explain(rm); explain(rm);
@ -357,7 +357,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm
return false; return false;
} }
new_lemma lemma(c()); new_lemma lemma(c(), "|xa| = |x| & x != 0 -> |a| = 1");
// mon_var = 0 // mon_var = 0
if (mon_var_is_sep_from_zero) if (mon_var_is_sep_from_zero)
c().explain_var_separated_from_zero(mon_var); c().explain_var_separated_from_zero(mon_var);
@ -418,7 +418,7 @@ bool basics::proportion_lemma_derived(const monic& rm, const factorization& fact
} }
// if there are no zero factors then |m| >= |m[factor_index]| // if there are no zero factors then |m| >= |m[factor_index]|
void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) {
new_lemma lemma(c()); new_lemma lemma(c(), "generate_pl_on_mon");
unsigned mon_var = m.var(); unsigned mon_var = m.var();
rational mv = val(mon_var); rational mv = val(mon_var);
rational sm = rational(nla::rat_sign(mv)); rational sm = rational(nla::rat_sign(mv));
@ -448,7 +448,7 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind
generate_pl_on_mon(m, factor_index); generate_pl_on_mon(m, factor_index);
return; return;
} }
new_lemma lemma(c()); new_lemma lemma(c(), "generate_pl");
int fi = 0; int fi = 0;
rational mv = var_val(m); rational mv = var_val(m);
rational sm = rational(nla::rat_sign(mv)); rational sm = rational(nla::rat_sign(mv));
@ -496,7 +496,7 @@ bool basics::factorization_has_real(const factorization& f) const {
void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) { void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) {
TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout););
SASSERT(var_val(rm).is_zero()&& ! c().rm_check(rm)); SASSERT(var_val(rm).is_zero()&& ! c().rm_check(rm));
new_lemma lemma(c()); new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0");
if (!is_separated_from_zero(f)) { if (!is_separated_from_zero(f)) {
c().mk_ineq(var(rm), llc::NE); c().mk_ineq(var(rm), llc::NE);
for (auto j : f) { for (auto j : f) {
@ -552,8 +552,10 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo
if (jl == null_lpvar) if (jl == null_lpvar)
return false; return false;
lpvar not_one_j = null_lpvar; lpvar not_one_j = null_lpvar;
unsigned num_occs = 0;
for (auto j : m.vars() ) { for (auto j : m.vars() ) {
if (j == jl) { if (j == jl) {
++num_occs;
continue; continue;
} }
if (abs(val(j)) != rational(1)) { if (abs(val(j)) != rational(1)) {
@ -562,11 +564,14 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo
} }
} }
if (num_occs > 1)
return false;
if (not_one_j == null_lpvar) { if (not_one_j == null_lpvar) {
return false; return false;
} }
new_lemma lemma(c()); new_lemma lemma(c(), __FUNCTION__);
// mon_var = 0 // mon_var = 0
c().mk_ineq(mon_var, llc::EQ); c().mk_ineq(mon_var, llc::EQ);
@ -614,7 +619,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co
} }
} }
new_lemma lemma(c()); new_lemma lemma(c(), __FUNCTION__);
for (auto j : m.vars()){ for (auto j : m.vars()){
if (not_one == j) continue; if (not_one == j) continue;
c().mk_ineq(j, llc::NE, val(j)); c().mk_ineq(j, llc::NE, val(j));
@ -666,7 +671,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic
return false; return false;
} }
new_lemma lemma(c()); new_lemma lemma(c(), __FUNCTION__);
// mon_var = 0 // mon_var = 0
c().mk_ineq(mon_var, llc::EQ); c().mk_ineq(mon_var, llc::EQ);
@ -748,7 +753,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const
TRACE("nla_solver_bl", tout << "not_one = " << not_one << "\n";); TRACE("nla_solver_bl", tout << "not_one = " << not_one << "\n";);
new_lemma lemma(c()); new_lemma lemma(c(), __FUNCTION__);
for (auto j : f) { for (auto j : f) {
lpvar var_j = var(j); lpvar var_j = var(j);
@ -780,7 +785,7 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f)
} }
if (zero_j == null_lpvar) { return; } if (zero_j == null_lpvar) { return; }
new_lemma lemma(c()); new_lemma lemma(c(), __FUNCTION__);
c().mk_ineq(zero_j, llc::NE); c().mk_ineq(zero_j, llc::NE);
c().mk_ineq(f.mon().var(), llc::EQ); c().mk_ineq(f.mon().var(), llc::EQ);
} }

30
src/math/lp/nla_core.cpp
View file

@ -1233,13 +1233,13 @@ rational core::val(const factorization& f) const {
return r; return r;
} }
new_lemma::new_lemma(core& c):c(c) { new_lemma::new_lemma(core& c, char const* name):name(name), c(c) {
c.m_lemma_vec->push_back(lemma()); c.m_lemma_vec->push_back(lemma());
} }
new_lemma::~new_lemma() { new_lemma::~new_lemma() {
// code for checking lemma can be added here // code for checking lemma can be added here
TRACE("nla_solver", tout << *this; ); TRACE("nla_solver", tout << name << "\n" << *this; );
} }
lemma& new_lemma::operator()() { lemma& new_lemma::operator()() {
@ -1247,7 +1247,29 @@ lemma& new_lemma::operator()() {
} }
std::ostream& new_lemma::display(std::ostream & out) const { std::ostream& new_lemma::display(std::ostream & out) const {
return c.print_specific_lemma(c.current_lemma(), out); auto const& lemma = c.current_lemma();
for (auto &p : lemma.expl()) {
out << "(" << p.second << ") ";
c.m_lar_solver.constraints().display(out, [this](lpvar j) { return c.var_str(j);}, p.second);
}
out << " ==> ";
if (lemma.ineqs().empty()) {
out << "false";
}
else {
bool first = true;
for (auto & in : lemma.ineqs()) {
if (first) first = false; else out << " or ";
c.print_ineq(in, out);
}
}
out << "\n";
for (lpvar j : c.collect_vars(lemma)) {
c.print_var(j, out);
}
return out;
} }
void core::negate_relation(unsigned j, const rational& a) { void core::negate_relation(unsigned j, const rational& a) {
@ -1674,7 +1696,7 @@ bool core::check_pdd_eq(const dd::solver::equation* e) {
return false; return false;
eval.get_interval<dd::w_dep::with_deps>(e->poly(), i_wd); eval.get_interval<dd::w_dep::with_deps>(e->poly(), i_wd);
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) { std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
new_lemma lemma(*this); new_lemma lemma(*this, "pdd");
current_expl().add(e); current_expl().add(e);
}; };
if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) { if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {

3
src/math/lp/nla_core.h
View file

@ -82,9 +82,10 @@ class core;
// correctness of the lemma can be checked at this point. // correctness of the lemma can be checked at this point.
// //
class new_lemma { class new_lemma {
char const* name;
core& c; core& c;
public: public:
new_lemma(core& c); new_lemma(core& c, char const* name);
~new_lemma(); ~new_lemma();
lemma& operator()(); lemma& operator()();
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;

2
src/math/lp/nla_intervals.cpp
View file

@ -84,7 +84,7 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
m_core->lp_settings().stats().m_cross_nested_forms++; m_core->lp_settings().stats().m_cross_nested_forms++;
scoped_dep_interval i(get_dep_intervals()); scoped_dep_interval i(get_dep_intervals());
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) { std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
new_lemma lemma(*m_core); new_lemma lemma(*m_core, "check_nex");
m_core->current_expl().add(e); m_core->current_expl().add(e);
}; };
if (!interval_of_expr<e_with_deps::without_deps>(n, 1, i, f)) { if (!interval_of_expr<e_with_deps::without_deps>(n, 1, i, f)) {

4
src/math/lp/nla_monotone_lemmas.cpp
View file

@ -50,7 +50,7 @@ void monotone::monotonicity_lemma(monic const& m) {
void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) { void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) {
TRACE("nla_solver", tout << "prod_val = " << prod_val << "\n"; TRACE("nla_solver", tout << "prod_val = " << prod_val << "\n";
tout << "m = "; c().print_monic_with_vars(m, tout);); tout << "m = "; c().print_monic_with_vars(m, tout););
new_lemma lemma(c()); new_lemma lemma(c(), __FUNCTION__);
for (lpvar j : m.vars()) { for (lpvar j : m.vars()) {
c().add_abs_bound(j, llc::GT); c().add_abs_bound(j, llc::GT);
} }
@ -66,7 +66,7 @@ void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) {
\/_i |m[i]| < |val(m[i])} or |m| >= |product_i val(m[i])| \/_i |m[i]| < |val(m[i])} or |m| >= |product_i val(m[i])|
*/ */
void monotone::monotonicity_lemma_lt(const monic& m, const rational& prod_val) { void monotone::monotonicity_lemma_lt(const monic& m, const rational& prod_val) {
new_lemma lemma(c()); new_lemma lemma(c(), __FUNCTION__);
for (lpvar j : m.vars()) { for (lpvar j : m.vars()) {
c().add_abs_bound(j, llc::LT); c().add_abs_bound(j, llc::LT);
} }

10
src/math/lp/nla_order_lemmas.cpp
View file

@ -92,7 +92,7 @@ void order::order_lemma_on_binomial(const monic& ac) {
void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) { void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) {
SASSERT(!_().mon_has_zero(xy.vars())); SASSERT(!_().mon_has_zero(xy.vars()));
int sy = rat_sign(val(y)); int sy = rat_sign(val(y));
new_lemma lemma(c()); new_lemma lemma(c(), __FUNCTION__);
mk_ineq(y, sy == 1 ? llc::LE : llc::GE); // negate sy mk_ineq(y, sy == 1 ? llc::LE : llc::GE); // negate sy
mk_ineq(x, sy*sign == 1 ? llc::GT : llc::LT , val(x)); mk_ineq(x, sy*sign == 1 ? llc::GT : llc::LT , val(x));
mk_ineq(xy.var(), - val(x), y, sign == 1 ? llc::LE : llc::GE); mk_ineq(xy.var(), - val(x), y, sign == 1 ? llc::LE : llc::GE);
@ -174,7 +174,7 @@ void order::generate_mon_ol(const monic& ac,
SASSERT(ab_cmp != llc::LT || (var_val(ac) >= var_val(bd) && val(a)*c_sign < val(b)*d_sign)); SASSERT(ab_cmp != llc::LT || (var_val(ac) >= var_val(bd) && val(a)*c_sign < val(b)*d_sign));
SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign)); SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign));
new_lemma lemma(_()); new_lemma lemma(_(), __FUNCTION__);
mk_ineq(c_sign, c, llc::LE); mk_ineq(c_sign, c, llc::LE);
explain(c); // this explains c == +- d explain(c); // this explains c == +- d
mk_ineq(c_sign, a, -d_sign * b.rat_sign(), b.var(), negate(ab_cmp)); mk_ineq(c_sign, a, -d_sign * b.rat_sign(), b.var(), negate(ab_cmp));
@ -223,7 +223,7 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab
if (mv != fv) { if (mv != fv) {
bool gt = mv > fv; bool gt = mv > fv;
for (unsigned j = 0, k = 1; j < 2; j++, k--) { for (unsigned j = 0, k = 1; j < 2; j++, k--) {
new_lemma lemma(_()); new_lemma lemma(_(), __FUNCTION__);
order_lemma_on_ab(lemma, m, rsign, var(ab[k]), var(ab[j]), gt); order_lemma_on_ab(lemma, m, rsign, var(ab[k]), var(ab[j]), gt);
explain(ab); explain(ab);
explain(m); explain(m);
@ -261,7 +261,7 @@ void order::generate_ol_eq(const monic& ac,
const monic& bc, const monic& bc,
const factor& b) { const factor& b) {
new_lemma lemma(_()); new_lemma lemma(_(), __FUNCTION__);
#if 0 #if 0
IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac
<< " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" << " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"
@ -287,7 +287,7 @@ void order::generate_ol(const monic& ac,
const monic& bc, const monic& bc,
const factor& b) { const factor& b) {
new_lemma lemma(_()); new_lemma lemma(_(), __FUNCTION__);
#if 0 #if 0
IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac
<< " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" << " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"

6
src/math/lp/nla_tangent_lemmas.cpp
View file

@ -74,7 +74,7 @@ struct imp {
void generate_tang_plane(const point & pl) { void generate_tang_plane(const point & pl) {
new_lemma lemma(c()); new_lemma lemma(c(), "generate tangent plane");
c().negate_relation(m_jx, m_x.rat_sign()*pl.x); c().negate_relation(m_jx, m_x.rat_sign()*pl.x);
c().negate_relation(m_jy, m_y.rat_sign()*pl.y); c().negate_relation(m_jy, m_y.rat_sign()*pl.y);
#if Z3DEBUG #if Z3DEBUG
@ -95,13 +95,13 @@ struct imp {
void generate_two_tang_lines() { void generate_two_tang_lines() {
{ {
new_lemma lemma(c()); new_lemma lemma(c(), "two tangent planes 1");
// Should be v = val(m_x)*val(m_y), and val(factor) = factor.rat_sign()*var(factor.var()) // Should be v = val(m_x)*val(m_y), and val(factor) = factor.rat_sign()*var(factor.var())
c().mk_ineq(m_jx, llc::NE, c().val(m_jx)); c().mk_ineq(m_jx, llc::NE, c().val(m_jx));
c().mk_ineq(m_j, - m_y.rat_sign() * m_xy.x, m_jy, llc::EQ); c().mk_ineq(m_j, - m_y.rat_sign() * m_xy.x, m_jy, llc::EQ);
} }
{ {
new_lemma lemma(c()); new_lemma lemma(c(), "two tangent planes 2");
c().mk_ineq(m_jy, llc::NE, c().val(m_jy)); c().mk_ineq(m_jy, llc::NE, c().val(m_jy));
c().mk_ineq(m_j, - m_x.rat_sign() * m_xy.y, m_jx, llc::EQ); c().mk_ineq(m_j, - m_x.rat_sign() * m_xy.y, m_jx, llc::EQ);
} }