cprover
interval.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: intervals
4 
5  Author: Daniel Neville (2017)
6 
7 \*******************************************************************/
8 #ifndef CPROVER_UTIL_INTERVAL_H
9 #define CPROVER_UTIL_INTERVAL_H
10 
11 #include <util/arith_tools.h>
12 #include <util/expr.h>
13 #include <util/namespace.h>
14 #include <util/simplify_expr.h>
15 #include <util/std_expr.h>
16 #include <util/std_types.h>
17 #include <util/symbol_table.h>
18 #include <util/threeval.h>
19 
20 #include <iostream>
21 #include <ostream>
22 #include <sstream>
23 
25 class max_exprt : public exprt
26 {
27 public:
28  explicit max_exprt(const typet &_type) : exprt(ID_max, _type)
29  {
30  }
31 
32  explicit max_exprt(const exprt &_expr) : exprt(ID_max, _expr.type())
33  {
34  }
35 };
36 
38 class min_exprt : public exprt
39 {
40 public:
41  explicit min_exprt(const typet &_type) : exprt(ID_min, _type)
42  {
43  }
44 
45  explicit min_exprt(const exprt &_expr) : exprt(ID_min, _expr.type())
46  {
47  }
48 };
49 
56 {
57 public:
59  const exprt &lower,
60  const exprt &upper,
61  const typet type)
62  : binary_exprt(lower, ID_constant_interval, upper, type)
63  {
65  }
66 
69  {
70  }
71 
72  explicit constant_interval_exprt(const exprt &x)
73  : constant_interval_exprt(x, x, x.type())
74  {
75  }
76 
79  {
80  }
81 
82  constant_interval_exprt(const exprt &lower, const exprt &upper)
83  : constant_interval_exprt(lower, upper, lower.type())
84  {
85  }
86 
87  bool is_well_formed() const
88  {
89  bool b = true;
90 
91  const typet &type = this->type();
92  const exprt &lower = get_lower();
93  const exprt &upper = get_upper();
94 
95  b &= is_numeric() || type.id() == ID_bool || type.is_nil();
96 
97  b &= type == lower.type();
98  b &= type == upper.type();
99 
100  b &= is_valid_bound(lower);
101  b &= is_valid_bound(upper);
102 
103  b &= !is_numeric() || is_bottom() || less_than_or_equal(lower, upper);
104 
105  return b;
106  }
107 
108  bool is_valid_bound(const exprt &expr) const
109  {
110  const irep_idt &id = expr.id();
111 
112  bool b = true;
113 
114  b &= id == ID_constant || id == ID_min || id == ID_max;
115 
116  if(type().id() == ID_bool && id == ID_constant)
117  {
118  b &= expr == true_exprt() || expr == false_exprt();
119  }
120 
121  return b;
122  }
123 
124  static constant_interval_exprt tvt_to_interval(const tvt &val);
125 
126  /* Naming scheme
127  * is_[X]? Returns bool / tvt
128  * get_[X]? Returns relevant object
129  * [X] Generator of some object.
130  * generate_[X] generator used for evaluation
131  */
132 
133  /* Getters */
134  const exprt &get_lower() const;
135  const exprt &get_upper() const;
136 
141  const constant_interval_exprt &other,
142  const irep_idt &) const;
143 
144  constant_interval_exprt eval(const irep_idt &unary_operator) const;
146  eval(const irep_idt &binary_operator, const constant_interval_exprt &o) const;
147 
148  /* Unary arithmetic */
151 
153 
154  /* Logical */
155  tvt is_definitely_true() const;
156  tvt is_definitely_false() const;
157 
158  tvt logical_and(const constant_interval_exprt &o) const;
159  tvt logical_or(const constant_interval_exprt &o) const;
160  tvt logical_xor(const constant_interval_exprt &o) const;
161  tvt logical_not() const;
162 
163  /* Binary */
169 
170  /* Binary shifts */
173 
174  /* Unary bitwise */
176 
177  /* Binary bitwise */
181 
182  tvt less_than(const constant_interval_exprt &o) const;
183  tvt greater_than(const constant_interval_exprt &o) const;
186  tvt equal(const constant_interval_exprt &o) const;
187  tvt not_equal(const constant_interval_exprt &o) const;
188 
191 
192  bool is_empty() const;
193  bool is_single_value_interval() const;
196  // tvt contains(constant_interval_exprt &o) const;
197 
198  /* SET OF EXPR COMPARATORS */
199  static bool equal(const exprt &a, const exprt &b);
200  static bool not_equal(const exprt &a, const exprt &b);
201  static bool less_than(const exprt &a, const exprt &b);
202  static bool less_than_or_equal(const exprt &a, const exprt &b);
203  static bool greater_than(const exprt &a, const exprt &b);
204  static bool greater_than_or_equal(const exprt &a, const exprt &b);
205  /* END SET OF EXPR COMPS */
206 
207  /* INTERVAL COMPARISONS, returns tvt.is_true(). False cannot be trusted
208  * (could be false or unknown, either use less_than, etc method or use the correct
209  * operator)! */
210  friend bool operator<(
213  friend bool operator>(
216  friend bool operator<=(
219  friend bool operator>=(
222  friend bool operator==(
225  friend bool operator!=(
228 
229  /* Operator override for intervals */
230  friend const constant_interval_exprt operator+(
233  friend const constant_interval_exprt operator-(
236  friend const constant_interval_exprt operator/(
239  friend const constant_interval_exprt operator*(
242  friend const constant_interval_exprt operator%(
245  friend const constant_interval_exprt operator!(
247  friend const constant_interval_exprt operator&(
250  friend const constant_interval_exprt operator|(
253  friend const constant_interval_exprt operator^(
256  friend const constant_interval_exprt operator<<(
259  friend const constant_interval_exprt operator>>(
262 
263  friend std::ostream &
264  operator<<(std::ostream &out, const constant_interval_exprt &i);
265  std::string to_string() const;
266 
267  /* Now static equivalents! */
268  static tvt is_true(const constant_interval_exprt &a);
269  static tvt is_false(const constant_interval_exprt &a);
270 
271  static tvt logical_and(
272  const constant_interval_exprt &a,
273  const constant_interval_exprt &b);
274  static tvt logical_or(
275  const constant_interval_exprt &a,
276  const constant_interval_exprt &b);
277  static tvt logical_xor(
278  const constant_interval_exprt &a,
279  const constant_interval_exprt &b);
280  static tvt logical_not(const constant_interval_exprt &a);
281 
284 
285  /* Binary */
296 
297  /* Binary shifts */
299  const constant_interval_exprt &a,
300  const constant_interval_exprt &b);
302  const constant_interval_exprt &a,
303  const constant_interval_exprt &b);
304 
305  /* Unary bitwise */
307 
308  /* Binary bitwise */
310  const constant_interval_exprt &a,
311  const constant_interval_exprt &b);
313  const constant_interval_exprt &a,
314  const constant_interval_exprt &b);
316  const constant_interval_exprt &a,
317  const constant_interval_exprt &b);
318 
319  static tvt
321  static tvt greater_than(
322  const constant_interval_exprt &a,
323  const constant_interval_exprt &b);
324  static tvt less_than_or_equal(
325  const constant_interval_exprt &a,
326  const constant_interval_exprt &b);
327  static tvt greater_than_or_equal(
328  const constant_interval_exprt &a,
329  const constant_interval_exprt &b);
330  static tvt
332  static tvt
334 
337 
338  static bool is_empty(const constant_interval_exprt &a);
340 
341  static bool is_top(const constant_interval_exprt &a);
342  static bool is_bottom(const constant_interval_exprt &a);
343 
344  static bool is_min(const constant_interval_exprt &a);
345  static bool is_max(const constant_interval_exprt &a);
346  /* End static equivalents */
347 
348  bool is_top() const;
349  bool is_bottom() const;
350  static constant_interval_exprt top(const typet &type);
351  static constant_interval_exprt bottom(const typet &type);
354 
355  bool has_no_lower_bound() const;
356  bool has_no_upper_bound() const;
357  static bool is_min(const exprt &expr);
358  static bool is_max(const exprt &expr);
359 
360  /* Generate min and max exprt according to current type */
361  min_exprt min() const;
362  max_exprt max() const;
363 
364  constant_exprt zero() const;
365  static constant_exprt zero(const typet &type);
366  static constant_exprt zero(const exprt &expr);
367  static constant_exprt zero(const constant_interval_exprt &interval);
368 
369  /* Private? */
373  const irep_idt &operation);
374  static exprt get_extreme(std::vector<exprt> values, bool min = true);
375  static exprt get_max(const exprt &a, const exprt &b);
376  static exprt get_min(const exprt &a, const exprt &b);
377  static exprt get_min(std::vector<exprt> &values);
378  static exprt get_max(std::vector<exprt> &values);
379 
380  /* we don't simplify in the constructor otherwise */
382  static exprt simplified_expr(exprt expr);
383 
384  /* Helpers */
385  /* Four common params: self, static: type, expr, interval */
386 
387  bool is_numeric() const;
388  static bool is_numeric(const typet &type);
389  static bool is_numeric(const exprt &expr);
390  static bool is_numeric(const constant_interval_exprt &interval);
391 
392  bool is_int() const;
393  static bool is_int(const typet &type);
394  static bool is_int(const exprt &expr);
395  static bool is_int(const constant_interval_exprt &interval);
396 
397  bool is_float() const;
398  static bool is_float(const typet &type);
399  static bool is_float(const exprt &expr);
400  static bool is_float(const constant_interval_exprt &interval);
401 
402  bool is_bitvector() const;
403  static bool is_bitvector(const typet &type);
404  static bool is_bitvector(const constant_interval_exprt &interval);
405  static bool is_bitvector(const exprt &expr);
406 
407  bool is_signed() const;
408  static bool is_signed(const typet &type);
409  static bool is_signed(const exprt &expr);
410  static bool is_signed(const constant_interval_exprt &interval);
411 
412  bool is_unsigned() const;
413  static bool is_unsigned(const typet &type);
414  static bool is_unsigned(const exprt &expr);
415  static bool is_unsigned(const constant_interval_exprt &interval);
416 
417  bool contains_zero() const;
418  bool contains(const constant_interval_exprt &interval) const;
419 
420  static bool is_extreme(const exprt &expr);
421  static bool is_extreme(const exprt &expr1, const exprt &expr2);
422 
423  static bool contains_extreme(const exprt expr);
424  static bool contains_extreme(const exprt expr1, const exprt expr2);
425 
426  bool is_positive() const;
427  static bool is_positive(const exprt &expr);
428  static bool is_positive(const constant_interval_exprt &interval);
429 
430  bool is_zero() const;
431  static bool is_zero(const exprt &expr);
432  static bool is_zero(const constant_interval_exprt &interval);
433 
434  bool is_negative() const;
435  static bool is_negative(const exprt &expr);
436  static bool is_negative(const constant_interval_exprt &interval);
437 
438  static exprt abs(const exprt &expr);
439 
440 private:
441  static void generate_expression(
442  const exprt &lhs,
443  const exprt &rhs,
444  const irep_idt &operation,
445  std::vector<exprt> &collection);
446  static void append_multiply_expression(
447  const exprt &lower,
448  const exprt &upper,
449  std::vector<exprt> &collection);
450  static void append_multiply_expression_max(
451  const exprt &expr,
452  std::vector<exprt> &collection);
453  static void append_multiply_expression_min(
454  const exprt &min,
455  const exprt &other,
456  std::vector<exprt> &collection);
457  static exprt generate_division_expression(const exprt &lhs, const exprt &rhs);
458  static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs);
460  const exprt &lhs,
461  const exprt &rhs,
462  const irep_idt &operation);
463 };
464 
465 inline const constant_interval_exprt &
467 {
468  PRECONDITION(expr.id() == ID_constant_interval);
469  return static_cast<const constant_interval_exprt &>(expr);
470 }
471 
472 #endif /* SRC_ANALYSES_INTERVAL_H_ */
constant_interval_exprt::is_definitely_true
tvt is_definitely_true() const
Definition: interval.cpp:215
constant_interval_exprt::is_signed
bool is_signed() const
Definition: interval.cpp:1174
constant_interval_exprt::max
max_exprt max() const
Definition: interval.cpp:1023
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
constant_interval_exprt::is_unsigned
bool is_unsigned() const
Definition: interval.cpp:1179
constant_interval_exprt::constant_interval_exprt
constant_interval_exprt(const exprt &lower, const exprt &upper)
Definition: interval.h:82
constant_interval_exprt::get_extremes
static constant_interval_exprt get_extremes(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs, const irep_idt &operation)
Definition: interval.cpp:467
constant_interval_exprt::unary_plus
constant_interval_exprt unary_plus() const
Definition: interval.cpp:36
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:641
max_exprt::max_exprt
max_exprt(const typet &_type)
Definition: interval.h:28
constant_interval_exprt::operator<
friend bool operator<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1490
constant_interval_exprt::right_shift
constant_interval_exprt right_shift(const constant_interval_exprt &o) const
Definition: interval.cpp:316
arith_tools.h
constant_interval_exprt::generate_shift_expression
static exprt generate_shift_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation)
Definition: interval.cpp:895
constant_interval_exprt::operator>>
friend const constant_interval_exprt operator>>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1600
constant_interval_exprt::decrement
constant_interval_exprt decrement() const
Definition: interval.cpp:462
constant_interval_exprt::constant_interval_exprt
constant_interval_exprt(const constant_interval_exprt &x)
Definition: interval.h:67
min_exprt::min_exprt
min_exprt(const exprt &_expr)
Definition: interval.h:45
typet
The type of an expression, extends irept.
Definition: type.h:29
constant_interval_exprt::simplified_expr
static exprt simplified_expr(exprt expr)
Definition: interval.cpp:983
threeval.h
constant_interval_exprt::get_max
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:956
constant_interval_exprt::is_valid_bound
bool is_valid_bound(const exprt &expr) const
Definition: interval.h:108
max_exprt
+∞ upper bound for intervals
Definition: interval.h:26
constant_interval_exprt::contains
bool contains(const constant_interval_exprt &interval) const
Definition: interval.cpp:1420
constant_interval_exprt::operator^
friend const constant_interval_exprt operator^(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1581
constant_interval_exprt::append_multiply_expression_max
static void append_multiply_expression_max(const exprt &expr, std::vector< exprt > &collection)
Appends interval bounds that could arise from MAX * expr.
Definition: interval.cpp:635
constant_interval_exprt::is_float
bool is_float() const
Definition: interval.cpp:1066
exprt
Base class for all expressions.
Definition: expr.h:53
constant_interval_exprt::is_extreme
static bool is_extreme(const exprt &expr)
Definition: interval.cpp:1189
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:631
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
constant_interval_exprt::is_well_formed
bool is_well_formed() const
Definition: interval.h:87
constant_interval_exprt::operator<=
friend bool operator<=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1504
constant_interval_exprt::generate_division_expression
static exprt generate_division_expression(const exprt &lhs, const exprt &rhs)
Definition: interval.cpp:680
min_exprt
-∞ upper bound for intervals
Definition: interval.h:39
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
namespace.h
constant_interval_exprt::is_bitvector
bool is_bitvector() const
Definition: interval.cpp:1184
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
constant_interval_exprt::zero
constant_exprt zero() const
Definition: interval.cpp:1013
constant_interval_exprt::greater_than
tvt greater_than(const constant_interval_exprt &o) const
Definition: interval.cpp:395
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
constant_interval_exprt::operator>
friend bool operator>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1497
constant_interval_exprt::logical_not
tvt logical_not() const
Definition: interval.cpp:281
constant_interval_exprt::is_int
bool is_int() const
Definition: interval.cpp:1061
expr.h
max_exprt::max_exprt
max_exprt(const exprt &_expr)
Definition: interval.h:32
constant_interval_exprt::not_equal
tvt not_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:452
constant_interval_exprt::handle_constant_binary_expression
constant_interval_exprt handle_constant_binary_expression(const constant_interval_exprt &other, const irep_idt &) const
Definition: interval.cpp:947
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
constant_interval_exprt::bitwise_xor
constant_interval_exprt bitwise_xor(const constant_interval_exprt &o) const
Definition: interval.cpp:332
constant_interval_exprt::bitwise_not
constant_interval_exprt bitwise_not() const
Definition: interval.cpp:364
constant_interval_exprt::contains_extreme
static bool contains_extreme(const exprt expr)
Definition: interval.cpp:1823
constant_interval_exprt::multiply
constant_interval_exprt multiply(const constant_interval_exprt &o) const
Definition: interval.cpp:123
constant_interval_exprt::is_max
static bool is_max(const constant_interval_exprt &a)
Definition: interval.cpp:1818
constant_interval_exprt::left_shift
constant_interval_exprt left_shift(const constant_interval_exprt &o) const
Definition: interval.cpp:299
constant_interval_exprt::is_zero
bool is_zero() const
Definition: interval.cpp:1913
constant_interval_exprt::is_single_value_interval
bool is_single_value_interval() const
Definition: interval.cpp:1858
min_exprt::min_exprt
min_exprt(const typet &_type)
Definition: interval.h:41
constant_interval_exprt::operator!
friend const constant_interval_exprt operator!(const constant_interval_exprt &lhs)
Definition: interval.cpp:1588
constant_interval_exprt::is_top
bool is_top() const
Definition: interval.cpp:1028
constant_interval_exprt::operator-
friend const constant_interval_exprt operator-(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1539
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
constant_interval_exprt::append_multiply_expression_min
static void append_multiply_expression_min(const exprt &min, const exprt &other, std::vector< exprt > &collection)
Appends interval bounds that could arise from MIN * other.
Definition: interval.cpp:660
constant_interval_exprt::eval
constant_interval_exprt eval(const irep_idt &unary_operator) const
Definition: interval.cpp:789
constant_interval_exprt::generate_modulo_expression
static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs)
Definition: interval.cpp:735
constant_interval_exprt::plus
constant_interval_exprt plus(const constant_interval_exprt &o) const
Definition: interval.cpp:73
std_types.h
Pre-defined types.
constant_interval_exprt::bottom
constant_interval_exprt bottom() const
Definition: interval.cpp:1054
constant_interval_exprt::bitwise_and
constant_interval_exprt bitwise_and(const constant_interval_exprt &o) const
Definition: interval.cpp:354
constant_interval_exprt::increment
constant_interval_exprt increment() const
Definition: interval.cpp:457
constant_interval_exprt::modulo
constant_interval_exprt modulo(const constant_interval_exprt &o) const
Definition: interval.cpp:151
constant_interval_exprt::less_than
tvt less_than(const constant_interval_exprt &o) const
Definition: interval.cpp:374
constant_interval_exprt::logical_or
tvt logical_or(const constant_interval_exprt &o) const
Definition: interval.cpp:252
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
constant_interval_exprt::operator|
friend const constant_interval_exprt operator|(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1574
constant_interval_exprt::operator<<
friend const constant_interval_exprt operator<<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1593
constant_interval_exprt::is_negative
bool is_negative() const
Definition: interval.cpp:1918
tvt
Definition: threeval.h:20
constant_interval_exprt::minus
constant_interval_exprt minus(const constant_interval_exprt &other) const
Definition: interval.cpp:111
constant_interval_exprt::is_numeric
bool is_numeric() const
Definition: interval.cpp:1076
simplify_expr.h
constant_interval_exprt::has_no_upper_bound
bool has_no_upper_bound() const
Definition: interval.cpp:1199
constant_interval_exprt::is_empty
bool is_empty() const
Definition: interval.cpp:1848
constant_interval_exprt::is_bottom
bool is_bottom() const
Definition: interval.cpp:1033
constant_interval_exprt::constant_interval_exprt
constant_interval_exprt(const exprt &lower, const exprt &upper, const typet type)
Definition: interval.h:58
constant_interval_exprt::get_extreme
static exprt get_extreme(std::vector< exprt > values, bool min=true)
Definition: interval.cpp:493
constant_interval_exprt::has_no_lower_bound
bool has_no_lower_bound() const
Definition: interval.cpp:1204
constant_interval_exprt::contains_zero
bool contains_zero() const
Definition: interval.cpp:1864
constant_interval_exprt::typecast
constant_interval_exprt typecast(const typet &type) const
Definition: interval.cpp:1620
constant_interval_exprt::operator&
friend const constant_interval_exprt operator&(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1567
to_constant_interval_expr
const constant_interval_exprt & to_constant_interval_expr(const exprt &expr)
Definition: interval.h:466
constant_interval_exprt::operator*
friend const constant_interval_exprt operator*(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1553
constant_interval_exprt::tvt_to_interval
static constant_interval_exprt tvt_to_interval(const tvt &val)
Definition: interval.cpp:1959
constant_interval_exprt::less_than_or_equal
tvt less_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:401
constant_interval_exprt::get_lower
const exprt & get_lower() const
Definition: interval.cpp:26
constant_interval_exprt::is_min
static bool is_min(const constant_interval_exprt &a)
Definition: interval.cpp:1813
constant_interval_exprt::abs
static exprt abs(const exprt &expr)
Definition: interval.cpp:1293
constant_interval_exprt::is_definitely_false
tvt is_definitely_false() const
Definition: interval.cpp:221
constant_interval_exprt::get_upper
const exprt & get_upper() const
Definition: interval.cpp:31
constant_interval_exprt::get_min
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:961
constant_interval_exprt::is_positive
bool is_positive() const
Definition: interval.cpp:1908
r
static int8_t r
Definition: irep_hash.h:59
constant_interval_exprt::top
constant_interval_exprt top() const
Definition: interval.cpp:1049
constant_interval_exprt::constant_interval_exprt
constant_interval_exprt(const typet &type)
Definition: interval.h:77
constant_interval_exprt::operator%
friend const constant_interval_exprt operator%(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1560
symbol_table.h
Author: Diffblue Ltd.
constant_interval_exprt::greater_than_or_equal
tvt greater_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:423
constant_interval_exprt::append_multiply_expression
static void append_multiply_expression(const exprt &lower, const exprt &upper, std::vector< exprt > &collection)
Adds all possible values that may arise from multiplication (more than one, in case of past the type ...
Definition: interval.cpp:597
constant_interval_exprt::min
min_exprt min() const
Definition: interval.cpp:1018
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
constant_interval_exprt::constant_interval_exprt
constant_interval_exprt(const exprt &x)
Definition: interval.h:72
constant_interval_exprt::generate_expression
static void generate_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation, std::vector< exprt > &collection)
Definition: interval.cpp:568
constant_interval_exprt::divide
constant_interval_exprt divide(const constant_interval_exprt &o) const
Definition: interval.cpp:134
constant_interval_exprt::operator>=
friend bool operator>=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1511
constant_interval_exprt::simplified_interval
static constant_interval_exprt simplified_interval(exprt &l, exprt &r)
Definition: interval.cpp:978
std_expr.h
API to expression classes.
constant_interval_exprt::logical_and
tvt logical_and(const constant_interval_exprt &o) const
Definition: interval.cpp:263
constant_interval_exprt::handle_constant_unary_expression
constant_interval_exprt handle_constant_unary_expression(const irep_idt &op) const
SET OF ARITHMETIC OPERATORS.
Definition: interval.cpp:935
constant_interval_exprt::operator==
friend bool operator==(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1518
constant_interval_exprt::operator/
friend const constant_interval_exprt operator/(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1546
constant_interval_exprt::unary_minus
constant_interval_exprt unary_minus() const
Definition: interval.cpp:41
constant_interval_exprt::logical_xor
tvt logical_xor(const constant_interval_exprt &o) const
Definition: interval.cpp:271
constant_interval_exprt::to_string
std::string to_string() const
Definition: interval.cpp:1429
constant_interval_exprt::bitwise_or
constant_interval_exprt bitwise_or(const constant_interval_exprt &o) const
Definition: interval.cpp:343
constant_interval_exprt::operator!=
friend bool operator!=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1525
constant_interval_exprt::operator+
friend const constant_interval_exprt operator+(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1532
constant_interval_exprt::equal
tvt equal(const constant_interval_exprt &o) const
Definition: interval.cpp:429