diff options
author | lianah <lianahady@gmail.com> | 2014-06-11 18:40:02 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-11 18:40:02 -0400 |
commit | 6fa77a772a67897c07615afdc3d95b38087ff741 (patch) | |
tree | b26897fa6f727129c2eadc6e6a2ccbd4d5ee58ab /src/theory | |
parent | d9c2c9a4c7fb1c213f420715dc546293418b4479 (diff) |
switched bv equality order
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_core.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 13 |
3 files changed, 2 insertions, 15 deletions
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<SimplifyEq>::apply(TNode node) { template<> inline bool RewriteRule<ReflexivityEq>::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<SolveEq>::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; } |