diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-08 17:56:46 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-08 17:56:46 -0500 |
commit | c2393be5f0385609a1fe7cfe76f5665ec53cf4a1 (patch) | |
tree | 816676ad664f9f97e613923a871d007d498a4fd8 /src/printer | |
parent | 7ce4d047670810a10a3f0fc202cd7d94bb4b7e69 (diff) |
SMT-LIB get-model output now is easier to machine-parse: contains (model...) bracketing
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 7 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 1 |
2 files changed, 8 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5821fbc77..000fd2fbf 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -541,6 +541,13 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro }/* Smt2Printer::toStream(CommandStatus*) */ +void Smt2Printer::toStream(std::ostream& out, Model& m) const throw() { + out << "(model" << std::endl; + this->Printer::toStream(out, m); + out << ")" << std::endl; +} + + void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() { theory::TheoryModel& tm = (theory::TheoryModel&) m; if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index c6d932457..32a0c94ba 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -30,6 +30,7 @@ namespace smt2 { class Smt2Printer : public CVC4::Printer { void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); void toStream(std::ostream& out, Model& m, const Command* c) const throw(); + void toStream(std::ostream& out, Model& m) const throw(); 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(); |