diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-11 15:35:14 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-11 15:35:14 +0200 |
| commit | c6179b1922e0366acec51eec24a2023d21354030 (patch) | |
| tree | 57804bae2910c556e704b2aa0fc3408ead7897b3 /src/smt/smt_engine.cpp | |
| parent | 9833e6635f6b5bee825034715d15ad73e9955a88 (diff) | |
Fix strings preprocessing + incremental, fixes bug 682. Add initial infrastructure for str.contains inferences.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 337c5104c..a1eca35fa 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -88,7 +88,7 @@ #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/options.h" #include "theory/datatypes/options.h" -#include "theory/strings/theory_strings_preprocess.h" +#include "theory/strings/theory_strings.h" #include "printer/options.h" #include "theory/arith/pseudoboolean_proc.h" @@ -3297,8 +3297,7 @@ void SmtEnginePrivate::processAssertions() { 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() ); + ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() ); //for (unsigned i = 0; i < d_assertions.size(); ++ i) { // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); //} |