cprover
widened_range.h
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#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H
10#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H
11
12#include <util/arith_tools.h>
13#include <util/interval.h>
14#include <util/namespace.h>
15#include <util/symbol_table.h>
16
18{
19public:
21 const constant_interval_exprt &lhs,
22 const constant_interval_exprt &rhs)
24 constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower())),
26 constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper())),
28 constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower())),
30 constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper())),
34 from_integer(1, lhs.type()))),
37 {
38 }
39
40 const bool is_lower_widened;
41 const bool is_upper_widened;
44
45private:
48
49public:
52
53private:
56};
57
58#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Represents an interval of values.
Definition: interval.h:48
Base class for all expressions.
Definition: expr.h:54
Binary minus.
Definition: std_expr.h:973
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The symbol table.
Definition: symbol_table.h:14
widened_ranget(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: widened_range.h:20
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 widened_upper_bound
Definition: widened_range.h:51
const exprt lower_bound
Definition: widened_range.h:42
exprt widen_upper_bound() const
const exprt widened_lower_bound
Definition: widened_range.h:50
const bool is_lower_widened
Definition: widened_range.h:40
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition: string_expr.h:48
Author: Diffblue Ltd.