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 /src | |
parent | caf65a13994dc1d39cc31a8cea76c6a7fddb338c (diff) |
Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)
Diffstat (limited to 'src')
-rw-r--r-- | src/preprocessing/passes/bool_to_bv.cpp | 8 |
1 files changed, 8 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) |