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 IntToBV preprocessing pass.
11 : : *
12 : : * Converts integer operations into bitvector operations. The width of the
13 : : * bitvectors is controlled through the `--solve-int-as-bv` command line
14 : : * option.
15 : : */
16 : :
17 : : #include "preprocessing/passes/int_to_bv.h"
18 : :
19 : : #include <string>
20 : : #include <unordered_map>
21 : : #include <vector>
22 : :
23 : : #include "expr/node.h"
24 : : #include "expr/node_traversal.h"
25 : : #include "expr/skolem_manager.h"
26 : : #include "options/base_options.h"
27 : : #include "options/smt_options.h"
28 : : #include "preprocessing/assertion_pipeline.h"
29 : : #include "preprocessing/preprocessing_pass_context.h"
30 : : #include "smt/logic_exception.h"
31 : : #include "theory/rewriter.h"
32 : : #include "theory/theory.h"
33 : : #include "util/bitvector.h"
34 : : #include "util/rational.h"
35 : :
36 : : namespace cvc5::internal {
37 : : namespace preprocessing {
38 : : namespace passes {
39 : :
40 : : using namespace std;
41 : : using namespace cvc5::internal::theory;
42 : :
43 : : namespace {
44 : :
45 : 0 : bool childrenTypesChanged(Node n, NodeMap& cache)
46 : : {
47 [ - - ]: 0 : for (Node child : n)
48 : : {
49 : 0 : TypeNode originalType = child.getType();
50 : 0 : TypeNode newType = cache[child].getType();
51 [ - - ]: 0 : if (newType != originalType)
52 : : {
53 : 0 : return true;
54 : : }
55 [ - - ][ - - ]: 0 : }
[ - - ]
56 : 0 : return false;
57 : : }
58 : :
59 : 57 : Node intToBVMakeBinary(NodeManager* nm, TNode n, NodeMap& cache)
60 : : {
61 : 57 : for (TNode current :
62 : 214 : NodeDfsIterable(n, VisitOrder::POSTORDER, [&cache](TNode nn) {
63 : 214 : return cache.count(nn) > 0;
64 [ + + ]: 328 : }))
65 : : {
66 : 214 : Node result;
67 [ + + ]: 214 : if (current.getNumChildren() == 0)
68 : : {
69 : 124 : result = current;
70 : : }
71 : 90 : else if (current.getNumChildren() > 2
72 [ + + ][ + - ]: 95 : && (current.getKind() == Kind::ADD
[ + + ]
73 [ + - ]: 5 : || current.getKind() == Kind::MULT
74 [ + + ]: 5 : || current.getKind() == Kind::NONLINEAR_MULT))
75 : : {
76 [ - + ][ - + ]: 2 : Assert(cache.find(current[0]) != cache.end());
[ - - ]
77 : 2 : result = cache[current[0]];
78 [ + + ]: 6 : for (unsigned i = 1; i < current.getNumChildren(); ++i)
79 : : {
80 [ - + ][ - + ]: 4 : Assert(cache.find(current[i]) != cache.end());
[ - - ]
81 : 4 : Node child = current[i];
82 : 8 : Node childRes = cache[current[i]];
83 : 4 : result = nm->mkNode(current.getKind(), result, childRes);
84 : 4 : }
85 : : }
86 : : else
87 : : {
88 : 88 : NodeBuilder builder(nm, current.getKind());
89 [ + + ]: 88 : if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
90 : : {
91 : 3 : builder << current.getOperator();
92 : : }
93 : :
94 [ + + ]: 254 : for (unsigned i = 0; i < current.getNumChildren(); ++i)
95 : : {
96 [ - + ][ - + ]: 166 : Assert(cache.find(current[i]) != cache.end());
[ - - ]
97 : 166 : builder << cache[current[i]];
98 : : }
99 : 88 : result = builder;
100 : 88 : }
101 : 214 : cache[current] = result;
102 : 271 : }
103 : 57 : return cache[n];
104 : : }
105 : : } // namespace
106 : :
107 : 57 : Node IntToBV::intToBV(TNode n, NodeMap& cache)
108 : : {
109 [ - + ][ - + ]: 57 : Assert(options().smt.solveIntAsBV <= 4294967295);
[ - - ]
110 : 57 : uint32_t size = options().smt.solveIntAsBV;
111 [ - + ][ - + ]: 57 : AlwaysAssert(size > 0);
[ - - ]
112 [ - + ][ - + ]: 57 : AlwaysAssert(!options().base.incrementalSolving);
[ - - ]
113 : :
114 : 57 : NodeManager* nm = nodeManager();
115 : 57 : NodeMap binaryCache;
116 : 57 : Node n_binary = intToBVMakeBinary(nm, n, binaryCache);
117 : :
118 : 57 : for (TNode current :
119 : 207 : NodeDfsIterable(n_binary, VisitOrder::POSTORDER, [&cache](TNode nn) {
120 : 207 : return cache.count(nn) > 0;
121 [ + + ]: 268 : }))
122 : : {
123 : 159 : TypeNode tn = current.getType();
124 : : // we only permit pure integer problems to be converted to BV with this
125 : : // preprocessing pass.
126 [ + - ][ + + ]: 159 : if (current.isClosure() || (!tn.isBoolean() && !tn.isInteger()))
[ + + ][ + + ]
127 : : {
128 : 4 : throw TypeCheckingExceptionPrivate(
129 : 8 : current, string("Cannot translate to BV: ") + current.toString());
130 : : }
131 [ + + ]: 155 : if (current.getNumChildren() > 0)
132 : : {
133 : : // Not a leaf
134 : 74 : vector<Node> children;
135 : 74 : uint64_t max = 0;
136 [ + + ]: 216 : for (const Node& nc : current)
137 : : {
138 [ - + ][ - + ]: 142 : Assert(cache.find(nc) != cache.end());
[ - - ]
139 : 142 : TNode childRes = cache[nc];
140 : 142 : TypeNode type = childRes.getType();
141 [ + + ]: 142 : if (type.isBitVector())
142 : : {
143 : 126 : uint32_t bvsize = type.getBitVectorSize();
144 [ + + ]: 126 : if (bvsize > max)
145 : : {
146 : 75 : max = bvsize;
147 : : }
148 : : }
149 : 142 : children.push_back(childRes);
150 : 142 : }
151 : :
152 : 74 : kind::Kind_t newKind = current.getKind();
153 [ + + ]: 74 : if (max > 0)
154 : : {
155 [ + + ][ - - ]: 63 : switch (newKind)
[ - - ][ - + ]
[ + - ]
156 : : {
157 : 8 : case Kind::ADD:
158 [ - + ][ - + ]: 8 : Assert(children.size() == 2);
[ - - ]
159 : 8 : newKind = Kind::BITVECTOR_ADD;
160 : 8 : max = max + 1;
161 : 8 : break;
162 : 17 : case Kind::MULT:
163 : : case Kind::NONLINEAR_MULT:
164 [ - + ][ - + ]: 17 : Assert(children.size() == 2);
[ - - ]
165 : 17 : newKind = Kind::BITVECTOR_MULT;
166 : 17 : max = max * 2;
167 : 17 : break;
168 : 0 : case Kind::SUB:
169 : 0 : Assert(children.size() == 2);
170 : 0 : newKind = Kind::BITVECTOR_SUB;
171 : 0 : max = max + 1;
172 : 0 : break;
173 : 0 : case Kind::NEG:
174 : 0 : Assert(children.size() == 1);
175 : 0 : newKind = Kind::BITVECTOR_NEG;
176 : 0 : max = max + 1;
177 : 0 : break;
178 : 0 : case Kind::LT: newKind = Kind::BITVECTOR_SLT; break;
179 : 0 : case Kind::LEQ: newKind = Kind::BITVECTOR_SLE; break;
180 : 0 : case Kind::GT: newKind = Kind::BITVECTOR_SGT; break;
181 : 18 : case Kind::GEQ: newKind = Kind::BITVECTOR_SGE; break;
182 : 20 : case Kind::EQUAL:
183 : 20 : case Kind::ITE: break;
184 : 0 : default:
185 [ - - ]: 0 : if (childrenTypesChanged(current, cache))
186 : : {
187 : 0 : std::stringstream ss;
188 : 0 : ss << "Cannot translate " << current
189 : 0 : << " to a bit-vector term. Remove option `--solve-int-as-bv`.";
190 : 0 : throw LogicException(ss.str());
191 : 0 : }
192 : 0 : break;
193 : : }
194 : :
195 [ + + ]: 191 : for (size_t i = 0, csize = children.size(); i < csize; ++i)
196 : : {
197 : 128 : TypeNode type = children[i].getType();
198 [ + + ]: 128 : if (!type.isBitVector())
199 : : {
200 : 2 : continue;
201 : : }
202 : 126 : uint32_t bvsize = type.getBitVectorSize();
203 [ + + ]: 126 : if (bvsize < max)
204 : : {
205 : : // sign extend
206 : : Node signExtendOp = nm->mkConst<BitVectorSignExtend>(
207 : 65 : BitVectorSignExtend(max - bvsize));
208 : 65 : children[i] = nm->mkNode(signExtendOp, children[i]);
209 : 65 : }
210 [ + + ]: 128 : }
211 : : }
212 : :
213 : : // abort if the kind did not change and
214 : : // the original type was integer.
215 : : // The only exception is an ITE,
216 : : // in which case we continue.
217 [ + + ]: 101 : if (tn.isInteger() && newKind != Kind::ITE
218 [ + + ][ - + ]: 101 : && newKind == current.getKind())
[ - + ]
219 : : {
220 : 0 : std::stringstream ss;
221 : 0 : ss << "Cannot translate the operator " << current.getKind()
222 : 0 : << " to a bit-vector operator. Remove option `--solve-int-as-bv`.";
223 : 0 : throw LogicException(ss.str());
224 : 0 : }
225 : 148 : NodeBuilder builder(nm, newKind);
226 [ - + ]: 74 : if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
227 : : {
228 : 0 : builder << current.getOperator();
229 : : }
230 : 74 : builder.append(children);
231 : : // Mark the substitution and continue
232 : 74 : Node result = builder;
233 : :
234 : 74 : result = rewrite(result);
235 : 74 : cache[current] = result;
236 : 74 : }
237 : : else
238 : : {
239 : : // It's a leaf: could be a variable or a numeral
240 : 81 : Node result = current;
241 [ + + ]: 81 : if (current.isVar())
242 : : {
243 [ + + ]: 102 : if (CVC5_EQUAL(current.getType(), nm->integerType()))
244 : : {
245 : 64 : result = NodeManager::mkDummySkolem("__intToBV_var",
246 : 96 : nm->mkBitVectorType(size));
247 : : /**
248 : : * Correctly convert signed/unsigned BV values to Integers as follows
249 : : * x < 0 ? -nat(-x) : nat(x)
250 : : * where x refers to the bit-vector term `result`.
251 : : */
252 : 32 : BitVector bvzero(size, Integer(0));
253 : : Node negResult = nm->mkNode(Kind::BITVECTOR_UBV_TO_INT,
254 : 64 : nm->mkNode(Kind::BITVECTOR_NEG, result));
255 : 128 : Node bv2int = nm->mkNode(
256 : : Kind::ITE,
257 : 64 : {nm->mkNode(Kind::BITVECTOR_SLT, result, nm->mkConst(bvzero)),
258 : 64 : nm->mkNode(Kind::NEG, negResult),
259 : 96 : nm->mkNode(Kind::BITVECTOR_UBV_TO_INT, result)});
260 : 32 : d_preprocContext->addSubstitution(current, bv2int);
261 : 32 : }
262 : : }
263 [ + - ]: 47 : else if (current.isConst())
264 : : {
265 [ + + ]: 47 : if (current.getType().isInteger())
266 : : {
267 : 30 : Rational constant = current.getConst<Rational>();
268 [ - + ][ - + ]: 30 : Assert(constant.isIntegral());
[ - - ]
269 : 30 : BitVector bv(size, constant.getNumerator());
270 [ + + ]: 30 : if (bv.toSignedInteger() != constant.getNumerator())
271 : : {
272 : 1 : throw TypeCheckingExceptionPrivate(
273 : : current,
274 : 2 : string("Not enough bits for constant in intToBV: ")
275 : 4 : + current.toString());
276 : : }
277 : 29 : result = nm->mkConst(bv);
278 : 31 : }
279 : : }
280 : : else
281 : : {
282 : 0 : throw TypeCheckingExceptionPrivate(
283 : 0 : current, string("Cannot translate to BV: ") + current.toString());
284 : : }
285 : 80 : cache[current] = result;
286 : 81 : }
287 : 231 : }
288 [ + - ]: 52 : Trace("int-to-bv-debug") << "original: " << n << std::endl;
289 [ + - ]: 52 : Trace("int-to-bv-debug") << "binary: " << n_binary << std::endl;
290 [ + - ]: 52 : Trace("int-to-bv-debug") << "result: " << cache[n_binary] << std::endl;
291 : 104 : return cache[n_binary];
292 : 62 : }
293 : :
294 : 52018 : IntToBV::IntToBV(PreprocessingPassContext* preprocContext)
295 : 52018 : : PreprocessingPass(preprocContext, "int-to-bv") {};
296 : :
297 : 22 : PreprocessingPassResult IntToBV::applyInternal(
298 : : AssertionPipeline* assertionsToPreprocess)
299 : : {
300 : : // this pass is refutation unsound, "unsat" will be "unknown"
301 : 22 : assertionsToPreprocess->markRefutationUnsound();
302 : 22 : NodeMap cache;
303 [ + + ]: 74 : for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
304 : : {
305 : 52 : assertionsToPreprocess->replace(
306 : 114 : i, intToBV((*assertionsToPreprocess)[i], cache));
307 : : }
308 : 17 : return PreprocessingPassResult::NO_CONFLICT;
309 : 22 : }
310 : :
311 : : } // namespace passes
312 : : } // namespace preprocessing
313 : : } // namespace cvc5::internal
|
