diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 177cfb3d3..8bb6ab306 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -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;
+ }
+
}
diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h
index 76524012f..747aca9a2 100644
--- a/src/math/lp/monomial_bounds.h
+++ b/src/math/lp/monomial_bounds.h
@@ -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();
};
}
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 5a6af5659..6a241e951 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -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
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 76397d529..5a597ae67 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -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 {
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 53d8b0da6..f4d09810e 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -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();
+ }
+
}
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index acd724af9..fec27c32b 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -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;
};
}
diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h
index 186c2e902..3930a62a9 100644
--- a/src/math/lp/nla_types.h
+++ b/src/math/lp/nla_types.h
@@ -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);
diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 5893c8520..3174ad775 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -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();
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 893fe4a43..17ab03ee6 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -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();
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 53b49a658..801eb474c 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -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;
diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index a538b2a80..42cda4bfb 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -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 {
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index fca7fcacf..9fcda7f64 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -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'),
diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index 777961334..bf27777c4 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -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);
}
diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h
index 1c5931136..d7cc421cf 100644
--- a/src/smt/smt_clause_proof.h
+++ b/src/smt/smt_clause_proof.h
@@ -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);
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index d075c0652..2561fbb5a 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -601,6 +601,7 @@ namespace smt {
finalize_resolve(conflict, not_l);
+
return true;
}
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 0e9e39996..b6d1e2f2b 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -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) {
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index dd9ba2dfe..470ea5f7b 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -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());
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index ae0af89ec..0a2b6e938 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -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.
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2a7412c29..a5c5084ab 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -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):