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, 20 insertions, 2 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 75f4d6a37..d1d6bd1f3 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -274,7 +274,9 @@ class TheoryEngine {
     void spendResource() throw() {
       d_engine->spendResource();
     }
-
+    void handleUserAttribute( const char* attr, theory::Theory* t ){
+      d_engine->handleUserAttribute( attr, t );
+    }
   };/* class TheoryEngine::EngineOutputChannel */
 
   /**
@@ -616,7 +618,7 @@ public:
   /**
    * collect model info
    */
-  void collectModelInfo( theory::TheoryModel* m );
+  void collectModelInfo( theory::TheoryModel* m, bool fullModel );
 
   /**
    * Get the current model
@@ -680,6 +682,22 @@ public:
 
   SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
 
+private:
+  std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
+public:
+
+  /** Set user attribute
+    * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
+    *  via the syntax (! n :attr)
+    */
+  void setUserAttribute( std::string& attr, Node n );
+
+  /** Handle user attribute
+    *   Associates theory t with the attribute attr.  Theory t will be
+    *   notifed whenever an attribute of name attr is set.
+    */
+  void handleUserAttribute( const char* attr, theory::Theory* t );
+
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */