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 : : * Preprocessing pass that lifts bit-vectors of size 1 to booleans.
11 : : *
12 : : * Implemented recursively.
13 : : */
14 : :
15 : : #include "preprocessing/passes/bv_to_bool.h"
16 : :
17 : : #include <string>
18 : : #include <unordered_map>
19 : : #include <vector>
20 : :
21 : : #include "expr/node.h"
22 : : #include "expr/node_visitor.h"
23 : : #include "preprocessing/assertion_pipeline.h"
24 : : #include "preprocessing/preprocessing_pass_context.h"
25 : : #include "theory/bv/theory_bv_utils.h"
26 : : #include "theory/rewriter.h"
27 : : #include "theory/theory.h"
28 : :
29 : : namespace cvc5::internal {
30 : : namespace preprocessing {
31 : : namespace passes {
32 : :
33 : : using namespace std;
34 : : using namespace cvc5::internal::theory;
35 : :
36 : 51930 : BVToBool::BVToBool(PreprocessingPassContext* preprocContext)
37 : : : PreprocessingPass(preprocContext, "bv-to-bool"),
38 : 51930 : d_liftCache(),
39 : 51930 : d_boolCache(),
40 : 51930 : d_one(bv::utils::mkOne(nodeManager(), 1)),
41 : 51930 : d_zero(bv::utils::mkZero(nodeManager(), 1)),
42 : 103860 : d_statistics(statisticsRegistry()) {};
43 : :
44 : 559 : PreprocessingPassResult BVToBool::applyInternal(
45 : : AssertionPipeline* assertionsToPreprocess)
46 : : {
47 : 559 : d_preprocContext->spendResource(Resource::PreprocessStep);
48 : 559 : std::vector<Node> new_assertions;
49 : 559 : liftBvToBool(assertionsToPreprocess->ref(), new_assertions);
50 [ + + ]: 2423 : for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
51 : : {
52 : 1871 : assertionsToPreprocess->replace(
53 : 1871 : i, new_assertions[i], nullptr, TrustId::PREPROCESS_BV_TO_BOOL);
54 [ + + ]: 1871 : if (assertionsToPreprocess->isInConflict())
55 : : {
56 : 7 : return PreprocessingPassResult::CONFLICT;
57 : : }
58 : 1864 : assertionsToPreprocess->ensureRewritten(i);
59 : : }
60 : 552 : return PreprocessingPassResult::NO_CONFLICT;
61 : 559 : }
62 : :
63 : 4341 : void BVToBool::addToLiftCache(TNode term, Node new_term)
64 : : {
65 [ - + ][ - + ]: 4341 : Assert(new_term != Node());
[ - - ]
66 [ - + ][ - + ]: 4341 : Assert(!hasLiftCache(term));
[ - - ]
67 [ - + ][ - + ]: 13023 : AssertEqual(term.getType(), new_term.getType());
[ - - ]
68 : 4341 : d_liftCache[term] = new_term;
69 : 4341 : }
70 : :
71 : 309 : Node BVToBool::getLiftCache(TNode term) const
72 : : {
73 [ - + ][ - + ]: 309 : Assert(hasLiftCache(term));
[ - - ]
74 : 618 : return d_liftCache.find(term)->second;
75 : : }
76 : :
77 : 13745 : bool BVToBool::hasLiftCache(TNode term) const
78 : : {
79 : 13745 : return d_liftCache.find(term) != d_liftCache.end();
80 : : }
81 : :
82 : 444 : void BVToBool::addToBoolCache(TNode term, Node new_term)
83 : : {
84 [ - + ][ - + ]: 444 : Assert(new_term != Node());
[ - - ]
85 [ - + ][ - + ]: 444 : Assert(!hasBoolCache(term));
[ - - ]
86 [ - + ][ - + ]: 444 : Assert(bv::utils::getSize(term) == 1);
[ - - ]
87 [ - + ][ - + ]: 444 : Assert(new_term.getType().isBoolean());
[ - - ]
88 : 444 : d_boolCache[term] = new_term;
89 : 444 : }
90 : :
91 : 146 : Node BVToBool::getBoolCache(TNode term) const
92 : : {
93 [ - + ][ - + ]: 146 : Assert(hasBoolCache(term));
[ - - ]
94 : 292 : return d_boolCache.find(term)->second;
95 : : }
96 : :
97 : 1660 : bool BVToBool::hasBoolCache(TNode term) const
98 : : {
99 : 1660 : return d_boolCache.find(term) != d_boolCache.end();
100 : : }
101 : 8786 : bool BVToBool::isConvertibleBvAtom(TNode node)
102 : : {
103 : 8786 : Kind kind = node.getKind();
104 : 9878 : return (kind == Kind::EQUAL && node[0].getType().isBitVector()
105 : 9605 : && node[0].getType().getBitVectorSize() == 1
106 : 9148 : && node[1].getType().isBitVector()
107 : 9148 : && node[1].getType().getBitVectorSize() == 1
108 [ + - ][ + + ]: 9148 : && node[0].getKind() != Kind::BITVECTOR_EXTRACT
[ - - ]
109 [ + + ][ + + ]: 18664 : && node[1].getKind() != Kind::BITVECTOR_EXTRACT);
[ + + ][ + + ]
[ - - ]
110 : : }
111 : :
112 : 924 : bool BVToBool::isConvertibleBvTerm(TNode node)
113 : : {
114 : 924 : if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1)
115 : 0 : return false;
116 : :
117 : 924 : Kind kind = node.getKind();
118 : :
119 [ + + ][ + + ]: 924 : if (kind == Kind::CONST_BITVECTOR || kind == Kind::ITE
120 [ + + ][ + + ]: 306 : || kind == Kind::BITVECTOR_AND || kind == Kind::BITVECTOR_OR
121 [ + - ][ + + ]: 264 : || kind == Kind::BITVECTOR_NOT || kind == Kind::BITVECTOR_XOR
122 [ + + ]: 262 : || kind == Kind::BITVECTOR_COMP)
123 : : {
124 : 676 : return true;
125 : : }
126 : :
127 : 248 : return false;
128 : : }
129 : :
130 : 351 : Node BVToBool::convertBvAtom(TNode node)
131 : : {
132 : 351 : Assert(node.getType().isBoolean() && node.getKind() == Kind::EQUAL);
133 [ - + ][ - + ]: 351 : Assert(bv::utils::getSize(node[0]) == 1);
[ - - ]
134 [ - + ][ - + ]: 351 : Assert(bv::utils::getSize(node[1]) == 1);
[ - - ]
135 : 351 : Node a = convertBvTerm(node[0]);
136 : 351 : Node b = convertBvTerm(node[1]);
137 : 702 : Node result = nodeManager()->mkNode(Kind::EQUAL, a, b);
138 [ + - ]: 702 : Trace("bv-to-bool") << "BVToBool::convertBvAtom " << node << " => " << result
139 : 351 : << "\n";
140 : :
141 : 351 : ++(d_statistics.d_numAtomsLifted);
142 : 702 : return result;
143 : 351 : }
144 : :
145 : 1070 : Node BVToBool::convertBvTerm(TNode node)
146 : : {
147 : 1070 : Assert(node.getType().isBitVector()
148 : : && node.getType().getBitVectorSize() == 1);
149 : :
150 [ + + ]: 1070 : if (hasBoolCache(node)) return getBoolCache(node);
151 : :
152 : 924 : NodeManager* nm = nodeManager();
153 : :
154 [ + + ]: 924 : if (!isConvertibleBvTerm(node))
155 : : {
156 : 248 : ++(d_statistics.d_numTermsForcedLifted);
157 : 496 : Node result = nm->mkNode(Kind::EQUAL, node, d_one);
158 : 248 : addToBoolCache(node, result);
159 [ + - ]: 496 : Trace("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
160 : 248 : << result << "\n";
161 : 248 : return result;
162 : 248 : }
163 : :
164 [ + + ]: 676 : if (node.getNumChildren() == 0)
165 : : {
166 [ - + ][ - + ]: 478 : Assert(node.getKind() == Kind::CONST_BITVECTOR);
[ - - ]
167 : : Node result =
168 [ + + ]: 478 : node == d_one ? bv::utils::mkTrue(nm) : bv::utils::mkFalse(nm);
169 : : // addToCache(node, result);
170 [ + - ]: 956 : Trace("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
171 : 478 : << result << "\n";
172 : 478 : return result;
173 : 478 : }
174 : :
175 : 198 : ++(d_statistics.d_numTermsLifted);
176 : :
177 : 198 : Kind kind = node.getKind();
178 [ + + ]: 198 : if (kind == Kind::ITE)
179 : : {
180 : 140 : Node cond = liftNode(node[0]);
181 : 140 : Node true_branch = convertBvTerm(node[1]);
182 : 140 : Node false_branch = convertBvTerm(node[2]);
183 : 280 : Node result = nm->mkNode(Kind::ITE, cond, true_branch, false_branch);
184 : 140 : addToBoolCache(node, result);
185 [ + - ]: 280 : Trace("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
186 : 140 : << result << "\n";
187 : 140 : return result;
188 : 140 : }
189 : :
190 : : Kind new_kind;
191 : : // special case for XOR as it has to be binary
192 : : // while BITVECTOR_XOR can be n-ary
193 [ + + ]: 58 : if (kind == Kind::BITVECTOR_XOR)
194 : : {
195 : 2 : Node result = convertBvTerm(node[0]);
196 [ + + ]: 4 : for (unsigned i = 1; i < node.getNumChildren(); ++i)
197 : : {
198 : 2 : Node converted = convertBvTerm(node[i]);
199 : 2 : result = nm->mkNode(Kind::XOR, result, converted);
200 : 2 : }
201 [ + - ]: 4 : Trace("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
202 : 2 : << result << "\n";
203 : 2 : return result;
204 : 2 : }
205 : :
206 [ + + ]: 56 : if (kind == Kind::BITVECTOR_COMP)
207 : : {
208 : 28 : Node result = nm->mkNode(Kind::EQUAL, node[0], node[1]);
209 : 14 : addToBoolCache(node, result);
210 [ + - ]: 28 : Trace("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
211 : 14 : << result << "\n";
212 : 14 : return result;
213 : 14 : }
214 : :
215 [ + + ][ - - ]: 42 : switch (kind)
216 : : {
217 : 14 : case Kind::BITVECTOR_OR: new_kind = Kind::OR; break;
218 : 28 : case Kind::BITVECTOR_AND: new_kind = Kind::AND; break;
219 : 0 : case Kind::BITVECTOR_NOT: new_kind = Kind::NOT; break;
220 : 0 : default: Unhandled();
221 : : }
222 : :
223 : 84 : NodeBuilder builder(nm, new_kind);
224 [ + + ]: 126 : for (unsigned i = 0; i < node.getNumChildren(); ++i)
225 : : {
226 : 84 : builder << convertBvTerm(node[i]);
227 : : }
228 : :
229 : 84 : Node result = builder;
230 : 42 : addToBoolCache(node, result);
231 [ + - ]: 84 : Trace("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => " << result
232 : 42 : << "\n";
233 : 42 : return result;
234 : : }
235 : :
236 : 9095 : Node BVToBool::liftNode(TNode current)
237 : : {
238 : 9095 : Node result;
239 : :
240 [ + + ]: 9095 : if (hasLiftCache(current))
241 : : {
242 : 309 : result = getLiftCache(current);
243 : : }
244 [ + + ]: 8786 : else if (isConvertibleBvAtom(current))
245 : : {
246 : 351 : result = convertBvAtom(current);
247 : 351 : addToLiftCache(current, result);
248 : : }
249 : : else
250 : : {
251 [ + + ]: 8435 : if (current.getNumChildren() == 0)
252 : : {
253 : 4445 : result = current;
254 : : }
255 : : else
256 : : {
257 : 3990 : NodeBuilder builder(nodeManager(), current.getKind());
258 [ + + ]: 3990 : if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
259 : : {
260 : 272 : builder << current.getOperator();
261 : : }
262 [ + + ]: 11067 : for (unsigned i = 0; i < current.getNumChildren(); ++i)
263 : : {
264 : : // Recursively lift children
265 : 7077 : Node converted = liftNode(current[i]);
266 [ - + ][ - + ]: 28308 : AssertEqual(converted.getType(), current[i].getType());
[ - - ]
267 : 7077 : builder << converted;
268 : 7077 : }
269 : 3990 : result = builder;
270 : 3990 : addToLiftCache(current, result);
271 : 3990 : }
272 : : }
273 [ - + ][ - + ]: 9095 : Assert(result != Node());
[ - - ]
274 [ - + ][ - + ]: 27285 : AssertEqual(result.getType(), current.getType());
[ - - ]
275 [ + - ]: 18190 : Trace("bv-to-bool") << "BVToBool::liftNode " << current << " => \n"
276 : 9095 : << result << "\n";
277 : 9095 : return result;
278 : 0 : }
279 : :
280 : 559 : void BVToBool::liftBvToBool(const std::vector<Node>& assertions,
281 : : std::vector<Node>& new_assertions)
282 : : {
283 [ + + ]: 2437 : for (unsigned i = 0; i < assertions.size(); ++i)
284 : : {
285 : 1878 : Node new_assertion = liftNode(assertions[i]);
286 : 1878 : new_assertions.push_back(rewrite(new_assertion));
287 [ + - ]: 3756 : Trace("bv-to-bool") << " " << assertions[i] << " => " << new_assertions[i]
288 : 1878 : << "\n";
289 : 1878 : }
290 : 559 : }
291 : :
292 : 51930 : BVToBool::Statistics::Statistics(StatisticsRegistry& reg)
293 : : : d_numTermsLifted(
294 : 51930 : reg.registerInt("preprocessing::passes::BVToBool::NumTermsLifted")),
295 : : d_numAtomsLifted(
296 : 51930 : reg.registerInt("preprocessing::passes::BVToBool::NumAtomsLifted")),
297 : 51930 : d_numTermsForcedLifted(reg.registerInt(
298 : : "preprocessing::passes::BVToBool::NumTermsForcedLifted"))
299 : : {
300 : 51930 : }
301 : :
302 : : } // namespace passes
303 : : } // namespace preprocessing
304 : : } // namespace cvc5::internal
|
