CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
convert_expr_to_smt.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
5
12
13class exprt;
14class typet;
15
19
24
28 const exprt &expression,
29 const smt_object_mapt &object_map,
32 const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object);
33
34#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
The type of an expression, extends irept.
Definition type.h:29
exprt lower_address_of_array_index(exprt expr)
Lower the address_of(array[idx]) sub expressions in expr to idx + address_of(array),...
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)...
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, const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
Converts the expression to an smt encoding of the same expression stored as term ast (abstract syntax...
Data structures and algorithms used by smt2_incremental_decision_proceduret to track data about the o...
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.
exprt object_size(const exprt &pointer)
Data structure for smt sorts.
Utilities for making a map of types to associated sizes.
std::unordered_map< typet, smt_termt, irep_hash > type_size_mapt