Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.

1 files changed, 94 insertions, 107 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index e5df41510..1cbfbd99b 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
@@ -46,7 +47,7 @@ QuantInfo::~QuantInfo() {
 }
 
 
-void QuantInfo::initialize( Node q, Node qn ) {
+void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
   d_q = q;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     d_match.push_back( TNode::null() );
@@ -107,6 +108,59 @@ void QuantInfo::initialize( Node q, Node qn ) {
     Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
   }
   Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
+  
+  if( d_mg->isValid() ){
+    //optimization : record variable argument positions for terms that must be matched
+    std::vector< TNode > vars;
+    //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
+    //if( options::qcfSkipRd() ){
+    //  for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
+    //    vars.push_back( d_vars[j] );
+    //  }
+    //}
+    //get all variables that are always relevant
+    std::map< TNode, bool > visited;
+    getPropagateVars( vars, q[1], false, visited );
+    for( unsigned j=0; j<vars.size(); j++ ){
+      Node v = vars[j];
+      TNode f = p->getTermDatabase()->getMatchOperator( v );
+      if( !f.isNull() ){
+        Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl;
+        for( unsigned k=0; k<v.getNumChildren(); k++ ){
+          Node n = v[k];
+          std::map< TNode, int >::iterator itv = d_var_num.find( n );
+          if( itv!=d_var_num.end() ){
+            Trace("qcf-opt") << "  arg " << k << " is var #" << itv->second << std::endl;
+            if( std::find( d_var_rel_dom[itv->second][f].begin(), d_var_rel_dom[itv->second][f].end(), k )==d_var_rel_dom[itv->second][f].end() ){
+              d_var_rel_dom[itv->second][f].push_back( k );
+            }
+          }
+        }
+      }
+    }    
+  }
+}
+
+void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){
+  std::map< TNode, bool >::iterator itv = visited.find( n );
+  if( itv==visited.end() ){
+    visited[n] = true;
+    bool rec = true;
+    bool newPol = pol;
+    if( d_var_num.find( n )!=d_var_num.end() ){
+      Assert( std::find( vars.begin(), vars.end(), n )==vars.end() );
+      vars.push_back( n );
+    }else if( MatchGen::isHandledBoolConnective( n ) ){
+      Assert( n.getKind()!=IMPLIES );
+      QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
+    }
+    Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
+    if( rec ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        getPropagateVars( vars, n[i], pol, visited );
+      }
+    }
+  }
 }
 
 void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
@@ -327,7 +381,7 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
         return 1;
       }else{
         //std::map< int, TNode >::iterator itm = d_match.find( v );
-
+        bool isGroundRep = false;
         if( vn!=-1 ){
           Debug("qcf-match-debug") << "  ...Variable bound to variable" << std::endl;
           //std::map< int, TNode >::iterator itmn = d_match.find( vn );
@@ -373,13 +427,14 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
         }else{
           Debug("qcf-match-debug") << "  ...Variable bound to ground" << std::endl;
           if( d_match[v].isNull() ){
+            //isGroundRep = true;   ??
           }else{
             //compare ground values
             Debug("qcf-match-debug") << "  -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
             return p->areMatchEqual( d_match[v], n ) ? 0 : -1;
           }
         }
-        if( setMatch( p, v, n ) ){
+        if( setMatch( p, v, n, isGroundRep ) ){
           Debug("qcf-match-debug") << "  -> success" << std::endl;
           return 1;
         }else{
@@ -445,8 +500,23 @@ bool QuantInfo::isConstrainedVar( int v ) {
   }
 }
 
-bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) {
+bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep ) {
   if( getCurrentCanBeEqual( p, v, n ) ){
+    if( isGroundRep ){
+      //fail if n does not exist in the relevant domain of each of the argument positions
+      std::map< int, std::map< TNode, std::vector< unsigned > > >::iterator it = d_var_rel_dom.find( v );
+      if( it!=d_var_rel_dom.end() ){
+        for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+          for( unsigned j=0; j<it2->second.size(); j++ ){
+            Debug("qcf-match-debug2") << n << " in relevant domain " <<  it2->second << "." << it2->second[j] << "?" << std::endl;
+            if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){
+              Debug("qcf-match-debug") << "  -> fail, since " << n << " is not in relevant domain of " << it2->second << "." << it2->second[j] << std::endl;
+              return false;
+            }
+          }
+        }
+      }
+    }
     Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " <<  d_curr_var_deq[v].size() << " disequalities" << std::endl;
     d_match[v] = n;
     return true;
@@ -566,7 +636,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
                 if( !z.isNull() ){
                   Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
                   assigned.push_back( vn );
-                  if( !setMatch( p, vn, z ) ){
+                  if( !setMatch( p, vn, z, false ) ){
                     success = false;
                     break;
                   }
@@ -608,7 +678,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
             if( !sum.isNull() ){
               assigned.push_back( slv_v );
               Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
-              if( !setMatch( p, slv_v, sum ) ){
+              if( !setMatch( p, slv_v, sum, false ) ){
                 success = false;
               }
               p->d_tempCache.push_back( sum );
@@ -694,7 +764,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
                 int currIndex = d_una_eqc_count[d_una_index];
                 d_una_eqc_count[d_una_index]++;
                 Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;
-                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){
+                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex], true ) ){
                   d_match_term[d_unassigned[d_una_index]] = TNode::null();
                   Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
                   d_una_index++;
@@ -1125,7 +1195,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     }else{
       //unassigned, set match to true/false
       d_qni_bound[0] = vn;
-      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false );
+      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false, false );
       d_child_counter = 0;
     }
     if( d_child_counter==0 ){
@@ -1365,17 +1435,6 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
           d_qni_bound_cons.clear();
         }
       }
-      /*
-      if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){
-        d_matched_basis = true;
-        Node f = getMatchOperator( d_n );
-        TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f );
-        if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){
-          success = true;
-          d_qni_bound[0] = d_qni_var_num[0];
-        }
-      }
-      */
     }
     Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;
     d_wasSet = success;
@@ -1595,7 +1654,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
               if( it != d_qn[index]->d_data.end() ) {
                 d_qni.push_back( it );
                 //set the match
-                if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){
+                if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first, true ) ){
                   Debug("qcf-match-debug") << "       Binding variable" << std::endl;
                   if( d_qn.size()<d_qni_size ){
                     d_qn.push_back( &it->second );
@@ -1640,7 +1699,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
             d_qni[index]++;
             if( d_qni[index]!=d_qn[index]->d_data.end() ){
               success = true;
-              if( qi->setMatch( p, itb->second, d_qni[index]->first ) ){
+              if( qi->setMatch( p, itb->second, d_qni[index]->first, true ) ){
                 Debug("qcf-match-debug") << "       Bind next variable" << std::endl;
                 if( d_qn.size()<d_qni_size ){
                   d_qn.push_back( &d_qni[index]->second );
@@ -1756,8 +1815,7 @@ bool MatchGen::isHandled( TNode n ) {
 
 QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
 QuantifiersModule( qe ),
-d_conflict( c, false ),
-d_qassert( c ) {
+d_conflict( c, false ) {
   d_fid_count = 0;
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
@@ -1782,7 +1840,7 @@ void QuantConflictFind::registerQuantifier( Node q ) {
     Trace("qcf-qregister") << " : " << q << std::endl;
     //make QcfNode structure
     Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
-    d_qinfo[q].initialize( q, q[1] );
+    d_qinfo[q].initialize( this, q, q[1] );
 
     //debug print
     Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
@@ -1797,7 +1855,7 @@ void QuantConflictFind::registerQuantifier( Node q ) {
         Trace("qcf-qregister") << std::endl;
       }
     }
-
+    
     Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
   }
 }
@@ -1805,10 +1863,8 @@ void QuantConflictFind::registerQuantifier( Node q ) {
 short QuantConflictFind::getMaxQcfEffort() {
   if( options::qcfMode()==QCF_CONFLICT_ONLY ){
     return effort_conflict;
-  }else if( options::qcfMode()==QCF_PROP_EQ ){
+  }else if( options::qcfMode()==QCF_PROP_EQ || options::qcfMode()==QCF_PARTIAL ){
     return effort_prop_eq;
-  }else if( options::qcfMode()==QCF_MC ){
-    return effort_mc;
   }else{
     return 0;
   }
@@ -1833,16 +1889,13 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
 //-------------------------------------------------- handling assertions / eqc
 
 void QuantConflictFind::assertNode( Node q ) {
+  /*
   if( d_quantEngine->hasOwnership( q, this ) ){
     Trace("qcf-proc") << "QCF : assertQuantifier : ";
     debugPrintQuant("qcf-proc", q);
     Trace("qcf-proc") << std::endl;
-    d_qassert.push_back( q );
-    //set the eqRegistries that this depends on to true
-    //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){
-    //  it->first->d_active.set( true );
-    //}
   }
+  */
 }
 
 /** new node */
@@ -1904,28 +1957,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
 
       //determine order for quantified formulas
       std::vector< Node > qorder;
-      std::map< Node, bool > qassert;
-      //mark which are asserted
-      for( unsigned i=0; i<d_qassert.size(); i++ ){
-        qassert[d_qassert[i]] = true;
-      }
-      //add which ones are specified in the order
-      for( unsigned i=0; i<d_quant_order.size(); i++ ){
-        Node n = d_quant_order[i];
-        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() && qassert.find( n )!=qassert.end() ){
-          qorder.push_back( n );
-        }
-      }
-      d_quant_order.clear();
-      d_quant_order.insert( d_quant_order.begin(), qorder.begin(), qorder.end() );
-      //add remaining
-      for( unsigned i=0; i<d_qassert.size(); i++ ){
-        Node n = d_qassert[i];
-        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() ){
-          qorder.push_back( n );
+      for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+        Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
+        if( d_quantEngine->hasOwnership( q, this ) ){
+          qorder.push_back( q );
         }
       }
-
       if( Trace.isOn("qcf-debug") ){
         Trace("qcf-debug") << std::endl;
         debugPrint("qcf-debug");
@@ -1974,7 +2011,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                       Trace("qcf-inst") << std::endl;
                       ++addedLemmas;
                       if( e==effort_conflict ){
-                        d_quant_order.insert( d_quant_order.begin(), q );
+                        d_quantEngine->markRelevant( q );
                         ++(d_statistics.d_conflict_inst);
                         if( options::qcfAllConflict() ){
                           isConflict = true;
@@ -1983,6 +2020,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                         }
                         break;
                       }else if( e==effort_prop_eq ){
+                        d_quantEngine->markRelevant( q );
                         ++(d_statistics.d_prop_inst);
                       }
                     }else{
@@ -2040,60 +2078,24 @@ void QuantConflictFind::computeRelevantEqr() {
     //d_uf_terms.clear();
     //d_eqc_uf_terms.clear();
     d_eqcs.clear();
-    d_model_basis.clear();
     //d_arg_reps.clear();
     //double clSet = 0;
     //if( Trace.isOn("qcf-opt") ){
     //  clSet = double(clock())/double(CLOCKS_PER_SEC);
     //}
 
-    //long nTermst = 0;
-    //long nTerms = 0;
-    //long nEqc = 0;
-
-    //which nodes are irrelevant for disequality matches
-    std::map< TNode, bool > irrelevant_dnode;
     //now, store matches
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
     while( !eqcs_i.isFinished() ){
-      //nEqc++;
       Node r = (*eqcs_i);
       if( getTermDatabase()->hasTermCurrent( r ) ){
         TypeNode rtn = r.getType();
-        if( options::qcfMode()==QCF_MC ){
-          std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );
-          if( itt==d_eqcs.end() ){
-            Node mb = getTermDatabase()->getModelBasisTerm( rtn );
-            if( !getEqualityEngine()->hasTerm( mb ) ){
-              Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;
-              Assert( false );
-            }
-            Node mbr = getRepresentative( mb );
-            if( mbr!=r ){
-              d_eqcs[rtn].push_back( mbr );
-            }
-            d_eqcs[rtn].push_back( r );
-            d_model_basis[rtn] = mb;
-          }else{
-            itt->second.push_back( r );
-          }
-        }else{
-          if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
-            d_eqcs[rtn].push_back( r );
-          }
+        if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
+          d_eqcs[rtn].push_back( r );
         }
       }
       ++eqcs_i;
     }
-    /*
-    if( Trace.isOn("qcf-opt") ){
-      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
-      Trace("qcf-opt") << "   " << nEqc << " equivalence classes. " << std::endl;
-      Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;
-      Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;
-    }
-    */
   }
 }
 
@@ -2120,21 +2122,6 @@ void QuantConflictFind::debugPrint( const char * c ) {
       ++eqc_i;
     }
     Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
-    /*
-    EqcInfo * eqcn = getEqcInfo( n, false );
-    if( eqcn ){
-      Trace(c) << "    DEQ : {";
-      pr = false;
-      for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){
-        if( (*it).second ){
-          Trace(c) << (pr ? "," : "" ) << " " << (*it).first;
-          pr = true;
-        }
-      }
-      Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
-    }
-    //}
-    */
     ++eqcs_i;
   }
 }