Merge from my post-smtcomp branch. Includes:
[cvc5.git] / src / printer / printer.h
1 /********************* */
2 /*! \file printer.h
3 ** \verbatim
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
13 **
14 ** \brief Base of the pretty-printer interface
15 **
16 ** Base of the pretty-printer interface.
17 **/
18
19 #include "cvc4_private.h"
20
21 #ifndef __CVC4__PRINTER__PRINTER_H
22 #define __CVC4__PRINTER__PRINTER_H
23
24 #include "util/language.h"
25 #include "expr/node.h"
26 #include "expr/command.h"
27
28 namespace CVC4 {
29
30 class Printer {
31 /** Printers for each OutputLanguage */
32 static Printer* d_printers[language::output::LANG_MAX];
33
34 /** Make a Printer for a given OutputLanguage */
35 static Printer* makePrinter(OutputLanguage lang);
36
37 public:
38 /** Get the Printer for a given OutputLanguage */
39 static Printer* getPrinter(OutputLanguage lang) {
40 if(d_printers[lang] == NULL) {
41 d_printers[lang] = makePrinter(lang);
42 }
43 return d_printers[lang];
44 }
45
46 /** Write a Node out to a stream with this Printer. */
47 virtual void toStream(std::ostream& out, TNode n,
48 int toDepth, bool types) const = 0;
49
50 /** Write a Command out to a stream with this Printer. */
51 virtual void toStream(std::ostream& out, const Command* c,
52 int toDepth, bool types) const = 0;
53 };/* class Printer */
54
55 }/* CVC4 namespace */
56
57 #endif /* __CVC4__PRINTER__PRINTER_H */
58