cvc4-1.4
subrange_bound.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__SUBRANGE_BOUND_H
21 #define __CVC4__SUBRANGE_BOUND_H
22 
23 #include "util/integer.h"
24 #include "util/exception.h"
25 
26 #include <limits>
27 
28 namespace CVC4 {
29 
37  bool d_nobound;
38  Integer d_bound;
39 
40 public:
41 
43  SubrangeBound() throw() :
44  d_nobound(true),
45  d_bound() {
46  }
47 
49  SubrangeBound(const Integer& i) throw() :
50  d_nobound(false),
51  d_bound(i) {
52  }
53 
54  ~SubrangeBound() throw() {
55  }
56 
58  const Integer& getBound() const throw(IllegalArgumentException) {
59  CheckArgument(!d_nobound, this, "SubrangeBound is infinite");
60  return d_bound;
61  }
62 
64  bool hasBound() const throw() {
65  return !d_nobound;
66  }
67 
69  bool operator==(const SubrangeBound& b) const throw() {
70  return hasBound() == b.hasBound() &&
71  (!hasBound() || getBound() == b.getBound());
72  }
73 
75  bool operator!=(const SubrangeBound& b) const throw() {
76  return !(*this == b);
77  }
78 
87  bool operator<(const SubrangeBound& b) const throw() {
88  return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
89  ( hasBound() && b.hasBound() && getBound() < b.getBound() );
90  }
91 
100  bool operator<=(const SubrangeBound& b) const throw() {
101  return !hasBound() || !b.hasBound() ||
102  ( hasBound() && b.hasBound() && getBound() <= b.getBound() );
103  }
104 
113  bool operator>(const SubrangeBound& b) const throw() {
114  return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
115  ( hasBound() && b.hasBound() && getBound() < b.getBound() );
116  }
117 
126  bool operator>=(const SubrangeBound& b) const throw() {
127  return !hasBound() || !b.hasBound() ||
128  ( hasBound() && b.hasBound() && getBound() <= b.getBound() );
129  }
130 
131 
132  static SubrangeBound min(const SubrangeBound& a, const SubrangeBound& b){
133  if(a.hasBound() && b.hasBound()){
134  return SubrangeBound(Integer::min(a.getBound(), b.getBound()));
135  }else{
136  return SubrangeBound();
137  }
138  }
139 
140  static SubrangeBound max(const SubrangeBound& a, const SubrangeBound& b){
141  if(a.hasBound() && b.hasBound()){
142  return SubrangeBound(Integer::max(a.getBound(), b.getBound()));
143  }else{
144  return SubrangeBound();
145  }
146  }
147 
148 };/* class SubrangeBound */
149 
151 public:
152 
155 
157  lower(l),
158  upper(u) {
159  CheckArgument(!l.hasBound() || !u.hasBound() ||
160  l.getBound() <= u.getBound(),
161  l, "Bad subrange bounds specified");
162  }
163 
164  bool operator==(const SubrangeBounds& bounds) const {
165  return lower == bounds.lower && upper == bounds.upper;
166  }
167 
168  bool operator!=(const SubrangeBounds& bounds) const {
169  return !(*this == bounds);
170  }
171 
177  bool operator<(const SubrangeBounds& bounds) const {
178  return (lower > bounds.lower && upper <= bounds.upper) ||
179  (lower >= bounds.lower && upper < bounds.upper);
180  }
181 
187  bool operator<=(const SubrangeBounds& bounds) const {
188  return lower >= bounds.lower && upper <= bounds.upper;
189  }
190 
196  bool operator>(const SubrangeBounds& bounds) const {
197  return (lower < bounds.lower && upper >= bounds.upper) ||
198  (lower <= bounds.lower && upper > bounds.upper);
199  }
200 
206  bool operator>=(const SubrangeBounds& bounds) const {
207  return lower <= bounds.lower && upper >= bounds.upper;
208  }
209 
213  static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){
214  return (a.lower.hasBound() && b.lower.hasBound()) ||
215  (a.upper.hasBound() && b.upper.hasBound());
216  }
217 
222  static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b){
223  DebugCheckArgument(joinIsBounded(a,b), a);
224  SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower);
225  SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper);
226  return SubrangeBounds(newLower, newUpper);
227  }
228 
229 };/* class SubrangeBounds */
230 
232  inline size_t operator()(const SubrangeBounds& bounds) const {
233  // We use Integer::hash() rather than Integer::getUnsignedLong()
234  // because the latter might overflow and throw an exception
235  size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() : std::numeric_limits<size_t>::max();
236  size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits<size_t>::max();
237  return l + 0x9e3779b9 + (u << 6) + (u >> 2);
238  }
239 };/* struct SubrangeBoundsHashFunction */
240 
241 inline std::ostream&
242 operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC;
243 
244 inline std::ostream&
245 operator<<(std::ostream& out, const SubrangeBound& bound) throw() {
246  if(bound.hasBound()) {
247  out << bound.getBound();
248  } else {
249  out << '_';
250  }
251 
252  return out;
253 }
254 
255 inline std::ostream&
256 operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() CVC4_PUBLIC;
257 
258 inline std::ostream&
259 operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() {
260  out << bounds.lower << ".." << bounds.upper;
261 
262  return out;
263 }
264 
265 }/* CVC4 namespace */
266 
267 #endif /* __CVC4__SUBRANGE_BOUND_H */
void DebugCheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:155
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,...)
Definition: exception.h:140
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&#39;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...
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
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, TypeConstant typeConstant)
Definition: kind.h:568
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.