mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
Move modular interval to interval directory
This commit is contained in:
Nikolaj Bjorner
parent
0f3c56213e
commit
91d6082f2f
|
|
@ -47,5 +47,6 @@ z3_add_component(rewriter
|
||||||
ast
|
ast
|
||||||
params
|
params
|
||||||
automata
|
automata
|
||||||
|
interval
|
||||||
polynomial
|
polynomial
|
||||||
)
|
)
|
||||||
|
|
|
||||||
|
|
@ -17,227 +17,10 @@ Author:
|
||||||
|
|
||||||
#pragma once
|
#pragma once
|
||||||
|
|
||||||
|
#include "math/interval/mod_interval.h"
|
||||||
|
|
||||||
namespace bv {
|
namespace bv {
|
||||||
|
|
||||||
template<typename T, typename Base>
|
|
||||||
struct interval_tpl : public Base {
|
|
||||||
T l, h;
|
|
||||||
unsigned sz = 0;
|
|
||||||
bool tight = true;
|
|
||||||
|
|
||||||
interval_tpl(T const& l, T const& h, unsigned sz, bool tight = false): l(l), h(h), sz(sz), tight(tight) {}
|
|
||||||
interval_tpl() {}
|
|
||||||
|
|
||||||
bool invariant() const {
|
|
||||||
return
|
|
||||||
0 <= l && (l <= Base::bound(sz)) &&
|
|
||||||
0 <= h && (h <= Base::bound(sz)) &&
|
|
||||||
(!is_wrapped() || l != h + 1);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool is_full() const {
|
|
||||||
return l == 0 && h == Base::bound(sz);
|
|
||||||
}
|
|
||||||
bool is_wrapped() const { return l > h; }
|
|
||||||
bool is_singleton() const { return l == h; }
|
|
||||||
|
|
||||||
bool operator==(const interval_tpl<T, Base>& b) const {
|
|
||||||
SASSERT(sz == b.sz);
|
|
||||||
return l == b.l && h == b.h && tight == b.tight;
|
|
||||||
}
|
|
||||||
bool operator!=(const interval_tpl& b) const { return !(*this == b); }
|
|
||||||
|
|
||||||
bool implies(const interval_tpl<T, Base>& b) const {
|
|
||||||
if (b.is_full())
|
|
||||||
return true;
|
|
||||||
else if (is_full())
|
|
||||||
return false;
|
|
||||||
else if (is_wrapped())
|
|
||||||
// l >= b.l >= b.h >= h
|
|
||||||
return b.is_wrapped() && h <= b.h && l >= b.l;
|
|
||||||
else if (b.is_wrapped())
|
|
||||||
// b.l > b.h >= h >= l
|
|
||||||
// h >= l >= b.l > b.h
|
|
||||||
return h <= b.h || l >= b.l;
|
|
||||||
else
|
|
||||||
return l >= b.l && h <= b.h;
|
|
||||||
}
|
|
||||||
|
|
||||||
/// return false if intersection is unsat
|
|
||||||
bool intersect(const interval_tpl<T, Base>& b, interval_tpl& result) const {
|
|
||||||
if (is_full() || *this == b) {
|
|
||||||
result = b;
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
if (b.is_full()) {
|
|
||||||
result = *this;
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (is_wrapped()) {
|
|
||||||
if (b.is_wrapped()) {
|
|
||||||
if (h >= b.l)
|
|
||||||
result = b;
|
|
||||||
else if (b.h >= l)
|
|
||||||
result = *this;
|
|
||||||
else
|
|
||||||
result = interval_tpl(std::max(l, b.l), std::min(h, b.h), sz);
|
|
||||||
}
|
|
||||||
else
|
|
||||||
return b.intersect(*this, result);
|
|
||||||
}
|
|
||||||
else if (b.is_wrapped()) {
|
|
||||||
// ... b.h ... l ... h ... b.l ..
|
|
||||||
if (h < b.l && l > b.h)
|
|
||||||
return false;
|
|
||||||
// ... l ... b.l ... h ...
|
|
||||||
if (h >= b.l && l <= b.h)
|
|
||||||
result = b;
|
|
||||||
else if (h >= b.l)
|
|
||||||
result = interval_tpl(b.l, h, sz);
|
|
||||||
else {
|
|
||||||
// ... l .. b.h .. h .. b.l ...
|
|
||||||
SASSERT(l <= b.h);
|
|
||||||
result = interval_tpl(l, std::min(h, b.h), sz);
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
if (l > b.h || h < b.l)
|
|
||||||
return false;
|
|
||||||
|
|
||||||
// 0 .. l.. l' ... h ... h'
|
|
||||||
result = interval_tpl(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight);
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
/// return false if negation is empty
|
|
||||||
bool negate(interval_tpl<T, Base>& result) const {
|
|
||||||
if (!tight)
|
|
||||||
result = interval_tpl(Base::zero(), Base::bound(sz), sz, true);
|
|
||||||
else if (is_full())
|
|
||||||
return false;
|
|
||||||
else if (l == 0 && Base::bound(sz) == h)
|
|
||||||
result = interval_tpl(Base::zero(), Base::bound(sz), sz);
|
|
||||||
else if (l == 0)
|
|
||||||
result = interval_tpl(h + 1, Base::bound(sz), sz);
|
|
||||||
else if (Base::bound(sz) == h)
|
|
||||||
result = interval_tpl(Base::zero(), l - 1, sz);
|
|
||||||
else
|
|
||||||
result = interval_tpl(h + 1, l - 1, sz);
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
struct rinterval_base {
|
|
||||||
static rational bound(unsigned sz) {
|
|
||||||
return rational::power_of_two(sz) - 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
static rational zero() { return rational::zero(); }
|
|
||||||
};
|
|
||||||
|
|
||||||
struct rinterval : public interval_tpl<rational, rinterval_base> {
|
|
||||||
rinterval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
|
|
||||||
this->l = l; this->h = h; this->sz = sz; this->tight = tight;
|
|
||||||
}
|
|
||||||
rinterval() { l = 0; h = 0; tight = true; }
|
|
||||||
};
|
|
||||||
|
|
||||||
struct iinterval_base {
|
|
||||||
static uint64_t uMaxInt(unsigned sz) {
|
|
||||||
SASSERT(sz <= 64);
|
|
||||||
return ULLONG_MAX >> (64u - sz);
|
|
||||||
}
|
|
||||||
|
|
||||||
static uint64_t bound(unsigned sz) { return uMaxInt(sz); }
|
|
||||||
static uint64_t zero() { return 0; }
|
|
||||||
};
|
|
||||||
|
|
||||||
struct iinterval : public interval_tpl<uint64_t, iinterval_base> {
|
|
||||||
iinterval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) {
|
|
||||||
this->l = l; this->h = h; this->sz = sz; this->tight = tight;
|
|
||||||
}
|
|
||||||
iinterval() { l = 0; h = 0; sz = 0; tight = true; }
|
|
||||||
};
|
|
||||||
|
|
||||||
struct interval {
|
|
||||||
bool is_small = true;
|
|
||||||
iinterval i;
|
|
||||||
rinterval r;
|
|
||||||
|
|
||||||
interval() {}
|
|
||||||
|
|
||||||
interval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
|
|
||||||
if (sz <= 64) {
|
|
||||||
is_small = true;
|
|
||||||
i.l = l.get_uint64();
|
|
||||||
i.h = h.get_uint64();
|
|
||||||
i.tight = tight;
|
|
||||||
i.sz = sz;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
is_small = false;
|
|
||||||
r.l = l;
|
|
||||||
r.h = h;
|
|
||||||
r.tight = tight;
|
|
||||||
r.sz = sz;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned size() const {
|
|
||||||
return is_small ? i.sz : r.sz;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool negate(interval& result) const {
|
|
||||||
result.is_small = is_small;
|
|
||||||
if (is_small)
|
|
||||||
return i.negate(result.i);
|
|
||||||
else
|
|
||||||
return r.negate(result.r);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool intersect(interval const& b, interval & result) const {
|
|
||||||
result.is_small = is_small;
|
|
||||||
SASSERT(b.is_small == is_small);
|
|
||||||
if (is_small)
|
|
||||||
return i.intersect(b.i, result.i);
|
|
||||||
else
|
|
||||||
return r.intersect(b.r, result.r);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool operator==(interval const& other) const {
|
|
||||||
SASSERT(is_small == other.is_small);
|
|
||||||
return is_small ? i == other.i : r == other.r;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool operator!=(interval const& other) const {
|
|
||||||
return !(*this == other);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool is_singleton() const { return is_small ? i.is_singleton() : r.is_singleton(); }
|
|
||||||
|
|
||||||
bool is_full() const { return is_small ? i.is_full() : r.is_full(); }
|
|
||||||
|
|
||||||
bool tight() const { return is_small ? i.tight : r.tight; }
|
|
||||||
|
|
||||||
bool implies(const interval& b) const {
|
|
||||||
SASSERT(is_small == b.is_small);
|
|
||||||
return is_small ? i.implies(b.i) : r.implies(b.r);
|
|
||||||
}
|
|
||||||
|
|
||||||
rational lo() const { return is_small ? rational(i.l, rational::ui64()) : r.l; }
|
|
||||||
rational hi() const { return is_small ? rational(i.h, rational::ui64()) : r.h; }
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
inline std::ostream& operator<<(std::ostream& o, const interval& I) {
|
|
||||||
if (I.is_small)
|
|
||||||
return o << "[" << I.i.l << ", " << I.i.h << "]";
|
|
||||||
else
|
|
||||||
return o << "[" << I.r.l << ", " << I.r.h << "]";
|
|
||||||
}
|
|
||||||
|
|
||||||
struct undo_bound {
|
struct undo_bound {
|
||||||
expr* e = nullptr;
|
expr* e = nullptr;
|
||||||
|
|
|
||||||
239
src/math/interval/mod_interval.h
Normal file
239
src/math/interval/mod_interval.h
Normal file
|
|
@ -0,0 +1,239 @@
|
||||||
|
/*++
|
||||||
|
Copyright (c) 2017 Microsoft Corporation
|
||||||
|
|
||||||
|
Module Name:
|
||||||
|
|
||||||
|
mod_interval.h
|
||||||
|
|
||||||
|
Abstract:
|
||||||
|
|
||||||
|
Modular interval for bit-vector comparisons
|
||||||
|
|
||||||
|
Author:
|
||||||
|
|
||||||
|
Nikolaj and Nuno
|
||||||
|
|
||||||
|
--*/
|
||||||
|
|
||||||
|
namespace bv {
|
||||||
|
|
||||||
|
template<typename T, typename Base>
|
||||||
|
struct interval_tpl : public Base {
|
||||||
|
T l, h;
|
||||||
|
unsigned sz = 0;
|
||||||
|
bool tight = true;
|
||||||
|
|
||||||
|
interval_tpl(T const& l, T const& h, unsigned sz, bool tight = false): l(l), h(h), sz(sz), tight(tight) {}
|
||||||
|
interval_tpl() {}
|
||||||
|
|
||||||
|
bool invariant() const {
|
||||||
|
return
|
||||||
|
0 <= l && (l <= Base::bound(sz)) &&
|
||||||
|
0 <= h && (h <= Base::bound(sz)) &&
|
||||||
|
(!is_wrapped() || l != h + 1);
|
||||||
|
}
|
||||||
|
|
||||||
|
bool is_full() const {
|
||||||
|
return l == 0 && h == Base::bound(sz);
|
||||||
|
}
|
||||||
|
bool is_wrapped() const { return l > h; }
|
||||||
|
bool is_singleton() const { return l == h; }
|
||||||
|
|
||||||
|
bool operator==(const interval_tpl<T, Base>& b) const {
|
||||||
|
SASSERT(sz == b.sz);
|
||||||
|
return l == b.l && h == b.h && tight == b.tight;
|
||||||
|
}
|
||||||
|
bool operator!=(const interval_tpl& b) const { return !(*this == b); }
|
||||||
|
|
||||||
|
bool implies(const interval_tpl<T, Base>& b) const {
|
||||||
|
if (b.is_full())
|
||||||
|
return true;
|
||||||
|
else if (is_full())
|
||||||
|
return false;
|
||||||
|
else if (is_wrapped())
|
||||||
|
// l >= b.l >= b.h >= h
|
||||||
|
return b.is_wrapped() && h <= b.h && l >= b.l;
|
||||||
|
else if (b.is_wrapped())
|
||||||
|
// b.l > b.h >= h >= l
|
||||||
|
// h >= l >= b.l > b.h
|
||||||
|
return h <= b.h || l >= b.l;
|
||||||
|
else
|
||||||
|
return l >= b.l && h <= b.h;
|
||||||
|
}
|
||||||
|
|
||||||
|
/// return false if intersection is unsat
|
||||||
|
bool intersect(const interval_tpl<T, Base>& b, interval_tpl& result) const {
|
||||||
|
if (is_full() || *this == b) {
|
||||||
|
result = b;
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
if (b.is_full()) {
|
||||||
|
result = *this;
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
if (is_wrapped()) {
|
||||||
|
if (b.is_wrapped()) {
|
||||||
|
if (h >= b.l)
|
||||||
|
result = b;
|
||||||
|
else if (b.h >= l)
|
||||||
|
result = *this;
|
||||||
|
else
|
||||||
|
result = interval_tpl(std::max(l, b.l), std::min(h, b.h), sz);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
return b.intersect(*this, result);
|
||||||
|
}
|
||||||
|
else if (b.is_wrapped()) {
|
||||||
|
// ... b.h ... l ... h ... b.l ..
|
||||||
|
if (h < b.l && l > b.h)
|
||||||
|
return false;
|
||||||
|
// ... l ... b.l ... h ...
|
||||||
|
if (h >= b.l && l <= b.h)
|
||||||
|
result = b;
|
||||||
|
else if (h >= b.l)
|
||||||
|
result = interval_tpl(b.l, h, sz);
|
||||||
|
else {
|
||||||
|
// ... l .. b.h .. h .. b.l ...
|
||||||
|
SASSERT(l <= b.h);
|
||||||
|
result = interval_tpl(l, std::min(h, b.h), sz);
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
if (l > b.h || h < b.l)
|
||||||
|
return false;
|
||||||
|
|
||||||
|
// 0 .. l.. l' ... h ... h'
|
||||||
|
result = interval_tpl(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight);
|
||||||
|
}
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
/// return false if negation is empty
|
||||||
|
bool negate(interval_tpl<T, Base>& result) const {
|
||||||
|
if (!tight)
|
||||||
|
result = interval_tpl(Base::zero(), Base::bound(sz), sz, true);
|
||||||
|
else if (is_full())
|
||||||
|
return false;
|
||||||
|
else if (l == 0 && Base::bound(sz) == h)
|
||||||
|
result = interval_tpl(Base::zero(), Base::bound(sz), sz);
|
||||||
|
else if (l == 0)
|
||||||
|
result = interval_tpl(h + 1, Base::bound(sz), sz);
|
||||||
|
else if (Base::bound(sz) == h)
|
||||||
|
result = interval_tpl(Base::zero(), l - 1, sz);
|
||||||
|
else
|
||||||
|
result = interval_tpl(h + 1, l - 1, sz);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
};
|
||||||
|
|
||||||
|
struct rinterval_base {
|
||||||
|
static rational bound(unsigned sz) {
|
||||||
|
return rational::power_of_two(sz) - 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
static rational zero() { return rational::zero(); }
|
||||||
|
};
|
||||||
|
|
||||||
|
struct rinterval : public interval_tpl<rational, rinterval_base> {
|
||||||
|
rinterval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
|
||||||
|
this->l = l; this->h = h; this->sz = sz; this->tight = tight;
|
||||||
|
}
|
||||||
|
rinterval() { l = 0; h = 0; tight = true; }
|
||||||
|
};
|
||||||
|
|
||||||
|
struct iinterval_base {
|
||||||
|
static uint64_t uMaxInt(unsigned sz) {
|
||||||
|
SASSERT(sz <= 64);
|
||||||
|
return ULLONG_MAX >> (64u - sz);
|
||||||
|
}
|
||||||
|
|
||||||
|
static uint64_t bound(unsigned sz) { return uMaxInt(sz); }
|
||||||
|
static uint64_t zero() { return 0; }
|
||||||
|
};
|
||||||
|
|
||||||
|
struct iinterval : public interval_tpl<uint64_t, iinterval_base> {
|
||||||
|
iinterval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) {
|
||||||
|
this->l = l; this->h = h; this->sz = sz; this->tight = tight;
|
||||||
|
}
|
||||||
|
iinterval() { l = 0; h = 0; sz = 0; tight = true; }
|
||||||
|
};
|
||||||
|
|
||||||
|
struct interval {
|
||||||
|
bool is_small = true;
|
||||||
|
iinterval i;
|
||||||
|
rinterval r;
|
||||||
|
|
||||||
|
interval() {}
|
||||||
|
|
||||||
|
interval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
|
||||||
|
if (sz <= 64) {
|
||||||
|
is_small = true;
|
||||||
|
i.l = l.get_uint64();
|
||||||
|
i.h = h.get_uint64();
|
||||||
|
i.tight = tight;
|
||||||
|
i.sz = sz;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
is_small = false;
|
||||||
|
r.l = l;
|
||||||
|
r.h = h;
|
||||||
|
r.tight = tight;
|
||||||
|
r.sz = sz;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
unsigned size() const {
|
||||||
|
return is_small ? i.sz : r.sz;
|
||||||
|
}
|
||||||
|
|
||||||
|
bool negate(interval& result) const {
|
||||||
|
result.is_small = is_small;
|
||||||
|
if (is_small)
|
||||||
|
return i.negate(result.i);
|
||||||
|
else
|
||||||
|
return r.negate(result.r);
|
||||||
|
}
|
||||||
|
|
||||||
|
bool intersect(interval const& b, interval & result) const {
|
||||||
|
result.is_small = is_small;
|
||||||
|
SASSERT(b.is_small == is_small);
|
||||||
|
if (is_small)
|
||||||
|
return i.intersect(b.i, result.i);
|
||||||
|
else
|
||||||
|
return r.intersect(b.r, result.r);
|
||||||
|
}
|
||||||
|
|
||||||
|
bool operator==(interval const& other) const {
|
||||||
|
SASSERT(is_small == other.is_small);
|
||||||
|
return is_small ? i == other.i : r == other.r;
|
||||||
|
}
|
||||||
|
|
||||||
|
bool operator!=(interval const& other) const {
|
||||||
|
return !(*this == other);
|
||||||
|
}
|
||||||
|
|
||||||
|
bool is_singleton() const { return is_small ? i.is_singleton() : r.is_singleton(); }
|
||||||
|
|
||||||
|
bool is_full() const { return is_small ? i.is_full() : r.is_full(); }
|
||||||
|
|
||||||
|
bool tight() const { return is_small ? i.tight : r.tight; }
|
||||||
|
|
||||||
|
bool implies(const interval& b) const {
|
||||||
|
SASSERT(is_small == b.is_small);
|
||||||
|
return is_small ? i.implies(b.i) : r.implies(b.r);
|
||||||
|
}
|
||||||
|
|
||||||
|
rational lo() const { return is_small ? rational(i.l, rational::ui64()) : r.l; }
|
||||||
|
rational hi() const { return is_small ? rational(i.h, rational::ui64()) : r.h; }
|
||||||
|
};
|
||||||
|
|
||||||
|
|
||||||
|
inline std::ostream& operator<<(std::ostream& o, const interval& I) {
|
||||||
|
if (I.is_small)
|
||||||
|
return o << "[" << I.i.l << ", " << I.i.h << "]";
|
||||||
|
else
|
||||||
|
return o << "[" << I.r.l << ", " << I.r.h << "]";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -20,13 +20,12 @@ Author:
|
||||||
|
|
||||||
#include "ast/bv_decl_plugin.h"
|
#include "ast/bv_decl_plugin.h"
|
||||||
#include "ast/ast_pp.h"
|
#include "ast/ast_pp.h"
|
||||||
|
#include "ast/rewriter/bv_bounds_base.h"
|
||||||
#include "ast/simplifiers/dominator_simplifier.h"
|
#include "ast/simplifiers/dominator_simplifier.h"
|
||||||
|
#include "ast/simplifiers/bv_bounds_simplifier.h"
|
||||||
#include "tactic/bv/bv_bounds_tactic.h"
|
#include "tactic/bv/bv_bounds_tactic.h"
|
||||||
#include "tactic/core/ctx_simplify_tactic.h"
|
#include "tactic/core/ctx_simplify_tactic.h"
|
||||||
#include "tactic/dependent_expr_state_tactic.h"
|
#include "tactic/dependent_expr_state_tactic.h"
|
||||||
#include "ast/rewriter/bv_bounds_base.h"
|
|
||||||
#include "ast/simplifiers/bv_bounds_simplifier.h"
|
|
||||||
|
|
||||||
#include <climits>
|
#include <climits>
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue