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, 8 insertions, 8 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 25800f5b3..234814245 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -389,16 +389,10 @@ public:
   CVC4::SExpr getAssignment() throw(ModalException, AssertionException);
 
   /**
-   * Add to Model Type.  This is used for recording which types should be reported
+   * Add to Model command.  This is used for recording a command that should be reported
    * during a get-model call.
    */
-  void addToModelType( Type& t );
-
-  /**
-   * Add to Model Function.  This is used for recording which functions should be reported
-   * during a get-model call.
-   */
-  void addToModelFunction( Expr& e );
+  void addToModelCommand( Command* c, int c_type );
 
   /**
    * Get the model (only if immediately preceded by a SAT
@@ -565,6 +559,12 @@ public:
    */
   void printModel( std::ostream& out, Model* m );
 
+  /** Set user attribute
+    * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
+    *  via the syntax (! expr :attr)
+    */
+  void setUserAttribute( std::string& attr, Expr expr );
+
 };/* class SmtEngine */
 
 }/* CVC4 namespace */