From ce883ca9296c872affb47547304a9ecc0ec5224d Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 3 Sep 2016 17:40:18 -0500
Subject: [PATCH] Miniscope top level conjunctions for prenex normal form,
 allow one level miniscoping in prenex normal form.

---
 src/smt/smt_engine.cpp                        |  1 +
 src/theory/quantifiers/inst_strategy_cbqi.cpp |  2 +-
 .../quantifiers/quantifiers_rewriter.cpp      | 54 ++++++++++++++++---
 src/theory/quantifiers/quantifiers_rewriter.h |  2 +-
 4 files changed, 50 insertions(+), 9 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8a636c85e..9c8838113 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1860,6 +1860,7 @@ void SmtEngine::setDefaults() {
   }
   if( options::cbqiNestedQE() ){
     options::prenexQuantAgg.set( true );
+    //options::prenexSkolemQuant.set( true );
   }
   //for induction techniques
   if( options::quantInduction() ){
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 814b276d3..3d4b6a333 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -252,7 +252,7 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
       //  if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
       for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
         Node q = it->first;
-        Trace("cbqi") << "CBQI : Process " << q << " at effort " << ee << std::endl;
+        Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
         if( d_nested_qe.find( q )==d_nested_qe.end() ){
           process( q, e, ee );
           if( d_quantEngine->inConflict() ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 24a6b78b0..672cce959 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1134,12 +1134,23 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s
   return body;
 }
 
-Node QuantifiersRewriter::computePrenexAgg( Node n ){
+Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){
   if( containsQuantifiers( n ) ){
-    if( n.getKind()==NOT ){
-      return computePrenexAgg( n[0] ).negate();
+    if( topLevel && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){
+      std::vector< Node > children;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = computePrenexAgg( n[i], true );
+        if( n.getKind()==NOT ){
+          nc = nc.negate();        
+        }
+        children.push_back( nc );
+      }
+      return NodeManager::currentNM()->mkNode( AND, children );
+    }else if( n.getKind()==NOT ){
+      return computePrenexAgg( n[0], false ).negate();
     }else if( n.getKind()==FORALL ){
-      Node nn = computePrenexAgg( n[1] );
+    /*
+      Node nn = computePrenexAgg( n[1], false );
       if( nn!=n[1] ){
         if( n.getNumChildren()==2 ){
           return NodeManager::currentNM()->mkNode( FORALL, n[0], nn );
@@ -1147,12 +1158,37 @@ Node QuantifiersRewriter::computePrenexAgg( Node n ){
           return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] );
         }
       }
+      */
+      std::vector< Node > children;
+      if( n[1].getKind()==OR ){
+        for( unsigned i=0; i<n[1].getNumChildren(); i++ ){
+          children.push_back( computePrenexAgg( n[1][i], false ) );
+        }
+      }else{
+        children.push_back( computePrenexAgg( n[1], false ) );
+      }
+      std::vector< Node > args;
+      for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+        args.push_back( n[0][i] );
+      }
+      std::vector< Node > nargs;
+      //for each child, strip top level quant
+      for( unsigned i=0; i<children.size(); i++ ){
+        if( children[i].getKind()==FORALL ){
+          for( unsigned j=0; j<children[i][0].getNumChildren(); j++ ){
+            args.push_back( children[i][0][j] );
+          }
+          children[i] = children[i][1];
+        }
+      }
+      Node nb = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+      return mkForall( args, nb, true );
     }else{
       std::vector< Node > args;
       std::vector< Node > nargs;
       Node nn = computePrenex( n, args, nargs, true );
       if( n!=nn ){
-        Node nnn = computePrenexAgg( nn );
+        Node nnn = computePrenexAgg( nn, false );
         //merge prenex
         if( nnn.getKind()==FORALL ){
           for( unsigned i=0; i<nnn[0].getNumChildren(); i++ ){
@@ -1770,6 +1806,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
   return n;
 }
 
+
 Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
   Node prev = n;
   if( n.getKind() == kind::REWRITE_RULE ){
@@ -1787,8 +1824,11 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
   }
   //pull all quantifiers globally
   if( options::prenexQuantAgg() ){
-    n = quantifiers::QuantifiersRewriter::computePrenexAgg( n );
-    Assert( isPrenexNormalForm( n ) );
+    Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl;
+    n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true );
+    n = Rewriter::rewrite( n );
+    Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl;
+    //Assert( isPrenexNormalForm( n ) );
   }
   if( n!=prev ){       
     Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index bb352f65c..2423caaee 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -60,7 +60,7 @@ public:
   static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
   static Node computeCondSplit( Node body, QAttributes& qa );
   static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol );
-  static Node computePrenexAgg( Node n );
+  static Node computePrenexAgg( Node n, bool topLevel );
   static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa );
 private:
-- 
2.30.2