From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Sat, 21 Oct 2017 02:01:51 +0000 (-0700)
Subject: Simplify atoms introduced while bitblasting. (#1267)
X-Git-Tag: cvc5-1.0.0~5545
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7908fd9c901c056628f5f3846049d078d48bc396;p=cvc5.git

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).
---

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 <cmath>
+#include <ostream>
+
 #include "cvc4_private.h"
 #include "expr/node.h"
 #include "theory/bv/bitblast_utils.h"
 #include "theory/bv/theory_bv_utils.h"
-#include <ostream>
-#include <cmath>
+#include "theory/rewriter.h"
+
 namespace CVC4 {
 
 namespace theory {
@@ -538,7 +541,8 @@ void DefaultUdivBB (TNode node, std::vector<T>& q, TBitblaster<T>* 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<T>& rem, TBitblaster<T>* 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<T>& res, TBitblaster<T>* 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<T>& res, TBitblaster<T>* 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<T>& res, TBitblaster<T>* 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);