mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
review of monotonicity lemma
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
30ce6f20f2
commit
31a96b3afa
|
@ -32,6 +32,19 @@ inline llc negate(llc cmp) {
|
|||
return cmp; // not reachable
|
||||
}
|
||||
|
||||
inline llc swap_side(llc cmp) {
|
||||
switch(cmp) {
|
||||
case llc::LE: return llc::GE;
|
||||
case llc::LT: return llc::GT;
|
||||
case llc::GE: return llc::LE;
|
||||
case llc::GT: return llc::LT;
|
||||
case llc::EQ: return llc::EQ;
|
||||
case llc::NE: return llc::NE;
|
||||
default: SASSERT(false);
|
||||
};
|
||||
return cmp; // not reachable
|
||||
}
|
||||
|
||||
class core;
|
||||
class intervals;
|
||||
struct common {
|
||||
|
|
|
@ -981,57 +981,6 @@ bool core::rm_check(const monic& rm) const {
|
|||
return check_monic(m_emons[rm.var()]);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Add |v| ~ |bound|
|
||||
where ~ is <, <=, >, >=,
|
||||
and bound = val(v)
|
||||
|
||||
|v| > |bound|
|
||||
<=>
|
||||
(v < 0 or v > |bound|) & (v > 0 or -v > |bound|)
|
||||
=> Let s be the sign of val(v)
|
||||
(s*v < 0 or s*v > |bound|)
|
||||
|
||||
|v| < |bound|
|
||||
<=>
|
||||
v < |bound| & -v < |bound|
|
||||
=> Let s be the sign of val(v)
|
||||
s*v < |bound|
|
||||
|
||||
*/
|
||||
|
||||
void core::add_abs_bound(new_lemma& lemma, lpvar v, llc cmp) {
|
||||
add_abs_bound(lemma, v, cmp, val(v));
|
||||
}
|
||||
|
||||
void core::add_abs_bound(new_lemma& lemma, lpvar v, llc cmp, rational const& bound) {
|
||||
SASSERT(!val(v).is_zero());
|
||||
lp::lar_term t; // t = abs(v)
|
||||
t.add_monomial(rrat_sign(val(v)), v);
|
||||
|
||||
switch (cmp) {
|
||||
case llc::GT:
|
||||
case llc::GE: // negate abs(v) >= 0
|
||||
lemma |= ineq(t, llc::LT, 0);
|
||||
break;
|
||||
case llc::LT:
|
||||
case llc::LE:
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
lemma |= ineq(t, cmp, abs(bound));
|
||||
}
|
||||
|
||||
// NB - move this comment to monotonicity or appropriate.
|
||||
/** \brief enforce the inequality |m| <= product |m[i]| .
|
||||
by enforcing lemma:
|
||||
/\_i |m[i]| <= |val(m[i])| => |m| <= |product_i val(m[i])|
|
||||
<=>
|
||||
\/_i |m[i]| > |val(m[i])} or |m| <= |product_i val(m[i])|
|
||||
*/
|
||||
|
||||
|
||||
bool core::find_bfc_to_refine_on_monic(const monic& m, factorization & bf) {
|
||||
for (auto f : factorization_factory_imp(m, *this)) {
|
||||
|
@ -1098,6 +1047,7 @@ new_lemma& new_lemma::operator|=(ineq const& ineq) {
|
|||
}
|
||||
return *this;
|
||||
}
|
||||
|
||||
|
||||
new_lemma::~new_lemma() {
|
||||
static int i = 0;
|
||||
|
@ -1446,10 +1396,10 @@ lbool core::check(vector<lemma>& l_vec) {
|
|||
|
||||
set_use_nra_model(false);
|
||||
|
||||
if (false && l_vec.empty() && !done())
|
||||
if (l_vec.empty() && !done())
|
||||
m_monomial_bounds();
|
||||
|
||||
if (l_vec.empty() && !done () && need_to_call_algebraic_methods())
|
||||
if (l_vec.empty() && !done() && need_to_call_algebraic_methods())
|
||||
m_horner.horner_lemmas();
|
||||
|
||||
if (l_vec.empty() && !done() && m_nla_settings.run_grobner()) {
|
||||
|
@ -1503,8 +1453,7 @@ bool core::no_lemmas_hold() const {
|
|||
return true;
|
||||
}
|
||||
|
||||
lbool core::test_check(
|
||||
vector<lemma>& l) {
|
||||
lbool core::test_check(vector<lemma>& l) {
|
||||
m_lar_solver.set_status(lp::lp_status::OPTIMAL);
|
||||
return check(l);
|
||||
}
|
||||
|
|
|
@ -415,8 +415,6 @@ public:
|
|||
bool rm_check(const monic&) const;
|
||||
std::unordered_map<unsigned, unsigned_vector> get_rm_by_arity();
|
||||
|
||||
void add_abs_bound(new_lemma& lemma, lpvar v, llc cmp);
|
||||
void add_abs_bound(new_lemma& lemma, lpvar v, llc cmp, rational const& bound);
|
||||
void negate_relation(new_lemma& lemma, unsigned j, const rational& a);
|
||||
void negate_factor_equality(new_lemma& 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);
|
||||
|
|
|
@ -30,35 +30,49 @@ void monotone::monotonicity_lemma(monic const& m) {
|
|||
const rational prod_val = abs(c().product_value(m));
|
||||
const rational m_val = abs(var_val(m));
|
||||
if (m_val < prod_val)
|
||||
monotonicity_lemma_lt(m, prod_val);
|
||||
monotonicity_lemma_lt(m);
|
||||
else if (m_val > prod_val)
|
||||
monotonicity_lemma_gt(m, prod_val);
|
||||
monotonicity_lemma_gt(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););
|
||||
/** \brief enforce the inequality |m| <= product |m[i]| .
|
||||
|
||||
/\_i |m[i]| <= |val(m[i])| => |m| <= |product_i val(m[i])|
|
||||
<=>
|
||||
\/_i |m[i]| > |val(m[i])| or |m| <= |product_i val(m[i])|
|
||||
|
||||
implied by
|
||||
m[i] > val(m[i]) for val(m[i]) > 0
|
||||
m[i] < val(m[i]) for val(m[i]) < 0
|
||||
m >= product m[i] for product m[i] < 0
|
||||
m <= product m[i] for product m[i] > 0
|
||||
*/
|
||||
void monotone::monotonicity_lemma_gt(const monic& m) {
|
||||
new_lemma lemma(c(), __FUNCTION__);
|
||||
rational product(1);
|
||||
for (lpvar j : m.vars()) {
|
||||
c().add_abs_bound(lemma, j, llc::GT);
|
||||
auto v = c().val(j);
|
||||
lemma |= ineq(j, v.is_neg() ? llc::LT : llc::GT, v);
|
||||
product *= v;
|
||||
}
|
||||
lpvar m_j = m.var();
|
||||
c().add_abs_bound(lemma, m_j, llc::LE, prod_val);
|
||||
lemma |= ineq(m.var(), product.is_neg() ? llc::GE : llc::LE, product);
|
||||
}
|
||||
|
||||
/** \brief enforce the inequality |m| >= product |m[i]| .
|
||||
|
||||
/\_i |m[i]| >= |val(m[i])| => |m| >= |product_i val(m[i])|
|
||||
<=>
|
||||
\/_i |m[i]| < |val(m[i])} or |m| >= |product_i val(m[i])|
|
||||
\/_i |m[i]| < |val(m[i])| or |m| >= |product_i val(m[i])|
|
||||
*/
|
||||
void monotone::monotonicity_lemma_lt(const monic& m, const rational& prod_val) {
|
||||
void monotone::monotonicity_lemma_lt(const monic& m) {
|
||||
new_lemma lemma(c(), __FUNCTION__);
|
||||
rational product(1);
|
||||
for (lpvar j : m.vars()) {
|
||||
c().add_abs_bound(lemma, j, llc::LT);
|
||||
auto v = c().val(j);
|
||||
lemma |= ineq(j, v.is_neg() ? llc::GT : llc::LT, v);
|
||||
product *= v;
|
||||
}
|
||||
lpvar m_j = m.var();
|
||||
c().add_abs_bound(lemma, m_j, llc::GE, prod_val);
|
||||
lemma |= ineq(m.var(), product.is_neg() ? llc::LE : llc::GE, product);
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -14,8 +14,8 @@ public:
|
|||
void monotonicity_lemma();
|
||||
private:
|
||||
void monotonicity_lemma(monic const& m);
|
||||
void monotonicity_lemma_gt(const monic& m, const rational& prod_val);
|
||||
void monotonicity_lemma_lt(const monic& m, const rational& prod_val);
|
||||
void monotonicity_lemma_gt(const monic& m);
|
||||
void monotonicity_lemma_lt(const monic& m);
|
||||
std::vector<rational> get_sorted_key(const monic& rm) const;
|
||||
vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monic& a) const;
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue