diff options
| -rw-r--r-- | src/preprocessing/passes/bool_to_bv.cpp | 8 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bool-to-bv.smt2 | 3 |
2 files changed, 11 insertions, 0 deletions
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) |