mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

na (#4254)

Browse source 
* remove level of indirection for context and ast_manager in smt_theory

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add request by #4252

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* move to def

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* int

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4251

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4255

* fix #4257

* add code to debug #4246

* restore new solver as default

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4246

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-09 17:40:02 -07:00 • committed by GitHub
parent becf423c77
commit fdc87f286f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
18 changed files with 269 additions and 231 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ackermannization/ackr_helper.h
View file

@ -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; }

4
src/ackermannization/lackr.cpp
View file

@ -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;
}

1
src/ackermannization/lackr.h
View file

@ -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;

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

@ -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

1
src/math/lp/nla_common.cpp
View file

@ -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);
}

1
src/math/lp/nla_common.h
View file

@ -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);

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

@ -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]) {

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

@ -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

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

@ -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;

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

@ -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);
}

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

@ -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);
}
}

7
src/math/lp/nla_order_lemmas.h
View file

@ -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);

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

@ -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() {

2
src/smt/params/smt_params_helper.pyg
View file

@ -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'),

33
src/smt/smt_consequences.cpp
View file

@ -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());

2
src/smt/smt_context.h
View file

@ -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);

14
src/smt/theory_lra.cpp
View file

@ -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(

23
src/solver/solver2tactic.cpp
View file

@ -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;