3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
Base class for all expressions.
The type of an expression, extends irept.
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.