* make Model class private (as discussed at meeting today)

* fix minor issue with s-expr parsing in CVC and SMT grammars
* other minor things

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 3 insertions, 2 deletions

diff --git a/src/expr/command.h b/src/expr/command.h
index 9fabf129e..2895f1d51 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -37,13 +37,13 @@
 #include "util/sexpr.h"
 #include "util/datatype.h"
 #include "util/proof.h"
-#include "util/util_model.h"
 
 namespace CVC4 {
 
 class SmtEngine;
 class Command;
 class CommandStatus;
+class Model;
 
 std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
@@ -520,7 +520,8 @@ public:
   GetModelCommand() throw();
   ~GetModelCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
-  Model* getResult() const throw();
+  // Model is private to the library -- for now
+  //Model* getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
   Command* clone() const;