1 /********************* */
2 /*! \file bool_to_bv.cpp
4 ** Top contributors (to current version):
5 ** Makai Mann, Yoni Zohar, Clark Barrett
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief The BoolToBV preprocessing pass
16 #include "preprocessing/passes/bool_to_bv.h"
20 #include "base/map_util.h"
21 #include "expr/node.h"
22 #include "smt/smt_statistics_registry.h"
23 #include "theory/rewriter.h"
24 #include "theory/theory.h"
27 namespace preprocessing
{
29 using namespace CVC4::theory
;
31 BoolToBV::BoolToBV(PreprocessingPassContext
* preprocContext
)
32 : PreprocessingPass(preprocContext
, "bool-to-bv"), d_statistics()
34 d_boolToBVMode
= options::boolToBitvector();
37 PreprocessingPassResult
BoolToBV::applyInternal(
38 AssertionPipeline
* assertionsToPreprocess
)
40 d_preprocContext
->spendResource(ResourceManager::Resource::PreprocessStep
);
42 size_t size
= assertionsToPreprocess
->size();
44 if (d_boolToBVMode
== options::BoolToBVMode::ALL
)
46 for (size_t i
= 0; i
< size
; ++i
)
48 Node newAssertion
= lowerAssertion((*assertionsToPreprocess
)[i
], true);
49 assertionsToPreprocess
->replace(i
, Rewriter::rewrite(newAssertion
));
54 Assert(d_boolToBVMode
== options::BoolToBVMode::ITE
);
55 for (size_t i
= 0; i
< size
; ++i
)
57 assertionsToPreprocess
->replace(
58 i
, Rewriter::rewrite(lowerIte((*assertionsToPreprocess
)[i
])));
62 return PreprocessingPassResult::NO_CONFLICT
;
65 void BoolToBV::updateCache(TNode n
, TNode rebuilt
)
67 // check more likely case first
68 if ((n
.getKind() != kind::ITE
) || !n
[1].getType().isBitVector())
70 d_lowerCache
[n
] = rebuilt
;
74 d_iteBVLowerCache
[n
] = rebuilt
;
78 Node
BoolToBV::fromCache(TNode n
) const
80 // check more likely case first
81 if (n
.getKind() != kind::ITE
)
83 if (d_lowerCache
.find(n
) != d_lowerCache
.end())
85 return d_lowerCache
.at(n
);
90 if (d_iteBVLowerCache
.find(n
) != d_iteBVLowerCache
.end())
92 return d_iteBVLowerCache
.at(n
);
98 inline bool BoolToBV::inCache(const Node
& n
) const
100 return (ContainsKey(d_lowerCache
, n
) || ContainsKey(d_iteBVLowerCache
, n
));
103 bool BoolToBV::needToRebuild(TNode n
) const
105 // check if any children were rebuilt
106 for (const Node
& nn
: n
)
116 Node
BoolToBV::lowerAssertion(const TNode
& assertion
, bool allowIteIntroduction
)
118 // first try to lower all the children
119 for (const Node
& c
: assertion
)
121 lowerNode(c
, allowIteIntroduction
);
124 // now try lowering the assertion, but don't force it with an ITE (even in mode all)
125 lowerNode(assertion
, false);
126 Node newAssertion
= fromCache(assertion
);
127 TypeNode newAssertionType
= newAssertion
.getType();
128 if (newAssertionType
.isBitVector())
130 Assert(newAssertionType
.getBitVectorSize() == 1);
131 newAssertion
= NodeManager::currentNM()->mkNode(
132 kind::EQUAL
, newAssertion
, bv::utils::mkOne(1));
133 newAssertionType
= newAssertion
.getType();
135 Assert(newAssertionType
.isBoolean());
139 Node
BoolToBV::lowerNode(const TNode
& node
, bool allowIteIntroduction
)
141 std::vector
<TNode
> to_visit
;
142 to_visit
.push_back(node
);
143 std::unordered_set
<TNode
, TNodeHashFunction
> visited
;
145 while (!to_visit
.empty())
147 TNode n
= to_visit
.back();
150 Debug("bool-to-bv") << "BoolToBV::lowerNode: Post-order traversal with "
151 << n
<< " and visited = " << ContainsKey(visited
, n
)
155 if (ContainsKey(visited
, n
))
157 visit(n
, allowIteIntroduction
);
162 to_visit
.push_back(n
);
164 // insert children in reverse order so that they're processed in order
165 // important for rewriting which sorts by node id
166 // NOTE: size_t is unsigned, so using underflow for termination condition
167 size_t numChildren
= n
.getNumChildren();
168 for (size_t i
= numChildren
- 1; i
< numChildren
; --i
)
170 to_visit
.push_back(n
[i
]);
175 return fromCache(node
);
178 void BoolToBV::visit(const TNode
& n
, bool allowIteIntroduction
)
180 Kind k
= n
.getKind();
182 // easy case -- just replace boolean constant
183 if (k
== kind::CONST_BOOLEAN
)
186 (n
== bv::utils::mkTrue()) ? bv::utils::mkOne(1)
187 : bv::utils::mkZero(1));
191 NodeManager
* nm
= NodeManager::currentNM();
195 case kind::EQUAL
: new_kind
= kind::BITVECTOR_COMP
; break;
196 case kind::AND
: new_kind
= kind::BITVECTOR_AND
; break;
197 case kind::OR
: new_kind
= kind::BITVECTOR_OR
; break;
198 case kind::NOT
: new_kind
= kind::BITVECTOR_NOT
; break;
199 case kind::XOR
: new_kind
= kind::BITVECTOR_XOR
; break;
200 case kind::IMPLIES
: new_kind
= kind::BITVECTOR_OR
; break;
201 case kind::ITE
: new_kind
= kind::BITVECTOR_ITE
; break;
202 case kind::BITVECTOR_ULT
: new_kind
= kind::BITVECTOR_ULTBV
; break;
203 case kind::BITVECTOR_SLT
: new_kind
= kind::BITVECTOR_SLTBV
; break;
204 case kind::BITVECTOR_ULE
:
205 case kind::BITVECTOR_UGT
:
206 case kind::BITVECTOR_UGE
:
207 case kind::BITVECTOR_SLE
:
208 case kind::BITVECTOR_SGT
:
209 case kind::BITVECTOR_SGE
:
210 // Should have been removed by rewriting.
215 // check if it's safe to lower or rebuild the node
216 // Note: might have to rebuild to keep changes to children, even if this node
217 // isn't being lowered
219 // it's safe to lower if all the children are bit-vectors
221 (new_kind
!= k
); // don't need to lower at all if kind hasn't changed
223 // it's safe to rebuild if rebuilding doesn't change any of the types of the
225 bool safe_to_rebuild
= true;
227 for (const Node
& nn
: n
)
229 safe_to_lower
= safe_to_lower
&& fromCache(nn
).getType().isBitVector();
230 safe_to_rebuild
= safe_to_rebuild
&& (fromCache(nn
).getType() == nn
.getType());
232 // if it's already not safe to do either, stop checking
233 if (!safe_to_lower
&& !safe_to_rebuild
)
239 Debug("bool-to-bv") << "safe_to_lower = " << safe_to_lower
240 << ", safe_to_rebuild = " << safe_to_rebuild
<< std::endl
;
242 if (new_kind
!= k
&& safe_to_lower
)
245 rebuildNode(n
, new_kind
);
248 else if (new_kind
!= k
&& allowIteIntroduction
&& fromCache(n
).getType().isBoolean())
250 // lower to BV using an ITE
252 if (safe_to_rebuild
&& needToRebuild(n
))
254 // need to rebuild to keep changes made to descendants
259 nm
->mkNode(kind::ITE
,
262 bv::utils::mkZero(1)));
263 Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
265 << fromCache(n
) << std::endl
;
266 ++(d_statistics
.d_numIntroducedItes
);
269 else if (safe_to_rebuild
&& needToRebuild(n
))
271 // rebuild to incorporate changes to children
272 Assert(k
== new_kind
);
275 else if (allowIteIntroduction
&& fromCache(n
).getType().isBoolean())
277 // force booleans (which haven't already been converted) to bit-vector
278 // needed to maintain the invariant that all boolean children
279 // have been converted (even constants and variables) when forcing
280 // with ITE introductions
282 n
, nm
->mkNode(kind::ITE
, n
, bv::utils::mkOne(1), bv::utils::mkZero(1)));
283 Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
285 << fromCache(n
) << std::endl
;
286 ++(d_statistics
.d_numIntroducedItes
);
291 Debug("bool-to-bv") << "BoolToBV::visit skipping: " << n
296 Node
BoolToBV::lowerIte(const TNode
& node
)
298 std::vector
<TNode
> visit
;
299 visit
.push_back(node
);
300 std::unordered_set
<TNode
, TNodeHashFunction
> visited
;
302 while (!visit
.empty())
304 TNode n
= visit
.back();
307 Debug("bool-to-bv") << "BoolToBV::lowerIte: Post-order traversal with " << n
308 << " and visited = " << ContainsKey(visited
, n
)
311 // Look for ITEs and mark visited
312 if (!ContainsKey(visited
, n
))
314 if ((n
.getKind() == kind::ITE
) && n
[1].getType().isBitVector())
316 Debug("bool-to-bv") << "BoolToBV::lowerIte: adding " << n
[0]
317 << " to set of ite conditions" << std::endl
;
318 // don't force in this case -- forcing only introduces more ITEs
319 Node loweredNode
= lowerNode(n
, false);
320 // some of the lowered nodes might appear elsewhere but not in an ITE
321 // reset the cache to prevent lowering them
322 // the bit-vector ITEs are still tracked in d_iteBVLowerCache though
323 d_lowerCache
.clear();
329 // insert in reverse order so that they're processed in order
330 for (int i
= n
.getNumChildren() - 1; i
>= 0; --i
)
332 visit
.push_back(n
[i
]);
336 else if (needToRebuild(n
))
338 // Note: it's always safe to rebuild here, because we've only lowered
339 // ITEs of type bit-vector to BITVECTOR_ITE
340 rebuildNode(n
, n
.getKind());
345 << "BoolToBV::lowerIte Skipping because don't need to rebuild: " << n
349 return fromCache(node
);
352 void BoolToBV::rebuildNode(const TNode
& n
, Kind new_kind
)
354 Kind k
= n
.getKind();
355 NodeManager
* nm
= NodeManager::currentNM();
356 NodeBuilder
<> builder(new_kind
);
358 Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n
359 << " and new_kind = " << kindToString(new_kind
)
362 if ((d_boolToBVMode
== options::BoolToBVMode::ALL
) && (new_kind
!= k
))
364 ++(d_statistics
.d_numTermsLowered
);
367 if (n
.getMetaKind() == kind::metakind::PARAMETERIZED
)
369 builder
<< n
.getOperator();
372 // special case IMPLIES because needs to be rewritten
373 if ((k
== kind::IMPLIES
) && (new_kind
!= k
))
375 builder
<< nm
->mkNode(kind::BITVECTOR_NOT
, fromCache(n
[0]));
376 builder
<< fromCache(n
[1]);
380 for (const Node
& nn
: n
)
382 builder
<< fromCache(nn
);
386 Debug("bool-to-bv") << "BoolToBV::rebuildNode " << n
<< " =>\n"
387 << builder
<< std::endl
;
389 updateCache(n
, builder
.constructNode());
392 BoolToBV::Statistics::Statistics()
393 : d_numIteToBvite("preprocessing::passes::BoolToBV::NumIteToBvite", 0),
394 d_numTermsLowered("preprocessing::passes:BoolToBV::NumTermsLowered", 0),
396 "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0)
398 smtStatisticsRegistry()->registerStat(&d_numIteToBvite
);
399 if (options::boolToBitvector() == options::BoolToBVMode::ALL
)
401 // these statistics wouldn't be correct in the ITE mode,
402 // because it might discard rebuilt nodes if it fails to
403 // convert a bool to width-one bit-vector (never forces)
404 smtStatisticsRegistry()->registerStat(&d_numTermsLowered
);
405 smtStatisticsRegistry()->registerStat(&d_numIntroducedItes
);
409 BoolToBV::Statistics::~Statistics()
411 smtStatisticsRegistry()->unregisterStat(&d_numIteToBvite
);
412 if (options::boolToBitvector() == options::BoolToBVMode::ALL
)
414 smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered
);
415 smtStatisticsRegistry()->unregisterStat(&d_numIntroducedItes
);
420 } // namespace passes
421 } // namespace preprocessing