diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-06 17:06:12 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-07 15:03:45 -0600 |
commit | 2594dfe76830d3e03aedf6bc3310bce6d362e4eb (patch) | |
tree | 96a89e2c893929df35527967a86a454bf288b14f /src/smt | |
parent | f854915d23418dbbf805db91ba3cde8204846219 (diff) |
Fix strings-exp setting.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 71 |
1 files changed, 35 insertions, 36 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4719af3c0..02542b640 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -793,42 +793,6 @@ void SmtEngine::finalOptionsAreSet() { return; } - // 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(); - 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()) { - 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; - } - */ - } - if(options::bitvectorEagerBitblast()) { // Eager solver should use the internal decision strategy options::decisionMode.set(DECISION_STRATEGY_INTERNAL); @@ -979,6 +943,41 @@ void SmtEngine::setLogicInternal() throw() { } } + // 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()) { + 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(); |