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

generate lemmas from nla_intervals

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-14 17:32:07 -07:00
parent c121c5d2d8
commit 3f6ecfb3b6
13 changed files with 292 additions and 408 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

84
src/math/lp/bound_analyzer_on_row.h
View file

@ -30,7 +30,7 @@ namespace lp {
template <typename C> // C plays a role of a container template <typename C> // C plays a role of a container
class bound_analyzer_on_row { class bound_analyzer_on_row {
const C& m_row; const C& m_row;
lp_bound_propagator & m_bp; lp_bound_propagator & m_bp;
unsigned m_row_or_term_index; unsigned m_row_or_term_index;
int m_column_of_u; // index of an unlimited from above monoid int m_column_of_u; // index of an unlimited from above monoid
// -1 means that such a value is not found, -2 means that at least two of such monoids were found // -1 means that such a value is not found, -2 means that at least two of such monoids were found
@ -55,8 +55,9 @@ public :
m_rs(rs) m_rs(rs)
{} {}
unsigned j;
void analyze() { void analyze() {
TRACE("lp_bound_prop", print_linear_combination_of_column_indices_only(m_row, tout); tout << " = " << m_rs << "\n";);
for (const auto & c : m_row) { for (const auto & c : m_row) {
if ((m_column_of_l == -2) && (m_column_of_u == -2)) if ((m_column_of_l == -2) && (m_column_of_u == -2))
break; break;
@ -79,53 +80,86 @@ public :
} }
bool upper_bound_is_available(unsigned j) const { bool upper_bound_is_available(unsigned j) const {
return m_bp.upper_bound_is_available(j); switch (m_bp.get_column_type(j))
{
case column_type::fixed:
case column_type::boxed:
case column_type::upper_bound:
return true;
default:
return false;
}
} }
bool lower_bound_is_available(unsigned j) const { bool lower_bound_is_available(unsigned j) const {
return m_bp.lower_bound_is_available(j); switch (m_bp.get_column_type(j))
{
case column_type::fixed:
case column_type::boxed:
case column_type::lower_bound:
return true;
default:
return false;
}
} }
impq ub(unsigned j) const { const impq & ub(unsigned j) const {
lp_assert(upper_bound_is_available(j)); lp_assert(upper_bound_is_available(j));
return m_bp.get_upper_bound(j); return m_bp.get_upper_bound(j);
} }
impq lb(unsigned j) const { const impq & lb(unsigned j) const {
lp_assert(lower_bound_is_available(j)); lp_assert(lower_bound_is_available(j));
return m_bp.get_lower_bound(j); return m_bp.get_lower_bound(j);
} }
mpq u_strict(unsigned j, bool & strict) const {
const impq u = ub(j);
strict = !is_zero(u.y);
return u.x;
}
mpq l_strict(unsigned j, bool & strict) const { const mpq & monoid_max_no_mult(bool a_is_pos, unsigned j, bool & strict) const {
const impq l = lb(j); if (a_is_pos) {
strict = !is_zero(l.y); strict = !is_zero(ub(j).y);
return l.x; return ub(j).x;
} }
strict = !is_zero(lb(j).y);
mpq monoid_max_no_mult(bool a_is_pos, unsigned j, bool & strict) const { return lb(j).x;
return a_is_pos? u_strict(j, strict) : l_strict(j, strict);
} }
mpq monoid_max(const mpq & a, unsigned j) const { mpq monoid_max(const mpq & a, unsigned j) const {
return a * (is_pos(a) ? ub(j).x : lb(j).x); if (is_pos(a)) {
return a * ub(j).x;
}
return a * lb(j).x;
} }
mpq monoid_max(const mpq & a, unsigned j, bool & strict) const { mpq monoid_max(const mpq & a, unsigned j, bool & strict) const {
return a * (is_pos(a)? u_strict(j, strict) : l_strict(j, strict)); if (is_pos(a)) {
strict = !is_zero(ub(j).y);
return a * ub(j).x;
}
strict = !is_zero(lb(j).y);
return a * lb(j).x;
} }
mpq monoid_min_no_mult(bool a_is_pos, unsigned j, bool & strict) const { const mpq & monoid_min_no_mult(bool a_is_pos, unsigned j, bool & strict) const {
return a_is_pos? l_strict(j, strict) : u_strict(j, strict); if (!a_is_pos) {
strict = !is_zero(ub(j).y);
return ub(j).x;
}
strict = !is_zero(lb(j).y);
return lb(j).x;
} }
mpq monoid_min(const mpq & a, unsigned j, bool& strict) const { mpq monoid_min(const mpq & a, unsigned j, bool& strict) const {
return a * (is_neg(a)? u_strict(j, strict) : l_strict(j, strict)); if (is_neg(a)) {
strict = !is_zero(ub(j).y);
return a * ub(j).x;
}
strict = !is_zero(lb(j).y);
return a * lb(j).x;
} }
mpq monoid_min(const mpq & a, unsigned j) const { mpq monoid_min(const mpq & a, unsigned j) const {
return a * (is_neg(a)? ub(j).x : lb(j).x ); if (is_neg(a)) {
return a * ub(j).x;
}
return a * lb(j).x;
} }

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

@ -37,8 +37,10 @@ public:
m_explanation.push_back(std::make_pair(one_of_type<mpq>(), j)); m_explanation.push_back(std::make_pair(one_of_type<mpq>(), j));
} }
void add(const explanation& e) { for (auto j: e.m_set_of_ci) add(j); } void add(const explanation& e) { for (auto j: e.m_set_of_ci) add(j); }
template <typename T>
void add_expl(const T& e) { for (auto j: e) add(j); }
void add(unsigned ci) { push_justification(ci); } void add(unsigned ci) { push_justification(ci); }
void add(const std::pair<mpq, constraint_index>& j) { push_justification(j.second, j.first); } void add(const std::pair<mpq, constraint_index>& j) { push_justification(j.second, j.first); }

21
src/math/lp/lar_solver.cpp
View file

@ -224,6 +224,27 @@ void lar_solver::propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagat
} }
void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp) {
unsigned i = ib.m_row_or_term_index;
int bound_sign = ib.m_is_lower_bound? 1: -1;
int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
unsigned bound_j = ib.m_j;
if (is_term(bound_j)) {
bound_j = m_var_register.external_to_local(bound_j);
}
for (auto const& r : A_r().m_rows[i]) {
unsigned j = r.var();
if (j == bound_j) continue;
mpq const& a = r.get_val();
int a_sign = is_pos(a)? 1: -1;
int sign = j_sign * a_sign;
const ul_pair & ul = m_columns_to_ul_pairs[j];
auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
lp_assert(is_valid(witness));
bp.consume(a, witness);
}
// lp_assert(implied_bound_is_correctly_explained(ib, explanation));
}
bool lar_solver::term_is_used_as_row(unsigned term) const { bool lar_solver::term_is_used_as_row(unsigned term) const {
lp_assert(is_term(term)); lp_assert(is_term(term));

6
src/math/lp/lar_solver.h
View file

@ -315,6 +315,10 @@ public:
void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset); void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset);
void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp);
bool term_is_used_as_row(unsigned term) const; bool term_is_used_as_row(unsigned term) const;
void propagate_bounds_on_terms(lp_bound_propagator & bp); void propagate_bounds_on_terms(lp_bound_propagator & bp);
@ -392,6 +396,8 @@ public:
bool use_tableau_costs() const; bool use_tableau_costs() const;
void detect_rows_of_column_with_bound_change(unsigned j);
void adjust_x_of_column(unsigned j); void adjust_x_of_column(unsigned j);
bool row_is_correct(unsigned i) const; bool row_is_correct(unsigned i) const;

133
src/math/lp/lp_bound_propagator.cpp
View file

@ -3,86 +3,19 @@
Author: Lev Nachmanson Author: Lev Nachmanson
*/ */
#include "math/lp/lar_solver.h" #include "math/lp/lar_solver.h"
#include "math/lp/nla_solver.h"
namespace lp { namespace lp {
lp_bound_propagator::lp_bound_propagator(lar_solver & ls):
lp_bound_propagator::lp_bound_propagator(lar_solver & ls, nla::solver* nla): m_lar_solver(ls) {}
m_lar_solver(ls), m_nla_solver(nla) {}
column_type lp_bound_propagator::get_column_type(unsigned j) const { column_type lp_bound_propagator::get_column_type(unsigned j) const {
return m_lar_solver.m_mpq_lar_core_solver.m_column_types()[j]; return m_lar_solver.m_mpq_lar_core_solver.m_column_types()[j];
} }
const impq & lp_bound_propagator::get_lower_bound(unsigned j) const {
bool lp_bound_propagator::lower_bound_is_available(unsigned j) const { return m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j];
if (lower_bound_is_available_for_column(j))
return true;
if (!m_nla_solver->is_monomial_var(j))
return false;
return m_nla_solver->monomial_has_lower_bound(j);
} }
const impq & lp_bound_propagator::get_upper_bound(unsigned j) const {
bool lp_bound_propagator::upper_bound_is_available_for_column(unsigned j) const { return m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j];
switch (get_column_type(j)) {
case column_type::fixed:
case column_type::boxed:
case column_type::upper_bound:
return true;
default:
return false;
}
} }
bool lp_bound_propagator::lower_bound_is_available_for_column(unsigned j) const {
switch (get_column_type(j)) {
case column_type::fixed:
case column_type::boxed:
case column_type::lower_bound:
return true;
default:
return false;
}
}
bool lp_bound_propagator::upper_bound_is_available(unsigned j) const {
if (upper_bound_is_available_for_column(j))
return true;
if (!m_nla_solver->is_monomial_var(j))
return false;
return m_nla_solver->monomial_has_upper_bound(j);
}
bool lp_bound_propagator::nl_monomial_upper_bound_is_available(unsigned j) const {
return m_nla_solver && m_nla_solver->is_monomial_var(j)
&&
m_nla_solver->monomial_has_upper_bound(j);
}
bool lp_bound_propagator::nl_monomial_lower_bound_is_available(unsigned j) const {
return m_nla_solver && m_nla_solver->is_monomial_var(j)
&&
m_nla_solver->monomial_has_lower_bound(j);
}
impq lp_bound_propagator::get_lower_bound(unsigned j) const {
lp_assert(lower_bound_is_available(j));
if (lower_bound_is_available_for_column(j)) {
const impq& l = m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j];
return nl_monomial_lower_bound_is_available(j)?
std::max(l, m_nla_solver->get_lower_bound(j)) : l;
}
return m_nla_solver->get_lower_bound(j);
}
impq lp_bound_propagator::get_upper_bound(unsigned j) const {
lp_assert(upper_bound_is_available(j));
if (upper_bound_is_available_for_column(j)) {
const impq& l = m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j];
return nl_monomial_upper_bound_is_available(j)?
std::min(l, m_nla_solver->get_upper_bound(j)) : l;
}
return m_nla_solver->get_upper_bound(j);
}
void lp_bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { void lp_bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
CTRACE("nla_solver", m_nla_solver && m_nla_solver->is_monomial_var(j), tout << "mon_var = " << j << "\n"; );
j = m_lar_solver.adjust_column_index_to_term_index(j); j = m_lar_solver.adjust_column_index_to_term_index(j);
lconstraint_kind kind = is_low? GE : LE; lconstraint_kind kind = is_low? GE : LE;
@ -118,58 +51,4 @@ void lp_bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool co
} }
} }
} }
bool lp_bound_propagator::nl_monomial_upper_bound_should_be_taken(unsigned j) const {
return (!upper_bound_is_available_for_column(j)) || (
nl_monomial_upper_bound_is_available(j) && m_nla_solver->get_upper_bound(j) < m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j]);
} }
bool lp_bound_propagator::nl_monomial_lower_bound_should_be_taken(unsigned j) const {
lp_assert(lower_bound_is_available(j));
return (!lower_bound_is_available_for_column(j)) || (nl_monomial_lower_bound_is_available(j) && m_nla_solver->get_lower_bound(j) > m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j]);
}
void lp_bound_propagator::explain_implied_bound(implied_bound & ib) {
unsigned i = ib.m_row_or_term_index;
int bound_sign = ib.m_is_lower_bound? 1: -1;
int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
unsigned bound_j = ib.m_j;
if (m_lar_solver.is_term(bound_j)) {
bound_j = m_lar_solver.m_var_register.external_to_local(bound_j);
}
for (auto const& r : m_lar_solver.A_r().m_rows[i]) {
unsigned j = r.var();
if (j == bound_j) continue;
mpq const& a = r.get_val();
int a_sign = is_pos(a)? 1: -1;
int sign = j_sign * a_sign;
if (sign > 0) {
if (nl_monomial_upper_bound_should_be_taken(j)) {
TRACE("nla_intervals", tout << "using the monomial upper bound\n";);
svector<lp::constraint_index> expl;
m_nla_solver->get_explanation_of_upper_bound_for_monomial(j, expl);
for (auto c : expl)
consume(a, c);
} else {
const ul_pair & ul = m_lar_solver.m_columns_to_ul_pairs[j];
auto witness = ul.upper_bound_witness();
lp_assert(is_valid(witness));
consume(a, witness);
}
} else {
if (nl_monomial_lower_bound_should_be_taken(j)) {
TRACE("nla_intervals", tout << "using the monomial lower bound\n";);
svector<lp::constraint_index> expl;
m_nla_solver->get_explanation_of_lower_bound_for_monomial(j, expl);
for (auto c : expl)
consume(a, c);
} else {
const ul_pair & ul = m_lar_solver.m_columns_to_ul_pairs[j];
auto witness = ul.lower_bound_witness();
lp_assert(is_valid(witness));
consume(a, witness);
}
}
}
}
} // end of namespace lp

21
src/math/lp/lp_bound_propagator.h
View file

@ -4,39 +4,24 @@
*/ */
#pragma once #pragma once
#include "math/lp/lp_settings.h" #include "math/lp/lp_settings.h"
namespace nla {
// forward definition
class solver;
}
namespace lp { namespace lp {
class lar_solver; class lar_solver;
class lp_bound_propagator { class lp_bound_propagator {
std::unordered_map<unsigned, unsigned> m_improved_lower_bounds; // these maps map a column index to the corresponding index in ibounds std::unordered_map<unsigned, unsigned> m_improved_lower_bounds; // these maps map a column index to the corresponding index in ibounds
std::unordered_map<unsigned, unsigned> m_improved_upper_bounds; std::unordered_map<unsigned, unsigned> m_improved_upper_bounds;
lar_solver & m_lar_solver; lar_solver & m_lar_solver;
nla::solver * m_nla_solver;
public: public:
vector<implied_bound> m_ibounds; vector<implied_bound> m_ibounds;
public: public:
lp_bound_propagator(lar_solver & ls, nla::solver * nla); lp_bound_propagator(lar_solver & ls);
column_type get_column_type(unsigned) const; column_type get_column_type(unsigned) const;
const impq & get_lower_bound(unsigned) const;
bool lower_bound_is_available_for_column(unsigned) const; const impq & get_upper_bound(unsigned) const;
bool upper_bound_is_available_for_column(unsigned) const;
bool lower_bound_is_available(unsigned) const;
bool upper_bound_is_available(unsigned) const;
impq get_lower_bound(unsigned) const;
impq get_upper_bound(unsigned) const;
void try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict); void try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict);
virtual bool bound_is_interesting(unsigned vi, virtual bool bound_is_interesting(unsigned vi,
lp::lconstraint_kind kind, lp::lconstraint_kind kind,
const rational & bval) {return true;} const rational & bval) {return true;}
unsigned number_of_found_bounds() const { return m_ibounds.size(); } unsigned number_of_found_bounds() const { return m_ibounds.size(); }
void explain_implied_bound(implied_bound & ib);
virtual void consume(mpq const& v, lp::constraint_index j) = 0; virtual void consume(mpq const& v, lp::constraint_index j) = 0;
bool nl_monomial_upper_bound_is_available(unsigned) const;
bool nl_monomial_lower_bound_is_available(unsigned) const;
bool nl_monomial_lower_bound_should_be_taken(unsigned) const;
bool nl_monomial_upper_bound_should_be_taken(unsigned) const;
}; };
} }

14
src/math/lp/nla_basics_lemmas.cpp
View file

@ -251,15 +251,15 @@ bool basics::basic_lemma(bool derived) {
if (basic_sign_lemma(derived)) if (basic_sign_lemma(derived))
return true; return true;
if (derived) if (derived)
return false; return c().m_intervals.get_lemmas();
const auto& rm_ref = c().m_to_refine; const auto& mon_inds_to_ref = c().m_to_refine;
TRACE("nla_solver", tout << "rm_ref = "; print_vector(rm_ref, tout);); TRACE("nla_solver", tout << "mon_inds_to_ref = "; print_vector(mon_inds_to_ref, tout););
unsigned start = c().random(); unsigned start = c().random();
unsigned sz = rm_ref.size(); unsigned sz = mon_inds_to_ref.size();
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
lpvar v = rm_ref[(j + start) % rm_ref.size()]; lpvar v = mon_inds_to_ref[(j + start) % mon_inds_to_ref.size()];
const monomial& r = c().m_emons[v]; const monomial& r = c().emons()[v];
SASSERT (!c().check_monomial(c().m_emons[v])); SASSERT (!c().check_monomial(c().emons()[v]));
basic_lemma_for_mon(r, derived); basic_lemma_for_mon(r, derived);
} }

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

@ -21,10 +21,11 @@ Revision History:
#include "math/lp/factorization_factory_imp.h" #include "math/lp/factorization_factory_imp.h"
namespace nla { namespace nla {
core::core(lp::lar_solver& s) : core::core(lp::lar_solver& s, reslimit & lim) :
m_evars(), m_evars(),
m_lar_solver(s), m_lar_solver(s),
m_tangents(this), m_tangents(this),
m_intervals(this, lim),
m_basics(this), m_basics(this),
m_order(this), m_order(this),
m_monotone(this), m_monotone(this),

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

@ -27,6 +27,7 @@
#include "math/lp/nla_monotone_lemmas.h" #include "math/lp/nla_monotone_lemmas.h"
#include "math/lp/emonomials.h" #include "math/lp/emonomials.h"
#include "math/lp/nla_settings.h" #include "math/lp/nla_settings.h"
#include "math/lp/nla_intervals.h"
namespace nla { namespace nla {
template <typename A, typename B> template <typename A, typename B>
@ -82,6 +83,7 @@ public:
vector<lemma> * m_lemma_vec; vector<lemma> * m_lemma_vec;
svector<lpvar> m_to_refine; svector<lpvar> m_to_refine;
tangents m_tangents; tangents m_tangents;
intervals m_intervals;
basics m_basics; basics m_basics;
order m_order; order m_order;
monotone m_monotone; monotone m_monotone;
@ -91,7 +93,7 @@ public:
emonomials& emons() { return m_emons; } emonomials& emons() { return m_emons; }
const emonomials& emons() const { return m_emons; } const emonomials& emons() const { return m_emons; }
// constructor // constructor
core(lp::lar_solver& s); core(lp::lar_solver& s, reslimit &);
bool compare_holds(const rational& ls, llc cmp, const rational& rs) const; bool compare_holds(const rational& ls, llc cmp, const rational& rs) const;

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

@ -1,90 +1,76 @@
#include "math/lp/nla_core.h" #include "math/lp/nla_core.h"
#include "math/interval/interval_def.h" #include "math/interval/interval_def.h"
#include "math/lp/nla_intervals.h" #include "math/lp/nla_intervals.h"
namespace nla { namespace nla {
bool intervals::check() { bool intervals::get_lemmas() {
// m_region.reset(); m_region.reset();
// for (auto const& m : m_core->emons()) { bool ret = false;
// if (!check(m)) { for (auto const& k : c().m_to_refine) {
// return false; if (get_lemma(c().emons()[k])) {
// } ret = true;
// } }
// for (auto const& t : ls().terms()) { if (c().done())
// if (!check(*t)) { break;
// return false; }
// } return ret;
// }
return true;
} }
// create a product of interval signs together with the depencies // create a product of interval signs together with the depencies
intervals::interval intervals::mul_signs_with_deps(const svector<lpvar>& vars) const { intervals::interval intervals::mul_signs_with_deps(const svector<lpvar>& vars) const {
interval a, b, c; interval a, b, c;
m_imanager.set(a, mpq(1)); m_imanager.set(a, mpq(1));
for (lpvar v : vars) { for (lpvar v : vars) {
set_var_interval_signs_with_deps(v, b); set_var_interval_signs_with_deps(v, b);
interval_deps deps; interval_deps deps;
m_imanager.mul(a, b, c, deps); m_imanager.mul(a, b, c, deps);
m_imanager.set(a, c); m_imanager.set(a, c);
m_config.add_deps(a, b, deps, a); m_config.add_deps(a, b, deps, a);
if (m_imanager.is_zero(a)) if (m_imanager.is_zero(a))
return a; return a;
} }
return a; return a;
} }
// bool intervals::check(monomial const& m) { bool intervals::get_lemma(monomial const& m) {
// interval a, b, c, d; interval b, c, d;
// m_imanager.set(a, mpq(1)); interval a = mul(m.vars());
// set_var_interval(m.var(), d); lp::impq v(val(m.var()));
// if (m_imanager.lower_is_inf(d) && m_imanager.upper_is_inf(d)) { if (!m_imanager.lower_is_inf(a)) {
// return true; lp::impq lb(rational(a.m_lower));
// } if (m_config.lower_is_open(a))
// for (lpvar v : m.vars()) { lb.y = 1;
// // TBD allow for division to get range of a if (v < lb) {
// // m = a*b*c, where m and b*c are bounded, then interval for a is m/b*c interval signs_a = mul_signs_with_deps(m.vars());
// if (m_imanager.lower_is_inf(a) && m_imanager.upper_is_inf(a)) { add_empty_lemma();
// return true; svector<lp::constraint_index> expl;
// } m_dep_manager.linearize(signs_a.m_lower_dep, expl);
// // TBD: deal with powers v^n interval instead of multiplying v*v .. * v _().current_expl().add_expl(expl);
// set_var_interval(v, b); llc cmp = m_config.lower_is_open(a)? llc::GT: llc::GE;
// interval_deps deps; mk_ineq(m.var(), cmp, lb.x);
// m_imanager.mul(a, b, c, deps); TRACE("nla_solver", _().print_lemma(tout); );
// m_imanager.set(a, c); return true;
// m_config.add_deps(a, b, deps, a); }
// } }
// if (m_imanager.before(a, d)) {
// svector<lp::constraint_index> cs;
// m_dep_manager.linearize(a.m_upper_dep, cs);
// m_dep_manager.linearize(d.m_lower_dep, cs);
// for (auto ci : cs) {
// (void)ci;
// SASSERT(false);
// //expl.push_justification(ci);
// }
// // TBD conflict
// return false;
// }
// if (m_imanager.before(d, a)) {
// svector<lp::constraint_index> cs;
// m_dep_manager.linearize(a.m_lower_dep, cs);
// m_dep_manager.linearize(d.m_upper_dep, cs);
// for (auto ci : cs) {
// (void)ci;
// SASSERT(false); //expl.push_justification(ci);
// }
// // TBD conflict
// return false;
// }
// // could also perform bounds propagation:
// // a has tighter lower/upper bound than m.var(),
// // -> transfer bound to m.var()
// // all but one variable has bound
// // -> transfer bound to that variable using division
// return true;
// }
if (!m_imanager.upper_is_inf(a)) {
lp::impq ub(rational(a.m_upper));
if (m_config.upper_is_open(a))
ub.y = 1;
if (v > ub) {
interval signs_a = mul_signs_with_deps(m.vars());
add_empty_lemma();
svector<lp::constraint_index> expl;
m_dep_manager.linearize(signs_a.m_upper_dep, expl);
_().current_expl().add_expl(expl);
llc cmp = m_config.lower_is_open(a)? llc::LT: llc::LE;
mk_ineq(m.var(), cmp, ub.x);
TRACE("nla_solver", _().print_lemma(tout); );
return true;
}
}
return false;
}
void intervals::set_var_interval(lpvar v, interval& b) const { void intervals::set_var_interval(lpvar v, interval& b) const {
lp::constraint_index ci; lp::constraint_index ci;
rational val; rational val;

249
src/math/lp/nla_intervals.h
View file

@ -26,40 +26,39 @@
namespace nla { namespace nla {
class core; class core;
class intervals { class intervals : common {
core * m_core; class ci_value_manager {
class ci_value_manager { public:
public: void inc_ref(lp::constraint_index const & v) {
void inc_ref(lp::constraint_index const & v) { }
}
void dec_ref(lp::constraint_index const & v) { void dec_ref(lp::constraint_index const & v) {
} }
}; };
struct ci_dependency_config { struct ci_dependency_config {
typedef ci_value_manager value_manager; typedef ci_value_manager value_manager;
typedef small_object_allocator allocator; typedef small_object_allocator allocator;
static const bool ref_count = false; static const bool ref_count = false;
typedef lp::constraint_index value; typedef lp::constraint_index value;
}; };
typedef dependency_manager<ci_dependency_config> ci_dependency_manager; typedef dependency_manager<ci_dependency_config> ci_dependency_manager;
typedef ci_dependency_manager::dependency ci_dependency; typedef ci_dependency_manager::dependency ci_dependency;
class im_config { class im_config {
unsynch_mpq_manager& m_manager; unsynch_mpq_manager& m_manager;
ci_dependency_manager& m_dep_manager; ci_dependency_manager& m_dep_manager;
public: public:
typedef unsynch_mpq_manager numeral_manager; typedef unsynch_mpq_manager numeral_manager;
// Every configuration object must provide an interval type. // Every configuration object must provide an interval type.
// The actual fields are irrelevant, the interval manager // The actual fields are irrelevant, the interval manager
// accesses interval data using the following API. // accesses interval data using the following API.
struct interval { struct interval {
interval(): interval():
@ -78,107 +77,105 @@ namespace nla {
}; };
void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const {
ci_dependency* lo = mk_dependency(a, b, deps.m_lower_deps); ci_dependency* lo = mk_dependency(a, b, deps.m_lower_deps);
ci_dependency* hi = mk_dependency(a, b, deps.m_upper_deps); ci_dependency* hi = mk_dependency(a, b, deps.m_upper_deps);
i.m_lower_dep = lo; i.m_lower_dep = lo;
i.m_upper_dep = hi; i.m_upper_dep = hi;
}
// Should be NOOPs for precise mpq types.
// For imprecise types (e.g., floats) it should set the rounding mode.
void round_to_minus_inf() {}
void round_to_plus_inf() {}
void set_rounding(bool to_plus_inf) {}
// Getters
mpq const & lower(interval const & a) const { return a.m_lower; }
mpq const & upper(interval const & a) const { return a.m_upper; }
mpq & lower(interval & a) { return a.m_lower; }
mpq & upper(interval & a) { return a.m_upper; }
bool lower_is_open(interval const & a) const { return a.m_lower_open; }
bool upper_is_open(interval const & a) const { return a.m_upper_open; }
bool lower_is_inf(interval const & a) const { return a.m_lower_inf; }
bool upper_is_inf(interval const & a) const { return a.m_upper_inf; }
bool is_zero(interval const & a) const {
return unsynch_mpq_manager::is_zero(a.m_lower)
&& unsynch_mpq_manager::is_zero(a.m_upper); }
// Setters
void set_lower(interval & a, mpq const & n) const { m_manager.set(a.m_lower, n); }
void set_upper(interval & a, mpq const & n) const { m_manager.set(a.m_upper, n); }
void set_lower(interval & a, rational const & n) const { set_lower(a, n.to_mpq()); }
void set_upper(interval & a, rational const & n) const { set_upper(a, n.to_mpq()); }
void set_lower_is_open(interval & a, bool v) const { a.m_lower_open = v; }
void set_upper_is_open(interval & a, bool v) const { a.m_upper_open = v; }
void set_lower_is_inf(interval & a, bool v) const { a.m_lower_inf = v; }
void set_upper_is_inf(interval & a, bool v) const { a.m_upper_inf = v; }
// Reference to numeral manager
numeral_manager & m() const { return m_manager; }
im_config(numeral_manager & m, ci_dependency_manager& d):m_manager(m), m_dep_manager(d) {}
private:
ci_dependency* mk_dependency(interval const& a, interval const& b, bound_deps bd) const {
ci_dependency* dep = nullptr;
if (dep_in_lower1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
} }
if (dep_in_lower2(bd)) {
// Should be NOOPs for precise mpq types. dep = m_dep_manager.mk_join(dep, b.m_lower_dep);
// For imprecise types (e.g., floats) it should set the rounding mode.
void round_to_minus_inf() {}
void round_to_plus_inf() {}
void set_rounding(bool to_plus_inf) {}
// Getters
mpq const & lower(interval const & a) const { return a.m_lower; }
mpq const & upper(interval const & a) const { return a.m_upper; }
mpq & lower(interval & a) { return a.m_lower; }
mpq & upper(interval & a) { return a.m_upper; }
bool lower_is_open(interval const & a) const { return a.m_lower_open; }
bool upper_is_open(interval const & a) const { return a.m_upper_open; }
bool lower_is_inf(interval const & a) const { return a.m_lower_inf; }
bool upper_is_inf(interval const & a) const { return a.m_upper_inf; }
bool is_zero(interval const & a) const {
return unsynch_mpq_manager::is_zero(a.m_lower)
&& unsynch_mpq_manager::is_zero(a.m_upper); }
// Setters
void set_lower(interval & a, mpq const & n) const { m_manager.set(a.m_lower, n); }
void set_upper(interval & a, mpq const & n) const { m_manager.set(a.m_upper, n); }
void set_lower(interval & a, rational const & n) const { set_lower(a, n.to_mpq()); }
void set_upper(interval & a, rational const & n) const { set_upper(a, n.to_mpq()); }
void set_lower_is_open(interval & a, bool v) const { a.m_lower_open = v; }
void set_upper_is_open(interval & a, bool v) const { a.m_upper_open = v; }
void set_lower_is_inf(interval & a, bool v) const { a.m_lower_inf = v; }
void set_upper_is_inf(interval & a, bool v) const { a.m_upper_inf = v; }
// Reference to numeral manager
numeral_manager & m() const { return m_manager; }
im_config(numeral_manager & m, ci_dependency_manager& d):m_manager(m), m_dep_manager(d) {}
private:
ci_dependency* mk_dependency(interval const& a, interval const& b, bound_deps bd) const {
ci_dependency* dep = nullptr;
if (dep_in_lower1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
}
if (dep_in_lower2(bd)) {
dep = m_dep_manager.mk_join(dep, b.m_lower_dep);
}
if (dep_in_upper1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_upper_dep);
}
if (dep_in_upper2(bd)) {
dep = m_dep_manager.mk_join(dep, b.m_upper_dep);
}
return dep;
} }
}; if (dep_in_upper1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_upper_dep);
small_object_allocator m_alloc; }
ci_value_manager m_val_manager; if (dep_in_upper2(bd)) {
unsynch_mpq_manager m_num_manager; dep = m_dep_manager.mk_join(dep, b.m_upper_dep);
mutable ci_dependency_manager m_dep_manager; }
im_config m_config; return dep;
mutable interval_manager<im_config> m_imanager; }
region m_region;
typedef interval_manager<im_config>::interval interval;
bool check(monomial const& m);
void set_var_interval(lpvar v, interval & b) const;
void set_var_interval_signs(lpvar v, interval & b) const;
void set_var_interval_signs_with_deps(lpvar v, interval & b) const;
ci_dependency* mk_dep(lp::constraint_index ci) const;
bool check(lp::lar_term const& t);
lp::lar_solver& ls();
const lp::lar_solver& ls() const;
public:
intervals(core* c, reslimit& lim) :
m_core(c),
m_alloc("intervals"),
m_dep_manager(m_val_manager, m_alloc),
m_config(m_num_manager, m_dep_manager),
m_imanager(lim, im_config(m_num_manager, m_dep_manager))
{}
bool check();
bool monomial_has_lower_bound(lpvar j) const;
bool monomial_has_upper_bound(lpvar j) const;
bool product_has_upper_bound(int sign, const svector<lpvar>&) const;
lp::impq get_upper_bound_of_monomial(lpvar j) const;
lp::impq get_lower_bound_of_monomial(lpvar j) const;
interval mul(const svector<lpvar>&) const;
interval mul_signs(const svector<lpvar>&) const;
interval mul_signs_with_deps(const svector<lpvar>&) const;
void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
std::ostream& print_explanations(const svector<lp::constraint_index> &, std::ostream&) const;
}; };
small_object_allocator m_alloc;
ci_value_manager m_val_manager;
unsynch_mpq_manager m_num_manager;
mutable ci_dependency_manager m_dep_manager;
im_config m_config;
mutable interval_manager<im_config> m_imanager;
region m_region;
typedef interval_manager<im_config>::interval interval;
void set_var_interval(lpvar v, interval & b) const;
void set_var_interval_signs(lpvar v, interval & b) const;
void set_var_interval_signs_with_deps(lpvar v, interval & b) const;
ci_dependency* mk_dep(lp::constraint_index ci) const;
lp::lar_solver& ls();
const lp::lar_solver& ls() const;
public:
intervals(core* c, reslimit& lim) :
common(c),
m_alloc("intervals"),
m_dep_manager(m_val_manager, m_alloc),
m_config(m_num_manager, m_dep_manager),
m_imanager(lim, im_config(m_num_manager, m_dep_manager))
{}
bool get_lemmas();
bool get_lemma(monomial const& m);
bool monomial_has_lower_bound(lpvar j) const;
bool monomial_has_upper_bound(lpvar j) const;
bool product_has_upper_bound(int sign, const svector<lpvar>&) const;
lp::impq get_upper_bound_of_monomial(lpvar j) const;
lp::impq get_lower_bound_of_monomial(lpvar j) const;
interval mul(const svector<lpvar>&) const;
interval mul_signs(const svector<lpvar>&) const;
interval mul_signs_with_deps(const svector<lpvar>&) const;
void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
std::ostream& print_explanations(const svector<lp::constraint_index> &, std::ostream&) const;
};
} // end of namespace nla } // end of namespace nla

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

@ -54,32 +54,10 @@ void solver::pop(unsigned n) {
} }
solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core, m_res_limit) { solver::solver(lp::lar_solver& s): m_core(alloc(core, s, m_res_limit)) {
} }
solver::~solver() { solver::~solver() {
dealloc(m_core); dealloc(m_core);
} }
lp::impq solver::get_upper_bound(lpvar j) const {
SASSERT(is_monomial_var(j) && m_intervals.monomial_has_upper_bound(j));
return m_intervals.get_upper_bound_of_monomial(j);
}
lp::impq solver::get_lower_bound(lpvar j) const {
SASSERT(is_monomial_var(j) && m_intervals.monomial_has_lower_bound(j));
return m_intervals.get_lower_bound_of_monomial(j);
}
bool solver::monomial_has_lower_bound(lpvar j) const {
return m_intervals.monomial_has_lower_bound(j);
}
bool solver::monomial_has_upper_bound(lpvar j) const {
return m_intervals.monomial_has_upper_bound(j);
}
void solver::get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const {
m_intervals.get_explanation_of_upper_bound_for_monomial(j, expl);
}
void solver::get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const{
m_intervals.get_explanation_of_lower_bound_for_monomial(j, expl);
}
} }

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

@ -34,7 +34,6 @@ namespace nla {
class solver { class solver {
core* m_core; core* m_core;
reslimit m_res_limit; reslimit m_res_limit;
intervals m_intervals;
public: public:
void add_monomial(lpvar v, unsigned sz, lpvar const* vs); void add_monomial(lpvar v, unsigned sz, lpvar const* vs);
@ -47,11 +46,5 @@ public:
lbool check(vector<lemma>&); lbool check(vector<lemma>&);
std::ostream& display(std::ostream& out); std::ostream& display(std::ostream& out);
bool is_monomial_var(lpvar) const; bool is_monomial_var(lpvar) const;
lp::impq get_lower_bound(lpvar j) const;
lp::impq get_upper_bound(lpvar j) const;
bool monomial_has_lower_bound(lpvar j) const;
bool monomial_has_upper_bound(lpvar j) const;
void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>&) const;
void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>&) const;
}; };
} }