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