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 511f09a712b8ffb63ec617345919594e28b9e180..f868e37385c4f2c42d85d1ad0a72eec50ba9c8ec 100644 (file)
--- 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 9d336af96ab724ab4a87c336458854b9ad801027..92c7e4117112d54d549cc4f3efbbeb0273bef58b 100644 (file)
--- 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)