convert_expr_to_smt.h File Reference

#include <solvers/smt2_incremental/smt_sorts.h>
#include <solvers/smt2_incremental/smt_terms.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).
smt_termt	convert_expr_to_smt (const exprt &expression)
	Converts the expression to an smt encoding of the same expression stored as term ast (abstract syntax tree).

Function Documentation

convert_expr_to_smt()

smt_termt convert_expr_to_smt

(

const exprt &

expression

)

Converts the expression to an smt encoding of the same expression stored as term ast (abstract syntax tree).

Definition at line 679 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 34 of file convert_expr_to_smt.cpp.