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