Optimizations for quantifiers conflict find: better caching, process matching constra...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 15 Jan 2014 16:22:10 +0000 (10:22 -0600)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 15 Jan 2014 16:22:23 +0000 (10:22 -0600)
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h

index 1bf53db9149ce65ac32598b0008c199e78a13762..d7111ea39485ce53dd8b139c851cf6e1e211a0f3 100755 (executable)
@@ -27,21 +27,36 @@ using namespace std;
 \r
 namespace CVC4 {\r
 \r
-Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, bool doAdd, int index ) {\r
+/*\r
+Node QcfNodeIndex::existsTerm( QuantConflictFind * qcf, Node n, int index ) {\r
   if( index==(int)n.getNumChildren() ){\r
     if( d_children.empty() ){\r
-      if( doAdd ){\r
-        d_children[ n ].clear();\r
-        return n;\r
-      }else{\r
-        return Node::null();\r
-      }\r
+      return Node::null();\r
     }else{\r
       return d_children.begin()->first;\r
     }\r
   }else{\r
     Node r = qcf->getRepresentative( n[index] );\r
-    return d_children[r].addTerm( qcf, n, doAdd, index+1 );\r
+    if( d_children.find( r )==d_children.end() ){\r
+      return n;\r
+    }else{\r
+      return d_children[r].existsTerm( qcf, n, index+1 );\r
+    }\r
+  }\r
+}\r
+\r
+\r
+Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, int index ) {\r
+  if( index==(int)n.getNumChildren() ){\r
+    if( d_children.empty() ){\r
+      d_children[ n ].clear();\r
+      return n;\r
+    }else{\r
+      return d_children.begin()->first;\r
+    }\r
+  }else{\r
+    Node r = qcf->getRepresentative( n[index] );\r
+    return d_children[r].addTerm( qcf, n, index+1 );\r
   }\r
 }\r
 \r
@@ -54,6 +69,49 @@ bool QcfNodeIndex::addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int ind
     return d_children[r].addTermEq( qcf, n1, n2, index+1 );\r
   }\r
 }\r
+*/\r
+\r
+\r
+\r
+Node QcfNodeIndex::existsTerm( Node n, std::vector< Node >& reps, int index ) {\r
+  if( index==(int)reps.size() ){\r
+    if( d_children.empty() ){\r
+      return Node::null();\r
+    }else{\r
+      return d_children.begin()->first;\r
+    }\r
+  }else{\r
+    if( d_children.find( reps[index] )==d_children.end() ){\r
+      return Node::null();\r
+    }else{\r
+      return d_children[reps[index]].existsTerm( n, reps, index+1 );\r
+    }\r
+  }\r
+}\r
+\r
+Node QcfNodeIndex::addTerm( Node n, std::vector< Node >& reps, int index ) {\r
+  if( index==(int)reps.size() ){\r
+    if( d_children.empty() ){\r
+      d_children[ n ].clear();\r
+      return n;\r
+    }else{\r
+      return d_children.begin()->first;\r
+    }\r
+  }else{\r
+    return d_children[reps[index]].addTerm( n, reps, index+1 );\r
+  }\r
+}\r
+\r
+bool QcfNodeIndex::addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index ) {\r
+  if( index==(int)reps1.size() ){\r
+    Node n = addTerm( n2, reps2 );\r
+    return n==n2;\r
+  }else{\r
+    return d_children[reps1[index]].addTermEq( n1, n2, reps1, reps2, index+1 );\r
+  }\r
+}\r
+\r
+\r
 \r
 void QcfNodeIndex::debugPrint( const char * c, int t ) {\r
   for( std::map< Node, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){\r
@@ -172,7 +230,7 @@ void QuantConflictFind::registerAssertions( std::vector< Node >& assertions ) {
 \r
 void QuantConflictFind::registerAssertion( Node n ) {\r
   if( n.getKind()==FORALL ){\r
-    registerQuant( Node::null(), n[1], NULL, true, true );\r
+    registerNode( Node::null(), n[1], NULL, true, true );\r
   }else{\r
     if( n.getType().isBoolean() ){\r
       for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
@@ -182,7 +240,7 @@ void QuantConflictFind::registerAssertion( Node n ) {
   }\r
 }\r
 */\r
-void QuantConflictFind::registerQuant( Node q, Node n, bool hasPol, bool pol ) {\r
+void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {\r
   //qcf->d_node = n;\r
   bool recurse = true;\r
   if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){\r
@@ -217,7 +275,7 @@ void QuantConflictFind::registerQuant( Node q, Node n, bool hasPol, bool pol ) {
       //QcfNode * qcfc = new QcfNode( d_c );\r
       //qcfc->d_parent = qcf;\r
       //qcf->d_child[i] = qcfc;\r
-      registerQuant( q, n[i], newHasPol, newPol );\r
+      registerNode( q, n[i], newHasPol, newPol );\r
     }\r
   }\r
 }\r
@@ -251,7 +309,7 @@ void QuantConflictFind::registerQuantifier( Node q ) {
   //make QcfNode structure\r
   Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;\r
   //d_qinfo[q].d_cf = new QcfNode( d_c );\r
-  registerQuant( q, q[1], true, true );\r
+  registerNode( q, q[1], true, true );\r
 \r
   //debug print\r
   Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;\r
@@ -270,6 +328,14 @@ void QuantConflictFind::registerQuantifier( Node q ) {
   Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;\r
   d_qinfo[q].d_mg = new MatchGen( this, q, q[1], true );\r
 \r
+  for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){\r
+    d_qinfo[q].d_var_mg[j] = new MatchGen( this, q, d_qinfo[q].d_vars[j], false, true );\r
+    if( !d_qinfo[q].d_var_mg[j]->isValid() ){\r
+      d_qinfo[q].d_mg->setInvalid();\r
+      break;\r
+    }\r
+  }\r
+\r
   Trace("qcf-qregister") << "Done registering quantifier." << std::endl;\r
 }\r
 \r
@@ -433,7 +499,8 @@ Node QuantConflictFind::getRepresentative( Node n ) {
 }\r
 Node QuantConflictFind::getTerm( Node n ) {\r
   if( n.getKind()==APPLY_UF ){\r
-    Node nn = d_uf_terms[n.getOperator()].addTerm( this, n, false );\r
+    computeArgReps( n );\r
+    Node nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );\r
     if( !nn.isNull() ){\r
       return nn;\r
     }\r
@@ -544,6 +611,9 @@ void QuantConflictFind::check( Theory::Effort level ) {
   Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
   if( d_conflict ){\r
     Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
+    if( level>=Theory::EFFORT_FULL ){\r
+      Assert( false );\r
+    }\r
   }else{\r
     bool addedLemma = false;\r
     if( d_performCheck ){\r
@@ -580,61 +650,8 @@ void QuantConflictFind::check( Theory::Effort level ) {
             Trace("qcf-check") << std::endl;\r
 \r
             if( !d_qinfo[q].isMatchSpurious( this ) ){\r
-              //assign values for variables that were unassigned (usually not necessary, but handles corner cases)\r
-              Trace("qcf-check") << std::endl;\r
-              std::vector< int > unassigned;\r
-              std::vector< TypeNode > unassigned_tn;\r
-              for( int i=0; i<d_qinfo[q].getNumVars(); i++ ){\r
-                if( d_qinfo[q].d_match.find( i )==d_qinfo[q].d_match.end() ){\r
-                  Assert( i<(int)q[0].getNumChildren() );\r
-                  unassigned.push_back( i );\r
-                  unassigned_tn.push_back( d_qinfo[q].getVar( i ).getType() );\r
-                }\r
-              }\r
-              bool success = true;\r
-              if( !unassigned.empty() ){\r
-                Trace("qcf-check") << "Assign to unassigned..." << std::endl;\r
-                int index = 0;\r
-                std::vector< int > eqc_count;\r
-                do {\r
-                  bool invalidMatch;\r
-                  while( ( index>=0 && (int)index<(int)unassigned.size() ) || invalidMatch ){\r
-                    invalidMatch = false;\r
-                    if( index==(int)eqc_count.size() ){\r
-                      eqc_count.push_back( 0 );\r
-                    }else{\r
-                      Assert( index==(int)eqc_count.size()-1 );\r
-                      if( eqc_count[index]<(int)d_eqcs[unassigned_tn[index]].size() ){\r
-                        int currIndex = eqc_count[index];\r
-                        eqc_count[index]++;\r
-                        Trace("qcf-check-unassign") << unassigned[index] << "->" << d_eqcs[unassigned_tn[index]][currIndex] << std::endl;\r
-                        if( d_qinfo[q].setMatch( this, unassigned[index], d_eqcs[unassigned_tn[index]][currIndex] ) ){\r
-                          Trace("qcf-check-unassign") << "Succeeded match" << std::endl;\r
-                          index++;\r
-                        }else{\r
-                          Trace("qcf-check-unassign") << "Failed match" << std::endl;\r
-                          invalidMatch = true;\r
-                        }\r
-                      }else{\r
-                        Trace("qcf-check-unassign") << "No more matches" << std::endl;\r
-                        eqc_count.pop_back();\r
-                        index--;\r
-                      }\r
-                    }\r
-                  }\r
-                  success = index>=0;\r
-                  if( success ){\r
-                    index = (int)unassigned.size()-1;\r
-                    Trace("qcf-check-unassign") << "  Try: " << std::endl;\r
-                    for( unsigned i=0; i<unassigned.size(); i++ ){\r
-                      int ui = unassigned[i];\r
-                      Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_qinfo[q].d_vars[ui] << " -> " << d_qinfo[q].d_match[ui] << std::endl;\r
-                    }\r
-                  }\r
-                }while( success && d_qinfo[q].isMatchSpurious( this ) );\r
-              }\r
-\r
-              if( success ){\r
+              std::vector< int > assigned;\r
+              if( d_qinfo[q].completeMatch( this, q, assigned ) ){\r
                 InstMatch m;\r
                 for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
                   Node cv = d_qinfo[q].getCurrentValue( d_qinfo[q].d_match[i] );\r
@@ -657,12 +674,13 @@ void QuantConflictFind::check( Theory::Effort level ) {
                   Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;\r
                   Assert( false );\r
                 }\r
+                //clean up assigned\r
+                for( unsigned i=0; i<assigned.size(); i++ ){\r
+                  d_qinfo[q].d_match.erase( assigned[i] );\r
+                }\r
               }else{\r
                 Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
               }\r
-              for( unsigned i=0; i<unassigned.size(); i++ ){\r
-                d_qinfo[q].d_match.erase( unassigned[i] );\r
-              }\r
             }else{\r
               Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
             }\r
@@ -683,8 +701,12 @@ void QuantConflictFind::check( Theory::Effort level ) {
 \r
 bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
   d_performCheck = false;\r
-  if( !d_conflict && level==Theory::EFFORT_FULL ){\r
-    d_performCheck = true;\r
+  if( !d_conflict ){\r
+    if( level==Theory::EFFORT_FULL ){\r
+      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;\r
+    }else if( level==Theory::EFFORT_STANDARD ){\r
+      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;\r
+    }\r
   }\r
   return d_performCheck;\r
 }\r
@@ -701,6 +723,7 @@ void QuantConflictFind::computeRelevantEqr() {
   d_uf_terms.clear();\r
   d_eqc_uf_terms.clear();\r
   d_eqcs.clear();\r
+  d_arg_reps.clear();\r
 \r
   //which nodes are irrelevant for disequality matches\r
   std::map< Node, bool > irrelevant_dnode;\r
@@ -740,9 +763,10 @@ void QuantConflictFind::computeRelevantEqr() {
       Node n = (*eqc_i);\r
       bool isRedundant;\r
       if( n.getKind()==APPLY_UF ){\r
-        Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( this, n );\r
+        computeArgReps( n );\r
+        Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( n, d_arg_reps[n] );\r
         isRedundant = (nadd!=n);\r
-        d_uf_terms[n.getOperator()].addTerm( this, n );\r
+        d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );\r
       }else{\r
         isRedundant = false;\r
       }\r
@@ -773,7 +797,7 @@ void QuantConflictFind::computeRelevantEqr() {
                 //fn with m\r
                 std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( m );\r
                 if( itm!=itn[j]->second.end() ){\r
-                  if( itm->second->d_qni.addTerm( this, n )==n ){\r
+                  if( itm->second->d_qni.addTerm( n, d_arg_reps[n] )==n ){\r
                     Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
                     Trace("qcf-reqr") << fn << " " << m << std::endl;\r
                   }\r
@@ -782,9 +806,10 @@ void QuantConflictFind::computeRelevantEqr() {
               if( !fm.isNull() ){\r
                 std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( fm );\r
                 if( itm!=itn[j]->second.end() ){\r
+                  Assert( d_arg_reps.find( m )!=d_arg_reps.end() );\r
                   if( j==0 ){\r
                     //n with fm\r
-                    if( itm->second->d_qni.addTerm( this, m )==m ){\r
+                    if( itm->second->d_qni.addTerm( m, d_arg_reps[m] )==m ){\r
                       Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
                       Trace("qcf-reqr") << n << " " << fm << std::endl;\r
                     }\r
@@ -795,7 +820,7 @@ void QuantConflictFind::computeRelevantEqr() {
                       if( i==0 || m.getOperator()==n.getOperator() ){\r
                         Node am = ((i==0)==mltn) ? n : m;\r
                         Node an = ((i==0)==mltn) ? m : n;\r
-                        if( itm->second->d_qni.addTermEq( this, an, am ) ){\r
+                        if( itm->second->d_qni.addTermEq( an, am, d_arg_reps[n], d_arg_reps[m] ) ){\r
                           Trace("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for ";\r
                           Trace("qcf-reqr") << fn << " " << fm << std::endl;\r
                         }\r
@@ -826,6 +851,14 @@ void QuantConflictFind::computeRelevantEqr() {
   }\r
 }\r
 \r
+void QuantConflictFind::computeArgReps( Node n ) {\r
+  if( d_arg_reps.find( n )==d_arg_reps.end() ){\r
+    for( unsigned j=0; j<n.getNumChildren(); j++ ){\r
+      d_arg_reps[n].push_back( getRepresentative( n[j] ) );\r
+    }\r
+  }\r
+}\r
+\r
 \r
 void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {\r
   d_match.clear();\r
@@ -853,6 +886,9 @@ void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {
     }\r
   }\r
   d_mg->reset_round( p );\r
+  for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){\r
+    it->second->reset_round( p );\r
+  }\r
 }\r
 \r
 int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) {\r
@@ -913,7 +949,7 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
   //for handling equalities between variables, and disequalities involving variables\r
   Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";\r
   Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;\r
-  Assert( n==getCurrentValue( n ) );\r
+  Assert( doRemove || n==getCurrentValue( n ) );\r
   Assert( doRemove || v==getCurrentRepVar( v ) );\r
   Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) );\r
   if( polarity ){\r
@@ -1060,6 +1096,90 @@ bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
   return false;\r
 }\r
 \r
+bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned ) {\r
+  //assign values for variables that were unassigned (usually not necessary, but handles corner cases)\r
+  Trace("qcf-check") << std::endl;\r
+  std::vector< int > unassigned[2];\r
+  std::vector< TypeNode > unassigned_tn[2];\r
+  for( int i=0; i<getNumVars(); i++ ){\r
+    if( d_match.find( i )==d_match.end() ){\r
+      Assert( i<(int)q[0].getNumChildren() );\r
+      int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;\r
+      unassigned[rindex].push_back( i );\r
+      unassigned_tn[rindex].push_back( getVar( i ).getType() );\r
+      assigned.push_back( i );\r
+    }\r
+  }\r
+  bool success = true;\r
+  for( unsigned r=0; r<2; r++ ){\r
+    if( success && !unassigned[r].empty() ){\r
+      Trace("qcf-check") << "Assign to unassigned, rep = " << r << "..." << std::endl;\r
+      int index = 0;\r
+      std::vector< int > eqc_count;\r
+      do {\r
+        bool invalidMatch;\r
+        while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch ){\r
+          invalidMatch = false;\r
+          if( index==(int)eqc_count.size() ){\r
+            //check if it has now been assigned\r
+            if( r==0 ){\r
+              d_var_mg[ unassigned[r][index] ]->reset( p, true, q );\r
+            }\r
+            eqc_count.push_back( 0 );\r
+          }else{\r
+            if( r==0 ){\r
+              if( d_var_mg[unassigned[r][index]]->getNextMatch( p, q ) ){\r
+                Trace("qcf-check-unassign") << "Succeeded match with mg" << std::endl;\r
+                index++;\r
+              }else{\r
+                Trace("qcf-check-unassign") << "Failed match with mg" << std::endl;\r
+                eqc_count.pop_back();\r
+                index--;\r
+              }\r
+            }else{\r
+              Assert( index==(int)eqc_count.size()-1 );\r
+              if( eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){\r
+                int currIndex = eqc_count[index];\r
+                eqc_count[index]++;\r
+                Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl;\r
+                if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){\r
+                  Trace("qcf-check-unassign") << "Succeeded match" << std::endl;\r
+                  index++;\r
+                }else{\r
+                  Trace("qcf-check-unassign") << "Failed match" << std::endl;\r
+                  invalidMatch = true;\r
+                }\r
+              }else{\r
+                Trace("qcf-check-unassign") << "No more matches" << std::endl;\r
+                eqc_count.pop_back();\r
+                index--;\r
+              }\r
+            }\r
+          }\r
+        }\r
+        success = index>=0;\r
+        if( success ){\r
+          index = (int)unassigned[r].size()-1;\r
+          Trace("qcf-check-unassign") << "  Try: " << std::endl;\r
+          for( unsigned i=0; i<unassigned[r].size(); i++ ){\r
+            int ui = unassigned[r][i];\r
+            Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;\r
+          }\r
+        }\r
+      }while( success && isMatchSpurious( p ) );\r
+    }\r
+  }\r
+  if( success ){\r
+    return true;\r
+  }else{\r
+    for( unsigned i=0; i<assigned.size(); i++ ){\r
+      d_match.erase( assigned[i] );\r
+    }\r
+    assigned.clear();\r
+    return false;\r
+  }\r
+}\r
+\r
 void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {\r
   for( int i=0; i<getNumVars(); i++ ){\r
     Trace(c) << "  " << d_vars[i] << " -> ";\r
@@ -1095,7 +1215,8 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
     Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() );\r
     if( n.getKind()==APPLY_UF ){\r
       d_type = typ_var;\r
-      d_type_not = true;  //implicit disequality, in disjunction at top level\r
+      //d_type_not = true;  //implicit disequality, in disjunction at top level\r
+      d_type_not = false;\r
       d_n = n;\r
       qni_apps.push_back( n );\r
     }else{\r
@@ -1103,6 +1224,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
       d_type = typ_invalid;\r
     }\r
   }else{\r
+    /*\r
     if( isTop && n.getKind()!=OR && p->d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){\r
       //conjoin extra constraints based on flattening with quantifier body\r
       d_children.push_back( MatchGen( p, q, n ) );\r
@@ -1113,7 +1235,9 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
         d_type = typ_top;\r
       }\r
       d_type_not = false;\r
-    }else if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+    }else\r
+    */\r
+    if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
       //we handle not immediately\r
       d_n = n.getKind()==NOT ? n[0] : n;\r
       d_type_not = n.getKind()==NOT;\r
@@ -1123,8 +1247,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
           d_children.push_back( MatchGen( p, q, d_n[i] ) );\r
           if( d_children[d_children.size()-1].d_type==typ_invalid ){\r
-            d_type = typ_invalid;\r
-            d_children.clear();\r
+            setInvalid();\r
             break;\r
           }else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){\r
             Trace("qcf-qregister-debug") << "Remove child, make built-in constraint" << std::endl;\r
@@ -1197,6 +1320,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
           //std::sort( d_children_order.begin(), d_children_order.end(), mgs );\r
         //}\r
       }\r
+      /*\r
       if( isTop ){\r
         int base = d_children.size();\r
         //add additional constraints based on flattening\r
@@ -1231,6 +1355,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
           }\r
         }\r
       }\r
+      */\r
     }\r
   }\r
   if( d_type!=typ_invalid ){\r
@@ -1355,6 +1480,41 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
   Debug("qcf-match") << ", children = " << d_children.size() << std::endl;\r
   if( d_children.empty() ){\r
     bool success = doMatching( p, q );\r
+    if( success ){\r
+      Debug("qcf-match") << "     Produce matches for bound variables..." << std::endl;\r
+      //also need to create match for each variable we bound\r
+      std::map< int, int >::iterator it = d_qni_bound.begin();\r
+      bool doReset = true;\r
+      while( success && it!=d_qni_bound.end() ){\r
+        std::map< int, MatchGen * >::iterator itm = p->d_qinfo[q].d_var_mg.find( it->second );\r
+        if( itm!=p->d_qinfo[q].d_var_mg.end() ){\r
+          Debug("qcf-match-debug") << "       process variable " << it->second << ", reset = " << doReset << std::endl;\r
+          if( doReset ){\r
+            itm->second->reset( p, true, q );\r
+          }\r
+          if( !itm->second->getNextMatch( p, q ) ){\r
+            do {\r
+              if( it==d_qni_bound.begin() ){\r
+                Debug("qcf-match-debug") << "       failed." << std::endl;\r
+                success = false;\r
+              }else{\r
+                Debug("qcf-match-debug") << "       decrement..." << std::endl;\r
+                --it;\r
+              }\r
+            }while( success && p->d_qinfo[q].d_var_mg.find( it->second )==p->d_qinfo[q].d_var_mg.end() );\r
+            doReset = false;\r
+          }else{\r
+            Debug("qcf-match-debug") << "       increment..." << std::endl;\r
+            ++it;\r
+            doReset = true;\r
+          }\r
+        }else{\r
+          Debug("qcf-match-debug") << "       skip..." << std::endl;\r
+          ++it;\r
+          doReset = true;\r
+        }\r
+      }\r
+    }\r
     if( !success ){\r
       for( std::map< int, Node >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){\r
         if( !it->second.isNull() ){\r
@@ -1621,6 +1781,11 @@ void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, boo
   }\r
 }\r
 \r
+void QuantConflictFind::MatchGen::setInvalid() {\r
+  d_type = typ_invalid;\r
+  d_children.clear();\r
+}\r
+\r
 \r
 //-------------------------------------------------- debugging\r
 \r
index 930b6ea52dc1809665df79a0be404c3cf904c5e6..0b503d49b22eb943698c5168b6e555b375cbcc65 100755 (executable)
@@ -33,9 +33,14 @@ class QcfNodeIndex {
 public:\r
   std::map< Node, QcfNodeIndex > d_children;\r
   void clear() { d_children.clear(); }\r
-  Node addTerm( QuantConflictFind * qcf, Node n, bool doAdd = true, int index = 0 );\r
-  bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 );\r
+  //Node existsTerm( QuantConflictFind * qcf, Node n, int index = 0 );\r
+  //Node addTerm( QuantConflictFind * qcf, Node n, int index = 0 );\r
+  //bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 );\r
   void debugPrint( const char * c, int t );\r
+  //optimized versions\r
+  Node existsTerm( Node n, std::vector< Node >& reps, int index = 0 );\r
+  Node addTerm( Node n, std::vector< Node >& reps, int index = 0 );\r
+  bool addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index = 0 );\r
 };\r
 \r
 class EqRegistry {\r
@@ -78,7 +83,7 @@ private:
   context::CDO< bool > d_conflict;\r
   bool d_performCheck;\r
   //void registerAssertion( Node n );\r
-  void registerQuant( Node q, Node n, bool hasPol, bool pol );\r
+  void registerNode( Node q, Node n, bool hasPol, bool pol );\r
   void flatten( Node q, Node n );\r
 private:\r
   std::map< TypeNode, Node > d_fv;\r
@@ -142,6 +147,7 @@ public:  //for quantifiers
     void reset( QuantConflictFind * p, bool tgt, Node q );\r
     bool getNextMatch( QuantConflictFind * p, Node q );\r
     bool isValid() { return d_type!=typ_invalid; }\r
+    void setInvalid();\r
   };\r
 private:\r
   //currently asserted quantifiers\r
@@ -159,6 +165,7 @@ private:
     int getNumVars() { return (int)d_vars.size(); }\r
     Node getVar( int i ) { return d_vars[i]; }\r
     MatchGen * d_mg;\r
+    std::map< int, MatchGen * > d_var_mg;\r
     void reset_round( QuantConflictFind * p );\r
   public:\r
     //current constraints\r
@@ -171,6 +178,7 @@ private:
     int addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove );\r
     bool setMatch( QuantConflictFind * p, int v, Node n );\r
     bool isMatchSpurious( QuantConflictFind * p );\r
+    bool completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned );\r
     void debugPrintMatch( const char * c );\r
   };\r
   std::map< Node, QuantInfo > d_qinfo;\r
@@ -197,6 +205,10 @@ private:  //for equivalence classes
   std::map< Node, std::map< Node, QcfNodeIndex > > d_eqc_uf_terms;\r
   // type -> list(eqc)\r
   std::map< TypeNode, std::vector< Node > > d_eqcs;\r
+  //mapping from UF terms to representatives of their arguments\r
+  std::map< Node, std::vector< Node > > d_arg_reps;\r
+  //compute arg reps\r
+  void computeArgReps( Node n );\r
 public:\r
   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );\r
 \r