diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 30 |
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(); |