Disable prenex by default when using fmf bound int, minor improvement to datatypes rewriter

2 files changed, 17 insertions, 9 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 02339dc26..90703774b 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -139,24 +139,32 @@ public:
         return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
       }else{
         //typically should not be called
+        TypeNode tn = in.getType();
         Node gt;
-        if( in.getType().isSort() ){
-          TypeEnumerator te(in.getType());
+        if( tn.isSort() ){
+          TypeEnumerator te(tn);
           gt = *te;
-        }else if( dt.isWellFounded() || in[0].isConst() ){
-          gt = in.getType().mkGroundTerm();
+        }else{
+          //check whether well-founded
+          bool isWellFounded = true;
+          if( isTypeDatatype( tn ) ){
+            const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
+            isWellFounded = dta.isWellFounded();
+          }
+          if( isWellFounded || in[0].isConst() ){
+            gt = tn.mkGroundTerm();
+          }
         }
         if( !gt.isNull() ){
-          TypeNode gtt = gt.getType();
           //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
-          if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){
+          if( tn.isDatatype() && !tn.isInstantiatedDatatype() ){
             gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                                  NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
+                                                  NodeManager::currentNM()->mkConst(AscriptionType(tn.toType())), gt);
           }
           Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
                                      << "Rewrite trivial selector " << in
                                      << " to distinguished ground term "
-                                     << in.getType().mkGroundTerm() << std::endl;
+                                     << gt << std::endl;
           return RewriteResponse(REWRITE_DONE,gt );
         }
       }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index a48b009c2..8c43453d7 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -21,7 +21,7 @@ option miniscopeQuantFreeVar /--disable-miniscope-quant-fv bool :default true
  disable miniscope quantifiers for ground subformulas
 
 # Whether to prenex (nested universal) quantifiers
-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"
+option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
  disable prenexing of quantified formulas
 
 # Whether to variable-eliminate quantifiers.