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