convert_expr_to_smt.h File Reference

#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>

Include dependency graph for convert_expr_to_smt.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
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). More...
exprt	lower_address_of_array_index (exprt expr)
	Lower the address_of(array[idx]) sub expressions in expr to idx + address_of(array), so that it can be fed to convert_expr_to_smt. More...
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 tree). More...

Function Documentation

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 tree).

Definition at line 1921 of file convert_expr_to_smt.cpp.

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 at line 100 of file convert_expr_to_smt.cpp.

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), so that it can be fed to convert_expr_to_smt.

Definition at line 1862 of file convert_expr_to_smt.cpp.