1 files changed, 13 insertions, 23 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index bf0bb03e1..2fa37ac35 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -26,6 +26,9 @@ namespace quantifiers {
 
 class InstStrategyUserPatterns;
 class InstStrategyAutoGenTriggers;
+class InstStrategyLocalTheoryExt;
+class InstStrategyFreeVariable;
+class InstStrategySimplex;
 
 /** instantiation strategy class */
 class InstStrategy {
@@ -33,7 +36,6 @@ public:
   enum Status {
     STATUS_UNFINISHED,
     STATUS_UNKNOWN,
-    STATUS_SAT,
   };/* enum Status */
 protected:
   /** reference to the instantiation engine */
@@ -57,16 +59,6 @@ public:
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   /** process method, returns a status */
   virtual int process( Node f, Theory::Effort effort, int e ) = 0;
-  /** update status */
-  static void updateStatus( int& currStatus, int addStatus ){
-    if( addStatus==STATUS_UNFINISHED ){
-      currStatus = STATUS_UNFINISHED;
-    }else if( addStatus==STATUS_UNKNOWN ){
-      if( currStatus==STATUS_SAT ){
-        currStatus = STATUS_UNKNOWN;
-      }
-    }
-  }
   /** identify */
   virtual std::string identify() const { return std::string("Unknown"); }
 };/* class InstStrategy */
@@ -77,24 +69,19 @@ private:
   /** instantiation strategies */
   std::vector< InstStrategy* > d_instStrategies;
   /** instantiation strategies active */
-  std::map< InstStrategy*, bool > d_instStrategyActive;
+  //std::map< InstStrategy*, bool > d_instStrategyActive;
   /** user-pattern instantiation strategy */
   InstStrategyUserPatterns* d_isup;
   /** auto gen triggers; only kept for destructor cleanup */
   InstStrategyAutoGenTriggers* d_i_ag;
-  /** is instantiation strategy active */
-  bool isActiveStrategy( InstStrategy* is ) {
-    return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
-  }
-  /** add inst strategy */
-  void addInstStrategy( InstStrategy* is ){
-    d_instStrategies.push_back( is );
-    d_instStrategyActive[is] = true;
-  }
+  /** local theory extensions */
+  InstStrategyLocalTheoryExt * d_i_lte;
+  /** full saturate */
+  InstStrategyFreeVariable * d_i_fs;
+  /** simplex (cbqi) */
+  InstStrategySimplex * d_i_splx;
 private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  /** status of instantiation round (one of InstStrategy::STATUS_*) */
-  int d_inst_round_status;
   /** whether the instantiation engine should set incomplete if it cannot answer SAT */
   bool d_setIncomplete;
   /** inst round counter */
@@ -111,6 +98,8 @@ private:
   bool hasApplyUf( Node f );
   /** whether to do CBQI for quantifier f */
   bool doCbqi( Node f );
+  /** is the engine incomplete for this quantifier */
+  bool isIncomplete( Node f );
 private:
   /** do instantiation round */
   bool doInstantiationRound( Theory::Effort effort );
@@ -149,6 +138,7 @@ public:
     IntStat d_instantiations_cbqi_arith;
     IntStat d_instantiations_cbqi_arith_minus;
     IntStat d_instantiations_cbqi_datatypes;
+    IntStat d_instantiations_lte;
     IntStat d_instantiation_rounds;
     Statistics();
     ~Statistics();