mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
prepare expressions for horner form
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
130995a3db
commit
902a223b34
6 changed files with 721 additions and 5 deletions
|
|
@ -28,6 +28,7 @@ z3_add_component(lp
|
|||
nla_basics_lemmas.cpp
|
||||
nla_common.cpp
|
||||
nla_core.cpp
|
||||
nla_intervals.cpp
|
||||
nla_monotone_lemmas.cpp
|
||||
nla_order_lemmas.cpp
|
||||
nla_solver.cpp
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
/*++
|
||||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
|
@ -19,6 +19,7 @@ Revision History:
|
|||
--*/
|
||||
#include "math/lp/nla_core.h"
|
||||
#include "math/lp/factorization_factory_imp.h"
|
||||
#include "math/lp/nla_expr.h"
|
||||
namespace nla {
|
||||
|
||||
core::core(lp::lar_solver& s, reslimit & lim) :
|
||||
|
|
@ -1356,16 +1357,68 @@ lbool core::test_check(
|
|||
return check(l);
|
||||
}
|
||||
|
||||
nla_expr<rational> core::mk_expr(lpvar j) const {
|
||||
return nla_expr<rational>::var(j);
|
||||
}
|
||||
|
||||
nla_expr<rational> core::mk_expr(const rational &a, lpvar j) const {
|
||||
if (a == 1)
|
||||
return mk_expr(j);
|
||||
nla_expr<rational> r(expr_type::MUL);
|
||||
r.add_child(nla_expr<rational>::scalar(a));
|
||||
r.add_child(nla_expr<rational>::var(j));
|
||||
return r;
|
||||
}
|
||||
|
||||
nla_expr<rational> core::mk_expr(const rational &a, const svector<lpvar>& vs) const {
|
||||
nla_expr<rational> r(expr_type::MUL);
|
||||
r.add_child(nla_expr<rational>::scalar(a));
|
||||
for (lpvar j : vs)
|
||||
r.add_child(nla_expr<rational>::var(j));
|
||||
return r;
|
||||
}
|
||||
nla_expr<rational> core::mk_expr(const lp::lar_term& t) const {
|
||||
auto coeffs = t.coeffs_as_vector();
|
||||
if (coeffs.size() == 1) {
|
||||
return mk_expr(coeffs[0].first, coeffs[0].second);
|
||||
}
|
||||
nla_expr<rational> r(expr_type::SUM);
|
||||
for (const auto & p : coeffs) {
|
||||
lpvar j = p.second;
|
||||
if (is_monomial_var(j))
|
||||
r.add_child(mk_expr(p.first, m_emons[j].vars()));
|
||||
else
|
||||
r.add_child(mk_expr(p.first, j));
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
std::ostream& core::print_terms(std::ostream& out) const {
|
||||
for (auto t: m_lar_solver.m_terms)
|
||||
print_term(*t, out) << "\n";
|
||||
for (unsigned i=0; i< m_lar_solver.m_terms.size(); i++) {
|
||||
unsigned ext = i + m_lar_solver.terms_start_index();
|
||||
if (!m_lar_solver.var_is_registered(ext)) {
|
||||
out << "term is not registered\n";
|
||||
continue;
|
||||
}
|
||||
|
||||
const lp::lar_term & t = *m_lar_solver.m_terms[i];
|
||||
print_term(t, out) << std::endl;
|
||||
lpvar j = m_lar_solver.external_to_local(ext);
|
||||
SASSERT(j + 1);
|
||||
SASSERT(value(t) == val(j));
|
||||
print_var(j, out);
|
||||
out << "term again "; print_term(t, out) << std::endl;
|
||||
auto e = mk_expr(t);
|
||||
out << "e= " << e << "\n";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const {
|
||||
return lp::print_linear_combination_customized(
|
||||
t.coeffs_as_vector(),
|
||||
[this](lpvar j) {
|
||||
return is_monomial_var(j)? product_indices_str(m_emons[j].vars()) : (std::string("v") + lp::T_to_string(j));
|
||||
return is_monomial_var(j)?
|
||||
(product_indices_str(m_emons[j].vars()) + (check_monomial(m_emons[j])? "": "_")) : (std::string("v") + lp::T_to_string(j));
|
||||
},
|
||||
out);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,6 +27,7 @@
|
|||
#include "math/lp/nla_monotone_lemmas.h"
|
||||
#include "math/lp/emonomials.h"
|
||||
#include "math/lp/nla_settings.h"
|
||||
#include "math/lp/nla_expr.h"
|
||||
namespace nla {
|
||||
|
||||
template <typename A, typename B>
|
||||
|
|
@ -344,7 +345,12 @@ public:
|
|||
lbool test_check(vector<lemma>& l);
|
||||
lpvar map_to_root(lpvar) const;
|
||||
std::ostream& print_terms(std::ostream&) const;
|
||||
std::ostream& print_term( const lp::lar_term&, std::ostream&) const;
|
||||
std::ostream& print_term( const lp::lar_term&, std::ostream&) const;
|
||||
nla_expr<rational> mk_expr(lpvar j) const;
|
||||
nla_expr<rational> mk_expr(const rational &a, lpvar j) const;
|
||||
|
||||
nla_expr<rational> mk_expr(const rational &a, const svector<lpvar>& vs) const;
|
||||
nla_expr<rational> mk_expr(const lp::lar_term& t) const;
|
||||
}; // end of core
|
||||
|
||||
struct pp_mon {
|
||||
|
|
|
|||
150
src/math/lp/nla_expr.h
Normal file
150
src/math/lp/nla_expr.h
Normal file
|
|
@ -0,0 +1,150 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "math/lp/nla_defs.h"
|
||||
namespace nla {
|
||||
enum class expr_type { SUM, MUL, VAR, SCALAR };
|
||||
// This class is needed in horner calculation with intervals
|
||||
template <typename T>
|
||||
class nla_expr {
|
||||
expr_type m_type;
|
||||
lpvar m_j;
|
||||
T m_v; // for the scalar
|
||||
vector<nla_expr> m_children;
|
||||
public:
|
||||
std::string str() const { std::stringstream ss; ss << *this; return ss.str(); }
|
||||
std::ostream & print_sum(std::ostream& out) const {
|
||||
bool first = true;
|
||||
for (const nla_expr& v : m_children) {
|
||||
std::string s = v.str();
|
||||
if (first) {
|
||||
first = false;
|
||||
if (v.is_simple())
|
||||
out << v;
|
||||
else
|
||||
out << "(" << s << ")";
|
||||
} else {
|
||||
if (v.is_simple()) {
|
||||
if (s[0] == '-') {
|
||||
out << s;
|
||||
} else {
|
||||
out << "+" << s;
|
||||
}
|
||||
} else {
|
||||
out << "+" << "(" << s << ")";
|
||||
}
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
std::ostream & print_mul(std::ostream& out) const {
|
||||
bool first = true;
|
||||
for (const nla_expr& v : m_children) {
|
||||
std::string s = v.str();
|
||||
if (first) {
|
||||
first = false;
|
||||
if (v.is_simple())
|
||||
out << s;
|
||||
else
|
||||
out << "(" << s << ")";
|
||||
} else {
|
||||
if (v.is_simple()) {
|
||||
if (s[0] == '-') {
|
||||
out << "*(" << s << ")";
|
||||
} else {
|
||||
out << "*" << s;
|
||||
}
|
||||
} else {
|
||||
out << "*(" << s << ")";
|
||||
}
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
std::ostream & print(std::ostream& out) const {
|
||||
switch(m_type) {
|
||||
case expr_type::SUM:
|
||||
return print_sum(out);
|
||||
case expr_type::MUL:
|
||||
return print_mul(out);
|
||||
case expr_type::VAR:
|
||||
out << "v" << m_j;
|
||||
return out;
|
||||
case expr_type::SCALAR:
|
||||
out << m_v;
|
||||
return out;
|
||||
default:
|
||||
return out;
|
||||
}
|
||||
}
|
||||
|
||||
bool is_simple() const {
|
||||
switch(m_type) {
|
||||
case expr_type::SUM:
|
||||
case expr_type::MUL:
|
||||
return m_children.size() <= 1;
|
||||
|
||||
default:
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
nla_expr(expr_type t): m_type(t) {}
|
||||
|
||||
void add_child(const nla_expr& e) {
|
||||
SASSERT(m_type == expr_type::SUM || m_type == expr_type::MUL);
|
||||
m_children.push_back(e);
|
||||
}
|
||||
|
||||
|
||||
static nla_expr sum(const nla_expr& v, const nla_expr & w) {
|
||||
nla_expr r(expr_type::SUM);
|
||||
r.add_child(v);
|
||||
r.add_child(w);
|
||||
return r;
|
||||
}
|
||||
static nla_expr mul(const nla_expr& v, const nla_expr & w) {
|
||||
nla_expr r(expr_type::MUL);
|
||||
r.add_child(v);
|
||||
r.add_child(w);
|
||||
return r;
|
||||
}
|
||||
|
||||
static nla_expr scalar(const T& v) {
|
||||
nla_expr r(expr_type::SCALAR);
|
||||
r.m_v = v;
|
||||
return r;
|
||||
}
|
||||
|
||||
static nla_expr var(lpvar j) {
|
||||
nla_expr r(expr_type::VAR);
|
||||
r.m_j = j;
|
||||
return r;
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
template <typename T>
|
||||
std::ostream& operator<<(std::ostream& out, const nla_expr<T>& e ) {
|
||||
return e.print(out);
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
315
src/math/lp/nla_intervals.cpp
Normal file
315
src/math/lp/nla_intervals.cpp
Normal file
|
|
@ -0,0 +1,315 @@
|
|||
#include "math/lp/nla_core.h"
|
||||
#include "math/interval/interval_def.h"
|
||||
#include "math/lp/nla_intervals.h"
|
||||
|
||||
namespace nla {
|
||||
|
||||
bool intervals::get_lemmas() {
|
||||
m_region.reset();
|
||||
bool ret = false;
|
||||
for (auto const& k : c().m_to_refine) {
|
||||
if (get_lemma(c().emons()[k])) {
|
||||
ret = true;
|
||||
}
|
||||
if (c().done())
|
||||
break;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
// create a product of interval signs together with the depencies
|
||||
intervals::interval intervals::mul_signs_with_deps(const svector<lpvar>& vars) const {
|
||||
interval a, b, c;
|
||||
m_imanager.set(a, mpq(1));
|
||||
for (lpvar v : vars) {
|
||||
set_var_interval_signs_with_deps(v, b);
|
||||
interval_deps deps;
|
||||
m_imanager.mul(a, b, c, deps);
|
||||
m_imanager.set(a, c);
|
||||
m_config.add_deps(a, b, deps, a);
|
||||
if (m_imanager.is_zero(a))
|
||||
return a;
|
||||
}
|
||||
return a;
|
||||
}
|
||||
|
||||
void intervals::get_lemma_for_zero_interval(monomial const& m) {
|
||||
if (val(m).is_zero()) return;
|
||||
interval signs_a = mul_signs_with_deps(m.vars());
|
||||
add_empty_lemma();
|
||||
svector<lp::constraint_index> expl;
|
||||
m_dep_manager.linearize(signs_a.m_lower_dep, expl);
|
||||
TRACE("nla_solver", print_vector(expl, tout) << "\n";);
|
||||
_().current_expl().add_expl(expl);
|
||||
mk_ineq(m.var(), llc::EQ);
|
||||
TRACE("nla_solver", _().print_lemma(tout); );
|
||||
}
|
||||
|
||||
bool intervals::get_lemma_for_lower(const monomial& m, const interval& a) {
|
||||
if (m_vars_pushed_up[m.var()] > 10)
|
||||
return false;
|
||||
lp::impq lb(rational(a.m_lower));
|
||||
if (m_config.lower_is_open(a))
|
||||
lb.y = 1;
|
||||
|
||||
lp::impq v(val(m.var()));
|
||||
if (v < lb) {
|
||||
m_vars_pushed_up[m.var()] = m_vars_pushed_up[m.var()] + 1;
|
||||
interval signs_a = mul_signs_with_deps(m.vars());
|
||||
add_empty_lemma();
|
||||
svector<lp::constraint_index> expl;
|
||||
m_dep_manager.linearize(signs_a.m_lower_dep, expl);
|
||||
_().current_expl().add_expl(expl);
|
||||
llc cmp = m_config.lower_is_open(a)? llc::GT: llc::GE;
|
||||
mk_ineq(m.var(), cmp, lb.x);
|
||||
TRACE("nla_solver", _().print_lemma(tout); );
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool intervals::get_lemma_for_upper(const monomial& m, const interval& a) {
|
||||
if (m_vars_pushed_down[m.var()] > 10)
|
||||
return false;
|
||||
lp::impq ub(rational(a.m_upper));
|
||||
if (m_config.upper_is_open(a))
|
||||
ub.y = 1;
|
||||
lp::impq v(val(m.var()));
|
||||
if (v > ub) {
|
||||
m_vars_pushed_down[m.var()] = m_vars_pushed_down[m.var()] + 1;
|
||||
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.upper_is_open(a)? llc::LT: llc::LE;
|
||||
mk_ineq(m.var(), cmp, ub.x);
|
||||
TRACE("nla_solver", _().print_lemma(tout); );
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
bool intervals::get_lemma(monomial const& m) {
|
||||
interval b, c, d;
|
||||
interval a = mul(m.vars());
|
||||
if (m_imanager.is_zero(a)) {
|
||||
get_lemma_for_zero_interval(m);
|
||||
return true;
|
||||
}
|
||||
if (!m_imanager.lower_is_inf(a)) {
|
||||
return get_lemma_for_lower(m, a);
|
||||
}
|
||||
|
||||
if (!m_imanager.upper_is_inf(a)) {
|
||||
return get_lemma_for_upper(m, a);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
void intervals::set_var_interval(lpvar v, interval& b) const {
|
||||
lp::constraint_index ci;
|
||||
rational val;
|
||||
bool is_strict;
|
||||
if (ls().has_lower_bound(v, ci, val, is_strict)) {
|
||||
m_config.set_lower(b, val);
|
||||
m_config.set_lower_is_open(b, is_strict);
|
||||
m_config.set_lower_is_inf(b, false);
|
||||
}
|
||||
else {
|
||||
m_config.set_lower_is_open(b, true);
|
||||
m_config.set_lower_is_inf(b, true);
|
||||
}
|
||||
if (ls().has_upper_bound(v, ci, val, is_strict)) {
|
||||
m_config.set_upper(b, val);
|
||||
m_config.set_upper_is_open(b, is_strict);
|
||||
m_config.set_upper_is_inf(b, false);
|
||||
}
|
||||
else {
|
||||
m_config.set_upper_is_open(b, true);
|
||||
m_config.set_upper_is_inf(b, true);
|
||||
}
|
||||
}
|
||||
|
||||
rational sign(const rational& v) { return v.is_zero()? v : (rational(v.is_pos()? 1 : -1)); }
|
||||
|
||||
void intervals::set_var_interval_signs(lpvar v, interval& b) const {
|
||||
lp::constraint_index ci;
|
||||
rational val;
|
||||
bool is_strict;
|
||||
if (ls().has_lower_bound(v, ci, val, is_strict)) {
|
||||
m_config.set_lower(b, sign(val));
|
||||
m_config.set_lower_is_open(b, is_strict);
|
||||
m_config.set_lower_is_inf(b, false);
|
||||
}
|
||||
else {
|
||||
m_config.set_lower_is_open(b, true);
|
||||
m_config.set_lower_is_inf(b, true);
|
||||
}
|
||||
if (ls().has_upper_bound(v, ci, val, is_strict)) {
|
||||
m_config.set_upper(b, sign(val));
|
||||
m_config.set_upper_is_open(b, is_strict);
|
||||
m_config.set_upper_is_inf(b, false);
|
||||
}
|
||||
else {
|
||||
m_config.set_upper_is_open(b, true);
|
||||
m_config.set_upper_is_inf(b, true);
|
||||
}
|
||||
}
|
||||
|
||||
void intervals::set_var_interval_signs_with_deps(lpvar v, interval& b) const {
|
||||
lp::constraint_index ci;
|
||||
rational val;
|
||||
bool is_strict;
|
||||
if (ls().has_lower_bound(v, ci, val, is_strict)) {
|
||||
m_config.set_lower(b, sign(val));
|
||||
m_config.set_lower_is_open(b, is_strict);
|
||||
m_config.set_lower_is_inf(b, false);
|
||||
b.m_lower_dep = mk_dep(ci);
|
||||
}
|
||||
else {
|
||||
m_config.set_lower_is_open(b, true);
|
||||
m_config.set_lower_is_inf(b, true);
|
||||
b.m_lower_dep = nullptr;
|
||||
}
|
||||
if (ls().has_upper_bound(v, ci, val, is_strict)) {
|
||||
m_config.set_upper(b, sign(val));
|
||||
m_config.set_upper_is_open(b, is_strict);
|
||||
m_config.set_upper_is_inf(b, false);
|
||||
b.m_upper_dep = mk_dep(ci);
|
||||
}
|
||||
else {
|
||||
m_config.set_upper_is_open(b, true);
|
||||
m_config.set_upper_is_inf(b, true);
|
||||
b.m_upper_dep = nullptr;
|
||||
}
|
||||
}
|
||||
|
||||
intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const {
|
||||
return m_dep_manager.mk_leaf(ci);
|
||||
}
|
||||
|
||||
lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const {
|
||||
const monomial& m = m_core->emons()[j];
|
||||
interval a = mul(m.vars());
|
||||
SASSERT(!m_imanager.upper_is_inf(a));
|
||||
auto r = lp::impq(a.m_upper);
|
||||
if (a.m_upper_open)
|
||||
r.y = -1;
|
||||
TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "upper = " << r << "\n";);
|
||||
return r;
|
||||
}
|
||||
lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
|
||||
const monomial& m = m_core->emons()[j];
|
||||
interval a = mul(m.vars());
|
||||
SASSERT(!a.m_lower_inf);
|
||||
auto r = lp::impq(a.m_lower);
|
||||
if (a.m_lower_open)
|
||||
r.y = 1;
|
||||
TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "lower = " << r << "\n";);
|
||||
return r;
|
||||
}
|
||||
|
||||
std::ostream& intervals::display(std::ostream& out, const interval& i) const {
|
||||
if (m_imanager.lower_is_inf(i)) {
|
||||
out << "(-oo";
|
||||
} else {
|
||||
out << (m_imanager.lower_is_open(i)? "(":"[") << rational(m_imanager.lower(i));
|
||||
}
|
||||
out << ",";
|
||||
if (m_imanager.upper_is_inf(i)) {
|
||||
out << "oo)";
|
||||
} else {
|
||||
out << rational(m_imanager.upper(i)) << (m_imanager.lower_is_open(i)? ")":"]");
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
|
||||
intervals::interval intervals::mul(const svector<lpvar>& vars) const {
|
||||
interval a;
|
||||
m_imanager.set(a, mpq(1));
|
||||
|
||||
for (lpvar j : vars) {
|
||||
interval b, c;
|
||||
set_var_interval(j, b);
|
||||
if (m_imanager.is_zero(b)) {
|
||||
return b;
|
||||
}
|
||||
m_imanager.mul(a, b, c);
|
||||
m_imanager.set(a, c);
|
||||
}
|
||||
return a;
|
||||
}
|
||||
|
||||
intervals::interval intervals::mul_signs(const svector<lpvar>& vars) const {
|
||||
interval a;
|
||||
m_imanager.set(a, mpq(1));
|
||||
|
||||
for (lpvar j : vars) {
|
||||
interval b, c;
|
||||
set_var_interval_signs(j, b);
|
||||
if (m_imanager.is_zero(b)) {
|
||||
return b;
|
||||
}
|
||||
m_imanager.mul(a, b, c);
|
||||
m_imanager.set(a, c);
|
||||
}
|
||||
return a;
|
||||
}
|
||||
|
||||
bool intervals::product_has_upper_bound(int sign, const svector<lpvar>& vars) const {
|
||||
interval a = mul_signs(vars);
|
||||
SASSERT(sign == 1 || sign == -1);
|
||||
return sign == 1 ? !m_imanager.upper_is_inf(a) : !m_imanager.lower_is_inf(a);
|
||||
}
|
||||
|
||||
bool intervals::monomial_has_lower_bound(lpvar j) const {
|
||||
const monomial& m = m_core->emons()[j];
|
||||
return product_has_upper_bound(-1, m.vars());
|
||||
}
|
||||
|
||||
bool intervals::monomial_has_upper_bound(lpvar j) const {
|
||||
const monomial& m = m_core->emons()[j];
|
||||
return product_has_upper_bound(1, m.vars());
|
||||
}
|
||||
lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; }
|
||||
|
||||
const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; }
|
||||
|
||||
std::ostream& intervals::print_explanations(const svector<lp::constraint_index> &expl , std::ostream& out) const {
|
||||
out << "interv expl:\n ";
|
||||
for (auto ci : expl)
|
||||
m_core->m_lar_solver.print_constraint_indices_only(ci, out);
|
||||
return out;
|
||||
}
|
||||
|
||||
void intervals::get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const {
|
||||
interval a = mul_signs_with_deps(m_core->emons()[j].vars());
|
||||
m_dep_manager.linearize(a.m_upper_dep, expl);
|
||||
TRACE("nla_intervals", print_explanations(expl, tout););
|
||||
}
|
||||
void intervals::get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const{
|
||||
interval a = mul_signs_with_deps(m_core->emons()[j].vars());
|
||||
m_dep_manager.linearize(a.m_lower_dep, expl);
|
||||
TRACE("nla_intervals", print_explanations(expl, tout););
|
||||
// return m_intervals.get_explanation_of_lower_bound_for_monomial(j, expl )
|
||||
}
|
||||
void intervals::push() {
|
||||
m_vars_pushed_up.push();
|
||||
m_vars_pushed_down.push();
|
||||
}
|
||||
void intervals::pop(unsigned k) {
|
||||
m_vars_pushed_up.pop(k);
|
||||
m_vars_pushed_down.pop(k);
|
||||
}
|
||||
|
||||
void intervals::init() {
|
||||
SASSERT(m_vars_pushed_down.size() == m_vars_pushed_up.size());
|
||||
unsigned n = c().m_lar_solver.number_of_vars();
|
||||
while (m_vars_pushed_up.size() < n) {
|
||||
m_vars_pushed_up.push_back(0);
|
||||
m_vars_pushed_down.push_back(0);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// instantiate the template
|
||||
template class interval_manager<nla::intervals::im_config>;
|
||||
191
src/math/lp/nla_intervals.h
Normal file
191
src/math/lp/nla_intervals.h
Normal file
|
|
@ -0,0 +1,191 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
Nikolaj Bjorner (nbjorner)
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "util/dependency.h"
|
||||
#include "util/small_object_allocator.h"
|
||||
#include "math/lp/nla_common.h"
|
||||
#include "math/lp/lar_solver.h"
|
||||
#include "math/interval/interval.h"
|
||||
|
||||
|
||||
namespace nla {
|
||||
class core;
|
||||
|
||||
class intervals : common {
|
||||
// fields to throttle the propagation on intervals
|
||||
lp::stacked_vector<unsigned> m_vars_pushed_up;
|
||||
lp::stacked_vector<unsigned> m_vars_pushed_down;
|
||||
|
||||
class ci_value_manager {
|
||||
public:
|
||||
void inc_ref(lp::constraint_index const & v) {
|
||||
}
|
||||
|
||||
void dec_ref(lp::constraint_index const & v) {
|
||||
}
|
||||
};
|
||||
|
||||
struct ci_dependency_config {
|
||||
typedef ci_value_manager value_manager;
|
||||
typedef small_object_allocator allocator;
|
||||
static const bool ref_count = false;
|
||||
typedef lp::constraint_index value;
|
||||
};
|
||||
|
||||
typedef dependency_manager<ci_dependency_config> ci_dependency_manager;
|
||||
|
||||
typedef ci_dependency_manager::dependency ci_dependency;
|
||||
|
||||
class im_config {
|
||||
unsynch_mpq_manager& m_manager;
|
||||
ci_dependency_manager& m_dep_manager;
|
||||
|
||||
public:
|
||||
typedef unsynch_mpq_manager numeral_manager;
|
||||
|
||||
|
||||
struct interval {
|
||||
interval():
|
||||
m_lower(), m_upper(),
|
||||
m_lower_open(1), m_upper_open(1),
|
||||
m_lower_inf(1), m_upper_inf(1),
|
||||
m_lower_dep(nullptr), m_upper_dep(nullptr) {}
|
||||
mpq m_lower;
|
||||
mpq m_upper;
|
||||
unsigned m_lower_open:1;
|
||||
unsigned m_upper_open:1;
|
||||
unsigned m_lower_inf:1;
|
||||
unsigned m_upper_inf:1;
|
||||
ci_dependency * m_lower_dep; // justification for the lower bound
|
||||
ci_dependency * m_upper_dep; // justification for the upper bound
|
||||
};
|
||||
|
||||
|
||||
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* hi = mk_dependency(a, b, deps.m_upper_deps);
|
||||
i.m_lower_dep = lo;
|
||||
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)) {
|
||||
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;
|
||||
}
|
||||
};
|
||||
|
||||
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;
|
||||
|
||||
public:
|
||||
typedef interval_manager<im_config>::interval interval;
|
||||
private:
|
||||
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);
|
||||
void get_lemma_for_zero_interval(monomial const& m);
|
||||
bool get_lemma_for_lower(monomial const& m, const interval& );
|
||||
bool get_lemma_for_upper(monomial const& m, const interval &);
|
||||
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;
|
||||
void push();
|
||||
void pop(unsigned k);
|
||||
void init();
|
||||
std::ostream& display(std::ostream& out, const intervals::interval& i) const;
|
||||
};
|
||||
|
||||
} // end of namespace nla
|
||||
Loading…
Add table
Add a link
Reference in a new issue