New trigger options. --inst-no-entail on by default. Misc cleanup.

15 files changed, 278 insertions, 339 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 299ae5678..6aa8b71dd 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -334,8 +334,8 @@ void TheoryDatatypes::check(Effort e) {
     }while( !d_conflict && addedFact );
     Trace("datatypes-debug") << "Finished. " << d_conflict << std::endl;
     if( !d_conflict ){
-      Trace("dt-model-test") << std::endl;
-      printModelDebug("dt-model-test");
+      Trace("dt-model-debug") << std::endl;
+      printModelDebug("dt-model-debug");
     }
   }
 
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index f378b4913..c205a280e 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -38,11 +38,6 @@ InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie
   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
 }
 
-bool InstStrategySimplex::calculateShouldProcess( Node f ){
-  //DO_THIS
-  return false;
-}
-
 void getInstantiationConstants( Node n, std::vector< Node >& ics ){
   if( n.getKind()==INST_CONSTANT ){
     if( std::find( ics.begin(), ics.end(), n )==ics.end() ){
@@ -58,6 +53,7 @@ void getInstantiationConstants( Node n, std::vector< Node >& ics ){
 
 void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
   Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
+  d_quantActive.clear();
   d_instRows.clear();
   d_tableaux_term.clear();
   d_tableaux.clear();
@@ -133,85 +129,87 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
   if( e<2 ){
     return STATUS_UNFINISHED;
   }else if( e==2 ){
-    //the point instantiation
-    InstMatch m_point( f );
-    bool m_point_valid = true;
-    int lem = 0;
-    //scan over all instantiation rows
-    for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-      Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
-      Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
-      for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
-        ArithVar x = d_instRows[ic][j];
-        if( !d_ceTableaux[ic][x].empty() ){
-          if( Debug.isOn("quant-arith-simplex") ){
-            Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
-            Debug("quant-arith-simplex") << "  ";
-            for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
-              if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
-              Debug("quant-arith-simplex") << it->first << " * " << it->second;
-            }
-            Debug("quant-arith-simplex") << " = ";
-            Node v = getTableauxValue( x, false );
-            Debug("quant-arith-simplex") << v << std::endl;
-            Debug("quant-arith-simplex") << "  term : " << d_tableaux_term[ic][x] << std::endl;
-            Debug("quant-arith-simplex") << "  ce-term : ";
-            for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
-              if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
-              Debug("quant-arith-simplex") << it->first << " * " << it->second;
-            }
-            Debug("quant-arith-simplex") << std::endl;
-          }
-          //instantiation row will be A*e + B*t = beta,
-          // where e is a vector of terms , and t is vector of ground terms.
-          // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
-          // We will construct the term ( beta - B*t)/coeff to use for e_i.
-          InstMatch m( f );
-          for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
-            if( f[0][k].getType().isInteger() ){
-              m.setValue( k, d_zero );
+    if( d_quantActive.find( f )!=d_quantActive.end() ){
+      //the point instantiation
+      InstMatch m_point( f );
+      bool m_point_valid = true;
+      int lem = 0;
+      //scan over all instantiation rows
+      for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+        Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+        Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
+        for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
+          ArithVar x = d_instRows[ic][j];
+          if( !d_ceTableaux[ic][x].empty() ){
+            if( Debug.isOn("quant-arith-simplex") ){
+              Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
+              Debug("quant-arith-simplex") << "  ";
+              for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
+                if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+                Debug("quant-arith-simplex") << it->first << " * " << it->second;
+              }
+              Debug("quant-arith-simplex") << " = ";
+              Node v = getTableauxValue( x, false );
+              Debug("quant-arith-simplex") << v << std::endl;
+              Debug("quant-arith-simplex") << "  term : " << d_tableaux_term[ic][x] << std::endl;
+              Debug("quant-arith-simplex") << "  ce-term : ";
+              for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
+                if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+                Debug("quant-arith-simplex") << it->first << " * " << it->second;
+              }
+              Debug("quant-arith-simplex") << std::endl;
             }
-          }
-          //By default, choose the first instantiation constant to be e_i.
-          Node var = d_ceTableaux[ic][x].begin()->first;
-          //if it is integer, we need to find variable with coefficent +/- 1
-          if( var.getType().isInteger() ){
-            std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
-            while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
-              ++it;
-              if( it==d_ceTableaux[ic][x].end() ){
-                var = Node::null();
-              }else{
-                var = it->first;
+            //instantiation row will be A*e + B*t = beta,
+            // where e is a vector of terms , and t is vector of ground terms.
+            // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
+            // We will construct the term ( beta - B*t)/coeff to use for e_i.
+            InstMatch m( f );
+            for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
+              if( f[0][k].getType().isInteger() ){
+                m.setValue( k, d_zero );
               }
             }
-            //Otherwise, try one that divides all ground term coefficients?
-            //  Might be futile, if rewrite ensures gcd of coeffs is 1.
-          }
-          if( !var.isNull() ){
-            //add to point instantiation if applicable
-            if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
-              Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
-              Node v = getTableauxValue( x, false );
-              if( !var.getType().isInteger() || v.getType().isInteger() ){
-                m_point.setValue( i, v );
-              }else{
-                m_point_valid = false;
+            //By default, choose the first instantiation constant to be e_i.
+            Node var = d_ceTableaux[ic][x].begin()->first;
+            //if it is integer, we need to find variable with coefficent +/- 1
+            if( var.getType().isInteger() ){
+              std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
+              while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
+                ++it;
+                if( it==d_ceTableaux[ic][x].end() ){
+                  var = Node::null();
+                }else{
+                  var = it->first;
+                }
               }
+              //Otherwise, try one that divides all ground term coefficients?
+              //  Might be futile, if rewrite ensures gcd of coeffs is 1.
             }
-            Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
-            if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
-              lem++;
+            if( !var.isNull() ){
+              //add to point instantiation if applicable
+              if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
+                Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
+                Node v = getTableauxValue( x, false );
+                if( !var.getType().isInteger() || v.getType().isInteger() ){
+                  m_point.setValue( i, v );
+                }else{
+                  m_point_valid = false;
+                }
+              }
+              Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
+              if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
+                lem++;
+              }
+            }else{
+              Debug("quant-arith-simplex") << "Could not find var." << std::endl;
             }
-          }else{
-            Debug("quant-arith-simplex") << "Could not find var." << std::endl;
           }
         }
       }
-    }
-    if( lem==0 && m_point_valid ){
-      if( d_quantEngine->addInstantiation( f, m_point ) ){
-        Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
+      if( lem==0 && m_point_valid ){
+        if( d_quantEngine->addInstantiation( f, m_point ) ){
+          Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
+        }
       }
     }
   }
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index bfc0501dc..72ab5d247 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -38,12 +38,11 @@ namespace quantifiers {
 
 
 class InstStrategySimplex : public InstStrategy{
-protected:
-  /** calculate if we should process this quantifier */
-  bool calculateShouldProcess( Node f );
 private:
   /** reference to theory arithmetic */
   arith::TheoryArith* d_th;
+  /** quantifiers we should process */
+  std::map< Node, bool > d_quantActive;
   /** delta */
   std::map< TypeNode, Node > d_deltas;
   /** for each quantifier, simplex rows */
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index fd5a3609f..249b71130 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -31,13 +31,12 @@ 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
+//3 :
 //4 :
 //5 : full saturate quantifiers
 
 
 //#define MULTI_TRIGGER_FULL_EFFORT_HALF
-#define MULTI_MULTI_TRIGGERS
 
 struct sortQuantifiersForSymbol {
   QuantifiersEngine* d_qe;
@@ -134,23 +133,32 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
   }
 }
 
-InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt,  int rgfr ) :
-                                                          InstStrategy( qe ), d_tr_strategy( tstrt ){
-  if( rgfr<0 ){
-    d_regenerate = false;
+InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){
+  //how to select trigger terms
+  if( options::triggerSelMode()==TRIGGER_SEL_MIN ){
+    d_tr_strategy = Trigger::TS_MIN_TRIGGER;
+  }else if( options::triggerSelMode()==TRIGGER_SEL_MAX ){
+    d_tr_strategy = Trigger::TS_MAX_TRIGGER;
   }else{
-    d_regenerate_frequency = rgfr;
+    d_tr_strategy = Trigger::TS_ALL;
+  }
+  //whether to select new triggers during the search
+  if( options::incrementTriggers() ){
+    d_regenerate_frequency = 3;
     d_regenerate = true;
+  }else{
+    d_regenerate = false;
   }
-  d_generate_additional = true;
 }
 
 void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
   //reset triggers
-  for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){
-    for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
-      itt->first->resetInstantiationRound();
-      itt->first->reset( Node::null() );
+  for( unsigned r=0; r<2; r++ ){
+    for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger[r].begin(); it != d_auto_gen_trigger[r].end(); ++it ){
+      for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
+        itt->first->resetInstantiationRound();
+        itt->first->reset( Node::null() );
+      }
     }
   }
   d_processed_trigger.clear();
@@ -180,7 +188,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
       }
       if( gen ){
         generateTriggers( f, effort, e, status );
-        if( d_auto_gen_trigger[f].empty() && f.getNumChildren()==2 ){
+        if( d_counter[f]==0 && d_auto_gen_trigger[0][f].empty() && d_auto_gen_trigger[1][f].empty() && f.getNumChildren()==2 ){
           Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
         }
       }
@@ -189,29 +197,32 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
       //  d_processed_trigger.clear();
       //  d_quantEngine->getEqualityQuery()->setLiberal( true );
       //}
-      for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){
-        Trigger* tr = itt->first;
-        if( tr ){
-          bool processTrigger = itt->second;
-          if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){
-            d_processed_trigger[f][tr] = true;
-            Trace("process-trigger") << "  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;
-            if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
-              d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;
-            }else{
+      bool hasInst = false;
+      for( unsigned r=0; r<2; r++ ){
+        for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[r][f].begin(); itt != d_auto_gen_trigger[r][f].end(); ++itt ){
+          Trigger* tr = itt->first;
+          if( tr ){
+            bool processTrigger = itt->second;
+            if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){
+              d_processed_trigger[f][tr] = true;
+              Trace("process-trigger") << "  Process ";
+              tr->debugPrint("process-trigger");
+              Trace("process-trigger") << "..." << std::endl;
+              InstMatch baseMatch( f );
+              int numInst = tr->addInstantiations( baseMatch );
+              hasInst = numInst>0 || hasInst;
+              Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
               d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;
+              if( r==1 ){
+                d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+              }
+              //d_quantEngine->d_hasInstantiated[f] = true;
             }
-            if( tr->isMultiTrigger() ){
-              d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
-            }
-            //d_quantEngine->d_hasInstantiated[f] = true;
           }
         }
+        if( hasInst && options::multiTriggerPriority() ){
+          break;
+        }
       }
       //if( e==4 ){
       //  d_quantEngine->getEqualityQuery()->setLiberal( false );
@@ -272,110 +283,101 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
     Trace("auto-gen-trigger") << std::endl;
   }
 
-  //populate candidate pattern term vector for the current trigger
-  std::vector< Node > patTerms;
-  //try to add single triggers first
-  for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
-    if( d_single_trigger_gen.find( d_patTerms[0][f][i] )==d_single_trigger_gen.end() ){
-      patTerms.push_back( d_patTerms[0][f][i] );
-    }
-  }
-  //if no single triggers exist, add multi trigger terms
-  if( patTerms.empty() && ( options::multiTriggerWhenSingle() || d_single_trigger_gen.empty() ) ){
-    patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
-  }
-
-  if( !patTerms.empty() ){
-    Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
-    //sort terms based on relevance
-    if( options::relevantTriggers() ){
-      sortQuantifiersForSymbol sqfs;
-      sqfs.d_qe = d_quantEngine;
-      //sort based on # occurrences (this will cause Trigger to select rarer symbols)
-      std::sort( patTerms.begin(), patTerms.end(), sqfs );
-      Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
-      for( int i=0; i<(int)patTerms.size(); i++ ){
-        Debug("relevant-trigger") << "   " << patTerms[i] << " (";
-        Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
+  unsigned rmin = d_patTerms[0][f].empty() ? 1 : 0;
+  unsigned rmax = ( options::multiTriggerWhenSingle() || e>2 ) ? 1 : rmin;
+  for( unsigned r=rmin; r<=rmax; r++ ){
+    std::vector< Node > patTerms;
+    for( int i=0; i<(int)d_patTerms[r][f].size(); i++ ){
+      if( r==1 || d_single_trigger_gen.find( d_patTerms[r][f][i] )==d_single_trigger_gen.end() ){
+        patTerms.push_back( d_patTerms[r][f][i] );
       }
-      //Notice() << "Terms based on relevance: " << std::endl;
-      //for( int i=0; i<(int)patTerms.size(); i++ ){
-      //  Notice() << "   " << patTerms[i] << " (";
-      //  Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
-      //}
     }
-    //now, generate the trigger...
-    int matchOption = 0;
-    Trigger* tr = NULL;
-    if( d_is_single_trigger[ patTerms[0] ] ){
-      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() );
-      d_single_trigger_gen[ patTerms[0] ] = true;
-    }else{
-      //only generate multi trigger if effort level > 5, or if no single triggers exist
-      if( !d_patTerms[0][f].empty() ){
-        if( e<=5 ){
-          status = STATUS_UNFINISHED;
-          return;
-        }else{
-          Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl;
+    if( !patTerms.empty() ){
+      Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
+      //sort terms based on relevance
+      if( options::relevantTriggers() ){
+        sortQuantifiersForSymbol sqfs;
+        sqfs.d_qe = d_quantEngine;
+        //sort based on # occurrences (this will cause Trigger to select rarer symbols)
+        std::sort( patTerms.begin(), patTerms.end(), sqfs );
+        Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
+        for( int i=0; i<(int)patTerms.size(); i++ ){
+          Debug("relevant-trigger") << "   " << patTerms[i] << " (";
+          Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
         }
       }
-      //if we are re-generating triggers, shuffle based on some method
-      if( d_made_multi_trigger[f] ){
-#ifndef MULTI_MULTI_TRIGGERS
-        return;
-#endif
-        std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
+      //now, generate the trigger...
+      int matchOption = 0;
+      Trigger* tr = NULL;
+      if( d_is_single_trigger[ patTerms[0] ] ){
+        tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() );
+        d_single_trigger_gen[ patTerms[0] ] = true;
       }else{
-        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() );
-    }
-    if( tr ){
-      if( tr->isMultiTrigger() ){
-        //disable all other multi triggers
-        for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){
-          if( it->first->isMultiTrigger() ){
-            d_auto_gen_trigger[f][ it->first ] = false;
+        //only generate multi trigger if effort level > 5, or if no single triggers exist
+        if( !d_patTerms[0][f].empty() ){
+          if( e<=5 && !options::multiTriggerWhenSingle() ){
+            status = STATUS_UNFINISHED;
+            return;
+          }else{
+            Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl;
           }
         }
+        //if we are re-generating triggers, shuffle based on some method
+        if( d_made_multi_trigger[f] ){
+          std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
+        }else{
+          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() );
       }
-      //making it during an instantiation round, so must reset
-      if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){
-        tr->resetInstantiationRound();
-        tr->reset( Node::null() );
-      }
-      d_auto_gen_trigger[f][tr] = true;
-      //if we are generating additional triggers...
-      if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){
-        int index = 0;
-        if( index<(int)patTerms.size() ){
-          //Notice() << "check add additional" << std::endl;
-          //check if similar patterns exist, and if so, add them additionally
-          int nqfs_curr = 0;
-          if( options::relevantTriggers() ){
-            nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
+      if( tr ){
+        unsigned tindex;
+        if( tr->isMultiTrigger() ){
+          //disable all other multi triggers
+          for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][f].begin(); it != d_auto_gen_trigger[1][f].end(); ++it ){
+            d_auto_gen_trigger[1][f][ it->first ] = false;
           }
-          index++;
-          bool success = true;
-          while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
-            success = false;
-            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() );
-              if( tr2 ){
-                //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
-                tr2->resetInstantiationRound();
-                tr2->reset( Node::null() );
-                d_auto_gen_trigger[f][tr2] = true;
-              }
-              success = true;
+          tindex = 1;
+        }else{
+          tindex = 0;
+        }
+        //making it during an instantiation round, so must reset
+        if( d_auto_gen_trigger[tindex][f].find( tr )==d_auto_gen_trigger[tindex][f].end() ){
+          tr->resetInstantiationRound();
+          tr->reset( Node::null() );
+        }
+        d_auto_gen_trigger[tindex][f][tr] = true;
+        //if we are generating additional triggers...
+        if( tindex==0 ){
+          int index = 0;
+          if( index<(int)patTerms.size() ){
+            //Notice() << "check add additional" << std::endl;
+            //check if similar patterns exist, and if so, add them additionally
+            int nqfs_curr = 0;
+            if( options::relevantTriggers() ){
+              nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
             }
             index++;
+            bool success = true;
+            while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
+              success = false;
+              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() );
+                if( tr2 ){
+                  //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
+                  tr2->resetInstantiationRound();
+                  tr2->reset( Node::null() );
+                  d_auto_gen_trigger[0][f][tr2] = true;
+                }
+                success = true;
+              }
+              index++;
+            }
+            //Notice() << "done check add additional" << std::endl;
           }
-          //Notice() << "done check add additional" << std::endl;
         }
       }
     }
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index d2c611d34..f630a0830 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -70,10 +70,8 @@ private:
   /** regeneration */
   bool d_regenerate;
   int d_regenerate_frequency;
-  /** generate additional triggers */
-  bool d_generate_additional;
-  /** triggers for each quantifier */
-  std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;
+  /** (single,multi) triggers for each quantifier */
+  std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger[2];
   std::map< Node, int > d_counter;
   /** single, multi triggers for each quantifier */
   std::map< Node, std::vector< Node > > d_patTerms[2];
@@ -89,16 +87,14 @@ private:
   void processResetInstantiationRound( Theory::Effort effort );
   int process( Node f, Theory::Effort effort, int e );
   /** generate triggers */
-  void generateTriggers( Node f, Theory::Effort effort, int e, int & status );
+  void generateTriggers( Node f, Theory::Effort effort, int e, int& status );
+  //bool addTrigger( inst::Trigger * tr, Node f, unsigned r );
   /** has user patterns */
   bool hasUserPatterns( Node f );
   /** has user patterns */
   std::map< Node, bool > d_hasUserPatterns;
 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 );
   ~InstStrategyAutoGenTriggers(){}
 public:
   /** get auto-generated trigger */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 518921433..52139a0b8 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -46,36 +46,30 @@ InstantiationEngine::~InstantiationEngine() {
 void InstantiationEngine::finishInit(){
   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 );
       d_instStrategies.push_back( d_isup );
     }
-    
+
     //auto-generated patterns
-    int tstrt = Trigger::TS_ALL;
-    if( options::triggerSelMode()==TRIGGER_SEL_MIN ){
-      tstrt = Trigger::TS_MIN_TRIGGER;
-    }else if( options::triggerSelMode()==TRIGGER_SEL_MAX ){
-      tstrt = Trigger::TS_MAX_TRIGGER;
-    }
-    d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, tstrt, 3 );
+    d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine );
     d_instStrategies.push_back( d_i_ag );
   }
-  
+
   //local theory extensions TODO?
   //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() ){
     d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
@@ -117,11 +111,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
     }
   }
   //if not, proceed to instantiation round
-  Debug("inst-engine") << "IE: Instantiation Round." << std::endl;
-  Debug("inst-engine-ctrl") << "IE: Instantiation Round." << std::endl;
-  //reset the quantifiers engine
-  Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
-  //reset the instantiators
+  //reset the instantiation strategies
   for( size_t i=0; i<d_instStrategies.size(); ++i ){
     InstStrategy* is = d_instStrategies[i];
     is->processResetInstantiationRound( effort );
@@ -146,13 +136,11 @@ 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( 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;
-              if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
-                finished = false;
-              }
+            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;
+            if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
+              finished = false;
             }
           }
         }
@@ -164,14 +152,10 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
     }
     e++;
   }
-  Debug("inst-engine") << "All instantiators finished, # added lemmas = ";
-  Debug("inst-engine") << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
   //Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
   if( !d_quantEngine->hasAddedLemma() ){
-    Debug("inst-engine-ctrl") << "---Fail." << std::endl;
     return false;
   }else{
-    Debug("inst-engine-ctrl") << "---Done. " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting) << std::endl;
     Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting)  << std::endl;
     return true;
   }
@@ -433,7 +417,6 @@ void InstantiationEngine::addUserNoPattern( Node f, Node pat ){
 InstantiationEngine::Statistics::Statistics():
   d_instantiations_user_patterns("InstantiationEngine::Instantiations_User_Patterns", 0),
   d_instantiations_auto_gen("InstantiationEngine::Instantiations_Auto_Gen", 0),
-  d_instantiations_auto_gen_min("InstantiationEngine::Instantiations_Auto_Gen_Min", 0),
   d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0),
   d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
   d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
@@ -443,7 +426,6 @@ InstantiationEngine::Statistics::Statistics():
 {
   StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
   StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
-  StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min);
   StatisticsRegistry::registerStat(&d_instantiations_guess);
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
@@ -455,7 +437,6 @@ InstantiationEngine::Statistics::Statistics():
 InstantiationEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
   StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
-  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min);
   StatisticsRegistry::unregisterStat(&d_instantiations_guess);
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 2d427ae0a..c69136933 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -40,21 +40,9 @@ public:
 protected:
   /** reference to the instantiation engine */
   QuantifiersEngine* d_quantEngine;
-  /** should process a quantifier */
-  std::map< Node, bool > d_quantActive;
-  /** calculate should process */
-  virtual bool calculateShouldProcess( Node f ) { return true; }
 public:
   InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
   virtual ~InstStrategy(){}
-
-  /** should process quantified formula f? */
-  bool shouldProcess( Node f ) {
-    if( d_quantActive.find( f )==d_quantActive.end() ){
-      d_quantActive[f] = calculateShouldProcess( f );
-    }
-    return d_quantActive[f];
-  }
   /** reset instantiation */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   /** process method, returns a status */
@@ -131,7 +119,6 @@ public:
   public:
     IntStat d_instantiations_user_patterns;
     IntStat d_instantiations_auto_gen;
-    IntStat d_instantiations_auto_gen_min;
     IntStat d_instantiations_guess;
     IntStat d_instantiations_cbqi_arith;
     IntStat d_instantiations_cbqi_arith_minus;
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 793e4a611..b03c4ad3b 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -7,7 +7,7 @@
 theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
 typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
 
-properties check propagate presolve getNextDecisionRequest
+properties check presolve getNextDecisionRequest
 
 rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"
 
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 214f3974e..a7440639b 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -5,25 +5,21 @@
 
 module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers
 
-option eMatching --e-matching bool :read-write :default true
- whether to do heuristic E-matching
+#### rewriter options
 
 # 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 ) )
 option miniscopeQuant --miniscope-quant bool :default true :read-write
  disable miniscope quantifiers
-
 # Whether to mini-scope quantifiers based on formulas with no free variables.
 # For example, forall x. ( P( x ) V Q ) will be rewritten to
 # ( forall x. P( x ) ) V Q
 option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
  disable miniscope quantifiers for ground subformulas
-
 # Whether to prenex (nested universal) quantifiers
 option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
  disable prenexing of quantified formulas
-
 # Whether to variable-eliminate quantifiers.
 # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
 #   forall y. P( c, y )
@@ -31,22 +27,18 @@ option varElimQuant --var-elim-quant bool :default true
  disable simple variable elimination for quantified formulas
 option dtVarExpandQuant --dt-var-exp-quant bool :default true
  expand datatype variables bound to one constructor in quantifiers
-
 option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
  split variables occurring as conditions of ITE in quantifiers
 option simpleIteLiftQuant --ite-lift-quant bool :default true
  disable simple ite lifting for quantified formulas
-
 # Whether to CNF quantifier bodies
 option cnfQuant --cnf-quant bool :default false
  apply CNF conversion to quantified formulas
 # Whether to NNF quantifier bodies
 option nnfQuant --nnf-quant bool :default true
  apply NNF conversion to quantified formulas
-
 option clauseSplit --clause-split bool :default false
  apply clause splitting to quantified formulas
-
 # Whether to pre-skolemize quantifier bodies.
 # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
 #   forall x. P( x ) => f( S( x ) ) = x
@@ -62,8 +54,17 @@ option macrosQuant --macros-quant bool :default false
 option foPropQuant --fo-prop-quant bool :default false
  perform first-order propagation on quantifiers
 
+#### E-matching options
+ 
+option eMatching --e-matching bool :read-write :default true
+ whether to do heuristic E-matching
+ 
 option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler  CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h"
  which ground terms to consider for instantiation
+# Whether to consider terms in the bodies of quantifiers for matching
+option registerQuantBodyTerms --register-quant-body-terms bool :default false
+ consider ground terms within bodies of quantified formulas for matching
+ 
 # Whether to use smart triggers
 option smartTriggers --smart-triggers bool :default true
  disable smart triggers
@@ -78,57 +79,51 @@ option purifyDtTriggers --purify-dt-triggers bool :default false :read-write
  purify dt triggers, match all constructors of correct form instead of selectors
 option pureThTriggers --pure-th-triggers bool :default false :read-write
  use pure theory terms as single triggers
-option multiTriggerWhenSingle --multi-trigger-when-single bool :default true
- never select multi-triggers when single triggers exist
+option multiTriggerWhenSingle --multi-trigger-when-single bool :default false
+ select multi triggers when single triggers exist
+option multiTriggerPriority --multi-trigger-priority bool :default false
+ only try multi triggers if single triggers give no instantiations
 option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler  CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h"
  selection mode for triggers
-
-option quantFunWellDefined --quant-fun-wd bool :default false
- assume that function defined by quantifiers are well defined
-option fmfFunWellDefined --fmf-fun bool :default false
- find models for finite runs of defined functions, assumes functions are well-defined
+option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h"
+ policy for handling user-provided patterns for quantifier instantiation
  
-# Whether to consider terms in the bodies of quantifiers for matching
-option registerQuantBodyTerms --register-quant-body-terms bool :default false
- consider ground terms within bodies of quantified formulas for matching
-
 option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :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 :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
-
+option internalReps --quant-internal-reps bool :default true
+ instantiate with representatives chosen by quantifiers engine
+ 
+option incrementTriggers --increment-triggers bool :default true
+ generate additional triggers as needed during search
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
 
-option instNoEntail --inst-no-entail bool :read-write :default false
- do not consider instances of quantified formulas that are currently entailed
-
 option fullSaturateQuant --full-saturate-quant bool :default false
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
 
 option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose literal matching mode
 
-option cbqi --enable-cbqi bool :read-write :default false
- turns on counterexample-based quantifier instantiation
-
-option recurseCbqi --cbqi-recurse bool :default false
- turns on recursive counterexample-based quantifier instantiation
-
-option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h"
- policy for handling user-provided patterns for quantifier instantiation
-
-option flipDecision --flip-decision/ bool :default false
- turns on flip decision heuristic
-
-option internalReps --quant-internal-reps bool :default true
- disables instantiating with representatives chosen by quantifiers engine
+option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
+ policy for instantiating axioms
 
+ 
+### finite model finding options
+ 
 option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
  use finite model finding heuristic for quantifier instantiation
 
+option quantFunWellDefined --quant-fun-wd bool :default false
+ assume that function defined by quantifiers are well defined
+option fmfFunWellDefined --fmf-fun bool :default false
+ find models for finite runs of defined functions, assumes functions are well-defined
+ 
 option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose mode for model-based quantifier instantiation
 option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false
@@ -150,10 +145,9 @@ option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
  finite model finding on bounded integer quantification
 option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write
  enforce bounds for bounded integer quantification lazily via use of proxy variables
-
-option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
- policy for instantiating axioms
-
+ 
+### conflict-based instantiation options 
+ 
 option quantConflictFind --quant-cf bool :read-write :default true
  enable conflict find mechanism for quantifiers
 option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h"
@@ -163,11 +157,18 @@ option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :
 option qcfTConstraint --qcf-tconstraint bool :read-write :default false
  enable entailment checks for t-constraints in qcf algorithm
 
+option instNoEntail --inst-no-entail bool :read-write :default true
+ do not consider instances of quantified formulas that are currently entailed
+ 
+### rewrite rules options 
+ 
 option quantRewriteRules --rewrite-rules bool :default true
  use rewrite rules module
 option rrOneInstPerRound --rr-one-inst-per-round bool :default false
  add one instance of rewrite rule per round
-
+ 
+### induction options 
+ 
 option quantInduction --quant-ind bool :default false
  use all available techniques for inductive reasoning
 option dtStcInduction --dt-stc-ind bool :read-write :default false
@@ -191,7 +192,9 @@ option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0
  number of ground terms to generate for model filtering
 option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
  more aggressive merging for universal equality engine, introduces terms
- 
+  
+### synthesis options 
+
 option ceGuidedInst --cegqi bool :default false :read-write
   counterexample-guided quantifier instantiation
 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"
@@ -215,6 +218,14 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true
   generalize based on arguments in global search space narrowing
 option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
   generalize based on content in global search space narrowing
+  
+# older implementation
+option cbqi --enable-cbqi bool :read-write :default false
+ turns on counterexample-based quantifier instantiation
+option recurseCbqi --cbqi-recurse bool :default false
+ turns on recursive counterexample-based quantifier instantiation
+ 
+### local theory extensions options 
 
 option localTheoryExt --local-t-ext bool :default false
   do instantiation based on local theory extensions
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index fdfad21b9..f492eb094 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -195,10 +195,10 @@ static const std::string termDbModeHelp = "\
 Modes for term database, supported by --term-db-mode:\n\
 \n\
 all  \n\
-+ Consider all terms in the system.\n\
++ Quantifiers module considers all ground terms.\n\
 \n\
 relevant \n\
-+ Consider only terms connected to current assertions. \n\
++ Quantifiers module considers only ground terms connected to current assertions. \n\
 \n\
 ";
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 1f15bb797..a78fa8d7b 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1271,8 +1271,3 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
   }
   return n;
 }
-
-bool QuantifiersRewriter::isDtStrInductionQuantifier( Node q ){
-  Assert( q.getKind()==FORALL );
-  return q[0].getNumChildren()==1 && datatypes::DatatypesRewriter::isTermDatatype( q[0][0] );
-}
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 7c57c6d60..838eff57b 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -79,8 +79,6 @@ public:
   static Node rewriteRewriteRule( Node r );
   static bool containsQuantifiers(Node n);
   static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
-private:
-  static bool isDtStrInductionQuantifier( Node q );
 };/* class QuantifiersRewriter */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 951a6b545..649d34922 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -163,10 +163,6 @@ void TheoryQuantifiers::check(Effort e) {
   getQuantifiersEngine()->check( e );
 }
 
-void TheoryQuantifiers::propagate(Effort level){
-  //getQuantifiersEngine()->propagate( level );
-}
-
 Node TheoryQuantifiers::getNextDecisionRequest(){
   return getQuantifiersEngine()->getNextDecisionRequest();
 }
@@ -185,22 +181,6 @@ void TheoryQuantifiers::assertExistential( Node n ){
   }
 }
 
-bool TheoryQuantifiers::flipDecision(){
-  //Debug("quantifiers-flip") << "No instantiation given, flip decision, level = " << d_valuation.getDecisionLevel() << std::endl;
-  //for( int i=1; i<=(int)d_valuation.getDecisionLevel(); i++ ){
-  //  Debug("quantifiers-flip") << "   " << d_valuation.getDecision( i ) << std::endl;
-  //}
-  //if( d_valuation.getDecisionLevel()>0 ){
-  //  double r = double(rand())/double(RAND_MAX);
-  //  unsigned decisionLevel = (unsigned)(r*d_valuation.getDecisionLevel());
-  //  d_out->flipDecision( decisionLevel );
-  //  return true;
-  //}else{
-  //  return false;
-  //}
-  return false;
-}
-
 void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
   QuantifiersAttributes::setUserAttribute( attr, n, node_values, str_value );
 }
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 6d3fa4d46..0f16f0e80 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -58,13 +58,11 @@ public:
   void preRegisterTerm(TNode n);
   void presolve();
   void check(Effort e);
-  void propagate(Effort level);
   Node getNextDecisionRequest();
   Node getValue(TNode n);
   void collectModelInfo( TheoryModel* m, bool fullModel );
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
-  bool flipDecision();
   void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
   eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
   bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 74a8fab73..5dc4d9408 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -417,12 +417,6 @@ void TheoryEngine::check(Theory::Effort effort) {
       if(d_logicInfo.isQuantified()) {
         // quantifiers engine must pass effort last call check
         d_quantEngine->check(Theory::EFFORT_LAST_CALL);
-        // if we have given up, then possibly flip decision
-        if(options::flipDecision()) {
-          if(d_incomplete && !d_inConflict && !needCheck()) {
-            ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision();
-          }
-        }
         // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
       } else if(options::produceModels()) {
         // must build model at this point