Packages/c/cbmc-doc-6.9.0-1.fc45.x86_64.rpm

// 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:57

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:1888

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:105

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:1947

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:90

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

smt_is_dynamic_objectt::make_applicationt
smt_function_application_termt::factoryt< smt_command_functiont > make_applicationt
Function which makes applications of the smt function.
Definition smt_is_dynamic_object.h:22

smt_object_sizet::make_applicationt
smt_function_application_termt::factoryt< smt_command_functiont > make_applicationt
Function which makes applications of the smt function.
Definition smt_object_size.h:21

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