diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-17 21:09:33 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-17 21:09:33 -0600 |
commit | 84da041c64ef16b95f3028183e1a5a2c994d98ec (patch) | |
tree | 66fc4c0fca3d1ed253a8a6dd4628b44a5fde69da /src/smt/smt_engine.cpp | |
parent | 12794a1a7daae3abe713e77d41bb58d59b061830 (diff) |
bring back the commits which is lost accidentally.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 66 |
1 files changed, 36 insertions, 30 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c1aff6f4b..ac8e5bfe7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -793,6 +793,34 @@ void SmtEngine::finalOptionsAreSet() { return; } + // 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); @@ -943,35 +971,6 @@ void SmtEngine::setLogicInternal() throw() { } } - - // 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(); @@ -3185,11 +3184,18 @@ void SmtEnginePrivate::processAssertions() { // Assertions ARE guaranteed to be rewritten by this point if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + dumpAssertions("pre-strings-pp", d_assertionsToPreprocess); CVC4::theory::strings::StringsPreprocess sp; - sp.simplify( d_assertionsToPreprocess ); + std::vector<Node> newNodes; + newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]); + sp.simplify( d_assertionsToPreprocess, newNodes ); + if(newNodes.size() > 1) { + d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes); + } for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] ); } + dumpAssertions("post-strings-pp", d_assertionsToPreprocess); } if( d_smt.d_logic.isQuantified() ){ dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); |