3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
28 const exprt &expression,
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
The type of an expression, extends irept.
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
1.9.8