summaryrefslogtreecommitdiff
path: root/src/printer/smt/smt_printer.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-07-17 22:07:59 +0000
committerMorgan Deters <mdeters@gmail.com>2012-07-17 22:07:59 +0000
commit4923b53ad705acc04348da693f03f83f8d9853db (patch)
treeb557cb22ce1f21bcbcca9d6ebdcbf205e5537b58 /src/printer/smt/smt_printer.h
parent2b83291d229c957e2becf7397d186040959602df (diff)
SMT-LIBv2 compliance updates:
* more correct support for get-info responses * printer infrastructure extended to SExprs * parser updates to correctly handle symbols and strings (there were some minor differences from the spec)
Diffstat (limited to 'src/printer/smt/smt_printer.h')
-rw-r--r--src/printer/smt/smt_printer.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h
index 612dfd19e..6e1c607bf 100644
--- a/src/printer/smt/smt_printer.h
+++ b/src/printer/smt/smt_printer.h
@@ -34,6 +34,7 @@ public:
void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const CommandStatus* s) const throw();
+ void toStream(std::ostream& out, const SExpr& sexpr) const throw();
};/* class SmtPrinter */
}/* CVC4::printer::smt namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback