From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 8 Jan 2013 22:56:46 +0000 (-0500)
Subject: SMT-LIB get-model output now is easier to machine-parse: contains (model...) bracketing
X-Git-Tag: cvc5-1.0.0~7461
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c2393be5f0385609a1fe7cfe76f5665ec53cf4a1;p=cvc5.git

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 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();
diff --git a/test/regress/regress0/bug411.smt2 b/test/regress/regress0/bug411.smt2
index af9acb97a..3e33c9cd5 100644
--- 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)