cprover
convert_expr_to_smt.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
5 
8 
9 class exprt;
10 class typet;
11 
15 
18 smt_termt convert_expr_to_smt(const exprt &expression);
19 
20 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
Base class for all expressions.
Definition: expr.h:54
The type of an expression, extends irept.
Definition: type.h:28
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...
Data structure for smt sorts.