mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-02 19:08:47 +00:00
Code Activity

include path

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-03 09:15:21 -07:00
parent 674e030456
commit c3ac079272
4 changed files with 37 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/bigfix/kremlib/LowStar_Endianness.h
View file

@ -11,7 +11,7 @@
#include "math/bigfix/kremlin/lowstar_endianness.h" #include "math/bigfix/kremlin/lowstar_endianness.h"
#include "math/bigfix/kremlin/internal/types.h" #include "math/bigfix/kremlin/internal/types.h"
#include "math/bigfix/kremlin/internal/target.h" #include "math/bigfix/kremlin/internal/target.h"
#include "math/bigfix/FStar_UInt128.h" #include "math/bigfix/kremlib/FStar_UInt128.h"
static inline void store128_le(uint8_t *x0, FStar_UInt128_uint128 x1); static inline void store128_le(uint8_t *x0, FStar_UInt128_uint128 x1);

14
src/math/interval/mod_interval.h
View file

@ -42,11 +42,11 @@ template<typename Numeral>
class mod_interval { class mod_interval {
bool emp { false }; bool emp { false };
public: public:
virtual ~mod_interval() {}
Numeral lo { 0 }; Numeral lo { 0 };
Numeral hi { 0 }; Numeral hi { 0 };
mod_interval() {} mod_interval() {}
mod_interval(Numeral const& l, Numeral const& h): lo(l), hi(h) {} mod_interval(Numeral const& l, Numeral const& h): lo(l), hi(h) {}
virtual ~mod_interval() {}
static mod_interval free() { return mod_interval(0, 0); } static mod_interval free() { return mod_interval(0, 0); }
static mod_interval empty() { mod_interval i(0, 0); i.emp = true; return i; } static mod_interval empty() { mod_interval i(0, 0); i.emp = true; return i; }
@ -60,12 +60,12 @@ public:
void set_bounds(Numeral const& l, Numeral const& h) { lo = l; hi = h; } void set_bounds(Numeral const& l, Numeral const& h) { lo = l; hi = h; }
void set_empty() { emp = true; } void set_empty() { emp = true; }
void intersect_ule(Numeral const& h); mod_interval& intersect_ule(Numeral const& h);
void intersect_uge(Numeral const& l); mod_interval& intersect_uge(Numeral const& l);
void intersect_ult(Numeral const& h); mod_interval& intersect_ult(Numeral const& h);
void intersect_ugt(Numeral const& l); mod_interval& intersect_ugt(Numeral const& l);
void intersect_fixed(Numeral const& n); mod_interval& intersect_fixed(Numeral const& n);
void intersect_diff(Numeral const& n); mod_interval& intersect_diff(Numeral const& n);
mod_interval operator&(mod_interval const& other) const; mod_interval operator&(mod_interval const& other) const;
mod_interval operator+(mod_interval const& other) const; mod_interval operator+(mod_interval const& other) const;

32
src/math/interval/mod_interval_def.h
View file

@ -124,35 +124,37 @@ Numeral mod_interval<Numeral>::closest_value(Numeral const& n) const {
// TBD: correctness and completeness for wrap-around semantics needs to be checked/fixed // TBD: correctness and completeness for wrap-around semantics needs to be checked/fixed
template<typename Numeral> template<typename Numeral>
void mod_interval<Numeral>::intersect_ule(Numeral const& h) { mod_interval<Numeral>& mod_interval<Numeral>::intersect_ule(Numeral const& h) {
if (is_empty()) if (is_empty())
return; return *this;
if (is_max(h)) if (is_max(h))
return; return *this;
else if (is_free()) else if (is_free())
lo = 0, hi = h + 1; lo = 0, hi = h + 1;
else if (hi > lo && lo > h) else if (hi > lo && lo > h)
set_empty(); set_empty();
else if (hi != 0 || h + 1 < hi) else if (hi != 0 || h + 1 < hi)
hi = h + 1; hi = h + 1;
return *this;
} }
template<typename Numeral> template<typename Numeral>
void mod_interval<Numeral>::intersect_uge(Numeral const& l) { mod_interval<Numeral>& mod_interval<Numeral>::intersect_uge(Numeral const& l) {
if (is_empty()) if (is_empty())
return; return *this;
if (lo < hi && hi <= l) if (lo < hi && hi <= l)
set_empty(); set_empty();
else if (is_free()) else if (is_free())
lo = l, hi = 0; lo = l, hi = 0;
else if (lo < hi && lo < l) else if (lo < hi && lo < l)
lo = l; lo = l;
return *this;
} }
template<typename Numeral> template<typename Numeral>
void mod_interval<Numeral>::intersect_ult(Numeral const& h) { mod_interval<Numeral>& mod_interval<Numeral>::intersect_ult(Numeral const& h) {
if (is_empty()) if (is_empty())
return; return *this;
if (h == 0) if (h == 0)
set_empty(); set_empty();
else if (is_free()) else if (is_free())
@ -161,12 +163,13 @@ void mod_interval<Numeral>::intersect_ult(Numeral const& h) {
set_empty(); set_empty();
else if (hi > lo && h < hi) else if (hi > lo && h < hi)
hi = h; hi = h;
return *this;
} }
template<typename Numeral> template<typename Numeral>
void mod_interval<Numeral>::intersect_ugt(Numeral const& l) { mod_interval<Numeral>& mod_interval<Numeral>::intersect_ugt(Numeral const& l) {
if (is_empty()) if (is_empty())
return; return *this;
if (is_max(l)) if (is_max(l))
set_empty(); set_empty();
else if (is_free()) else if (is_free())
@ -177,24 +180,26 @@ void mod_interval<Numeral>::intersect_ugt(Numeral const& l) {
set_empty(); set_empty();
else if (lo < hi) else if (lo < hi)
lo = l + 1; lo = l + 1;
return *this;
} }
template<typename Numeral> template<typename Numeral>
void mod_interval<Numeral>::intersect_fixed(Numeral const& a) { mod_interval<Numeral>& mod_interval<Numeral>::intersect_fixed(Numeral const& a) {
if (is_empty()) if (is_empty())
return; return *this;
if (!contains(a)) if (!contains(a))
set_empty(); set_empty();
else if (is_max(a)) else if (is_max(a))
lo = a, hi = 0; lo = a, hi = 0;
else else
lo = a, hi = a + 1; lo = a, hi = a + 1;
return *this;
} }
template<typename Numeral> template<typename Numeral>
void mod_interval<Numeral>::intersect_diff(Numeral const& a) { mod_interval<Numeral>& mod_interval<Numeral>::intersect_diff(Numeral const& a) {
if (!contains(a) || is_empty()) if (!contains(a) || is_empty())
return; return *this;
if (a == lo && a + 1 == hi) if (a == lo && a + 1 == hi)
set_empty(); set_empty();
else if (a == lo && hi == 0 && is_max(a)) else if (a == lo && hi == 0 && is_max(a))
@ -205,4 +210,5 @@ void mod_interval<Numeral>::intersect_diff(Numeral const& a) {
hi = a; hi = a;
else if (hi == 0 && is_max(a)) else if (hi == 0 && is_max(a))
hi = a; hi = a;
return *this;
} }

8
src/test/mod_interval.cpp
View file

@ -11,6 +11,14 @@ static void test_interval1() {
std::cout << "-" << i2 << " := " << (-i2) << "\n"; std::cout << "-" << i2 << " := " << (-i2) << "\n";
} }
static void test_interval2() {
mod_interval<uint32_t> i;
std::cout << " >= 0: " << i.intersect_uge(0) << "\n";
std::cout << " >= 1: " << i.intersect_uge(1) << "\n";
}
void tst_mod_interval() { void tst_mod_interval() {
test_interval1(); test_interval1();
test_interval2();
} }