Smarter options, but still have a bug

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 406db286fd1efa3e3fb596594e83b48969aebc3c..4e0ea51a612b8aa0ca569f560e1cbd236246171b 100644 (file)
--- 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();

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 4a853b6cdbd4d0d22a44784cc943b14491fa37e7..bfb1d6f6548f911f81f04de2e476ba1c27dfd288 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -91,7 +91,7 @@ option flipDecision --flip-decision/ bool :default false
 option internalReps /--disable-quant-internal-reps bool :default true
  disables instantiating with representatives chosen by quantifiers engine
 
-option finiteModelFind --finite-model-find bool :default false
+option finiteModelFind --finite-model-find bool :default false :read-write
  use finite model finding heuristic for quantifier instantiation
 
 option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
@@ -113,7 +113,7 @@ option fmfFreshDistConst --fmf-fresh-dc bool :default false
  use fresh distinguished representative when applying Inst-Gen techniques
 option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
-option fmfBoundInt --fmf-bound-int bool :default false
+option fmfBoundInt --fmf-bound-int bool :default false :read-write
  finite model finding on bounded integer quantification
 
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"

diff --git a/src/theory/strings/options b/src/theory/strings/options
index 6f4355fb6045b356c6261ee7ec9b309cc23e24eb..5ac86dcae844c35c749777e690f2a074a80e19a0 100644 (file)
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -11,7 +11,7 @@ option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int
 option stringRegExpUnrollDepth strings-regexp-depth --strings-regexp-depth=N int16_t :default 10 :read-write
  the depth of unrolloing regular expression used by the theory of strings, default 10
 
-option stringFMF strings-fmf --strings-fmf bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
+option stringFMF strings-fmf --strings-fmf bool :default false :read-write
  the finite model finding used by the theory of strings
 
 option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate less_equal(2) :predicate-include "smt/smt_engine.h"