convert_expr_to_smt.h File Reference
#include <solvers/smt2_incremental/object_tracking.h>#include <solvers/smt2_incremental/smt_object_size.h>#include <solvers/smt2_incremental/smt_sorts.h>#include <solvers/smt2_incremental/smt_terms.h>#include <solvers/smt2_incremental/type_size_mapping.h>
Include dependency graph for convert_expr_to_smt.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Functions | |
| smt_sortt | convert_type_to_smt_sort (const typet &type) |
Converts the type to an smt encoding of the same expression stored as sort ast (abstract syntax tree). More... | |
| exprt | lower_address_of_array_index (exprt expr) |
Lower the address_of(array[idx]) sub expressions in expr to idx + address_of(array), so that it can be fed to convert_expr_to_smt. More... | |
| smt_termt | convert_expr_to_smt (const exprt &expression, const smt_object_mapt &object_map, const type_size_mapt &pointer_sizes, const smt_object_sizet::make_applicationt &object_size) |
Converts the expression to an smt encoding of the same expression stored as term ast (abstract syntax tree). More... | |
Function Documentation
◆ convert_expr_to_smt()
| smt_termt convert_expr_to_smt | ( | const exprt & | expression, |
| const smt_object_mapt & | object_map, | ||
| const type_size_mapt & | pointer_sizes, | ||
| const smt_object_sizet::make_applicationt & | object_size | ||
| ) |
Converts the expression to an smt encoding of the same expression stored as term ast (abstract syntax tree).
Definition at line 1837 of file convert_expr_to_smt.cpp.
◆ convert_type_to_smt_sort()
Converts the type to an smt encoding of the same expression stored as sort ast (abstract syntax tree).
Definition at line 100 of file convert_expr_to_smt.cpp.
◆ lower_address_of_array_index()
Lower the address_of(array[idx]) sub expressions in expr to idx + address_of(array), so that it can be fed to convert_expr_to_smt.
Definition at line 1818 of file convert_expr_to_smt.cpp.
