mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

merging master to unit_prop_on_monomials

Browse source
This commit is contained in:
Lev Nachmanson 2023-10-02 16:42:59 -07:00
parent a297a2b25c
commit 7de06c4350
19 changed files with 333 additions and 375 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -10,34 +10,9 @@
#include "math/lp/monomial_bounds.h"
#include "math/lp/nla_core.h"
#include "math/lp/nla_intervals.h"
#include "math/lp/numeric_pair.h"
namespace nla {
// here non_fixed is the only non-fixed variable in the monomial,
// vars is the vector of the monomial variables,
// k is the product of all fixed variables in vars
void monomial_bounds::propagate_nonfixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
vector<std::pair<lp::mpq, unsigned>> coeffs;
coeffs.push_back(std::make_pair(-k, non_fixed));
coeffs.push_back(std::make_pair(rational::one(), monic_var));
lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
auto* dep = explain_fixed(vars, non_fixed);
// term_index becomes the column index of the term slack variable
term_index = c().lra.map_term_index_to_column_index(term_index);
c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep);
c().lra.track_column_feasibility(term_index);
if (!c().lra.column_is_feasible(term_index)) {
c().lra.set_status(lp::lp_status::UNKNOWN);
}
}
u_dependency* monomial_bounds::explain_fixed(const svector<lpvar>& vars, lpvar non_fixed) {
u_dependency* dep = nullptr;
for (auto v : vars)
if (v != non_fixed)
dep = c().lra.join_deps(dep, c().lra.get_bound_constraint_witnesses_for_column(v));
return dep;
}
monomial_bounds::monomial_bounds(core* c):
common(c),
@ -50,6 +25,7 @@ namespace nla {
}
}
bool monomial_bounds::is_too_big(mpq const& q) const {
return rational(q).bitsize() > 256;
}
@ -283,25 +259,127 @@ namespace nla {
}
}
// returns true iff (all variables are fixed,
// or all but one variable are fixed) and the bounds are not big,
// or at least one variable is fixed to zero.
bool monomial_bounds::is_linear(monic const& m, lpvar& zero_var, lpvar& non_fixed) {
zero_var = non_fixed = null_lpvar;
unsigned n_of_non_fixed = 0;
bool big_bound = false;
for (lpvar v : m) {
if (!c().var_is_fixed(v)) {
n_of_non_fixed++;
non_fixed = v;
} else if (c().var_is_fixed_to_zero(v)) {
zero_var = v;
return true;
} else if (c().fixed_var_has_big_bound(v)) {
big_bound |= true;
void monomial_bounds::unit_propagate() {
for (auto const& m : c().m_emons) {
unit_propagate(m);
if (c().lra.get_status() == lp::lp_status::INFEASIBLE) {
lp::explanation exp;
c().lra.get_infeasibility_explanation(exp);
new_lemma lemma(c(), "propagate fixed - infeasible lra");
lemma &= exp;
return;
}
}
return n_of_non_fixed <= 1 && !big_bound;
if (c().m_conflicts > 0 ) {
return;
}
}
}
void monomial_bounds::unit_propagate(monic const& m) {
if (m.is_propagated())
return;
if (!is_linear(m))
return;
rational k = fixed_var_product(m);
lpvar w = non_fixed_var(m);
if (w == null_lpvar || k == 0) {
propagate_fixed(m, k);
}
else
propagate_nonfixed(m, k, w);
}
lp::explanation monomial_bounds::get_explanation(u_dependency* dep) {
lp::explanation exp;
svector<lp::constraint_index> cs;
c().lra.dep_manager().linearize(dep, cs);
for (auto d : cs)
exp.add_pair(d, mpq(1));
return exp;
}
void monomial_bounds::propagate_fixed(monic const& m, rational const& k) {
auto* dep = explain_fixed(m, k);
if (!c().lra.is_base(m.var())) {
lp::impq val(k);
c().lra.set_value_for_nbasic_column(m.var(), val);
}
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
// propagate fixed equality
auto exp = get_explanation(dep);
c().add_fixed_equality(m.var(), k, exp);
}
void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
VERIFY(k != 0);
vector<std::pair<lp::mpq, unsigned>> coeffs;
coeffs.push_back(std::make_pair(-k, w));
coeffs.push_back(std::make_pair(rational::one(), m.var()));
lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
auto* dep = explain_fixed(m, k);
term_index = c().lra.map_term_index_to_column_index(term_index);
c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep);
if (k == 1) {
lp::explanation exp = get_explanation(dep);
c().add_equality(m.var(), w, exp);
}
}
u_dependency* monomial_bounds::explain_fixed(monic const& m, rational const& k) {
u_dependency* dep = nullptr;
auto update_dep = [&](unsigned j) {
dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_lower_bound_witness(j));
dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_upper_bound_witness(j));
return dep;
};
if (k == 0) {
for (auto j : m.vars())
if (c().var_is_fixed_to_zero(j))
return update_dep(j);
}
else {
for (auto j : m.vars())
if (c().var_is_fixed(j))
update_dep(j);
}
return dep;
}
bool monomial_bounds::is_linear(monic const& m) {
unsigned non_fixed = 0;
for (lpvar v : m) {
if (!c().var_is_fixed(v))
++non_fixed;
else if (c().val(v).is_zero())
return true;
}
return non_fixed <= 1;
}
rational monomial_bounds::fixed_var_product(monic const& m) {
rational r(1);
for (lpvar v : m) {
if (c().var_is_fixed(v))
r *= c().lra.get_column_value(v).x;
}
return r;
}
lpvar monomial_bounds::non_fixed_var(monic const& m) {
for (lpvar v : m)
if (!c().var_is_fixed(v))
return v;
return null_lpvar;
}
}

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

@ -17,24 +17,32 @@ namespace nla {
class monomial_bounds : common {
dep_intervals& dep;
u_dependency* explain_fixed(const svector<lpvar>& vars, lpvar non_fixed);
void var2interval(lpvar v, scoped_dep_interval& i);
bool is_too_big(mpq const& q) const;
bool propagate_down(monic const& m, lpvar u);
bool propagate_value(dep_interval& range, lpvar v);
bool propagate_value(dep_interval& range, lpvar v, unsigned power);
void compute_product(unsigned start, monic const& m, scoped_dep_interval& i);
bool propagate(monic const& m);
void propagate_fixed(monic const& m, rational const& k);
void propagate_nonfixed(monic const& m, rational const& k, lpvar w);
u_dependency* explain_fixed(monic const& m, rational const& k);
lp::explanation get_explanation(u_dependency* dep);
bool propagate_down(monic const& m, dep_interval& mi, lpvar v, unsigned power, 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;
// monomial propagation
bool_vector m_propagated;
bool is_linear(monic const& m, lpvar& zero_var, lpvar& non_fixed);
void unit_propagate(monic const& m);
bool is_linear(monic const& m);
rational fixed_var_product(monic const& m);
lpvar non_fixed_var(monic const& m);
public:
monomial_bounds(core* core);
void propagate();
void propagate_nonfixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k);
void unit_propagate();
};
}

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

@ -17,12 +17,11 @@ Author:
#include "math/grobner/pdd_solver.h"
#include "math/dd/pdd_interval.h"
#include "math/dd/pdd_eval.h"
#include "nla_core.h"
namespace nla {
typedef lp::lar_term term;
core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim, std_vector<lp::implied_bound>& implied_bounds) :
core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
m_evars(),
lra(s),
m_reslim(lim),
@ -39,11 +38,11 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim, std_vector<lp:
m_grobner(this),
m_emons(m_evars),
m_use_nra_model(false),
m_nra(s, m_nra_lim, *this),
m_implied_bounds(implied_bounds) {
m_nlsat_delay = lp_settings().nlsat_delay();
m_nra(s, m_nra_lim, *this)
{
m_nlsat_delay = lp_settings().nlsat_delay();
}
bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {
switch(cmp) {
case llc::LE: return ls <= rs;
@ -138,7 +137,6 @@ void core::add_monic(lpvar v, unsigned sz, lpvar const* vs) {
m_add_buffer[i] = j;
}
m_emons.add(v, m_add_buffer);
m_monics_with_changed_bounds.insert(v);
}
void core::push() {
@ -543,13 +541,6 @@ bool core::var_is_fixed_to_zero(lpvar j) const {
lra.column_is_fixed(j) &&
lra.get_lower_bound(j) == lp::zero_of_type<lp::impq>();
}
bool core::fixed_var_has_big_bound(lpvar j) const {
SASSERT(lra.column_is_fixed(j));
const auto& b = lra.get_lower_bound(j);
return b.x.is_big() || b.y.is_big();
}
bool core::var_is_fixed_to_val(lpvar j, const rational& v) const {
return
lra.column_is_fixed(j) &&
@ -818,7 +809,10 @@ void core::print_stats(std::ostream& out) {
void core::clear() {
m_lemmas.clear();
m_literal_vec->clear();
m_literals.clear();
m_fixed_equalities.clear();
m_equalities.clear();
m_conflicts = 0;
}
void core::init_search() {
@ -1065,14 +1059,6 @@ new_lemma& new_lemma::operator|=(ineq const& ineq) {
}
return *this;
}
// Contrary to new_lemma::operator|=, this method does not assert that the model does not satisfy the ineq.
new_lemma& new_lemma::operator+=(ineq const& ineq) {
if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) {
current().push_back(ineq);
}
return *this;
}
new_lemma::~new_lemma() {
@ -1080,6 +1066,9 @@ new_lemma::~new_lemma() {
(void)i;
(void)name;
// code for checking lemma can be added here
if (current().is_conflict()) {
c.m_conflicts++;
}
TRACE("nla_solver", tout << name << " " << (++i) << "\n" << *this; );
}
@ -1511,12 +1500,12 @@ void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(vo
}
lbool core::check_power(lpvar r, lpvar x, lpvar y) {
m_lemmas.reset();
clear();
return m_powers.check(r, x, y, m_lemmas);
}
void core::check_bounded_divisions() {
m_lemmas.reset();
clear();
m_divisions.check_bounded_divisions();
}
// looking for a free variable inside of a monic to split
@ -1528,18 +1517,17 @@ void core::add_bounds() {
for (lpvar j : m.vars()) {
if (!var_is_free(j)) continue;
// split the free variable (j <= 0, or j > 0), and return
m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
++lp_settings().stats().m_nla_bounds;
return;
}
}
}
lbool core::check(vector<ineq>& lits) {
lbool core::check() {
lp_settings().stats().m_nla_calls++;
TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
lra.get_rid_of_inf_eps();
m_literal_vec = &lits;
if (!(lra.get_status() == lp::lp_status::OPTIMAL ||
lra.get_status() == lp::lp_status::FEASIBLE)) {
TRACE("nla_solver", tout << "unknown because of the lra.m_status = " << lra.get_status() << "\n";);
@ -1559,7 +1547,7 @@ lbool core::check(vector<ineq>& lits) {
bool run_bounded_nlsat = should_run_bounded_nlsat();
bool run_bounds = params().arith_nl_branching();
auto no_effect = [&]() { return !done() && m_lemmas.empty() && lits.empty(); };
auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty(); };
if (no_effect())
m_monomial_bounds.propagate();
@ -1577,7 +1565,7 @@ lbool core::check(vector<ineq>& lits) {
{1, check2},
{1, check3} };
check_weighted(3, checks);
if (!m_lemmas.empty() || !lits.empty())
if (!m_lemmas.empty() || !m_literals.empty())
return l_false;
}
@ -1656,9 +1644,8 @@ lbool core::bounded_nlsat() {
m_nlsat_fails = 0;
m_nlsat_delay /= 2;
}
if (ret == l_true) {
m_lemmas.reset();
}
if (ret == l_true)
clear();
return ret;
}
@ -1672,10 +1659,10 @@ bool core::no_lemmas_hold() const {
return true;
}
lbool core::test_check() {
vector<ineq> lits;
lra.set_status(lp::lp_status::OPTIMAL);
return check(lits);
return check();
}
std::ostream& core::print_terms(std::ostream& out) const {
@ -1826,162 +1813,13 @@ bool core::improve_bounds() {
}
return bounds_improved;
}
bool core::is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed) {
zero_var = non_fixed = null_lpvar;
unsigned n_of_non_fixed = 0;
for (lpvar v : m) {
if (!var_is_fixed(v)) {
n_of_non_fixed++;
non_fixed = v;
continue;
}
const auto& b = get_lower_bound(v);
if (b.is_zero()) {
zero_var = v;
return true;
}
}
return n_of_non_fixed <= 1;
void core::propagate() {
clear();
m_monomial_bounds.unit_propagate();
}
void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep) {
TRACE("add_bound", lra.print_column_info(j, tout) << std::endl;);
j = lra.column_to_reported_index(j);
unsigned k;
if (!m_improved_lower_bounds.find(j, k)) {
m_improved_lower_bounds.insert(j, static_cast<unsigned>(m_implied_bounds.size()));
m_implied_bounds.push_back(lp::implied_bound(v, j, true, is_strict, explain_dep));
}
else {
auto& found_bound = m_implied_bounds[k];
if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
found_bound = lp::implied_bound(v, j, true, is_strict, explain_dep);
TRACE("add_bound", lra.print_implied_bound(found_bound, tout););
}
}
}
void core::add_upper_bound_monic(lpvar j, const lp::mpq& bound_val, bool is_strict, std::function<u_dependency*()> explain_dep) {
j = lra.column_to_reported_index(j);
unsigned k;
if (!m_improved_upper_bounds.find(j, k)) {
m_improved_upper_bounds.insert(j, static_cast<unsigned>(m_implied_bounds.size()));
m_implied_bounds.push_back(lp::implied_bound(bound_val, j, false, is_strict, explain_dep));
}
else {
auto& found_bound = m_implied_bounds[k];
if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
found_bound = lp::implied_bound(bound_val, j, false, is_strict, explain_dep);
TRACE("add_bound", lra.print_implied_bound(found_bound, tout););
}
}
}
bool core::upper_bound_is_available(unsigned j) const {
switch (get_column_type(j)) {
case lp::column_type::fixed:
case lp::column_type::boxed:
case lp::column_type::upper_bound:
return true;
default:
return false;
}
}
bool core::lower_bound_is_available(unsigned j) const {
switch (get_column_type(j)) {
case lp::column_type::fixed:
case lp::column_type::boxed:
case lp::column_type::lower_bound:
return true;
default:
return false;
}
}
} // end of nla
void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k) {
auto* lps = &lra;
auto lambda = [vars, lps]() { return lps->get_bound_constraint_witnesses_for_columns(vars); };
add_lower_bound_monic(monic_var, k, false, lambda);
add_upper_bound_monic(monic_var, k, false, lambda);
}
void core::add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) {
auto* lps = &lra;
auto lambda = [zero_var, lps]() {
return lps->get_bound_constraint_witnesses_for_column(zero_var);
};
TRACE("add_bound", lra.print_column_info(zero_var, tout) << std::endl;);
add_lower_bound_monic(monic_var, lp::mpq(0), false, lambda);
add_upper_bound_monic(monic_var, lp::mpq(0), false, lambda);
}
void core::propagate_monic_non_fixed_with_lemma(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
lp::impq bound_value;
new_lemma lemma(*this, "propagate monic with non fixed");
// using += to not assert thath the inequality does not hold
lemma += ineq(term(rational(1), monic_var, -k, non_fixed), llc::EQ, 0);
lp::explanation exp;
for (auto v : m_emons[monic_var].vars()) {
if (v == non_fixed) continue;
u_dependency* dep = lra.get_column_lower_bound_witness(v);
for (auto ci : lra.flatten(dep)) {
exp.push_back(ci);
}
dep = lra.get_column_upper_bound_witness(v);
for (auto ci : lra.flatten(dep)) {
exp.push_back(ci);
}
}
lemma &= exp;
}
void core::calculate_implied_bounds_for_monic(lp::lpvar monic_var) {
if (!is_monic_var(monic_var)) return;
m_propagated.reserve(monic_var + 1, false);
bool throttle = params().arith_nl_throttle_unit_prop();
if (throttle && m_propagated[monic_var])
return;
lpvar non_fixed, zero_var;
const auto& vars = m_emons[monic_var].vars();
if (!is_linear(vars, zero_var, non_fixed))
return;
if (throttle)
trail().push(set_bitvector_trail(m_propagated, monic_var));
if (zero_var != null_lpvar)
add_bounds_for_zero_var(monic_var, zero_var);
else {
rational k = rational(1);
for (auto v : vars)
if (v != non_fixed) {
k *= val(v);
if (k.is_big()) return;
}
if (non_fixed != null_lpvar)
m_monomial_bounds.propagate_nonfixed(monic_var, vars, non_fixed, k);
else // all variables are fixed
propagate_monic_with_all_fixed(monic_var, vars, k);
}
}
void core::init_bound_propagation() {
m_implied_bounds.clear();
m_improved_lower_bounds.reset();
m_improved_upper_bounds.reset();
m_column_types = &lra.get_column_types();
m_lemmas.clear();
// find m_monics_with_changed_bounds
for (lpvar j : lra.columns_with_changed_bounds()) {
if (is_monic_var(j))
m_monics_with_changed_bounds.insert(j);
else {
for (const auto & m: m_emons.get_use_list(j)) {
m_monics_with_changed_bounds.insert(m.var());
}
}
}
}
} // namespace nla

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

@ -44,7 +44,6 @@ bool try_insert(const A& elem, B& collection) {
return true;
}
class core {
friend struct common;
friend class new_lemma;
@ -86,9 +85,10 @@ class core {
smt_params_helper m_params;
std::function<bool(lpvar)> m_relevant;
vector<lemma> m_lemmas;
vector<ineq> * m_literal_vec = nullptr;
vector<ineq> m_literals;
vector<equality> m_equalities;
vector<fixed_equality> m_fixed_equalities;
indexed_uint_set m_to_refine;
indexed_uint_set m_monics_with_changed_bounds;
tangents m_tangents;
basics m_basics;
order m_order;
@ -97,16 +97,13 @@ class core {
divisions m_divisions;
intervals m_intervals;
monomial_bounds m_monomial_bounds;
unsigned m_conflicts;
horner m_horner;
grobner m_grobner;
emonics m_emons;
svector<lpvar> m_add_buffer;
mutable indexed_uint_set m_active_var_set;
// these maps map a column index to the corresponding index in ibounds
u_map<unsigned> m_improved_lower_bounds;
u_map<unsigned> m_improved_upper_bounds;
const vector<lp::column_type>* m_column_types;
reslimit m_nra_lim;
bool m_use_nra_model = false;
@ -114,17 +111,16 @@ class core {
bool m_cautious_patching = true;
lpvar m_patched_var = 0;
monic const* m_patched_monic = nullptr;
bool_vector m_propagated;
void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
void add_bounds();
std_vector<lp::implied_bound> & m_implied_bounds;
// try to improve bounds for variables in monomials.
bool improve_bounds();
void clear_monics_with_changed_bounds() { m_monics_with_changed_bounds.reset(); }
public:
// constructor
core(lp::lar_solver& s, params_ref const& p, reslimit&, std_vector<lp::implied_bound> & implied_bounds);
const auto& monics_with_changed_bounds() const { return m_monics_with_changed_bounds; }
core(lp::lar_solver& s, params_ref const& p, reslimit&);
void insert_to_refine(lpvar j);
void erase_from_to_refine(lpvar j);
@ -314,7 +310,6 @@ public:
bool sign_contradiction(const monic& m) const;
bool var_is_fixed_to_zero(lpvar j) const;
bool fixed_var_has_big_bound(lpvar j) const;
bool var_is_fixed_to_val(lpvar j, const rational& v) const;
bool var_is_fixed(lpvar j) const;
@ -392,11 +387,13 @@ public:
bool conflict_found() const;
lbool check(vector<ineq>& ineqs);
lbool check();
lbool check_power(lpvar r, lpvar x, lpvar y);
void check_bounded_divisions();
bool no_lemmas_hold() const;
void propagate();
lbool test_check();
lpvar map_to_root(lpvar) const;
@ -432,26 +429,22 @@ public:
void set_use_nra_model(bool m);
bool use_nra_model() const { return m_use_nra_model; }
void collect_statistics(::statistics&);
vector<nla::lemma> const& lemmas() const { return m_lemmas; }
vector<nla::ineq> const& literals() const { return m_literals; }
vector<equality> const& equalities() const { return m_equalities; }
vector<fixed_equality> const& fixed_equalities() const { return m_fixed_equalities; }
bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed);
void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var);
void propagate_monic_non_fixed_with_lemma(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k);
void propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k);
void add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep);
void add_upper_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep);
bool upper_bound_is_available(unsigned j) const;
bool lower_bound_is_available(unsigned j) const;
vector<nla::lemma> const& lemmas() const { return m_lemmas; }
void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); }
void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); }
private:
lp::column_type get_column_type(unsigned j) const { return (*m_column_types)[j]; }
void restore_patched_values();
void constrain_nl_in_tableau();
bool solve_tableau();
void restore_tableau();
void save_tableau();
bool integrality_holds();
void calculate_implied_bounds_for_monic(lp::lpvar v);
void init_bound_propagation();
}; // end of core
struct pp_mon {

41
src/math/lp/nla_solver.cpp
View file

@ -42,10 +42,14 @@ namespace nla {
bool solver::need_check() { return m_core->has_relevant_monomial(); }
lbool solver::check(vector<ineq>& lits) {
return m_core->check(lits);
lbool solver::check() {
return m_core->check();
}
void solver::propagate() {
m_core->propagate();
}
void solver::push(){
m_core->push();
}
@ -54,8 +58,8 @@ namespace nla {
m_core->pop(n);
}
solver::solver(lp::lar_solver& s, params_ref const& p, reslimit& limit, std_vector<lp::implied_bound> & implied_bounds):
m_core(alloc(core, s, p, limit, implied_bounds)) {
solver::solver(lp::lar_solver& s, params_ref const& p, reslimit& limit):
m_core(alloc(core, s, p, limit)) {
}
bool solver::influences_nl_var(lpvar j) const {
@ -88,9 +92,6 @@ namespace nla {
m_core->collect_statistics(st);
}
void solver::calculate_implied_bounds_for_monic(lp::lpvar v) {
m_core->calculate_implied_bounds_for_monic(v);
}
// ensure r = x^y, add abstraction/refinement lemmas
lbool solver::check_power(lpvar r, lpvar x, lpvar y) {
return m_core->check_power(r, x, y);
@ -100,22 +101,20 @@ namespace nla {
m_core->check_bounded_divisions();
}
void solver::init_bound_propagation() {
m_core->init_bound_propagation();
}
vector<nla::lemma> const& solver::lemmas() const {
return m_core->lemmas();
}
void solver::propagate_bounds_for_touched_monomials() {
init_bound_propagation();
for (unsigned v : m_core->monics_with_changed_bounds()) {
calculate_implied_bounds_for_monic(v);
if (m_core->lra.get_status() == lp::lp_status::INFEASIBLE) {
break;
}
}
m_core->clear_monics_with_changed_bounds();
vector<nla::ineq> const& solver::literals() const {
return m_core->literals();
}
vector<nla::equality> const& solver::equalities() const {
return m_core->equalities();
}
vector<nla::fixed_equality> const& solver::fixed_equalities() const {
return m_core->fixed_equalities();
}
}

15
src/math/lp/nla_solver.h
View file

@ -23,9 +23,10 @@ namespace nla {
class solver {
core* m_core;
public:
solver(lp::lar_solver& s, params_ref const& p, reslimit& limit, std_vector<lp::implied_bound> & implied_bounds);
solver(lp::lar_solver& s, params_ref const& p, reslimit& limit);
~solver();
void add_monic(lpvar v, unsigned sz, lpvar const* vs);
void add_idivision(lpvar q, lpvar x, lpvar y);
void add_rdivision(lpvar q, lpvar x, lpvar y);
@ -35,7 +36,7 @@ namespace nla {
void push();
void pop(unsigned scopes);
bool need_check();
lbool check(vector<ineq>& lits);
lbool check();
void propagate();
lbool check_power(lpvar r, lpvar x, lpvar y);
bool is_monic_var(lpvar) const;
@ -46,9 +47,9 @@ namespace nla {
nlsat::anum_manager& am();
nlsat::anum const& am_value(lp::var_index v) const;
void collect_statistics(::statistics & st);
void calculate_implied_bounds_for_monic(lp::lpvar v);
void init_bound_propagation();
vector<nla::lemma> const& lemmas() const;
void propagate_bounds_for_touched_monomials();
vector<nla::lemma> const& lemmas() const;
vector<nla::ineq> const& literals() const;
vector<nla::fixed_equality> const& fixed_equalities() const;
vector<nla::equality> const& equalities() const;
};
}

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

@ -24,6 +24,20 @@ namespace nla {
typedef lp::explanation expl_set;
typedef lp::var_index lpvar;
const lpvar null_lpvar = UINT_MAX;
struct equality {
lp::lpvar i, j;
lp::explanation e;
equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e):i(i),j(j),e(e) {}
};
struct fixed_equality {
lp::lpvar v;
rational k;
lp::explanation e;
fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e):v(v),k(k),e(e) {}
};
inline int rat_sign(const rational& r) { return r.is_pos()? 1 : ( r.is_neg()? -1 : 0); }
inline rational rrat_sign(const rational& r) { return rational(rat_sign(r)); }
@ -83,7 +97,6 @@ namespace nla {
new_lemma& operator&=(const factorization& f);
new_lemma& operator&=(lpvar j);
new_lemma& operator|=(ineq const& i);
new_lemma& operator+=(ineq const& i);
new_lemma& explain_fixed(lpvar j);
new_lemma& explain_equiv(lpvar u, lpvar v);
new_lemma& explain_var_separated_from_zero(lpvar j);

2
src/sat/smt/arith_internalize.cpp
View file

@ -61,7 +61,7 @@ namespace arith {
void solver::ensure_nla() {
if (!m_nla) {
m_nla = alloc(nla::solver, *m_solver.get(), s().params(), m.limit(), m_implied_bounds);
m_nla = alloc(nla::solver, *m_solver.get(), s().params(), m.limit());
for (auto const& _s : m_scopes) {
(void)_s;
m_nla->push();

6
src/sat/smt/arith_solver.cpp
View file

@ -253,7 +253,7 @@ namespace arith {
first = false;
reset_evidence();
m_explanation.clear();
be.explain_implied();
lp().explain_implied_bound(be, m_bp);
}
CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
updt_unassigned_bounds(v, -1);
@ -1416,7 +1416,7 @@ namespace arith {
}
void solver::assume_literals() {
for (auto const& ineq : m_nla_literals) {
for (auto const& ineq : m_nla->literals()) {
auto lit = mk_ineq_literal(ineq);
ctx.mark_relevant(lit);
s().set_phase(lit);
@ -1459,7 +1459,7 @@ namespace arith {
return l_true;
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_nla->check(m_nla_literals);
lbool r = m_nla->check();
switch (r) {
case l_false:
assume_literals();

1
src/sat/smt/arith_solver.h
View file

@ -249,7 +249,6 @@ namespace arith {
// lemmas
lp::explanation m_explanation;
vector<nla::ineq> m_nla_literals;
literal_vector m_core, m_core2;
vector<rational> m_coeffs;
svector<enode_pair> m_eqs;

6
src/sat/smt/euf_proof_checker.cpp
View file

@ -501,8 +501,9 @@ namespace euf {
for (expr* arg : clause)
std::cout << "\n " << mk_bounded_pp(arg, m);
std::cout << ")\n";
std::cout.flush();
if (is_rup(proof_hint))
if (false && is_rup(proof_hint))
diagnose_rup_failure(clause);
add_clause(clause);
@ -527,9 +528,6 @@ namespace euf {
for (expr* f : core)
std::cout << mk_pp(f, m) << "\n";
}
SASSERT(false);
exit(0);
}
void smt_proof_checker::collect_statistics(statistics& st) const {

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

@ -71,8 +71,6 @@ def_module_params(module_name='smt',
('arith.nl.grobner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'),
('arith.nl.grobner_frequency', UINT, 4, 'grobner\'s call frequency'),
('arith.nl.grobner', BOOL, True, 'run grobner\'s basis heuristic'),
('arith.nl.use_lemmas_in_unit_prop', BOOL, False, 'use lemmas in monomial unit propagation'),
('arith.nl.throttle_unit_prop', BOOL, True, 'unit propogate a monomial only once per scope'),
('arith.nl.grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '),
('arith.nl.grobner_expr_size_growth', UINT, 2, 'grobner\'s maximum expr size growth'),
('arith.nl.grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'),

22
src/smt/smt_clause_proof.cpp
View file

@ -90,14 +90,14 @@ namespace smt {
return proof_ref(m);
}
void clause_proof::add(clause& c) {
void clause_proof::add(clause& c, literal_buffer const* simp_lits) {
if (!is_enabled())
return;
justification* j = c.get_justification();
auto st = kind2st(c.get_kind());
auto pr = justification2proof(st, j);
CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
update(c, st, pr);
update(c, st, pr, simp_lits);
}
void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) {
@ -137,12 +137,15 @@ namespace smt {
update(st, m_lits, pr);
}
void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j) {
void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits) {
if (!is_enabled())
return;
m_lits.reset();
m_lits.push_back(ctx.literal2expr(lit1));
m_lits.push_back(ctx.literal2expr(lit2));
if (simp_lits)
for (auto lit : *simp_lits)
m_lits.push_back(ctx.literal2expr(~lit));
auto st = kind2st(k);
auto pr = justification2proof(st, j);
update(st, m_lits, pr);
@ -160,7 +163,7 @@ namespace smt {
}
void clause_proof::del(clause& c) {
update(c, status::deleted, justification2proof(status::deleted, nullptr));
update(c, status::deleted, justification2proof(status::deleted, nullptr), nullptr);
}
std::ostream& clause_proof::display_literals(std::ostream& out, expr_ref_vector const& v) {
@ -190,7 +193,9 @@ namespace smt {
if (ctx.get_fparams().m_clause_proof)
m_trail.push_back(info(st, v, p));
if (m_on_clause_eh)
m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());
m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());
static unsigned s_count = 0;
if (m_has_log) {
init_pp_out();
auto& out = *m_pp_out;
@ -220,12 +225,15 @@ namespace smt {
}
}
void clause_proof::update(clause& c, status st, proof* p) {
void clause_proof::update(clause& c, status st, proof* p, literal_buffer const* simp_lits) {
if (!is_enabled())
return;
m_lits.reset();
for (literal lit : c)
m_lits.push_back(ctx.literal2expr(lit));
m_lits.push_back(ctx.literal2expr(lit));
if (simp_lits)
for (auto lit : *simp_lits)
m_lits.push_back(ctx.literal2expr(~lit));
update(st, m_lits, p);
}

6
src/smt/smt_clause_proof.h
View file

@ -68,7 +68,7 @@ namespace smt {
void init_pp_out();
void update(status st, expr_ref_vector& v, proof* p);
void update(clause& c, status st, proof* p);
void update(clause& c, status st, proof* p, literal_buffer const* simp_lits);
status kind2st(clause_kind k);
proof_ref justification2proof(status st, justification* j);
void log(status st, proof* p);
@ -79,8 +79,8 @@ namespace smt {
clause_proof(context& ctx);
void shrink(clause& c, unsigned new_size);
void add(literal lit, clause_kind k, justification* j);
void add(literal lit1, literal lit2, clause_kind k, justification* j);
void add(clause& c);
void add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits = nullptr);
void add(clause& c, literal_buffer const* simp_lits = nullptr);
void add(unsigned n, literal const* lits, clause_kind k, justification* j);
void propagate(literal lit, justification const& j, literal_vector const& ante);
void del(clause& c);

1
src/smt/smt_conflict_resolution.cpp
View file

@ -601,6 +601,7 @@ namespace smt {
finalize_resolve(conflict, not_l);
return true;
}

6
src/smt/smt_internalizer.cpp
View file

@ -1378,12 +1378,12 @@ namespace smt {
clause * context::mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k, clause_del_eh * del_eh) {
TRACE("mk_clause", display_literals_verbose(tout << "creating clause: " << literal_vector(num_lits, lits) << "\n", num_lits, lits) << "\n";);
m_clause_proof.add(num_lits, lits, k, j);
literal_buffer simp_lits;
switch (k) {
case CLS_TH_AXIOM:
dump_axiom(num_lits, lits);
Z3_fallthrough;
case CLS_AUX: {
literal_buffer simp_lits;
if (m_searching)
dump_lemma(num_lits, lits);
if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) {
@ -1451,7 +1451,7 @@ namespace smt {
else if (get_assignment(l2) == l_false) {
assign(l1, b_justification(~l2));
}
m_clause_proof.add(l1, l2, k, j);
m_clause_proof.add(l1, l2, k, j, &simp_lits);
m_stats.m_num_mk_bin_clause++;
return nullptr;
}
@ -1464,7 +1464,7 @@ namespace smt {
bool reinit = save_atoms;
SASSERT(!lemma || j == 0 || !j->in_region());
clause * cls = clause::mk(m, num_lits, lits, k, j, del_eh, save_atoms, m_bool_var2expr.data());
m_clause_proof.add(*cls);
m_clause_proof.add(*cls, &simp_lits);
if (lemma) {
cls->set_activity(activity);
if (k == CLS_LEARNED) {

3
src/smt/theory_arith_aux.h
View file

@ -1535,7 +1535,8 @@ namespace smt {
m_stats.m_max_min++;
unsigned best_efforts = 0;
bool inc = false;
SASSERT(!maintain_integrality || valid_assignment());
SASSERT(satisfy_bounds());

15
src/smt/theory_arith_nl.h
View file

@ -765,10 +765,8 @@ typename theory_arith<Ext>::numeral theory_arith<Ext>::get_monomial_fixed_var_pr
template<typename Ext>
expr * theory_arith<Ext>::get_monomial_non_fixed_var(expr * m) const {
SASSERT(is_pure_monomial(m));
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i);
theory_var _var = expr2var(arg);
if (!is_fixed(_var))
for (expr* arg : *to_app(m)) {
if (!is_fixed(expr2var(arg)))
return arg;
}
return nullptr;
@ -780,7 +778,7 @@ expr * theory_arith<Ext>::get_monomial_non_fixed_var(expr * m) const {
*/
template<typename Ext>
bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
TRACE("non_linear", tout << "checking whether v" << v << " became linear...\n";);
TRACE("non_linear_verbose", tout << "checking whether v" << v << " became linear...\n";);
if (m_data[v].m_nl_propagated)
return false; // already propagated this monomial.
expr * m = var2expr(v);
@ -819,6 +817,11 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
ctx.mark_as_relevant(rhs);
}
TRACE("non_linear_bug", tout << "enode: " << ctx.get_enode(rhs) << " enode_id: " << ctx.get_enode(rhs)->get_owner_id() << "\n";);
IF_VERBOSE(3,
for (auto* arg : *to_app(m))
if (is_fixed(expr2var(arg)))
verbose_stream() << mk_pp(arg, get_manager()) << " = " << -k << "\n");
theory_var new_v = expr2var(rhs);
SASSERT(new_v != null_theory_var);
new_lower = alloc(derived_bound, new_v, inf_numeral(0), B_LOWER);
@ -906,7 +909,7 @@ bool theory_arith<Ext>::propagate_linear_monomials() {
return false;
if (!reflection_enabled())
return false;
TRACE("non_linear", tout << "propagating linear monomials...\n";);
TRACE("non_linear_verbose", tout << "propagating linear monomials...\n";);
bool p = false;
// CMW: m_nl_monomials can grow during this loop, so
// don't use iterators.

120
src/smt/theory_lra.cpp
View file

@ -264,7 +264,7 @@ class theory_lra::imp {
void ensure_nla() {
if (!m_nla) {
m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit(), m_implied_bounds);
m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit());
for (auto const& _s : m_scopes) {
(void)_s;
m_nla->push();
@ -1528,14 +1528,12 @@ public:
unsigned old_sz = m_assume_eq_candidates.size();
unsigned num_candidates = 0;
int start = ctx().get_random_value();
unsigned num_relevant = 0;
for (theory_var i = 0; i < sz; ++i) {
theory_var v = (i + start) % sz;
enode* n1 = get_enode(v);
if (!th.is_relevant_and_shared(n1)) {
continue;
}
++num_relevant;
ensure_column(v);
if (!is_registered_var(v))
continue;
@ -1553,7 +1551,7 @@ public:
num_candidates++;
}
}
if (num_candidates > 0) {
ctx().push_trail(restore_vector(m_assume_eq_candidates, old_sz));
}
@ -1605,8 +1603,7 @@ public:
case l_true:
return FC_DONE;
case l_false:
for (const nla::lemma & l : m_nla->lemmas())
false_case_of_check_nla(l);
add_lemmas();
return FC_CONTINUE;
case l_undef:
return FC_GIVEUP;
@ -1803,8 +1800,7 @@ public:
if (!m_nla)
return true;
m_nla->check_bounded_divisions();
for (auto & lemma : m_nla->lemmas())
false_case_of_check_nla(lemma);
add_lemmas();
return m_nla->lemmas().empty();
}
@ -2003,7 +1999,7 @@ public:
// create term >= 0 (or term <= 0)
atom = mk_bound(ineq.term(), ineq.rs(), is_lower);
return literal(ctx().get_bool_var(atom), pos);
}
}
void false_case_of_check_nla(const nla::lemma & l) {
m_lemma = l; //todo avoid the copy
@ -2024,14 +2020,11 @@ public:
final_check_status check_nla_continue() {
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_nla->check(m_nla_literals);
lbool r = m_nla->check();
switch (r) {
case l_false:
for (const nla::ineq& i : m_nla_literals)
assume_literal(i);
for (const nla::lemma & l : m_nla->lemmas())
false_case_of_check_nla(l);
add_lemmas();
return FC_CONTINUE;
case l_true:
return assume_eqs()? FC_CONTINUE: FC_DONE;
@ -2120,6 +2113,8 @@ public:
bool propagate_core() {
m_model_is_initialized = false;
flush_bound_axioms();
// disabled in master:
propagate_nla();
if (!can_propagate_core())
return false;
m_new_def = false;
@ -2151,7 +2146,6 @@ public:
break;
case l_true:
propagate_basic_bounds();
propagate_bounds_with_nlp();
propagate_bounds_with_lp_solver();
break;
case l_undef:
@ -2161,6 +2155,47 @@ public:
return true;
}
void propagate_nla() {
if (m_nla) {
m_nla->propagate();
add_lemmas();
add_equalities();
}
}
void add_equalities() {
if (!propagate_eqs())
return;
for (auto const& [v,k,e] : m_nla->fixed_equalities())
add_equality(v, k, e);
for (auto const& [i,j,e] : m_nla->equalities())
add_eq(i,j,e,false);
}
void add_equality(lpvar j, rational const& k, lp::explanation const& exp) {
//verbose_stream() << "equality " << j << " " << k << "\n";
TRACE("arith", tout << "equality " << j << " " << k << "\n");
theory_var v;
if (k == 1)
v = m_one_var;
else if (k == 0)
v = m_zero_var;
else if (!m_value2var.find(k, v))
return;
theory_var w = lp().local_to_external(j);
if (w < 0)
return;
lpvar i = register_theory_var_in_lar_solver(v);
add_eq(i, j, exp, true);
}
void add_lemmas() {
for (const nla::ineq& i : m_nla->literals())
assume_literal(i);
for (const nla::lemma & l : m_nla->lemmas())
false_case_of_check_nla(l);
}
bool should_propagate() const {
return bound_prop_mode::BP_NONE != propagation_mode();
}
@ -2173,50 +2208,33 @@ public:
set_evidence(j, m_core, m_eqs);
m_explanation.add_pair(j, v);
}
void propagate_bounds_with_lp_solver() {
if (!should_propagate())
return;
m_bp.init();
lp().propagate_bounds_for_touched_rows(m_bp);
if (!m.inc())
return;
void finish_bound_propagation() {
if (is_infeasible()) {
get_infeasibility_explanation_and_set_conflict();
// verbose_stream() << "unsat\n";
}
else {
for (auto &ib : m_bp.ibounds()) {
unsigned count = 0, prop = 0;
for (auto& ib : m_bp.ibounds()) {
m.inc();
if (ctx().inconsistent())
break;
propagate_lp_solver_bound(ib);
++prop;
count += propagate_lp_solver_bound(ib);
}
}
}
void propagate_bounds_with_lp_solver() {
if (!should_propagate())
return;
m_bp.init();
lp().propagate_bounds_for_touched_rows(m_bp);
if (m.inc())
finish_bound_propagation();
}
void propagate_bounds_for_monomials() {
m_nla->propagate_bounds_for_touched_monomials();
for (const auto & l : m_nla->lemmas())
false_case_of_check_nla(l);
}
void propagate_bounds_with_nlp() {
if (!m_nla)
return;
if (is_infeasible() || !should_propagate())
return;
propagate_bounds_for_monomials();
if (m.inc())
finish_bound_propagation();
}
bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const {
theory_var v = lp().local_to_external(vi);
if (v == null_theory_var)
@ -3161,8 +3179,7 @@ public:
std::function<expr*(void)> fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); };
scoped_trace_stream _sts(th, fn);
// SASSERT(validate_eq(x, y));
//VERIFY(validate_eq(x, y));
ctx().assign_eq(x, y, eq_justification(js));
}
@ -3206,12 +3223,11 @@ public:
}
lp::explanation m_explanation;
vector<nla::ineq> m_nla_literals;
literal_vector m_core;
svector<enode_pair> m_eqs;
vector<parameter> m_params;
void reset_evidence() {
void reset_evidence() {
m_core.reset();
m_eqs.reset();
m_params.reset();
@ -3278,6 +3294,7 @@ public:
display(tout << "is-conflict: " << is_conflict << "\n"););
for (auto ev : m_explanation)
set_evidence(ev.ci(), m_core, m_eqs);
// SASSERT(validate_conflict(m_core, m_eqs));
if (is_conflict) {
@ -3533,6 +3550,8 @@ public:
lbool r = nctx.check();
if (r == l_true) {
nctx.display_asserted_formulas(std::cout);
std::cout.flush();
std::cout.flush();
}
return l_true != r;
}
@ -3882,6 +3901,7 @@ public:
IF_VERBOSE(1, verbose_stream() << enode_pp(n, ctx()) << " evaluates to " << r2 << " but arith solver has " << r1 << "\n");
}
}
};
theory_lra::theory_lra(context& ctx):