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

diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 1e42abd22..bc712955e 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -61,17 +61,17 @@ public:
   void presolve();
   void check(Effort e);
   void propagate(Effort level);
+  Node getNextDecisionRequest();
   Node getValue(TNode n);
-  void collectModelInfo( TheoryModel* m );
+  void collectModelInfo( TheoryModel* m, bool fullModel );
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
   bool flipDecision();
+  void setUserAttribute( std::string& attr, Node n );
 private:
   void assertUniversal( Node n );
   void assertExistential( Node n );
   bool restart();
-public:
-  void performCheck(Effort e);
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */