From fdc87f286f83ea0be6cb90663f3f9f4393c04077 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 May 2020 17:40:02 -0700 Subject: [PATCH] na (#4254) * remove level of indirection for context and ast_manager in smt_theory Signed-off-by: Nikolaj Bjorner * add request by #4252 Signed-off-by: Nikolaj Bjorner * move to def Signed-off-by: Nikolaj Bjorner * int Signed-off-by: Nikolaj Bjorner * fix #4251 Signed-off-by: Nikolaj Bjorner * fix #4255 * fix #4257 * add code to debug #4246 * restore new solver as default * na Signed-off-by: Nikolaj Bjorner * fix #4246 Signed-off-by: Nikolaj Bjorner --- src/ackermannization/ackr_helper.h | 12 +++ src/ackermannization/lackr.cpp | 4 + src/ackermannization/lackr.h | 1 + src/math/lp/nla_basics_lemmas.cpp | 147 +++++++++++++-------------- src/math/lp/nla_common.cpp | 1 - src/math/lp/nla_common.h | 1 - src/math/lp/nla_core.cpp | 119 +++++++++++----------- src/math/lp/nla_core.h | 70 +++++++++---- src/math/lp/nla_intervals.cpp | 6 +- src/math/lp/nla_monotone_lemmas.cpp | 6 +- src/math/lp/nla_order_lemmas.cpp | 29 +++--- src/math/lp/nla_order_lemmas.h | 7 +- src/math/lp/nla_tangent_lemmas.cpp | 23 +++-- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/smt_consequences.cpp | 33 +++--- src/smt/smt_context.h | 2 +- src/smt/theory_lra.cpp | 14 +-- src/solver/solver2tactic.cpp | 23 ++--- 18 files changed, 269 insertions(+), 231 deletions(-) diff --git a/src/ackermannization/ackr_helper.h b/src/ackermannization/ackr_helper.h index 1bfa0d6ba..5512b9d47 100644 --- a/src/ackermannization/ackr_helper.h +++ b/src/ackermannization/ackr_helper.h @@ -83,6 +83,18 @@ public: sels.erase(s); } } + + void prune_non_funs(fun2terms_map& f2t, ast_mark& non_funs) { + ptr_vector to_delete; + for (auto& kv : f2t) { + if (non_funs.is_marked(kv.m_key)) { + to_delete.push_back(kv.m_key); + dealloc(kv.m_value); + } + } + for (func_decl * f : to_delete) + f2t.erase(f); + } inline bv_util& bvutil() { return m_bvutil; } diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index e351da9c9..1f50c2c9e 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -271,6 +271,7 @@ lbool lackr::lazy() { bool lackr::collect_terms() { ptr_vector stack = m_formulas; expr_mark visited; + func_decl* f; while (!stack.empty()) { expr * curr = stack.back(); @@ -291,6 +292,8 @@ bool lackr::collect_terms() { m_ackr_helper.mark_non_select(a, m_non_select); add_term(a); } + if (m_autil.is_as_array(curr, f)) + m_non_funs.mark(f, true); break; } case AST_QUANTIFIER: @@ -302,6 +305,7 @@ bool lackr::collect_terms() { } m_ackr_helper.prune_non_select(m_sel2terms, m_non_select); + m_ackr_helper.prune_non_funs(m_fun2terms, m_non_funs); return true; } diff --git a/src/ackermannization/lackr.h b/src/ackermannization/lackr.h index e559b5c77..51a743fc6 100644 --- a/src/ackermannization/lackr.h +++ b/src/ackermannization/lackr.h @@ -94,6 +94,7 @@ class lackr { model_ref m_model; bool m_eager; expr_mark m_non_select; + ast_mark m_non_funs; lackr_stats& m_st; bool m_is_init; diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 567258b81..bcfcdfce9 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -91,12 +91,11 @@ 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"; ); generate_zero_lemmas(m); } else { - add_lemma(); + new_lemma lemma(c()); for(lpvar j: m.vars()) { negate_strict_sign(j); } c().mk_ineq(m.var(), product_sign == 1? llc::GT : llc::LT); - TRACE("nla_solver", c().print_lemma(tout); tout << "\n";); } } @@ -158,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 // but it is not the case in the model void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& sign) { - add_lemma(); + new_lemma lemma(c()); TRACE("nla_solver", tout << "m = " << pp_mon_with_vars(_(), m); tout << "n = " << pp_mon_with_vars(_(), n); @@ -168,12 +167,11 @@ void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& TRACE("nla_solver", tout << "m exp = "; _().print_explanation(_().current_expl(), tout);); explain(n); TRACE("nla_solver", tout << "n exp = "; _().print_explanation(_().current_expl(), tout);); - TRACE("nla_solver", c().print_lemma(tout);); } // try to find a variable j such that val(j) = 0 // and the bounds on j contain 0 as an inner point lpvar basics::find_best_zero(const monic& m, unsigned_vector & fixed_zeros) const { - lpvar zero_j = -1; + lpvar zero_j = null_lpvar; for (unsigned j : m.vars()){ if (val(j).is_zero()){ if (c().var_is_fixed_to_zero(j)) @@ -186,15 +184,14 @@ lpvar basics::find_best_zero(const monic& m, unsigned_vector & fixed_zeros) cons return zero_j; } void basics::add_trival_zero_lemma(lpvar zero_j, const monic& m) { - add_lemma(); + new_lemma lemma(c()); c().mk_ineq(zero_j, llc::NE); c().mk_ineq(m.var(), llc::EQ); - TRACE("nla_solver", c().print_lemma(tout);); } 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";); // we know all the signs - add_lemma(); + new_lemma lemma(c()); c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT)); for (unsigned j : m.vars()){ if (j != zero_j) { @@ -202,13 +199,11 @@ void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, in } } negate_strict_sign(m.var()); - TRACE("nla_solver", c().print_lemma(tout);); } void basics::add_fixed_zero_lemma(const monic& m, lpvar j) { - add_lemma(); + new_lemma lemma(c()); c().explain_fixed_var(j); c().mk_ineq(m.var(), llc::EQ); - TRACE("nla_solver", c().print_lemma(tout);); } void basics::negate_strict_sign(lpvar j) { TRACE("nla_solver_details", tout << pp_var(c(), j) << "\n";); @@ -234,7 +229,7 @@ bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) { return true; #if 0 TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); - add_lemma(); + new_lemma lemma(c()); c().explain_fixed_var(var(rm)); std::unordered_set processed; for (auto j : f) { @@ -242,7 +237,6 @@ bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) { c().mk_ineq(var(j), llc::EQ); } explain(rm); - TRACE("nla_solver", c().print_lemma(tout);); return true; #endif } @@ -304,7 +298,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); if (! c().var_is_separated_from_zero(var(rm))) return false; - int zero_j = -1; + lpvar zero_j = null_lpvar; for (auto j : f) { if ( c().var_is_fixed_to_zero(var(j))) { zero_j = var(j); @@ -312,14 +306,13 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori } } - if (zero_j == -1) { + if (zero_j == null_lpvar) { return false; } - add_lemma(); + new_lemma lemma(c()); c().explain_fixed_var(zero_j); c().explain_var_separated_from_zero(var(rm)); explain(rm); - TRACE("nla_solver", c().print_lemma(tout);); return true; } // use the fact that @@ -337,7 +330,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm return false; } bool mon_var_is_sep_from_zero = c().var_is_separated_from_zero(mon_var); - lpvar jl = -1; + lpvar jl = null_lpvar; for (auto fc : f ) { lpvar j = var(fc); if (abs(val(j)) == abs_mv && c().vars_are_equiv(j, mon_var) && @@ -346,10 +339,10 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm break; } } - if (jl == static_cast(-1)) + if (jl == null_lpvar) return false; - lpvar not_one_j = -1; + lpvar not_one_j = null_lpvar; for (auto j : f ) { if (var(j) == jl) { continue; @@ -360,11 +353,11 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm } } - if (not_one_j == static_cast(-1)) { + if (not_one_j == null_lpvar) { return false; } - add_lemma(); + new_lemma lemma(c()); // mon_var = 0 if (mon_var_is_sep_from_zero) c().explain_var_separated_from_zero(mon_var); @@ -379,7 +372,6 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm // not_one_j = -1 c().mk_ineq(not_one_j, llc::EQ, -rational(1)); explain(rm); - TRACE("nla_solver", c().print_lemma(tout); ); return true; } @@ -426,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]| void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { - add_lemma(); + new_lemma lemma(c()); unsigned mon_var = m.var(); rational mv = val(mon_var); rational sm = rational(nla::rat_sign(mv)); @@ -443,7 +435,6 @@ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { c().mk_ineq(sm, mon_var, -sj, j, llc::GE ); } } - TRACE("nla_solver", c().print_lemma(tout); ); } // none of the factors is zero and the product is not zero @@ -451,13 +442,13 @@ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { void basics::generate_pl(const monic& m, const factorization& fc, int factor_index) { TRACE("nla_solver", tout << "factor_index = " << factor_index << ", m = " << pp_mon(c(), m); - tout << ", fc = "; c().print_factorization(fc, tout); + tout << ", fc = " << c().pp(fc); tout << "orig mon = "; c().print_monic(c().emons()[m.var()], tout);); if (fc.is_mon()) { generate_pl_on_mon(m, factor_index); return; } - add_lemma(); + new_lemma lemma(c()); int fi = 0; rational mv = var_val(m); rational sm = rational(nla::rat_sign(mv)); @@ -479,7 +470,6 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind explain(fc); explain(m); } - TRACE("nla_solver", c().print_lemma(tout); ); } bool basics::is_separated_from_zero(const factorization& f) const { @@ -506,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) { TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); SASSERT(var_val(rm).is_zero()&& ! c().rm_check(rm)); - add_lemma(); + new_lemma lemma(c()); if (!is_separated_from_zero(f)) { c().mk_ineq(var(rm), llc::NE); for (auto j : f) { @@ -519,7 +509,6 @@ void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factori } } explain(f); - TRACE("nla_solver", c().print_lemma(tout);); } void basics::basic_lemma_for_mon_model_based(const monic& rm) { @@ -553,16 +542,16 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo if (abs_mv == rational::zero()) { return false; } - lpvar jl = -1; + lpvar jl = null_lpvar; for (auto j : m.vars() ) { if (abs(val(j)) == abs_mv) { jl = j; break; } } - if (jl == static_cast(-1)) + if (jl == null_lpvar) return false; - lpvar not_one_j = -1; + lpvar not_one_j = null_lpvar; for (auto j : m.vars() ) { if (j == jl) { continue; @@ -573,11 +562,11 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo } } - if (not_one_j == static_cast(-1)) { + if (not_one_j == null_lpvar) { return false; } - add_lemma(); + new_lemma lemma(c()); // mon_var = 0 c().mk_ineq(mon_var, llc::EQ); @@ -592,13 +581,13 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo // not_one_j = -1 c().mk_ineq(not_one_j, llc::EQ, -rational(1)); - TRACE("nla_solver", c().print_lemma(tout); ); return true; } + // use the fact // 1 * 1 ... * 1 * x * 1 ... * 1 = x bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(const monic& m) { - lpvar not_one = -1; + lpvar not_one = null_lpvar; rational sign(1); TRACE("nla_solver_bl", tout << "m = "; c().print_monic(m, tout);); for (auto j : m.vars()){ @@ -610,7 +599,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co sign = - sign; continue; } - if (not_one == static_cast(-1)) { + if (not_one == null_lpvar) { not_one = j; continue; } @@ -618,25 +607,24 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co return false; } - if (not_one + 1) { // we found the only not_one + if (not_one != null_lpvar) { // we found the only not_one if (var_val(m) == val(not_one) * sign) { TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;); return false; } } - - add_lemma(); + + new_lemma lemma(c()); for (auto j : m.vars()){ if (not_one == j) continue; c().mk_ineq(j, llc::NE, val(j)); } - if (not_one == static_cast(-1)) { + if (not_one == null_lpvar) { c().mk_ineq(m.var(), llc::EQ, sign); } else { c().mk_ineq(m.var(), -sign, not_one, llc::EQ); } - TRACE("nla_solver", c().print_lemma(tout);); return true; } @@ -654,16 +642,16 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic if (abs_mv == rational::zero()) { return false; } - lpvar jl = -1; + lpvar jl = null_lpvar; for (auto j : f ) { if (abs(val(j)) == abs_mv) { jl = var(j); break; } } - if (jl == static_cast(-1)) + if (jl == null_lpvar) return false; - lpvar not_one_j = -1; + lpvar not_one_j = null_lpvar; for (auto j : f ) { if (var(j) == jl) { continue; @@ -674,11 +662,11 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic } } - if (not_one_j == static_cast(-1)) { + if (not_one_j == null_lpvar) { return false; } - add_lemma(); + new_lemma lemma(c()); // mon_var = 0 c().mk_ineq(mon_var, llc::EQ); @@ -696,7 +684,6 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic explain(rm); explain(f); - TRACE("nla_solver", c().print_lemma(tout); ); return true; } @@ -710,14 +697,26 @@ void basics::basic_lemma_for_mon_neutral_model_based(const monic& rm, const fact basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(rm, f); } } -// use the fact -// 1 * 1 ... * 1 * x * 1 ... * 1 = x + +/** + + - m := f1*f2*.. + - f_i are factors of m + - at most one variable among f_i evaluates to something else than -1, +1. + - m = sign * f_i + - sign = sign of f_1 * .. * f_{i-1} * f_{i+1} ... = +/- 1 + - lemma: + /\_{j != i} f_j = val(f_j) => m = sign * f_i + or + /\ f_j = val(f_j) => m = sign if all factors evaluate to +/- 1 + +*/ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const monic& m, const factorization& f) { - rational sign = sign_to_rat(m.rsign()); + rational sign(1); SASSERT(m.rsign() == canonize_sign(f)); - TRACE("nla_solver_bl", tout << pp_mon_with_vars(_(), m) <<"\nf = "; c().print_factorization(f, tout); tout << "sign = " << sign << '\n'; ); - lpvar not_one = -1; - for (auto j : f){ + TRACE("nla_solver_bl", tout << pp_mon_with_vars(_(), m) <<"\nf = " << c().pp(f) << "sign = " << sign << '\n'; ); + lpvar not_one = null_lpvar; + for (auto j : f) { TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout);); auto v = val(j); if (v == rational(1)) { @@ -729,7 +728,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const continue; } - if (not_one == static_cast(-1)) { + if (not_one == null_lpvar) { not_one = var(j); continue; } @@ -738,48 +737,41 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const return false; } - if (not_one + 1) { - // we found the only not_one - if (var_val(m) == val(not_one) * sign) { - TRACE("nla_solver", tout << "the whole is equal to the factor" << std::endl;); - return false; - } - } else { + if (not_one == null_lpvar && var_val(m) == sign) { // we have +-ones only in the factorization - if (var_val(m) == sign) { - return false; - } + return false; + } + if (not_one != null_lpvar && var_val(m) == val(not_one) * sign) { + TRACE("nla_solver", tout << "the whole is equal to the factor" << std::endl;); + return false; } TRACE("nla_solver_bl", tout << "not_one = " << not_one << "\n";); - add_lemma(); + new_lemma lemma(c()); - for (auto j : f){ + for (auto j : f) { lpvar var_j = var(j); if (not_one == var_j) continue; TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout);); c().mk_ineq(var_j, llc::NE, val(var_j)); } - if (not_one == static_cast(-1)) { + if (not_one == null_lpvar) { c().mk_ineq(m.var(), llc::EQ, sign); } else { c().mk_ineq(m.var(), -sign, not_one, llc::EQ); } explain(m); explain(f); - TRACE("nla_solver", - c().print_lemma(tout); - tout << "m = " << pp_mon_with_vars(c(), m); - ); + TRACE("nla_solver", tout << "m = " << pp_mon_with_vars(c(), m);); return true; } void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f) { - TRACE("nla_solver_bl", c().print_factorization(f, tout);); - int zero_j = -1; + TRACE("nla_solver_bl", tout << c().pp(f);); + lpvar zero_j = null_lpvar; for (auto j : f) { if (val(j).is_zero()) { zero_j = var(j); @@ -787,11 +779,10 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f) } } - if (zero_j == -1) { return; } - add_lemma(); + if (zero_j == null_lpvar) { return; } + new_lemma lemma(c()); c().mk_ineq(zero_j, llc::NE); c().mk_ineq(f.mon().var(), llc::EQ); - TRACE("nla_solver", c().print_lemma(tout);); } // x = 0 or y = 0 -> xy = 0 diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 548ce80f5..ebb0a8a30 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -41,7 +41,6 @@ rational common::mul_val(monic const& m) const { return c().mul_val(m); } template lpvar common::var(T const& t) const { return c().var(t); } template lpvar common::var(factor const& t) const; template lpvar common::var(monic const& t) const; -void common::add_lemma() { c().add_lemma(); } template bool common::canonize_sign(const T& t) const { return c().canonize_sign(t); } diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index 9e40d763f..c15246915 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -63,7 +63,6 @@ struct common { bool done() const; template void explain(const T&); void explain(lpvar); - void add_lemma(); template bool canonize_sign(const T&) const; void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs); void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 65d2e009f..0b663f9be 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -208,8 +208,7 @@ std::ostream & core::print_factor(const factor& f, std::ostream& out) const { if (f.sign()) out << "- "; if (f.is_var()) { - out << "VAR, "; - print_var(f.var(), out); + out << "VAR, " << pp(f.var()); } else { out << "MON, v" << m_emons[f.var()] << " = "; print_product(m_emons[f.var()].rvars(), out); @@ -220,7 +219,7 @@ std::ostream & core::print_factor(const factor& f, std::ostream& out) const { std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out) const { if (f.is_var()) { - print_var(f.var(), out); + out << pp(f.var()); } else { out << " MON = " << pp_mon_with_vars(*this, m_emons[f.var()]); @@ -240,10 +239,7 @@ std::ostream& core::print_monic(const monic& m, std::ostream& out) const { std::ostream& core::print_bfc(const factorization& m, std::ostream& out) const { SASSERT(m.size() == 2); - out << "( x = "; - print_factor(m[0], out); - out << "* y = "; - print_factor(m[1], out); out << ")"; + out << "( x = " << pp(m[0]) << "* y = " << pp(m[1]) << ")"; return out; } @@ -260,7 +256,7 @@ std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const } std::ostream& core::print_monic_with_vars(const monic& m, std::ostream& out) const { - out << "["; print_var(m.var(), out) << "]\n"; + out << "[" << pp(m.var()) << "]\n"; out << "vars:"; print_product_with_vars(m.vars(), out) << "\n"; if (m.vars() == m.rvars()) out << "same rvars, and m.rsign = " << m.rsign() << " of course\n"; @@ -318,7 +314,7 @@ bool core::explain_lower_bound(const lp::lar_term& t, const rational& rs, lp::ex return true; } -bool core:: explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const { +bool core::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 @@ -362,7 +358,7 @@ bool core::explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& boun } // return true iff the negation of the ineq can be derived from the constraints -bool core:: explain_ineq(const lp::lar_term& t, llc cmp, const rational& rs) { +bool core::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 // removed from the lemma @@ -409,7 +405,7 @@ bool core:: explain_ineq(const lp::lar_term& t, llc cmp, const rational& rs) { if t is an octagon term -+x -+ y try to explain why the term always is equal zero */ -bool core:: explain_by_equiv(const lp::lar_term& t, lp::explanation& e) const { +bool core::explain_by_equiv(const lp::lar_term& t, lp::explanation& e) const { lpvar i,j; bool sign; if (!is_octagon_term(t, sign, i, j)) @@ -446,31 +442,31 @@ void core::mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc c mk_ineq(t, cmp, rs); } -void core:: mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs) { +void core::mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs) { mk_ineq(rational(1), j, b, k, cmp, rs); } -void core:: mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp) { +void core::mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp) { mk_ineq(j, b, k, cmp, rational::zero()); } -void core:: mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp) { +void core::mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp) { mk_ineq(a, j, b, k, cmp, rational::zero()); } -void core:: mk_ineq(const rational& a ,lpvar j, lpvar k, llc cmp, const rational& rs) { +void core::mk_ineq(const rational& a ,lpvar j, lpvar k, llc cmp, const rational& rs) { mk_ineq(a, j, rational(1), k, cmp, rs); } -void core:: mk_ineq(lpvar j, lpvar k, llc cmp, const rational& rs) { +void core::mk_ineq(lpvar j, lpvar k, llc cmp, const rational& rs) { mk_ineq(j, rational(1), k, cmp, rs); } -void core:: mk_ineq(lpvar j, llc cmp, const rational& rs) { +void core::mk_ineq(lpvar j, llc cmp, const rational& rs) { mk_ineq(rational(1), j, cmp, rs); } -void core:: mk_ineq(const rational& a, lpvar j, llc cmp, const rational& rs) { +void core::mk_ineq(const rational& a, lpvar j, llc cmp, const rational& rs) { lp::lar_term t; t.add_monomial(a, j); mk_ineq(t, cmp, rs); @@ -487,20 +483,20 @@ llc apply_minus(llc cmp) { return cmp; } -void core:: mk_ineq(const rational& a, lpvar j, llc cmp) { +void core::mk_ineq(const rational& a, lpvar j, llc cmp) { mk_ineq(a, j, cmp, rational::zero()); } -void core:: mk_ineq(lpvar j, lpvar k, llc cmp, lemma& l) { +void core::mk_ineq(lpvar j, lpvar k, llc cmp, lemma& l) { mk_ineq(rational(1), j, rational(1), k, cmp, rational::zero()); } -void core:: mk_ineq(lpvar j, llc cmp) { +void core::mk_ineq(lpvar j, llc cmp) { mk_ineq(j, cmp, rational::zero()); } // the monics should be equal by modulo sign but this is not so in the model -void core:: fill_explanation_and_lemma_sign(const monic& a, const monic & b, rational const& sign) { +void core::fill_explanation_and_lemma_sign(const monic& a, const monic & b, rational const& sign) { SASSERT(sign == 1 || sign == -1); explain(a, current_expl()); explain(b, current_expl()); @@ -524,9 +520,7 @@ svector core::reduce_monic_to_rooted(const svector & vars, rationa auto root = m_evars.find(v); s ^= root.sign(); TRACE("nla_solver_eq", - print_var(v,tout); - tout << " mapped to "; - print_var(root.var(), tout);); + tout << pp(v) << " mapped to " << pp(root.var()) << "\n";); ret.push_back(root.var()); } sign = rational(s? -1: 1); @@ -564,11 +558,11 @@ int core::vars_sign(const svector& v) { -bool core:: has_upper_bound(lpvar j) const { +bool core::has_upper_bound(lpvar j) const { return m_lar_solver.column_has_upper_bound(j); } -bool core:: has_lower_bound(lpvar j) const { +bool core::has_lower_bound(lpvar j) const { return m_lar_solver.column_has_lower_bound(j); } const rational& core::get_upper_bound(unsigned j) const { @@ -612,30 +606,29 @@ bool core::sign_contradiction(const monic& m) const { /* unsigned_vector eq_vars(lpvar j) const { - TRACE("nla_solver_eq", tout << "j = "; print_var(j, tout); tout << "eqs = "; - for(auto jj : m_evars.eq_vars(j)) { - print_var(jj, tout); + TRACE("nla_solver_eq", tout << "j = " << pp(j) << "eqs = "; + for(auto jj : m_evars.eq_vars(j)) tout << pp(jj) << " "; }); return m_evars.eq_vars(j); } */ -bool core:: var_is_fixed_to_zero(lpvar j) const { +bool core::var_is_fixed_to_zero(lpvar j) const { return m_lar_solver.column_is_fixed(j) && m_lar_solver.get_lower_bound(j) == lp::zero_of_type(); } -bool core:: var_is_fixed_to_val(lpvar j, const rational& v) const { +bool core::var_is_fixed_to_val(lpvar j, const rational& v) const { return m_lar_solver.column_is_fixed(j) && m_lar_solver.get_lower_bound(j) == lp::impq(v); } -bool core:: var_is_fixed(lpvar j) const { +bool core::var_is_fixed(lpvar j) const { return m_lar_solver.column_is_fixed(j); } -bool core:: var_is_free(lpvar j) const { +bool core::var_is_free(lpvar j) const { return m_lar_solver.column_is_free(j); } @@ -696,8 +689,7 @@ std::ostream & core::print_factorization(const factorization& f, std::ostream& o } else { for (unsigned k = 0; k < f.size(); k++ ) { - out << "("; - print_factor(f[k], out) << ")"; + out << "(" << pp(f[k]) << ")"; if (k < f.size() - 1) out << "*"; } @@ -757,15 +749,15 @@ void core::explain_fixed_var(lpvar j) { current_expl().add(m_lar_solver.get_column_lower_bound_witness(j)); } -bool core:: var_has_positive_lower_bound(lpvar j) const { +bool core::var_has_positive_lower_bound(lpvar j) const { return m_lar_solver.column_has_lower_bound(j) && m_lar_solver.get_lower_bound(j) > lp::zero_of_type(); } -bool core:: var_has_negative_upper_bound(lpvar j) const { +bool core::var_has_negative_upper_bound(lpvar j) const { return m_lar_solver.column_has_upper_bound(j) && m_lar_solver.get_upper_bound(j) < lp::zero_of_type(); } -bool core:: var_is_separated_from_zero(lpvar j) const { +bool core::var_is_separated_from_zero(lpvar j) const { return var_has_negative_upper_bound(j) || var_has_positive_lower_bound(j); @@ -806,7 +798,7 @@ bool core::has_zero_factor(const factorization& factorization) const { template -bool core:: mon_has_zero(const T& product) const { +bool core::mon_has_zero(const T& product) const { for (lpvar j: product) { if (val(j).is_zero()) return true; @@ -846,7 +838,7 @@ void core::collect_equivs() { // returns true iff the term is in a form +-x-+y. // the sign is true iff the term is x+y, -x-y. -bool core:: is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar &j) const { +bool core::is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar &j) const { if (t.size() != 2) return false; bool seen_minus = false; @@ -898,14 +890,14 @@ bool core::rm_table_is_ok() const { return true; } -bool core:: tables_are_ok() const { +bool core::tables_are_ok() const { return vars_table_is_ok() && rm_table_is_ok(); } -bool core:: var_is_a_root(lpvar j) const { return m_evars.is_root(j); } +bool core::var_is_a_root(lpvar j) const { return m_evars.is_root(j); } template -bool core:: vars_are_roots(const T& v) const { +bool core::vars_are_roots(const T& v) const { for (lpvar j: v) { if (!var_is_a_root(j)) return false; @@ -1033,7 +1025,7 @@ bool core::divide(const monic& bc, const factor& c, factor & b) const { // Dividing by bc.rvars() we get canonize_sign(bc) = canonize_sign(b)*canonize_sign(c) // Currently, canonize_sign(b) is 1, we might need to adjust it b.sign() = canonize_sign(b) ^ canonize_sign(c) ^ canonize_sign(bc); - TRACE("nla_solver", tout << "success div:"; print_factor(b, tout);); + TRACE("nla_solver", tout << "success div:" << pp(b) << "\n";); return true; } @@ -1069,20 +1061,18 @@ void core::negate_factor_relation(const rational& a_sign, const factor& a, const } std::ostream& core::print_lemma(std::ostream& out) const { - print_specific_lemma(current_lemma(), out); - return out; + return print_specific_lemma(current_lemma(), out); } -void core::print_specific_lemma(const lemma& l, std::ostream& out) const { +std::ostream& core::print_specific_lemma(const lemma& l, std::ostream& out) const { static int n = 0; - out << "lemma:" << ++n << " "; + out << "lemma:" << ++n << " "; print_ineqs(l, out); - print_explanation(l.expl(), out); - std::unordered_set vars = collect_vars(current_lemma()); - - for (lpvar j : vars) { + print_explanation(l.expl(), out); + for (lpvar j : collect_vars(current_lemma())) { print_var(j, out); } + return out; } @@ -1243,8 +1233,21 @@ rational core::val(const factorization& f) const { return r; } -void core::add_lemma() { - m_lemma_vec->push_back(lemma()); +new_lemma::new_lemma(core& c):c(c) { + c.m_lemma_vec->push_back(lemma()); +} + +new_lemma::~new_lemma() { + // code for checking lemma can be added here + TRACE("nla_solver", tout << *this; ); +} + +lemma& new_lemma::operator()() { + return c.current_lemma(); +} + +std::ostream& new_lemma::display(std::ostream & out) const { + return c.print_specific_lemma(c.current_lemma(), out); } void core::negate_relation(unsigned j, const rational& a) { @@ -1521,7 +1524,7 @@ lbool core::check(vector& l_vec) { return ret; } -bool core:: no_lemmas_hold() const { +bool core::no_lemmas_hold() const { for (auto & l : * m_lemma_vec) { if (lemma_holds(l)) { TRACE("nla_solver", print_specific_lemma(l, tout);); @@ -1671,7 +1674,7 @@ bool core::check_pdd_eq(const dd::solver::equation* e) { return false; eval.get_interval(e->poly(), i_wd); std::function f = [this](const lp::explanation& e) { - add_lemma(); + new_lemma lemma(*this); current_expl().add(e); }; if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) { @@ -1685,7 +1688,7 @@ bool core::check_pdd_eq(const dd::solver::equation* e) { void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector & q) { if (active_var_set_contains(j) || var_is_fixed(j)) return; - TRACE("grobner", tout << "j = " << j << ", "; print_var(j, tout) << "\n";); + TRACE("grobner", tout << "j = " << j << ", " << pp(j);); const auto& matrix = m_lar_solver.A_r(); insert_to_active_var_set(j); for (auto & s : matrix.m_columns[j]) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index df84eff62..a7c0ec952 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -74,7 +74,46 @@ public: bool is_conflict() const { return m_ineqs.empty() && !m_expl.empty(); } }; +class core; +// +// lemmas are created in a scope. +// when the destructor of new_lemma is invoked +// all constraints are assumed added to the lemma +// correctness of the lemma can be checked at this point. +// +class new_lemma { + core& c; +public: + new_lemma(core& c); + ~new_lemma(); + lemma& operator()(); + std::ostream& display(std::ostream& out) const; +}; + +inline std::ostream& operator<<(std::ostream& out, new_lemma const& l) { + return l.display(out); +} + +struct pp_fac { + core const& c; + factor const& f; + pp_fac(core const& c, factor const& f): c(c), f(f) {} +}; + +struct pp_var { + core const& c; + lpvar v; + pp_var(core const& c, lpvar v): c(c), v(v) {} +}; + +struct pp_factorization { + core const& c; + factorization const& f; + pp_factorization(core const& c, factorization const& f): c(c), f(f) {} +}; + class core { + friend class new_lemma; public: var_eqs m_evars; lp::lar_solver& m_lar_solver; @@ -92,8 +131,8 @@ public: private: emonics m_emons; svector m_add_buffer; - mutable lp::u_set m_active_var_set; - lp::u_set m_rows; + mutable lp::u_set m_active_var_set; + lp::u_set m_rows; public: reslimit m_reslim; @@ -161,7 +200,7 @@ public: svector sorted_rvars(const factor& f) const; bool done() const; - void add_lemma(); + // the value of the factor is equal to the value of the variable multiplied // by the canonize_sign bool canonize_sign(const factor& f) const; @@ -197,6 +236,7 @@ public: void explain_var_separated_from_zero(lpvar j); void explain_fixed_var(lpvar j); + std::ostream & print_ineq(const ineq & in, std::ostream & out) const; std::ostream & print_var(lpvar j, std::ostream & out) const; std::ostream & print_monics(std::ostream & out) const; @@ -224,8 +264,12 @@ public: void print_monic_stats(const monic& m, std::ostream& out); void print_stats(std::ostream& out); std::ostream& print_lemma(std::ostream& out) const; - - void print_specific_lemma(const lemma& l, std::ostream& out) const; + + pp_var pp(lpvar j) const { return pp_var(*this, j); } + pp_fac pp(factor const& f) const { return pp_fac(*this, f); } + pp_factorization pp(factorization const& f) const { return pp_factorization(*this, f); } + + std::ostream& print_specific_lemma(const lemma& l, std::ostream& out) const; void trace_print_ol(const monic& ac, @@ -440,23 +484,11 @@ struct pp_mon_with_vars { pp_mon_with_vars(core const& c, monic const& m): c(c), m(m) {} pp_mon_with_vars(core const& c, lpvar v): c(c), m(c.emons()[v]) {} }; + inline std::ostream& operator<<(std::ostream& out, pp_mon const& p) { return p.c.print_monic(p.m, out); } inline std::ostream& operator<<(std::ostream& out, pp_mon_with_vars const& p) { return p.c.print_monic_with_vars(p.m, out); } - -struct pp_fac { - core const& c; - factor const& f; - pp_fac(core const& c, factor const& f): c(c), f(f) {} -}; - inline std::ostream& operator<<(std::ostream& out, pp_fac const& f) { return f.c.print_factor(f.f, out); } - -struct pp_var { - core const& c; - lpvar v; - pp_var(core const& c, lpvar v): c(c), v(v) {} -}; - +inline std::ostream& operator<<(std::ostream& out, pp_factorization const& f) { return f.c.print_factorization(f.f, out); } inline std::ostream& operator<<(std::ostream& out, pp_var const& v) { return v.c.print_var(v.v, out); } } // end of namespace nla diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index a9019b7ac..751f2b342 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -84,9 +84,9 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) { m_core->lp_settings().stats().m_cross_nested_forms++; scoped_dep_interval i(get_dep_intervals()); std::function f = [this](const lp::explanation& e) { - m_core->add_lemma(); - m_core->current_expl().add(e); - }; + new_lemma lemma(*m_core); + m_core->current_expl().add(e); + }; if (!interval_of_expr(n, 1, i, f)) { // found a conflict during the interval calculation return true; diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index 05ffade3a..378afb8cb 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -27,7 +27,7 @@ monotone::monotone(core * c) : common(c) {} void monotone::monotonicity_lemma() { unsigned shift = random(); unsigned size = c().m_to_refine.size(); - for(unsigned i = 0; i < size && !done(); i++) { + for (unsigned i = 0; i < size && !done(); i++) { lpvar v = c().m_to_refine[(i + shift) % size]; monotonicity_lemma(c().emons()[v]); } @@ -50,7 +50,7 @@ void monotone::monotonicity_lemma(monic const& m) { void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) { TRACE("nla_solver", tout << "prod_val = " << prod_val << "\n"; tout << "m = "; c().print_monic_with_vars(m, tout);); - add_lemma(); + new_lemma lemma(c()); for (lpvar j : m.vars()) { 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])| */ void monotone::monotonicity_lemma_lt(const monic& m, const rational& prod_val) { - add_lemma(); + new_lemma lemma(c()); for (lpvar j : m.vars()) { c().add_abs_bound(j, llc::LT); } diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index f8e9faada..38aa8cf5e 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -92,11 +92,10 @@ 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) { SASSERT(!_().mon_has_zero(xy.vars())); int sy = rat_sign(val(y)); - add_lemma(); + new_lemma lemma(c()); 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(xy.var(), - val(x), y, sign == 1 ? llc::LE : llc::GE); - TRACE("nla_solver", print_lemma(tout);); } // We look for monics e = m.rvars()[k]*d and see if we can create an order lemma for m and e @@ -175,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::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign)); - add_lemma(); + new_lemma lemma(_()); mk_ineq(c_sign, c, llc::LE); explain(c); // this explains c == +- d mk_ineq(c_sign, a, -d_sign * b.rat_sign(), b.var(), negate(ab_cmp)); @@ -183,7 +182,6 @@ void order::generate_mon_ol(const monic& ac, explain(bd); explain(b); explain(d); - TRACE("nla_solver", print_lemma(tout);); } @@ -225,9 +223,10 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab if (mv != fv) { bool gt = mv > fv; for (unsigned j = 0, k = 1; j < 2; j++, k--) { - order_lemma_on_ab(m, rsign, var(ab[k]), var(ab[j]), gt); - explain(ab); explain(m); - TRACE("nla_solver", _().print_lemma(tout);); + new_lemma lemma(_()); + order_lemma_on_ab(lemma, m, rsign, var(ab[k]), var(ab[j]), gt); + explain(ab); + explain(m); } } for (unsigned j = 0, k = 1; j < 2; j++, k--) { @@ -262,7 +261,7 @@ void order::generate_ol_eq(const monic& ac, const monic& bc, const factor& b) { - add_lemma(); + new_lemma lemma(_()); #if 0 IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac << " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" @@ -288,7 +287,7 @@ void order::generate_ol(const monic& ac, const monic& bc, const factor& b) { - add_lemma(); + new_lemma lemma(_()); #if 0 IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac << " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" @@ -337,9 +336,8 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac, given: sign * m = ab lemma b != val(b) || sign 0 m <= a*val(b) */ -void order::order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a, lpvar b) { +void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) { SASSERT(sign * var_val(m) > val(a) * val(b)); - add_lemma(); // negate b == val(b) mk_ineq(b, llc::NE, val(b)); // ab <= val(b)a @@ -349,22 +347,21 @@ void order::order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a, given: sign * m = ab lemma b != val(b) || sign*m >= a*val(b) */ -void order::order_lemma_on_ab_lt(const monic& m, const rational& sign, lpvar a, lpvar b) { +void order::order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) { TRACE("nla_solver", tout << "sign = " << sign << ", m = "; c().print_monic(m, tout) << ", a = "; c().print_var(a, tout) << ", b = "; c().print_var(b, tout) << "\n";); SASSERT(sign * var_val(m) < val(a) * val(b)); - add_lemma(); // negate b == val(b) mk_ineq(b, llc::NE, val(b)); // ab >= val(b)a mk_ineq(sign, m.var(), -val(b), a, llc::GE); } -void order::order_lemma_on_ab(const monic& m, const rational& sign, lpvar a, lpvar b, bool gt) { +void order::order_lemma_on_ab(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b, bool gt) { if (gt) - order_lemma_on_ab_gt(m, sign, a, b); + order_lemma_on_ab_gt(lemma, m, sign, a, b); else - order_lemma_on_ab_lt(m, sign, a, b); + order_lemma_on_ab_lt(lemma, m, sign, a, b); } } diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h index 203bf9ec1..dbd579bae 100644 --- a/src/math/lp/nla_order_lemmas.h +++ b/src/math/lp/nla_order_lemmas.h @@ -23,6 +23,7 @@ namespace nla { class core; +class new_lemma; class order: common { public: order(core *c) : common(c) {} @@ -49,9 +50,9 @@ private: void order_lemma_on_factorization(const monic& rm, const factorization& ab); - void order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a, lpvar b); - void order_lemma_on_ab_lt(const monic& m, const rational& sign, lpvar a, lpvar b); - void order_lemma_on_ab(const monic& m, const rational& sign, lpvar a, lpvar b, bool gt); + void order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b); + void order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b); + void order_lemma_on_ab(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b, bool gt); void order_lemma_on_factor_binomial_explore(const monic& m, bool k); void order_lemma_on_factor_binomial_rm(const monic& ac, bool k, const monic& bd); void order_lemma_on_binomial_ac_bd(const monic& ac, bool k, const monic& bd, const factor& b, lpvar d); diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index 90b3d3b0e..3d515d7af 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -74,7 +74,7 @@ struct imp { void generate_tang_plane(const point & pl) { - c().add_lemma(); + new_lemma lemma(c()); c().negate_relation(m_jx, m_x.rat_sign()*pl.x); c().negate_relation(m_jy, m_y.rat_sign()*pl.y); #if Z3DEBUG @@ -90,18 +90,21 @@ struct imp { t.add_monomial(- m_y.rat_sign()*pl.x, m_jy); t.add_monomial(- m_x.rat_sign()*pl.y, m_jx); t.add_var(m_j); - c().mk_ineq(t, m_below? llc::GT : llc::LT, - pl.x*pl.y); + c().mk_ineq(t, m_below? llc::GT : llc::LT, - pl.x*pl.y); } void generate_two_tang_lines() { - m_tang.add_lemma(); - // 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_j, - m_y.rat_sign() * m_xy.x, m_jy, llc::EQ); - - m_tang.add_lemma(); - 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); + { + new_lemma lemma(c()); + // 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_j, - m_y.rat_sign() * m_xy.x, m_jy, llc::EQ); + } + { + new_lemma lemma(c()); + 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); + } } // Get two planes tangent to surface z = xy, one at point a, and another at point b, creating a cut void get_initial_tang_points() { diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index c31bf4d1b..5c1ac5d9d 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -41,7 +41,7 @@ def_module_params(module_name='smt', ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), - ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), + ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=2'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'), diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 782490e72..d6d9fa3d6 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -29,9 +29,10 @@ namespace smt { expr_ref context::antecedent2fml(index_set const& vars) { expr_ref_vector premises(m); for (unsigned v : vars) { - expr* e = bool_var2expr(v); - e = m_assumption2orig.find(e); - premises.push_back(get_assignment(v) != l_false ? e : m.mk_not(e)); + expr* e; + if (m_assumption2orig.find(v, e)) { + premises.push_back(get_assignment(v) != l_false ? e : m.mk_not(e)); + } } return mk_and(premises); } @@ -277,6 +278,7 @@ namespace smt { m_antecedents.insert(true_literal.var(), index_set()); pop_to_base_lvl(); expr_ref_vector vars(m), assumptions(m); + index_set _assumptions; m_var2val.reset(); m_var2orig.reset(); m_assumption2orig.reset(); @@ -310,17 +312,21 @@ namespace smt { for (expr* a : assumptions0) { if (is_uninterp_const(a)) { assumptions.push_back(a); - m_assumption2orig.insert(a, a); } else { if (!pushed) pushed = true, push(); expr_ref c(m.mk_fresh_const("a", m.get_sort(a)), m); expr_ref eq(m.mk_eq(c, a), m); assert_expr(eq); - assumptions.push_back(c); - m_assumption2orig.insert(c, a); + assumptions.push_back(c); } + expr* e = assumptions.back(); + if (!e_internalized(e)) internalize(e, false); + literal lit = get_literal(e); + _assumptions.insert(lit.var()); + m_assumption2orig.insert(lit.var(), a); } + lbool is_sat = check(assumptions.size(), assumptions.c_ptr()); if (is_sat != l_true) { TRACE("context", tout << is_sat << "\n";); @@ -333,11 +339,6 @@ namespace smt { TRACE("context", display(tout);); - index_set _assumptions; - for (expr* e : assumptions) { - if (!e_internalized(e)) internalize(e, false); - _assumptions.insert(get_literal(e).var()); - } model_ref mdl; get_model(mdl); expr_ref_vector trail(m); @@ -459,9 +460,7 @@ namespace smt { } m_antecedents.reset(); - literal_vector const& lits = assigned_literals(); - for (unsigned i = 0; i < lits.size(); ++i) { - literal lit = lits[i]; + for (literal lit : assigned_literals()) { index_set s; if (_asms.contains(lit.index())) { s.insert(lit.var()); @@ -472,10 +471,8 @@ namespace smt { m_antecedents.insert(lit.var(), s); if (_nasms.contains(lit.index())) { expr_ref_vector core(m); - index_set::iterator it = s.begin(), end = s.end(); - for (; it != end; ++it) { - core.push_back(var2expr[*it]); - } + for (auto v : s) + core.push_back(var2expr[v]); core.push_back(var2expr[lit.var()]); cores.push_back(core); min_core_size = std::min(min_core_size, core.size()); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 8ababb67e..1889b96ef 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1498,7 +1498,7 @@ namespace smt { //typedef uint_set index_set; u_map m_antecedents; obj_map m_var2orig; - obj_map m_assumption2orig; + u_map m_assumption2orig; obj_map m_var2val; void extract_fixed_consequences(literal lit, index_set const& assumptions, expr_ref_vector& conseq); void extract_fixed_consequences(unsigned& idx, index_set const& assumptions, expr_ref_vector& conseq); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 308a02750..42a437d4d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2162,7 +2162,10 @@ public: nla::lemma m_lemma; - void false_case_of_check_nla() { + void false_case_of_check_nla(const nla::lemma & l) { + m_lemma = l; //todo avoid the copy + m_explanation = l.expl(); + m_stats.m_nla_explanations += static_cast(l.expl().size()); literal_vector core; for (auto const& ineq : m_lemma.ineqs()) { bool is_lower = true, pos = true, is_eq = false; @@ -2197,10 +2200,7 @@ public: case l_false: { m_stats.m_nla_lemmas += lv.size(); for(const nla::lemma & l : lv) { - m_lemma = l; //todo avoid the copy - m_explanation = l.expl(); - m_stats.m_nla_explanations += static_cast(l.expl().size()); - false_case_of_check_nla(); + false_case_of_check_nla(l); } break; } @@ -3257,7 +3257,7 @@ public: } } - lp::explanation m_explanation; + lp::explanation m_explanation; literal_vector m_core; svector m_eqs; @@ -3324,7 +3324,7 @@ public: set_evidence(ev.second, m_core, m_eqs); } } - // SASSERT(validate_conflict()); + // SASSERT(validate_conflict(m_core, m_eqs)); dump_conflict(m_core, m_eqs); if (is_conflict) { ctx().set_conflict( diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index ffc93a21a..498b4d545 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -44,10 +44,7 @@ void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clause deps.reset(); m.linearize(d, deps); SASSERT(!deps.empty()); // d != 0, then deps must not be empty - ptr_vector::iterator it = deps.begin(); - ptr_vector::iterator end = deps.end(); - for (; it != end; ++it) { - expr * d = *it; + for (expr* d : deps) { if (is_uninterp_const(d) && m.is_bool(d)) { // no need to create a fresh boolean variable for d if (!bool2dep.contains(d)) { @@ -156,14 +153,16 @@ public: if (!m.inc()) { throw tactic_exception(Z3_CANCELED_MSG); } - model_converter_ref mc; - mc = local_solver->get_model_converter(); - mc = concat(fmc.get(), mc.get()); - in->reset(); - in->add(mc.get()); - unsigned sz = local_solver->get_num_assertions(); - for (unsigned i = 0; i < sz; ++i) { - in->assert_expr(local_solver->get_assertion(i)); + if (!in->unsat_core_enabled()) { + model_converter_ref mc; + mc = local_solver->get_model_converter(); + mc = concat(fmc.get(), mc.get()); + in->reset(); + in->add(mc.get()); + unsigned sz = local_solver->get_num_assertions(); + for (unsigned i = 0; i < sz; ++i) { + in->assert_expr(local_solver->get_assertion(i)); + } } result.push_back(in.get()); break;