cprover
Loading...
Searching...
No Matches
struct_encoding.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
5
6#include <util/expr.h> // For passing exprt by value. // IWYU pragma: keep
7#include <util/type.h> // For passing `typet` by value. // IWYU pragma: keep
8
9#include <memory>
10
11class namespacet;
12class boolbv_widtht;
13class member_exprt;
15
18{
19public:
20 explicit struct_encodingt(const namespacet &ns);
23
24 typet encode(typet type) const;
25 exprt encode(exprt expr) const;
28 exprt
30
31private:
32 std::unique_ptr<boolbv_widtht> boolbv_width;
33 std::reference_wrapper<const namespacet> ns;
34
36};
37
38#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Base class for all expressions.
Definition expr.h:56
Extract member of struct or union.
Definition std_expr.h:2794
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Encodes struct types/values into non-struct expressions/types.
std::unique_ptr< boolbv_widtht > boolbv_width
std::reference_wrapper< const namespacet > ns
typet encode(typet type) const
exprt decode(const exprt &encoded, const struct_tag_typet &original_type) const
Reconstructs a struct expression of the original_type using the data from the bit vector encoded expr...
exprt encode_member(const member_exprt &member_expr) const
The member expression selects the value of a field from a struct or union.
struct_encodingt(const namespacet &ns)
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
The type of an expression, extends irept.
Definition type.h:29
Defines typet, type_with_subtypet and type_with_subtypest.