mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 11:25:51 +00:00
use dep_intervals inside of nla_intervals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
ee255ef8b3
commit
22bec010ba
10 changed files with 260 additions and 667 deletions
|
|
@ -35,27 +35,6 @@ void dep_intervals::set_interval_for_scalar(interval& a, const rational& v) {
|
|||
set_upper_is_inf(a, false);
|
||||
}
|
||||
|
||||
template <e_with_deps wd>
|
||||
void dep_intervals::copy_upper_bound(const interval& a, interval& i) const {
|
||||
SASSERT(a.m_upper_inf == false);
|
||||
i.m_upper_inf = false;
|
||||
m_config.set_upper(i, a.m_upper);
|
||||
i.m_upper_open = a.m_upper_open;
|
||||
if (wd == with_deps) {
|
||||
i.m_upper_dep = a.m_upper_dep;
|
||||
}
|
||||
}
|
||||
|
||||
template <e_with_deps wd>
|
||||
void dep_intervals::copy_lower_bound(const interval& a, interval& i) const {
|
||||
SASSERT(a.m_lower_inf == false);
|
||||
i.m_lower_inf = false;
|
||||
m_config.set_lower(i, a.m_lower);
|
||||
i.m_lower_open = a.m_lower_open;
|
||||
if (wd == with_deps) {
|
||||
i.m_lower_dep = a.m_lower_dep;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
|
@ -75,88 +54,6 @@ void dep_intervals::set_zero_interval_deps_for_mult(interval& a) {
|
|||
a.m_upper_dep = a.m_lower_dep;
|
||||
}
|
||||
|
||||
template <e_with_deps wd>
|
||||
void dep_intervals::mul(const rational& r, const interval& a, interval& b) const {
|
||||
if (r.is_zero()) return;
|
||||
m_imanager.mul(r.to_mpq(), a, b);
|
||||
if (wd == with_deps) {
|
||||
if (r.is_pos()) {
|
||||
b.m_lower_dep = a.m_lower_dep;
|
||||
b.m_upper_dep = a.m_upper_dep;
|
||||
}
|
||||
else {
|
||||
b.m_upper_dep = a.m_lower_dep;
|
||||
b.m_lower_dep = a.m_upper_dep;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
template <e_with_deps wd>
|
||||
dep_intervals::interval dep_intervals::intersect(const interval& a, const interval& b) const {
|
||||
interval i;
|
||||
update_lower_for_intersection<wd>(a, b, i);
|
||||
update_upper_for_intersection<wd>(a, b, i);
|
||||
return i;
|
||||
}
|
||||
|
||||
template <e_with_deps wd>
|
||||
void dep_intervals::update_lower_for_intersection(const interval& a, const interval& b, interval& i) const {
|
||||
if (a.m_lower_inf) {
|
||||
if (b.m_lower_inf)
|
||||
return;
|
||||
copy_lower_bound<wd>(b, i);
|
||||
return;
|
||||
}
|
||||
if (b.m_lower_inf) {
|
||||
SASSERT(!a.m_lower_inf);
|
||||
copy_lower_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
if (m_num_manager.lt(a.m_lower, b.m_lower)) {
|
||||
copy_lower_bound<wd>(b, i);
|
||||
return;
|
||||
}
|
||||
if (m_num_manager.gt(a.m_lower, b.m_lower)) {
|
||||
copy_lower_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
SASSERT(m_num_manager.eq(a.m_lower, b.m_lower));
|
||||
if (a.m_lower_open) { // we might consider to look at b.m_lower_open too here
|
||||
copy_lower_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
copy_lower_bound<wd>(b, i);
|
||||
}
|
||||
|
||||
template <e_with_deps wd>
|
||||
void dep_intervals::update_upper_for_intersection(const interval& a, const interval& b, interval& i) const {
|
||||
if (a.m_upper_inf) {
|
||||
if (b.m_upper_inf)
|
||||
return;
|
||||
copy_upper_bound<wd>(b, i);
|
||||
return;
|
||||
}
|
||||
if (b.m_upper_inf) {
|
||||
SASSERT(!a.m_upper_inf);
|
||||
copy_upper_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
if (m_num_manager.gt(a.m_upper, b.m_upper)) {
|
||||
copy_upper_bound<wd>(b, i);
|
||||
return;
|
||||
}
|
||||
if (m_num_manager.lt(a.m_upper, b.m_upper)) {
|
||||
copy_upper_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
SASSERT(m_num_manager.eq(a.m_upper, b.m_upper));
|
||||
if (a.m_upper_open) { // we might consider to look at b.m_upper_open too here
|
||||
copy_upper_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
|
||||
copy_upper_bound<wd>(b, i);
|
||||
}
|
||||
|
||||
|
||||
void dep_intervals::add(const rational& r, interval& a) const {
|
||||
|
|
@ -168,23 +65,6 @@ void dep_intervals::add(const rational& r, interval& a) const {
|
|||
}
|
||||
}
|
||||
|
||||
template <e_with_deps wd>
|
||||
dep_intervals::interval dep_intervals::power(const interval& a, unsigned n) {
|
||||
interval b;
|
||||
if (with_deps == wd) {
|
||||
interval_deps_combine_rule combine_rule;
|
||||
m_imanager.power(a, n, b, combine_rule);
|
||||
combine_deps(a, combine_rule, b);
|
||||
}
|
||||
else {
|
||||
m_imanager.power(a, n, b);
|
||||
}
|
||||
TRACE("dep_intervals", tout << "power of "; display(tout, a) << " = ";
|
||||
display(tout, b) << "\n"; );
|
||||
return b;
|
||||
}
|
||||
|
||||
|
||||
bool dep_intervals::separated_from_zero_on_lower(const interval& i) const {
|
||||
if (lower_is_inf(i))
|
||||
return false;
|
||||
|
|
|
|||
|
|
@ -132,6 +132,7 @@ private:
|
|||
}
|
||||
};
|
||||
|
||||
public:
|
||||
mutable unsynch_mpq_manager m_num_manager;
|
||||
mutable u_dependency_manager m_dep_manager;
|
||||
im_config m_config;
|
||||
|
|
@ -139,14 +140,27 @@ private:
|
|||
|
||||
typedef interval_manager<im_config>::interval interval;
|
||||
|
||||
unsynch_mpq_manager& num_manager() { return m_num_manager; }
|
||||
const unsynch_mpq_manager& num_manager() const { return m_num_manager; }
|
||||
|
||||
u_dependency* mk_leaf(unsigned d) { return m_dep_manager.mk_leaf(d); }
|
||||
u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_manager.mk_join(a, b); }
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
void update_lower_for_intersection(const interval& a, const interval& b, interval& i) const;
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
void update_upper_for_intersection(const interval& a, const interval& b, interval& i) const;
|
||||
void mul(const rational& r, const interval& a, interval& b) const {
|
||||
if (r.is_zero()) return;
|
||||
m_imanager.mul(r.to_mpq(), a, b);
|
||||
if (wd == with_deps) {
|
||||
if (r.is_pos()) {
|
||||
b.m_lower_dep = a.m_lower_dep;
|
||||
b.m_upper_dep = a.m_upper_dep;
|
||||
}
|
||||
else {
|
||||
b.m_upper_dep = a.m_lower_dep;
|
||||
b.m_lower_dep = a.m_upper_dep;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void mul(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); }
|
||||
void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); }
|
||||
|
|
@ -179,10 +193,8 @@ public:
|
|||
bool is_zero(const interval& a) const { return m_config.is_zero(a); }
|
||||
bool upper_is_inf(const interval& a) const { return m_config.upper_is_inf(a); }
|
||||
bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); }
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
void mul(const rational& r, const interval& a, interval& b) const;
|
||||
|
||||
bool lower_is_open(const interval& a) const { return m_config.lower_is_open(a); }
|
||||
bool upper_is_open(const interval& a) const { return m_config.upper_is_open(a); }
|
||||
void add(const rational& r, interval& a) const;
|
||||
void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); }
|
||||
void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); }
|
||||
|
|
@ -197,16 +209,43 @@ public:
|
|||
}
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
interval power(const interval& a, unsigned n);
|
||||
interval power(const interval& a, unsigned n) {
|
||||
interval b;
|
||||
if (with_deps == wd) {
|
||||
interval_deps_combine_rule combine_rule;
|
||||
m_imanager.power(a, n, b, combine_rule);
|
||||
combine_deps(a, combine_rule, b);
|
||||
}
|
||||
else {
|
||||
m_imanager.power(a, n, b);
|
||||
}
|
||||
TRACE("dep_intervals", tout << "power of "; display(tout, a) << " = ";
|
||||
display(tout, b) << "\n"; );
|
||||
return b;
|
||||
}
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
void copy_upper_bound(const interval& a, interval& i) const;
|
||||
void copy_upper_bound(const interval& a, interval& i) const {
|
||||
SASSERT(a.m_upper_inf == false);
|
||||
i.m_upper_inf = false;
|
||||
m_config.set_upper(i, a.m_upper);
|
||||
i.m_upper_open = a.m_upper_open;
|
||||
if (wd == with_deps) {
|
||||
i.m_upper_dep = a.m_upper_dep;
|
||||
}
|
||||
}
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
void copy_lower_bound(const interval& a, interval& i) const;
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
interval intersect(const interval& a, const interval& b) const;
|
||||
void copy_lower_bound(const interval& a, interval& i) const {
|
||||
SASSERT(a.m_lower_inf == false);
|
||||
i.m_lower_inf = false;
|
||||
m_config.set_lower(i, a.m_lower);
|
||||
i.m_lower_open = a.m_lower_open;
|
||||
if (wd == with_deps) {
|
||||
i.m_lower_dep = a.m_lower_dep;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void set_zero_interval_deps_for_mult(interval&);
|
||||
void set_zero_interval(interval&, u_dependency* dep = nullptr) const;
|
||||
|
|
@ -223,4 +262,75 @@ public:
|
|||
mpq const& upper(interval const& a) const { return m_config.upper(a); }
|
||||
bool is_empty(interval const& a) const;
|
||||
void set_interval_for_scalar(interval&, const rational&);
|
||||
template <typename T>
|
||||
void linearize(u_dependency* dep, T& expl) const { m_dep_manager.linearize(dep, expl); }
|
||||
|
||||
void reset() { m_dep_manager.reset(); }
|
||||
|
||||
template <enum with_deps_t wd> interval intersect(const interval& a, const interval& b) const {
|
||||
interval i;
|
||||
update_lower_for_intersection<wd>(a, b, i);
|
||||
update_upper_for_intersection<wd>(a, b, i);
|
||||
return i;
|
||||
}
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
void update_lower_for_intersection(const interval& a, const interval& b, interval& i) const {
|
||||
if (a.m_lower_inf) {
|
||||
if (b.m_lower_inf)
|
||||
return;
|
||||
copy_lower_bound<wd>(b, i);
|
||||
return;
|
||||
}
|
||||
if (b.m_lower_inf) {
|
||||
SASSERT(!a.m_lower_inf);
|
||||
copy_lower_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
if (m_num_manager.lt(a.m_lower, b.m_lower)) {
|
||||
copy_lower_bound<wd>(b, i);
|
||||
return;
|
||||
}
|
||||
if (m_num_manager.gt(a.m_lower, b.m_lower)) {
|
||||
copy_lower_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
SASSERT(m_num_manager.eq(a.m_lower, b.m_lower));
|
||||
if (a.m_lower_open) { // we might consider to look at b.m_lower_open too here
|
||||
copy_lower_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
copy_lower_bound<wd>(b, i);
|
||||
}
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
void update_upper_for_intersection(const interval& a, const interval& b, interval& i) const {
|
||||
if (a.m_upper_inf) {
|
||||
if (b.m_upper_inf)
|
||||
return;
|
||||
copy_upper_bound<wd>(b, i);
|
||||
return;
|
||||
}
|
||||
if (b.m_upper_inf) {
|
||||
SASSERT(!a.m_upper_inf);
|
||||
copy_upper_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
if (m_num_manager.gt(a.m_upper, b.m_upper)) {
|
||||
copy_upper_bound<wd>(b, i);
|
||||
return;
|
||||
}
|
||||
if (m_num_manager.lt(a.m_upper, b.m_upper)) {
|
||||
copy_upper_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
SASSERT(m_num_manager.eq(a.m_upper, b.m_upper));
|
||||
if (a.m_upper_open) { // we might consider to look at b.m_upper_open too here
|
||||
copy_upper_bound<wd>(a, i);
|
||||
return;
|
||||
}
|
||||
|
||||
copy_upper_bound<wd>(b, i);
|
||||
}
|
||||
typedef im_config::interval interv;
|
||||
};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue