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
6
#include <
solvers/smt2_incremental/smt_sorts.h
>
7
#include <
solvers/smt2_incremental/smt_terms.h
>
8
9
class
exprt
;
10
class
typet
;
11
14
smt_sortt
convert_type_to_smt_sort
(
const
typet
&type);
15
18
smt_termt
convert_expr_to_smt
(
const
exprt
&expression);
19
20
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H
typet
The type of an expression, extends irept.
Definition:
type.h:28
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:
convert_expr_to_smt.cpp:34
smt_termt
Definition:
smt_terms.h:16
exprt
Base class for all expressions.
Definition:
expr.h:54
smt_sorts.h
Data structure for smt sorts.
smt_sortt
Definition:
smt_sorts.h:18
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...
Definition:
convert_expr_to_smt.cpp:581
smt_terms.h
solvers
smt2_incremental
convert_expr_to_smt.h
Generated by
1.8.20