cprover
Loading...
Searching...
No Matches
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
9class exprt;
10class typet;
11
15
18smt_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:29
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.