cprover
smt2_format.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
#ifndef CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
10
#define CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
11
12
#include <
util/expr.h
>
13
14
template
<
typename
T>
15
struct
smt2_format_containert
16
{
17
explicit
smt2_format_containert
(
const
T &_o) :
o
(_o)
18
{
19
}
20
21
const
T &
o
;
22
};
23
24
template
<
typename
T>
25
static
inline
smt2_format_containert<T>
smt2_format
(
const
T &_o)
26
{
27
return
smt2_format_containert<T>
(_o);
28
}
29
30
template
<
typename
T>
31
static
inline
std::ostream &
32
operator<<
(std::ostream &out,
const
smt2_format_containert<T>
&c)
33
{
34
return
smt2_format_rec
(out, c.
o
);
35
}
36
37
std::ostream &
smt2_format_rec
(std::ostream &,
const
exprt
&);
38
std::ostream &
smt2_format_rec
(std::ostream &,
const
typet
&);
39
40
#endif // CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
smt2_format_containert::o
const T & o
Definition:
smt2_format.h:21
smt2_format_rec
std::ostream & smt2_format_rec(std::ostream &, const exprt &)
Definition:
smt2_format.cpp:45
typet
The type of an expression, extends irept.
Definition:
type.h:29
exprt
Base class for all expressions.
Definition:
expr.h:53
expr.h
smt2_format
static smt2_format_containert< T > smt2_format(const T &_o)
Definition:
smt2_format.h:25
smt2_format_containert::smt2_format_containert
smt2_format_containert(const T &_o)
Definition:
smt2_format.h:17
operator<<
static std::ostream & operator<<(std::ostream &out, const smt2_format_containert< T > &c)
Definition:
smt2_format.h:32
smt2_format_containert
Definition:
smt2_format.h:16
solvers
smt2
smt2_format.h
Generated by
1.8.20