diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 52bc0c4d3..0d473a1a1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -349,7 +349,9 @@ private: */ bool checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache); - + // Lift bit-vectors of size 1 to booleans + void bvToBool(); + // Simplify ITE structure void simpITE(); @@ -1825,11 +1827,15 @@ bool SmtEnginePrivate::nonClausalSimplify() { } hash_set<TNode, TNodeHashFunction> s; + Trace("debugging") << "NonClausal simplify pre-preprocess\n"; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { Node assertion = d_assertionsToPreprocess[i]; Node assertionNew = d_topLevelSubstitutions.apply(assertion); + Trace("debugging") << "assertion = " << assertion << endl; + Trace("debugging") << "assertionNew = " << assertionNew << endl; if (assertion != assertionNew) { assertion = Rewriter::rewrite(assertionNew); + Trace("debugging") << "rewrite(assertion) = " << assertion << endl; } Assert(Rewriter::rewrite(assertion) == assertion); for (;;) { @@ -1838,8 +1844,11 @@ bool SmtEnginePrivate::nonClausalSimplify() { break; } ++d_smt.d_stats->d_numConstantProps; + Trace("debugging") << "assertionNew = " << assertionNew << endl; assertion = Rewriter::rewrite(assertionNew); + Trace("debugging") << "assertionNew = " << assertionNew << endl; } + Trace("debugging") << "\n"; s.insert(assertion); d_assertionsToCheck.push_back(assertion); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " @@ -1927,6 +1936,15 @@ bool SmtEnginePrivate::nonClausalSimplify() { } +void SmtEnginePrivate::bvToBool() { + Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl; + std::vector<Node> new_assertions; + d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]); + } +} + void SmtEnginePrivate::simpITE() { TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); @@ -2780,6 +2798,17 @@ void SmtEnginePrivate::processAssertions() { } dumpAssertions("post-static-learning", d_assertionsToCheck); + // Lift bit-vectors of size 1 to bool + if(options::bvToBool()) { + Chat() << "...doing bvToBool..." << endl; + bvToBool(); + } + + Trace("smt") << "POST bvToBool" << endl; + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + + dumpAssertions("pre-ite-removal", d_assertionsToCheck); { Chat() << "removing term ITEs..." << endl; |