cbmc/convert__expr__to__smt_8h_source.html

 // Author: Diffblue Ltd.


 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H

 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H


 #include <solvers/smt2_incremental/ast/smt_sorts.h>

 #include <solvers/smt2_incremental/ast/smt_terms.h>

 #include <solvers/smt2_incremental/object_tracking.h>

 #include <solvers/smt2_incremental/smt_is_dynamic_object.h>

 #include <solvers/smt2_incremental/smt_object_size.h>

 #include <solvers/smt2_incremental/type_size_mapping.h>


 class exprt;

 class typet;


 smt_sortt convert_type_to_smt_sort(const typet &type);


 exprt lower_address_of_array_index(exprt expr);


 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);


 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H

exprt
Base class for all expressions.
Definition: expr.h:56

smt_function_application_termt::factoryt< smt_command_functiont >

smt_sortt
Definition: smt_sorts.h:18

smt_termt
Definition: smt_terms.h:21

typet
The type of an expression, extends irept.
Definition: type.h:29

lower_address_of_array_index
exprt lower_address_of_array_index(exprt expr)
Lower the address_of(array[idx]) sub expressions in expr to idx + address_of(array),...
Definition: convert_expr_to_smt.cpp:1862

convert_type_to_smt_sort
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)...
Definition: convert_expr_to_smt.cpp:100

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, 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...
Definition: convert_expr_to_smt.cpp:1921

object_tracking.h
Data structures and algorithms used by smt2_incremental_decision_proceduret to track data about the o...

smt_object_mapt
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.
Definition: object_tracking.h:91

object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:33

smt_is_dynamic_object.h

smt_object_size.h

smt_sorts.h
Data structure for smt sorts.

smt_terms.h

type_size_mapping.h
Utilities for making a map of types to associated sizes.

type_size_mapt
std::unordered_map< typet, smt_termt, irep_hash > type_size_mapt
Definition: type_size_mapping.h:18