mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

r_interval::contains

Browse source
This commit is contained in:
Jakob Rath 2024-04-11 11:11:02 +02:00
parent 3f3b052933
commit 020a4d5d04
1 changed files with 22 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/sat/smt/polysat/interval.h
View file

@ -146,6 +146,27 @@ namespace polysat {
return contains(lo(), hi(), val); return contains(lo(), hi(), val);
} }
bool contains(r_interval const& other) const {
if (is_full())
return true;
if (other.is_full())
return false;
// lo <= lo' <= hi' <= hi
if (lo() <= other.lo() && other.lo() <= other.hi() && other.hi() <= hi())
return true;
if (lo() <= hi())
return false;
// hi < lo <= lo' <= hi'
if (lo() <= other.lo() && other.lo() <= other.hi())
return true;
// lo' <= hi' <= hi < lo
if (other.lo() <= other.hi() && other.hi() <= hi())
return true;
// hi' <= hi < lo <= lo'
if (other.hi() <= hi() && lo() <= other.lo())
return true;
return false;
}
}; };
inline std::ostream& operator<<(std::ostream& os, r_interval const& i) { inline std::ostream& operator<<(std::ostream& os, r_interval const& i) {
@ -206,7 +227,7 @@ namespace polysat {
return true; return true;
if (other.is_full()) if (other.is_full())
return false; return false;
// lo <= lo' <= hi' <= hi' // lo <= lo' <= hi' <= hi
if (lo_val() <= other.lo_val() && other.lo_val() <= other.hi_val() && other.hi_val() <= hi_val()) if (lo_val() <= other.lo_val() && other.lo_val() <= other.hi_val() && other.hi_val() <= hi_val())
return true; return true;
if (lo_val() <= hi_val()) if (lo_val() <= hi_val())