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, 4 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index c6aaed18a..13de210ab 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -29,14 +29,13 @@ namespace quantifiers {
 class InstantiationEngine : public QuantifiersModule
 {
 private:
-  TheoryQuantifiers* d_th;
-  QuantifiersEngine* getQuantifiersEngine();
-private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   /** status of instantiation round (one of InstStrategy::STATUS_*) */
   int d_inst_round_status;
   /** map from universal quantifiers to their counterexample literals */
   std::map< Node, Node > d_ce_lit;
+  /** whether the instantiation engine should set incomplete if it cannot answer SAT */
+  bool d_setIncomplete;
 private:
   bool hasAddedCbqiLemma( Node f );
   void addCbqiLemma( Node f );
@@ -59,7 +58,7 @@ private:
   /** debug sat */
   void debugSat( int reason );
 public:
-  InstantiationEngine( TheoryQuantifiers* th );
+  InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
   ~InstantiationEngine(){}
 
   void check( Theory::Effort e );