Go to the documentation of this file.
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
27 const exprt &expression,
32 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
The type of an expression, extends irept.
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)...
Base class for all expressions.
exprt lower_address_of_array_index(exprt expr)
Lower the address_of(array[idx]) sub expressions in expr to idx + address_of(array),...
exprt object_size(const exprt &pointer)
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...
std::unordered_map< exprt, decision_procedure_objectt, irep_hash > smt_object_mapt
Mapping from an object's base expression to the set of information about it which we track.
std::unordered_map< typet, smt_termt, irep_full_hash > type_size_mapt
1.8.17