merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

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 */