Refactor quantifier prenex option. By default, do not pull quantifiers with user patterns.

4 files changed, 44 insertions, 3 deletions

diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 26978c8f9..993ac5536 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -116,6 +116,16 @@ typedef enum {
   TRIGGER_SEL_MAX,
 } TriggerSelMode;
 
+typedef enum {
+  /** default : prenex quantifiers without user patterns */
+  PRENEX_NO_USER_PAT,
+  /** prenex all */
+  PRENEX_ALL,
+  /** prenex none */
+  PRENEX_NONE,
+} PrenexQuantMode;
+
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 162bbc158..872f270e7 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -18,7 +18,7 @@ option miniscopeQuantFreeVar /--disable-miniscope-quant-fv bool :default true
  disable miniscope quantifiers for ground subformulas
 
 # Whether to prenex (nested universal) quantifiers
-option prenexQuant /--disable-prenex-quant bool :default true
+option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
  disable prenexing of quantified formulas
 
 # Whether to variable-eliminate quantifiers.
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 97eaf4aaa..9558aa0e0 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -165,6 +165,19 @@ max \n\
 + Consider only maximal subterms that meet criteria for triggers. \n\
 \n\
 ";
+static const std::string 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\
+";
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
     return INST_WHEN_PRE_FULL;
@@ -309,6 +322,7 @@ inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, S
                           optarg + "'.  Try --user-pat help.");
   }
 }
+
 inline TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg ==  "default" || optarg == "all" ) {
     return TRIGGER_SEL_DEFAULT;
@@ -324,6 +338,23 @@ inline TriggerSelMode stringToTriggerSelMode(std::string option, std::string opt
                           optarg + "'.  Try --trigger-sel help.");
   }
 }
+
+inline PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "default" ) {
+    return PRENEX_NO_USER_PAT;
+  } else if(optarg == "all") {
+    return PRENEX_ALL;
+  } else if(optarg == "none") {
+    return PRENEX_NONE;
+  } else if(optarg ==  "help") {
+    puts(prenexQuantModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --prenex-quant: `") +
+                          optarg + "'.  Try --prenex-quant help.");
+  }
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 754bfacb1..d142007c6 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -577,7 +577,7 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui
 
 Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){
   if( body.getKind()==FORALL ){
-    if( pol ){
+    if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){
       std::vector< Node > terms;
       std::vector< Node > subs;
       //for doing prenexing of same-signed quantifiers
@@ -950,7 +950,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
     return options::simpleIteLiftQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
-    return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
+    return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return options::varElimQuant() || options::dtVarExpandQuant();
   }else if( computeOption==COMPUTE_CNF ){