Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not drop patterns from merged prenex (fixes bug 743).

10 files changed, 109 insertions, 14 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 6a5f6cd39..8cd651da5 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -369,6 +369,19 @@ min-s-all \n\
 + Consider only minimal subterms that meet criteria for single triggers, all otherwise. \n\
 \n\
 ";
+const std::string OptionsHandler::s_triggerActiveSelModeHelp = "\
+Trigger active selection modes currently supported by the --trigger-sel option:\n\
+\n\
+all \n\
++ Make all triggers active. \n\
+\n\
+min \n\
++ Activate triggers with minimal ground terms.\n\
+\n\
+max \n\
++ Activate triggers with maximal ground terms. \n\
+\n\
+";
 const std::string OptionsHandler::s_prenexQuantModeHelp = "\
 Prenex quantifiers modes currently supported by the --prenex-quant option:\n\
 \n\
@@ -630,9 +643,7 @@ theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string
 }
 
 theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) {
-  if(optarg ==  "default") {
-    return theory::quantifiers::TRIGGER_SEL_DEFAULT;
-  } else if(optarg == "min") {
+  if(optarg ==  "default" || optarg == "min") {
     return theory::quantifiers::TRIGGER_SEL_MIN;
   } else if(optarg == "max") {
     return theory::quantifiers::TRIGGER_SEL_MAX;
@@ -651,6 +662,21 @@ theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::
   }
 }
 
+theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg ==  "default" || optarg == "all") {
+    return theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL;
+  } else if(optarg == "min") {
+    return theory::quantifiers::TRIGGER_ACTIVE_SEL_MIN;
+  } else if(optarg == "max") {
+    return theory::quantifiers::TRIGGER_ACTIVE_SEL_MAX;
+  } else if(optarg ==  "help") {
+    puts(s_triggerActiveSelModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --trigger-active-sel: `") +
+                          optarg + "'.  Try --trigger-active-sel help.");
+  }
+}
 
 theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg ==  "default" ) {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 5db2887c0..e327b9c8e 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -94,6 +94,7 @@ public:
   theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException);
+  theory::quantifiers::TriggerActiveSelMode stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException);
@@ -221,6 +222,7 @@ public:
   static const std::string s_termDbModeHelp;
   static const std::string s_theoryOfModeHelp;
   static const std::string s_triggerSelModeHelp;
+  static const std::string s_triggerActiveSelModeHelp;
   static const std::string s_ufssModeHelp;
   static const std::string s_userPatModeHelp;
   static const std::string s_errorSelectionRulesHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 65445be17..fe76f8798 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -101,8 +101,6 @@ enum UserPatMode {
 };
 
 enum TriggerSelMode {
-  /** default for trigger selection */
-  TRIGGER_SEL_DEFAULT,
   /** only consider minimal terms for triggers */
   TRIGGER_SEL_MIN,
   /** only consider maximal terms for triggers */
@@ -115,6 +113,15 @@ enum TriggerSelMode {
   TRIGGER_SEL_ALL,
 };
 
+enum TriggerActiveSelMode {
+  /** always use all triggers */
+  TRIGGER_ACTIVE_SEL_ALL,
+  /** only use triggers with minimal # of ground terms */
+  TRIGGER_ACTIVE_SEL_MIN,
+  /** only use triggers with maximal # of ground terms */
+  TRIGGER_ACTIVE_SEL_MAX,
+};
+
 enum CVC4_PUBLIC PrenexQuantMode {
   /** default : prenex quantifiers without user patterns */
   PRENEX_NO_USER_PAT,
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 980179378..0b5474959 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -89,8 +89,10 @@ 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 "options/quantifiers_modes.h" :handler  stringToTriggerSelMode
+option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_MIN :read-write :include "options/quantifiers_modes.h" :handler  stringToTriggerSelMode
  selection mode for triggers
+option triggerActiveSelMode --trigger-active-sel CVC4::theory::quantifiers::TriggerActiveSelMode :default CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerActiveSelMode
+ selection mode to activate triggers
 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
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 2d3bf76f6..b3df9ca5d 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -65,6 +65,24 @@ void InstMatchGenerator::setActiveAdd(bool val){
   }
 }
 
+int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) {
+  if( Trigger::isAtomicTrigger( d_match_pattern ) ){
+    Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
+    unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
+    Trace("trigger-active-sel-debug") << "Number of ground terms for " << f << " is " << ngt << std::endl;
+    return ngt;
+  }else if( d_match_pattern.getKind()==INST_CONSTANT ){
+    TypeNode tn = d_match_pattern.getType();
+    unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn );
+    Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl;
+    return ngtt;
+//  }else if( d_match_pattern_getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+    
+  }else{
+    return -1;
+  }
+}
+
 void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){
   if( !d_pattern.isNull() ){
     Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl;
@@ -837,6 +855,14 @@ int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){
   return qe->addInstantiation( q, m ) ? 1 : 0;
 }
 
+int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) {
+  Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
+  unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
+  Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " << f << " is " << ngt << std::endl;
+  return ngt;   
+}
+
+
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 096774c51..65c5a1427 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -46,6 +46,8 @@ public:
   virtual int addTerm( Node q, Node t, QuantifiersEngine* qe ) { return 0; }
   /** set active add */
   virtual void setActiveAdd( bool val ) {}
+  /** get active score */
+  virtual int getActiveScore( QuantifiersEngine * qe ) { return 0; }
 };/* class IMGenerator */
 
 class CandidateGenerator;
@@ -116,6 +118,7 @@ public:
 
   bool d_active_add;
   void setActiveAdd( bool val );
+  int getActiveScore( QuantifiersEngine * qe );
 
   static InstMatchGenerator* mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe );
   static InstMatchGenerator* mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
@@ -239,6 +242,8 @@ public:
   int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
   /** add ground term t, possibly add instantiations */
   int addTerm( Node q, Node t, QuantifiersEngine* qe );
+  /** get active score */
+  int getActiveScore( QuantifiersEngine * qe );
 };/* class InstMatchGeneratorSimple */
 
 }
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index efd765c86..49e0a698f 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -149,11 +149,7 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
 
 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){
   //how to select trigger terms
-  if( options::triggerSelMode()==quantifiers::TRIGGER_SEL_DEFAULT ){
-    d_tr_strategy = quantifiers::TRIGGER_SEL_MIN;
-  }else{
-    d_tr_strategy = options::triggerSelMode();
-  }
+  d_tr_strategy = options::triggerSelMode();
   //whether to select new triggers during the search
   if( options::incrementTriggers() ){
     d_regenerate_frequency = 3;
@@ -211,6 +207,29 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
       //  d_processed_trigger.clear();
       //  d_quantEngine->getEqualityQuery()->setLiberal( true );
       //}
+      if( options::triggerActiveSelMode()!=TRIGGER_ACTIVE_SEL_ALL ){
+        int max_score = -1;
+        Trigger * max_trigger = NULL;
+        for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[0][f].begin(); itt != d_auto_gen_trigger[0][f].end(); ++itt ){
+          int score = itt->first->getActiveScore();
+          if( options::triggerActiveSelMode()==TRIGGER_ACTIVE_SEL_MIN ){
+            if( score>=0 && ( score<max_score || max_score<0 ) ){
+              max_score = score;
+              max_trigger = itt->first;
+            } 
+          }else{
+            if( score>max_score ){
+              max_score = score;
+              max_trigger = itt->first;
+            }
+          }
+          d_auto_gen_trigger[0][f][itt->first] = false;
+        }
+        if( max_trigger!=NULL ){
+          d_auto_gen_trigger[0][f][max_trigger] = true;
+        }
+      }
+      
       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 ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 68f824c57..2d56f2cdf 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -202,6 +202,9 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
       }      
       children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) );
       children.push_back( body[1] );
+      if( body.getNumChildren()==3 ){
+        children.push_back( body[2] );
+      }
       Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
       if( in!=n ){
         Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index ee091919d..2faed3af0 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -386,9 +386,9 @@ bool Trigger::isCbqiKind( Kind k ) {
 
 bool Trigger::isSimpleTrigger( Node n ){
   Node t = n.getKind()==NOT ? n[0] : n;
-  if( n.getKind()==IFF || n.getKind()==EQUAL ){
-    if( !quantifiers::TermDb::hasInstConstAttr( n[1] ) ){
-      t = n[0];
+  if( t.getKind()==IFF || t.getKind()==EQUAL ){
+    if( !quantifiers::TermDb::hasInstConstAttr( t[1] ) ){
+      t = t[0];
     }
   }
   if( isAtomicTrigger( t ) ){
@@ -742,6 +742,10 @@ InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) {
   }
 }
 
+int Trigger::getActiveScore() {
+  return d_mg->getActiveScore( d_quantEngine );
+}
+
 Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
   if( nodes.empty() ){
     return d_tr.empty() ? NULL : d_tr[0];
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index a3da4d398..6d7bf1f4d 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -134,6 +134,7 @@ class Trigger {
     }
     Trace(c) << " )";
   }
+  int getActiveScore();
 private:
   /** trigger constructor */
   Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes );