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<func_decl> 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<expr> 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<lpvar> 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<lpvar>(-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<lpvar>(-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<lpvar>(-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<lpvar>(-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<lpvar>(-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<lpvar>(-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<lpvar>(-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<lpvar>(-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<lpvar>(-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<lpvar>(-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 <typename T> lpvar common::var(T const& t) const { return c().var(t); }
template lpvar common::var<factor>(factor const& t) const;
template lpvar common::var<monic>(monic const& t) const;
-void common::add_lemma() { c().add_lemma(); }
template <typename T> 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 <typename T> void explain(const T&);
void explain(lpvar);
- void add_lemma();
template <typename T> 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<lpvar> core::reduce_monic_to_rooted(const svector<lpvar> & 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<lpvar>& 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<lp::impq>();
}
-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<lp::impq>();
}
-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<lp::impq>();
}
-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 <typename T>
-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 <typename T>
-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<lpvar> 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<lemma>& 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<dd::w_dep::with_deps>(e->poly(), i_wd);
std::function<void (const lp::explanation&)> 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<lpvar> & 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<emonics> m_evars;
lp::lar_solver& m_lar_solver;
@@ -92,8 +131,8 @@ public:
private:
emonics m_emons;
svector<lpvar> 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<lpvar> 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<void (const lp::explanation&)> 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<e_with_deps::without_deps>(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<index_set> m_antecedents;
obj_map<expr, expr*> m_var2orig;
- obj_map<expr, expr*> m_assumption2orig;
+ u_map<expr*> m_assumption2orig;
obj_map<expr, expr*> 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<unsigned>(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<unsigned>(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<enode_pair> 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<expr>::iterator it = deps.begin();
- ptr_vector<expr>::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;