1 /********************* */
2 /*! \file bv_to_bool.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Yoni Zohar, Liana Hadarean, Aina Niemetz
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans.
13 **
14 ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
15 **/
16
17 #include "preprocessing/passes/bv_to_bool.h"
18
19 #include <string>
20 #include <unordered_map>
21 #include <vector>
22
23 #include "expr/node.h"
24 #include "smt/smt_statistics_registry.h"
25 #include "smt_util/node_visitor.h"
26 #include "theory/rewriter.h"
27 #include "theory/theory.h"
28
29 namespace CVC4 {
30 namespace preprocessing {
31 namespace passes {
32
33 using namespace std;
34 using namespace CVC4::theory;
35
BVToBool(PreprocessingPassContext * preprocContext)36 BVToBool::BVToBool(PreprocessingPassContext* preprocContext)
37 : PreprocessingPass(preprocContext, "bv-to-bool"),
38 d_liftCache(),
39 d_boolCache(),
40 d_one(bv::utils::mkOne(1)),
41 d_zero(bv::utils::mkZero(1)),
42 d_statistics(){};
43
applyInternal(AssertionPipeline * assertionsToPreprocess)44 PreprocessingPassResult BVToBool::applyInternal(
45 AssertionPipeline* assertionsToPreprocess)
46 {
47 NodeManager::currentResourceManager()->spendResource(
48 options::preprocessStep());
49 std::vector<Node> new_assertions;
50 liftBvToBool(assertionsToPreprocess->ref(), new_assertions);
51 for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
52 {
53 assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i]));
54 }
55 return PreprocessingPassResult::NO_CONFLICT;
56 }
57
addToLiftCache(TNode term,Node new_term)58 void BVToBool::addToLiftCache(TNode term, Node new_term)
59 {
60 Assert(new_term != Node());
61 Assert(!hasLiftCache(term));
62 Assert(term.getType() == new_term.getType());
63 d_liftCache[term] = new_term;
64 }
65
getLiftCache(TNode term) const66 Node BVToBool::getLiftCache(TNode term) const
67 {
68 Assert(hasLiftCache(term));
69 return d_liftCache.find(term)->second;
70 }
71
hasLiftCache(TNode term) const72 bool BVToBool::hasLiftCache(TNode term) const
73 {
74 return d_liftCache.find(term) != d_liftCache.end();
75 }
76
addToBoolCache(TNode term,Node new_term)77 void BVToBool::addToBoolCache(TNode term, Node new_term)
78 {
79 Assert(new_term != Node());
80 Assert(!hasBoolCache(term));
81 Assert(bv::utils::getSize(term) == 1);
82 Assert(new_term.getType().isBoolean());
83 d_boolCache[term] = new_term;
84 }
85
getBoolCache(TNode term) const86 Node BVToBool::getBoolCache(TNode term) const
87 {
88 Assert(hasBoolCache(term));
89 return d_boolCache.find(term)->second;
90 }
91
hasBoolCache(TNode term) const92 bool BVToBool::hasBoolCache(TNode term) const
93 {
94 return d_boolCache.find(term) != d_boolCache.end();
95 }
isConvertibleBvAtom(TNode node)96 bool BVToBool::isConvertibleBvAtom(TNode node)
97 {
98 Kind kind = node.getKind();
99 return (kind == kind::EQUAL && node[0].getType().isBitVector()
100 && node[0].getType().getBitVectorSize() == 1
101 && node[1].getType().isBitVector()
102 && node[1].getType().getBitVectorSize() == 1
103 && node[0].getKind() != kind::BITVECTOR_EXTRACT
104 && node[1].getKind() != kind::BITVECTOR_EXTRACT);
105 }
106
isConvertibleBvTerm(TNode node)107 bool BVToBool::isConvertibleBvTerm(TNode node)
108 {
109 if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1)
110 return false;
111
112 Kind kind = node.getKind();
113
114 if (kind == kind::CONST_BITVECTOR || kind == kind::ITE
115 || kind == kind::BITVECTOR_AND
116 || kind == kind::BITVECTOR_OR
117 || kind == kind::BITVECTOR_NOT
118 || kind == kind::BITVECTOR_XOR
119 || kind == kind::BITVECTOR_COMP)
120 {
121 return true;
122 }
123
124 return false;
125 }
126
convertBvAtom(TNode node)127 Node BVToBool::convertBvAtom(TNode node)
128 {
129 Assert(node.getType().isBoolean() && node.getKind() == kind::EQUAL);
130 Assert(bv::utils::getSize(node[0]) == 1);
131 Assert(bv::utils::getSize(node[1]) == 1);
132 Node a = convertBvTerm(node[0]);
133 Node b = convertBvTerm(node[1]);
134 Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
135 Debug("bv-to-bool") << "BVToBool::convertBvAtom " << node << " => " << result
136 << "\n";
137
138 ++(d_statistics.d_numAtomsLifted);
139 return result;
140 }
141
convertBvTerm(TNode node)142 Node BVToBool::convertBvTerm(TNode node)
143 {
144 Assert(node.getType().isBitVector()
145 && node.getType().getBitVectorSize() == 1);
146
147 if (hasBoolCache(node)) return getBoolCache(node);
148
149 NodeManager* nm = NodeManager::currentNM();
150
151 if (!isConvertibleBvTerm(node))
152 {
153 ++(d_statistics.d_numTermsForcedLifted);
154 Node result = nm->mkNode(kind::EQUAL, node, d_one);
155 addToBoolCache(node, result);
156 Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
157 << result << "\n";
158 return result;
159 }
160
161 if (node.getNumChildren() == 0)
162 {
163 Assert(node.getKind() == kind::CONST_BITVECTOR);
164 Node result = node == d_one ? bv::utils::mkTrue() : bv::utils::mkFalse();
165 // addToCache(node, result);
166 Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
167 << result << "\n";
168 return result;
169 }
170
171 ++(d_statistics.d_numTermsLifted);
172
173 Kind kind = node.getKind();
174 if (kind == kind::ITE)
175 {
176 Node cond = liftNode(node[0]);
177 Node true_branch = convertBvTerm(node[1]);
178 Node false_branch = convertBvTerm(node[2]);
179 Node result = nm->mkNode(kind::ITE, cond, true_branch, false_branch);
180 addToBoolCache(node, result);
181 Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
182 << result << "\n";
183 return result;
184 }
185
186 Kind new_kind;
187 // special case for XOR as it has to be binary
188 // while BITVECTOR_XOR can be n-ary
189 if (kind == kind::BITVECTOR_XOR)
190 {
191 new_kind = kind::XOR;
192 Node result = convertBvTerm(node[0]);
193 for (unsigned i = 1; i < node.getNumChildren(); ++i)
194 {
195 Node converted = convertBvTerm(node[i]);
196 result = nm->mkNode(kind::XOR, result, converted);
197 }
198 Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
199 << result << "\n";
200 return result;
201 }
202
203 if (kind == kind::BITVECTOR_COMP)
204 {
205 Node result = nm->mkNode(kind::EQUAL, node[0], node[1]);
206 addToBoolCache(node, result);
207 Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
208 << result << "\n";
209 return result;
210 }
211
212 switch (kind)
213 {
214 case kind::BITVECTOR_OR: new_kind = kind::OR; break;
215 case kind::BITVECTOR_AND: new_kind = kind::AND; break;
216 case kind::BITVECTOR_NOT: new_kind = kind::NOT; break;
217 default: Unhandled();
218 }
219
220 NodeBuilder<> builder(new_kind);
221 for (unsigned i = 0; i < node.getNumChildren(); ++i)
222 {
223 builder << convertBvTerm(node[i]);
224 }
225
226 Node result = builder;
227 addToBoolCache(node, result);
228 Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => " << result
229 << "\n";
230 return result;
231 }
232
liftNode(TNode current)233 Node BVToBool::liftNode(TNode current)
234 {
235 Node result;
236
237 if (hasLiftCache(current))
238 {
239 result = getLiftCache(current);
240 }
241 else if (isConvertibleBvAtom(current))
242 {
243 result = convertBvAtom(current);
244 addToLiftCache(current, result);
245 }
246 else
247 {
248 if (current.getNumChildren() == 0)
249 {
250 result = current;
251 }
252 else
253 {
254 NodeBuilder<> builder(current.getKind());
255 if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
256 {
257 builder << current.getOperator();
258 }
259 for (unsigned i = 0; i < current.getNumChildren(); ++i)
260 {
261 Node converted = liftNode(current[i]);
262 Assert(converted.getType() == current[i].getType());
263 builder << converted;
264 }
265 result = builder;
266 addToLiftCache(current, result);
267 }
268 }
269 Assert(result != Node());
270 Assert(result.getType() == current.getType());
271 Debug("bv-to-bool") << "BVToBool::liftNode " << current << " => \n"
272 << result << "\n";
273 return result;
274 }
275
liftBvToBool(const std::vector<Node> & assertions,std::vector<Node> & new_assertions)276 void BVToBool::liftBvToBool(const std::vector<Node>& assertions,
277 std::vector<Node>& new_assertions)
278 {
279 for (unsigned i = 0; i < assertions.size(); ++i)
280 {
281 Node new_assertion = liftNode(assertions[i]);
282 new_assertions.push_back(Rewriter::rewrite(new_assertion));
283 Trace("bv-to-bool") << " " << assertions[i] << " => " << new_assertions[i]
284 << "\n";
285 }
286 }
287
Statistics()288 BVToBool::Statistics::Statistics()
289 : d_numTermsLifted("preprocessing::passes::BVToBool::NumTermsLifted", 0),
290 d_numAtomsLifted("preprocessing::passes::BVToBool::NumAtomsLifted", 0),
291 d_numTermsForcedLifted(
292 "preprocessing::passes::BVToBool::NumTermsForcedLifted", 0)
293 {
294 smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
295 smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
296 smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted);
297 }
298
~Statistics()299 BVToBool::Statistics::~Statistics()
300 {
301 smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted);
302 smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted);
303 smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
304 }
305
306
307 } // passes
308 } // Preprocessing
309 } // CVC4
310