Add --user-pat=interleave. Remove unused lte inst strategy.

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 414df288210ba810524cc2f2524be09046ad6709..81771c374300b2227eb089808e7c777ca8c90c7f 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -29,12 +29,13 @@ using namespace CVC4::theory::inst;
 using namespace CVC4::theory::quantifiers;
 
 //priority levels :
-//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers)
-//2 : user patterns (when user-pat=resort ), auto gen patterns (for user pattern quantifiers, when user-pat=use)
+//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={ignore,resort})
+//2 : user patterns (when user-pat=resort), auto gen patterns (for user pattern quantifiers when user-pat=use)
 //3 :
 //4 :
 //5 : full saturate quantifiers
 
+// user-pat=interleave alternates between use and resort
 
 //#define MULTI_TRIGGER_FULL_EFFORT_HALF
 
@@ -67,14 +68,14 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
   if( e==0 ){
     return STATUS_UNFINISHED;
   }else{
-    int peffort = options::userPatternsQuant()==USER_PAT_MODE_RESORT ? 2 : 1;
+    int peffort = d_quantEngine->getInstUserPatMode()==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;
-      if( options::userPatternsQuant()==USER_PAT_MODE_RESORT  ){
+      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() );
@@ -125,7 +126,7 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
     d_quantEngine->getPhaseReqTerms( f, nodes );
     //check match option
     int matchOption = 0;
-    if( options::userPatternsQuant()==USER_PAT_MODE_RESORT ){
+    if( d_quantEngine->getInstUserPatMode()==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() ) );
@@ -165,10 +166,11 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort
 }
 
 int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
-  if( hasUserPatterns( f ) && options::userPatternsQuant()==USER_PAT_MODE_TRUST ){
+  UserPatMode upMode = d_quantEngine->getInstUserPatMode();
+  if( hasUserPatterns( f ) && upMode==USER_PAT_MODE_TRUST ){
     return STATUS_UNKNOWN;
   }else{
-    int peffort = ( hasUserPatterns( f ) && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE && options::userPatternsQuant()!=USER_PAT_MODE_RESORT ) ? 2 : 1;
+    int peffort = ( hasUserPatterns( f ) && upMode!=USER_PAT_MODE_IGNORE && upMode!=USER_PAT_MODE_RESORT ) ? 2 : 1;
     if( e<peffort ){
       return STATUS_UNFINISHED;
     }else{
@@ -417,37 +419,7 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node f, Node pat ) {
   }
 }
 
-
-void InstStrategyLocalTheoryExt::processResetInstantiationRound( Theory::Effort effort ){
-  //reset triggers
-  for( std::map< Node, Trigger* >::iterator it = d_lte_trigger.begin(); it != d_lte_trigger.end(); ++it ){
-    it->second->resetInstantiationRound();
-    it->second->reset( Node::null() );
-  }
-}
-
-int InstStrategyLocalTheoryExt::process( Node f, Theory::Effort effort, int e ) {
-  if( e<3 ){
-    return STATUS_UNFINISHED;
-  }else if( e==3 ){
-    if( isLocalTheoryExt( f ) ){
-      std::map< Node, Trigger* >::iterator it = d_lte_trigger.find( f );
-      if( it!=d_lte_trigger.end() ){
-        Trigger * tr = it->second;
-        //process the trigger
-        Trace("process-trigger") << "  LTE process ";
-        tr->debugPrint("process-trigger");
-        Trace("process-trigger") << "..." << std::endl;
-        InstMatch baseMatch( f );
-        int numInst = tr->addInstantiations( baseMatch );
-        Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
-        d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_lte += numInst;
-      }
-    }
-  }
-  return STATUS_UNKNOWN;
-}
-
+/*  TODO?
 bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
   std::map< Node, bool >::iterator itq = d_quant.find( f );
   if( itq==d_quant.end() ){
@@ -483,6 +455,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
     return itq->second;
   }
 }
+*/
 
 void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
 

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index f630a0830f0350d6d61e7ef033778bf3936b67b8..02ddd233e7d13c5fad580a7ca4b30f9cfb15cd44 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -105,26 +105,6 @@ public:
   void addUserNoPattern( Node f, Node pat );
 };/* class InstStrategyAutoGenTriggers */
 
-
-class InstStrategyLocalTheoryExt : public InstStrategy {
-private:
-  /** have we registered quantifier, value is whether it is an LTE term */
-  std::map< Node, bool > d_quant;
-  /** triggers for each quantifier */
-  std::map< Node, inst::Trigger* > d_lte_trigger;
-private:
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategyLocalTheoryExt( QuantifiersEngine* qe ) : InstStrategy( qe ){}
-  /** identify */
-  std::string identify() const { return std::string("LocalTheoryExt"); }
-  /** is local theory quantifier? */
-  bool isLocalTheoryExt( Node f );
-};
-
-
 class InstStrategyFreeVariable : public InstStrategy{
 private:
   /** guessed instantiations */

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index e867aae1e0de10ffb15d4c746df6a056bcb00584..4fbf298f4f957bfa20dca9bacefc88b1c80b15d0 100644 (file)
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -31,14 +31,13 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){
 
 }
 
 InstantiationEngine::~InstantiationEngine() {
   delete d_i_ag;
   delete d_isup;
-  delete d_i_lte;
   delete d_i_fs;
   delete d_i_splx;
   delete d_i_cegqi;
@@ -59,12 +58,6 @@ void InstantiationEngine::finishInit(){
     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 );

diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index dc5b976f033f4f12853f23cd42a87a2ef31cd6d2..5d46a981585bac304eacf4421c9baddbc64a137b 100644 (file)
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -26,7 +26,6 @@ namespace quantifiers {
 
 class InstStrategyUserPatterns;
 class InstStrategyAutoGenTriggers;
-class InstStrategyLocalTheoryExt;
 class InstStrategyFreeVariable;
 class InstStrategySimplex;
 class InstStrategyCegqi;
@@ -63,8 +62,6 @@ private:
   InstStrategyUserPatterns* d_isup;
   /** auto gen triggers; only kept for destructor cleanup */
   InstStrategyAutoGenTriggers* d_i_ag;
-  /** local theory extensions */
-  InstStrategyLocalTheoryExt * d_i_lte;
   /** full saturate */
   InstStrategyFreeVariable * d_i_fs;
   /** simplex (cbqi) */

diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index d0bed023d36a42c8f4a29bb08e1bbe62f2609348..47cb62715244ffee485c74bae4ce8f17ecf7c160 100644 (file)
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -103,6 +103,8 @@ typedef enum {
   USER_PAT_MODE_RESORT,
   /** ignore user patterns */
   USER_PAT_MODE_IGNORE,
+  /** interleave use/resort for user patterns */
+  USER_PAT_MODE_INTERLEAVE,
 } UserPatMode;
 
 typedef enum {

diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index f492eb0945bd8df9a758659b6f0279c99582767f..9fb5dd69d5814c5927417debe235c78a6a21a0b7 100644 (file)
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -148,6 +148,9 @@ resort \n\
 ignore \n\
 + Ignore user-provided patterns. \n\
 \n\
+interleave \n\
++ Alternate between use/resort. \n\
+\n\
 ";
 static const std::string triggerSelModeHelp = "\
 Trigger selection modes currently supported by the --trigger-sel option:\n\
@@ -336,6 +339,8 @@ inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, S
     return USER_PAT_MODE_RESORT;
   } else if(optarg == "ignore") {
     return USER_PAT_MODE_IGNORE;
+  } else if(optarg == "interleave") {
+    return USER_PAT_MODE_INTERLEAVE;
   } else if(optarg ==  "help") {
     puts(userPatModeHelp.c_str());
     exit(1);

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a2d68f7c90c080c56c1710882ded4e039304d68d..e654a689d6b3f3d621cd1bb37449e3ef65ea6292 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -893,6 +893,14 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   return performCheck;
 }
 
+quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() {
+  if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE ){
+    return d_ierCounter%2==0 ? quantifiers::USER_PAT_MODE_USE : quantifiers::USER_PAT_MODE_RESORT;
+  }else{
+    return options::userPatternsQuant();
+  }
+}
+
 void QuantifiersEngine::flushLemmas(){
   if( !d_lemmas_waiting.empty() ){
     //take default output channel if none is provided

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index e613ef2845a7388e281f2834fc20e70b1e4f21a3..d5887f90768c3c0c53adf99f37e21f0ee71f7565 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -21,6 +21,7 @@
 #include "util/hash.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/modes.h"
 #include "expr/attribute.h"
 
 #include "util/statistics_registry.h"
@@ -284,6 +285,8 @@ public:
   int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
   /** get needs check */
   bool getInstWhenNeedsCheck( Theory::Effort e );
+  /** get user pat mode */
+  quantifiers::UserPatMode getInstUserPatMode();
   /** set instantiation level attr */
   static void setInstantiationLevelAttr( Node n, uint64_t level );
 public: