Refactor QCF slightly. Bug fix for relevant domain (non-ground terms were added...

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index aead93d07acc036c8b1abab4eb0eeaf01d5966f4..d2920f6caa6bce9186d3552ecf42b8f71423adcb 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -69,14 +69,94 @@ void QcfNodeIndex::debugPrint( const char * c, int t ) {
 }\r
 \r
 \r
-void QuantInfo::initialize( Node q ) {\r
+void QuantInfo::initialize( Node q, Node qn ) {\r
   d_q = q;\r
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
     d_match.push_back( TNode::null() );\r
     d_match_term.push_back( TNode::null() );\r
   }\r
+\r
+  //register the variables\r
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
+    d_var_num[q[0][i]] = i;\r
+    d_vars.push_back( q[0][i] );\r
+  }\r
+\r
+  registerNode( qn, true, true );\r
+\r
+\r
+  Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;\r
+  d_mg = new MatchGen( this, qn, true );\r
+\r
+  if( d_mg->isValid() ){\r
+    for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){\r
+      d_var_mg[j] = new MatchGen( this, d_vars[j], false, true );\r
+      if( !d_var_mg[j]->isValid() ){\r
+        d_mg->setInvalid();\r
+        break;\r
+      }\r
+    }\r
+    //must also contain all variables?\r
+    /*\r
+      if( d_mg->isValid() ){\r
+        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
+          if( d_has_var.find( q[0][i] )==d_has_var.end() ){\r
+            d_mg->setInvalid();\r
+            break;\r
+          }\r
+        }\r
+      }\r
+    */\r
+  }\r
 }\r
 \r
+void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {\r
+  if( n.getKind()==FORALL ){\r
+    //do nothing\r
+  }else{\r
+    if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){\r
+      if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+        //literals\r
+        if( n.getKind()==APPLY_UF ){\r
+          flatten( n );\r
+        }else if( n.getKind()==EQUAL ){\r
+          for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+            flatten( n[i] );\r
+          }\r
+        }\r
+      }\r
+    }\r
+    if( n.getKind()==BOUND_VARIABLE ){\r
+      d_has_var[n] = true;\r
+    }\r
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+      bool newHasPol;\r
+      bool newPol;\r
+      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );\r
+      //QcfNode * qcfc = new QcfNode( d_c );\r
+      //qcfc->d_parent = qcf;\r
+      //qcf->d_child[i] = qcfc;\r
+      registerNode( n[i], newHasPol, newPol );\r
+    }\r
+  }\r
+}\r
+\r
+void QuantInfo::flatten( Node n ) {\r
+  if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){\r
+    if( d_var_num.find( n )==d_var_num.end() ){\r
+      //Trace("qcf-qregister") << "    Flatten term " << n[i] << std::endl;\r
+      d_var_num[n] = d_vars.size();\r
+      d_vars.push_back( n );\r
+      d_match.push_back( TNode::null() );\r
+      d_match_term.push_back( TNode::null() );\r
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+        flatten( n[i] );\r
+      }\r
+    }\r
+  }\r
+}\r
+\r
+\r
 void QuantInfo::reset_round( QuantConflictFind * p ) {\r
   for( unsigned i=0; i<d_match.size(); i++ ){\r
     d_match[i] = TNode::null();\r
@@ -364,6 +444,9 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
       std::vector< int > eqc_count;\r
       bool doFail = false;\r
       do {\r
+        if( doFail ){\r
+          Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;\r
+        }\r
         bool invalidMatch = false;\r
         while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch || doFail ){\r
           invalidMatch = false;\r
@@ -399,7 +482,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
                 }while( index>=0 && eqc_count[index]==-1 );\r
               }\r
             }else{\r
-              Assert( index==(int)eqc_count.size()-1 );\r
+              Assert( doFail || index==(int)eqc_count.size()-1 );\r
               if( !doFail && eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){\r
                 int currIndex = eqc_count[index];\r
                 eqc_count[index]++;\r
@@ -467,6 +550,7 @@ void QuantInfo::debugPrintMatch( const char * c ) {
   }\r
 }\r
 \r
+\r
 /*\r
 struct MatchGenSort {\r
   MatchGen * d_mg;\r
@@ -476,14 +560,14 @@ struct MatchGenSort {
 };\r
 */\r
 \r
-MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVar ){\r
+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isTop, bool isVar ){\r
   Trace("qcf-qregister-debug") << "Make match gen for " << n << ", top/var = " << isTop << " " << isVar << std::endl;\r
   std::vector< Node > qni_apps;\r
   d_qni_size = 0;\r
   if( isVar ){\r
-    Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() );\r
-    if( p->isHandledUfTerm( n ) ){\r
-      d_qni_var_num[0] = p->d_qinfo[q].getVarNum( n );\r
+    Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );\r
+    if( isHandledUfTerm( n ) ){\r
+      d_qni_var_num[0] = qi->getVarNum( n );\r
       d_qni_size++;\r
       d_type = typ_var;\r
       d_type_not = false;\r
@@ -491,9 +575,9 @@ MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVa
       for( unsigned j=0; j<d_n.getNumChildren(); j++ ){\r
         Node nn = d_n[j];\r
         Trace("qcf-qregister-debug") << "  " << d_qni_size;\r
-        if( p->d_qinfo[q].isVar( nn ) ){\r
-          Trace("qcf-qregister-debug") << " is var #" << p->d_qinfo[q].d_var_num[nn] << std::endl;\r
-          d_qni_var_num[d_qni_size] = p->d_qinfo[q].d_var_num[nn];\r
+        if( qi->isVar( nn ) ){\r
+          Trace("qcf-qregister-debug") << " is var #" << qi->d_var_num[nn] << std::endl;\r
+          d_qni_var_num[d_qni_size] = qi->d_var_num[nn];\r
         }else{\r
           Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;\r
           d_qni_gterm[d_qni_size] = nn;\r
@@ -513,7 +597,7 @@ MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVa
         //non-literals\r
         d_type = typ_formula;\r
         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
-          d_children.push_back( MatchGen( p, q, d_n[i] ) );\r
+          d_children.push_back( MatchGen( qi, d_n[i] ) );\r
           if( d_children[d_children.size()-1].d_type==typ_invalid ){\r
             setInvalid();\r
             break;\r
@@ -543,12 +627,14 @@ MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVa
         d_type = typ_invalid;\r
         //literals\r
         if( d_n.getKind()==APPLY_UF ){\r
-          Assert( p->d_qinfo[q].isVar( d_n ) );\r
+          Assert( qi->isVar( d_n ) );\r
           d_type = typ_pred;\r
         }else if( d_n.getKind()==EQUAL ){\r
           for( unsigned i=0; i<2; i++ ){\r
             if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){\r
-              Assert( p->d_qinfo[q].isVar( d_n[i] ) );\r
+              Assert( qi->isVar( d_n[i] ) );\r
+            }else{\r
+              d_qni_gterm[i] = d_n[i];\r
             }\r
           }\r
           d_type = typ_eq;\r
@@ -616,13 +702,15 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
 \r
   //set up processing matches\r
   if( d_type==typ_invalid ){\r
-    //d_child_counter = 0;\r
+    if( p->d_effort>QuantConflictFind::effort_conflict ){\r
+      d_child_counter = 0;\r
+    }\r
   }else if( d_type==typ_ground ){\r
     if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){\r
       d_child_counter = 0;\r
     }\r
   }else if( d_type==typ_var ){\r
-    Assert( p->isHandledUfTerm( d_n ) );\r
+    Assert( isHandledUfTerm( d_n ) );\r
     Node f = d_n.getOperator();\r
     Debug("qcf-match-debug") << "       reset: Var will match operators of " << f << std::endl;\r
     QcfNodeIndex * qni = p->getQcfNodeIndex( Node::null(), f );\r
@@ -641,7 +729,14 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       d_tgt = true;\r
     }else{\r
       for( unsigned i=0; i<2; i++ ){\r
-        nn[i] = qi->getCurrentValue( d_n[i] );\r
+        TNode nc;\r
+        std::map< int, TNode >::iterator it = d_qni_gterm_rep.find( i );\r
+        if( it!=d_qni_gterm_rep.end() ){\r
+          nc = it->second;\r
+        }else{\r
+          nc = d_n[i];\r
+        }\r
+        nn[i] = qi->getCurrentValue( nc );\r
         vn[i] = qi->getCurrentRepVar( qi->getVarNum( nn[i] ) );\r
       }\r
     }\r
@@ -1048,6 +1143,17 @@ void MatchGen::setInvalid() {
   d_children.clear();\r
 }\r
 \r
+bool MatchGen::isHandledUfTerm( TNode n ) {\r
+  return n.getKind()==APPLY_UF;\r
+}\r
+\r
+Node MatchGen::getFunction( Node n ) {\r
+  if( isHandledUfTerm( n ) ){\r
+    return n.getOperator();\r
+  }else{\r
+    return Node::null();\r
+  }\r
+}\r
 \r
 \r
 QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :\r
@@ -1060,32 +1166,6 @@ d_qassert( c ) {
   d_false = NodeManager::currentNM()->mkConst<bool>(false);\r
 }\r
 \r
-Node QuantConflictFind::getFunction( Node n, int& index, bool isQuant ) {\r
-  if( isQuant && !quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
-    index = 0;\r
-    return n;\r
-  }else if( isHandledUfTerm( n ) ){\r
-    /*\r
-    std::map< Node, Node >::iterator it = d_op_node.find( n.getOperator() );\r
-    if( it==d_op_node.end() ){\r
-      std::vector< Node > children;\r
-      children.push_back( n.getOperator() );\r
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
-        children.push_back( getFv( n[i].getType() ) );\r
-      }\r
-      Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );\r
-      d_op_node[n.getOperator()] = nn;\r
-      return nn;\r
-    }else{\r
-      return it->second;\r
-    }*/\r
-    index = 1;\r
-    return n.getOperator();\r
-  }else{\r
-    return Node::null();\r
-  }\r
-}\r
-\r
 Node QuantConflictFind::mkEqNode( Node a, Node b ) {\r
   if( a.getType().isBoolean() ){\r
     return a.iffNode( b );\r
@@ -1096,91 +1176,15 @@ Node QuantConflictFind::mkEqNode( Node a, Node b ) {
 \r
 //-------------------------------------------------- registration\r
 \r
-void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {\r
-  if( n.getKind()==FORALL ){\r
-    //do nothing\r
-  }else{\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
-      if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
-        //literals\r
-\r
-        /*\r
-          if( n.getKind()==APPLY_UF || ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){\r
-            for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
-              flatten( q, n[i] );\r
-            }\r
-          }else if( n.getKind()==EQUAL ){\r
-            for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
-              for( unsigned j=0; j<n[i].getNumChildren(); j++ ){\r
-                flatten( q, n[i][j] );\r
-              }\r
-            }\r
-          }\r
-\r
-          */\r
-\r
-        if( n.getKind()==APPLY_UF ){\r
-          flatten( q, n );\r
-        }else if( n.getKind()==EQUAL ){\r
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
-            flatten( q, n[i] );\r
-          }\r
-        }\r
-\r
-      }else{\r
-        Trace("qcf-qregister") << "    RegisterGroundLit : " << n;\r
-      }\r
-      recurse = false;\r
-    }\r
-    if( recurse ){\r
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
-        bool newHasPol;\r
-        bool newPol;\r
-        QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );\r
-        //QcfNode * qcfc = new QcfNode( d_c );\r
-        //qcfc->d_parent = qcf;\r
-        //qcf->d_child[i] = qcfc;\r
-        registerNode( q, n[i], newHasPol, newPol );\r
-      }\r
-    }\r
-  }\r
-}\r
-\r
-void QuantConflictFind::flatten( Node q, Node n ) {\r
-  if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){\r
-    if( d_qinfo[q].d_var_num.find( n )==d_qinfo[q].d_var_num.end() ){\r
-      //Trace("qcf-qregister") << "    Flatten term " << n[i] << std::endl;\r
-      d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();\r
-      d_qinfo[q].d_vars.push_back( n );\r
-      d_qinfo[q].d_match.push_back( TNode::null() );\r
-      d_qinfo[q].d_match_term.push_back( TNode::null() );\r
-    }\r
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
-      flatten( q, n[i] );\r
-    }\r
-  }\r
-}\r
-\r
 void QuantConflictFind::registerQuantifier( Node q ) {\r
   d_quants.push_back( q );\r
   d_quant_id[q] = d_quants.size();\r
-  d_qinfo[q].initialize( q );\r
   Trace("qcf-qregister") << "Register ";\r
   debugPrintQuant( "qcf-qregister", q );\r
   Trace("qcf-qregister") << " : " << q << std::endl;\r
-\r
-  //register the variables\r
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
-    d_qinfo[q].d_var_num[q[0][i]] = i;\r
-    d_qinfo[q].d_vars.push_back( q[0][i] );\r
-  }\r
-\r
   //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
-  registerNode( q, q[1], true, true );\r
+  d_qinfo[q].initialize( q, q[1] );\r
 \r
   //debug print\r
   Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;\r
@@ -1196,17 +1200,6 @@ void QuantConflictFind::registerQuantifier( Node q ) {
     }\r
   }\r
 \r
-  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
@@ -1339,7 +1332,7 @@ Node QuantConflictFind::getRepresentative( Node n ) {
   }\r
 }\r
 Node QuantConflictFind::evaluateTerm( Node n ) {\r
-  if( isHandledUfTerm( n ) ){\r
+  if( MatchGen::isHandledUfTerm( n ) ){\r
     Node nn;\r
     if( getEqualityEngine()->hasTerm( n ) ){\r
       computeArgReps( n );\r
@@ -1673,17 +1666,13 @@ void QuantConflictFind::computeRelevantEqr() {
         bool isRedundant;\r
         std::map< TNode, std::vector< TNode > >::iterator it_na;\r
         TNode fn;\r
-        if( isHandledUfTerm( n ) ){\r
+        if( MatchGen::isHandledUfTerm( n ) ){\r
           computeArgReps( n );\r
           it_na = d_arg_reps.find( n );\r
           Assert( it_na!=d_arg_reps.end() );\r
           Node nadd = d_eqc_uf_terms[n.getOperator()].d_children[r].addTerm( n, d_arg_reps[n] );\r
           isRedundant = (nadd!=n);\r
           d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );\r
-          if( !isRedundant ){\r
-            int jindex;\r
-            fn = getFunction( n, jindex );\r
-          }\r
         }else{\r
           isRedundant = false;\r
         }\r
@@ -1705,16 +1694,12 @@ void QuantConflictFind::computeRelevantEqr() {
 \r
 void QuantConflictFind::computeArgReps( TNode n ) {\r
   if( d_arg_reps.find( n )==d_arg_reps.end() ){\r
-    Assert( isHandledUfTerm( n ) );\r
+    Assert( MatchGen::isHandledUfTerm( n ) );\r
     for( unsigned j=0; j<n.getNumChildren(); j++ ){\r
       d_arg_reps[n].push_back( getRepresentative( n[j] ) );\r
     }\r
   }\r
 }\r
-bool QuantConflictFind::isHandledUfTerm( TNode n ) {\r
-  return n.getKind()==APPLY_UF;\r
-}\r
-\r
 \r
 //-------------------------------------------------- debugging\r
 \r

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 29ddceb4018c4517b31b5768efe7eac1086ea90e..010a8e1944b6f8ce51ea479c9123ae1b00b724ed 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -80,7 +80,7 @@ public:
   void debugPrintType( const char * c, short typ, bool isTrace = false );\r
 public:\r
   MatchGen() : d_type( typ_invalid ){}\r
-  MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop = false, bool isVar = false );\r
+  MatchGen( QuantInfo * qi, Node n, bool isTop = false, bool isVar = false );\r
   bool d_tgt;\r
   Node d_n;\r
   std::vector< MatchGen > d_children;\r
@@ -91,10 +91,19 @@ public:
   bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );\r
   bool isValid() { return d_type!=typ_invalid; }\r
   void setInvalid();\r
+\r
+  // is this term treated as UF application?\r
+  static bool isHandledUfTerm( TNode n );\r
+  static Node getFunction( Node n );\r
 };\r
 \r
 //info for quantifiers\r
 class QuantInfo {\r
+private:\r
+  void registerNode( Node n, bool hasPol, bool pol );\r
+  void flatten( Node n );\r
+  //the variables that this quantified formula has not beneath nested quantifiers\r
+  std::map< TNode, bool > d_has_var;\r
 public:\r
   QuantInfo() : d_mg( NULL ) {}\r
   std::vector< TNode > d_vars;\r
@@ -111,7 +120,7 @@ public:
   void reset_round( QuantConflictFind * p );\r
 public:\r
   //initialize\r
-  void initialize( Node q );\r
+  void initialize( Node q, Node qn );\r
   //current constraints\r
   std::vector< TNode > d_match;\r
   std::vector< TNode > d_match_term;\r
@@ -140,11 +149,8 @@ private:
   context::CDO< bool > d_conflict;\r
   bool d_performCheck;\r
   //void registerAssertion( Node n );\r
-  void registerNode( Node q, Node n, bool hasPol, bool pol );\r
-  void flatten( Node q, Node n );\r
 private:\r
   std::map< Node, Node > d_op_node;\r
-  Node getFunction( Node n, int& index, bool isQuant = false );\r
   int d_fid_count;\r
   std::map< Node, int > d_fid;\r
   Node mkEqNode( Node a, Node b );\r
@@ -189,8 +195,6 @@ private:  //for equivalence classes
   std::map< TNode, std::vector< TNode > > d_arg_reps;\r
   //compute arg reps\r
   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

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 5e489c5be303ba787ca65bd5a039d449fc55b57f..9166b81e880da1c99b13cdc78a3a59b703cdd982 100644 (file)
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -153,7 +153,7 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
         if( rf!=rq ){
           rq->merge( rf );
         }
-      }else{
+      }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n[i] ) ){
         //term to add
         rf->addTerm( n[i] );
       }