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