diff options
| author | lianah <lianahady@gmail.com> | 2014-06-12 09:23:10 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-12 09:23:10 -0400 |
| commit | ca633914d065d2c9abdc624da10c4eea5c7e0020 (patch) | |
| tree | 4cb3bab6fe2e2b595f687be9dfdd5a3acc25bb94 /src/theory/bv | |
| parent | 5899aab331ddec4d1c07387e596e1f1bc495ea94 (diff) | |
added bvcomp case to bv to bool lifting
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 72131d6e7..aef1437a0 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -86,7 +86,8 @@ bool BvToBoolPreprocessor::isConvertibleBvTerm(TNode node) { kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR || kind == kind::BITVECTOR_NOT || - kind == kind::BITVECTOR_XOR) { + kind == kind::BITVECTOR_XOR || + kind == kind::BITVECTOR_COMP) { return true; } @@ -156,7 +157,13 @@ Node BvToBoolPreprocessor::convertBvTerm(TNode node) { Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; return result; } - + + if (kind == kind::BITVECTOR_COMP) { + Node result = utils::mkNode(kind::EQUAL, node[0], node[1]); + addToBoolCache(node, result); + Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; + return result; + } switch(kind) { case kind::BITVECTOR_OR: |