Performance optimization for E-matching, working on using QCF module for propagations.

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 783f6284d4dc5d343b695d331abc0d62ef4ea4d5..60fa672b303f7684ddb5f2dd7347e069c6698f91 100644 (file)
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -68,35 +68,57 @@ void CandidateGeneratorQE::resetInstantiationRound(){
 void CandidateGeneratorQE::reset( Node eqc ){
   d_term_iter = 0;
   if( eqc.isNull() ){
-    d_using_term_db = true;
+    d_mode = cand_term_db;
   }else{
     //create an equivalence class iterator in eq class eqc
-    d_eqc.clear();
-    d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
-    d_using_term_db = false;
+    //d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
+
+    eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
+    if( ee->hasTerm( eqc ) ){
+      Node rep = ee->getRepresentative( eqc );
+      d_eqc_iter = eq::EqClassIterator( rep, ee );
+      d_mode = cand_term_eqc;
+    }else{
+      d_n = eqc;
+      d_mode = cand_term_ident;
+    }
+    //a should be in its equivalence class
+    //Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
+  }
+}
+bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
+  if( n.hasOperator() && n.getOperator()==d_op ){
+    if( isLegalCandidate( n ) ){
+      return true;
+    }
   }
+  return false;
 }
 
 Node CandidateGeneratorQE::getNextCandidate(){
-  if( d_term_iter>=0 ){
-    if( d_using_term_db ){
-      //get next candidate term in the uf term database
-      while( d_term_iter<d_term_iter_limit ){
-        Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
-        d_term_iter++;
-        if( isLegalCandidate( n ) ){
-          return n;
-        }
+  if( d_mode==cand_term_db ){
+    //get next candidate term in the uf term database
+    while( d_term_iter<d_term_iter_limit ){
+      Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+      d_term_iter++;
+      if( isLegalCandidate( n ) ){
+        return n;
       }
-    }else{
-      while( d_term_iter<(int)d_eqc.size() ){
-        Node n = d_eqc[d_term_iter];
-        d_term_iter++;
-        if( n.hasOperator() && n.getOperator()==d_op ){
-          if( isLegalCandidate( n ) ){
-            return n;
-          }
-        }
+    }
+  }else if( d_mode==cand_term_eqc ){
+    while( !d_eqc_iter.isFinished() ){
+      Node n = *d_eqc_iter;
+      ++d_eqc_iter;
+      if( isLegalOpCandidate( n ) ){
+        return n;
+      }
+    }
+  }else if( d_mode==cand_term_ident ){
+    if( !d_n.isNull() ){
+      Node n = d_n;
+      d_n = Node::null();
+      if( isLegalOpCandidate( n ) ){
+        return n;
       }
     }
   }

diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index a87c24596e9cfe3516ef96a3689ede69b7b6e71f..74029b633fa1b19ccb5b54ba4027c36589d93294 100644 (file)
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -79,10 +79,19 @@ private:
   //instantiator pointer
   QuantifiersEngine* d_qe;
   //the equality class iterator
-  std::vector< Node > d_eqc;
+  eq::EqClassIterator d_eqc_iter;
+  //std::vector< Node > d_eqc;
   int d_term_iter;
   int d_term_iter_limit;
   bool d_using_term_db;
+  enum {
+    cand_term_db,
+    cand_term_ident,
+    cand_term_eqc,
+  };
+  short d_mode;
+  bool isLegalOpCandidate( Node n );
+  Node d_n;
 public:
   CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
   ~CandidateGeneratorQE(){}

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 4cb62b5234c9d0d459d62f62af0d1c23ac9fc686..66191107da51b3f8ef6a3ceefc09fb1d4a9f7343 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -353,7 +353,7 @@ void QuantConflictFind::getEqRegistryApps( Node lit, std::vector< Node >& terms
   }\r
 }\r
 \r
-int QuantConflictFind::evaluate( Node n ) {\r
+int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {\r
   int ret = 0;\r
   if( n.getKind()==EQUAL ){\r
     Node n1 = getTerm( n[0] );\r
@@ -425,6 +425,33 @@ int QuantConflictFind::evaluate( Node n ) {
   return ret;\r
 }\r
 \r
+bool QuantConflictFind::isPropagationSet() {\r
+  return !d_prop_eq[0].isNull();\r
+}\r
+\r
+bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {\r
+  return n1==n2;\r
+  /*\r
+  if( n1==n2 ){\r
+    return true;\r
+  }else if( isPropagationSet() && d_prop_pol ){\r
+    return ( d_prop_eq[0]==n1 && d_prop_eq[1]==n2 ) || ( d_prop_eq[0]==n2 && d_prop_eq[1]==n1 );\r
+  }\r
+  */\r
+}\r
+\r
+bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {\r
+  //return n1!=n2;\r
+  return areDisequal( n1, n2 );\r
+  /*\r
+  if( n1!=n2 ){\r
+    return true;\r
+  }else if( isPropagationSet() && !d_prop_pol ){\r
+    return ( d_prop_eq[0]==n1 && d_prop_eq[1]==n2 ) || ( d_prop_eq[0]==n2 && d_prop_eq[1]==n1 );\r
+  }\r
+  */\r
+}\r
+\r
 //-------------------------------------------------- handling assertions / eqc\r
 \r
 void QuantConflictFind::assertNode( Node q ) {\r
@@ -467,20 +494,6 @@ Node QuantConflictFind::getTerm( Node n ) {
 }\r
 \r
 QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) {\r
-  /*\r
-  NodeBoolMap::iterator it = d_eqc.find( n );\r
-  if( it==d_eqc.end() ){\r
-    if( doCreate ){\r
-      d_eqc[n] = true;\r
-    }else{\r
-      //equivalence class does not currently exist\r
-      return NULL;\r
-    }\r
-  }else{\r
-    //should only ask for valid equivalence classes\r
-    Assert( (*it).second );\r
-  }\r
-  */\r
   std::map< Node, EqcInfo * >::iterator it2 = d_eqc_info.find( n );\r
   if( it2==d_eqc_info.end() ){\r
     if( doCreate ){\r
@@ -494,6 +507,24 @@ QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreat
   return it2->second;\r
 }\r
 \r
+QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {\r
+  std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms[ eqc ].find( f );\r
+  if( itut!=d_eqc_uf_terms[ eqc ].end() ){\r
+    return &itut->second;\r
+  }else{\r
+    return NULL;\r
+  }\r
+}\r
+\r
+QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {\r
+  std::map< TNode, QcfNodeIndex >::iterator itut = d_uf_terms.find( f );\r
+  if( itut!=d_uf_terms.end() ){\r
+    return &itut->second;\r
+  }else{\r
+    return NULL;\r
+  }\r
+}\r
+\r
 /** new node */\r
 void QuantConflictFind::newEqClass( Node n ) {\r
   Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;\r
@@ -573,7 +604,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
       Assert( false );\r
     }\r
   }else{\r
-    bool addedLemma = false;\r
+    int addedLemmas = 0;\r
     if( d_performCheck ){\r
       ++(d_statistics.d_inst_rounds);\r
       double clSet = 0;\r
@@ -590,69 +621,82 @@ void QuantConflictFind::check( Theory::Effort level ) {
         Trace("qcf-debug") << std::endl;\r
       }\r
 \r
-\r
-      Trace("qcf-check") << "Checking quantified formulas..." << std::endl;\r
-      for( unsigned j=0; j<d_qassert.size(); j++ ){\r
-        Node q = d_qassert[j];\r
-        Trace("qcf-check") << "Check quantified formula ";\r
-        debugPrintQuant("qcf-check", q);\r
-        Trace("qcf-check") << " : " << q << "..." << std::endl;\r
-\r
-        Assert( d_qinfo.find( q )!=d_qinfo.end() );\r
-        if( d_qinfo[q].d_mg->isValid() ){\r
-          d_qinfo[q].reset_round( this );\r
-          //try to make a matches making the body false\r
-          d_qinfo[q].d_mg->reset( this, false, q );\r
-          while( d_qinfo[q].d_mg->getNextMatch( this, q ) ){\r
-\r
-            Trace("qcf-check") << "*** Produced match : " << std::endl;\r
-            d_qinfo[q].debugPrintMatch("qcf-check");\r
-            Trace("qcf-check") << std::endl;\r
-\r
-            if( !d_qinfo[q].isMatchSpurious( this ) ){\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
-                  Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_qinfo[q].d_match[i] << std::endl;\r
-                  m.set( d_quantEngine, q, i, cv );\r
-                }\r
-                if( Debug.isOn("qcf-check-inst") ){\r
-                  Node inst = d_quantEngine->getInstantiation( q, m );\r
-                  Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
-                  Assert( evaluate( inst )==-1 );\r
-                }\r
-                if( d_quantEngine->addInstantiation( q, m ) ){\r
-                  Trace("qcf-check") << "   ... Added instantiation" << std::endl;\r
-                  d_quantEngine->flushLemmas();\r
-                  d_conflict.set( true );\r
-                  addedLemma = true;\r
-                  ++(d_statistics.d_conflict_inst);\r
-                  break;\r
+      for( short e = effort_conflict; e<=effort_conflict; e++ ){\r
+        d_effort = e;\r
+        if( e == effort_propagation ){\r
+          for( unsigned i=0; i<2; i++ ){\r
+            d_prop_eq[i] = Node::null();\r
+          }\r
+        }\r
+        Trace("qcf-check") << "Checking quantified formulas..." << std::endl;\r
+        for( unsigned j=0; j<d_qassert.size(); j++ ){\r
+          Node q = d_qassert[j];\r
+          Trace("qcf-check") << "Check quantified formula ";\r
+          debugPrintQuant("qcf-check", q);\r
+          Trace("qcf-check") << " : " << q << "..." << std::endl;\r
+\r
+          Assert( d_qinfo.find( q )!=d_qinfo.end() );\r
+          if( d_qinfo[q].d_mg->isValid() ){\r
+            d_qinfo[q].reset_round( this );\r
+            //try to make a matches making the body false\r
+            d_qinfo[q].d_mg->reset( this, false, q );\r
+            while( d_qinfo[q].d_mg->getNextMatch( this, q ) ){\r
+\r
+              Trace("qcf-check") << "*** Produced match : " << std::endl;\r
+              d_qinfo[q].debugPrintMatch("qcf-check");\r
+              Trace("qcf-check") << std::endl;\r
+\r
+              if( !d_qinfo[q].isMatchSpurious( this ) ){\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
+                    Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_qinfo[q].d_match[i] << std::endl;\r
+                    m.set( d_quantEngine, q, i, cv );\r
+                  }\r
+                  if( Debug.isOn("qcf-check-inst") ){\r
+                    Node inst = d_quantEngine->getInstantiation( q, m );\r
+                    Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
+                    Assert( evaluate( inst )==-1 );\r
+                  }\r
+                  if( d_quantEngine->addInstantiation( q, m ) ){\r
+                    Trace("qcf-check") << "   ... Added instantiation" << std::endl;\r
+                    ++addedLemmas;\r
+                    if( e==effort_conflict ){\r
+                      d_conflict.set( true );\r
+                      ++(d_statistics.d_conflict_inst);\r
+                      break;\r
+                    }else if( e==effort_propagation ){\r
+                      ++(d_statistics.d_prop_inst);\r
+                    }\r
+                  }else{\r
+                    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") << "   ... 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
+                  Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
                 }\r
               }else{\r
-                Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
+                Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
               }\r
-            }else{\r
-              Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
             }\r
           }\r
+          if( d_conflict ){\r
+            break;\r
+          }\r
         }\r
-        if( addedLemma ){\r
-          break;\r
+        if( Trace.isOn("qcf-engine") ){\r
+          double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
+          Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet) << ", addedLemmas = " << addedLemmas << std::endl;\r
+        }\r
+        if( addedLemmas>0 ){\r
+          d_quantEngine->flushLemmas();\r
         }\r
-      }\r
-      if( Trace.isOn("qcf-engine") ){\r
-        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
-        Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet) << ", addedLemma = " << addedLemma << std::endl;\r
       }\r
     }\r
     Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
@@ -955,7 +999,7 @@ bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p,
       return false;\r
     }else if( !isVar( n ) && !isVar( cv ) ){\r
       //they must actually be disequal\r
-      if( !p->areDisequal( n, cv ) ){\r
+      if( !p->areMatchDisequal( n, cv ) ){\r
         return false;\r
       }\r
     }\r
@@ -1022,16 +1066,14 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
             //copy or check disequalities\r
             std::map< int, std::map< Node, int > >::iterator itd = d_curr_var_deq.find( v );\r
             if( itd!=d_curr_var_deq.end() ){\r
-              //std::vector< Node > addDeq;\r
               for( std::map< Node, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){\r
                 Node dv = getCurrentValue( it->first );\r
                 if( !alreadySet ){\r
                   if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){\r
                     d_curr_var_deq[vn][dv] = v;\r
-                    //addDeq.push_back( dv );\r
                   }\r
                 }else{\r
-                  if( itmn->second!=dv ){\r
+                  if( !p->areMatchDisequal( itmn->second, dv ) ){\r
                     Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;\r
                     return -1;\r
                   }\r
@@ -1049,7 +1091,7 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
             }else{\r
               Debug("qcf-match-debug") << "  -> Both variables bound, compare" << std::endl;\r
               //are they currently equal\r
-              return itm->second==itmn->second ? 0 : -1;\r
+              return p->areMatchEqual( itm->second, itmn->second ) ? 0 : -1;\r
             }\r
           }\r
         }else{\r
@@ -1059,7 +1101,7 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
           }else{\r
             //compare ground values\r
             Debug("qcf-match-debug") << "  -> Ground value, compare " << itm->second << " "<< n << std::endl;\r
-            return itm->second==n ? 0 : -1;\r
+            return p->areMatchEqual( itm->second, n ) ? 0 : -1;\r
           }\r
         }\r
         if( setMatch( p, v, n ) ){\r
@@ -1088,7 +1130,8 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
           //check if it respects equality\r
           std::map< int, Node >::iterator itm = d_match.find( v );\r
           if( itm!=d_match.end() ){\r
-            if( getCurrentValue( n )==itm->second ){\r
+            Node nv = getCurrentValue( n );\r
+            if( !p->areMatchDisequal( nv, itm->second ) ){\r
               Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;\r
               return -1;\r
             }\r
@@ -1230,13 +1273,14 @@ void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {
   }\r
 }\r
 \r
-\r
+/*\r
 struct MatchGenSort {\r
   QuantConflictFind::MatchGen * d_mg;\r
   bool operator() (int i,int j) {\r
     return d_mg->d_children[i].d_type<d_mg->d_children[j].d_type;\r
   }\r
 };\r
+*/\r
 \r
 QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVar ){\r
   Trace("qcf-qregister-debug") << "Make match gen for " << n << ", top/var = " << isTop << " " << isVar << std::endl;\r
@@ -1255,19 +1299,6 @@ 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
-      if( d_children[0].d_type==typ_invalid ){\r
-        d_children.clear();\r
-        d_type = typ_invalid;\r
-      }else{\r
-        d_type = typ_top;\r
-      }\r
-      d_type_not = false;\r
-    }else\r
-    */\r
     if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
       //we handle not immediately\r
       d_n = n.getKind()==NOT ? n[0] : n;\r
@@ -1338,56 +1369,20 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
       d_n = n;\r
       d_type = typ_ground;\r
     }\r
-    if( d_type!=typ_invalid ){\r
+    //if( d_type!=typ_invalid ){\r
       //determine an efficient children ordering\r
-      if( !d_children.empty() ){\r
-        for( unsigned i=0; i<d_children.size(); i++ ){\r
-          d_children_order.push_back( i );\r
-        }\r
+      //if( !d_children.empty() ){\r
+        //for( unsigned i=0; i<d_children.size(); i++ ){\r
+        //  d_children_order.push_back( i );\r
+        //}\r
         //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){\r
           //sort based on the type of the constraint : ground comes first, then literals, then others\r
           //MatchGenSort mgs;\r
           //mgs.d_mg = this;\r
           //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
-        for( unsigned j=q[0].getNumChildren(); j<p->d_qinfo[q].d_vars.size(); j++ ){\r
-          d_children.push_back( MatchGen( p, q, p->d_qinfo[q].d_vars[j], false, true ) );\r
-        }\r
-\r
-        //choose variable order for variables based on when they are bound\r
-        std::vector< int > varOrder;\r
-        varOrder.insert( varOrder.end(), d_children_order.begin(), d_children_order.end() );\r
-        d_children_order.clear();\r
-        std::map< int, bool > bound;\r
-        for( unsigned i=0; i<varOrder.size(); i++ ){\r
-          int curr = varOrder[i];\r
-          Trace("qcf-qregister-debug") << "Var Order : " << curr << std::endl;\r
-          d_children_order.push_back( curr );\r
-          for( std::map< int, int >::iterator it = d_children[curr].d_qni_var_num.begin();\r
-               it != d_children[curr].d_qni_var_num.end(); ++it ){\r
-            if( it->second>=(int)q[0].getNumChildren() && bound.find( it->second )==bound.end() ){\r
-              bound[ it->second ] = true;\r
-              int var = base + it->second - (int)q[0].getNumChildren();\r
-              d_children_order.push_back( var );\r
-              Trace("qcf-qregister-debug") << "Var Order, bound : " << var << std::endl;\r
-            }\r
-          }\r
-        }\r
-        for( unsigned j=q[0].getNumChildren(); j<p->d_qinfo[q].d_vars.size(); j++ ){\r
-          if( bound.find( j )==bound.end() ){\r
-            int var = base + j - (int)q[0].getNumChildren();\r
-            d_children_order.push_back( var );\r
-            Trace("qcf-qregister-debug") << "Var Order, remaining : " << j << std::endl;\r
-          }\r
-        }\r
-      }\r
-      */\r
-    }\r
+      //}\r
+    //}\r
   }\r
   if( d_type!=typ_invalid ){\r
     if( !qni_apps.empty() ){\r
@@ -1411,7 +1406,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
   Trace("qcf-qregister-debug")  << "Done make match gen " << n << ", type = ";\r
   debugPrintType( "qcf-qregister-debug", d_type, true );\r
   Trace("qcf-qregister-debug") << std::endl;\r
-  Assert( d_children.size()==d_children_order.size() );\r
+  //Assert( d_children.size()==d_children_order.size() );\r
 }\r
 \r
 void QuantConflictFind::MatchGen::reset_round( QuantConflictFind * p ) {\r
@@ -1435,7 +1430,7 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q
 \r
   //set up processing matches\r
   if( d_type==typ_ground ){\r
-    if( p->evaluate( d_n )==( d_tgt ? 1 : -1 ) ){\r
+    if( p->evaluate( d_n, d_tgt, true )==( d_tgt ? 1 : -1 ) ){\r
       //store dummy variable\r
       d_qn.push_back( NULL );\r
     }\r
@@ -1450,18 +1445,18 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q
     if( it!=p->d_qinfo[q].d_match.end() && d_tgt ) {\r
       Debug("qcf-match") << "       will be matching var within eqc = " << it->second << std::endl;\r
       //f-applications in the equivalence class in match[ repVar ]\r
-      std::map< TNode, QcfNodeIndex >::iterator itut = p->d_eqc_uf_terms[ it->second ].find( f );\r
-      if( itut!=p->d_eqc_uf_terms[ it->second ].end() ){\r
-        d_qn.push_back( &itut->second );\r
+      QcfNodeIndex * qni = p->getQcfNodeIndex( it->second, f );\r
+      if( qni ){\r
+        d_qn.push_back( qni );\r
       }\r
     }else{\r
       Debug("qcf-match") << "       will be matching var within any eqc." << std::endl;\r
       //we are binding rep var\r
       d_qni_bound_cons[repVar] = Node::null();\r
       //must look at all f-applications\r
-      std::map< TNode, QcfNodeIndex >::iterator itut = p->d_uf_terms.find( f );\r
-      if( itut!=p->d_uf_terms.end() ){\r
-        d_qn.push_back( &itut->second );\r
+      QcfNodeIndex * qni = p->getQcfNodeIndex( f );\r
+      if( qni ){\r
+        d_qn.push_back( qni );\r
       }\r
     }\r
   }else if( d_type==typ_var_eq ){\r
@@ -1513,6 +1508,7 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
     bool success = doMatching( p, q );\r
     if( success ){\r
       Debug("qcf-match") << "     Produce matches for bound variables..." << std::endl;\r
+\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
@@ -1546,6 +1542,7 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
         }\r
       }\r
     }\r
+    //if not successful, clean up the variables you bound\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
@@ -1580,7 +1577,7 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
             if( getChild( d_child_counter )->getNextMatch( p, q ) ){\r
               if( d_child_counter<(int)(getNumChildren()-1) ){\r
                 d_child_counter++;\r
-                Debug("qcf-match-debug") << "       Reset child " << d_child_counter << " of " << d_n << ", all match " << d_children_order.size() << " " << d_children_order[d_child_counter] << std::endl;\r
+                Debug("qcf-match-debug") << "       Reset child " << d_child_counter << " of " << d_n << std::endl;\r
                 getChild( d_child_counter )->reset( p, d_tgt, q );\r
               }else{\r
                 success = true;\r
@@ -1724,6 +1721,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
               Debug("qcf-match-debug") << "       Failed to match" << std::endl;\r
               d_qn.pop_back();\r
             }\r
+            //TODO : if it is equal to something else, also try that\r
           }\r
         }else{\r
           Assert( d_qn.size()==d_qni.size() );\r
@@ -1747,6 +1745,8 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
             }else{\r
               Debug("qcf-match-debug") << "       Bind next variable, no more variables to bind" << std::endl;\r
             }\r
+          }else{\r
+            //TODO : if it equal to something else, also try that\r
           }\r
           //if not incrementing, move to next\r
           if( !success ){\r
@@ -1928,15 +1928,18 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
 \r
 QuantConflictFind::Statistics::Statistics():\r
   d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),\r
-  d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 )\r
+  d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),\r
+  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 )\r
 {\r
   StatisticsRegistry::registerStat(&d_inst_rounds);\r
   StatisticsRegistry::registerStat(&d_conflict_inst);\r
+  StatisticsRegistry::registerStat(&d_prop_inst);\r
 }\r
 \r
 QuantConflictFind::Statistics::~Statistics(){\r
   StatisticsRegistry::unregisterStat(&d_inst_rounds);\r
   StatisticsRegistry::unregisterStat(&d_conflict_inst);\r
+  StatisticsRegistry::unregisterStat(&d_prop_inst);\r
 }\r
 \r
 }
\ No newline at end of file

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 657586d1a504d44b14589588f6e0eb3a908b2d5d..15923b0badf83ebd61edc815e435e4c1b73d3bd7 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -101,7 +101,7 @@ private:  //for ground terms
   std::map< int, std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > > > d_eqr[2];\r
   EqRegistry * getEqRegistry( bool polarity, Node lit, bool doCreate = true );\r
   void getEqRegistryApps( Node lit, std::vector< Node >& terms );\r
-  int evaluate( Node n );\r
+  int evaluate( Node n, bool pref = false, bool hasPref = false );\r
 public:  //for quantifiers\r
   //match generator\r
   class MatchGen {\r
@@ -109,9 +109,10 @@ public:  //for quantifiers
     //current children information\r
     int d_child_counter;\r
     //children of this object\r
-    std::vector< int > d_children_order;\r
+    //std::vector< int > d_children_order;\r
     unsigned getNumChildren() { return d_children.size(); }\r
-    MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }\r
+    //MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }\r
+    MatchGen * getChild( int i ) { return &d_children[i]; }\r
     //current matching information\r
     std::vector< QcfNodeIndex * > d_qn;\r
     std::vector< std::map< TNode, QcfNodeIndex >::iterator > d_qni;\r
@@ -203,6 +204,8 @@ private:  //for equivalence classes
   std::map< TNode, QcfNodeIndex > d_uf_terms;\r
   // eqc x operator -> index(terms)\r
   std::map< TNode, std::map< TNode, QcfNodeIndex > > d_eqc_uf_terms;\r
+  QcfNodeIndex * getQcfNodeIndex( Node eqc, Node f );\r
+  QcfNodeIndex * getQcfNodeIndex( Node f );\r
   // type -> list(eqc)\r
   std::map< TypeNode, std::vector< TNode > > d_eqcs;\r
   //mapping from UF terms to representatives of their arguments\r
@@ -211,6 +214,18 @@ private:  //for equivalence classes
   void computeArgReps( TNode n );\r
   // is this term treated as UF application?\r
   bool isHandledUfTerm( TNode n );\r
+public:\r
+  enum {\r
+    effort_conflict,\r
+    effort_propagation,\r
+  };\r
+  short d_effort;\r
+  //for effort_prop\r
+  TNode d_prop_eq[2];\r
+  bool d_prop_pol;\r
+  bool isPropagationSet();\r
+  bool areMatchEqual( TNode n1, TNode n2 );\r
+  bool areMatchDisequal( TNode n1, TNode n2 );\r
 public:\r
   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );\r
 \r
@@ -247,6 +262,7 @@ public:
   public:\r
     IntStat d_inst_rounds;\r
     IntStat d_conflict_inst;\r
+    IntStat d_prop_inst;\r
     Statistics();\r
     ~Statistics();\r
   };\r

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2ddc83a4b78a33705dbfa4af32a845b6d2bdd14f..001d8b2b6956a78ae87a64418bdd3a9ae93177b8 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -346,19 +346,28 @@ Node QuantifiersEngine::doSubstitute( Node n, std::vector< Node >& terms ){
   if( n.getKind()==INST_CONSTANT ){
     Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
     return terms[n.getAttribute(InstVarNumAttribute())];
-  }else if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
-    Debug("check-inst") << "No inst const attr : " << n << std::endl;
-    return n;
   }else{
-    Debug("check-inst") << "Recurse on : " << n << std::endl;
+    //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
+      //Debug("check-inst") << "No inst const attr : " << n << std::endl;
+      //return n;
+    //}else{
+      //Debug("check-inst") << "Recurse on : " << n << std::endl;
     std::vector< Node > cc;
     if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
       cc.push_back( n.getOperator() );
     }
+    bool changed = false;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      cc.push_back( doSubstitute( n[i], terms ) );
+      Node c = doSubstitute( n[i], terms );
+      cc.push_back( c );
+      changed = changed || c!=n[i];
+    }
+    if( changed ){
+      Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
+      return ret;
+    }else{
+      return n;
     }
-    return NodeManager::currentNM()->mkNode( n.getKind(), cc );
   }
 }