diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 11:05:09 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:59:00 -0600 |
commit | acb79cbe43ddcd855db042b7c937fc2eacaa0ac3 (patch) | |
tree | e8af21bba458cbc2a00d3512519cea3e07af3b65 /src/smt | |
parent | 76f497ef9444a81143ad35b2eda899e119b8e662 (diff) |
a new regular expression engine for solving both positive and negative membership constraints
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9abd6e165..4719af3c0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -793,6 +793,14 @@ 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() ) { @@ -808,11 +816,11 @@ void SmtEngine::finalOptionsAreSet() { 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 ); |