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