#include <smt_tuple_node.h>
|
| | smt_tuple_node_flattener (smt_solver_baset *_ctx, const namespacet &_ns) |
| virtual | ~smt_tuple_node_flattener ()=default |
| smt_sortt | mk_struct_sort (const type2tc &type) override |
| | Create a sort representing a struct.
|
| smt_astt | tuple_create (const expr2tc &structdef) override |
| | Create a new tuple from a struct definition.
|
| smt_astt | tuple_fresh (smt_sortt s, std::string name="") override |
| | Create a fresh tuple, with freely valued fields.
|
| smt_astt | mk_tuple_symbol (const std::string &name, smt_sortt s) override |
| | Convert a symbol to a tuple_smt_ast.
|
| expr2tc | tuple_get (const expr2tc &expr) override |
| | Extract the assignment to a tuple-typed symbol from the SMT solvers model.
|
| expr2tc | tuple_get (const type2tc &type, smt_astt a) override |
| expr2tc | tuple_get_rec (tuple_node_smt_astt tuple) |
| expr2tc | tuple_get_array_elem (smt_astt array, uint64_t index, const type2tc &subtype) override |
| smt_astt | mk_tuple_array_symbol (const expr2tc &expr) override |
| | Like mk_tuple_symbol, but for arrays.
|
| smt_astt | tuple_array_of (const expr2tc &init_value, unsigned long domain_width) override |
| | Create a potentially /large/ array of tuples.
|
| smt_astt | tuple_array_create (const type2tc &array_type, smt_astt *input_args, bool const_array, smt_sortt domain) override |
| void | add_tuple_constraints_for_solving () override |
| void | push_tuple_ctx () override |
| void | pop_tuple_ctx () override |
| void | note_elements_populated (tuple_node_smt_ast *tuple) |
| | Record that tuple had its elements installed at the current context level, having itself been created at a shallower one — so pop_tuple_ctx must clear them before the ASTs they name are destroyed.
|
| virtual | ~tuple_iface ()=default |
◆ smt_tuple_node_flattener()
◆ ~smt_tuple_node_flattener()
| virtual smt_tuple_node_flattener::~smt_tuple_node_flattener |
( |
| ) |
|
|
virtualdefault |
◆ add_tuple_constraints_for_solving()
| void smt_tuple_node_flattener::add_tuple_constraints_for_solving |
( |
| ) |
|
|
overridevirtual |
◆ mk_struct_sort()
Create a sort representing a struct.
i.e., a tuple. Ideally this should actually be part of the overridden tuple api, but due to history it isn't yet. If solvers don't support tuples, implement this to abort.
- Parameters
-
| type | The struct type to create a tuple representation of. |
- Returns
- The tuple representation of the type, wrapped in an smt_sort.
Implements tuple_iface.
◆ mk_tuple_array_symbol()
| smt_astt smt_tuple_node_flattener::mk_tuple_array_symbol |
( |
const expr2tc & | expr | ) |
|
|
overridevirtual |
Like mk_tuple_symbol, but for arrays.
Implements tuple_iface.
◆ mk_tuple_symbol()
| smt_astt smt_tuple_node_flattener::mk_tuple_symbol |
( |
const std::string & | name, |
|
|
smt_sortt | s ) |
|
overridevirtual |
Convert a symbol to a tuple_smt_ast.
Implements tuple_iface.
◆ note_elements_populated()
Record that tuple had its elements installed at the current context level, having itself been created at a shallower one — so pop_tuple_ctx must clear them before the ASTs they name are destroyed.
Keying on the level the vector was installed at rather than the one its contents were allocated at is what makes the clear both safe and exact: installation never precedes allocation, pops descend, and the vector a tuple held before the install was empty.
◆ pop_tuple_ctx()
| void smt_tuple_node_flattener::pop_tuple_ctx |
( |
| ) |
|
|
overridevirtual |
◆ push_tuple_ctx()
| void smt_tuple_node_flattener::push_tuple_ctx |
( |
| ) |
|
|
overridevirtual |
◆ tuple_array_create()
◆ tuple_array_of()
| smt_astt smt_tuple_node_flattener::tuple_array_of |
( |
const expr2tc & | init_value, |
|
|
unsigned long | domain_width ) |
|
overridevirtual |
Create a potentially /large/ array of tuples.
This is called when we encounter an array_of operation, with a very large array size, of tuple sort.
- Parameters
-
| Expression | of tuple value to populate this array with. |
| domain_width | The size of array to create, in domain bits. |
- Returns
- An AST representing an array of the tuple value, init_value.
Implements tuple_iface.
◆ tuple_create()
| smt_astt smt_tuple_node_flattener::tuple_create |
( |
const expr2tc & | structdef | ) |
|
|
overridevirtual |
Create a new tuple from a struct definition.
- Parameters
-
| structdef | A constant_struct2tc, describing all the members of the tuple to create. |
- Returns
- AST representing the created tuple
Implements tuple_iface.
◆ tuple_fresh()
| smt_astt smt_tuple_node_flattener::tuple_fresh |
( |
smt_sortt | s, |
|
|
std::string | name = "" ) |
|
overridevirtual |
Create a fresh tuple, with freely valued fields.
- Parameters
-
| s | Sort of the tuple to create |
- Returns
- AST representing the created tuple
Implements tuple_iface.
◆ tuple_get() [1/2]
Extract the assignment to a tuple-typed symbol from the SMT solvers model.
Implements tuple_iface.
◆ tuple_get() [2/2]
◆ tuple_get_array_elem()
| expr2tc smt_tuple_node_flattener::tuple_get_array_elem |
( |
smt_astt | array, |
|
|
uint64_t | index, |
|
|
const type2tc & | subtype ) |
|
overridevirtual |
◆ tuple_get_rec()
◆ array_conv
◆ ctx
◆ ns
The documentation for this class was generated from the following files:
1.15.0