merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

1 files changed, 3 insertions, 0 deletions

diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 05c3b9695..517786400 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -34,6 +34,8 @@ namespace theory {
 namespace quantifiers {
 
 class TheoryEngine;
+class ModelEngine;
+class InstantiationEngine;
 
 class TheoryQuantifiers : public Theory {
 private:
@@ -59,6 +61,7 @@ public:
   void check(Effort e);
   void propagate(Effort level);
   Node getValue(TNode n);
+  void collectModelInfo( TheoryModel* m );
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
   bool flipDecision();