From: lianah Date: Wed, 11 Jun 2014 22:40:02 +0000 (-0400) Subject: switched bv equality order X-Git-Tag: cvc5-1.0.0~6833 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6fa77a772a67897c07615afdc3d95b38087ff741;p=cvc5.git switched bv equality order --- diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index 649af5ff9..43acfef75 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -270,7 +270,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::EQUAL && node[0] > node[1]); + return (node.getKind() == kind::EQUAL && node[0] < node[1]); } template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index b13172bfa..0807b3d66 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -684,7 +684,7 @@ Node RewriteRule::apply(TNode node) { return utils::mkTrue(); } - if (newLeft > newRight) { + if (newLeft < newRight) { Assert((newRight == left && newLeft == right) || Rewriter::rewrite(newRight) != left || Rewriter::rewrite(newLeft) != right); diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 6fd3bbf92..4a0da44cc 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -60,20 +60,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { if(res.node!= node) { Debug("bitvector-rewrite") << "TheoryBV::postRewrite " << node << std::endl; Debug("bitvector-rewrite") << "TheoryBV::postRewrite to " << res.node << std::endl; - if (res.node.getKind() == kind::EQUAL) { - Assert (res.node[0] < res.node[1]); - } - } - if (res.node.getKind() == kind::EQUAL) { - Assert (res.node[0] < res.node[1]); } - - // if (res.status == REWRITE_DONE) { - // Node rewr = res.node; - // Node rerewr = d_rewriteTable[rewr.getKind()](rewr, false).node; - // Assert(rewr == rerewr); - // } - return res; }