Model output is now const; this related to bug 519

10 files changed, 19 insertions, 19 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 57462c9f7..88c769f26 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -185,11 +185,11 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* AstPrinter::toStream(CommandStatus*) */
 
-void AstPrinter::toStream(std::ostream& out, Model& m) const throw() {
+void AstPrinter::toStream(std::ostream& out, const Model& m) const throw() {
   out << "Model()";
 }
 
-void AstPrinter::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+void AstPrinter::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
   // shouldn't be called; only the non-Command* version above should be
   Unreachable();
 }
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index c9ee6071d..f09de9d00 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -29,13 +29,13 @@ namespace ast {
 
 class AstPrinter : 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, const Model& m, const Command* c) const throw();
 public:
   using CVC4::Printer::toStream;
   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, Model& m) const throw();
+  void toStream(std::ostream& out, const Model& m) const throw();
 };/* class AstPrinter */
 
 }/* CVC4::printer::ast namespace */
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 23c4727f3..513ff7276 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -813,8 +813,8 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* CvcPrinter::toStream(CommandStatus*) */
 
-void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
-  theory::TheoryModel& tm = (theory::TheoryModel&) m;
+void CvcPrinter::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
+  const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
     if( options::modelUninterpDtEnum() && tn.isSort() &&
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 49b70b012..15b04488d 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -29,7 +29,7 @@ namespace cvc {
 
 class CvcPrinter : public CVC4::Printer {
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw();
-  void toStream(std::ostream& out, Model& m, const Command* c) const throw();
+  void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
 public:
   using CVC4::Printer::toStream;
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 2a10ae451..344cbfe8c 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -125,7 +125,7 @@ void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
   }
 }/* Printer::toStream(SExpr) */
 
-void Printer::toStream(std::ostream& out, Model& m) const throw() {
+void Printer::toStream(std::ostream& out, const Model& m) const throw() {
   for(size_t i = 0; i < m.getNumCommands(); ++i) {
     toStream(out, m, m.getCommand(i));
   }
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 48a041d6a..5198a6ef1 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -43,7 +43,7 @@ protected:
   Printer() throw() {}
 
   /** write model response to command */
-  virtual void toStream(std::ostream& out, Model& m, const Command* c) const throw() = 0;
+  virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0;
 
 public:
   /** Get the Printer for a given OutputLanguage */
@@ -79,7 +79,7 @@ public:
   virtual void toStream(std::ostream& out, const Result& r) const throw();
 
   /** Write a Model out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, Model& m) const throw();
+  virtual void toStream(std::ostream& out, const Model& m) const throw();
 
 };/* class Printer */
 
diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
index f62709988..c5c491cc0 100644
--- a/src/printer/smt1/smt1_printer.cpp
+++ b/src/printer/smt1/smt1_printer.cpp
@@ -49,11 +49,11 @@ void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw()
   Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
 }/* Smt1Printer::toStream() */
 
-void Smt1Printer::toStream(std::ostream& out, Model& m) const throw() {
+void Smt1Printer::toStream(std::ostream& out, const Model& m) const throw() {
   Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m);
 }
 
-void Smt1Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+void Smt1Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
   // shouldn't be called; only the non-Command* version above should be
   Unreachable();
 }
diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h
index 185d23699..9faf76cc0 100644
--- a/src/printer/smt1/smt1_printer.h
+++ b/src/printer/smt1/smt1_printer.h
@@ -28,14 +28,14 @@ namespace printer {
 namespace smt1 {
 
 class Smt1Printer : public CVC4::Printer {
-  void toStream(std::ostream& out, Model& m, const Command* c) const throw();
+  void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
 public:
   using CVC4::Printer::toStream;
   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();
-  void toStream(std::ostream& out, Model& m) const throw();
+  void toStream(std::ostream& out, const Model& m) const throw();
 };/* class Smt1Printer */
 
 }/* CVC4::printer::smt1 namespace */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index ae787f42f..1ab364f0c 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -606,15 +606,15 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
 }/* Smt2Printer::toStream(CommandStatus*) */
 
 
-void Smt2Printer::toStream(std::ostream& out, Model& m) const throw() {
+void Smt2Printer::toStream(std::ostream& out, const 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;
+void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
+  const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
     if( options::modelUninterpDtEnum() && tn.isSort() &&
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 76ec39258..871b3823a 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -29,8 +29,8 @@ 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();
+  void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
+  void toStream(std::ostream& out, const Model& m) const throw();
 public:
   using CVC4::Printer::toStream;
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();