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

remove lar_solver from nla_intervals fields

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-06 10:17:42 -07:00
parent f5c3484fe2
commit f22252112e
3 changed files with 99 additions and 99 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,109 +1,110 @@
#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::check() {
// m_region.reset(); // m_region.reset();
// for (auto const& m : m_core->emons()) { // for (auto const& m : m_core->emons()) {
// if (!check(m)) { // if (!check(m)) {
// return false; // return false;
// } // }
// } // }
// for (auto const& t : m_solver.terms()) { // for (auto const& t : ls().terms()) {
// if (!check(*t)) { // if (!check(*t)) {
// return false; // return false;
// } // }
// } // }
return true;
}
bool intervals::check(monomial const& m) {
interval a, b, c, d;
m_imanager.set(a, rational(1).to_mpq());
set_interval(m.var(), d);
if (m_imanager.lower_is_inf(d) && m_imanager.upper_is_inf(d)) {
return true; return true;
} }
for (lpvar v : m.vars()) {
bool intervals::check(monomial const& m) { // TBD allow for division to get range of a
interval a, b, c, d; // m = a*b*c, where m and b*c are bounded, then interval for a is m/b*c
m_imanager.set(a, rational(1).to_mpq()); if (m_imanager.lower_is_inf(a) && m_imanager.upper_is_inf(a)) {
set_interval(m.var(), d);
if (m_imanager.lower_is_inf(d) && m_imanager.upper_is_inf(d)) {
return true; return true;
} }
for (lpvar v : m.vars()) { // TBD: deal with powers v^n interval instead of multiplying v*v .. * v
// TBD allow for division to get range of a set_interval(v, b);
// m = a*b*c, where m and b*c are bounded, then interval for a is m/b*c interval_deps deps;
if (m_imanager.lower_is_inf(a) && m_imanager.upper_is_inf(a)) { m_imanager.mul(a, b, c, deps);
return true; m_imanager.set(a, c);
} m_config.set_deps(a, b, deps, a);
// TBD: deal with powers v^n interval instead of multiplying v*v .. * v
set_interval(v, b);
interval_deps deps;
m_imanager.mul(a, b, c, deps);
m_imanager.set(a, c);
m_config.set_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) {
//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) {
//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.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;
}
void intervals::set_interval(lpvar v, interval& b) { void intervals::set_interval(lpvar v, interval& b) {
lp::constraint_index ci; lp::constraint_index ci;
rational val; rational val;
bool is_strict; bool is_strict;
if (m_solver.has_lower_bound(v, ci, val, is_strict)) { if (ls().has_lower_bound(v, ci, val, is_strict)) {
m_config.set_lower(b, val); m_config.set_lower(b, val);
m_config.set_lower_is_open(b, is_strict); m_config.set_lower_is_open(b, is_strict);
m_config.set_lower_is_inf(b, false); m_config.set_lower_is_inf(b, false);
b.m_lower_dep = mk_dep(ci); 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 (m_solver.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);
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;
}
} }
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, 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) { intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) {
return m_dep_manager.mk_leaf(ci); return m_dep_manager.mk_leaf(ci);
} }
bool intervals::check(lp::lar_term const& t) { bool intervals::check(lp::lar_term const& t) {
// convert term into factors for improved precision // convert term into factors for improved precision
return true; return true;
} }
lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const { lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const {
SASSERT(false); SASSERT(false);
@ -117,7 +118,7 @@ lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
bool intervals::product_has_upper_bound(int sign, const svector<lpvar>&) const { bool intervals::product_has_upper_bound(int sign, const svector<lpvar>&) const {
interval a; interval a;
throw; SASSERT(false);
} }
bool intervals::monomial_has_lower_bound(lpvar j) const { bool intervals::monomial_has_lower_bound(lpvar j) const {
@ -129,5 +130,6 @@ bool intervals::monomial_has_upper_bound(lpvar j) const {
const monomial& m = m_core->emons()[j]; const monomial& m = m_core->emons()[j];
return product_has_upper_bound(-1, m.vars()); return product_has_upper_bound(-1, m.vars());
} }
lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; }
} }
template class interval_manager<nla::intervals::im_config>; template class interval_manager<nla::intervals::im_config>;

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

@ -142,7 +142,6 @@ namespace nla {
im_config m_config; im_config m_config;
interval_manager<im_config> m_imanager; interval_manager<im_config> m_imanager;
region m_region; region m_region;
lp::lar_solver& m_solver;
typedef interval_manager<im_config>::interval interval; typedef interval_manager<im_config>::interval interval;
@ -153,15 +152,14 @@ namespace nla {
ci_dependency* mk_dep(lp::constraint_index ci); ci_dependency* mk_dep(lp::constraint_index ci);
bool check(lp::lar_term const& t); bool check(lp::lar_term const& t);
lp::lar_solver& ls();
public: public:
intervals(core* c, reslimit& lim, lp::lar_solver& s) : intervals(core* c, reslimit& lim) :
m_core(c), m_core(c),
m_alloc("intervals"), m_alloc("intervals"),
m_dep_manager(m_val_manager, m_alloc), m_dep_manager(m_val_manager, m_alloc),
m_config(m_num_manager, m_dep_manager), m_config(m_num_manager, m_dep_manager),
m_imanager(lim, im_config(m_num_manager, m_dep_manager)), m_imanager(lim, im_config(m_num_manager, m_dep_manager))
m_solver(s)
{} {}
bool check(); bool check();
bool monomial_has_lower_bound(lpvar j) const; bool monomial_has_lower_bound(lpvar j) const;

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

@ -55,7 +55,7 @@ void solver::pop(unsigned n) {
} }
solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core, m_res_limit, s) { solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core, m_res_limit) {
} }
solver::~solver() { solver::~solver() {