Model output is now const; this related to bug 519

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 57462c9f746c6bf5548ea68dfe3bce586538b774..88c769f2661acc152b0ff1bf7d0b7340fbb7166e 100644 (file)
--- 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 c9ee6071d46e1ea5b280b5e6616b6f5de37530e5..f09de9d00940a4c318ee5eea140b9d4d181e10d7 100644 (file)
--- 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 23c4727f3221d032b0b0dd90fa5acf94a5aef257..513ff7276d58d0550678726c40cc8185beab8731 100644 (file)
--- 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 49b70b0120334ab5acab65ffe8c0f680886be738..15b04488d21d36d2363d1f0420c892d9d1566090 100644 (file)
--- 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 2a10ae4515a8ec3875ac05d659509f5f2a5f4637..344cbfe8c0dfeebe20d4636b6b721ec640c3f830 100644 (file)
--- 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 48a041d6a3e1c7bf673204eec9296cc342c89040..5198a6ef1f2f225d73981c9a3431579d330a6ea8 100644 (file)
--- 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 f62709988a54ac337e2624182b832b580769fbb8..c5c491cc0ffb4490a91b2ab56497224dbb573be4 100644 (file)
--- 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 185d236996192da3cbd9f2ddf44afb93ad1446f7..9faf76cc0f547bcab467f3547e6f8f1f7f3af68a 100644 (file)
--- 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 ae787f42f2976befa46dfd856e35b09bb0da29d1..1ab364f0c6bed15538900823a38665b5565a49f2 100644 (file)
--- 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 76ec3925802f1fb94768de1369d78e98d2c13e91..871b3823aaf2a0ef6dabba3c4296fabea830f05e 100644 (file)
--- 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();

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fbe44220707355ca1ec3b81d658ed425a9111e31..4ee00161f881e185ed9beb934191e2b0ba4c5bc2 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3166,7 +3166,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
   return quickCheck().asValidityResult();
 }
 
-Node SmtEngine::postprocess(TNode node, TypeNode expectedType) {
+Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
   ModelPostprocessor mpost;
   NodeVisitor<ModelPostprocessor> visitor;
   Node value = visitor.run(mpost, node);
@@ -3221,7 +3221,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
   return n.toExpr();
 }
 
-Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, TypeCheckingException, LogicException) {
+Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
 
@@ -3448,13 +3448,8 @@ void SmtEngine::checkModel(bool hardFailure) {
   // Check individual theory assertions
   d_theoryEngine->checkTheoryAssertionsWithModel();
 
-  if(Notice.isOn()) {
-    // This operator<< routine is non-const (i.e., takes a non-const Model&).
-    // This confuses the Notice() output routines, so extract the ostream
-    // from it and output it "manually."  Should be fixed by making Model
-    // accessors const.
-    Notice.getStream() << *m;
-  }
+  // Output the model
+  Notice() << *m;
 
   // We have a "fake context" for the substitution map (we don't need it
   // to be context-dependent)

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 1b5af415f18102e2a81bb4df7d5d07867116370d..a45fe3383b7d312c5a20a93f2a2a549e912089f1 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -249,7 +249,7 @@ class CVC4_PUBLIC SmtEngine {
    * like turning datatypes back into tuples, length-1-bitvectors back
    * into booleans, etc.
    */
-  Node postprocess(TNode n, TypeNode expectedType);
+  Node postprocess(TNode n, TypeNode expectedType) const;
 
   /**
    * This is something of an "init" procedure, but is idempotent; call
@@ -444,7 +444,7 @@ public:
    * by a SAT or INVALID query).  Only permitted if the SmtEngine is
    * set to operate interactively and produce-models is on.
    */
-  Expr getValue(const Expr& e) throw(ModalException, TypeCheckingException, LogicException);
+  Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException);
 
   /**
    * Add a function to the set of expressions whose value is to be

diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp
index ab4c95ea558febbf5f8cf3a54eaf6467a093dcdc..1c2dc2edfb063c36945448ef9378e5bc8f4f73c4 100644 (file)
--- a/src/util/util_model.cpp
+++ b/src/util/util_model.cpp
@@ -24,7 +24,7 @@ using namespace std;
 
 namespace CVC4 {
 
-std::ostream& operator<<(std::ostream& out, Model& m) {
+std::ostream& operator<<(std::ostream& out, const Model& m) {
   smt::SmtScope smts(&m.d_smt);
   Expr::dag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream(out, m);

diff --git a/src/util/util_model.h b/src/util/util_model.h
index 535493a2dc1141a9a591cb0114e155dc50a283f9..365e7124d7d793642c330e8f4fc40ff50f60d305 100644 (file)
--- a/src/util/util_model.h
+++ b/src/util/util_model.h
@@ -29,10 +29,10 @@ class Command;
 class SmtEngine;
 class Model;
 
-std::ostream& operator<<(std::ostream&, Model&);
+std::ostream& operator<<(std::ostream&, const Model&);
 
 class Model {
-  friend std::ostream& operator<<(std::ostream&, Model&);
+  friend std::ostream& operator<<(std::ostream&, const Model&);
 
 protected:
   /** The SmtEngine we're associated with */
@@ -50,6 +50,8 @@ public:
   const Command* getCommand(size_t i) const;
   /** get the smt engine that this model is hooked up to */
   SmtEngine* getSmtEngine() { return &d_smt; }
+  /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
+  const SmtEngine* getSmtEngine() const { return &d_smt; }
 
 public:
   /** get value for expression */