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