From 91d6082f2fd764340f7c0fa0aa0c97861a104d9b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Jan 2023 17:55:36 -0800
Subject: [PATCH] Move modular interval to interval directory
---
src/ast/rewriter/CMakeLists.txt | 1 +
src/ast/rewriter/bv_bounds_base.h | 221 +-------------------------
src/math/interval/mod_interval.h | 239 +++++++++++++++++++++++++++++
src/tactic/bv/bv_bounds_tactic.cpp | 5 +-
4 files changed, 244 insertions(+), 222 deletions(-)
create mode 100644 src/math/interval/mod_interval.h
diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index 17410807a..df803b0f1 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/src/ast/rewriter/CMakeLists.txt
@@ -47,5 +47,6 @@ z3_add_component(rewriter
ast
params
automata
+ interval
polynomial
)
diff --git a/src/ast/rewriter/bv_bounds_base.h b/src/ast/rewriter/bv_bounds_base.h
index 8ddb429e9..840cf6e3e 100644
--- a/src/ast/rewriter/bv_bounds_base.h
+++ b/src/ast/rewriter/bv_bounds_base.h
@@ -17,227 +17,10 @@ Author:
#pragma once
+#include "math/interval/mod_interval.h"
+
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 {
expr* e = nullptr;
diff --git a/src/math/interval/mod_interval.h b/src/math/interval/mod_interval.h
new file mode 100644
index 000000000..88acdd8d6
--- /dev/null
+++ b/src/math/interval/mod_interval.h
@@ -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 << "]";
+ }
+}
diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index 45ff60ec0..5f856800e 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -20,13 +20,12 @@ Author:
#include "ast/bv_decl_plugin.h"
#include "ast/ast_pp.h"
+#include "ast/rewriter/bv_bounds_base.h"
#include "ast/simplifiers/dominator_simplifier.h"
+#include "ast/simplifiers/bv_bounds_simplifier.h"
#include "tactic/bv/bv_bounds_tactic.h"
#include "tactic/core/ctx_simplify_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>