cprover
Loading...
Searching...
No Matches
simplify_expr_with_value_set.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Variant of simplify_exprt that uses a value_sett
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
9#ifndef CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H
10#define CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H
11
13
14class value_sett;
15
17{
18public:
20 const value_sett &_vs,
21 const irep_idt &_mode,
22 const namespacet &_ns)
23 : simplify_exprt(_ns), value_set(_vs), language_mode(_mode)
24 {
25 }
26
27 [[nodiscard]] resultt<>
31 [[nodiscard]] resultt<>
33 [[nodiscard]] resultt<>
35
36protected:
39};
40
41#endif // CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The offset (in bytes) of a pointer relative to the object.
resultt simplify_pointer_offset(const pointer_offset_exprt &) override
simplify_expr_with_value_sett(const value_sett &_vs, const irep_idt &_mode, const namespacet &_ns)
resultt simplify_inequality(const binary_relation_exprt &) override
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_inequality_pointer_object(const binary_relation_exprt &) override
When all candidates in the value set have the same offset we can replace a pointer_offset expression ...
simplify_exprt(const namespacet &_ns)
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition value_set.h:43
resultt
The result of goto verifying.
Definition properties.h:45
dstringt irep_idt