mirror of
https://github.com/Z3Prover/z3
synced 2025-05-11 09:44:43 +00:00
separate into self-contained mod interval
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
04c0db75bf
commit
62b7719d5a
8 changed files with 193 additions and 150 deletions
|
|
@ -12,4 +12,5 @@ z3_add_component(polysat
|
|||
util
|
||||
dd
|
||||
simplex
|
||||
interval
|
||||
)
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@ Author:
|
|||
|
||||
#include <limits>
|
||||
#include "math/simplex/sparse_matrix.h"
|
||||
#include "math/interval/mod_interval.h"
|
||||
#include "util/heap.h"
|
||||
#include "util/map.h"
|
||||
#include "util/lbool.h"
|
||||
|
|
@ -29,54 +30,6 @@ namespace polysat {
|
|||
|
||||
typedef unsigned var_t;
|
||||
|
||||
template<typename Numeral>
|
||||
struct pp {
|
||||
Numeral n;
|
||||
pp(Numeral const& n):n(n) {}
|
||||
};
|
||||
|
||||
template<typename Numeral>
|
||||
inline std::ostream& operator<<(std::ostream& out, pp<Numeral> const& p) {
|
||||
if ((0 - p.n) < p.n)
|
||||
return out << "-" << (0 - p.n);
|
||||
return out << p.n;
|
||||
}
|
||||
|
||||
/**
|
||||
* Modular interval arithmetic
|
||||
*/
|
||||
template<typename Numeral>
|
||||
struct interval {
|
||||
bool emp { false };
|
||||
Numeral lo { 0 };
|
||||
Numeral hi { 0 };
|
||||
interval() {}
|
||||
interval(Numeral const& l, Numeral const& h): lo(l), hi(h) {}
|
||||
static interval free() { return interval(0, 0); }
|
||||
static interval empty() { interval i(0, 0); i.emp = true; return i; }
|
||||
bool is_free() const { return !emp && lo == hi; }
|
||||
bool is_empty() const { return emp; }
|
||||
bool contains(Numeral const& n) const;
|
||||
interval operator&(interval const& other) const;
|
||||
interval operator+(interval const& other) const;
|
||||
interval operator-(interval const& other) const;
|
||||
interval operator*(interval const& other) const;
|
||||
interval operator-() const;
|
||||
interval operator*(Numeral const& n) const;
|
||||
interval operator+(Numeral const& n) const { return interval(lo + n, hi + n); }
|
||||
interval operator-(Numeral const& n) const { return interval(lo - n, hi - n); }
|
||||
interval& operator+=(interval const& other) { *this = *this + other; return *this; }
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
if (is_empty()) return out << "empty";
|
||||
if (is_free()) return out << "free";
|
||||
return out << "[" << pp(lo) << ", " << pp(hi) << "[";
|
||||
}
|
||||
};
|
||||
|
||||
template<typename Numeral>
|
||||
inline std::ostream& operator<<(std::ostream& out, interval<Numeral> const& i) {
|
||||
return i.display(out);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
class fixplex {
|
||||
|
|
@ -111,7 +64,7 @@ namespace polysat {
|
|||
S_DEFAULT
|
||||
};
|
||||
|
||||
struct var_info : public interval<numeral> {
|
||||
struct var_info : public mod_interval<numeral> {
|
||||
unsigned m_base2row:29;
|
||||
unsigned m_is_base:1;
|
||||
numeral m_value { 0 };
|
||||
|
|
@ -119,8 +72,8 @@ namespace polysat {
|
|||
m_base2row(0),
|
||||
m_is_base(false)
|
||||
{}
|
||||
var_info& operator&=(interval<numeral> const& range) {
|
||||
interval<numeral>::operator=(range);
|
||||
var_info& operator&=(mod_interval<numeral> const& range) {
|
||||
mod_interval<numeral>::operator=(range);
|
||||
return *this;
|
||||
}
|
||||
};
|
||||
|
|
@ -215,7 +168,7 @@ namespace polysat {
|
|||
void fixed_var_eh(row const& r, var_t x);
|
||||
void eq_eh(var_t x, var_t y, row const& r1, row const& r2);
|
||||
void propagate_bounds(row const& r);
|
||||
void new_bound(row const& r, var_t x, interval<numeral> const& range);
|
||||
void new_bound(row const& r, var_t x, mod_interval<numeral> const& range);
|
||||
void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& value);
|
||||
numeral value2delta(var_t v, numeral const& new_value) const;
|
||||
void update_value(var_t v, numeral const& delta);
|
||||
|
|
@ -224,7 +177,7 @@ namespace polysat {
|
|||
var_t select_pivot_core(var_t x, numeral const& new_value, numeral& out_b);
|
||||
bool in_bounds(var_t v) const { return in_bounds(v, value(v)); }
|
||||
bool in_bounds(var_t v, numeral const& b) const { return in_bounds(b, m_vars[v]); }
|
||||
bool in_bounds(numeral const& val, interval<numeral> const& range) const { return range.contains(val); }
|
||||
bool in_bounds(numeral const& val, mod_interval<numeral> const& range) const { return range.contains(val); }
|
||||
bool is_free(var_t v) const { return lo(v) == hi(v); }
|
||||
bool is_non_free(var_t v) const { return !is_free(v); }
|
||||
bool is_fixed(var_t v) const { return lo(v) + 1 == hi(v); }
|
||||
|
|
|
|||
|
|
@ -20,99 +20,10 @@ Author:
|
|||
|
||||
#include "math/polysat/fixplex.h"
|
||||
#include "math/simplex/sparse_matrix_def.h"
|
||||
#include "math/interval/mod_interval_def.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
template<typename Numeral>
|
||||
bool interval<Numeral>::contains(Numeral const& n) const {
|
||||
if (is_empty())
|
||||
return false;
|
||||
if (is_free())
|
||||
return true;
|
||||
if (lo < hi)
|
||||
return lo <= n && n < hi;
|
||||
else
|
||||
return lo <= n || n < hi;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
interval<Numeral> interval<Numeral>::operator+(interval<Numeral> const& other) const {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (other.is_empty())
|
||||
return other;
|
||||
if (is_free())
|
||||
return *this;
|
||||
if (other.is_free())
|
||||
return other;
|
||||
Numeral sz = (hi - lo) + (other.hi - other.lo);
|
||||
if (sz < (hi - lo))
|
||||
return interval::free();
|
||||
return interval(lo + other.lo, hi + other.hi);
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
interval<Numeral> interval<Numeral>::operator-(interval<Numeral> const& other) const {
|
||||
return *this + (-other);
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
interval<Numeral> interval<Numeral>::operator-() const {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (is_free())
|
||||
return *this;
|
||||
return interval(1 - hi, 1 - lo);
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
interval<Numeral> interval<Numeral>::operator*(Numeral const& n) const {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (n == 0)
|
||||
return interval(0, 1);
|
||||
if (n == 1)
|
||||
return *this;
|
||||
if (is_free())
|
||||
return *this;
|
||||
Numeral sz = hi - lo;
|
||||
if (0 - n < n) {
|
||||
Numeral mn = 0 - n;
|
||||
Numeral mz = mn * sz;
|
||||
if (mz / mn != sz)
|
||||
return interval::free();
|
||||
return interval((hi - 1) * n, n * lo + 1);
|
||||
}
|
||||
else {
|
||||
Numeral mz = n * sz;
|
||||
if (mz / n != sz)
|
||||
return interval::free();
|
||||
return interval(n * lo, n * (hi - 1) + 1);
|
||||
}
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
interval<Numeral> interval<Numeral>::operator&(interval const& other) const {
|
||||
Numeral l, h;
|
||||
if (is_free() || other.is_empty())
|
||||
return other;
|
||||
if (other.is_free() || is_empty())
|
||||
return *this;
|
||||
if (contains(other.lo))
|
||||
l = other.lo;
|
||||
else if (other.contains(lo))
|
||||
l = lo;
|
||||
else
|
||||
return interval::empty();
|
||||
if (contains(other.hi - 1))
|
||||
h = other.hi;
|
||||
else if (other.contains(hi - 1))
|
||||
h = hi;
|
||||
else
|
||||
return interval::empty();
|
||||
return interval(l, h);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
fixplex<Ext>::~fixplex() {
|
||||
reset();
|
||||
|
|
@ -513,7 +424,7 @@ namespace polysat {
|
|||
bool fixplex<Ext>::is_infeasible_row(var_t x) {
|
||||
SASSERT(is_base(x));
|
||||
auto r = base2row(x);
|
||||
interval<numeral> range(0, 1);
|
||||
mod_interval<numeral> range(0, 1);
|
||||
for (auto const& e : M.row_entries(row(r))) {
|
||||
var_t v = e.var();
|
||||
numeral const& c = e.coeff();
|
||||
|
|
@ -915,7 +826,7 @@ namespace polysat {
|
|||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::propagate_bounds(row const& r) {
|
||||
interval<numeral> range(0, 1);
|
||||
mod_interval<numeral> range(0, 1);
|
||||
numeral free_c = 0;
|
||||
var_t free_v = null_var;
|
||||
for (auto const& e : M.row_entries(r)) {
|
||||
|
|
@ -949,7 +860,7 @@ namespace polysat {
|
|||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::new_bound(row const& r, var_t x, interval<numeral> const& range) {
|
||||
void fixplex<Ext>::new_bound(row const& r, var_t x, mod_interval<numeral> const& range) {
|
||||
if (range.is_free())
|
||||
return;
|
||||
m_vars[x] &= range;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue