SMT-LIB get-model output now is easier to machine-parse: contains (model...) bracketing

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5821fbc77e6e9eabd5c15b4cbb430c37b2fb672e..000fd2fbfb7cadab7faa18a0b03daf1dd5a7f2a2 100644 (file)
--- 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 c6d932457bee2b46151a2934a6502cdae33e7c21..32a0c94ba82e54c6c19417b1a1d111628c5ebec1 100644 (file)
--- 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();

diff --git a/test/regress/regress0/bug411.smt2 b/test/regress/regress0/bug411.smt2
index af9acb97af5feb9a098dbbc00799a4609f47d229..3e33c9cd5bcf45efbdb333c91bbc65b4caa588ec 100644 (file)
--- a/test/regress/regress0/bug411.smt2
+++ b/test/regress/regress0/bug411.smt2
@@ -1,5 +1,7 @@
 ; EXPECT: sat
+; EXPECT: (model
 ; EXPECT: (define-fun x () Int 5)
+; EXPECT: )
 ; EXIT: 10
 (set-option :produce-models true)
 (set-logic QF_UFLIA)