From 7908fd9c901c056628f5f3846049d078d48bc396 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 20 Oct 2017 19:01:51 -0700 Subject: [PATCH] Simplify atoms introduced while bitblasting. (#1267) If a newly introduced atom is not rewritten it can happen that the literals of both the original atom and the rewritten atom end up in the CNF. However, only the original atom has a BB definition and the literal of the rewritten atom is unconstrained (no BB definition). --- src/theory/bv/bitblast_strategies_template.h | 28 +++++++++++++------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h index a93e3416c..e2e176817 100644 --- a/src/theory/bv/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast_strategies_template.h @@ -17,12 +17,15 @@ #ifndef __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H #define __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H +#include +#include + #include "cvc4_private.h" #include "expr/node.h" #include "theory/bv/bitblast_utils.h" #include "theory/bv/theory_bv_utils.h" -#include -#include +#include "theory/rewriter.h" + namespace CVC4 { namespace theory { @@ -538,7 +541,8 @@ void DefaultUdivBB (TNode node, std::vector& q, TBitblaster* bb) { } // cache the remainder in case we need it later - Node remainder = utils::mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]); + Node remainder = Rewriter::rewrite( + utils::mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1])); bb->storeBBTerm(remainder, r); } @@ -566,7 +570,8 @@ void DefaultUremBB (TNode node, std::vector& rem, TBitblaster* bb) { } // cache the quotient in case we need it later - Node quotient = utils::mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]); + Node quotient = Rewriter::rewrite( + utils::mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1])); bb->storeBBTerm(quotient, q); } @@ -602,8 +607,9 @@ void DefaultShlBB (TNode node, std::vector& res, TBitblaster* bb) { // check for b < log2(n) unsigned size = utils::getSize(node); unsigned log2_size = std::ceil(log2((double)size)); - Node a_size = utils::mkConst(BitVector(size, size)); - Node b_ult_a_size_node = utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size); + Node a_size = utils::mkConst(BitVector(size, size)); + Node b_ult_a_size_node = + Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size)); // ensure that the inequality is bit-blasted bb->bbAtom(b_ult_a_size_node); T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); @@ -650,8 +656,9 @@ void DefaultLshrBB (TNode node, std::vector& res, TBitblaster* bb) { // check for b < log2(n) unsigned size = utils::getSize(node); unsigned log2_size = std::ceil(log2((double)size)); - Node a_size = utils::mkConst(BitVector(size, size)); - Node b_ult_a_size_node = utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size); + Node a_size = utils::mkConst(BitVector(size, size)); + Node b_ult_a_size_node = + Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size)); // ensure that the inequality is bit-blasted bb->bbAtom(b_ult_a_size_node); T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); @@ -700,8 +707,9 @@ void DefaultAshrBB (TNode node, std::vector& res, TBitblaster* bb) { // check for b < n unsigned size = utils::getSize(node); unsigned log2_size = std::ceil(log2((double)size)); - Node a_size = utils::mkConst(BitVector(size, size)); - Node b_ult_a_size_node = utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size); + Node a_size = utils::mkConst(BitVector(size, size)); + Node b_ult_a_size_node = + Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size)); // ensure that the inequality is bit-blasted bb->bbAtom(b_ult_a_size_node); T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); -- 2.30.2