Refactor prenex modes.

6 files changed, 54 insertions, 43 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 8cd651da5..1d7355d9f 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -385,15 +385,18 @@ max \n\
 const std::string OptionsHandler::s_prenexQuantModeHelp = "\
 Prenex quantifiers modes currently supported by the --prenex-quant option:\n\
 \n\
-default \n\
-+ Default, prenex all nested quantifiers except those with user patterns.\n\
-\n\
-all \n\
-+ Prenex all nested quantifiers.\n\
-\n\
 none \n\
 + Do no prenex nested quantifiers. \n\
 \n\
+default | simple \n\
++ Default, do simple prenexing of same sign quantifiers.\n\
+\n\
+dnorm \n\
++ Prenex to disjunctive prenex normal form.\n\
+\n\
+norm \n\
++ Prenex to prenex normal form.\n\
+\n\
 ";
 
 const std::string OptionsHandler::s_cegqiFairModeHelp = "\
@@ -679,12 +682,14 @@ theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveS
 }
 
 theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) {
-  if(optarg ==  "default" ) {
-    return theory::quantifiers::PRENEX_NO_USER_PAT;
-  } else if(optarg == "all") {
-    return theory::quantifiers::PRENEX_ALL;
+  if(optarg== "default" || optarg== "simple" ) {
+    return theory::quantifiers::PRENEX_QUANT_SIMPLE;
   } else if(optarg == "none") {
-    return theory::quantifiers::PRENEX_NONE;
+    return theory::quantifiers::PRENEX_QUANT_NONE;
+  } else if(optarg == "dnorm") {
+    return theory::quantifiers::PRENEX_QUANT_DISJ_NORMAL;
+  } else if(optarg == "norm") {
+    return theory::quantifiers::PRENEX_QUANT_NORMAL;
   } else if(optarg ==  "help") {
     puts(s_prenexQuantModeHelp.c_str());
     exit(1);
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index fe76f8798..cc6abaa8b 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -123,12 +123,14 @@ enum TriggerActiveSelMode {
 };
 
 enum CVC4_PUBLIC PrenexQuantMode {
-  /** default : prenex quantifiers without user patterns */
-  PRENEX_NO_USER_PAT,
-  /** prenex all */
-  PRENEX_ALL,
-  /** prenex none */
-  PRENEX_NONE,
+  /** do not prenex */
+  PRENEX_QUANT_NONE,
+  /** prenex same sign quantifiers */
+  PRENEX_QUANT_SIMPLE,
+  /** aggressive prenex, disjunctive prenex normal form */
+  PRENEX_QUANT_DISJ_NORMAL,
+  /** prenex normal form */
+  PRENEX_QUANT_NORMAL,
 };
 
 enum CegqiFairMode {
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 2e9aa00cc..04b918afc 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -19,10 +19,10 @@ option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
  miniscope quantifiers for ground subformulas
 option quantSplit --quant-split bool :default true :read-write
  apply splitting to quantified formulas based on variable disjoint disjuncts
-option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode
+option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode
  prenex mode for quantified formulas
-option prenexQuantAgg --prenex-quant-agg bool :default false :read-write
- aggressive prenexing to ensure prenex normal form
+option prenexQuantUser --prenex-quant-user bool :default false :read-write
+ prenex quantified formulas with user patterns
 # 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 )
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c9f80c2aa..b7997a204 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1732,7 +1732,7 @@ void SmtEngine::setDefaults() {
       options::mbqiMode.set( quantifiers::MBQI_NONE );
     }
     if( ! options::prenexQuant.wasSetByUser() ){
-      options::prenexQuant.set( quantifiers::PRENEX_NONE );
+      options::prenexQuant.set( quantifiers::PRENEX_QUANT_NONE );
     }
   }
   if( options::ufssSymBreak() ){
@@ -1856,8 +1856,14 @@ void SmtEngine::setDefaults() {
     options::quantConflictFind.set( true );
   }
   if( options::cbqiNestedQE() ){
-    options::prenexQuantAgg.set( true );
-    //options::prenexSkolemQuant.set( true );
+    //only sound with prenex = disj_normal or normal
+    if( options::prenexQuant()<=quantifiers::PRENEX_QUANT_DISJ_NORMAL ){
+      options::prenexQuant.set( quantifiers::PRENEX_QUANT_DISJ_NORMAL );
+    }
+    options::prenexQuantUser.set( true );
+    if( !options::preSkolemQuant.wasSetByUser() ){
+      options::preSkolemQuant.set( true );
+    }
   }
   //for induction techniques
   if( options::quantInduction() ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 672cce959..3bf7749a4 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, std::vector< Node >& nargs, bool pol ){
+Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ){
   if( body.getKind()==FORALL ){
-    if( ( pol || options::prenexQuantAgg() ) && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){
+    if( ( pol || prenexAgg ) && ( options::prenexQuantUser() || body.getNumChildren()==2 ) ){
       std::vector< Node > terms;
       std::vector< Node > subs;
       //for doing prenexing of same-signed quantifiers
@@ -1095,16 +1095,16 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s
       return newBody;
     }
   //must remove structure
-  }else if( options::prenexQuantAgg() && body.getKind()==kind::ITE && body.getType().isBoolean() ){
+  }else if( prenexAgg && 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 ){
+    return computePrenex( nn, args, nargs, pol, prenexAgg );
+  }else if( prenexAgg && 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 );
+    return computePrenex( nn, args, nargs, pol, prenexAgg );
   }else if( body.getType().isBoolean() ){
     Assert( body.getKind()!=EXISTS );
     bool childrenChanged = false;
@@ -1114,7 +1114,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s
       bool newPol;
       QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol );
       if( newHasPol ){
-        Node n = computePrenex( body[i], args, nargs, newPol );
+        Node n = computePrenex( body[i], args, nargs, newPol, prenexAgg );
         newChildren.push_back( n );
         if( n!=body[i] ){
           childrenChanged = true;
@@ -1136,7 +1136,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s
 
 Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){
   if( containsQuantifiers( n ) ){
-    if( topLevel && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){
+    if( topLevel && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL && ( 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 );
@@ -1160,7 +1160,7 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){
       }
       */
       std::vector< Node > children;
-      if( n[1].getKind()==OR ){
+      if( n[1].getKind()==OR && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL ){
         for( unsigned i=0; i<n[1].getNumChildren(); i++ ){
           children.push_back( computePrenexAgg( n[1][i], false ) );
         }
@@ -1186,7 +1186,7 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){
     }else{
       std::vector< Node > args;
       std::vector< Node > nargs;
-      Node nn = computePrenex( n, args, nargs, true );
+      Node nn = computePrenex( n, args, nargs, true, true );
       if( n!=nn ){
         Node nnn = computePrenexAgg( nn, false );
         //merge prenex
@@ -1533,7 +1533,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
   }else if( computeOption==COMPUTE_COND_SPLIT ){
     return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger;
   }else if( computeOption==COMPUTE_PRENEX ){
-    return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std;
+    return options::prenexQuant()!=PRENEX_QUANT_NONE && !options::aggressiveMiniscopeQuant() && is_std;
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return ( options::varElimQuant() || options::dtVarExpandQuant() ) && is_std;
   }else{
@@ -1552,9 +1552,9 @@ 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( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
       if( !qa.d_qid_num.isNull() ){
+        //already processed this, return self
         return f;
       }
     }
@@ -1572,14 +1572,12 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   }else if( computeOption==COMPUTE_COND_SPLIT ){
     n = computeCondSplit( n, qa );
   }else if( computeOption==COMPUTE_PRENEX ){
-    if( options::prenexQuantAgg() ){
-      //Node pf = computePrenexAgg( f );
-      //Assert( isPrenexNormalForm( pf ) );
-      //will do it at preprocess time
+    if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
+      //will rewrite at preprocess time
       return f;
     }else{
       std::vector< Node > nargs;
-      n = computePrenex( n, args, nargs, true );
+      n = computePrenex( n, args, nargs, true, false );
       Assert( nargs.empty() );
     }
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
@@ -1823,7 +1821,7 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
     }
   }
   //pull all quantifiers globally
-  if( options::prenexQuantAgg() ){
+  if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
     Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl;
     n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true );
     n = Rewriter::rewrite( n );
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 2423caaee..90a22f4b7 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -59,7 +59,7 @@ public:
   //cache is dependent upon currCond, icache is not, new_conds are negated conditions
   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 computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg );
   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 );