20 #ifndef __CVC4__SUBRANGE_BOUND_H 21 #define __CVC4__SUBRANGE_BOUND_H 23 #include "util/integer.h" 70 return hasBound() == b.hasBound() &&
71 (!hasBound() || getBound() == b.getBound());
88 return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
89 ( hasBound() && b.hasBound() && getBound() < b.getBound() );
101 return !hasBound() || !b.hasBound() ||
102 ( hasBound() && b.hasBound() && getBound() <= b.getBound() );
114 return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
115 ( hasBound() && b.hasBound() && getBound() < b.getBound() );
127 return !hasBound() || !b.hasBound() ||
128 ( hasBound() && b.hasBound() && getBound() <= b.getBound() );
161 l,
"Bad subrange bounds specified");
165 return lower == bounds.
lower && upper == bounds.
upper;
169 return !(*
this == bounds);
178 return (lower > bounds.
lower && upper <= bounds.
upper) ||
179 (lower >= bounds.
lower && upper < bounds.
upper);
188 return lower >= bounds.
lower && upper <= bounds.
upper;
197 return (lower < bounds.lower && upper >= bounds.
upper) ||
198 (lower <= bounds.
lower && upper > bounds.
upper);
207 return lower <= bounds.
lower && upper >= bounds.
upper;
237 return l + 0x9e3779b9 + (u << 6) + (u >> 2);
void DebugCheckArgument(bool cond, const T &arg, const char *fmt,...)
size_t hash() const
Computes the hash of the node from the first word of the numerator, the denominator.
bool operator!=(const SubrangeBounds &bounds) const
bool operator==(const SubrangeBounds &bounds) const
bool operator!=(const SubrangeBound &b) const
Test two SubrangeBounds for disequality.
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
bool operator>=(const SubrangeBounds &bounds) const
Is this pair of SubrangeBounds "greater than" (does it contain) the given pair of SubrangeBounds...
static SubrangeBounds join(const SubrangeBounds &a, const SubrangeBounds &b)
Returns the join of two subranges, a and b.
CVC4's exception base class and some associated utilities.
bool operator<=(const SubrangeBound &b) const
Is this SubrangeBound "less than or equal to" another? For two SubrangeBounds that "have bounds...
const Integer & getBound() const
Get the finite SubrangeBound, failing an assertion if infinite.
size_t operator()(const SubrangeBounds &bounds) const
bool operator>(const SubrangeBounds &bounds) const
Is this pair of SubrangeBounds "greater than" (does it contain) the given pair of SubrangeBounds...
bool operator<=(const SubrangeBounds &bounds) const
Is this pair of SubrangeBounds "less than or equal" (contained inside) the given pair of SubrangeBoun...
SubrangeBound(const Integer &i)
Construct a finite SubrangeBound.
bool operator<(const SubrangeBounds &bounds) const
Is this pair of SubrangeBounds "less than" (contained inside) the given pair of SubrangeBounds? Think of this as a subtype relation, e.g., [0,2] < [0,3].
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
bool hasBound() const
Returns true iff this is a finite SubrangeBound.
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool operator>(const SubrangeBound &b) const
Is this SubrangeBound "greater than" another? For two SubrangeBounds that "have bounds," this is defined as expected.
bool operator>=(const SubrangeBound &b) const
Is this SubrangeBound "greater than or equal to" another? For two SubrangeBounds that "have bounds...
static const Integer & min(const Integer &a, const Integer &b)
Returns a reference to the minimum of two integers.
static const Integer & max(const Integer &a, const Integer &b)
Returns a reference to the maximum of two integers.
SubrangeBounds(const SubrangeBound &l, const SubrangeBound &u)
struct CVC4::options::out__option_t out
SubrangeBound()
Construct an infinite SubrangeBound.
static SubrangeBound max(const SubrangeBound &a, const SubrangeBound &b)
static SubrangeBound min(const SubrangeBound &a, const SubrangeBound &b)
Representation of a subrange bound.
static bool joinIsBounded(const SubrangeBounds &a, const SubrangeBounds &b)
Returns true if the join of two subranges is not (- infinity, + infinity).
bool operator==(const SubrangeBound &b) const
Test two SubrangeBounds for equality.
bool operator<(const SubrangeBound &b) const
Is this SubrangeBound "less than" another? For two SubrangeBounds that "have bounds," this is defined as expected.