From 446cba594a8b26c03aabb2385b18c2ccad637f2f Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 6 Jul 2013 20:32:48 -0400
Subject: Model output is now const; this related to bug 519

---
 src/util/util_model.cpp | 2 +-
 src/util/util_model.h   | 6 ++++--
 2 files changed, 5 insertions(+), 3 deletions(-)

(limited to 'src/util')

diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp
index ab4c95ea5..1c2dc2edf 100644
--- 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 535493a2d..365e7124d 100644
--- 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 */
-- 
cgit v1.2.3