diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-07 15:22:40 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-07 15:22:50 -0500 |
commit | f62609d9eca8086d5c68b77cfd0a5d717d24aeab (patch) | |
tree | 55b504bf063bcbde7e71be13078e9b9a7df4a984 /src/smt/smt_engine.cpp | |
parent | f9899f4ffc081369f419b8572a5aa397fbaa428a (diff) |
Refactoring of strings preprocess module. When enabled, apply eager preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 08495c936..b76b90e84 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3986,15 +3986,6 @@ 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); - if( !options::stringLazyPreproc() ){ - ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() ); - } - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; - dumpAssertions("post-strings-pp", d_assertions); - } if( d_smt.d_logic.isTheoryEnabled(THEORY_SEP) ) { //separation logic solver needs to register the entire input ((theory::sep::TheorySep*)d_smt.d_theoryEngine->theoryOf(THEORY_SEP))->processAssertions( d_assertions.ref() ); |