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

3 files changed, 59 insertions, 3 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index bdefe6755..bdb3f6cf6 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -379,6 +379,15 @@ Expr Datatype::getConstructor(std::string name) const {
   return (*this)[name].getConstructor();
 }
 
+bool Datatype::involvesExternalType() const{
+  for(const_iterator i = begin(); i != end(); ++i) {
+    if( (*i).involvesExternalType() ){
+      return true;
+    }
+  }
+  return false;
+}
+
 void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
                                   const std::map<std::string, DatatypeType>& resolutions,
                                   const std::vector<Type>& placeholders,
@@ -689,7 +698,7 @@ Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException)
     }
     groundTerms.push_back(selType.mkGroundTerm());
   }
-  
+
   groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
   if( groundTerm.getType()!=t ){
     Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
@@ -722,6 +731,15 @@ Expr DatatypeConstructor::getSelector(std::string name) const {
   return (*this)[name].getSelector();
 }
 
+bool DatatypeConstructor::involvesExternalType() const{
+  for(const_iterator i = begin(); i != end(); ++i) {
+    if(! SelectorType((*i).getSelector().getType()).getRangeType().isDatatype()) {
+      return true;
+    }
+  }
+  return false;
+}
+
 DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) :
   d_name(name),
   d_selector(selector),
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 60d2c7acd..9853ba417 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -316,6 +316,12 @@ public:
    */
   Expr getSelector(std::string name) const;
 
+  /**
+   * Get whether this datatype involves an external type.  If so,
+   * then we will pose additional requirements for sharing.
+   */
+  bool involvesExternalType() const;
+
 };/* class DatatypeConstructor */
 
 /**
@@ -370,7 +376,7 @@ public:
  *    list[T] = cons(car : T, cdr : list[T]) | null,
  *    tree = node(children : list[tree]) | leaf
  *  END;
- * 
+ *
  * Here, the definition of the parametric datatype list, where T is a type variable.
  * In other words, this defines a family of types list[C] where C is any concrete
  * type.  Datatypes can be parameterized over multiple type variables using the
@@ -562,6 +568,12 @@ public:
    */
   Expr getConstructor(std::string name) const;
 
+  /**
+   * Get whether this datatype involves an external type.  If so,
+   * then we will pose additional requirements for sharing.
+   */
+  bool involvesExternalType() const;
+
 };/* class Datatype */
 
 /**
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 */