From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 21 Jan 2014 19:40:00 +0000 (-0600)
Subject: Smarter options, but still have a bug
X-Git-Tag: cvc5-1.0.0~7135^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aa578ea6e6487c2fffaa72c600e482ef7ce6035d;p=cvc5.git

Smarter options, but still have a bug
---

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();
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 4a853b6cd..bfb1d6f65 100644
--- 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 6f4355fb6..5ac86dcae 100644
--- 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"