Option for prenex normal form

1 files changed, 123 insertions, 10 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index b0718699e..24a6b78b0 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1074,9 +1074,9 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
   return body;
 }
 
-Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){
+Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol ){
   if( body.getKind()==FORALL ){
-    if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){
+    if( ( pol || options::prenexQuantAgg() ) && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){
       std::vector< Node > terms;
       std::vector< Node > subs;
       //for doing prenexing of same-signed quantifiers
@@ -1085,14 +1085,27 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
         terms.push_back( body[0][i] );
         subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) );
       }
-      args.insert( args.end(), subs.begin(), subs.end() );
+      if( pol ){
+        args.insert( args.end(), subs.begin(), subs.end() );
+      }else{
+        nargs.insert( nargs.end(), subs.begin(), subs.end() );
+      }
       Node newBody = body[1];
       newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
       return newBody;
-    }else{
-      return body;
     }
-  }else{
+  //must remove structure
+  }else if( options::prenexQuantAgg() && body.getKind()==kind::ITE && body.getType().isBoolean() ){
+    Node nn = NodeManager::currentNM()->mkNode( kind::AND,
+              NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ),
+              NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) );
+    return computePrenex( nn, args, nargs, pol );
+  }else if( options::prenexQuantAgg() && body.getKind()==kind::IFF ){
+    Node nn = NodeManager::currentNM()->mkNode( kind::AND,
+              NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ),
+              NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) );
+    return computePrenex( nn, args, nargs, pol );
+  }else if( body.getType().isBoolean() ){
     Assert( body.getKind()!=EXISTS );
     bool childrenChanged = false;
     std::vector< Node > newChildren;
@@ -1101,7 +1114,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
       bool newPol;
       QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol );
       if( newHasPol ){
-        Node n = computePrenex( body[i], args, newPol );
+        Node n = computePrenex( body[i], args, nargs, newPol );
         newChildren.push_back( n );
         if( n!=body[i] ){
           childrenChanged = true;
@@ -1116,10 +1129,61 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
       }else{
         return NodeManager::currentNM()->mkNode( body.getKind(), newChildren );
       }
+    }
+  }
+  return body;
+}
+
+Node QuantifiersRewriter::computePrenexAgg( Node n ){
+  if( containsQuantifiers( n ) ){
+    if( n.getKind()==NOT ){
+      return computePrenexAgg( n[0] ).negate();
+    }else if( n.getKind()==FORALL ){
+      Node nn = computePrenexAgg( n[1] );
+      if( nn!=n[1] ){
+        if( n.getNumChildren()==2 ){
+          return NodeManager::currentNM()->mkNode( FORALL, n[0], nn );
+        }else{
+          return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] );
+        }
+      }
     }else{
-      return body;
+      std::vector< Node > args;
+      std::vector< Node > nargs;
+      Node nn = computePrenex( n, args, nargs, true );
+      if( n!=nn ){
+        Node nnn = computePrenexAgg( nn );
+        //merge prenex
+        if( nnn.getKind()==FORALL ){
+          for( unsigned i=0; i<nnn[0].getNumChildren(); i++ ){
+            args.push_back( nnn[0][i] );
+          }
+          nnn = nnn[1];
+          //pos polarity variables are inner
+          if( !args.empty() ){
+            nnn = mkForall( args, nnn, true );
+          }
+          args.clear();
+        }else if( nnn.getKind()==NOT && nnn[0].getKind()==FORALL ){
+          for( unsigned i=0; i<nnn[0][0].getNumChildren(); i++ ){
+            nargs.push_back( nnn[0][0][i] );
+          }
+          nnn = nnn[0][1].negate();
+        }
+        if( !nargs.empty() ){
+          nnn = mkForall( nargs, nnn.negate(), true ).negate();
+        }
+        if( !args.empty() ){
+          nnn = mkForall( args, nnn, true );
+        }
+        return nnn;
+      }else{
+        Assert( args.empty() );
+        Assert( nargs.empty() );
+      }
     }
   }
+  return n;
 }
 
 Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) {
@@ -1237,6 +1301,26 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttri
     return NodeManager::currentNM()->mkNode( kind::FORALL, children );
   }
 }
+Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, bool marked ) {
+  if( args.empty() ){
+    return body;
+  }else{
+    std::vector< Node > children;
+    children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
+    children.push_back( body );
+    std::vector< Node > iplc;
+    if( marked ){
+      Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
+      QuantIdNumAttribute ida;
+      avar.setAttribute(ida,0);
+      iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
+    }
+    if( !iplc.empty() ){
+      children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
+    }
+    return NodeManager::currentNM()->mkNode( FORALL, children );
+  }
+}
 
 //computes miniscoping, also eliminates variables that do not occur free in body
 Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){
@@ -1423,7 +1507,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
 
 //general method for computing various rewrites
 Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){
-  Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl;
+  Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl;
   std::vector< Node > args;
   for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
     args.push_back( f[0][i] );
@@ -1432,6 +1516,12 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   if( computeOption==COMPUTE_ELIM_SYMBOLS ){
     n = computeElimSymbols( n );
   }else if( computeOption==COMPUTE_MINISCOPING ){
+    if( options::prenexQuantAgg() ){
+      //if( isPrenexNormalForm( n ) ){
+      if( !qa.d_qid_num.isNull() ){
+        return f;
+      }
+    }
     //return directly
     return computeMiniscoping( args, n, qa );
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
@@ -1446,7 +1536,16 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   }else if( computeOption==COMPUTE_COND_SPLIT ){
     n = computeCondSplit( n, qa );
   }else if( computeOption==COMPUTE_PRENEX ){
-    n = computePrenex( n, args, true );
+    if( options::prenexQuantAgg() ){
+      //Node pf = computePrenexAgg( f );
+      //Assert( isPrenexNormalForm( pf ) );
+      //will do it at preprocess time
+      return f;
+    }else{
+      std::vector< Node > nargs;
+      n = computePrenex( n, args, nargs, true );
+      Assert( nargs.empty() );
+    }
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     n = computeVarElimination( n, args, qa );
   }
@@ -1592,6 +1691,15 @@ bool QuantifiersRewriter::containsQuantifiers( Node n ){
     return cq;
   }
 }
+bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
+  if( n.getKind()==FORALL ){
+    return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] );
+  }else if( n.getKind()==NOT ){
+    return n[0].getKind()!=NOT && isPrenexNormalForm( n[0] );
+  }else{
+    return !containsQuantifiers( n );
+  }
+}
 
 Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){
   Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
@@ -1677,6 +1785,11 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
       }
     }
   }
+  //pull all quantifiers globally
+  if( options::prenexQuantAgg() ){
+    n = quantifiers::QuantifiersRewriter::computePrenexAgg( n );
+    Assert( isPrenexNormalForm( n ) );
+  }
   if( n!=prev ){       
     Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl;
     Trace("quantifiers-preprocess") << "..returned " << n << std::endl;