Add --user-pat=resort. Minor cleanup of options.

4 files changed, 52 insertions, 36 deletions

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 4abdb66f6..e95936220 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -59,30 +59,39 @@ void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort ef
 int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
   if( e==0 ){
     return STATUS_UNFINISHED;
-  }else if( e==1 ){
-    d_counter[f]++;
+  }else{
+    int peffort = options::userPatternsQuant()==USER_PAT_MODE_RESORT ? 2 : 1;
+    if( e<peffort ){
+      return STATUS_UNFINISHED;
+    }else if( e==peffort ){
+      d_counter[f]++;
+      
       Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl;
-
-    Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;
-    //Notice() << "Try user-provided patterns..." << std::endl;
-    for( int i=0; i<(int)d_user_gen[f].size(); i++ ){
-      bool processTrigger = true;
-      if( processTrigger ){
-        Trace("process-trigger") << "  Process (user) ";
-        d_user_gen[f][i]->debugPrint("process-trigger");
-        Trace("process-trigger") << "..." << std::endl;
-        InstMatch baseMatch( f );
-        int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
-        Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
-        d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;
-        if( d_user_gen[f][i]->isMultiTrigger() ){
-          d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+      if( options::userPatternsQuant()==USER_PAT_MODE_RESORT  ){
+        int matchOption = 0;
+        for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){
+          d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], matchOption, true, Trigger::TR_RETURN_NULL, options::smartTriggers() ) );
+        }
+        d_user_gen_wait[f].clear();
+      }
+      
+      for( unsigned i=0; i<d_user_gen[f].size(); i++ ){
+        bool processTrigger = true;
+        if( processTrigger ){
+          Trace("process-trigger") << "  Process (user) ";
+          d_user_gen[f][i]->debugPrint("process-trigger");
+          Trace("process-trigger") << "..." << std::endl;
+          InstMatch baseMatch( f );
+          int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
+          Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
+          d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;
+          if( d_user_gen[f][i]->isMultiTrigger() ){
+            d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+          }
+          //d_quantEngine->d_hasInstantiated[f] = true;
         }
-        //d_quantEngine->d_hasInstantiated[f] = true;
       }
     }
-    Debug("quant-uf-strategy") << "done." << std::endl;
-    //Notice() << "done" << std::endl;
   }
   return STATUS_UNKNOWN;
 }
@@ -106,7 +115,11 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
     d_quantEngine->getPhaseReqTerms( f, nodes );
     //check match option
     int matchOption = 0;
-    d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) );
+    if( options::userPatternsQuant()==USER_PAT_MODE_RESORT ){
+      d_user_gen_wait[f].push_back( nodes );
+    }else{
+      d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) );
+    }
   }
 }
 
@@ -136,11 +149,11 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
   if( hasUserPatterns( f ) && options::userPatternsQuant()==USER_PAT_MODE_TRUST ){
     return STATUS_UNKNOWN;
   }else{
-    int peffort = ( hasUserPatterns( f ) && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ) ? 2 : 1;
-    //int peffort = 1;
+    int peffort = ( hasUserPatterns( f ) && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE && options::userPatternsQuant()!=USER_PAT_MODE_RESORT ) ? 2 : 1;
     if( e<peffort ){
       return STATUS_UNFINISHED;
     }else{
+      Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
       int status = STATUS_UNKNOWN;
       bool gen = false;
       if( e==peffort ){
@@ -160,14 +173,11 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
           Trace("no-trigger") << "Could not find trigger for " << f << std::endl;
         }
       }
-      Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
 
       //if( e==4 ){
       //  d_processed_trigger.clear();
       //  d_quantEngine->getEqualityQuery()->setLiberal( true );
       //}
-      Debug("quant-uf-strategy")  << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;
-      //Notice() << "Try auto-generated triggers..." << std::endl;
       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 ){
@@ -195,8 +205,6 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
       //if( e==4 ){
       //  d_quantEngine->getEqualityQuery()->setLiberal( false );
       //}
-      Debug("quant-uf-strategy") << "done." << std::endl;
-      //Notice() << "done" << std::endl;
       return status;
     }
   }
@@ -281,8 +289,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
     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, options::smartTriggers() );
       d_single_trigger_gen[ patTerms[0] ] = true;
     }else{
       //only generate multi trigger if effort level > 5, or if no single triggers exist
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 935432683..dd4486803 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -36,6 +36,8 @@ class InstStrategyUserPatterns : public InstStrategy{
 private:
   /** explicitly provided patterns */
   std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
+  /** waiting to be generated patterns */
+  std::map< Node, std::vector< std::vector< Node > > > d_user_gen_wait;
   /** counter for quantifiers */
   std::map< Node, int > d_counter;
   /** process functions */
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 53842b373..acc883f2a 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -103,6 +103,8 @@ typedef enum {
   USER_PAT_MODE_USE,
   /** default, if patterns are supplied for a quantifier, use only those */
   USER_PAT_MODE_TRUST,
+  /** resort to user patterns only when necessary */
+  USER_PAT_MODE_RESORT,
   /** ignore user patterns */
   USER_PAT_MODE_IGNORE,
 } UserPatMode;
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 461dbafe9..c2afbbd3e 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -148,6 +148,9 @@ use \n\
 + Use both user-provided and auto-generated patterns when patterns\n\
   are provided for a quantified formula.\n\
 \n\
+resort \n\
++ Use user-provided patterns only after auto-generated patterns saturate.\n\
+\n\
 ignore \n\
 + Ignore user-provided patterns. \n\
 \n\
@@ -181,11 +184,11 @@ none \n\
 static const std::string cegqiFairModeHelp = "\
 Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\
 \n\
-default \n\
-+ Default, enforce fairness using an uninterpreted function for datatypes size.\n\
+uf-dt-size \n\
++ Enforce fairness using an uninterpreted function for datatypes size.\n\
 \n\
-dt-size \n\
-+ Enforce fairness using size theory operator.\n\
+default | dt-size \n\
++ Default, enforce fairness using size theory operator.\n\
 \n\
 none \n\
 + Do not enforce fairness. \n\
@@ -326,6 +329,8 @@ inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, S
     return USER_PAT_MODE_USE;
   } else if(optarg ==  "default" || optarg == "trust") {
     return USER_PAT_MODE_TRUST;
+  } else if(optarg == "resort") {
+    return USER_PAT_MODE_RESORT;
   } else if(optarg == "ignore") {
     return USER_PAT_MODE_IGNORE;
   } else if(optarg ==  "help") {
@@ -370,9 +375,9 @@ inline PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string o
 }
 
 inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "default" || optarg == "uf-dt-size" ) {
+  if(optarg == "uf-dt-size" ) {
     return CEGQI_FAIR_UF_DT_SIZE;
-  } else if(optarg == "dt-size") {
+  } else if(optarg == "default" || optarg == "dt-size") {
     return CEGQI_FAIR_DT_SIZE;
   } else if(optarg == "none") {
     return CEGQI_FAIR_NONE;