1 files changed, 13 insertions, 4 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 46244aec6..2f980fe2f 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -553,11 +553,11 @@ public:
    * Get all relevant information in this theory regarding the current
    * model.  This should be called after a call to check( FULL_EFFORT )
    * for all theories with no conflicts and no lemmas added.
+   * If fullModel is true, then we must specify sufficient information for
+   * the model class to construct constant representatives for each equivalence
+   * class.
    */
-  virtual void collectModelInfo( TheoryModel* m ){
-    Unimplemented("Theory %s doesn't support Theory::getModel interface",
-                  identify().c_str());
-  }
+  virtual void collectModelInfo( TheoryModel* m, bool fullModel ){ }
 
   /**
    * Return a decision request, if the theory has one, or the NULL node
@@ -657,6 +657,15 @@ public:
    */
   virtual std::string identify() const = 0;
 
+  /** 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)
+    */
+  virtual void setUserAttribute( std::string& attr, Node n ) {
+    Unimplemented("Theory %s doesn't support Theory::setUserAttribute interface",
+                  identify().c_str());
+  }
+
   /** A set of theories */
   typedef uint32_t Set;