diff options
| author | makaimann <makaim@stanford.edu> | 2018-05-21 14:07:48 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-21 14:07:48 -0700 |
| commit | d5e51b2f33773837768a5d89f9be2928f1551d27 (patch) | |
| tree | cea2c17665183e1de534d8238726a28d008fba21 | |
| parent | caf65a13994dc1d39cc31a8cea76c6a7fddb338c (diff) | |
Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)
| -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) |