From ca633914d065d2c9abdc624da10c4eea5c7e0020 Mon Sep 17 00:00:00 2001 From: lianah Date: Thu, 12 Jun 2014 09:23:10 -0400 Subject: [PATCH] added bvcomp case to bv to bool lifting --- src/theory/bv/bv_to_bool.cpp | 11 +++++++++-- 1 file 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: -- 2.30.2