diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-09 15:51:26 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-09 15:51:26 +0200 |
| commit | 3f59801357808a538934b04ce7bf0894dec1b0dd (patch) | |
| tree | 9a32729a077f25fbd7ef2e84825d1e177d29bafd /src/smt | |
| parent | 7443276e61db276e5ba48d605cb6b08a35c5a100 (diff) | |
Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and strings preprocessing. Minor fix for conjecture generation for finite types.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 19 |
1 files changed, 5 insertions, 14 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cb18b8464..25ac4c516 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3165,15 +3165,10 @@ void SmtEnginePrivate::processAssertions() { if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { dumpAssertions("pre-strings-pp", d_assertions); CVC4::theory::strings::StringsPreprocess sp; - std::vector<Node> newNodes; - newNodes.push_back(d_assertions[d_realAssertionsEnd - 1]); - sp.simplify( d_assertions.ref(), newNodes ); - if(newNodes.size() > 1) { - d_assertions[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes); - } - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions[i] = Rewriter::rewrite( d_assertions[i] ); - } + sp.simplify( d_assertions.ref() ); + //for (unsigned i = 0; i < d_assertions.size(); ++ i) { + // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); + //} dumpAssertions("post-strings-pp", d_assertions); } if( d_smt.d_logic.isQuantified() ){ @@ -3182,7 +3177,7 @@ void SmtEnginePrivate::processAssertions() { if( d_assertions[i].getKind() == kind::REWRITE_RULE ){ Node prev = d_assertions[i]; Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl; - d_assertions[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) ); + d_assertions.replace(i, Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) ) ); Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl; Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl; } @@ -3235,10 +3230,6 @@ void SmtEnginePrivate::processAssertions() { } } - //if( options::quantConflictFind() ){ - // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertions ); - //} - if( options::pbRewrites() ){ d_pbsProcessor.learn(d_assertions.ref()); if(d_pbsProcessor.likelyToHelp()){ |