New options for trigger selection, add option --strict-triggers. Do not infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.

17 files changed, 126 insertions, 98 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 90202d6f5..d08f5f533 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -347,15 +347,21 @@ interleave \n\
 const std::string OptionsHandler::s_triggerSelModeHelp = "\
 Trigger selection modes currently supported by the --trigger-sel option:\n\
 \n\
-default \n\
-+ Default, consider all subterms of quantified formulas for trigger selection.\n\
-\n\
-min \n\
+min | default \n\
 + Consider only minimal subterms that meet criteria for triggers.\n\
 \n\
 max \n\
 + Consider only maximal subterms that meet criteria for triggers. \n\
 \n\
+all \n\
++ Consider all subterms that meet criteria for triggers. \n\
+\n\
+min-s-max \n\
++ Consider only minimal subterms that meet criteria for single triggers, maximal otherwise. \n\
+\n\
+min-s-all \n\
++ Consider only minimal subterms that meet criteria for single triggers, all otherwise. \n\
+\n\
 ";
 const std::string OptionsHandler::s_prenexQuantModeHelp = "\
 Prenex quantifiers modes currently supported by the --prenex-quant option:\n\
@@ -608,6 +614,10 @@ theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::
     return theory::quantifiers::TRIGGER_SEL_MIN;
   } else if(optarg == "max") {
     return theory::quantifiers::TRIGGER_SEL_MAX;
+  } else if(optarg == "min-s-max") {
+    return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX;
+  } else if(optarg == "min-s-all") {
+    return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL;
   } else if(optarg == "all") {
     return theory::quantifiers::TRIGGER_SEL_ALL;
   } else if(optarg ==  "help") {
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 8ecf65a33..a437cfc97 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -107,6 +107,10 @@ enum TriggerSelMode {
   TRIGGER_SEL_MIN,
   /** only consider maximal terms for triggers */
   TRIGGER_SEL_MAX,
+  /** consider minimal terms for single triggers, maximal for non-single */
+  TRIGGER_SEL_MIN_SINGLE_MAX,
+  /** consider minimal terms for single triggers, all for non-single */
+  TRIGGER_SEL_MIN_SINGLE_ALL,
   /** consider all terms for triggers */
   TRIGGER_SEL_ALL,
 };
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 5f23a02e0..8ed4f24c0 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -69,8 +69,8 @@ option inferArithTriggerEq --infer-arith-trigger-eq bool :default false
 option inferArithTriggerEqExp --infer-arith-trigger-eq-exp bool :default false
  record explanations for inferArithTriggerEq
  
-option smartTriggers --smart-triggers bool :default true
- enable smart triggers
+option strictTriggers --strict-triggers bool :default false
+ only instantiate quantifiers with user patterns based on triggers
 option relevantTriggers --relevant-triggers bool :default false
  prefer triggers that are more relevant based on SInE style analysis
 option relationalTriggers --relational-triggers bool :default false
@@ -89,7 +89,7 @@ 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 "options/quantifiers_modes.h" :handler  stringToTriggerSelMode
  selection mode for triggers
-option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "options/quantifiers_modes.h" :handler stringToUserPatMode
+option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :read-write :include "options/quantifiers_modes.h" :handler stringToUserPatMode
  policy for handling user-provided patterns for quantifier instantiation
 option incrementTriggers --increment-triggers bool :default true
  generate additional triggers as needed during search
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ddbb9eef7..bff8e187f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1846,6 +1846,11 @@ void SmtEngine::setDefaults() {
     }
   }
   //implied options...
+  if( options::strictTriggers() ){
+    if( !options::userPatternsQuant.wasSetByUser() ){
+      options::userPatternsQuant.set( quantifiers::USER_PAT_MODE_TRUST );
+    }
+  }
   if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 16a9d3bc7..8abc3f65a 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -54,12 +54,17 @@ bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE
     aen->d_quant = q;
     return true;
   }else{
-    //lemma ( q <=> d_quant )
-    Trace("quant-ae") << "Alpha equivalent : " << std::endl;
-    Trace("quant-ae") << "  " << q << std::endl;
-    Trace("quant-ae") << "  " << aen->d_quant << std::endl;
-    qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) );
-    return false;
+    if( q.getNumChildren()==2 ){
+      //lemma ( q <=> d_quant )
+      Trace("quant-ae") << "Alpha equivalent : " << std::endl;
+      Trace("quant-ae") << "  " << q << std::endl;
+      Trace("quant-ae") << "  " << aen->d_quant << std::endl;
+      qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) );
+      return false;
+    }else{
+      //do not reduce annotated quantified formulas based on alpha equivalence 
+      return true;
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index d43d7a792..491da7116 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -13,8 +13,6 @@
  **/
 
 #include "theory/quantifiers/inst_strategy_e_matching.h"
-
-#include "options/quantifiers_options.h"
 #include "theory/quantifiers/inst_match_generator.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/term_database.h"
@@ -85,7 +83,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
       if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT  ){
         int matchOption = 0;
         for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){
-          Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], matchOption, true, Trigger::TR_RETURN_NULL, options::smartTriggers() );
+          Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], matchOption, true, Trigger::TR_RETURN_NULL );
           if( t ){
             d_user_gen[f].push_back( t );
           }
@@ -134,19 +132,17 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
     if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
       d_user_gen_wait[q].push_back( nodes );
     }else{
-      d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) );
+      d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW ) );
     }
   }
 }
 
 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){
   //how to select trigger terms
-  if( options::triggerSelMode()==TRIGGER_SEL_MIN || options::triggerSelMode()==TRIGGER_SEL_DEFAULT ){
-    d_tr_strategy = Trigger::TS_MIN_TRIGGER;
-  }else if( options::triggerSelMode()==TRIGGER_SEL_MAX ){
-    d_tr_strategy = Trigger::TS_MAX_TRIGGER;
+  if( options::triggerSelMode()==quantifiers::TRIGGER_SEL_DEFAULT ){
+    d_tr_strategy = quantifiers::TRIGGER_SEL_MIN;
   }else{
-    d_tr_strategy = Trigger::TS_ALL;
+    d_tr_strategy = options::triggerSelMode();
   }
   //whether to select new triggers during the search
   if( options::incrementTriggers() ){
@@ -358,7 +354,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       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() );
+        tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL );
         d_single_trigger_gen[ patTerms[0] ] = true;
       }else{
         //only generate multi trigger if option set, or if no single triggers exist
@@ -376,7 +372,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
           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 );
       }
       if( tr ){
         unsigned tindex;
@@ -412,7 +408,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
               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 );
                 if( tr2 ){
                   //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
                   tr2->resetInstantiationRound();
@@ -484,7 +480,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
       }
       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() );
+      Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD );
       d_lte_trigger[f] = tr;
     }else{
       Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index ac4eb9d98..d48084514 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/trigger.h"
 #include "theory/quantifiers_engine.h"
 #include "util/statistics_registry.h"
+#include "options/quantifiers_options.h"
 
 namespace CVC4 {
 namespace theory {
@@ -64,7 +65,7 @@ public:
   };
 private:
   /** trigger generation strategy */
-  int d_tr_strategy;
+  TriggerSelMode d_tr_strategy;
   /** regeneration */
   bool d_regenerate;
   int d_regenerate_frequency;
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index f98ab2b7c..8e88d3434 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -165,6 +165,22 @@ bool InstantiationEngine::isIncomplete( Node q ) {
   return true;
 }
 
+void InstantiationEngine::preRegisterQuantifier( Node q ) {
+  if( options::strictTriggers() && q.getNumChildren()==3 ){
+    //if strict triggers, take ownership of this quantified formula
+    bool hasPat = false;
+    for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+      if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN  ){
+        hasPat = true;
+        break;
+      }
+    }
+    if( hasPat ){
+      d_quantEngine->setOwner( q, this, 1 );
+    }
+  }
+}
+
 void InstantiationEngine::registerQuantifier( Node f ){
   if( d_quantEngine->hasOwnership( f, this ) ){
     //for( unsigned i=0; i<d_instStrategies.size(); ++i ){
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 5aab6ece0..4d1d4a20f 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -79,6 +79,7 @@ public:
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();
+  void preRegisterQuantifier( Node q );
   void registerQuantifier( Node q );
   Node explain(TNode n){ return Node::null(); }
   /** add user pattern */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index cfd1edd1f..bcd36f37a 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -660,7 +660,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
       //if applicable, try to add exceptions here
       if( !tr_terms.empty() ){
         //make a trigger for these terms, add instantiations
-        inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, 0, true, inst::Trigger::TR_MAKE_NEW, options::smartTriggers() );
+        inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, 0, true, inst::Trigger::TR_MAKE_NEW );
         //Notice() << "Trigger = " << (*tr) << std::endl;
         tr->resetInstantiationRound();
         tr->reset( Node::null() );
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index cc5a31aa8..79c300401 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -231,6 +231,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
   RewriteStatus status = REWRITE_DONE;
   Node ret = in;
+  int rew_op = -1;
   //get the body
   if( in.getKind()==EXISTS ){
     std::vector< Node > children;
@@ -251,6 +252,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
         if( doOperation( in, op, qa ) ){
           ret = computeOperation( in, op, qa );
           if( ret!=in ){
+            rew_op = op;
             status = REWRITE_AGAIN_FULL;
             break;
           }
@@ -260,7 +262,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   }
   //print if changed
   if( in!=ret ){
-    Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
+    Trace("quantifiers-rewrite") << "*** rewrite (op=" << rew_op << ") " << in << std::endl;
     Trace("quantifiers-rewrite") << " to " << std::endl;
     Trace("quantifiers-rewrite") << ret << std::endl;
   }
@@ -1537,8 +1539,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
   return mkForAll( args, body, qa );
 }
 
-bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& qa ){
-  bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef();
+bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){
+  bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant()==USER_PAT_MODE_TRUST;
+  bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef() && !is_strict_trigger;
   if( computeOption==COMPUTE_ELIM_SYMBOLS ){
     return true;
   }else if( computeOption==COMPUTE_MINISCOPING ){
@@ -1551,15 +1554,15 @@ bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& q
     return true;
     //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
   }else if( computeOption==COMPUTE_COND_SPLIT ){
-    return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && is_std;
+    return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger;
   }else if( computeOption==COMPUTE_PRENEX ){
-    return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
+    return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std;
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std;
   //}else if( computeOption==COMPUTE_CNF ){
   //  return options::cnfQuant();
   }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
-    return options::purifyQuant();
+    return options::purifyQuant() && is_std;
   }else{
     return false;
   }
@@ -1617,7 +1620,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
       std::vector< Node > children;
       children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
       children.push_back( n );
-      if( !qa.d_ipl.isNull() ){
+      if( !qa.d_ipl.isNull() && args.size()==f[0].getNumChildren() ){
         children.push_back( qa.d_ipl );
       }
       return NodeManager::currentNM()->mkNode(kind::FORALL, children );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 372aefaf4..5d20a7048 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1945,7 +1945,7 @@ void TermDb::computeAttributes( Node q ) {
       Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl;
     }
     //set rewrite engine as owner
-    d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() );
+    d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine(), 2 );
   }
   if( d_qattr[q].isFunDef() ){
     Node f = d_qattr[q].d_fundef_f;
@@ -1954,19 +1954,19 @@ void TermDb::computeAttributes( Node q ) {
       exit( 1 );
     }
     d_fun_defs[f] = true;
-    d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() );
+    d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 );
   }
   if( d_qattr[q].d_sygus ){
     if( d_quantEngine->getCegInstantiation()==NULL ){
       Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
     }
-    d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+    d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 );
   }
   if( d_qattr[q].d_synthesis ){
     if( d_quantEngine->getCegInstantiation()==NULL ){
       Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
     }
-    d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+    d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 );
   }
 }
 
@@ -1976,7 +1976,9 @@ void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){
     qa.d_ipl = q[2];
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
       Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl;
-      if( q[2][i].getKind()==INST_ATTRIBUTE ){
+      if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN ){
+        qa.d_hasPattern = true;
+      }else if( q[2][i].getKind()==INST_ATTRIBUTE ){
         Node avar = q[2][i][0];
         if( avar.getAttribute(AxiomAttribute()) ){
           Trace("quant-attr") << "Attribute : axiom : " << q << std::endl;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 15be94fe2..4cba619a8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -138,9 +138,10 @@ public:
 
 class QAttributes{
 public:
-  QAttributes() : d_conjecture(false), d_axiom(false), d_sygus(false),
+  QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
                   d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
   ~QAttributes(){}
+  bool d_hasPattern;
   Node d_rr;
   bool d_conjecture;
   bool d_axiom;
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 0ecb6dc83..b4e00386a 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -13,8 +13,6 @@
  **/
 
 #include "theory/quantifiers/trigger.h"
-
-#include "options/quantifiers_options.h"
 #include "theory/quantifiers/candidate_generator.h"
 #include "theory/quantifiers/inst_match_generator.h"
 #include "theory/quantifiers/term_database.h"
@@ -33,33 +31,25 @@ namespace theory {
 namespace inst {
 
 /** trigger class constructor */
-Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
-                  int matchOption, bool smartTriggers )
+Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption )
     : d_quantEngine( qe ), d_f( f )
 {
   d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
   Trace("trigger") << "Trigger for " << f << ": " << std::endl;
-  for( int i=0; i<(int)d_nodes.size(); i++ ){
+  for( unsigned i=0; i<d_nodes.size(); i++ ){
     Trace("trigger") << "   " << d_nodes[i] << std::endl;
   }
-  Trace("trigger-debug") << ", smart triggers = " << smartTriggers;
-  Trace("trigger") << std::endl;
-  if( smartTriggers ){
-    if( d_nodes.size()==1 ){
-      if( isSimpleTrigger( d_nodes[0] ) ){
-        d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] );
-      }else{
-        d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe );
-        d_mg->setActiveAdd(true);
-      }
+  if( d_nodes.size()==1 ){
+    if( isSimpleTrigger( d_nodes[0] ) ){
+      d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] );
     }else{
-      d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
-      //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
-      //d_mg->setActiveAdd();
+      d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe );
+      d_mg->setActiveAdd(true);
     }
   }else{
-    d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes, qe );
-    d_mg->setActiveAdd(true);
+    d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
+    //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
+    //d_mg->setActiveAdd();
   }
   if( d_nodes.size()==1 ){
     if( isSimpleTrigger( d_nodes[0] ) ){
@@ -68,11 +58,10 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
       ++(qe->d_statistics.d_simple_triggers);
     }
   }else{
-    Trace("multi-trigger") << "Multi-trigger ";
-    debugPrint("multi-trigger");
-    Trace("multi-trigger") << " for " << f << std::endl;
-    //Notice() << "Multi-trigger for " << f << " : " << std::endl;
-    //Notice() << "   " << (*this) << std::endl;
+    Trace("multi-trigger") << "Trigger for " << f << ": " << std::endl;
+    for( unsigned i=0; i<d_nodes.size(); i++ ){
+      Trace("multi-trigger") << "   " << d_nodes[i] << std::endl;
+    }
     ++(qe->d_statistics.d_multi_triggers);
   }
   //Notice() << "Trigger : " << (*this) << "  for " << f << std::endl;
@@ -123,8 +112,7 @@ int Trigger::addInstantiations( InstMatch& baseMatch ){
   return addedLemmas;
 }
 
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption,
-                             bool smartTriggers ){
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption ){
   std::vector< Node > trNodes;
   if( !keepAll ){
     //only take nodes that contribute variables to the trigger when added
@@ -211,15 +199,15 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
       }
     }
   }
-  Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers );
+  Trigger* t = new Trigger( qe, f, trNodes, matchOption );
   qe->getTriggerDatabase()->addTrigger( trNodes, t );
   return t;
 }
 
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption ){
   std::vector< Node > nodes;
   nodes.push_back( n );
-  return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );
+  return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption );
 }
 
 bool Trigger::isUsable( Node n, Node q ){
@@ -360,7 +348,7 @@ bool Trigger::isSimpleTrigger( Node n ){
 
 //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
 bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, 
-                                int tstrt, std::vector< Node >& exclude, 
+                                quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
                                 std::map< Node, int >& reqPol, std::vector< Node >& added,
                                 bool pol, bool hasPol, bool epol, bool hasEPol ){
   std::map< Node, Node >::iterator itv = visited.find( n );
@@ -371,14 +359,16 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited,
     if( n.getKind()!=FORALL ){
       bool rec = true;
       Node nu;
+      bool nu_single = false;
       if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
         nu = getIsUsableTrigger( n, f, pol, hasPol );
         if( !nu.isNull() ){
           reqPol[ nu ] = hasEPol ? ( epol ? 1 : -1 ) : 0;
           visited[ nu ] = nu;
           quantifiers::TermDb::computeVarContains( nu, visited_fv[ nu ] );
+          nu_single = visited_fv[nu].size()==f[0].getNumChildren();
           retVal = true;
-          if( tstrt==TS_MAX_TRIGGER ){
+          if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
             rec = false;
           }
         }
@@ -404,7 +394,7 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited,
             }
             added.push_back( added2[i] );
           }
-          if( rm_nu && tstrt==TS_MIN_TRIGGER ){
+          if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
             visited[nu] = Node::null();
             reqPol.erase( nu );
           }else{
@@ -502,14 +492,14 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector<
   return true;
 }
 
-void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, 
+void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
                                std::map< Node, int >& reqPol, bool filterInst ){
   std::map< Node, Node > visited;
   if( filterInst ){
     //immediately do not consider any term t for which another term is an instance of t
     std::vector< Node > patTerms2;
     std::map< Node, int > reqPol2;
-    collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, reqPol2, false );
+    collectPatTerms( qe, f, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol2, false );
     std::vector< Node > temp;
     temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
     qe->getTermDatabase()->filterInstances( temp );
@@ -525,7 +515,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
       }
       Trace("trigger-filter-instance") << std::endl;
     }
-    if( tstrt==TS_ALL ){
+    if( tstrt==quantifiers::TRIGGER_SEL_ALL ){
       for( unsigned i=0; i<temp.size(); i++ ){
         reqPol[temp[i]] = reqPol2[temp[i]];
         patTerms.push_back( temp[i] );
@@ -630,7 +620,7 @@ void Trigger::getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std:
   std::map< Node, int > reqPol;
   //collect all patterns from icn
   std::vector< Node > exclude;
-  collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude, reqPol );
+  collectPatTerms( qe, f, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol );
   //collect all variables from all patterns in patTerms, add to t_vars
   for( unsigned i=0; i<patTerms.size(); i++ ){
     qe->getTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars );
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 97ed51fe0..06e9011c7 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -21,6 +21,7 @@
 
 #include "expr/node.h"
 #include "theory/quantifiers/inst_match.h"
+#include "options/quantifiers_options.h"
 
 // Forward declarations for defining the Trigger and TriggerTrie.
 namespace CVC4 {
@@ -86,20 +87,12 @@ class Trigger {
   };
   static Trigger* mkTrigger( QuantifiersEngine* qe, Node f,
                              std::vector< Node >& nodes, int matchOption = 0,
-                             bool keepAll = true, int trOption = TR_MAKE_NEW,
-                             bool smartTriggers = false );
+                             bool keepAll = true, int trOption = TR_MAKE_NEW );
   static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n,
                              int matchOption = 0, bool keepAll = true,
-                             int trOption = TR_MAKE_NEW,
-                             bool smartTriggers = false );
-  //different strategies for choosing trigger terms
-  enum {
-    TS_MAX_TRIGGER = 0,
-    TS_MIN_TRIGGER,
-    TS_ALL,
-  };
+                             int trOption = TR_MAKE_NEW );
   static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n,
-                               std::vector< Node >& patTerms, int tstrt,
+                               std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt,
                                std::vector< Node >& exclude, std::map< Node, int >& reqPol,
                                bool filterInst = false );
   /** is usable trigger */
@@ -132,8 +125,7 @@ class Trigger {
 
 private:
   /** trigger constructor */
-  Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes,
-           int matchOption = 0, bool smartTriggers = false );
+  Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0 );
 
   /** is subterm of trigger usable */
   static bool isUsable( Node n, Node q );
@@ -141,7 +133,7 @@ private:
                                   bool hasPol = false );
   /** collect all APPLY_UF pattern terms for f in n */
   static bool collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, 
-                                int tstrt, std::vector< Node >& exclude, 
+                                quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
                                 std::map< Node, int >& reqPol, std::vector< Node >& added,
                                 bool pol, bool hasPol, bool epol, bool hasEPol );
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ad226681d..1a2762409 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -315,13 +315,17 @@ QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
   }
 }
 
-void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) {
+void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) {
   QuantifiersModule * mo = getOwner( q );
   if( mo!=m ){
     if( mo!=NULL ){
-      Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << "!" << std::endl;
+      if( priority<=d_owner_priority[q] ){
+        Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << " with higher priority!" << std::endl;
+        return;
+      }
     }
     d_owner[q] = m;
+    d_owner_priority[q] = priority;
   }
 }
 
@@ -393,9 +397,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
       Trace("quant-engine-debug") << std::endl;
       Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
-      //if( d_model->getNumToReduceQuantifiers()>0 ){
-      //  Trace("quant-engine-debug") << "  # quantified formulas to reduce = " << d_model->getNumToReduceQuantifiers() << std::endl;
-      //}
       if( !d_lemmas_waiting.empty() ){
         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
       }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 83849cd60..641c7624e 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -271,11 +271,12 @@ public:  //modules
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
+  std::map< Node, int > d_owner_priority;
 public:
   /** get owner */
   QuantifiersModule * getOwner( Node q );
   /** set owner */
-  void setOwner( Node q, QuantifiersModule * m );
+  void setOwner( Node q, QuantifiersModule * m, int priority = 0 );
   /** considers */
   bool hasOwnership( Node q, QuantifiersModule * m = NULL );
 public: