cprover
Loading...
Searching...
No Matches
widened_range.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: helper for extending intervals during widening merges
4
5 Author: Jez Higgins
6
7\*******************************************************************/
8
9#include "widened_range.h"
10#include <util/simplify_expr.h>
11
12static bool has_underflowed(const exprt &value)
13{
15 value, from_integer(0, value.type()));
16}
17static bool has_overflowed(const exprt &value, const exprt &initial_value)
18{
19 return constant_interval_exprt::less_than(value, initial_value);
20}
21
23{
25 return lower_bound;
26
27 auto new_lower_bound = simplify_expr(minus_exprt(lower_bound, range_), ns_);
28
29 if(
31 has_underflowed(new_lower_bound))
32 return min_value_exprt(lower_bound.type());
33
34 return new_lower_bound;
35}
36
38{
40 return upper_bound;
41
42 auto new_upper_bound = simplify_expr(plus_exprt(upper_bound, range_), ns_);
43
44 if(
46 has_overflowed(new_upper_bound, upper_bound))
47 return max_value_exprt(upper_bound.type());
48
49 return new_upper_bound;
50}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
tvt greater_than(const constant_interval_exprt &o) const
Definition interval.cpp:397
static bool contains_extreme(const exprt expr)
tvt less_than(const constant_interval_exprt &o) const
Definition interval.cpp:376
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
+∞ upper bound for intervals
Definition interval.h:18
-∞ upper bound for intervals
Definition interval.h:33
Binary minus.
Definition std_expr.h:1061
The plus expression Associativity is not specified.
Definition std_expr.h:1002
const exprt upper_bound
exprt widen_lower_bound() const
const bool is_upper_widened
namespacet ns_
const exprt lower_bound
exprt widen_upper_bound() const
const bool is_lower_widened
exprt simplify_expr(exprt src, const namespacet &ns)
static bool has_overflowed(const exprt &value, const exprt &initial_value)
static bool has_underflowed(const exprt &value)