Smarter options, but still have a bug

1 files changed, 30 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 406db286f..4e0ea51a6 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -64,6 +64,7 @@
 #include "theory/substitutions.h"
 #include "theory/uf/options.h"
 #include "theory/arith/options.h"
+#include "theory/strings/options.h"
 #include "theory/bv/options.h"
 #include "theory/theory_traits.h"
 #include "theory/logic_info.h"
@@ -941,6 +942,35 @@ void SmtEngine::setLogicInternal() throw() {
     }
   }
 
+
+  //for strings
+  if(options::stringExp.wasSetByUser()) {
+	  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;
+		  //exception
+		  //throw OptionException("The string-exp option requires quantifier option. One suggestion is UFSLIA.");
+	  }
+	  if(! options::finiteModelFind.wasSetByUser()) {
+		  //exception
+		  throw OptionException("The string-exp option requires finite-model-find option.");
+		  //options::finiteModelFind.set( true );
+		  //Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
+	  }
+	  if(! options::fmfBoundInt.wasSetByUser()) {
+		  //exception
+		  throw OptionException("The string-exp option requires fmf-bound-int option.");
+		  //options::fmfBoundInt.set( true );
+		  //Trace("smt") << "turning on fmf-bound-int, 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();