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_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_exprt(upper_bound.type());
48
49 return new_upper_bound;
50}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
tvt greater_than(const constant_interval_exprt &o) const
Definition: interval.cpp:398
static bool contains_extreme(const exprt expr)
Definition: interval.cpp:1829
tvt less_than(const constant_interval_exprt &o) const
Definition: interval.cpp:377
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
+∞ upper bound for intervals
Definition: interval.h:18
-∞ upper bound for intervals
Definition: interval.h:31
Binary minus.
Definition: std_expr.h:973
The plus expression Associativity is not specified.
Definition: std_expr.h:914
const exprt upper_bound
Definition: widened_range.h:43
exprt widen_lower_bound() const
const bool is_upper_widened
Definition: widened_range.h:41
namespacet ns_
Definition: widened_range.h:46
const exprt lower_bound
Definition: widened_range.h:42
exprt widen_upper_bound() const
const bool is_lower_widened
Definition: widened_range.h:40
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)