6 files changed, 66 insertions, 8 deletions
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 );