mirror of
https://github.com/Z3Prover/z3
synced 2025-08-13 22:41:15 +00:00
4a870966ad
set UNIT_PROPAGATE_BOUNDS 1 to use the unit propagation version. It applies unit propagation eagerly (does not depend on checking LIA consistency before final check) and avoid creating new literals in most cases
435 lines
16 KiB
C++
435 lines
16 KiB
C++
/*++
|
|
Copyright (c) 2017 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
dep_intervals.h
|
|
|
|
Abstract:
|
|
|
|
intervals with dependency tracking.
|
|
|
|
Author:
|
|
Nikolaj Bjorner (nbjorner)
|
|
Lev Nachmanson (levnach)
|
|
|
|
Revision History:
|
|
|
|
extracted from nla_intervals.h
|
|
|
|
--*/
|
|
|
|
#pragma once
|
|
#include "util/dependency.h"
|
|
#include "util/region.h"
|
|
#include "util/rational.h"
|
|
#include "util/rlimit.h"
|
|
#include "math/interval/interval.h"
|
|
|
|
class dep_intervals {
|
|
|
|
public:
|
|
enum with_deps_t { with_deps, without_deps };
|
|
|
|
private:
|
|
class im_config {
|
|
unsynch_mpq_manager& m_manager;
|
|
u_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;
|
|
u_dependency* m_lower_dep; // justification for the lower bound
|
|
u_dependency* m_upper_dep; // justification for the upper bound
|
|
};
|
|
|
|
void add_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
|
|
auto lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_combine);
|
|
auto upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine);
|
|
i.m_lower_dep = lower_dep;
|
|
i.m_upper_dep = upper_dep;
|
|
}
|
|
|
|
void add_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const {
|
|
auto lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_combine);
|
|
auto upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_combine);
|
|
i.m_lower_dep = lower_dep;
|
|
i.m_upper_dep = upper_dep;
|
|
}
|
|
|
|
|
|
// 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_inf(interval const& a) const { return upper_is_inf(a) && lower_is_inf(a); }
|
|
bool is_zero(interval const& a) const {
|
|
return (!lower_is_inf(a)) && (!upper_is_inf(a)) &&
|
|
(!lower_is_open(a)) && (!upper_is_open(a)) &&
|
|
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; }
|
|
void set_lower_dep(interval& a, u_dependency* d) const { a.m_lower_dep = d; }
|
|
void set_upper_dep(interval& a, u_dependency* d) const { a.m_upper_dep = d; }
|
|
|
|
// Reference to numeral manager
|
|
numeral_manager& m() const { return m_manager; }
|
|
|
|
im_config(numeral_manager& m, u_dependency_manager& d) :m_manager(m), m_dep_manager(d) {}
|
|
private:
|
|
u_dependency* mk_dependency(interval const& a, interval const& b, deps_combine_rule bd) const {
|
|
u_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;
|
|
}
|
|
|
|
u_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const {
|
|
u_dependency* dep = nullptr;
|
|
if (dep_in_lower1(bd)) {
|
|
dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
|
|
}
|
|
if (dep_in_upper1(bd)) {
|
|
dep = m_dep_manager.mk_join(dep, a.m_upper_dep);
|
|
}
|
|
return dep;
|
|
}
|
|
};
|
|
|
|
|
|
public:
|
|
typedef interval_manager<im_config>::interval interval;
|
|
|
|
u_dependency_manager& m_dep_manager;
|
|
mutable unsynch_mpq_manager m_num_manager;
|
|
|
|
im_config m_config;
|
|
mutable interval_manager<im_config> m_imanager;
|
|
|
|
|
|
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); }
|
|
|
|
|
|
public:
|
|
u_dependency_manager& dep_manager() { return m_dep_manager; }
|
|
|
|
dep_intervals(u_dependency_manager& dm, reslimit& lim) :
|
|
m_dep_manager(dm),
|
|
m_config(m_num_manager, dm),
|
|
m_imanager(lim, im_config(m_num_manager, dm))
|
|
{}
|
|
|
|
std::ostream& display(std::ostream& out, const interval& i) const;
|
|
void set_lower(interval& a, rational const& n) const { m_config.set_lower(a, n.to_mpq()); }
|
|
void set_upper(interval& a, rational const& n) const { m_config.set_upper(a, n.to_mpq()); }
|
|
void set_lower_is_open(interval& a, bool strict) const { m_config.set_lower_is_open(a, strict); }
|
|
void set_lower_is_inf(interval& a, bool inf) const { m_config.set_lower_is_inf(a, inf); }
|
|
void set_upper_is_open(interval& a, bool strict) const { m_config.set_upper_is_open(a, strict); }
|
|
void set_upper_is_inf(interval& a, bool inf) const { m_config.set_upper_is_inf(a, inf); }
|
|
void set_lower_dep(interval& a, u_dependency* d) const { m_config.set_lower_dep(a, d); }
|
|
void set_upper_dep(interval& a, u_dependency* d) const { m_config.set_upper_dep(a, d); }
|
|
u_dependency* get_lower_dep(interval const& a) const { return a.m_lower_dep; }
|
|
u_dependency* get_upper_dep(interval const& a) const { return a.m_upper_dep; }
|
|
void reset(interval& a) const { set_lower_is_inf(a, true); set_upper_is_inf(a, true); }
|
|
void set_value(interval& a, rational const& n) const {
|
|
set_lower(a, n);
|
|
set_upper(a, n);
|
|
set_lower_is_open(a, false);
|
|
set_upper_is_open(a, false);
|
|
set_lower_is_inf(a, false);
|
|
set_upper_is_inf(a, false);
|
|
}
|
|
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); }
|
|
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); }
|
|
template <typename T>
|
|
void get_upper_dep(const interval& a, T& expl) { linearize(a.m_upper_dep, expl); }
|
|
template <typename T>
|
|
void get_lower_dep(const interval& a, T& expl) { linearize(a.m_lower_dep, expl); }
|
|
bool is_above(const interval& a, const rational& r) const;
|
|
bool is_below(const interval& a, const rational& r) const;
|
|
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); }
|
|
|
|
template <enum with_deps_t wd>
|
|
void set(interval& a, const interval& b) const {
|
|
m_imanager.set(a, b);
|
|
if (wd == with_deps) {
|
|
a.m_lower_dep = b.m_lower_dep;
|
|
a.m_upper_dep = b.m_upper_dep;
|
|
}
|
|
}
|
|
|
|
template <enum with_deps_t wd>
|
|
void power(const interval& a, unsigned n, interval& b) {
|
|
if (n == 1 && &a == &b)
|
|
return;
|
|
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"; );
|
|
}
|
|
|
|
template <enum with_deps_t wd>
|
|
void mul(const rational& r, const interval& a, interval& b) const {
|
|
m_imanager.mul(r.to_mpq(), a, b);
|
|
if (wd == with_deps) {
|
|
auto lower_dep = a.m_lower_dep;
|
|
auto upper_dep = a.m_upper_dep;
|
|
if (!r.is_pos()) {
|
|
std::swap(lower_dep, upper_dep);
|
|
}
|
|
b.m_lower_dep = lower_dep;
|
|
b.m_upper_dep = upper_dep;
|
|
}
|
|
}
|
|
|
|
template <enum with_deps_t wd>
|
|
void mul(const interval& a, const interval& b, interval& c) {
|
|
if (wd == with_deps) {
|
|
interval_deps_combine_rule comb_rule;
|
|
mul(a, b, c, comb_rule);
|
|
combine_deps(a, b, comb_rule, c);
|
|
}
|
|
else {
|
|
mul(a, b, c);
|
|
}
|
|
}
|
|
|
|
template <enum with_deps_t wd>
|
|
void div(const interval& a, const interval& b, interval& c) {
|
|
if (wd == with_deps) {
|
|
interval_deps_combine_rule comb_rule;
|
|
m_imanager.div(a, b, c, comb_rule);
|
|
combine_deps(a, b, comb_rule, c);
|
|
}
|
|
else {
|
|
m_imanager.div(a, b, c);
|
|
}
|
|
}
|
|
|
|
template <enum with_deps_t wd>
|
|
void add(const interval& a, const interval& b, interval& c) {
|
|
if (wd == with_deps) {
|
|
interval_deps_combine_rule comb_rule;
|
|
add(a, b, c, comb_rule);
|
|
combine_deps(a, b, comb_rule, c);
|
|
}
|
|
else {
|
|
add(a, b, c);
|
|
}
|
|
}
|
|
|
|
template <enum with_deps_t wd>
|
|
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 {
|
|
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;
|
|
bool is_inf(const interval& i) const { return m_config.is_inf(i); }
|
|
bool separated_from_zero_on_lower(const interval&) const;
|
|
bool separated_from_zero_on_upper(const interval&) const;
|
|
inline bool separated_from_zero(const interval& i) const {
|
|
return separated_from_zero_on_upper(i) || separated_from_zero_on_lower(i);
|
|
}
|
|
// if the separation happens then call f()
|
|
template <typename T>
|
|
bool check_interval_for_conflict_on_zero(const interval& i, u_dependency* dep, std::function<void (const T&)> f) {
|
|
return check_interval_for_conflict_on_zero_lower(i, dep, f) || check_interval_for_conflict_on_zero_upper(i, dep, f);
|
|
}
|
|
template <typename T>
|
|
bool check_interval_for_conflict_on_zero_lower(const interval& i, u_dependency* dep, std::function<void (const T&)> f) {
|
|
if (!separated_from_zero_on_lower(i)) {
|
|
return false;
|
|
}
|
|
TRACE("dep_intervals", display(tout, i););
|
|
dep = m_dep_manager.mk_join(dep, i.m_lower_dep);
|
|
T expl;
|
|
linearize(dep, expl);
|
|
f(expl);
|
|
return true;
|
|
}
|
|
template <typename T>
|
|
bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency* dep, std::function<void (const T&)> f) {
|
|
if (!separated_from_zero_on_upper(i))
|
|
return false;
|
|
TRACE("dep_intervals", display(tout, i););
|
|
dep = m_dep_manager.mk_join(dep, i.m_upper_dep);
|
|
T expl;
|
|
linearize(dep, expl);
|
|
f(expl);
|
|
return true;
|
|
}
|
|
mpq const& lower(interval const& a) const { return m_config.lower(a); }
|
|
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 {
|
|
vector<unsigned, false> v;
|
|
m_dep_manager.linearize(dep, v);
|
|
for (auto ci: v)
|
|
expl.push_back(ci);
|
|
}
|
|
|
|
|
|
void reset() { }
|
|
|
|
void del(interval& i) { m_imanager.del(i); }
|
|
|
|
template <enum with_deps_t wd> void intersect(const interval& a, const interval& b, interval& i) const {
|
|
update_lower_for_intersection<wd>(a, b, i);
|
|
update_upper_for_intersection<wd>(a, b, 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);
|
|
}
|
|
private:
|
|
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); }
|
|
|
|
void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
|
|
m_config.add_deps(a, b, deps, i);
|
|
}
|
|
|
|
void combine_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const {
|
|
m_config.add_deps(a, deps, i);
|
|
}
|
|
|
|
};
|
|
|
|
typedef _scoped_interval<dep_intervals> scoped_dep_interval;
|
|
typedef dep_intervals::interval dep_interval;
|