diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-26 14:35:40 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-26 14:35:40 +0200 |
| commit | 51aa945e59ecf3354192f40c3f645d8b221e34a9 (patch) | |
| tree | efd08ada86eaaefe42f371a6744dcf681266e6a6 /src/smt | |
| parent | e61a79df77924c66e8f6ff3141172bda49301475 (diff) | |
Lazy preprocessing of extended operators in strings. Add regressions. Fixes bug 613.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 519f330df..ae93176b2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3294,17 +3294,18 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-bv-to-bool", d_assertions); Trace("smt") << "POST bvToBool" << endl; } - - if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl; - dumpAssertions("pre-strings-pp", d_assertions); - CVC4::theory::strings::StringsPreprocess sp; - sp.simplify( d_assertions.ref() ); - //for (unsigned i = 0; i < d_assertions.size(); ++ i) { - // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); - //} - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; - dumpAssertions("post-strings-pp", d_assertions); + if( !options::stringLazyPreproc() ){ + if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl; + dumpAssertions("pre-strings-pp", d_assertions); + CVC4::theory::strings::StringsPreprocess sp; + sp.simplify( d_assertions.ref() ); + //for (unsigned i = 0; i < d_assertions.size(); ++ i) { + // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); + //} + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; + dumpAssertions("post-strings-pp", d_assertions); + } } if( d_smt.d_logic.isQuantified() ){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; |