From: lianah <lianahady@gmail.com>
Date: Thu, 12 Jun 2014 13:23:10 +0000 (-0400)
Subject: added bvcomp case to bv to bool lifting
X-Git-Tag: cvc5-1.0.0~6831
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca633914d065d2c9abdc624da10c4eea5c7e0020;p=cvc5.git

added bvcomp case to bv to bool lifting
---

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 72131d6e7..aef1437a0 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -86,7 +86,8 @@ bool BvToBoolPreprocessor::isConvertibleBvTerm(TNode node) {
       kind == kind::BITVECTOR_AND ||
       kind == kind::BITVECTOR_OR ||
       kind == kind::BITVECTOR_NOT ||
-      kind == kind::BITVECTOR_XOR) {
+      kind == kind::BITVECTOR_XOR ||
+      kind == kind::BITVECTOR_COMP) {
     return true; 
   }
 
@@ -156,7 +157,13 @@ Node BvToBoolPreprocessor::convertBvTerm(TNode node) {
     Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; 
     return result; 
   }
-  
+
+  if (kind == kind::BITVECTOR_COMP) {
+    Node result = utils::mkNode(kind::EQUAL, node[0], node[1]);
+    addToBoolCache(node, result);
+    Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; 
+    return result; 
+  }
 
   switch(kind) {
   case kind::BITVECTOR_OR: