mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 10:30:44 +00:00
Code Activity

rename new_lemma to lemma_builder

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-06-25 06:04:07 -07:00 • committed by Lev Nachmanson
parent 2f2289eaff
commit 5bda42e104
17 changed files with 135 additions and 115 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/lp/monomial_bounds.cpp
View file

@ -110,7 +110,7 @@ namespace nla {
dep.get_upper_dep(range, ex); dep.get_upper_dep(range, ex);
if (is_too_big(upper)) if (is_too_big(upper))
return false; return false;
new_lemma lemma(c(), "propagate value - upper bound of range is below value"); lemma_builder lemma(c(), "propagate value - upper bound of range is below value");
lemma &= ex; lemma &= ex;
lemma |= ineq(v, cmp, upper); lemma |= ineq(v, cmp, upper);
TRACE(nla_solver, dep.display(tout << c().val(v) << " > ", range) << "\n" << lemma << "\n";); TRACE(nla_solver, dep.display(tout << c().val(v) << " > ", range) << "\n" << lemma << "\n";);
@ -124,7 +124,7 @@ namespace nla {
dep.get_lower_dep(range, ex); dep.get_lower_dep(range, ex);
if (is_too_big(lower)) if (is_too_big(lower))
return false; return false;
new_lemma lemma(c(), "propagate value - lower bound of range is above value"); lemma_builder lemma(c(), "propagate value - lower bound of range is above value");
lemma &= ex; lemma &= ex;
lemma |= ineq(v, cmp, lower); lemma |= ineq(v, cmp, lower);
TRACE(nla_solver, dep.display(tout << c().val(v) << " < ", range) << "\n" << lemma << "\n";); TRACE(nla_solver, dep.display(tout << c().val(v) << " < ", range) << "\n" << lemma << "\n";);
@ -196,7 +196,7 @@ namespace nla {
// p even, range.upper < 0, v^p >= 0 -> infeasible // p even, range.upper < 0, v^p >= 0 -> infeasible
if (p % 2 == 0 && rational(dep.upper(range)).is_neg()) { if (p % 2 == 0 && rational(dep.upper(range)).is_neg()) {
++c().lra.settings().stats().m_nla_propagate_bounds; ++c().lra.settings().stats().m_nla_propagate_bounds;
new_lemma lemma(c(), "range requires a non-negative upper bound"); lemma_builder lemma(c(), "range requires a non-negative upper bound");
lemma &= ex; lemma &= ex;
return true; return true;
} }
@ -208,7 +208,7 @@ namespace nla {
if ((p % 2 == 1) || c().val(v).is_pos()) { if ((p % 2 == 1) || c().val(v).is_pos()) {
++c().lra.settings().stats().m_nla_propagate_bounds; ++c().lra.settings().stats().m_nla_propagate_bounds;
auto le = dep.upper_is_open(range) ? llc::LT : llc::LE; auto le = dep.upper_is_open(range) ? llc::LT : llc::LE;
new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value"); lemma_builder lemma(c(), "propagate value - root case - upper bound of range is below value");
lemma &= ex; lemma &= ex;
lemma |= ineq(v, le, r); lemma |= ineq(v, le, r);
return true; return true;
@ -218,7 +218,7 @@ namespace nla {
++c().lra.settings().stats().m_nla_propagate_bounds; ++c().lra.settings().stats().m_nla_propagate_bounds;
SASSERT(!r.is_neg()); SASSERT(!r.is_neg());
auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE; auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE;
new_lemma lemma(c(), "propagate value - root case - upper bound of range is below negative value"); lemma_builder lemma(c(), "propagate value - root case - upper bound of range is below negative value");
lemma &= ex; lemma &= ex;
lemma |= ineq(v, ge, -r); lemma |= ineq(v, ge, -r);
return true; return true;
@ -242,7 +242,7 @@ namespace nla {
auto le = dep.lower_is_open(range) ? llc::LT : llc::LE; auto le = dep.lower_is_open(range) ? llc::LT : llc::LE;
lp::explanation ex; lp::explanation ex;
dep.get_lower_dep(range, ex); dep.get_lower_dep(range, ex);
new_lemma lemma(c(), "propagate value - root case - lower bound of range is above value"); lemma_builder lemma(c(), "propagate value - root case - lower bound of range is above value");
lemma &= ex; lemma &= ex;
lemma |= ineq(v, ge, r); lemma |= ineq(v, ge, r);
if (p % 2 == 0) if (p % 2 == 0)
@ -380,7 +380,7 @@ namespace nla {
return false; return false;
lp::explanation exp; lp::explanation exp;
c().lra.get_infeasibility_explanation(exp); c().lra.get_infeasibility_explanation(exp);
new_lemma lemma(c(), "propagate fixed - infeasible lra"); lemma_builder lemma(c(), "propagate fixed - infeasible lra");
lemma &= exp; lemma &= exp;
return true; return true;
} }

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

@ -83,7 +83,7 @@ void basics::basic_sign_lemma_model_based_one_mon(const monic& m, int product_si
TRACE(nla_solver_bl, tout << "zero product sign: " << pp_mon(_(), m)<< "\n";); TRACE(nla_solver_bl, tout << "zero product sign: " << pp_mon(_(), m)<< "\n";);
generate_zero_lemmas(m); generate_zero_lemmas(m);
} else { } else {
new_lemma lemma(c(), __FUNCTION__); lemma_builder lemma(c(), __FUNCTION__);
for (lpvar j: m.vars()) { for (lpvar j: m.vars()) {
negate_strict_sign(lemma, j); negate_strict_sign(lemma, j);
} }
@ -149,7 +149,7 @@ bool basics::basic_sign_lemma(bool derived) {
// the value of the i-th monic has to be equal to the value of the k-th monic modulo sign // the value of the i-th monic has to be equal to the value of the k-th monic modulo sign
// but it is not the case in the model // but it is not the case in the model
void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& sign) { void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& sign) {
new_lemma lemma(c(), "sign lemma"); lemma_builder lemma(c(), "sign lemma");
TRACE(nla_solver, TRACE(nla_solver,
tout << "m = " << pp_mon_with_vars(_(), m); tout << "m = " << pp_mon_with_vars(_(), m);
tout << "n = " << pp_mon_with_vars(_(), n); tout << "n = " << pp_mon_with_vars(_(), n);
@ -175,7 +175,7 @@ lpvar basics::find_best_zero(const monic& m, unsigned_vector & fixed_zeros) cons
} }
void basics::add_trivial_zero_lemma(lpvar zero_j, const monic& m) { void basics::add_trivial_zero_lemma(lpvar zero_j, const monic& m) {
new_lemma lemma(c(), "x = 0 => x*y = 0"); lemma_builder lemma(c(), "x = 0 => x*y = 0");
lemma |= ineq(zero_j, llc::NE, 0); lemma |= ineq(zero_j, llc::NE, 0);
lemma |= ineq(m.var(), llc::EQ, 0); lemma |= ineq(m.var(), llc::EQ, 0);
} }
@ -183,7 +183,7 @@ void basics::add_trivial_zero_lemma(lpvar zero_j, const monic& m) {
void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj) { void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj) {
TRACE(nla_solver_bl, tout << "sign_of_zj = " << sign_of_zj << "\n";); TRACE(nla_solver_bl, tout << "sign_of_zj = " << sign_of_zj << "\n";);
// we know all the signs // we know all the signs
new_lemma lemma(c(), "strict case 0"); lemma_builder lemma(c(), "strict case 0");
lemma |= ineq(zero_j, sign_of_zj == 1? llc::GT : llc::LT, 0); lemma |= ineq(zero_j, sign_of_zj == 1? llc::GT : llc::LT, 0);
for (unsigned j : m.vars()) { for (unsigned j : m.vars()) {
if (j != zero_j) { if (j != zero_j) {
@ -194,12 +194,12 @@ void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, in
} }
void basics::add_fixed_zero_lemma(const monic& m, lpvar j) { void basics::add_fixed_zero_lemma(const monic& m, lpvar j) {
new_lemma lemma(c(), "fixed zero"); lemma_builder lemma(c(), "fixed zero");
lemma.explain_fixed(j); lemma.explain_fixed(j);
lemma |= ineq(m.var(), llc::EQ, 0); lemma |= ineq(m.var(), llc::EQ, 0);
} }
void basics::negate_strict_sign(new_lemma& lemma, lpvar j) { void basics::negate_strict_sign(lemma_builder& lemma, lpvar j) {
TRACE(nla_solver_details, tout << pp_var(c(), j) << " " << val(j).is_zero() << "\n";); TRACE(nla_solver_details, tout << pp_var(c(), j) << " " << val(j).is_zero() << "\n";);
if (!val(j).is_zero()) { if (!val(j).is_zero()) {
int sign = nla::rat_sign(val(j)); int sign = nla::rat_sign(val(j));
@ -226,7 +226,7 @@ bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) {
return false; return false;
} }
TRACE(nla_solver, c().trace_print_monic_and_factorization(rm, f, tout);); TRACE(nla_solver, c().trace_print_monic_and_factorization(rm, f, tout););
new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0"); lemma_builder lemma(c(), "xy = 0 -> x = 0 or y = 0");
lemma.explain_fixed(var(rm)); lemma.explain_fixed(var(rm));
std::unordered_set<lpvar> processed; std::unordered_set<lpvar> processed;
for (auto j : f) { for (auto j : f) {
@ -298,7 +298,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori
for (auto fc : f) { for (auto fc : f) {
if (!c().var_is_fixed_to_zero(var(fc))) if (!c().var_is_fixed_to_zero(var(fc)))
continue; continue;
new_lemma lemma(c(), "x = 0 or y = 0 -> xy = 0"); lemma_builder lemma(c(), "x = 0 or y = 0 -> xy = 0");
lemma.explain_fixed(var(fc)); lemma.explain_fixed(var(fc));
lemma.explain_var_separated_from_zero(var(rm)); lemma.explain_var_separated_from_zero(var(rm));
lemma &= rm; lemma &= rm;
@ -345,7 +345,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz
// (mon_var != 0 || u != 0) & mon_var = +/- u => // (mon_var != 0 || u != 0) & mon_var = +/- u =>
// v = 1 or v = -1 // v = 1 or v = -1
new_lemma lemma(c(), "|xa| = |x| & x != 0 -> |a| = 1"); lemma_builder lemma(c(), "|xa| = |x| & x != 0 -> |a| = 1");
lemma.explain_var_separated_from_zero(mon_var_is_sep_from_zero ? mon_var : u); lemma.explain_var_separated_from_zero(mon_var_is_sep_from_zero ? mon_var : u);
lemma.explain_equiv(mon_var, u); lemma.explain_equiv(mon_var, u);
lemma |= ineq(v, llc::EQ, 1); lemma |= ineq(v, llc::EQ, 1);
@ -387,7 +387,7 @@ void basics::proportion_lemma_model_based(const monic& rm, const factorization&
*/ */
void basics::generate_pl_on_mon(const monic& m, unsigned k) { void basics::generate_pl_on_mon(const monic& m, unsigned k) {
SASSERT(!c().has_real(m)); SASSERT(!c().has_real(m));
new_lemma lemma(c(), "generate_pl_on_mon"); lemma_builder lemma(c(), "generate_pl_on_mon");
unsigned mon_var = m.var(); unsigned mon_var = m.var();
rational mv = val(mon_var); rational mv = val(mon_var);
SASSERT(abs(mv) < abs(val(m.vars()[k]))); SASSERT(abs(mv) < abs(val(m.vars()[k])));
@ -423,7 +423,7 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind
generate_pl_on_mon(m, factor_index); generate_pl_on_mon(m, factor_index);
return; return;
} }
new_lemma lemma(c(), "generate_pl"); lemma_builder lemma(c(), "generate_pl");
int fi = 0; int fi = 0;
rational mv = var_val(m); rational mv = var_val(m);
rational sm = rational(nla::rat_sign(mv)); rational sm = rational(nla::rat_sign(mv));
@ -459,7 +459,7 @@ bool basics::is_separated_from_zero(const factorization& f) const {
void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) { void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) {
TRACE(nla_solver, c().trace_print_monic_and_factorization(rm, f, tout);); TRACE(nla_solver, c().trace_print_monic_and_factorization(rm, f, tout););
SASSERT(var_val(rm).is_zero() && !c().rm_check(rm)); SASSERT(var_val(rm).is_zero() && !c().rm_check(rm));
new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0"); lemma_builder lemma(c(), "xy = 0 -> x = 0 or y = 0");
if (!is_separated_from_zero(f)) { if (!is_separated_from_zero(f)) {
lemma |= ineq(var(rm), llc::NE, 0); lemma |= ineq(var(rm), llc::NE, 0);
for (auto j : f) { for (auto j : f) {
@ -511,7 +511,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co
if (!can_create_lemma_for_mon_neutral_from_factors_to_monic_model_based(m, m, not_one, sign)) if (!can_create_lemma_for_mon_neutral_from_factors_to_monic_model_based(m, m, not_one, sign))
return false; return false;
new_lemma lemma(c(), __FUNCTION__); lemma_builder lemma(c(), __FUNCTION__);
for (auto j : m.vars()) { for (auto j : m.vars()) {
if (not_one != j) if (not_one != j)
lemma |= ineq(j, llc::NE, val(j)); lemma |= ineq(j, llc::NE, val(j));
@ -556,7 +556,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic
// v = 1 // v = 1
// v = -1 // v = -1
new_lemma lemma(c(), __FUNCTION__); lemma_builder lemma(c(), __FUNCTION__);
lemma |= ineq(mon_var, llc::EQ, 0); lemma |= ineq(mon_var, llc::EQ, 0);
lemma |= ineq(term(u, rational(val(u) == -val(mon_var) ? 1 : -1), mon_var), llc::NE, 0); lemma |= ineq(term(u, rational(val(u) == -val(mon_var) ? 1 : -1), mon_var), llc::NE, 0);
lemma |= ineq(v, llc::EQ, 1); lemma |= ineq(v, llc::EQ, 1);
@ -641,7 +641,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const
return false; return false;
TRACE(nla_solver_bl, tout << "not_one = " << not_one << "\n";); TRACE(nla_solver_bl, tout << "not_one = " << not_one << "\n";);
new_lemma lemma(c(), __FUNCTION__); lemma_builder lemma(c(), __FUNCTION__);
for (auto j : f) { for (auto j : f) {
lpvar var_j = var(j); lpvar var_j = var(j);
@ -665,7 +665,7 @@ void basics::basic_lemma_for_mon_non_zero_model_based(const monic& rm, const fac
TRACE(nla_solver_bl, c().trace_print_monic_and_factorization(rm, f, tout);); TRACE(nla_solver_bl, c().trace_print_monic_and_factorization(rm, f, tout););
for (auto j : f) { for (auto j : f) {
if (val(j).is_zero()) { if (val(j).is_zero()) {
new_lemma lemma(c(), "x = 0 => x*... = 0"); lemma_builder lemma(c(), "x = 0 => x*... = 0");
lemma |= ineq(var(j), llc::NE, 0); lemma |= ineq(var(j), llc::NE, 0);
lemma |= ineq(f.mon().var(), llc::EQ, 0); lemma |= ineq(f.mon().var(), llc::EQ, 0);
lemma &= f; lemma &= f;

4
src/math/lp/nla_basics_lemmas.h
View file

@ -14,7 +14,7 @@
namespace nla { namespace nla {
class core; class core;
class new_lemma; class lemma_builder;
struct basics: common { struct basics: common {
basics(core *core); basics(core *core);
bool basic_sign_lemma_on_two_monics(const monic& m, const monic& n); bool basic_sign_lemma_on_two_monics(const monic& m, const monic& n);
@ -84,7 +84,7 @@ struct basics: common {
void generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj); void generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj);
void add_fixed_zero_lemma(const monic& m, lpvar j); void add_fixed_zero_lemma(const monic& m, lpvar j);
void negate_strict_sign(new_lemma& lemma, lpvar j); void negate_strict_sign(lemma_builder& lemma, lpvar j);
// x != 0 or y = 0 => |xy| >= |y| // x != 0 or y = 0 => |xy| >= |y|
void proportion_lemma_model_based(const monic& rm, const factorization& factorization); void proportion_lemma_model_based(const monic& rm, const factorization& factorization);
// if there are no zero factors then |m| >= |m[factor_index]| // if there are no zero factors then |m| >= |m[factor_index]|

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

@ -350,7 +350,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 // return true iff the negation of the ineq can be derived from the constraints
bool core::explain_ineq(new_lemma& lemma, const lp::lar_term& t, llc cmp, const rational& rs) { bool core::explain_ineq(lemma_builder& lemma, 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 // check that we have something like 0 < 0, which is always false and can be safely
// removed from the lemma // removed from the lemma
@ -410,7 +410,7 @@ bool core::explain_by_equiv(const lp::lar_term& t, lp::explanation& e) const {
return true; return true;
} }
void core::mk_ineq_no_expl_check(new_lemma& lemma, lp::lar_term& t, llc cmp, const rational& rs) { void core::mk_ineq_no_expl_check(lemma_builder& lemma, lp::lar_term& t, llc cmp, const rational& rs) {
TRACE(nla_solver_details, lra.print_term_as_indices(t, tout << "t = ");); TRACE(nla_solver_details, lra.print_term_as_indices(t, tout << "t = "););
lemma |= ineq(cmp, t, rs); lemma |= ineq(cmp, t, rs);
CTRACE(nla_solver, ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";); CTRACE(nla_solver, ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";);
@ -429,7 +429,7 @@ llc apply_minus(llc cmp) {
} }
// the monics should be equal by modulo sign but this is not so in the model // the monics should be equal by modulo sign but this is not so in the model
void core::fill_explanation_and_lemma_sign(new_lemma& lemma, const monic& a, const monic & b, rational const& sign) { void core::fill_explanation_and_lemma_sign(lemma_builder& lemma, const monic& a, const monic & b, rational const& sign) {
SASSERT(sign == 1 || sign == -1); SASSERT(sign == 1 || sign == -1);
lemma &= a; lemma &= a;
lemma &= b; lemma &= b;
@ -899,7 +899,7 @@ bool core::divide(const monic& bc, const factor& c, factor & b) const {
} }
void core::negate_factor_equality(new_lemma& lemma, const factor& c, void core::negate_factor_equality(lemma_builder& lemma, const factor& c,
const factor& d) { const factor& d) {
if (c == d) if (c == d)
return; return;
@ -910,7 +910,7 @@ void core::negate_factor_equality(new_lemma& lemma, const factor& c,
lemma |= ineq(term(i, rational(iv == jv ? -1 : 1), j), llc::NE, 0); lemma |= ineq(term(i, rational(iv == jv ? -1 : 1), j), llc::NE, 0);
} }
void core::negate_factor_relation(new_lemma& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b) { void core::negate_factor_relation(lemma_builder& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b) {
rational a_fs = sign_to_rat(canonize_sign(a)); rational a_fs = sign_to_rat(canonize_sign(a));
rational b_fs = sign_to_rat(canonize_sign(b)); rational b_fs = sign_to_rat(canonize_sign(b));
llc cmp = a_sign*val(a) < b_sign*val(b)? llc::GE : llc::LE; llc cmp = a_sign*val(a) < b_sign*val(b)? llc::GE : llc::LE;
@ -1040,11 +1040,11 @@ rational core::val(const factorization& f) const {
return r; return r;
} }
new_lemma::new_lemma(core& c, char const* name):name(name), c(c) { lemma_builder::lemma_builder(core& c, char const* name):name(name), c(c) {
c.m_lemmas.push_back(lemma()); c.m_lemmas.push_back(lemma());
} }
new_lemma& new_lemma::operator|=(ineq const& ineq) { lemma_builder& lemma_builder::operator|=(ineq const& ineq) {
if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) { if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) {
CTRACE(nla_solver, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";); CTRACE(nla_solver, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";);
SASSERT(c.m_use_nra_model || !c.ineq_holds(ineq)); SASSERT(c.m_use_nra_model || !c.ineq_holds(ineq));
@ -1054,7 +1054,7 @@ new_lemma& new_lemma::operator|=(ineq const& ineq) {
} }
new_lemma::~new_lemma() { lemma_builder::~lemma_builder() {
static int i = 0; static int i = 0;
(void)i; (void)i;
(void)name; (void)name;
@ -1067,22 +1067,22 @@ new_lemma::~new_lemma() {
TRACE(nla_solver, tout << name << " " << (++i) << "\n" << *this; ); TRACE(nla_solver, tout << name << " " << (++i) << "\n" << *this; );
} }
lemma& new_lemma::current() const { lemma& lemma_builder::current() const {
return c.m_lemmas.back(); return c.m_lemmas.back();
} }
new_lemma& new_lemma::operator&=(lp::explanation const& e) { lemma_builder& lemma_builder::operator&=(lp::explanation const& e) {
expl().add_expl(e); expl().add_expl(e);
return *this; return *this;
} }
new_lemma& new_lemma::operator&=(const monic& m) { lemma_builder& lemma_builder::operator&=(const monic& m) {
for (lpvar j : m.vars()) for (lpvar j : m.vars())
*this &= j; *this &= j;
return *this; return *this;
} }
new_lemma& new_lemma::operator&=(const factor& f) { lemma_builder& lemma_builder::operator&=(const factor& f) {
if (f.type() == factor_type::VAR) if (f.type() == factor_type::VAR)
*this &= f.var(); *this &= f.var();
else else
@ -1090,7 +1090,7 @@ new_lemma& new_lemma::operator&=(const factor& f) {
return *this; return *this;
} }
new_lemma& new_lemma::operator&=(const factorization& f) { lemma_builder& lemma_builder::operator&=(const factorization& f) {
if (f.is_mon()) if (f.is_mon())
return *this; return *this;
for (const auto& fc : f) { for (const auto& fc : f) {
@ -1099,19 +1099,19 @@ new_lemma& new_lemma::operator&=(const factorization& f) {
return *this; return *this;
} }
new_lemma& new_lemma::operator&=(lpvar j) { lemma_builder& lemma_builder::operator&=(lpvar j) {
c.m_evars.explain(j, expl()); c.m_evars.explain(j, expl());
return *this; return *this;
} }
new_lemma& new_lemma::explain_fixed(lpvar j) { lemma_builder& lemma_builder::explain_fixed(lpvar j) {
SASSERT(c.var_is_fixed(j)); SASSERT(c.var_is_fixed(j));
explain_existing_lower_bound(j); explain_existing_lower_bound(j);
explain_existing_upper_bound(j); explain_existing_upper_bound(j);
return *this; return *this;
} }
new_lemma& new_lemma::explain_equiv(lpvar a, lpvar b) { lemma_builder& lemma_builder::explain_equiv(lpvar a, lpvar b) {
SASSERT(abs(c.val(a)) == abs(c.val(b))); SASSERT(abs(c.val(a)) == abs(c.val(b)));
if (c.vars_are_equiv(a, b)) { if (c.vars_are_equiv(a, b)) {
*this &= a; *this &= a;
@ -1123,7 +1123,7 @@ new_lemma& new_lemma::explain_equiv(lpvar a, lpvar b) {
return *this; return *this;
} }
new_lemma& new_lemma::explain_var_separated_from_zero(lpvar j) { lemma_builder& lemma_builder::explain_var_separated_from_zero(lpvar j) {
SASSERT(c.var_is_separated_from_zero(j)); SASSERT(c.var_is_separated_from_zero(j));
if (c.lra.column_has_upper_bound(j) && if (c.lra.column_has_upper_bound(j) &&
(c.lra.get_upper_bound(j)< lp::zero_of_type<lp::impq>())) (c.lra.get_upper_bound(j)< lp::zero_of_type<lp::impq>()))
@ -1133,7 +1133,7 @@ new_lemma& new_lemma::explain_var_separated_from_zero(lpvar j) {
return *this; return *this;
} }
new_lemma& new_lemma::explain_existing_lower_bound(lpvar j) { lemma_builder& lemma_builder::explain_existing_lower_bound(lpvar j) {
SASSERT(c.has_lower_bound(j)); SASSERT(c.has_lower_bound(j));
lp::explanation ex; lp::explanation ex;
c.lra.push_explanation(c.lra.get_column_lower_bound_witness(j), ex); c.lra.push_explanation(c.lra.get_column_lower_bound_witness(j), ex);
@ -1142,7 +1142,7 @@ new_lemma& new_lemma::explain_existing_lower_bound(lpvar j) {
return *this; return *this;
} }
new_lemma& new_lemma::explain_existing_upper_bound(lpvar j) { lemma_builder& lemma_builder::explain_existing_upper_bound(lpvar j) {
SASSERT(c.has_upper_bound(j)); SASSERT(c.has_upper_bound(j));
lp::explanation ex; lp::explanation ex;
c.lra.push_explanation(c.lra.get_column_upper_bound_witness(j), ex); c.lra.push_explanation(c.lra.get_column_upper_bound_witness(j), ex);
@ -1150,7 +1150,7 @@ new_lemma& new_lemma::explain_existing_upper_bound(lpvar j) {
return *this; return *this;
} }
std::ostream& new_lemma::display(std::ostream & out) const { std::ostream& lemma_builder::display(std::ostream & out) const {
auto const& lemma = current(); auto const& lemma = current();
for (auto p : lemma.expl()) { for (auto p : lemma.expl()) {
@ -1175,7 +1175,7 @@ std::ostream& new_lemma::display(std::ostream & out) const {
return out; return out;
} }
void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) { void core::negate_relation(lemma_builder& lemma, unsigned j, const rational& a) {
SASSERT(val(j) != a); SASSERT(val(j) != a);
lemma |= ineq(j, val(j) < a ? llc::GE : llc::LE, a); lemma |= ineq(j, val(j) < a ? llc::GE : llc::LE, a);
} }

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

@ -46,7 +46,7 @@ bool try_insert(const A& elem, B& collection) {
class core { class core {
friend struct common; friend struct common;
friend class new_lemma; friend class lemma_builder;
friend class grobner; friend class grobner;
friend class order; friend class order;
friend struct basics; friend struct basics;
@ -263,7 +263,7 @@ public:
std::ostream& out); std::ostream& out);
void mk_ineq_no_expl_check(new_lemma& lemma, lp::lar_term& t, llc cmp, const rational& rs); void mk_ineq_no_expl_check(lemma_builder& lemma, lp::lar_term& t, llc cmp, const rational& rs);
void maybe_add_a_factor(lpvar i, void maybe_add_a_factor(lpvar i,
const factor& c, const factor& c,
@ -273,7 +273,7 @@ public:
llc apply_minus(llc cmp); llc apply_minus(llc cmp);
void fill_explanation_and_lemma_sign(new_lemma& lemma, const monic& a, const monic & b, rational const& sign); void fill_explanation_and_lemma_sign(lemma_builder& lemma, const monic& a, const monic & b, rational const& sign);
svector<lpvar> reduce_monic_to_rooted(const svector<lpvar> & vars, rational & sign) const; svector<lpvar> reduce_monic_to_rooted(const svector<lpvar> & vars, rational & sign) const;
@ -319,7 +319,7 @@ public:
bool var_is_separated_from_zero(lpvar j) const; bool var_is_separated_from_zero(lpvar j) const;
bool vars_are_equiv(lpvar a, lpvar b) const; bool vars_are_equiv(lpvar a, lpvar b) const;
bool explain_ineq(new_lemma& lemma, const lp::lar_term& t, llc cmp, const rational& rs); bool explain_ineq(lemma_builder& lemma, const lp::lar_term& t, llc cmp, const rational& rs);
bool explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const; bool explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const;
bool explain_lower_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const; bool explain_lower_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const;
bool explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const; bool explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const;
@ -370,9 +370,9 @@ public:
bool rm_check(const monic&) const; bool rm_check(const monic&) const;
std::unordered_map<unsigned, unsigned_vector> get_rm_by_arity(); std::unordered_map<unsigned, unsigned_vector> get_rm_by_arity();
void negate_relation(new_lemma& lemma, unsigned j, const rational& a); void negate_relation(lemma_builder& lemma, unsigned j, const rational& a);
void negate_factor_equality(new_lemma& lemma, const factor& c, const factor& d); void negate_factor_equality(lemma_builder& lemma, const factor& c, const factor& d);
void negate_factor_relation(new_lemma& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b); void negate_factor_relation(lemma_builder& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b);
bool find_bfc_to_refine_on_monic(const monic&, factorization & bf); bool find_bfc_to_refine_on_monic(const monic&, factorization & bf);

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

@ -55,7 +55,7 @@ namespace nla {
auto monotonicity1 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val, auto monotonicity1 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val,
auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) { auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) {
if (y1val >= y2val && y2val > 0 && 0 <= x1val && x1val <= x2val && q1val > q2val) { if (y1val >= y2val && y2val > 0 && 0 <= x1val && x1val <= x2val && q1val > q2val) {
new_lemma lemma(c, "y1 >= y2 > 0 & 0 <= x1 <= x2 => x1/y1 <= x2/y2"); lemma_builder lemma(c, "y1 >= y2 > 0 & 0 <= x1 <= x2 => x1/y1 <= x2/y2");
lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0); lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0);
lemma |= ineq(y2, llc::LE, 0); lemma |= ineq(y2, llc::LE, 0);
lemma |= ineq(x1, llc::LT, 0); lemma |= ineq(x1, llc::LT, 0);
@ -69,7 +69,7 @@ namespace nla {
auto monotonicity2 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val, auto monotonicity2 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val,
auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) { auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) {
if (y2val <= y1val && y1val < 0 && x1val >= x2val && x2val >= 0 && q1val > q2val) { if (y2val <= y1val && y1val < 0 && x1val >= x2val && x2val >= 0 && q1val > q2val) {
new_lemma lemma(c, "y2 <= y1 < 0 & x1 >= x2 >= 0 => x1/y1 <= x2/y2"); lemma_builder lemma(c, "y2 <= y1 < 0 & x1 >= x2 >= 0 => x1/y1 <= x2/y2");
lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0); lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0);
lemma |= ineq(y1, llc::GE, 0); lemma |= ineq(y1, llc::GE, 0);
lemma |= ineq(term(x1, rational(-1), x2), llc::LT, 0); lemma |= ineq(term(x1, rational(-1), x2), llc::LT, 0);
@ -83,7 +83,7 @@ namespace nla {
auto monotonicity3 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val, auto monotonicity3 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val,
auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) { auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) {
if (y2val <= y1val && y1val < 0 && x1val <= x2val && x2val <= 0 && q1val < q2val) { if (y2val <= y1val && y1val < 0 && x1val <= x2val && x2val <= 0 && q1val < q2val) {
new_lemma lemma(c, "y2 <= y1 < 0 & x1 <= x2 <= 0 => x1/y1 >= x2/y2"); lemma_builder lemma(c, "y2 <= y1 < 0 & x1 <= x2 <= 0 => x1/y1 >= x2/y2");
lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0); lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0);
lemma |= ineq(y1, llc::GE, 0); lemma |= ineq(y1, llc::GE, 0);
lemma |= ineq(term(x1, rational(-1), x2), llc::GT, 0); lemma |= ineq(term(x1, rational(-1), x2), llc::GT, 0);
@ -187,14 +187,14 @@ namespace nla {
rational hi = yv * div_v + yv - 1; rational hi = yv * div_v + yv - 1;
rational lo = yv * div_v; rational lo = yv * div_v;
if (xv > hi) { if (xv > hi) {
new_lemma lemma(c, "y = yv & x <= yv * div(xv, yv) + yv - 1 => div(p, y) <= div(xv, yv)"); lemma_builder lemma(c, "y = yv & x <= yv * div(xv, yv) + yv - 1 => div(p, y) <= div(xv, yv)");
lemma |= ineq(y, llc::NE, yv); lemma |= ineq(y, llc::NE, yv);
lemma |= ineq(x, llc::GT, hi); lemma |= ineq(x, llc::GT, hi);
lemma |= ineq(q, llc::LE, div_v); lemma |= ineq(q, llc::LE, div_v);
return; return;
} }
if (xv < lo) { if (xv < lo) {
new_lemma lemma(c, "y = yv & x >= yv * div(xv, yv) => div(xv, yv) <= div(x, y)"); lemma_builder lemma(c, "y = yv & x >= yv * div(xv, yv) => div(xv, yv) <= div(x, y)");
lemma |= ineq(y, llc::NE, yv); lemma |= ineq(y, llc::NE, yv);
lemma |= ineq(x, llc::LT, lo); lemma |= ineq(x, llc::LT, lo);
lemma |= ineq(q, llc::GE, div_v); lemma |= ineq(q, llc::GE, div_v);

12
src/math/lp/nla_grobner.cpp
View file

@ -142,7 +142,7 @@ namespace nla {
ineq new_eq(v, llc::EQ, rational::zero()); ineq new_eq(v, llc::EQ, rational::zero());
if (c().ineq_holds(new_eq)) if (c().ineq_holds(new_eq))
return false; return false;
new_lemma lemma(c(), "pdd-eq"); lemma_builder lemma(c(), "pdd-eq");
add_dependencies(lemma, eq); add_dependencies(lemma, eq);
lemma |= new_eq; lemma |= new_eq;
return true; return true;
@ -159,7 +159,7 @@ namespace nla {
ineq new_eq(term(a, v), llc::EQ, b); ineq new_eq(term(a, v), llc::EQ, b);
if (c().ineq_holds(new_eq)) if (c().ineq_holds(new_eq))
return false; return false;
new_lemma lemma(c(), "pdd-eq"); lemma_builder lemma(c(), "pdd-eq");
add_dependencies(lemma, eq); add_dependencies(lemma, eq);
lemma |= new_eq; lemma |= new_eq;
return true; return true;
@ -202,7 +202,7 @@ namespace nla {
if (c().ineq_holds(i)) if (c().ineq_holds(i))
return false; return false;
new_lemma lemma(c(), "pdd-factored"); lemma_builder lemma(c(), "pdd-factored");
add_dependencies(lemma, eq); add_dependencies(lemma, eq);
for (auto const& i : ineqs) for (auto const& i : ineqs)
lemma |= i; lemma |= i;
@ -219,7 +219,7 @@ namespace nla {
} }
void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) { void grobner::add_dependencies(lemma_builder& lemma, const dd::solver::equation& eq) {
lp::explanation exp; lp::explanation exp;
explain(eq, exp); explain(eq, exp);
lemma &= exp; lemma &= exp;
@ -344,7 +344,7 @@ namespace nla {
} }
evali.get_interval<dd::w_dep::with_deps>(e.poly(), i_wd); evali.get_interval<dd::w_dep::with_deps>(e.poly(), i_wd);
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) { std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
new_lemma lemma(m_core, "pdd"); lemma_builder lemma(m_core, "pdd");
lemma &= e; lemma &= e;
}; };
if (di.check_interval_for_conflict_on_zero(i_wd, e.dep(), f)) { if (di.check_interval_for_conflict_on_zero(i_wd, e.dep(), f)) {
@ -686,7 +686,7 @@ namespace nla {
bool grobner::add_nla_conflict(const dd::solver::equation& eq) { bool grobner::add_nla_conflict(const dd::solver::equation& eq) {
if (is_nla_conflict(eq)) { if (is_nla_conflict(eq)) {
new_lemma lemma(m_core,"nla-conflict"); lemma_builder lemma(m_core,"nla-conflict");
lp::explanation exp; lp::explanation exp;
explain(eq, exp); explain(eq, exp);
lemma &= exp; lemma &= exp;

2
src/math/lp/nla_grobner.h
View file

@ -44,7 +44,7 @@ namespace nla {
bool propagate_linear_equations(); bool propagate_linear_equations();
bool propagate_linear_equations(dd::solver::equation const& eq); bool propagate_linear_equations(dd::solver::equation const& eq);
void add_dependencies(new_lemma& lemma, dd::solver::equation const& eq); void add_dependencies(lemma_builder& lemma, dd::solver::equation const& eq);
void explain(dd::solver::equation const& eq, lp::explanation& exp); void explain(dd::solver::equation const& eq, lp::explanation& exp);
bool add_horner_conflict(dd::solver::equation const& eq); bool add_horner_conflict(dd::solver::equation const& eq);

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

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

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

@ -54,7 +54,7 @@ void monotone::monotonicity_lemma(monic const& m) {
*/ */
void monotone::monotonicity_lemma_gt(const monic& m) { void monotone::monotonicity_lemma_gt(const monic& m) {
new_lemma lemma(c(), "monotonicity > "); lemma_builder lemma(c(), "monotonicity > ");
rational product(1); rational product(1);
for (lpvar j : m.vars()) { for (lpvar j : m.vars()) {
auto v = c().val(j); auto v = c().val(j);
@ -76,7 +76,7 @@ void monotone::monotonicity_lemma_gt(const monic& m) {
x <= -2 & y >= 3 => x*y <= -6 x <= -2 & y >= 3 => x*y <= -6
*/ */
void monotone::monotonicity_lemma_lt(const monic& m) { void monotone::monotonicity_lemma_lt(const monic& m) {
new_lemma lemma(c(), "monotonicity <"); lemma_builder lemma(c(), "monotonicity <");
rational product(1); rational product(1);
for (lpvar j : m.vars()) { for (lpvar j : m.vars()) {
auto v = c().val(j); auto v = c().val(j);

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

@ -10,6 +10,7 @@
#include "math/lp/nla_core.h" #include "math/lp/nla_core.h"
#include "math/lp/nla_common.h" #include "math/lp/nla_common.h"
#include "math/lp/factorization_factory_imp.h" #include "math/lp/factorization_factory_imp.h"
#include "util/trail.h"
namespace nla { namespace nla {
@ -83,17 +84,33 @@ void order::order_lemma_on_binomial(const monic& ac) {
void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) { void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) {
if (!c().var_is_int(x) && val(x).is_big()) if (!c().var_is_int(x) && val(x).is_big())
return; return;
if (&xy == m_last_binom) // throttle!!!
return;
c().trail().push(value_trail(m_last_binom, &xy));
SASSERT(!_().mon_has_zero(xy.vars())); SASSERT(!_().mon_has_zero(xy.vars()));
int sy = rat_sign(val(y)); int sy = rat_sign(val(y));
new_lemma lemma(c(), __FUNCTION__); lemma_builder lemma(c(), __FUNCTION__);
lemma |= ineq(y, sy == 1 ? llc::LE : llc::GE, 0); // negate sy lemma |= ineq(y, sy == 1 ? llc::LE : llc::GE, 0); // negate sy
lemma |= ineq(x, sy*sign == 1 ? llc::GT : llc::LT , val(x)); lemma |= ineq(x, sy*sign == 1 ? llc::GT : llc::LT , val(x));
lemma |= ineq(term(xy.var(), - val(x), y), sign == 1 ? llc::LE : llc::GE, 0); lemma |= ineq(term(xy.var(), - val(x), y), sign == 1 ? llc::LE : llc::GE, 0);
} }
bool order::throttle_monic(const monic& ac, std::string const & debug_location ) { // todo - remove debug location!
// Check if throttling is enabled
if (!c().params().arith_nl_thrl())
return false;
// Check if this monic has already been processed using its variable ID
if (m_processed_monics.contains(ac.var())) {
TRACE(nla_solver, tout << "throttled at " << debug_location << "\n";);
return true;
}
// Mark this monic as processed and add to trail for backtracking
m_processed_monics.insert(ac.var());
c().trail().push(insert_map(m_processed_monics, ac.var()));
return false;
}
// We look for monics e = m.rvars()[k]*d and see if we can create an order lemma for m and e // We look for monics e = m.rvars()[k]*d and see if we can create an order lemma for m and e
void order::order_lemma_on_factor_binomial_explore(const monic& ac, bool k) { void order::order_lemma_on_factor_binomial_explore(const monic& ac, bool k) {
TRACE(nla_solver, tout << "ac = " << pp_mon_with_vars(c(), ac);); TRACE(nla_solver, tout << "ac = " << pp_mon_with_vars(c(), ac););
@ -170,7 +187,7 @@ void order::generate_mon_ol(const monic& ac,
SASSERT(ab_cmp != llc::LT || (var_val(ac) >= var_val(bd) && val(a)*c_sign < val(b)*d_sign)); SASSERT(ab_cmp != llc::LT || (var_val(ac) >= var_val(bd) && val(a)*c_sign < val(b)*d_sign));
SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign)); SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign));
new_lemma lemma(_(), __FUNCTION__); lemma_builder lemma(_(), __FUNCTION__);
lemma |= ineq(term(c_sign, c), llc::LE, 0); lemma |= ineq(term(c_sign, c), llc::LE, 0);
lemma &= c; // this explains c == +- d lemma &= c; // this explains c == +- d
lemma |= ineq(term(c_sign, a, -d_sign * b.rat_sign(), b.var()), negate(ab_cmp), 0); lemma |= ineq(term(c_sign, a, -d_sign * b.rat_sign(), b.var()), negate(ab_cmp), 0);
@ -220,7 +237,7 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab
if (mv != fv && !c().has_real(m)) { if (mv != fv && !c().has_real(m)) {
bool gt = mv > fv; bool gt = mv > fv;
for (unsigned j = 0, k = 1; j < 2; j++, k--) { for (unsigned j = 0, k = 1; j < 2; j++, k--) {
new_lemma lemma(_(), __FUNCTION__); lemma_builder lemma(_(), __FUNCTION__);
order_lemma_on_ab(lemma, m, rsign, var(ab[k]), var(ab[j]), gt); order_lemma_on_ab(lemma, m, rsign, var(ab[k]), var(ab[j]), gt);
lemma &= ab; lemma &= ab;
lemma &= m; lemma &= m;
@ -255,7 +272,7 @@ void order::generate_ol_eq(const monic& ac,
const monic& bc, const monic& bc,
const factor& b) { const factor& b) {
new_lemma lemma(_(), __FUNCTION__); lemma_builder lemma(_(), __FUNCTION__);
IF_VERBOSE(100, IF_VERBOSE(100,
verbose_stream() verbose_stream()
<< var_val(ac) << "(" << mul_val(ac) << "): " << ac << var_val(ac) << "(" << mul_val(ac) << "): " << ac
@ -280,7 +297,7 @@ void order::generate_ol(const monic& ac,
const monic& bc, const monic& bc,
const factor& b) { const factor& b) {
new_lemma lemma(_(), __FUNCTION__); lemma_builder lemma(_(), __FUNCTION__);
TRACE(nla_solver, _().trace_print_ol(ac, a, c, bc, b, tout);); TRACE(nla_solver, _().trace_print_ol(ac, a, c, bc, b, tout););
IF_VERBOSE(10, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac IF_VERBOSE(10, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac
<< " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"
@ -335,7 +352,7 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
given: sign * m = ab given: sign * m = ab
lemma b != val(b) || sign*m <= a*val(b) lemma b != val(b) || sign*m <= a*val(b)
*/ */
void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) { void order::order_lemma_on_ab_gt(lemma_builder& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) {
SASSERT(sign * var_val(m) > val(a) * val(b)); SASSERT(sign * var_val(m) > val(a) * val(b));
// negate b == val(b) // negate b == val(b)
lemma |= ineq(b, llc::NE, val(b)); lemma |= ineq(b, llc::NE, val(b));
@ -346,7 +363,7 @@ void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rationa
given: sign * m = ab given: sign * m = ab
lemma b != val(b) || sign*m >= a*val(b) lemma b != val(b) || sign*m >= a*val(b)
*/ */
void order::order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) { void order::order_lemma_on_ab_lt(lemma_builder& 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) << 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";); ", b = "; c().print_var(b, tout) << "\n";);
SASSERT(sign * var_val(m) < val(a) * val(b)); SASSERT(sign * var_val(m) < val(a) * val(b));
@ -356,7 +373,7 @@ void order::order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rationa
lemma |= ineq(term(sign, m.var(), -val(b), a), llc::GE, 0); lemma |= ineq(term(sign, m.var(), -val(b), a), llc::GE, 0);
} }
void order::order_lemma_on_ab(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b, bool gt) { void order::order_lemma_on_ab(lemma_builder& lemma, const monic& m, const rational& sign, lpvar a, lpvar b, bool gt) {
if (gt) if (gt)
order_lemma_on_ab_gt(lemma, m, sign, a, b); order_lemma_on_ab_gt(lemma, m, sign, a, b);
else else

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

@ -9,17 +9,19 @@
#pragma once #pragma once
#include "math/lp/factorization.h" #include "math/lp/factorization.h"
#include "math/lp/nla_common.h" #include "math/lp/nla_common.h"
#include "util/hashtable.h"
#include "util/hash.h"
namespace nla { namespace nla {
class core; class core;
class new_lemma; class lemma_builder;
class order: common { class order: common {
public: public:
order(core *c) : common(c) {} order(core *c) : common(c) {}
void order_lemma(); void order_lemma();
monic const* m_last_binom = nullptr; int_hashtable<int_hash, default_eq<int>> m_processed_monics;
bool throttle_monic(const monic&, const std::string & debug_location);
private: private:
bool order_lemma_on_ac_and_bc_and_factors(const monic& ac, bool order_lemma_on_ac_and_bc_and_factors(const monic& ac,
@ -41,9 +43,9 @@ public:
void order_lemma_on_factorization(const monic& rm, const factorization& ab); void order_lemma_on_factorization(const monic& rm, const factorization& ab);
void order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b); void order_lemma_on_ab_gt(lemma_builder& 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_lt(lemma_builder& 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_ab(lemma_builder& 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_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_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); void order_lemma_on_binomial_ac_bd(const monic& ac, bool k, const monic& bd, const factor& b, lpvar d);

18
src/math/lp/nla_powers.cpp
View file

@ -89,7 +89,7 @@ namespace nla {
lemmas.reset(); lemmas.reset();
auto x_exp_0 = [&]() { auto x_exp_0 = [&]() {
new_lemma lemma(c, "x != 0 => x^0 = 1"); lemma_builder lemma(c, "x != 0 => x^0 = 1");
lemma |= ineq(x, llc::EQ, rational::zero()); lemma |= ineq(x, llc::EQ, rational::zero());
lemma |= ineq(y, llc::NE, rational::zero()); lemma |= ineq(y, llc::NE, rational::zero());
lemma |= ineq(r, llc::EQ, rational::one()); lemma |= ineq(r, llc::EQ, rational::one());
@ -97,7 +97,7 @@ namespace nla {
}; };
auto zero_exp_y = [&]() { auto zero_exp_y = [&]() {
new_lemma lemma(c, "y != 0 => 0^y = 0"); lemma_builder lemma(c, "y != 0 => 0^y = 0");
lemma |= ineq(x, llc::NE, rational::zero()); lemma |= ineq(x, llc::NE, rational::zero());
lemma |= ineq(y, llc::EQ, rational::zero()); lemma |= ineq(y, llc::EQ, rational::zero());
lemma |= ineq(r, llc::EQ, rational::zero()); lemma |= ineq(r, llc::EQ, rational::zero());
@ -105,14 +105,14 @@ namespace nla {
}; };
auto x_gt_0 = [&]() { auto x_gt_0 = [&]() {
new_lemma lemma(c, "x > 0 => x^y > 0"); lemma_builder lemma(c, "x > 0 => x^y > 0");
lemma |= ineq(x, llc::LE, rational::zero()); lemma |= ineq(x, llc::LE, rational::zero());
lemma |= ineq(r, llc::GT, rational::zero()); lemma |= ineq(r, llc::GT, rational::zero());
return l_false; return l_false;
}; };
auto y_lt_1 = [&]() { auto y_lt_1 = [&]() {
new_lemma lemma(c, "x > 1, y < 0 => x^y < 1"); lemma_builder lemma(c, "x > 1, y < 0 => x^y < 1");
lemma |= ineq(x, llc::LE, rational::one()); lemma |= ineq(x, llc::LE, rational::one());
lemma |= ineq(y, llc::GE, rational::zero()); lemma |= ineq(y, llc::GE, rational::zero());
lemma |= ineq(r, llc::LT, rational::one()); lemma |= ineq(r, llc::LT, rational::one());
@ -120,7 +120,7 @@ namespace nla {
}; };
auto y_gt_1 = [&]() { auto y_gt_1 = [&]() {
new_lemma lemma(c, "x > 1, y > 0 => x^y > 1"); lemma_builder lemma(c, "x > 1, y > 0 => x^y > 1");
lemma |= ineq(x, llc::LE, rational::one()); lemma |= ineq(x, llc::LE, rational::one());
lemma |= ineq(y, llc::LE, rational::zero()); lemma |= ineq(y, llc::LE, rational::zero());
lemma |= ineq(r, llc::GT, rational::one()); lemma |= ineq(r, llc::GT, rational::one());
@ -128,7 +128,7 @@ namespace nla {
}; };
auto x_ge_3 = [&]() { auto x_ge_3 = [&]() {
new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1"); lemma_builder lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1");
lemma |= ineq(x, llc::LT, rational(3)); lemma |= ineq(x, llc::LT, rational(3));
lemma |= ineq(y, llc::EQ, rational::zero()); lemma |= ineq(y, llc::EQ, rational::zero());
lemma |= ineq(lp::lar_term(r, rational::minus_one(), y), llc::GT, rational::one()); lemma |= ineq(lp::lar_term(r, rational::minus_one(), y), llc::GT, rational::one());
@ -172,21 +172,21 @@ namespace nla {
if (rval == r2val) if (rval == r2val)
return l_true; return l_true;
if (c.random() % 2 == 0) { if (c.random() % 2 == 0) {
new_lemma lemma(c, "x == x0, y == y0 => r = x0^y0"); lemma_builder lemma(c, "x == x0, y == y0 => r = x0^y0");
lemma |= ineq(x, llc::NE, xval); lemma |= ineq(x, llc::NE, xval);
lemma |= ineq(y, llc::NE, yval); lemma |= ineq(y, llc::NE, yval);
lemma |= ineq(r, llc::EQ, r2val); lemma |= ineq(r, llc::EQ, r2val);
return l_false; return l_false;
} }
if (yval > 0 && r2val > rval) { if (yval > 0 && r2val > rval) {
new_lemma lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0"); lemma_builder lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0");
lemma |= ineq(x, llc::LT, xval); lemma |= ineq(x, llc::LT, xval);
lemma |= ineq(y, llc::LT, yval); lemma |= ineq(y, llc::LT, yval);
lemma |= ineq(r, llc::GE, r2val); lemma |= ineq(r, llc::GE, r2val);
return l_false; return l_false;
} }
if (r2val < rval) { if (r2val < rval) {
new_lemma lemma(c, "0 < x <= x0, y <= y0 => r <= x0^y0"); lemma_builder lemma(c, "0 < x <= x0, y <= y0 => r <= x0^y0");
lemma |= ineq(x, llc::LE, rational::zero()); lemma |= ineq(x, llc::LE, rational::zero());
lemma |= ineq(x, llc::GT, xval); lemma |= ineq(x, llc::GT, xval);
lemma |= ineq(y, llc::GT, yval); lemma |= ineq(y, llc::GT, yval);

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

@ -61,7 +61,7 @@ private:
core & c() { return m_tang.c(); } core & c() { return m_tang.c(); }
void explain(new_lemma& lemma) { void explain(lemma_builder& lemma) {
if (!m_is_mon) { if (!m_is_mon) {
lemma &= m_m; lemma &= m_m;
lemma &= m_x; lemma &= m_x;
@ -70,7 +70,7 @@ private:
} }
void generate_plane(const point & pl) { void generate_plane(const point & pl) {
new_lemma lemma(c(), "generate tangent plane"); lemma_builder lemma(c(), "generate tangent plane");
c().negate_relation(lemma, m_jx, m_x.rat_sign()*pl.x); c().negate_relation(lemma, m_jx, m_x.rat_sign()*pl.x);
c().negate_relation(lemma, m_jy, m_y.rat_sign()*pl.y); c().negate_relation(lemma, m_jy, m_y.rat_sign()*pl.y);
#if Z3DEBUG #if Z3DEBUG
@ -91,7 +91,7 @@ private:
} }
void generate_line1() { void generate_line1() {
new_lemma lemma(c(), "tangent line 1"); lemma_builder lemma(c(), "tangent line 1");
// Should be v = val(m_x)*val(m_y), and val(factor) = factor.rat_sign()*var(factor.var()) // Should be v = val(m_x)*val(m_y), and val(factor) = factor.rat_sign()*var(factor.var())
lemma |= ineq(m_jx, llc::NE, c().val(m_jx)); lemma |= ineq(m_jx, llc::NE, c().val(m_jx));
lemma |= ineq(lp::lar_term(m_j, - m_y.rat_sign() * m_xy.x, m_jy), llc::EQ, 0); lemma |= ineq(lp::lar_term(m_j, - m_y.rat_sign() * m_xy.x, m_jy), llc::EQ, 0);
@ -99,7 +99,7 @@ private:
} }
void generate_line2() { void generate_line2() {
new_lemma lemma(c(), "tangent line 2"); lemma_builder lemma(c(), "tangent line 2");
lemma |= ineq(m_jy, llc::NE, c().val(m_jy)); lemma |= ineq(m_jy, llc::NE, c().val(m_jy));
lemma |= ineq(lp::lar_term(m_j, - m_x.rat_sign() * m_xy.y, m_jx), llc::EQ, 0); lemma |= ineq(lp::lar_term(m_j, - m_x.rat_sign() * m_xy.y, m_jx), llc::EQ, 0);
explain(lemma); explain(lemma);

30
src/math/lp/nla_types.h
View file

@ -69,27 +69,27 @@ namespace nla {
// all constraints are assumed added to the lemma // all constraints are assumed added to the lemma
// correctness of the lemma can be checked at this point. // correctness of the lemma can be checked at this point.
// //
class new_lemma { class lemma_builder {
char const* name; char const* name;
core& c; core& c;
lemma& current() const; lemma& current() const;
public: public:
new_lemma(core& c, char const* name); lemma_builder(core& c, char const* name);
~new_lemma(); ~lemma_builder();
lemma& operator()() { return current(); } lemma& operator()() { return current(); }
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
new_lemma& operator&=(lp::explanation const& e); lemma_builder& operator&=(lp::explanation const& e);
new_lemma& operator&=(const monic& m); lemma_builder& operator&=(const monic& m);
new_lemma& operator&=(const factor& f); lemma_builder& operator&=(const factor& f);
new_lemma& operator&=(const factorization& f); lemma_builder& operator&=(const factorization& f);
new_lemma& operator&=(lpvar j); lemma_builder& operator&=(lpvar j);
new_lemma& operator|=(ineq const& i); lemma_builder& operator|=(ineq const& i);
new_lemma& explain_fixed(lpvar j); lemma_builder& explain_fixed(lpvar j);
new_lemma& explain_equiv(lpvar u, lpvar v); lemma_builder& explain_equiv(lpvar u, lpvar v);
new_lemma& explain_var_separated_from_zero(lpvar j); lemma_builder& explain_var_separated_from_zero(lpvar j);
new_lemma& explain_existing_lower_bound(lpvar j); lemma_builder& explain_existing_lower_bound(lpvar j);
new_lemma& explain_existing_upper_bound(lpvar j); lemma_builder& explain_existing_upper_bound(lpvar j);
lp::explanation& expl() { return current().expl(); } lp::explanation& expl() { return current().expl(); }
@ -97,7 +97,7 @@ namespace nla {
}; };
inline std::ostream& operator<<(std::ostream& out, new_lemma const& l) { inline std::ostream& operator<<(std::ostream& out, lemma_builder const& l) {
return l.display(out); return l.display(out);
} }

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

@ -228,7 +228,7 @@ struct solver::imp {
ex.push_back(idx); ex.push_back(idx);
TRACE(nra, lra.display_constraint(tout << "ex: " << idx << ": ", idx) << "\n";); TRACE(nra, lra.display_constraint(tout << "ex: " << idx << ": ", idx) << "\n";);
} }
nla::new_lemma lemma(m_nla_core, __FUNCTION__); nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
lemma &= ex; lemma &= ex;
m_nla_core.set_use_nra_model(true); m_nla_core.set_use_nra_model(true);
break; break;
@ -416,7 +416,7 @@ struct solver::imp {
dm.linearize(static_cast<u_dependency*>(c), lv); dm.linearize(static_cast<u_dependency*>(c), lv);
for (auto ci : lv) for (auto ci : lv)
ex.push_back(ci); ex.push_back(ci);
nla::new_lemma lemma(m_nla_core, __FUNCTION__); nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
lemma &= ex; lemma &= ex;
break; break;
} }

1
src/params/smt_params_helper.pyg
View file

@ -65,6 +65,7 @@ def_module_params(module_name='smt',
('arith.nl.order', BOOL, True, 'run order lemmas'), ('arith.nl.order', BOOL, True, 'run order lemmas'),
('arith.nl.expp', BOOL, False, 'expensive patching'), ('arith.nl.expp', BOOL, False, 'expensive patching'),
('arith.nl.tangents', BOOL, True, 'run tangent lemmas'), ('arith.nl.tangents', BOOL, True, 'run tangent lemmas'),
('arith.nl.thrl', BOOL, True, 'throttle repeated lemmas - debug, remove later!!!'),
('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'), ('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'),
('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'), ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'),