From 100037d531ff1fd30ed3dd5bed91076c383ad55c Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Mar 2017 09:11:52 -0500
Subject: [PATCH] Minor fixes for trigger selection max.

---
 .../quantifiers/inst_match_generator.cpp      | 27 +++---
 src/theory/quantifiers/trigger.cpp            | 85 ++++++++++---------
 src/theory/quantifiers/trigger.h              |  2 +-
 3 files changed, 58 insertions(+), 56 deletions(-)

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 7cf9868bd..661451b68 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -482,19 +482,19 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersE
 /** constructors */
 InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) :
 d_f( q ){
-  Debug("smart-multi-trigger") << "Making smart multi-trigger for " << q << std::endl;
+  Trace("smart-multi-trigger") << "Making smart multi-trigger for " << q << std::endl;
   std::map< Node, std::vector< Node > > var_contains;
   qe->getTermDatabase()->getVarContains( q, pats, var_contains );
   //convert to indicies
   for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
-    Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";
+    Trace("smart-multi-trigger") << "Pattern " << it->first << " contains: ";
     for( int i=0; i<(int)it->second.size(); i++ ){
-      Debug("smart-multi-trigger") << it->second[i] << " ";
+      Trace("smart-multi-trigger") << it->second[i] << " ";
       int index = it->second[i].getAttribute(InstVarNumAttribute());
       d_var_contains[ it->first ].push_back( index );
       d_var_to_node[ index ].push_back( it->first );
     }
-    Debug("smart-multi-trigger") << std::endl;
+    Trace("smart-multi-trigger") << std::endl;
   }
   for( unsigned i=0; i<pats.size(); i++ ){
     Node n = pats[i];
@@ -506,7 +506,7 @@ d_f( q ){
     int numSharedVars = 0;
     for( unsigned j=0; j<d_var_contains[n].size(); j++ ){
       if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
-        Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
+        Trace("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
         unique_vars.push_back( d_var_contains[n][j] );
       }else{
         shared_vars[ d_var_contains[n][j] ] = true;
@@ -530,11 +530,11 @@ d_f( q ){
       index = index==0 ? (int)(pats.size()-1) : (index-1);
     }
     vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
-    Debug("smart-multi-trigger") << "   Index[" << i << "]: ";
+    Trace("smart-multi-trigger") << "   Index[" << i << "]: ";
     for( unsigned j=0; j<vars.size(); j++ ){
-      Debug("smart-multi-trigger") << vars[j] << " ";
+      Trace("smart-multi-trigger") << vars[j] << " ";
     }
-    Debug("smart-multi-trigger") << std::endl;
+    Trace("smart-multi-trigger") << std::endl;
     //make ordered inst match trie
     d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
     d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() );
@@ -567,9 +567,9 @@ void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
 
 int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
   int addedLemmas = 0;
-  Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
+  Trace("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
   for( unsigned i=0; i<d_children.size(); i++ ){
-    Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
+    Trace("smart-multi-trigger") << "Calculate matches " << i << std::endl;
     std::vector< InstMatch > newMatches;
     InstMatch m( q );
     while( d_children[i]->getNextMatch( q, m, qe ) ){
@@ -577,8 +577,9 @@ int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, Qu
       newMatches.push_back( InstMatch( &m ) );
       m.clear();
     }
-    Debug("smart-multi-trigger") << "Made " << newMatches.size() << " new matches for index " << i << std::endl;
+    Trace("smart-multi-trigger") << "Made " << newMatches.size() << " new matches for index " << i << std::endl;
     for( unsigned j=0; j<newMatches.size(); j++ ){
+      Trace("smart-multi-trigger2") << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl;
       processNewMatch( qe, newMatches[j], i, addedLemmas );
       if( qe->inConflict() ){
         return addedLemmas;
@@ -594,7 +595,7 @@ void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch&
   //possibly only do the following if we know that new matches will be produced?
   //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
   // we can safely skip the following lines, even when we have already produced this match.
-  Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;
+  Trace("smart-multi-trigger-debug") << "Child " << fromChildIndex << " produced match " << m << std::endl;
   //process new instantiations
   int childIndex = (fromChildIndex+1)%(int)d_children.size();
   std::vector< IndexedTrie > unique_var_tries;
@@ -696,7 +697,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe,
     //m is an instantiation
     if( qe->addInstantiation( d_f, m ) ){
       addedLemmas++;
-      Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;
+      Trace("smart-multi-trigger-debug") << "-> Produced instantiation " << m << std::endl;
     }
   }
 }
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 1bfc53b41..7072d0499 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -398,16 +398,14 @@ 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 q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
+void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
                                 quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
                                 bool pol, bool hasPol, bool epol, bool hasEPol ){
   std::map< Node, Node >::iterator itv = visited.find( n );
   if( itv==visited.end() ){
     visited[ n ] = Node::null();
     Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
-    bool retVal = false;
     if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){
-      bool rec = true;
       Node nu;
       bool nu_single = false;
       if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
@@ -426,11 +424,11 @@ bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited,
           }
           Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) );
           Assert( isUsableTrigger( nu, q ) );
-          //do not add if already excluded
+          //do not add if already visited
           bool add = true;
           if( n!=nu ){
             std::map< Node, Node >::iterator itvu = visited.find( nu );
-            if( itvu!=visited.end() && itvu->second.isNull() ){
+            if( itvu!=visited.end() ){
               add = false;
             }
           }
@@ -439,55 +437,58 @@ bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited,
             visited[ nu ] = nu;
             tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
             nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
-            retVal = true;
-            if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
-              rec = false;
-            }
+          }else{
+            nu = Node::null();
           }
         }
       }
-      if( rec ){
-        Node nrec = nu.isNull() ? n : nu;
-        std::vector< Node > added2;
-        for( unsigned i=0; i<nrec.getNumChildren(); i++ ){
-          bool newHasPol, newPol;
-          bool newHasEPol, newEPol;
-          QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol );
-          QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
-          if( collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol ) ){
-            retVal = true;
-          }
-        }
-        if( !nu.isNull() ){
-          bool rm_nu = false;
-          //discard if we added a subterm as a trigger with all variables that nu has
-          for( unsigned i=0; i<added2.size(); i++ ){
-            Assert( tinfo.find( added2[i] )!=tinfo.end() );
-            if( added2[i]!=nu ){
+      Node nrec = nu.isNull() ? n : nu;
+      std::vector< Node > added2;
+      for( unsigned i=0; i<nrec.getNumChildren(); i++ ){
+        bool newHasPol, newPol;
+        bool newHasEPol, newEPol;
+        QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol );
+        QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
+        collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol );
+      }
+      if( !nu.isNull() ){
+        bool rm_nu = false;
+        for( unsigned i=0; i<added2.size(); i++ ){
+          Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i << " : " << added2[i] << std::endl;
+          Assert( added2[i]!=nu );
+          // if child was not already removed
+          if( tinfo.find( added2[i] )!=tinfo.end() ){
+            if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
+              //discard all subterms
+              Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
+              visited[added2[i]] = Node::null();
+              tinfo.erase( added2[i] );
+            }else{
               if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
+                //discard if we added a subterm as a trigger with all variables that nu has
+                Trace("auto-gen-trigger-debug2") << "......subsumes parent." << std::endl;
                 rm_nu = true;
               }
-              added.push_back( added2[i] );
-            }else{
-              Assert( false );
+              if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){
+                added.push_back( added2[i] );
+              }
             }
           }
-          if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
-            visited[nu] = Node::null();
-            tinfo.erase( nu );
-          }else{
-            added.push_back( nu );
-          }
+        }
+        if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
+          visited[nu] = Node::null();
+          tinfo.erase( nu );
+        }else{
+          Assert( std::find( added.begin(), added.end(), nu )==added.end() );
+          added.push_back( nu );
         }
       }
     }
-    return retVal;
   }else{
-    if( itv->second.isNull() ){
-      return false;
-    }else{
-      added.push_back( itv->second );
-      return true;
+    if( !itv->second.isNull() ){
+      if( std::find( added.begin(), added.end(), itv->second )==added.end() ){
+        added.push_back( itv->second );
+      }
     }
   }
 }
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 631627331..9ff82595f 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -142,7 +142,7 @@ private:
   static Node getIsUsableEq( Node q, Node eq );
   static bool isUsableEqTerms( Node q, Node n1, Node n2 );
   /** collect all APPLY_UF pattern terms for f in n */
-  static bool collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
+  static void collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
                                 quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
                                 bool pol, bool hasPol, bool epol, bool hasEPol );
 
-- 
2.30.2