cprover
interval_template.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_ANALYSES_INTERVAL_TEMPLATE_H
11 #define CPROVER_ANALYSES_INTERVAL_TEMPLATE_H
12 
13 #include <algorithm>
14 #include <iosfwd>
15 
16 #include <util/threeval.h>
17 
18 template<class T> class interval_templatet
19 {
20 public:
22  {
23  // this is 'top'
24  }
25 
26  explicit interval_templatet(const T &x):
27  lower_set(true),
28  upper_set(true),
29  lower(x),
30  upper(x)
31  {
32  }
33 
34  explicit interval_templatet(const T &l, const T &u):
35  lower_set(true),
36  upper_set(true),
37  lower(l),
38  upper(u)
39  {
40  }
41 
44 
45  const T &get_lower() const
46  {
47  return lower;
48  }
49 
50  const T &get_upper() const
51  {
52  return upper;
53  }
54 
55  bool empty() const
56  {
57  return upper_set && lower_set && lower>upper;
58  }
59 
60  bool is_bottom() const // equivalent to 'false'
61  {
62  return empty();
63  }
64 
65  bool is_top() const // equivalent to 'true'
66  {
67  return !lower_set && !upper_set;
68  }
69 
70  bool singleton() const
71  {
72  return upper_set && lower_set && lower==upper;
73  }
74 
75  // constraints
76  void make_le_than(const T &v) // add upper bound
77  {
78  if(upper_set)
79  {
80  if(upper>v)
81  upper=v;
82  }
83  else
84  {
85  upper_set=true;
86  upper=v;
87  }
88  }
89 
90  void make_ge_than(const T &v) // add lower bound
91  {
92  if(lower_set)
93  {
94  if(lower<v)
95  lower=v;
96  }
97  else
98  {
99  lower_set=true;
100  lower=v;
101  }
102  }
103 
104  // Union or disjunction
106  {
108  }
109 
110  // Intersection or conjunction
112  {
113  intersect_with(i);
114  }
115 
117  {
118  if(i.lower_set)
119  {
120  if(lower_set)
121  {
122  lower=std::max(lower, i.lower);
123  }
124  else
125  {
126  lower_set=true;
127  lower=i.lower;
128  }
129  }
130 
131  if(i.upper_set)
132  {
133  if(upper_set)
134  {
135  upper=std::min(upper, i.upper);
136  }
137  else
138  {
139  upper_set=true;
140  upper=i.upper;
141  }
142  }
143  }
144 
146  {
147  if(i.lower_set && lower_set)
148  lower=std::min(lower, i.lower);
149  else if(!i.lower_set && lower_set)
150  lower_set=false;
151 
152  if(i.upper_set && upper_set)
153  upper=std::max(upper, i.upper);
154  else if(!i.upper_set && upper_set)
155  upper_set=false;
156  }
157 };
158 
159 template<class T>
161 {
162  if(a.upper_set && b.lower_set && a.upper<=b.lower)
163  return tvt(true);
164  if(a.lower_set && b.upper_set && a.lower>b.upper)
165  return tvt(false);
166 
167  return tvt::unknown();
168 }
169 
170 template<class T>
172 {
173  return b<=a;
174 }
175 
176 template<class T>
178 {
179  return !(a>=b);
180 }
181 
182 template<class T>
184 {
185  return !(a<=b);
186 }
187 
188 template<class T>
190 {
191  if(a.lower_set!=b.lower_set)
192  return false;
193  if(a.upper_set!=b.upper_set)
194  return false;
195 
196  if(a.lower_set && a.lower!=b.lower)
197  return false;
198  if(a.upper_set && a.upper!=b.upper)
199  return false;
200 
201  return true;
202 }
203 
204 template<class T>
206 {
207  return !(a==b);
208 }
209 
210 template<class T>
212 {
214  i.upper_set=true;
215  i.upper=u;
216  return i;
217 }
218 
219 template<class T>
221 {
223  i.lower_set=true;
224  i.lower=l;
225  return i;
226 }
227 
228 template<class T>
229 std::ostream &operator << (std::ostream &out, const interval_templatet<T> &i)
230 {
231  if(i.lower_set)
232  out << '[' << i.lower;
233  else
234  out << ")-INF";
235 
236  out << ',';
237 
238  if(i.upper_set)
239  out << i.upper << ']';
240  else
241  out << "+INF(";
242 
243  return out;
244 }
245 
246 #endif // CPROVER_ANALYSES_INTERVAL_TEMPLATE_H
void intersect_with(const interval_templatet &i)
std::ostream & operator<<(std::ostream &out, const interval_templatet< T > &i)
void make_le_than(const T &v)
static tvt unknown()
Definition: threeval.h:33
bool operator!=(const interval_templatet< T > &a, const interval_templatet< T > &b)
void join(const interval_templatet< T > &i)
tvt operator>(const interval_templatet< T > &a, const interval_templatet< T > &b)
interval_templatet< T > upper_interval(const T &u)
const T & get_lower() const
tvt operator<=(const interval_templatet< T > &a, const interval_templatet< T > &b)
Definition: threeval.h:19
interval_templatet(const T &x)
void meet(const interval_templatet< T > &i)
bool is_bottom() const
interval_templatet(const T &l, const T &u)
bool operator==(const interval_templatet< T > &a, const interval_templatet< T > &b)
void make_ge_than(const T &v)
tvt operator>=(const interval_templatet< T > &a, const interval_templatet< T > &b)
void approx_union_with(const interval_templatet &i)
tvt operator<(const interval_templatet< T > &a, const interval_templatet< T > &b)
interval_templatet< T > lower_interval(const T &l)
const T & get_upper() const
bool singleton() const