1 files changed, 27 insertions, 1 deletions
diff --git a/src/util/model.h b/src/util/model.h
index 60f1ab23f..747247ae1 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -20,12 +20,38 @@
 #define __CVC4__MODEL_H
 
 #include <iostream>
+#include <vector>
 
 namespace CVC4 {
 
+class Command;
+
 class Model
 {
 public:
+  //types of commands that are recorded for get-model
+  enum {
+    COMMAND_DECLARE_SORT,       //DeclareTypeCommand
+    COMMAND_DECLARE_FUN,        //DeclareFunctionCommand
+    COMMAND_DECLARE_DATATYPES,  //DatatypeDeclarationCommand
+  };
+private:
+  //list of commands that the model must report when calling get model
+  std::vector< Command* > d_commands;
+  std::vector< int > d_command_types;
+public:
+  /** add command */
+  virtual void addCommand( Command* c, int c_type ){
+    d_commands.push_back( c );
+    d_command_types.push_back( c_type );
+  }
+  /** get number of commands to report */
+  int getNumCommands() { return (int)d_commands.size(); }
+  /** get command */
+  Command* getCommand( int i ) { return d_commands[i]; }
+  /** get type of command */
+  int getCommandType( int i ) { return d_command_types[i]; }
+public:
   virtual void toStream(std::ostream& out) = 0;
 };/* class Model */
 
@@ -34,7 +60,7 @@ class ModelBuilder
 public:
   ModelBuilder(){}
   virtual ~ModelBuilder(){}
-  virtual void buildModel( Model* m ) = 0;
+  virtual void buildModel( Model* m, bool fullModel ) = 0;
 };/* class ModelBuilder */
 
 }/* CVC4 namespace */