From: lianah Date: Wed, 1 May 2013 17:22:29 +0000 (-0400) Subject: added back BitwiseEq rule X-Git-Tag: cvc5-1.0.0~7292 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=54e6807cec9523a3f5b5279e5a5fce8f9ba4f76a;p=cvc5.git added back BitwiseEq rule --- 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 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::applies(t)) { - // Node result = RewriteRule::run(t); - // return Rewriter::rewrite(result); - // } + if (RewriteRule::applies(t)) { + Node result = RewriteRule::run(t); + return Rewriter::rewrite(result); + } - if (/*options::bitvectorCoreSolver() && */t.getKind() == kind::EQUAL) { + if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { std::vector 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::apply(TNode node) { return result; } - template <> bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLT);