bc61368c10d85cb16c09f4c3561fd593069f78ef
1 /********************* */
2 /*! \file smt_printer.cpp
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
14 ** \brief The pretty-printer interface for the SMT output language
16 ** The pretty-printer interface for the SMT output language.
19 #include "printer/smt/smt_printer.h"
20 #include "expr/expr.h" // for ExprSetDepth etc..
21 #include "util/language.h" // for LANG_AST
22 #include "expr/node_manager.h" // for VarNameAttr
23 #include "expr/command.h"
36 void SmtPrinter::toStream(std::ostream
& out
, TNode n
,
37 int toDepth
, bool types
, size_t dag
) const throw() {
38 n
.toStream(out
, toDepth
, types
, dag
, language::output::LANG_SMTLIB_V2
);
39 }/* SmtPrinter::toStream() */
41 void SmtPrinter::toStream(std::ostream
& out
, const Command
* c
,
42 int toDepth
, bool types
, size_t dag
) const throw() {
43 c
->toStream(out
, toDepth
, types
, dag
, language::output::LANG_SMTLIB_V2
);
44 }/* SmtPrinter::toStream() */
46 void SmtPrinter::toStream(std::ostream
& out
, const CommandStatus
* s
) const throw() {
47 s
->toStream(out
, language::output::LANG_SMTLIB_V2
);
48 }/* SmtPrinter::toStream() */
50 void SmtPrinter::toStream(std::ostream
& out
, const SExpr
& sexpr
) const throw() {
51 Printer::getPrinter(language::output::LANG_SMTLIB_V2
)->toStream(out
, sexpr
);
52 }/* SmtPrinter::toStream() */
54 void SmtPrinter::toStream(std::ostream
& out
, Model
* m
, const Command
* c
) const throw() {
55 Printer::getPrinter(language::output::LANG_SMTLIB_V2
)->toStream(out
, m
, c
);
58 }/* CVC4::printer::smt namespace */
59 }/* CVC4::printer namespace */