From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 25 Jun 2014 20:35:27 +0000 (-0400)
Subject: Turn strings-exp off by default (for the release)
X-Git-Tag: cvc5-1.0.0~6710^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6782c2ba8ec393c059a56949971ec6373bd907dd;p=cvc5.git

Turn strings-exp off by default (for the release)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8938cd769..61fdfb8c0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -872,12 +872,14 @@ void SmtEngine::setDefaults() {
   }
 
   // set strings-exp
+  /* - disabled for 1.4 release [MGD 2014.06.25]
   if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
     if(! options::stringExp.wasSetByUser()) {
       options::stringExp.set( true );
       Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
     }
   }
+  */
   // for strings
   if(options::stringExp()) {
     if( !d_logic.isQuantified() ) {
@@ -891,6 +893,9 @@ void SmtEngine::setDefaults() {
       Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
     }
     if(! options::fmfBoundInt.wasSetByUser()) {
+      if(! options::fmfBoundIntLazy.wasSetByUser()) {
+        options::fmfBoundIntLazy.set( true );
+      }
       options::fmfBoundInt.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
@@ -927,44 +932,6 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  // set strings-exp
-  if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS)) {
-    if(! options::stringExp.wasSetByUser()) {
-      options::stringExp.set(true);
-      Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
-    }
-  }
-  // for strings
-  if(options::stringExp()) {
-    if( !d_logic.isQuantified() ) {
-      d_logic = d_logic.getUnlockedCopy();
-      d_logic.enableQuantifiers();
-      d_logic.lock();
-      Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl;
-    }
-    if(! options::finiteModelFind.wasSetByUser()) {
-      options::finiteModelFind.set( true );
-      Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
-    }
-    if(! options::fmfBoundInt.wasSetByUser()) {
-      if(! options::fmfBoundIntLazy.wasSetByUser()) {
-        options::fmfBoundIntLazy.set( true );
-      }
-      options::fmfBoundInt.set( true );
-      Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
-    }
-        /*
-    if(! options::rewriteDivk.wasSetByUser()) {
-      options::rewriteDivk.set( true );
-      Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
-    }*/
-    /*
-    if(! options::stringFMF.wasSetByUser()) {
-      options::stringFMF.set( true );
-      Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
-    }
-    */
-  }
   // by default, symmetry breaker is on only for QF_UF
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
     bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
diff --git a/test/regress/regress0/strings/artemis-0512-nonterm.smt2 b/test/regress/regress0/strings/artemis-0512-nonterm.smt2
index ed97f36dd..4b1cad8f6 100644
--- a/test/regress/regress0/strings/artemis-0512-nonterm.smt2
+++ b/test/regress/regress0/strings/artemis-0512-nonterm.smt2
@@ -1,4 +1,5 @@
 (set-logic QF_S)
+(set-option :strings-exp true)
 (set-info :status unsat)
 
 (declare-const Y String)
diff --git a/test/regress/regress0/strings/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2
index 3987c92ac..ae61b5f5b 100644
--- a/test/regress/regress0/strings/leadingzero001.smt2
+++ b/test/regress/regress0/strings/leadingzero001.smt2
@@ -1,4 +1,5 @@
 (set-logic QF_S)
+(set-option :strings-exp true)
 (set-info :status sat)
 
 (declare-fun Y () String)
diff --git a/test/regress/regress0/strings/reloop.smt2 b/test/regress/regress0/strings/reloop.smt2
index f54607121..39b2b76b1 100644
--- a/test/regress/regress0/strings/reloop.smt2
+++ b/test/regress/regress0/strings/reloop.smt2
@@ -1,4 +1,5 @@
 (set-logic QF_S)
+(set-option :strings-exp true)
 (set-info :status sat)
 
 (declare-fun x () String)