mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

a fix in add_abs_bound() and integrating NB changes

Browse source
This commit is contained in:
Lev Nachmanson 2019-04-08 15:00:05 -07:00
parent a323eaf1c8
commit c7dec3ef4d
2 changed files with 139 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/util/lp/factorization.h
View file

@ -36,24 +36,22 @@ public:
factor() {}
explicit factor(unsigned j) : factor(j, factor_type::VAR) {}
factor(unsigned i, factor_type t) : m_index(i), m_type(t) {}
unsigned index() const {return m_index;}
unsigned& index() {return m_index;}
factor_type type() const {return m_type;}
factor_type& type() {return m_type;}
unsigned index() const { return m_index; }
unsigned& index() { return m_index; }
factor_type type() const { return m_type; }
factor_type& type() { return m_type; }
bool is_var() const { return m_type == factor_type::VAR; }
bool operator==(factor const& other) const {
return m_index == other.index() && m_type == other.type();
}
bool operator!=(factor const& other) const {
return m_index != other.index() || m_type != other.type();
}
};
inline bool operator==(const factor& a, const factor& b) {
return a.index() == b.index() && a.type() == b.type();
}
inline bool operator!=(const factor& a, const factor& b) {
return ! (a == b);
}
class factorization {
vector<factor> m_vars;
vector<factor> m_vars;
const monomial* m_mon;
public:
factorization(const monomial* m): m_mon(m) {
@ -77,11 +75,11 @@ public:
struct const_iterator_mon {
// fields
svector<bool> m_mask;
svector<bool> m_mask;
const factorization_factory * m_ff;
bool m_full_factorization_returned;
bool m_full_factorization_returned;
//typedefs
// typedefs
typedef const_iterator_mon self_type;
typedef factorization value_type;
typedef int difference_type;
@ -109,7 +107,7 @@ struct const_iterator_mon {
struct factorization_factory {
const svector<lpvar>& m_vars;
const monomial* m_monomial;
const monomial* m_monomial;
// returns true if found
virtual bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned& i) const = 0;
virtual const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const = 0;

148
src/util/lp/nla_solver.cpp
View file

@ -529,6 +529,8 @@ struct solver::imp {
}
m_lar_solver.subs_term_columns(t);
current_lemma().push_back(ineq(cmp, t, rs));
CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";);
SASSERT(!ineq_holds(ineq(cmp, t, rs)));
}
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs) {
lp::lar_term t;
@ -2048,6 +2050,42 @@ struct solver::imp {
register_monomials_in_tables();
}
#if 0
void init_to_refine() {
m_to_refine.clear();
for (auto const & m : m_emons)
if (!check_monomial(m))
m_to_refine.push_back(m.var());
TRACE("nla_solver",
tout << m_to_refine.size() << " mons to refine:\n";
for (unsigned v : m_to_refine) tout << m_emons.var2monomial(v) << "\n";
}
std::unordered_set<lpvar> collect_vars( const lemma& l) {
std::unordered_set<lpvar> vars;
auto insert_j = [&](lpvar j) {
vars.insert(j);
auto const* m = m_emons.var2monomial(j);
if (m) for (lpvar k : *m) vars.insert(k);
};
for (const auto& i : current_lemma().ineqs()) {
for (const auto& p : i.term()) {
insert_j(p.var());
}
}
for (const auto& p : current_expl()) {
const auto& c = m_lar_solver.get_constraint(p.second);
for (const auto& r : c.coeffs()) {
insert_j(r.second);
}
}
return vars;
}
#endif
void init_to_refine() {
m_to_refine.clear();
for (unsigned i = 0; i < m_monomials.size(); i++) {
@ -2336,7 +2374,11 @@ struct solver::imp {
}
}
// if gt is true we need to deduce ab <= vvr(b)*a
/**
\brief Add lemma:
a > 0 & b <= value(b) => sign*ab <= value(b)*a if value(a) > 0
a < 0 & b >= value(b) => sign*ab <= value(b)*a if value(a) < 0
*/
void order_lemma_on_ab_gt(const monomial& m, const rational& sign, lpvar a, lpvar b) {
SASSERT(sign * vvr(m) > vvr(a) * vvr(b));
add_empty_lemma();
@ -2360,6 +2402,11 @@ struct solver::imp {
}
}
// we need to deduce ab >= vvr(b)*a
/**
\brief Add lemma:
a > 0 & b >= value(b) => sign*ab >= value(b)*a if value(a) > 0
a < 0 & b <= value(b) => sign*ab >= value(b)*a if value(a) < 0
*/
void order_lemma_on_ab_lt(const monomial& m, const rational& sign, lpvar a, lpvar b) {
SASSERT(sign * vvr(m) < vvr(a) * vvr(b));
add_empty_lemma();
@ -2619,6 +2666,8 @@ struct solver::imp {
mk_ineq(as, a, -bs, b, llc::GE); // negate |aj| < |bj|
}
// a < 0 & b < 0 => a < b
void assert_abs_val_a_le_abs_var_b(
const rooted_mon& a,
const rooted_mon& b,
@ -2788,6 +2837,19 @@ struct solver::imp {
} while (i != ii);
}
#if 0
void monotonicity_lemma() {
auto const& vars = m_rm_table.m_to_refine
unsigned sz = vars.size();
unsigned start = random();
for (unsigned j = 0; !done() && j < sz; ++j) {
unsigned i = (start + j) % sz;
monotonicity_lemma(*m_emons.var2monomial(vars[i]));
}
}
#endif
void monotonicity_lemma(unsigned i_mon) {
const monomial & m = m_monomials[i_mon];
SASSERT(!check_monomial(m));
@ -2801,53 +2863,93 @@ struct solver::imp {
monotonicity_lemma_gt(m, prod_val);
}
// assert that |j| <= |j|
// add |j| <= |vvr(j)|
void var_abs_val_le(lpvar j) {
auto s = rational(rat_sign(vvr(j)));
mk_ineq(s, j, llc::LT);
mk_ineq(s, j, llc::GT, abs(vvr(j)));
}
// assert that |j| >= |j|
// assert that |j| >= |vvr(j)|
void var_abs_val_ge(lpvar j) {
auto s = rational(rat_sign(vvr(j)));
mk_ineq(s, j, llc::LT);
mk_ineq(s, j, llc::LT, abs(vvr(j)));
}
/** \brief enforce that the |m| <= product |m[i]| .
For each i assert
sign(m[i])*m[i] < 0 or m[i] > |m[i]|,
and assert sign(m)*m < 0 or |m| <= product |m[i]|
/**
\brief Add |v| ~ |bound|
where ~ is <, <=, >, >=,
and bound = vvr(v)
|v| > |bound|
<=>
(v < 0 or v > |bound|) & (v > 0 or -v > |bound|)
=> Let s be the sign of vvr(v)
(s*v < 0 or s*v > |bound|)
|v| < |bound|
<=>
v < |bound| & -v < |bound|
=> Let s be the sign of vvr(v)
s*v < |bound|
*/
void add_abs_bound(lpvar v, llc cmp) {
add_abs_bound(v, cmp, vvr(v));
}
void add_abs_bound(lpvar v, llc cmp, rational const& bound) {
lp::lar_term t; // t = abs(v)
t.add_coeff_var(rrat_sign(vvr(v)), v);
switch (cmp) {
case llc::GT:
case llc::GE: // negate abs(v) >= 0
mk_ineq(t, llc::LT, rational(0));
break;
case llc::LT:
case llc::LE:
break;
default:
UNREACHABLE();
break;
}
mk_ineq(t, cmp, abs(bound));
}
/** \brief enforce the inequality |m| <= product |m[i]| .
by enforcing lemma:
/\_i |m[i]| <= |vvr(m[i])| => |m| <= |product_i vvr(m[i])|
<=>
\/_i |m[i]| > |vvr(m[i])} or |m| <= |product_i vvr(m[i])|
*/
void monotonicity_lemma_gt(const monomial& m, const rational& prod_val) {
// the abs of the monomial is too large
SASSERT(prod_val.is_pos());
add_empty_lemma();
for (lpvar j : m) {
var_abs_val_le(j);
add_abs_bound(j, llc::GT);
}
lpvar m_j = m.var();
auto s = rational(rat_sign(vvr(m_j)));
mk_ineq(s, m_j, llc::LE, prod_val);
add_abs_bound(m_j, llc::LE, prod_val);
TRACE("nla_solver", print_lemma(tout););
}
/** \brief enforce that the |m| >= product |m[i]| .
For each i assert
sign(m[i])*m[i] < 0 or m[i] < |m[i]|,
and assert sign(m)*m < 0 or |m| >= product |m[i]|
/** \brief enforce the inequality |m| >= product |m[i]| .
/\_i |m[i]| >= |vvr(m[i])| => |m| >= |product_i vvr(m[i])|
<=>
\/_i |m[i]| < |vvr(m[i])} or |m| >= |product_i vvr(m[i])|
*/
void monotonicity_lemma_lt(const monomial& m, const rational& prod_val) {
// the abs of the monomial is too small
SASSERT(prod_val.is_pos());
add_empty_lemma();
for (lpvar j : m) {
var_abs_val_ge(j);
add_abs_bound(j, llc::LT);
}
lpvar m_j = m.var();
auto s = rational(rat_sign(vvr(m_j)));
mk_ineq(s, m_j, llc::LT);
mk_ineq(s, m_j, llc::GE, prod_val);
add_abs_bound(m_j, llc::GE, prod_val);
TRACE("nla_solver", print_lemma(tout););
}
@ -3164,8 +3266,6 @@ struct solver::imp {
TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << m_lemma_vec->size() << "\n";);
IF_VERBOSE(2, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monomials(verbose_stream());});
CTRACE("nla_solver", ret == l_undef, tout << "Monomials\n"; print_monomials(tout););
SASSERT(ret != l_false || no_lemmas_hold());
return ret;
}