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

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index a86984cca..8ddf809b6 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -27,6 +27,8 @@
 namespace CVC4 {
 namespace theory {
 
+class Theory;
+
 /**
  * A LemmaStatus, returned from OutputChannel::lemma(), provides information
  * about the lemma added.  In particular, it contains the T-rewritten lemma
@@ -206,8 +208,14 @@ public:
    * long-running operations, they cannot rely on resource() to break
    * out of infinite or intractable computations.
    */
-  virtual void spendResource() throw() {
-  }
+  virtual void spendResource() throw() {}
+
+  /** Handle user attribute
+    *   Associates theory t with the attribute attr.  Theory t will be
+    *   notifed whenever an attribute of name attr is set on a node.
+    *   This can happen through, for example, the SMT LIB v2 language.
+    */
+  virtual void handleUserAttribute( const char* attr, Theory* t ){}
 
 };/* class OutputChannel */