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);
bool operator>(const SubrangeBounds &bounds) const
Is this pair of SubrangeBounds "greater than" (does it contain) the given pair of SubrangeBounds...
void DebugCheckArgument(bool cond, const T &arg, const char *fmt,...)
bool hasBound() const
Returns true iff this is a finite SubrangeBound.
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
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 &, const Command &)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
bool operator!=(const SubrangeBound &b) const
Test two SubrangeBounds for disequality.
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 "greater than or equal to" another? For two SubrangeBounds that "have bounds...
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.
SubrangeBound(const Integer &i)
Construct a finite SubrangeBound.
bool operator>=(const SubrangeBounds &bounds) const
Is this pair of SubrangeBounds "greater than" (does it contain) the given pair of SubrangeBounds...
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool operator<=(const SubrangeBounds &bounds) const
Is this pair of SubrangeBounds "less than or equal" (contained inside) the given pair of SubrangeBoun...
static const Integer & min(const Integer &a, const Integer &b)
Returns a reference to the minimum of two integers.
bool operator!=(const SubrangeBounds &bounds) const
static const Integer & max(const Integer &a, const Integer &b)
Returns a reference to the maximum of two integers.
bool operator>(const SubrangeBound &b) const
Is this SubrangeBound "greater than" another? For two SubrangeBounds that "have bounds," this is defined as expected.
SubrangeBounds(const SubrangeBound &l, const SubrangeBound &u)
struct CVC4::options::out__option_t out
SubrangeBound()
Construct an infinite SubrangeBound.
bool operator==(const SubrangeBounds &bounds) const
static SubrangeBound max(const SubrangeBound &a, const SubrangeBound &b)
bool operator<=(const SubrangeBound &b) const
Is this SubrangeBound "less than or equal to" another? For two SubrangeBounds that "have bounds...
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).
size_t operator()(const SubrangeBounds &bounds) const
const Integer & getBound() const
Get the finite SubrangeBound, failing an assertion if infinite.