From: lianah <lianahady@gmail.com>
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<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; 
 }