Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Makai Mann, Yoni Zohar, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * The BoolToBV preprocessing pass.
14 : : *
15 : : */
16 : :
17 : : #include "preprocessing/passes/bool_to_bv.h"
18 : :
19 : : #include <string>
20 : :
21 : : #include "base/map_util.h"
22 : : #include "expr/node.h"
23 : : #include "options/bv_options.h"
24 : : #include "preprocessing/assertion_pipeline.h"
25 : : #include "preprocessing/preprocessing_pass_context.h"
26 : : #include "theory/bv/theory_bv_utils.h"
27 : : #include "theory/rewriter.h"
28 : : #include "theory/theory.h"
29 : :
30 : : namespace cvc5::internal {
31 : : namespace preprocessing {
32 : : namespace passes {
33 : : using namespace cvc5::internal::theory;
34 : :
35 : 48144 : BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
36 : : : PreprocessingPass(preprocContext, "bool-to-bv"),
37 : 48144 : d_statistics(statisticsRegistry())
38 : : {
39 : 48144 : d_boolToBVMode = options().bv.boolToBitvector;
40 : 48144 : };
41 : :
42 : 12 : PreprocessingPassResult BoolToBV::applyInternal(
43 : : AssertionPipeline* assertionsToPreprocess)
44 : : {
45 : 12 : d_preprocContext->spendResource(Resource::PreprocessStep);
46 : :
47 : 12 : size_t size = assertionsToPreprocess->size();
48 [ + + ][ - + ]: 12 : Assert(d_boolToBVMode == options::BoolToBVMode::ALL
[ - + ][ - - ]
49 : : || d_boolToBVMode == options::BoolToBVMode::ITE);
50 [ + + ]: 100 : for (size_t i = 0; i < size; ++i)
51 : : {
52 : 88 : Node newAssertion;
53 [ + + ]: 88 : if (d_boolToBVMode == options::BoolToBVMode::ALL)
54 : : {
55 : 68 : newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true);
56 : : }
57 : : else
58 : : {
59 : 20 : newAssertion = lowerIte((*assertionsToPreprocess)[i]);
60 : : }
61 : 88 : assertionsToPreprocess->replace(i, rewrite(newAssertion));
62 [ - + ]: 88 : if (assertionsToPreprocess->isInConflict())
63 : : {
64 : 0 : return PreprocessingPassResult::CONFLICT;
65 : : }
66 : : }
67 : 12 : return PreprocessingPassResult::NO_CONFLICT;
68 : : }
69 : :
70 : 156 : void BoolToBV::updateCache(TNode n, TNode rebuilt)
71 : : {
72 : : // check more likely case first
73 : 156 : if ((n.getKind() != Kind::ITE) || !n[1].getType().isBitVector())
74 : : {
75 : 152 : d_lowerCache[n] = rebuilt;
76 : : }
77 : : else
78 : : {
79 : 4 : d_iteBVLowerCache[n] = rebuilt;
80 : : }
81 : 156 : }
82 : :
83 : 1288 : Node BoolToBV::fromCache(TNode n) const
84 : : {
85 : : // check more likely case first
86 [ + + ]: 1288 : if (n.getKind() != Kind::ITE)
87 : : {
88 [ + + ]: 1272 : if (d_lowerCache.find(n) != d_lowerCache.end())
89 : : {
90 : 680 : return d_lowerCache.at(n);
91 : : }
92 : : }
93 : : else
94 : : {
95 [ + + ]: 16 : if (d_iteBVLowerCache.find(n) != d_iteBVLowerCache.end())
96 : : {
97 : 8 : return d_iteBVLowerCache.at(n);
98 : : }
99 : : }
100 : 600 : return n;
101 : : }
102 : :
103 : 220 : inline bool BoolToBV::inCache(const Node& n) const
104 : : {
105 [ + - ][ + + ]: 220 : return (ContainsKey(d_lowerCache, n) || ContainsKey(d_iteBVLowerCache, n));
106 : : }
107 : :
108 : 532 : bool BoolToBV::needToRebuild(TNode n) const
109 : : {
110 : : // check if any children were rebuilt
111 [ + + ]: 748 : for (const Node& nn : n)
112 : : {
113 [ + + ]: 220 : if (inCache(nn))
114 : : {
115 : 4 : return true;
116 : : }
117 : : }
118 : 528 : return false;
119 : : }
120 : :
121 : 68 : Node BoolToBV::lowerAssertion(const TNode& assertion, bool allowIteIntroduction)
122 : : {
123 : : // first try to lower all the children
124 [ + + ]: 166 : for (const Node& c : assertion)
125 : : {
126 : 98 : lowerNode(c, allowIteIntroduction);
127 : : }
128 : :
129 : : // now try lowering the assertion, but don't force it with an ITE (even in mode all)
130 : 68 : lowerNode(assertion, false);
131 : 68 : Node newAssertion = fromCache(assertion);
132 : 136 : TypeNode newAssertionType = newAssertion.getType();
133 [ + + ]: 68 : if (newAssertionType.isBitVector())
134 : : {
135 [ - + ][ - + ]: 64 : Assert(newAssertionType.getBitVectorSize() == 1);
[ - - ]
136 : : newAssertion =
137 : 64 : nodeManager()->mkNode(Kind::EQUAL, newAssertion, bv::utils::mkOne(1));
138 : 64 : newAssertionType = newAssertion.getType();
139 : : }
140 [ - + ][ - + ]: 68 : Assert(newAssertionType.isBoolean());
[ - - ]
141 : 136 : return newAssertion;
142 : : }
143 : :
144 : 170 : Node BoolToBV::lowerNode(const TNode& node, bool allowIteIntroduction)
145 : : {
146 : 340 : std::vector<TNode> to_visit;
147 : 170 : to_visit.push_back(node);
148 : 170 : std::unordered_set<TNode> visited;
149 : :
150 [ + + ]: 1342 : while (!to_visit.empty())
151 : : {
152 : 2344 : TNode n = to_visit.back();
153 : 1172 : to_visit.pop_back();
154 : :
155 [ + - ]: 2344 : Trace("bool-to-bv") << "BoolToBV::lowerNode: Post-order traversal with "
156 : 1172 : << n << " and visited = " << ContainsKey(visited, n)
157 : 1172 : << std::endl;
158 : :
159 : : // Mark as visited
160 [ + + ]: 1172 : if (ContainsKey(visited, n))
161 : : {
162 : 608 : visit(n, allowIteIntroduction);
163 : : }
164 : : else
165 : : {
166 : 564 : visited.insert(n);
167 : 564 : to_visit.push_back(n);
168 : :
169 : : // insert children in reverse order so that they're processed in order
170 : : // important for rewriting which sorts by node id
171 : : // NOTE: size_t is unsigned, so using underflow for termination condition
172 : 564 : size_t numChildren = n.getNumChildren();
173 [ + + ]: 1002 : for (size_t i = numChildren - 1; i < numChildren; --i)
174 : : {
175 : 438 : to_visit.push_back(n[i]);
176 : : }
177 : : }
178 : : }
179 : :
180 : 340 : return fromCache(node);
181 : : }
182 : :
183 : 608 : void BoolToBV::visit(const TNode& n, bool allowIteIntroduction)
184 : : {
185 : 608 : Kind k = n.getKind();
186 : :
187 : : // easy case -- just replace boolean constant
188 [ + + ]: 608 : if (k == Kind::CONST_BOOLEAN)
189 : : {
190 : 10 : updateCache(n,
191 [ + - ]: 20 : (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1)
192 : : : bv::utils::mkZero(1));
193 : 120 : return;
194 : : }
195 : :
196 : 598 : NodeManager* nm = nodeManager();
197 : 598 : Kind new_kind = k;
198 [ + + ][ + + ]: 598 : switch (k)
[ + + ][ + + ]
[ + - ][ + ]
199 : : {
200 : 38 : case Kind::EQUAL: new_kind = Kind::BITVECTOR_COMP; break;
201 : 8 : case Kind::AND: new_kind = Kind::BITVECTOR_AND; break;
202 : 4 : case Kind::OR: new_kind = Kind::BITVECTOR_OR; break;
203 : 26 : case Kind::NOT: new_kind = Kind::BITVECTOR_NOT; break;
204 : 6 : case Kind::XOR: new_kind = Kind::BITVECTOR_XOR; break;
205 : 20 : case Kind::IMPLIES: new_kind = Kind::BITVECTOR_OR; break;
206 : 12 : case Kind::ITE: new_kind = Kind::BITVECTOR_ITE; break;
207 : 16 : case Kind::BITVECTOR_ULT: new_kind = Kind::BITVECTOR_ULTBV; break;
208 : 4 : case Kind::BITVECTOR_SLT: new_kind = Kind::BITVECTOR_SLTBV; break;
209 : 0 : case Kind::BITVECTOR_ULE:
210 : : case Kind::BITVECTOR_UGT:
211 : : case Kind::BITVECTOR_UGE:
212 : : case Kind::BITVECTOR_SLE:
213 : : case Kind::BITVECTOR_SGT:
214 : : case Kind::BITVECTOR_SGE:
215 : : // Should have been removed by rewriting.
216 : 0 : Unreachable();
217 : 464 : default: break;
218 : : }
219 : :
220 : : // check if it's safe to lower or rebuild the node
221 : : // Note: might have to rebuild to keep changes to children, even if this node
222 : : // isn't being lowered
223 : :
224 : : // it's safe to lower if all the children are bit-vectors
225 : 598 : bool safe_to_lower =
226 : 598 : (new_kind != k); // don't need to lower at all if kind hasn't changed
227 : :
228 : : // it's safe to rebuild if rebuilding doesn't change any of the types of the
229 : : // children
230 : 598 : bool safe_to_rebuild = true;
231 : :
232 [ + + ]: 988 : for (const Node& nn : n)
233 : : {
234 : 430 : safe_to_lower = safe_to_lower && fromCache(nn).getType().isBitVector();
235 : 430 : safe_to_rebuild = safe_to_rebuild && (fromCache(nn).getType() == nn.getType());
236 : :
237 : : // if it's already not safe to do either, stop checking
238 [ + + ][ + + ]: 430 : if (!safe_to_lower && !safe_to_rebuild)
239 : : {
240 : 40 : break;
241 : : }
242 : : }
243 [ + - ]: 1196 : Trace("bool-to-bv") << "safe_to_lower = " << safe_to_lower
244 : 598 : << ", safe_to_rebuild = " << safe_to_rebuild << std::endl;
245 : :
246 [ + + ][ + + ]: 598 : if (new_kind != k && safe_to_lower)
247 : : {
248 : : // lower to BV
249 : 102 : rebuildNode(n, new_kind);
250 : 102 : return;
251 : : }
252 : 496 : else if (new_kind != k && allowIteIntroduction && fromCache(n).getType().isBoolean())
253 : : {
254 : : // lower to BV using an ITE
255 : :
256 [ + + ][ - + ]: 8 : if (safe_to_rebuild && needToRebuild(n))
[ + + ][ - + ]
[ - - ]
257 : : {
258 : : // need to rebuild to keep changes made to descendants
259 : 0 : rebuildNode(n, k);
260 : : }
261 : :
262 : 8 : updateCache(n,
263 : 32 : nm->mkNode(Kind::ITE,
264 : 16 : fromCache(n),
265 : 16 : bv::utils::mkOne(1),
266 : 16 : bv::utils::mkZero(1)));
267 [ + - ]: 16 : Trace("bool-to-bv") << "BoolToBV::visit forcing " << n
268 : 0 : << " =>\n"
269 : 8 : << fromCache(n) << std::endl;
270 [ + - ]: 8 : if (d_boolToBVMode == options::BoolToBVMode::ALL)
271 : : {
272 : : // this statistic only makes sense for ALL mode
273 : 8 : ++(d_statistics.d_numIntroducedItes);
274 : : }
275 : 8 : return;
276 : : }
277 [ + + ][ - + ]: 488 : else if (safe_to_rebuild && needToRebuild(n))
[ + + ][ - + ]
[ - - ]
278 : : {
279 : : // rebuild to incorporate changes to children
280 : 0 : rebuildNode(n, k);
281 : : }
282 : 488 : else if (allowIteIntroduction && fromCache(n).getType().isBoolean())
283 : : {
284 : : // force booleans (which haven't already been converted) to bit-vector
285 : : // needed to maintain the invariant that all boolean children
286 : : // have been converted (even constants and variables) when forcing
287 : : // with ITE introductions
288 : 32 : updateCache(
289 : 64 : n, nm->mkNode(Kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1)));
290 [ + - ]: 64 : Trace("bool-to-bv") << "BoolToBV::visit forcing " << n
291 : 0 : << " =>\n"
292 : 32 : << fromCache(n) << std::endl;
293 [ + - ]: 32 : if (d_boolToBVMode == options::BoolToBVMode::ALL)
294 : : {
295 : : // this statistic only makes sense for ALL mode
296 : 32 : ++(d_statistics.d_numIntroducedItes);
297 : : }
298 : : }
299 : : else
300 : : {
301 : : // do nothing
302 [ + - ]: 912 : Trace("bool-to-bv") << "BoolToBV::visit skipping: " << n
303 : 456 : << std::endl;
304 : : }
305 : : }
306 : :
307 : 20 : Node BoolToBV::lowerIte(const TNode& node)
308 : : {
309 : 40 : std::vector<TNode> visit;
310 : 20 : visit.push_back(node);
311 : 20 : std::unordered_set<TNode> visited;
312 : :
313 [ + + ]: 168 : while (!visit.empty())
314 : : {
315 : 296 : TNode n = visit.back();
316 : 148 : visit.pop_back();
317 : :
318 [ + - ]: 296 : Trace("bool-to-bv") << "BoolToBV::lowerIte: Post-order traversal with " << n
319 : 148 : << " and visited = " << ContainsKey(visited, n)
320 : 148 : << std::endl;
321 : :
322 : : // Look for ITEs and mark visited
323 [ + + ]: 148 : if (!ContainsKey(visited, n))
324 : : {
325 : 72 : if ((n.getKind() == Kind::ITE) && n[1].getType().isBitVector())
326 : : {
327 [ + - ][ - + ]: 8 : Trace("bool-to-bv") << "BoolToBV::lowerIte: adding " << n[0]
[ - - ]
328 : 4 : << " to set of ite conditions" << std::endl;
329 : : // don't force in this case -- forcing only introduces more ITEs
330 : 8 : Node loweredNode = lowerNode(n, false);
331 : : // some of the lowered nodes might appear elsewhere but not in an ITE
332 : : // reset the cache to prevent lowering them
333 : : // the bit-vector ITEs are still tracked in d_iteBVLowerCache though
334 : 4 : d_lowerCache.clear();
335 : : }
336 : : else
337 : : {
338 : 68 : visit.push_back(n);
339 : 68 : visited.insert(n);
340 : : // insert in reverse order so that they're processed in order
341 [ + + ]: 128 : for (int i = n.getNumChildren() - 1; i >= 0; --i)
342 : : {
343 : 60 : visit.push_back(n[i]);
344 : : }
345 : : }
346 : : }
347 [ + + ]: 76 : else if (needToRebuild(n))
348 : : {
349 : : // Note: it's always safe to rebuild here, because we've only lowered
350 : : // ITEs of type bit-vector to BITVECTOR_ITE
351 : 4 : rebuildNode(n, n.getKind());
352 : : }
353 : : else
354 : : {
355 [ + - ]: 144 : Trace("bool-to-bv")
356 : 0 : << "BoolToBV::lowerIte Skipping because don't need to rebuild: " << n
357 : 72 : << std::endl;
358 : : }
359 : : }
360 : 40 : return fromCache(node);
361 : : }
362 : :
363 : 106 : void BoolToBV::rebuildNode(const TNode& n, Kind new_kind)
364 : : {
365 : 106 : Kind k = n.getKind();
366 : 106 : NodeManager* nm = nodeManager();
367 : 106 : NodeBuilder builder(new_kind);
368 : :
369 [ + - ]: 212 : Trace("bool-to-bv") << "BoolToBV::rebuildNode with " << n
370 [ - + ][ - - ]: 106 : << " and new_kind = " << kindToString(new_kind)
371 : 106 : << std::endl;
372 : :
373 [ + + ][ + - ]: 106 : if ((d_boolToBVMode == options::BoolToBVMode::ALL) && (new_kind != k))
374 : : {
375 : : // this statistic only makes sense for ALL mode
376 : 94 : ++(d_statistics.d_numTermsLowered);
377 : : }
378 : :
379 [ - + ]: 106 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
380 : : {
381 : 0 : builder << n.getOperator();
382 : : }
383 : : // special case IMPLIES because needs to be rewritten
384 [ + + ][ + - ]: 106 : if ((k == Kind::IMPLIES) && (new_kind != k))
385 : : {
386 : 20 : builder << nm->mkNode(Kind::BITVECTOR_NOT, fromCache(n[0]));
387 : 20 : builder << fromCache(n[1]);
388 : : }
389 : : else
390 : : {
391 [ + + ]: 244 : for (const Node& nn : n)
392 : : {
393 : 158 : builder << fromCache(nn);
394 : : }
395 : : }
396 : :
397 [ + - ]: 212 : Trace("bool-to-bv") << "BoolToBV::rebuildNode " << n << " =>\n"
398 : 106 : << builder << std::endl;
399 : :
400 : 106 : updateCache(n, builder.constructNode());
401 : 106 : }
402 : :
403 : 48144 : BoolToBV::Statistics::Statistics(StatisticsRegistry& reg)
404 : : : d_numIteToBvite(
405 : 48144 : reg.registerInt("preprocessing::passes::BoolToBV::NumIteToBvite")),
406 : : // the following two statistics are not correct in the ITE mode, because
407 : : // we might discard rebuilt nodes if we fails to convert a bool to
408 : : // width-one bit-vector (never forces)
409 : : d_numTermsLowered(
410 : 48144 : reg.registerInt("preprocessing::passes:BoolToBV::NumTermsLowered")),
411 : : d_numIntroducedItes(reg.registerInt(
412 : 48144 : "preprocessing::passes::BoolToBV::NumTermsForcedLowered"))
413 : : {
414 : 48144 : }
415 : :
416 : : } // namespace passes
417 : : } // namespace preprocessing
418 : : } // namespace cvc5::internal
|
