mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

adding monomial bounds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-13 18:44:04 -07:00
parent bdecbe4ed7
commit 4e51633e6f
6 changed files with 136 additions and 117 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/math/interval/dep_intervals.cpp
View file

@ -89,21 +89,23 @@ bool dep_intervals::separated_from_zero_on_upper(const interval& i) const {
std::ostream& dep_intervals::display(std::ostream& out, const interval& i) const { std::ostream& dep_intervals::display(std::ostream& out, const interval& i) const {
if (m_imanager.lower_is_inf(i)) { if (m_imanager.lower_is_inf(i)) {
out << "(-oo"; out << "(-oo";
} else { }
else {
out << (m_imanager.lower_is_open(i)? "(":"[") << rational(m_imanager.lower(i)); out << (m_imanager.lower_is_open(i)? "(":"[") << rational(m_imanager.lower(i));
} }
out << ","; out << ",";
if (m_imanager.upper_is_inf(i)) { if (m_imanager.upper_is_inf(i)) {
out << "oo)"; out << "oo)";
} else { }
else {
out << rational(m_imanager.upper(i)) << (m_imanager.upper_is_open(i)? ")":"]"); out << rational(m_imanager.upper(i)) << (m_imanager.upper_is_open(i)? ")":"]");
} }
if (i.m_lower_dep) { if (i.m_lower_dep) {
out << "\nlower deps\n"; // out << "\nlower deps\n";
// TBD: print_dependencies(i.m_lower_dep, out); // TBD: print_dependencies(i.m_lower_dep, out);
} }
if (i.m_upper_dep) { if (i.m_upper_dep) {
out << "\nupper deps\n"; // out << "\nupper deps\n";
// TBD: print_dependencies(i.m_upper_dep, out); // TBD: print_dependencies(i.m_upper_dep, out);
} }
return out; return out;
@ -125,21 +127,21 @@ bool dep_intervals::is_empty(interval const& a) const {
bool dep_intervals::is_above(const interval& i, const rational& r) const { bool dep_intervals::is_above(const interval& i, const rational& r) const {
if (lower_is_inf(i)) if (lower_is_inf(i))
return false; return false;
if (m_num_manager.lt(lower(i), r.to_mpq())) if (m_num_manager.lt(r.to_mpq(), lower(i)))
return false; return true;
if (m_num_manager.eq(lower(i), r.to_mpq()) && !m_config.lower_is_open(i)) if (m_num_manager.eq(lower(i), r.to_mpq()) && m_config.lower_is_open(i))
return false; return true;
return true; return false;
} }
bool dep_intervals::is_below(const interval& i, const rational& r) const { bool dep_intervals::is_below(const interval& i, const rational& r) const {
if (upper_is_inf(i)) if (upper_is_inf(i))
return false; return false;
if (m_num_manager.lt(upper(i), r.to_mpq())) if (m_num_manager.lt(upper(i), r.to_mpq()))
return false; return true;
if (m_num_manager.eq(upper(i), r.to_mpq()) && !m_config.upper_is_open(i)) if (m_num_manager.eq(upper(i), r.to_mpq()) && m_config.upper_is_open(i))
return false; return true;
return true; return false;
} }

2
src/math/interval/dep_intervals.h
View file

@ -411,12 +411,10 @@ private:
void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); } void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); }
void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
SASSERT(&a != &i && &b != &i);
m_config.add_deps(a, b, deps, i); m_config.add_deps(a, b, deps, i);
} }
void combine_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const { void combine_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const {
SASSERT(&a != &i);
m_config.add_deps(a, deps, i); m_config.add_deps(a, deps, i);
} }

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

@ -13,7 +13,9 @@
namespace nla { namespace nla {
monomial_bounds::monomial_bounds(core* c):common(c) {} monomial_bounds::monomial_bounds(core* c):
common(c),
dep(c->m_intervals.get_dep_intervals()) {}
bool monomial_bounds::operator()() { bool monomial_bounds::operator()() {
bool propagated = false; bool propagated = false;
@ -29,9 +31,7 @@ namespace nla {
* Accumulate product of variables in monomial starting at position 'start' * Accumulate product of variables in monomial starting at position 'start'
*/ */
void monomial_bounds::compute_product(unsigned start, monic const& m, scoped_dep_interval& product) { void monomial_bounds::compute_product(unsigned start, monic const& m, scoped_dep_interval& product) {
auto & intervals = c().m_intervals; scoped_dep_interval vi(dep);
auto & dep_intervals = intervals.get_dep_intervals();
scoped_dep_interval vi(dep_intervals);
for (unsigned i = start; i < m.size(); ) { for (unsigned i = start; i < m.size(); ) {
lpvar v = m.vars()[i]; lpvar v = m.vars()[i];
unsigned power = 1; unsigned power = 1;
@ -40,8 +40,8 @@ namespace nla {
for (; i < m.size() && m.vars()[i] == v; ++i) { for (; i < m.size() && m.vars()[i] == v; ++i) {
++power; ++power;
} }
dep_intervals.power<dep_intervals::with_deps>(vi, power, vi); dep.power<dep_intervals::with_deps>(vi, power, vi);
dep_intervals.mul<dep_intervals::with_deps>(product, vi, product); dep.mul<dep_intervals::with_deps>(product, vi, product);
} }
} }
@ -51,26 +51,27 @@ namespace nla {
* a bounds axiom. * a bounds axiom.
*/ */
bool monomial_bounds::propagate_value(dep_interval& range, lpvar v) { bool monomial_bounds::propagate_value(dep_interval& range, lpvar v) {
auto & intervals = c().m_intervals; auto val = c().val(v);
auto & dep_intervals = intervals.get_dep_intervals(); if (dep.is_below(range, val)) {
if (dep_intervals.is_below(range, c().val(v))) {
lp::explanation ex; lp::explanation ex;
dep_intervals.get_upper_dep(range, ex); dep.get_upper_dep(range, ex);
auto const& upper = dep_intervals.upper(range); auto const& upper = dep.upper(range);
auto cmp = dep_intervals.upper_is_open(range) ? llc::LT : llc::LE; auto cmp = dep.upper_is_open(range) ? llc::LT : llc::LE;
new_lemma lemma(c(), "propagate value - upper bound of range is below value"); new_lemma 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 << val << " > ", range) << "\n" << lemma << "\n";);
return true; return true;
} }
else if (dep_intervals.is_above(range, c().val(v))) { else if (dep.is_above(range, val)) {
lp::explanation ex; lp::explanation ex;
dep_intervals.get_lower_dep(range, ex); dep.get_lower_dep(range, ex);
auto const& lower = dep_intervals.lower(range); auto const& lower = dep.lower(range);
auto cmp = dep_intervals.lower_is_open(range) ? llc::GT : llc::GE; auto cmp = dep.lower_is_open(range) ? llc::GT : llc::GE;
new_lemma lemma(c(), "propagate value - lower bound of range is above value"); new_lemma 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 << val << " < ", range) << "\n" << lemma << "\n";);
return true; return true;
} }
else { else {
@ -79,26 +80,26 @@ namespace nla {
} }
void monomial_bounds::var2interval(lpvar v, scoped_dep_interval& i) { void monomial_bounds::var2interval(lpvar v, scoped_dep_interval& i) {
auto & intervals = c().m_intervals;
auto & dep_intervals = intervals.get_dep_intervals();
lp::constraint_index ci; lp::constraint_index ci;
rational bound; rational bound;
bool is_strict; bool is_strict;
if (c().has_lower_bound(v, ci, bound, is_strict)) { if (c().has_lower_bound(v, ci, bound, is_strict)) {
dep_intervals.set_lower_is_open(i, is_strict); dep.set_lower_is_open(i, is_strict);
dep_intervals.set_lower(i, bound); dep.set_lower(i, bound);
dep_intervals.set_lower_dep(i, dep_intervals.mk_leaf(ci)); dep.set_lower_dep(i, dep.mk_leaf(ci));
dep.set_lower_is_inf(i, false);
} }
else { else {
dep_intervals.set_lower_is_inf(i, true); dep.set_lower_is_inf(i, true);
} }
if (c().has_upper_bound(v, ci, bound, is_strict)) { if (c().has_upper_bound(v, ci, bound, is_strict)) {
dep_intervals.set_upper_is_open(i, is_strict); dep.set_upper_is_open(i, is_strict);
dep_intervals.set_upper(i, bound); dep.set_upper(i, bound);
dep_intervals.set_upper_dep(i, dep_intervals.mk_leaf(ci)); dep.set_upper_dep(i, dep.mk_leaf(ci));
dep.set_upper_is_inf(i, false);
} }
else { else {
dep_intervals.set_upper_is_inf(i, true); dep.set_upper_is_inf(i, true);
} }
} }
@ -110,15 +111,22 @@ namespace nla {
* If the value of m.var() is outside of product_of_all_vars, add a bounds lemma. * If the value of m.var() is outside of product_of_all_vars, add a bounds lemma.
*/ */
bool monomial_bounds::propagate(monic const& m) { bool monomial_bounds::propagate(monic const& m) {
auto & intervals = c().m_intervals; unsigned num_free, power;
auto & dep_intervals = intervals.get_dep_intervals(); lpvar free_var;
scoped_dep_interval product(dep_intervals); analyze_monomial(m, num_free, free_var, power);
scoped_dep_interval vi(dep_intervals), mi(dep_intervals); bool m_is_free = is_free(m.var());
scoped_dep_interval other_product(dep_intervals); if (num_free >= 2)
var2interval(m.var(), mi);
if (dep_intervals.lower_is_inf(mi) && dep_intervals.upper_is_inf(mi))
return false; return false;
dep_intervals.set_value(product, rational::one()); if (num_free >= 1 && m_is_free)
return false;
SASSERT(num_free == 0 || !m_is_free);
bool do_propagate_up = num_free == 0;
bool do_propagate_down = !m_is_free;
scoped_dep_interval product(dep);
scoped_dep_interval vi(dep), mi(dep);
scoped_dep_interval other_product(dep);
var2interval(m.var(), mi);
dep.set_value(product, rational::one());
for (unsigned i = 0; i < m.size(); ) { for (unsigned i = 0; i < m.size(); ) {
lpvar v = m.vars()[i]; lpvar v = m.vars()[i];
++i; ++i;
@ -126,28 +134,60 @@ namespace nla {
for (; i < m.size() && v == m.vars()[i]; ++i) for (; i < m.size() && v == m.vars()[i]; ++i)
++power; ++power;
var2interval(v, vi); var2interval(v, vi);
dep_intervals.power<dep_intervals::with_deps>(vi, power, vi); dep.power<dep_intervals::with_deps>(vi, power, vi);
if (power == 1) {
dep_intervals.set<dep_intervals::with_deps>(other_product, product); if (power == 1 && do_propagate_down && (num_free == 0 || free_var == v)) {
dep.set<dep_intervals::with_deps>(other_product, product);
compute_product(i, m, other_product); compute_product(i, m, other_product);
if (propagate_down(m, mi, v, other_product)) if (propagate_down(m, mi, v, other_product))
return true; return true;
} }
dep_intervals.mul<dep_intervals::with_deps>(product, vi, product); dep.mul<dep_intervals::with_deps>(product, vi, product);
} }
return propagate_value(product, m.var()); return do_propagate_up && propagate_value(product, m.var());
} }
bool monomial_bounds::propagate_down(monic const& m, dep_interval& mi, lpvar v, dep_interval& product) { bool monomial_bounds::propagate_down(monic const& m, dep_interval& mi, lpvar v, dep_interval& product) {
auto & intervals = c().m_intervals; if (!dep.separated_from_zero(product))
auto & dep_intervals = intervals.get_dep_intervals();
if (!dep_intervals.separated_from_zero(product))
return false; return false;
scoped_dep_interval range(dep_intervals); scoped_dep_interval range(dep);
dep_intervals.set<dep_intervals::with_deps>(range, mi); dep.div<dep_intervals::with_deps>(mi, product, range);
dep_intervals.div<dep_intervals::with_deps>(range, product, range);
return propagate_value(range, v); return propagate_value(range, v);
} }
bool monomial_bounds::is_free(lpvar v) const {
return !c().has_lower_bound(v) && !c().has_upper_bound(v);
}
bool monomial_bounds::is_zero(lpvar v) const {
return
c().has_lower_bound(v) &&
c().has_upper_bound(v) &&
c().get_lower_bound(v).is_zero() &&
c().get_lower_bound(v) == c().get_upper_bound(v);
}
void monomial_bounds::analyze_monomial(monic const& m, unsigned& num_free, lpvar& fv, unsigned& fv_power) const {
unsigned power = 0;
num_free = 0;
fv = null_lpvar;
fv_power = 0;
for (unsigned i = 0; i < m.vars().size(); ) {
lpvar v = m.vars()[i];
unsigned power = 1;
++i;
for (; i < m.vars().size() && m.vars()[i] == v; ++i, ++power);
if (is_zero(v)) {
num_free = 0;
return;
}
if (power % 2 == 1 && is_free(v)) {
++num_free;
fv_power = power;
fv = v;
}
}
}
} }

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

@ -10,20 +10,21 @@
#include "math/lp/nla_common.h" #include "math/lp/nla_common.h"
#include "math/lp/nla_intervals.h" #include "math/lp/nla_intervals.h"
#include "math/lp/nex.h"
#include "math/lp/cross_nested.h"
#include "math/lp/u_set.h" #include "math/lp/u_set.h"
namespace nla { namespace nla {
class core; class core;
class monomial_bounds : common { class monomial_bounds : common {
dep_intervals& dep;
void var2interval(lpvar v, scoped_dep_interval& i); void var2interval(lpvar v, scoped_dep_interval& i);
bool propagate_down(monic const& m, lpvar u); bool propagate_down(monic const& m, lpvar u);
bool propagate_value(dep_interval& range, lpvar v); bool propagate_value(dep_interval& range, lpvar v);
void compute_product(unsigned start, monic const& m, scoped_dep_interval& i); void compute_product(unsigned start, monic const& m, scoped_dep_interval& i);
bool propagate(monic const& m); bool propagate(monic const& m);
bool propagate_down(monic const& m, dep_interval& mi, lpvar v, dep_interval& product); bool propagate_down(monic const& m, dep_interval& mi, lpvar v, dep_interval& product);
void analyze_monomial(monic const& m, unsigned& num_free, lpvar& free_v, unsigned& power) const;
bool is_free(lpvar v) const;
bool is_zero(lpvar v) const;
public: public:
monomial_bounds(core* core); monomial_bounds(core* core);
bool operator()(); bool operator()();

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

@ -29,6 +29,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
m_monotone(this), m_monotone(this),
m_intervals(this, lim), m_intervals(this, lim),
m_horner(this), m_horner(this),
m_monomial_bounds(this),
m_pdd_manager(s.number_of_vars()), m_pdd_manager(s.number_of_vars()),
m_pdd_grobner(lim, m_pdd_manager), m_pdd_grobner(lim, m_pdd_manager),
m_emons(m_evars), m_emons(m_evars),
@ -137,13 +138,13 @@ void core::add_monic(lpvar v, unsigned sz, lpvar const* vs) {
} }
void core::push() { void core::push() {
TRACE("nla_solver",); TRACE("nla_solver_verbose", tout << "\n";);
m_emons.push(); m_emons.push();
} }
void core::pop(unsigned n) { void core::pop(unsigned n) {
TRACE("nla_solver", tout << "n = " << n << "\n";); TRACE("nla_solver_verbose", tout << "n = " << n << "\n";);
m_emons.pop(n); m_emons.pop(n);
SASSERT(elists_are_consistent(false)); SASSERT(elists_are_consistent(false));
} }
@ -403,10 +404,8 @@ bool core::explain_by_equiv(const lp::lar_term& t, lp::explanation& e) const {
m_evars.explain(signed_var(i, false), signed_var(j, sign), e); m_evars.explain(signed_var(i, false), signed_var(j, sign), e);
TRACE("nla_solver", tout << "explained :"; m_lar_solver.print_term_as_indices(t, tout);); TRACE("nla_solver", tout << "explained :"; m_lar_solver.print_term_as_indices(t, tout););
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(new_lemma& lemma, lp::lar_term& t, llc cmp, const rational& rs) {
TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = ");); TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = "););
@ -424,8 +423,7 @@ llc apply_minus(llc cmp) {
default: break; default: break;
} }
return cmp; return 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(new_lemma& lemma, const monic& a, const monic & b, rational const& sign) {
@ -475,9 +473,7 @@ int core::vars_sign(const svector<lpvar>& v) {
} }
return sign; return sign;
} }
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); return m_lar_solver.column_has_upper_bound(j);
} }
@ -1214,10 +1210,8 @@ std::ostream& new_lemma::display(std::ostream & out) const {
for (lpvar j : c.collect_vars(lemma)) { for (lpvar j : c.collect_vars(lemma)) {
c.print_var(j, out); c.print_var(j, out);
} }
return out; return out;
} }
void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) { void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) {
SASSERT(val(j) != a); SASSERT(val(j) != a);
@ -1238,21 +1232,6 @@ bool core::done() const {
lp_settings().get_cancel_flag(); lp_settings().get_cancel_flag();
} }
void core::incremental_linearization(bool constraint_derived) {
TRACE("nla_solver_details", print_terms(tout); tout << m_lar_solver.constraints(););
m_basics.basic_lemma(constraint_derived);
if (!m_lemma_vec->empty() || constraint_derived || done())
return;
TRACE("nla_solver", tout << "passed constraint_derived and basic lemmas\n";);
SASSERT(elists_are_consistent(true));
if (!done())
m_order.order_lemma();
if (!done())
m_monotone.monotonicity_lemma();
if (!done())
m_tangents.tangent_lemma();
}
bool core::elist_is_consistent(const std::unordered_set<lpvar> & list) const { bool core::elist_is_consistent(const std::unordered_set<lpvar> & list) const {
bool first = true; bool first = true;
bool p; bool p;
@ -1359,12 +1338,9 @@ bool core::patch_blocker(lpvar u, const monic& m) const {
} }
bool core::try_to_patch(lpvar k, const rational& v, const monic & m) { bool core::try_to_patch(lpvar k, const rational& v, const monic & m) {
return m_lar_solver.try_to_patch(k, v, auto blocker = [this, k, m](lpvar u) { return u != k && patch_blocker(u, m); };
[this, k, m](lpvar u) { auto change_report = [this](lpvar u) { update_to_refine_of_var(u); };
if (u == k) return m_lar_solver.try_to_patch(k, v, blocker, change_report);
return false; // ok to patch
return patch_blocker(u, m); },
[this](lpvar u) { update_to_refine_of_var(u); });
} }
bool in_power(const svector<lpvar>& vs, unsigned l) { bool in_power(const svector<lpvar>& vs, unsigned l) {
@ -1465,22 +1441,25 @@ lbool core::check(vector<lemma>& l_vec) {
patch_monomials_with_real_vars(); patch_monomials_with_real_vars();
if (m_to_refine.is_empty()) { return l_true; } if (m_to_refine.is_empty()) { return l_true; }
init_search(); init_search();
lbool ret = l_undef;
set_use_nra_model(false); set_use_nra_model(false);
if (need_to_call_algebraic_methods()) { if (false && l_vec.empty() && !done())
if (!m_horner.horner_lemmas() && m_nla_settings.run_grobner() && !done()) { m_monomial_bounds();
clear_and_resize_active_var_set();
find_nl_cluster(); if (l_vec.empty() && !done () && need_to_call_algebraic_methods())
run_grobner(); m_horner.horner_lemmas();
}
}
TRACE("nla_solver_details", print_terms(tout); tout << m_lar_solver.constraints(););
if (!done())
m_basics.basic_lemma(true);
TRACE("nla_solver", tout << "passed constraint_derived and basic lemmas\n";); if (l_vec.empty() && !done() && m_nla_settings.run_grobner()) {
SASSERT(!l_vec.empty() || elists_are_consistent(true)); clear_and_resize_active_var_set();
find_nl_cluster();
run_grobner();
}
if (l_vec.empty() && !done())
m_basics.basic_lemma(true);
if (l_vec.empty() && !done()) if (l_vec.empty() && !done())
m_basics.basic_lemma(false); m_basics.basic_lemma(false);
@ -1495,16 +1474,13 @@ lbool core::check(vector<lemma>& l_vec) {
m_tangents.tangent_lemma(); m_tangents.tangent_lemma();
} }
if (!m_reslim.inc())
return l_undef;
lbool ret = l_vec.empty() ? l_undef : l_false;
#if 0 #if 0
if (l_vec.empty()) if (l_vec.empty() && !done())
ret = m_nra.check(); ret = m_nra.check();
}
#endif #endif
if (ret == l_undef && !l_vec.empty() && m_reslim.inc())
ret = l_false;
TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.size() << "\n";); TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.size() << "\n";);
IF_VERBOSE(2, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());}); IF_VERBOSE(2, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());});

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

@ -22,6 +22,7 @@
#include "math/lp/nla_settings.h" #include "math/lp/nla_settings.h"
#include "math/lp/nex.h" #include "math/lp/nex.h"
#include "math/lp/horner.h" #include "math/lp/horner.h"
#include "math/lp/monomial_bounds.h"
#include "math/lp/nla_intervals.h" #include "math/lp/nla_intervals.h"
#include "math/grobner/pdd_solver.h" #include "math/grobner/pdd_solver.h"
#include "nlsat/nlsat_solver.h" #include "nlsat/nlsat_solver.h"
@ -148,7 +149,8 @@ public:
basics m_basics; basics m_basics;
order m_order; order m_order;
monotone m_monotone; monotone m_monotone;
intervals m_intervals; intervals m_intervals;
monomial_bounds m_monomial_bounds;
horner m_horner; horner m_horner;
nla_settings m_nla_settings; nla_settings m_nla_settings;
dd::pdd_manager m_pdd_manager; dd::pdd_manager m_pdd_manager;