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>
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