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, 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;