diff options
author | lianah <lianahady@gmail.com> | 2013-05-01 13:22:29 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-05-01 13:22:29 -0400 |
commit | 54e6807cec9523a3f5b5279e5a5fce8f9ba4f76a (patch) | |
tree | c523bcd8f43de72ac937057657a096265dc7ed9b /src | |
parent | db93834744ae5e1c93404e6236e1b46348037770 (diff) |
added back BitwiseEq rule
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 1 |
3 files changed, 12 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bc89e8d44..78f6e3dae 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1822,11 +1822,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 (;;) { @@ -1835,8 +1839,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(): " diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index b2f91e070..6f450d08e 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -284,12 +284,12 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu Node TheoryBV::ppRewrite(TNode t) { - // if (RewriteRule<BitwiseEq>::applies(t)) { - // Node result = RewriteRule<BitwiseEq>::run<false>(t); - // return Rewriter::rewrite(result); - // } + if (RewriteRule<BitwiseEq>::applies(t)) { + Node result = RewriteRule<BitwiseEq>::run<false>(t); + return Rewriter::rewrite(result); + } - if (/*options::bitvectorCoreSolver() && */t.getKind() == kind::EQUAL) { + if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { std::vector<Node> equalities; Slicer::splitEqualities(t, equalities); return utils::mkAnd(equalities); diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index a63721de1..626116453 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -85,7 +85,6 @@ Node RewriteRule<SgeEliminate>::apply(TNode node) { return result; } - template <> bool RewriteRule<SltEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLT); |