CBMC
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 <iosfwd>
13 
14 class exprt;
15 class typet;
16 
17 template <typename T>
18 struct smt2_format_containert
19 {
20  explicit smt2_format_containert(const T &_o) : o(_o)
21  {
22  }
23 
24  const T &o;
25 };
26 
27 template <typename T>
28 static inline smt2_format_containert<T> smt2_format(const T &_o)
29 {
30  return smt2_format_containert<T>(_o);
31 }
32 
33 template <typename T>
34 static inline std::ostream &
35 operator<<(std::ostream &out, const smt2_format_containert<T> &c)
36 {
37  return smt2_format_rec(out, c.o);
38 }
39 
40 std::ostream &smt2_format_rec(std::ostream &, const exprt &);
41 std::ostream &smt2_format_rec(std::ostream &, const typet &);
42 
43 #endif // CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
exprt
Base class for all expressions.
Definition: expr.h:56
typet
The type of an expression, extends irept.
Definition: type.h:29
operator<<
static std::ostream & operator<<(std::ostream &out, const smt2_format_containert< T > &c)
Definition: smt2_format.h:35
smt2_format_rec
std::ostream & smt2_format_rec(std::ostream &, const exprt &)
Definition: smt2_format.cpp:45
smt2_format
static smt2_format_containert< T > smt2_format(const T &_o)
Definition: smt2_format.h:28
smt2_format_containert
Definition: smt2_format.h:19
smt2_format_containert::o
const T & o
Definition: smt2_format.h:24
smt2_format_containert::smt2_format_containert
smt2_format_containert(const T &_o)
Definition: smt2_format.h:20