cprover
convert_expr_to_smt.h File Reference
+ 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...
 
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). More...
 

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 581 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.