From: makaimann <makaim@stanford.edu>
Date: Mon, 21 May 2018 21:07:48 +0000 (-0700)
Subject: Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)
X-Git-Tag: cvc5-1.0.0~5030
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d5e51b2f33773837768a5d89f9be2928f1551d27;p=cvc5.git

Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)
---

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index 511f09a71..f868e3738 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -100,6 +100,7 @@ Node BoolToBV::lowerNode(TNode current, bool topLevel)
         case kind::OR: new_kind = kind::BITVECTOR_OR; break;
         case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;
         case kind::XOR: new_kind = kind::BITVECTOR_XOR; break;
+        case kind::IMPLIES: new_kind = kind::BITVECTOR_OR; break;
         case kind::ITE:
           if (current.getType().isBitVector() || current.getType().isBoolean())
           {
@@ -138,6 +139,13 @@ Node BoolToBV::lowerNode(TNode current, bool topLevel)
         converted = lowerNode(current[2]);
         builder << converted;
       }
+      else if (kind == kind::IMPLIES) {
+        // Special-case IMPLIES because needs to be rewritten.
+        converted = lowerNode(current[0]);
+        builder << nm->mkNode(kind::BITVECTOR_NOT, converted);
+        converted = lowerNode(current[1]);
+        builder << converted;
+      }
       else
       {
         for (unsigned i = 0; i < current.getNumChildren(); ++i)
diff --git a/test/regress/regress0/bv/bool-to-bv.smt2 b/test/regress/regress0/bv/bool-to-bv.smt2
index 9d336af96..92c7e4117 100644
--- a/test/regress/regress0/bv/bool-to-bv.smt2
+++ b/test/regress/regress0/bv/bool-to-bv.smt2
@@ -4,6 +4,9 @@
 (declare-fun x2 () (_ BitVec 3))
 (declare-fun x1 () (_ BitVec 3))
 (declare-fun x0 () (_ BitVec 3))
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
 (assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
 (assert (= #b000 x2))
+(assert (=> b1 b2))
 (check-sat)