Always miniscope nested quantifiers. Disable miniscoping when cegqi enabled. Simplify option names.

4 files changed, 110 insertions, 151 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 71bfcd42b..089fd973e 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -589,7 +589,7 @@ void CegInstantiation::analyzeSygusConjecture( Node q ) {
         d_single_inv_app_map[q][prog] = sinv;
       }
       //construct the single invocation version of the property
-      Trace("cegqi-analyze") << "Single invocation formula is : " << std::endl;
+      Trace("cegqi-analyze") << "Single invocation formula conjuncts are : " << std::endl;
       std::vector< Node > si_conj;
       for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
         std::vector< Node > tmp;
@@ -626,14 +626,14 @@ void CegInstantiation::analyzeSygusConjecture( Node q ) {
             disj.push_back( cr );
           }
           Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj );
-          Trace("cegqi-analyze-debug") << "    " << curr;
+          Trace("cegqi-analyze") << "    " << curr;
           if( it->first.isNull() ){
             si_conj.push_back( curr.negate() );
           }else{
             tmp.push_back( curr );
             Trace("cegqi-analyze-debug") << " under " << it->first;
           }
-          Trace("cegqi-analyze-debug") << std::endl;
+          Trace("cegqi-analyze") << std::endl;
         }
         if( !it->first.isNull() ){
           Assert( !tmp.empty() );
@@ -644,7 +644,7 @@ void CegInstantiation::analyzeSygusConjecture( Node q ) {
         }
       }
       Node si = si_conj.size()==1 ? si_conj[0] : NodeManager::currentNM()->mkNode( OR, si_conj );
-      Trace("cegqi-analyze") << "  " << si << std::endl;
+      Trace("cegqi-analyze-debug") << "...formula is : " << si << std::endl;
       d_single_inv[q] = si;
     }else{
       Trace("cegqi-analyze") << "Property is not single invocation." << std::endl;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index b47c98aa3..6fc13498c 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -11,13 +11,13 @@ option eMatching --e-matching bool :read-write :default true
 # Whether to mini-scope quantifiers.
 # For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
 # ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
-option miniscopeQuant /--disable-miniscope-quant bool :default true
+option miniscopeQuant --miniscope-quant bool :default true :read-write
  disable miniscope quantifiers
 
 # Whether to mini-scope quantifiers based on formulas with no free variables.
 # For example, forall x. ( P( x ) V Q ) will be rewritten to
 # ( forall x. P( x ) ) V Q
-option miniscopeQuantFreeVar /--disable-miniscope-quant-fv bool :default true
+option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
  disable miniscope quantifiers for ground subformulas
 
 # Whether to prenex (nested universal) quantifiers
@@ -27,14 +27,14 @@ option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMod
 # Whether to variable-eliminate quantifiers.
 # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
 #   forall y. P( c, y )
-option varElimQuant /--disable-var-elim-quant bool :default true
+option varElimQuant --var-elim-quant bool :default true
  disable simple variable elimination for quantified formulas
 option dtVarExpandQuant --dt-var-exp-quant bool :default true
  expand datatype variables bound to one constructor in quantifiers
 
 option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
  split variables occurring as conditions of ITE in quantifiers
-option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
+option simpleIteLiftQuant --ite-lift-quant bool :default true
  disable simple ite lifting for quantified formulas
 
 # Whether to CNF quantifier bodies
@@ -65,7 +65,7 @@ option foPropQuant --fo-prop-quant bool :default false
 option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler  CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h"
  which ground terms to consider for instantiation
 # Whether to use smart triggers
-option smartTriggers /--disable-smart-triggers bool :default true
+option smartTriggers --smart-triggers bool :default true
  disable smart triggers
 # Whether to use relevent triggers
 option relevantTriggers --relevant-triggers bool :default false
@@ -123,7 +123,7 @@ option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode
 option flipDecision --flip-decision/ bool :default false
  turns on flip decision heuristic
 
-option internalReps /--disable-quant-internal-reps bool :default true
+option internalReps --quant-internal-reps bool :default true
  disables instantiating with representatives chosen by quantifiers engine
 
 option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
@@ -138,13 +138,13 @@ option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
 
 option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
-option fmfInstGen /--disable-fmf-inst-gen bool :default true
+option fmfInstGen --fmf-inst-gen bool :default true
  disable Inst-Gen instantiation techniques for finite model finding
 option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
  only perform Inst-Gen instantiation techniques on one quantifier per round
 option fmfFreshDistConst --fmf-fresh-dc bool :default false
  use fresh distinguished representative when applying Inst-Gen techniques
-option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
+option fmfFmcSimple --fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
 option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
  finite model finding on bounded integer quantification
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 1e6ec3a02..1f15bb797 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -153,31 +153,9 @@ bool QuantifiersRewriter::hasArg1( Node a, Node n ) {
   }
 }
 
-void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){
-  std::vector< Node > processed;
-  setNestedQuantifiers2( n, q, processed );
-}
-
-void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ) {
-  if( std::find( processed.begin(), processed.end(), n )==processed.end() ){
-    processed.push_back( n );
-    if( n.getKind()==FORALL || n.getKind()==EXISTS ){
-      Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl;
-      NestedQuantAttribute nqai;
-      n[0].setAttribute(nqai,q);
-    }
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      setNestedQuantifiers2( n[i], q, processed );
-    }
-  }
-}
-
 RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
   if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
-    Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in[0].hasAttribute(NestedQuantAttribute()) << std::endl;
-    if( !in.hasAttribute(NestedQuantAttribute()) ){
-      setNestedQuantifiers( in[ 1 ], in );
-    }
+    Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << std::endl;
     std::vector< Node > args;
     for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
       args.push_back( in[0][i] );
@@ -211,7 +189,6 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
       }
       Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
       if( in!=n ){
-        setAttributes( in, n );
         Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
         Trace("quantifiers-pre-rewrite") << " to " << std::endl;
         Trace("quantifiers-pre-rewrite") << n << std::endl;
@@ -224,7 +201,7 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
 
 RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
-  Trace("quantifiers-rewrite-debug") << "Attributes : " << in[0].hasAttribute(NestedQuantAttribute())  << std::endl;
+  Trace("quantifiers-rewrite-debug") << "Attributes : " << std::endl;
   if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){
     RewriteStatus status = REWRITE_DONE;
     Node ret = in;
@@ -250,8 +227,9 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
       ret = ret.negate();
       status = REWRITE_AGAIN_FULL;
     }else{
-      bool isNested = in[0].hasAttribute(NestedQuantAttribute());
       for( int op=0; op<COMPUTE_LAST; op++ ){
+        //TODO : compute isNested (necessary?)
+        bool isNested = false;
         if( doOperation( in, isNested, op ) ){
           ret = computeOperation( in, isNested, op );
           if( ret!=in ){
@@ -263,11 +241,9 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
     }
     //print if changed
     if( in!=ret ){
-      setAttributes( in, ret );
       Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
       Trace("quantifiers-rewrite") << " to " << std::endl;
       Trace("quantifiers-rewrite") << ret << std::endl;
-      //Trace("quantifiers-rewrite-debug") << "Attributes : " << ret[0].hasAttribute(NestedQuantAttribute()) << std::endl;
     }
     return RewriteResponse( status, ret );
   }
@@ -540,14 +516,6 @@ Node QuantifiersRewriter::computeClause( Node n ){
   }
 }
 
-void QuantifiersRewriter::setAttributes( Node in, Node n ) {
-  if( n.getKind()==FORALL && in.getKind()==FORALL ){
-    if( in[0].hasAttribute(NestedQuantAttribute()) ){
-      setNestedQuantifiers( n[0], in[0].getAttribute(NestedQuantAttribute()) );
-    }
-  }
-}
-
 Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){
   if( isLiteral( n ) ){
     return n;
@@ -830,7 +798,7 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node i
   }
 }
 
-Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested ){
+Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ){
   //Notice() << "rewrite quant " << body << std::endl;
   if( body.getKind()==FORALL ){
     //combine arguments
@@ -840,7 +808,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args,
     }
     newArgs.insert( newArgs.end(), args.begin(), args.end() );
     return mkForAll( newArgs, body[ 1 ], ipl );
-  }else if( !isNested ){
+  }else{
     if( body.getKind()==NOT ){
       //push not downwards
       if( body[0].getKind()==NOT ){
@@ -903,108 +871,106 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args,
   //}
 }
 
-Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested ){
-  if( !isNested ){
-    std::map< Node, std::vector< Node > > varLits;
-    std::map< Node, std::vector< Node > > litVars;
-    if( body.getKind()==OR ){
-      Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
-      for( size_t i=0; i<body.getNumChildren(); i++ ){
-        std::vector< Node > activeArgs;
-        computeArgVec( args, activeArgs, body[i] );
-        for (unsigned j=0; j<activeArgs.size(); j++ ){
-          varLits[activeArgs[j]].push_back( body[i] );
-        }
-        litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() );
+Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){
+  std::map< Node, std::vector< Node > > varLits;
+  std::map< Node, std::vector< Node > > litVars;
+  if( body.getKind()==OR ){
+    Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
+    for( size_t i=0; i<body.getNumChildren(); i++ ){
+      std::vector< Node > activeArgs;
+      computeArgVec( args, activeArgs, body[i] );
+      for (unsigned j=0; j<activeArgs.size(); j++ ){
+        varLits[activeArgs[j]].push_back( body[i] );
       }
-      //find the variable in the least number of literals
-      Node bestVar;
-      for( std::map< Node, std::vector< Node > >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
-        if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){
-          bestVar = it->first;
-        }
+      litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() );
+    }
+    //find the variable in the least number of literals
+    Node bestVar;
+    for( std::map< Node, std::vector< Node > >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
+      if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){
+        bestVar = it->first;
       }
-      Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl;
-      if( !bestVar.isNull() && varLits[bestVar].size()<body.getNumChildren() ){
-        //we can miniscope
-        Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
-        //make the bodies
-        std::vector< Node > qlit1;
-        qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() );
-        std::vector< Node > qlitt;
-        //for all literals not containing bestVar
-        for( size_t i=0; i<body.getNumChildren(); i++ ){
-          if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
-            qlitt.push_back( body[i] );
-          }
+    }
+    Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl;
+    if( !bestVar.isNull() && varLits[bestVar].size()<body.getNumChildren() ){
+      //we can miniscope
+      Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
+      //make the bodies
+      std::vector< Node > qlit1;
+      qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() );
+      std::vector< Node > qlitt;
+      //for all literals not containing bestVar
+      for( size_t i=0; i<body.getNumChildren(); i++ ){
+        if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
+          qlitt.push_back( body[i] );
         }
-        //make the variable lists
-        std::vector< Node > qvl1;
-        std::vector< Node > qvl2;
-        std::vector< Node > qvsh;
-        for( unsigned i=0; i<args.size(); i++ ){
-          bool found1 = false;
-          bool found2 = false;
-          for( size_t j=0; j<varLits[args[i]].size(); j++ ){
-            if( !found1 && std::find( qlit1.begin(), qlit1.end(), varLits[args[i]][j] )!=qlit1.end() ){
-              found1 = true;
-            }else if( !found2 && std::find( qlitt.begin(), qlitt.end(), varLits[args[i]][j] )!=qlitt.end() ){
-              found2 = true;
-            }
-            if( found1 && found2 ){
-              break;
-            }
+      }
+      //make the variable lists
+      std::vector< Node > qvl1;
+      std::vector< Node > qvl2;
+      std::vector< Node > qvsh;
+      for( unsigned i=0; i<args.size(); i++ ){
+        bool found1 = false;
+        bool found2 = false;
+        for( size_t j=0; j<varLits[args[i]].size(); j++ ){
+          if( !found1 && std::find( qlit1.begin(), qlit1.end(), varLits[args[i]][j] )!=qlit1.end() ){
+            found1 = true;
+          }else if( !found2 && std::find( qlitt.begin(), qlitt.end(), varLits[args[i]][j] )!=qlitt.end() ){
+            found2 = true;
           }
-          if( found1 ){
-            if( found2 ){
-              qvsh.push_back( args[i] );
-            }else{
-              qvl1.push_back( args[i] );
-            }
-          }else{
-            Assert(found2);
-            qvl2.push_back( args[i] );
+          if( found1 && found2 ){
+            break;
           }
         }
-        Assert( !qvl1.empty() );
-        Assert( !qvl2.empty() || !qvsh.empty() );
-        //check for literals that only contain shared variables
-        std::vector< Node > qlitsh;
-        std::vector< Node > qlit2;
-        for( size_t i=0; i<qlitt.size(); i++ ){
-          bool hasVar2 = false;
-          for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
-            if( std::find( qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j] )!=qvl2.end() ){
-              hasVar2 = true;
-              break;
-            }
-          }
-          if( hasVar2 ){
-            qlit2.push_back( qlitt[i] );
+        if( found1 ){
+          if( found2 ){
+            qvsh.push_back( args[i] );
           }else{
-            qlitsh.push_back( qlitt[i] );
+            qvl1.push_back( args[i] );
           }
+        }else{
+          Assert(found2);
+          qvl2.push_back( args[i] );
         }
-        varLits.clear();
-        litVars.clear();
-        Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size();
-        Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl;
-        Node n1 = qlit1.size()==1 ? qlit1[0] : NodeManager::currentNM()->mkNode( OR, qlit1 );
-        n1 = computeAggressiveMiniscoping( qvl1, n1 );
-        qlitsh.push_back( n1 );
-        if( !qlit2.empty() ){
-          Node n2 = qlit2.size()==1 ? qlit2[0] : NodeManager::currentNM()->mkNode( OR, qlit2 );
-          n2 = computeAggressiveMiniscoping( qvl2, n2 );
-          qlitsh.push_back( n2 );
+      }
+      Assert( !qvl1.empty() );
+      Assert( !qvl2.empty() || !qvsh.empty() );
+      //check for literals that only contain shared variables
+      std::vector< Node > qlitsh;
+      std::vector< Node > qlit2;
+      for( size_t i=0; i<qlitt.size(); i++ ){
+        bool hasVar2 = false;
+        for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
+          if( std::find( qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j] )!=qvl2.end() ){
+            hasVar2 = true;
+            break;
+          }
         }
-        Node n = NodeManager::currentNM()->mkNode( OR, qlitsh );
-        if( !qvsh.empty() ){
-          Node bvl = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qvsh);
-          n = NodeManager::currentNM()->mkNode( FORALL, bvl, n );
+        if( hasVar2 ){
+          qlit2.push_back( qlitt[i] );
+        }else{
+          qlitsh.push_back( qlitt[i] );
         }
-        Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl;
-        return n;
       }
+      varLits.clear();
+      litVars.clear();
+      Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size();
+      Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl;
+      Node n1 = qlit1.size()==1 ? qlit1[0] : NodeManager::currentNM()->mkNode( OR, qlit1 );
+      n1 = computeAggressiveMiniscoping( qvl1, n1 );
+      qlitsh.push_back( n1 );
+      if( !qlit2.empty() ){
+        Node n2 = qlit2.size()==1 ? qlit2[0] : NodeManager::currentNM()->mkNode( OR, qlit2 );
+        n2 = computeAggressiveMiniscoping( qvl2, n2 );
+        qlitsh.push_back( n2 );
+      }
+      Node n = NodeManager::currentNM()->mkNode( OR, qlitsh );
+      if( !qvsh.empty() ){
+        Node bvl = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qvsh);
+        n = NodeManager::currentNM()->mkNode( FORALL, bvl, n );
+      }
+      Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl;
+      return n;
     }
   }
   return mkForAll( args, body, Node::null() );
@@ -1068,9 +1034,9 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
       n = computeElimSymbols( n );
     }else if( computeOption==COMPUTE_MINISCOPING ){
       //return directly
-      return computeMiniscoping( f, args, n, ipl, isNested );
+      return computeMiniscoping( f, args, n, ipl );
     }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
-      return computeAggressiveMiniscoping( args, n, isNested );
+      return computeAggressiveMiniscoping( args, n );
     }else if( computeOption==COMPUTE_NNF ){
       n = computeNNF( n );
     }else if( computeOption==COMPUTE_PROCESS_ITE ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index badf97c46..7c57c6d60 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -26,10 +26,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-// attribute for "contains instantiation constants from"
-struct NestedQuantAttributeId {};
-typedef expr::Attribute<NestedQuantAttributeId, Node> NestedQuantAttribute;
-
 class QuantifiersRewriter {
 public:
   static bool isClause( Node n );
@@ -43,14 +39,11 @@ private:
   static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
   static bool hasArg( std::vector< Node >& args, Node n );
   static bool hasArg1( Node a, Node n );
-  static void setNestedQuantifiers( Node n, Node q );
-  static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed );
   static Node computeClause( Node n );
-  static void setAttributes( Node in, Node n );
 private:
   static Node computeElimSymbols( Node body );
-  static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested = false );
-  static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false );
+  static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
+  static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   static Node computeNNF( Node body );
   static Node computeProcessIte( Node body, bool hasPol, bool pol );
   static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );