Add local theory extensions instantiation strategy (incomplete). Refactor how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.

16 files changed, 303 insertions, 144 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c87753d8d..a80177429 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1268,25 +1268,22 @@ void SmtEngine::setDefaults() {
     options::decisionMode.set(decMode);
     options::decisionStopOnly.set(stoponly);
   }
-
-  //for finite model finding
-  if( ! options::instWhenMode.wasSetByUser()){
-    //instantiate only on last call
-    if( options::fmfInstEngine() ){
-      Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
-      options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
+  //local theory extensions 
+  if( options::localTheoryExt() ){
+    //no E-matching?
+    if( !options::instMaxLevel.wasSetByUser() ){
+      options::instMaxLevel.set( 0 );
     }
   }
   if( d_logic.hasCardinalityConstraints() ){
     //must have finite model finding on
     options::finiteModelFind.set( true );
   }
-  if( options::recurseCbqi() ){
-    options::cbqi.set( true );
-  }
   if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) {
     options::fmfBoundInt.set( true );
   }
+  //now have determined whether fmfBoundInt is on/off
+  //apply fmfBoundInt options
   if( options::fmfBoundInt() ){
     //must have finite model finding on
     options::finiteModelFind.set( true );
@@ -1301,6 +1298,35 @@ void SmtEngine::setDefaults() {
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
+  if( options::fmfFunWellDefined() ){
+    if( !options::finiteModelFind.wasSetByUser() ){
+      options::finiteModelFind.set( true );
+    }
+  }
+  
+  //now, have determined whether finite model find is on/off
+  //apply finite model finding options
+  if( options::finiteModelFind() ){
+    if( !options::eMatching.wasSetByUser() ){
+      options::eMatching.set( options::fmfInstEngine() );
+    }
+    if( !options::quantConflictFind.wasSetByUser() ){
+      options::quantConflictFind.set( false );
+    }
+    //for finite model finding
+    if( ! options::instWhenMode.wasSetByUser()){
+      //instantiate only on last call
+      if( options::eMatching() ){
+        Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
+        options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
+      }
+    }
+  }
+  
+  //implied options...
+  if( options::recurseCbqi() ){
+    options::cbqi.set( true );
+  }
   if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }
@@ -1342,16 +1368,7 @@ void SmtEngine::setDefaults() {
       options::conjectureGen.set( false );
     }
   }
-  if( options::fmfFunWellDefined() ){
-    if( !options::finiteModelFind.wasSetByUser() ){
-      options::finiteModelFind.set( true );
-    }
-  }
-  if( options::finiteModelFind() ){
-    if( !options::quantConflictFind.wasSetByUser() ){
-      options::quantConflictFind.set( false );
-    }
-  }
+
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
     if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index dd56ebba9..a70343702 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -123,6 +123,7 @@ void TheoryDatatypes::check(Effort e) {
   if (done() && !fullEffort(e)) {
     return;
   }
+  d_addedLemma = false;
 
   TimerStat::CodeTimer checkTimer(d_checkTime);
 
@@ -150,14 +151,15 @@ void TheoryDatatypes::check(Effort e) {
     flushPendingFacts();
   }
 
-  if( e == EFFORT_FULL && !d_conflict && !d_valuation.needCheck() ) {
+  if( e == EFFORT_FULL && !d_conflict && !d_addedLemma && !d_valuation.needCheck() ) {
     //check for cycles
+    Assert( d_pending.empty() && d_pending_merge.empty() );
     bool addedFact;
     do {
       checkCycles();
       addedFact = !d_pending.empty() || !d_pending_merge.empty();
       flushPendingFacts();
-      if( d_conflict ){
+      if( d_conflict || d_addedLemma ){
         return;
       }
     }while( addedFact );
@@ -305,6 +307,7 @@ void TheoryDatatypes::flushPendingFacts(){
         }
         Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
         d_out->lemma( lem );
+        d_addedLemma = true;
       }else{
         assertFact( fact, exp );
       }
@@ -1506,6 +1509,7 @@ void TheoryDatatypes::checkCycles() {
   }
   //process codatatypes
   if( cdt_eqc.size()>1 && options::cdtBisimilar() ){
+    printModelDebug("dt-cdt-debug");
     Trace("dt-cdt-debug") << "Process " << cdt_eqc.size() << " co-datatypes" << std::endl;
     std::vector< std::vector< Node > > part_out;
     std::vector< TNode > exp;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 84d894098..30b0140a9 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -160,6 +160,8 @@ private:
   //BoolMap d_consEqc;
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
+  /** Added lemma ? */
+  bool d_addedLemma;
   /** The conflict node */
   Node d_conflictNode;
   /** cache for which terms we have called collectTerms(...) on */
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index a10181c51..cfaa6d1ad 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -192,19 +192,29 @@ void CandidateGeneratorQEAll::resetInstantiationRound() {
 
 void CandidateGeneratorQEAll::reset( Node eqc ) {
   d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+  d_firstTime = true;
 }
 
 Node CandidateGeneratorQEAll::getNextCandidate() {
   while( !d_eq.isFinished() ){
     Node n = (*d_eq);
-    if( options::instMaxLevel()!=-1 ){
-      n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index );
-    }
     ++d_eq;
-    if( n.getType().isSubtypeOf( d_match_pattern.getType() ) ){
-      //an equivalence class with the same type as the pattern, return it
-      return n;
+    if( n.getType().isSubtypeOf( d_match_pattern_type ) ){
+      if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
+        if( options::instMaxLevel()!=-1 ){
+          n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index );
+        }
+        d_firstTime = false;
+        //an equivalence class with the same type as the pattern, return it
+        return n;
+      }
     }
   }
+  if( d_firstTime ){
+    Assert( d_qe->getTermDatabase()->d_type_map[d_match_pattern_type].empty() );
+    //must return something
+    d_firstTime = false;
+    return d_qe->getTermDatabase()->getFreeVariableForType( d_match_pattern_type );
+  }
   return Node::null();
 }
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 011e2924d..7a959a70d 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -150,6 +150,8 @@ private:
   // quantifier/index for the variable we are matching
   Node d_f;
   unsigned d_index;
+  //first time
+  bool d_firstTime;
 public:
   CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
   ~CandidateGeneratorQEAll(){}
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 4a5197fc8..cd24f9ac2 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -456,7 +456,7 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersE
 }
 
 /** constructors */
-InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) :
+InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe ) :
 d_f( f ){
   Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;
   std::map< Node, std::vector< Node > > var_contains;
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 850affe56..1be67caed 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -184,7 +184,7 @@ private:
   void calculateMatches( QuantifiersEngine* qe );
 public:
   /** constructors */
-  InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
+  InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe );
   /** destructor */
   ~InstMatchGeneratorMulti(){}
   /** reset instantiation round (call this whenever equivalence classes have changed) */
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 8a0ec3c09..8918a6dac 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -28,6 +28,14 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 using namespace CVC4::theory::quantifiers;
 
+//priority levels :
+//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers)
+//2 : user patterns (when user-pat=resort ), auto gen patterns (for user pattern quantifiers, when user-pat=use)
+//3 : local theory extensions
+//4 :
+//5 : full saturate quantifiers
+
+
 //#define MULTI_TRIGGER_FULL_EFFORT_HALF
 #define MULTI_MULTI_TRIGGERS
 
@@ -220,15 +228,16 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
     d_patTerms[0][f].clear();
     d_patTerms[1][f].clear();
     std::vector< Node > patTermsF;
+    //well-defined function: can assume LHS is only trigger
+    Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
     if( d_quantEngine->getTermDatabase()->isQAttrFunDef( f ) && options::quantFunWellDefined() ){
-      Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
       Assert( bd.getKind()==EQUAL || bd.getKind()==IFF );
       Assert( bd[0].getKind()==APPLY_UF );
       patTermsF.push_back( bd[0] );
     }else{
-      Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, d_user_no_gen[f], true );
+      Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true );
     }
-    Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
+    Trace("auto-gen-trigger") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
     Trace("auto-gen-trigger") << "   ";
     for( int i=0; i<(int)patTermsF.size(); i++ ){
       Trace("auto-gen-trigger") << patTermsF[i] << " ";
@@ -321,8 +330,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
         d_made_multi_trigger[f] = true;
       }
       //will possibly want to get an old trigger
-      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,
-                               options::smartTriggers() );
+      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, options::smartTriggers() );
     }
     if( tr ){
       if( tr->isMultiTrigger() ){
@@ -356,8 +364,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
             if( !options::relevantTriggers() ||
                 d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
               d_single_trigger_gen[ patTerms[index] ] = true;
-              Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,
-                                                 options::smartTriggers() );
+              Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() );
               if( tr2 ){
                 //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
                 tr2->resetInstantiationRound();
@@ -404,7 +411,75 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node f, Node pat ) {
   }
 }
 
+
+void InstStrategyLocalTheoryExt::processResetInstantiationRound( Theory::Effort effort ){
+  //reset triggers
+  for( std::map< Node, Trigger* >::iterator it = d_lte_trigger.begin(); it != d_lte_trigger.end(); ++it ){
+    it->second->resetInstantiationRound();
+    it->second->reset( Node::null() );
+  }
+}
+
+int InstStrategyLocalTheoryExt::process( Node f, Theory::Effort effort, int e ) {
+  if( e<3 ){
+    return STATUS_UNFINISHED;
+  }else if( e==3 ){
+    if( isLocalTheoryExt( f ) ){
+      std::map< Node, Trigger* >::iterator it = d_lte_trigger.find( f );
+      if( it!=d_lte_trigger.end() ){
+        Trigger * tr = it->second;
+        //process the trigger
+        Trace("process-trigger") << "  LTE process ";
+        tr->debugPrint("process-trigger");
+        Trace("process-trigger") << "..." << std::endl;
+        InstMatch baseMatch( f );
+        int numInst = tr->addInstantiations( baseMatch );
+        Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
+        d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_lte += numInst;
+      }
+    }
+  }
+  return STATUS_UNKNOWN;
+}
+
+bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
+  std::map< Node, bool >::iterator itq = d_quant.find( f );
+  if( itq==d_quant.end() ){
+    //generate triggers
+    Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
+    std::vector< Node > vars;
+    std::vector< Node > patTerms;
+    bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms );
+    if( ret ){
+      d_quant[f] = ret;
+      //add all variables to trigger that don't already occur
+      for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+        Node x = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+        if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
+          patTerms.push_back( x );
+        }
+      }
+      Trace("local-t-ext") << "Local theory extensions trigger for " << f << " : " << std::endl;
+      for( unsigned i=0; i<patTerms.size(); i++ ){
+        Trace("local-t-ext") << "  " << patTerms[i] << std::endl;
+      }
+      Trace("local-t-ext") << std::endl;
+      int matchOption = 0;
+      Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD, options::smartTriggers() );
+      d_lte_trigger[f] = tr;
+    }else{
+      Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl;
+      Trace("local-t-ext-warn") << "WARNING: not local theory extensions : " << f << std::endl;
+    }
+    d_quant[f] = ret;
+    return ret;
+  }else{
+    return itq->second;
+  }
+}
+
 void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
+  
 }
 
 int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
@@ -503,6 +578,6 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
         }
       }
     }
-    return STATUS_UNKNOWN;
   }
+  return STATUS_UNKNOWN;
 }
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index dd4486803..d2c611d34 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -58,7 +58,7 @@ public:
   std::string identify() const { return std::string("UserPatterns"); }
 };/* class InstStrategyUserPatterns */
 
-class InstStrategyAutoGenTriggers : public InstStrategy{
+class InstStrategyAutoGenTriggers : public InstStrategy {
 public:
   enum {
     RELEVANCE_NONE,
@@ -98,7 +98,7 @@ public:
   /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)
       rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)
       rgfr is the frequency at which triggers are generated */
-  InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt,  int rgfr = -1 );
+  InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rgfr = -1 );
   ~InstStrategyAutoGenTriggers(){}
 public:
   /** get auto-generated trigger */
@@ -109,6 +109,26 @@ public:
   void addUserNoPattern( Node f, Node pat );
 };/* class InstStrategyAutoGenTriggers */
 
+
+class InstStrategyLocalTheoryExt : public InstStrategy {
+private:
+  /** have we registered quantifier, value is whether it is an LTE term */
+  std::map< Node, bool > d_quant;
+  /** triggers for each quantifier */
+  std::map< Node, inst::Trigger* > d_lte_trigger;
+private:
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e );
+public:
+  InstStrategyLocalTheoryExt( QuantifiersEngine* qe ) : InstStrategy( qe ){}
+  /** identify */
+  std::string identify() const { return std::string("LocalTheoryExt"); }
+  /** is local theory quantifier? */
+  bool isLocalTheoryExt( Node f );
+};
+
+
 class InstStrategyFreeVariable : public InstStrategy{
 private:
   /** guessed instantiations */
@@ -124,6 +144,7 @@ public:
   std::string identify() const { return std::string("FreeVariable"); }
 };/* class InstStrategyFreeVariable */
 
+
 }
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 1cb86e32f..ade6d4313 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -31,26 +31,26 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
 
 }
 
 InstantiationEngine::~InstantiationEngine() {
   delete d_i_ag;
   delete d_isup;
+  delete d_i_lte;
+  delete d_i_fs;
+  delete d_i_splx;
 }
 
 void InstantiationEngine::finishInit(){
-  if( !options::finiteModelFind() || options::fmfInstEngine() ){
-
+  if( options::eMatching() ){
     //these are the instantiation strategies for E-matching
     
     //user-provided patterns
     if( options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
       d_isup = new InstStrategyUserPatterns( d_quantEngine );
-      addInstStrategy( d_isup );
-    }else{
-      d_isup = NULL;
+      d_instStrategies.push_back( d_isup );
     }
     
     //auto-generated patterns
@@ -61,18 +61,25 @@ void InstantiationEngine::finishInit(){
       tstrt = Trigger::TS_MAX_TRIGGER;
     }
     d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, tstrt, 3 );
-    addInstStrategy( d_i_ag );
-    
-    //full saturation : instantiate from relevant domain, then arbitrary terms
-    if( !options::finiteModelFind() && options::fullSaturateQuant() ){
-      addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) );
-    }
+    d_instStrategies.push_back( d_i_ag );
+  }
+  
+  //local theory extensions
+  if( options::localTheoryExt() ){
+    d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine );
+    d_instStrategies.push_back( d_i_lte );
+  }
+  
+  //full saturation : instantiate from relevant domain, then arbitrary terms
+  if( options::fullSaturateQuant() ){
+    d_i_fs = new InstStrategyFreeVariable( d_quantEngine );
+    d_instStrategies.push_back( d_i_fs );
   }
   
   //counterexample-based quantifier instantiation
   if( options::cbqi() ){
-    addInstStrategy( new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ) );
-  //  addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) );
+    d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
+    d_instStrategies.push_back( d_i_splx );
   }
 }
 
@@ -117,18 +124,16 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   //reset the instantiators
   for( size_t i=0; i<d_instStrategies.size(); ++i ){
     InstStrategy* is = d_instStrategies[i];
-    if( isActiveStrategy( is ) ){
-      is->processResetInstantiationRound( effort );
-    }
+    is->processResetInstantiationRound( effort );
   }
   //iterate over an internal effort level e
   int e = 0;
   int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
-  d_inst_round_status = InstStrategy::STATUS_UNFINISHED;
+  bool finished = false;
   //while unfinished, try effort level=0,1,2....
-  while( d_inst_round_status==InstStrategy::STATUS_UNFINISHED && e<=eLimit ){
+  while( !finished && e<=eLimit ){
     Debug("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl;
-    d_inst_round_status = InstStrategy::STATUS_SAT;
+    finished = true;
     //instantiate each quantifier
     for( int q=0; q<d_quantEngine->getModel()->getNumAssertedQuantifiers(); q++ ){
       Node f = d_quantEngine->getModel()->getAssertedQuantifier( q );
@@ -141,11 +146,13 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           //check each instantiation strategy
           for( size_t i=0; i<d_instStrategies.size(); ++i ){
             InstStrategy* is = d_instStrategies[i];
-            if( isActiveStrategy( is ) && is->shouldProcess( f ) ){
+            if( is->shouldProcess( f ) ){
               Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
               int quantStatus = is->process( f, effort, e_use );
               Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
-              InstStrategy::updateStatus( d_inst_round_status, quantStatus );
+              if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
+                finished = false;
+              }
             }
           }
         }
@@ -153,7 +160,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
     }
     //do not consider another level if already added lemma at this level
     if( d_quantEngine->d_lemmas_waiting.size()>lastWaiting ){
-      d_inst_round_status = InstStrategy::STATUS_UNKNOWN;
+      finished = true;
     }
     e++;
   }
@@ -266,28 +273,27 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
     }
     if( quantActive ){
       bool addedLemmas = doInstantiationRound( e );
-      //Debug("quantifiers-dec") << "Do instantiation, level = " << d_quantEngine->getValuation().getDecisionLevel() << std::endl;
-      //for( int i=1; i<=(int)d_valuation.getDecisionLevel(); i++ ){
-      //  Debug("quantifiers-dec") << "   " << d_valuation.getDecision( i ) << std::endl;
-      //}
-      if( e==Theory::EFFORT_LAST_CALL ){
-        if( !addedLemmas ){
-          if( d_inst_round_status==InstStrategy::STATUS_SAT ){
-            Debug("inst-engine") << "No instantiation given, returning SAT..." << std::endl;
-            debugSat( SAT_INST_STRATEGY );
-          }else if( d_setIncomplete ){
+      if( !addedLemmas && e==Theory::EFFORT_LAST_CALL ){
+        //check if we need to set the incomplete flag
+        if( d_setIncomplete ){
+          //check if we are complete for all active quantifiers
+          bool inc = false;
+          for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+            Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+            if( isIncomplete( f ) ){
+              inc = true;
+              break;
+            }
+          }
+          if( inc ){
             Debug("inst-engine") << "No instantiation given, returning unknown..." << std::endl;
             d_quantEngine->getOutputChannel().setIncomplete();
           }else{
-            Assert( options::finiteModelFind() );
-            Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl;
+            Debug("inst-engine") << "Instantiation strategies were complete..." << std::endl;
           }
-        }
-      }
-    }else{
-      if( e==Theory::EFFORT_LAST_CALL ){
-        if( options::cbqi() ){
-          debugSat( SAT_CBQI );
+        }else{
+          Assert( options::finiteModelFind() );
+          Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl;
         }
       }
     }
@@ -365,6 +371,15 @@ bool InstantiationEngine::doCbqi( Node f ){
   }
 }
 
+bool InstantiationEngine::isIncomplete( Node f ) {
+  if( d_i_lte ){
+    //TODO : ensure completeness for local theory extensions
+    //return !d_i_lte->isLocalTheoryExt( f );
+    return true;
+  }else{
+    return true;
+  }
+}
 
 
 
@@ -449,6 +464,7 @@ InstantiationEngine::Statistics::Statistics():
   d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
   d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
   d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0),
+  d_instantiations_lte("InstantiationEngine::Instantiations_Local_T_Ext", 0),
   d_instantiation_rounds("InstantiationEngine::Rounds", 0 )
 {
   StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
@@ -458,6 +474,7 @@ InstantiationEngine::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes);
+  StatisticsRegistry::registerStat(&d_instantiations_lte);
   StatisticsRegistry::registerStat(&d_instantiation_rounds);
 }
 
@@ -469,5 +486,6 @@ InstantiationEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes);
+  StatisticsRegistry::unregisterStat(&d_instantiations_lte);
   StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
 }
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();
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index f4f1bcd86..dad173ff5 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -5,6 +5,9 @@
 
 module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers
 
+option eMatching --e-matching bool :read-write :default true
+ whether to do heuristic E-matching
+
 # Whether to mini-scope quantifiers.
 # For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
 # ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
@@ -87,7 +90,7 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false
 
 option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
  when to apply instantiation
-option instMaxLevel --inst-max-level=N int :default -1
+option instMaxLevel --inst-max-level=N int :read-write :default -1
  maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
 option instLevelInputOnly --inst-level-input-only bool :default true
  only input terms are assigned instantiation level zero
@@ -190,4 +193,8 @@ option ceGuidedInst --cegqi bool :default false
 option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
   if and how to apply fairness for cegqi
  
+
+option localTheoryExt --local-t-ext bool :default false
+  do instantiation based on local theory extensions
+ 
 endmodule
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9e7d14b9a..5dc8bb384 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -847,21 +847,29 @@ Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) {
 
 
 Node TermDb::getFreeVariableForInstConstant( Node n ){
-  TypeNode tn = n.getType();
+  return getFreeVariableForType( n.getType() );
+}
+
+Node TermDb::getFreeVariableForType( TypeNode tn ) {
   if( d_free_vars.find( tn )==d_free_vars.end() ){
-	for( unsigned i=0; i<d_type_map[ tn ].size(); i++ ){
-	  if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){
-	    d_free_vars[tn] = d_type_map[ tn ][ i ];
-	  }
-	}
-	if( d_free_vars.find( tn )==d_free_vars.end() ){
+    for( unsigned i=0; i<d_type_map[ tn ].size(); i++ ){
+      if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){
+        d_free_vars[tn] = d_type_map[ tn ][ i ];
+      }
+    }
+    if( d_free_vars.find( tn )==d_free_vars.end() ){
       //if integer or real, make zero
       if( tn.isInteger() || tn.isReal() ){
         Rational z(0);
         d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
       }else{
-	    d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" );
-	    Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl;
+        Node n = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" );
+        d_free_vars[tn] = n;
+        Trace("mkVar") << "FreeVar:: Make variable " << n << " : " << tn << std::endl;
+        //must set instantiation level attribute to 0 if we are using instantiation max level
+        if( options::instMaxLevel()!=-1 ){
+          QuantifiersEngine::setInstantiationLevelAttr( n, 0 );
+        }
       }
     }
   }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 4dca6b36c..2b151bb04 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -279,6 +279,8 @@ public:
 public:
   /** get free variable for instantiation constant */
   Node getFreeVariableForInstConstant( Node n );
+  /** get free variable for type */
+  Node getFreeVariableForType( TypeNode tn );
 
 //for triggers
 private:
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 511103019..65b976b4a 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -47,7 +47,7 @@ d_quantEngine( qe ), d_f( f ){
         d_mg->setActiveAdd(true);
       }
     }else{
-      d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption );
+      d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
       //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
       //d_mg->setActiveAdd();
     }
@@ -385,29 +385,7 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
   }
 }
 
-bool Trigger::isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms ) {
-  if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
-    bool hasVar = false;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( n[i].getKind()==APPLY_UF ){
-        return false;
-      }else if( n[i].getKind()==INST_CONSTANT ){
-        hasVar = true;
-        //if( std::find( var_found.begin(), var_found.end(), n[i]
-      }
-    }
-    if( hasVar ){
-      patTerms.push_back( n );
-    }
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !isLocalTheoryExt2( n, var_found, patTerms ) ){
-        return false;
-      } 
-    }
-  }
-  return true;
-}
+
 
 bool Trigger::isBooleanTermTrigger( Node n ) {
   if( n.getKind()==ITE ){
@@ -438,9 +416,36 @@ bool Trigger::isPureTheoryTrigger( Node n ) {
   }
 }
 
-bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& patTerms ) {
-  std::vector< Node > var_found;
-  return isLocalTheoryExt2( n, var_found, patTerms );
+bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
+  if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
+    if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){
+      bool hasVar = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( n[i].getKind()==INST_CONSTANT ){
+          hasVar = true;
+          if( std::find( vars.begin(), vars.end(), n[i] )==vars.end() ){
+            vars.push_back( n[i] );
+          }else{
+            //do not allow duplicate variables
+            return false;
+          }
+        }else{
+          //do not allow nested function applications
+          return false;
+        }
+      }
+      if( hasVar ){
+        patTerms.push_back( n );
+      }
+    }
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( !isLocalTheoryExt( n[i], vars, patTerms ) ){
+        return false;
+      } 
+    }
+  }
+  return true;
 }
 
 void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 482701a82..28da9f959 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -95,8 +95,6 @@ private:
   static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
   /** collect all APPLY_UF pattern terms for f in n */
   static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
-  /** is local theory extensions term */
-  static bool isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms );
 public:
   //different strategies for choosing trigger terms
   enum {
@@ -113,7 +111,7 @@ public:
   static bool isSimpleTrigger( Node n );
   static bool isBooleanTermTrigger( Node n );
   static bool isPureTheoryTrigger( Node n );
-  static bool isLocalTheoryExt( Node n, std::vector< Node >& patTerms );
+  static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms );
   /** return data structure for producing matches for this trigger. */
   static InstMatchGenerator* getInstMatchGenerator( Node n );
   static Node getInversionVariable( Node n );