From fe9b2276fac81030eb9803d4327f7458bae2576e Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sun, 28 Dec 2014 05:42:28 +0100
Subject: [PATCH] Disable prenex by default when using fmf bound int, minor
 improvement to datatypes rewriter

---
 src/smt/smt_engine.cpp                    |  9 ++++++---
 src/theory/datatypes/datatypes_rewriter.h | 24 +++++++++++++++--------
 src/theory/quantifiers/options            |  2 +-
 test/regress/regress0/bug590.smt2.expect  |  2 +-
 4 files changed, 24 insertions(+), 13 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 918d6f30d..d039377a1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1279,7 +1279,7 @@ void SmtEngine::setDefaults() {
     options::decisionMode.set(decMode);
     options::decisionStopOnly.set(stoponly);
   }
-  //local theory extensions 
+  //local theory extensions
   if( options::localTheoryExt() ){
     //no E-matching?
     if( !options::instMaxLevel.wasSetByUser() ){
@@ -1305,6 +1305,9 @@ void SmtEngine::setDefaults() {
       //if bounded integers are set, use no MBQI by default
       options::mbqiMode.set( quantifiers::MBQI_NONE );
     }
+    if( ! options::prenexQuant.wasSetByUser() ){
+      options::prenexQuant.set( quantifiers::PRENEX_NONE );
+    }
   }
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
@@ -1314,7 +1317,7 @@ void SmtEngine::setDefaults() {
       options::finiteModelFind.set( true );
     }
   }
-  
+
   //now, have determined whether finite model find is on/off
   //apply finite model finding options
   if( options::finiteModelFind() ){
@@ -1340,7 +1343,7 @@ void SmtEngine::setDefaults() {
       }
     }
   }
-  
+
   //implied options...
   if( options::recurseCbqi() ){
     options::cbqi.set( true );
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.
diff --git a/test/regress/regress0/bug590.smt2.expect b/test/regress/regress0/bug590.smt2.expect
index 987ace150..b24a807f7 100644
--- a/test/regress/regress0/bug590.smt2.expect
+++ b/test/regress/regress0/bug590.smt2.expect
@@ -1,2 +1,2 @@
 % EXPECT: unknown
-% EXPECT: ((charlst2 (store ((as const (Array Int String)) "C") 0 "&gt;")))
+% EXPECT: ((charlst2 ((as const (Array Int String)) "")))
-- 
2.30.2