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 : : * Various utility functions for bit-blasting.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
16 : : #define CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
17 : :
18 : : #include <ostream>
19 : :
20 : : #include "expr/node.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : : namespace bv {
25 : :
26 : : template <class T>
27 : : class TBitblaster;
28 : :
29 : : template <class T>
30 : : std::string toString(const std::vector<T>& bits);
31 : :
32 : : template <>
33 : 0 : inline std::string toString<Node>(const std::vector<Node>& bits)
34 : : {
35 : 0 : std::ostringstream os;
36 [ - - ]: 0 : for (int i = bits.size() - 1; i >= 0; --i)
37 : : {
38 : 0 : TNode bit = bits[i];
39 [ - - ]: 0 : if (bit.getKind() == Kind::CONST_BOOLEAN)
40 : : {
41 [ - - ]: 0 : os << (bit.getConst<bool>() ? "1" : "0");
42 : : }
43 : : else
44 : : {
45 : 0 : os << bit << " ";
46 : : }
47 : 0 : }
48 : 0 : os << "\n";
49 : 0 : return os.str();
50 : 0 : }
51 : :
52 : : template <class T>
53 : : T mkTrue(NodeManager* nm);
54 : : template <class T>
55 : : T mkFalse(NodeManager* nm);
56 : : template <class T>
57 : : T mkNot(T a);
58 : : template <class T>
59 : : T mkOr(T a, T b);
60 : : template <std::size_t N>
61 : : Node mkOr(const TNode (&children)[N]);
62 : : template <class T>
63 : : T mkOr(NodeManager* nm, const std::vector<T>& a);
64 : : template <class T>
65 : : T mkAnd(T a, T b);
66 : : template <std::size_t N>
67 : : Node mkAnd(const TNode (&children)[N]);
68 : : template <class T>
69 : : T mkAnd(NodeManager* nm, const std::vector<T>& a);
70 : : template <class T>
71 : : T mkXor(T a, T b);
72 : : template <class T>
73 : : T mkIff(T a, T b);
74 : : template <class T>
75 : : T mkIte(T cond, T a, T b);
76 : :
77 : : template <>
78 : 115904 : inline Node mkTrue<Node>(NodeManager* nm)
79 : : {
80 : 231808 : return nm->mkConst<bool>(true);
81 : : }
82 : :
83 : : template <>
84 : 997083 : inline Node mkFalse<Node>(NodeManager* nm)
85 : : {
86 : 1994166 : return nm->mkConst<bool>(false);
87 : : }
88 : :
89 : : template <>
90 : 743872 : inline Node mkNot<Node>(Node a)
91 : : {
92 : 743872 : return NodeManager::mkNode(Kind::NOT, a);
93 : : }
94 : :
95 : : template <>
96 : 193845 : inline Node mkOr<Node>(Node a, Node b)
97 : : {
98 : 193845 : return NodeManager::mkNode(Kind::OR, a, b);
99 : : }
100 : :
101 : : template <std::size_t N>
102 : 1331363 : inline Node mkOr(const TNode (&children)[N])
103 : : {
104 : : static_assert(N >= 1, "mkOr requires at least 1 child!");
105 : : if constexpr (N == 1) return children[0];
106 : 1331363 : return NodeManager::mkNode(Kind::OR, children);
107 : : }
108 : :
109 : : template <>
110 : : inline Node mkOr<Node>(NodeManager* nm, const std::vector<Node>& children)
111 : : {
112 : : Assert(children.size());
113 : : if (children.size() == 1) return children[0];
114 : : return nm->mkNode(Kind::OR, children);
115 : : }
116 : :
117 : : template <>
118 : 2913706 : inline Node mkAnd<Node>(Node a, Node b)
119 : : {
120 : 2913706 : return NodeManager::mkNode(Kind::AND, a, b);
121 : : }
122 : :
123 : : template <std::size_t N>
124 : 82314 : inline Node mkAnd(const TNode (&children)[N])
125 : : {
126 : : static_assert(N >= 1, "mkAnd requires at least 1 child!");
127 : : if constexpr (N == 1) return children[0];
128 : 82314 : return NodeManager::mkNode(Kind::AND, children);
129 : : }
130 : :
131 : : template <>
132 : 90150 : inline Node mkAnd<Node>(NodeManager* nm, const std::vector<Node>& children)
133 : : {
134 [ - + ][ - + ]: 90150 : Assert(children.size());
[ - - ]
135 [ + + ]: 90150 : if (children.size() == 1) return children[0];
136 : 61376 : return nm->mkNode(Kind::AND, children);
137 : : }
138 : :
139 : : template <>
140 : 3364334 : inline Node mkXor<Node>(Node a, Node b)
141 : : {
142 : 3364334 : return NodeManager::mkNode(Kind::XOR, a, b);
143 : : }
144 : :
145 : : template <>
146 : 1109790 : inline Node mkIff<Node>(Node a, Node b)
147 : : {
148 : 1109790 : return NodeManager::mkNode(Kind::EQUAL, a, b);
149 : : }
150 : :
151 : : template <>
152 : 1027199 : inline Node mkIte<Node>(Node cond, Node a, Node b)
153 : : {
154 : 1027199 : return NodeManager::mkNode(Kind::ITE, cond, a, b);
155 : : }
156 : :
157 : : /*
158 : : Various helper functions that get called by the bitblasting procedures
159 : : */
160 : :
161 : : template <class T>
162 : 24992 : void inline extractBits(const std::vector<T>& b,
163 : : std::vector<T>& dest,
164 : : unsigned lo,
165 : : unsigned hi)
166 : : {
167 [ + - ][ + - ]: 24992 : Assert(lo < b.size() && hi < b.size() && lo <= hi);
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
168 [ + + ]: 211910 : for (unsigned i = lo; i <= hi; ++i)
169 : : {
170 : 186918 : dest.push_back(b[i]);
171 : : }
172 : 24992 : }
173 : :
174 : : template <class T>
175 : 21556 : void inline negateBits(const std::vector<T>& bits, std::vector<T>& negated_bits)
176 : : {
177 [ + + ]: 378733 : for (unsigned i = 0; i < bits.size(); ++i)
178 : : {
179 : 357177 : negated_bits.push_back(mkNot(bits[i]));
180 : : }
181 : 21556 : }
182 : :
183 : : template <class T>
184 : 7252 : bool inline isZero(NodeManager* nm, const std::vector<T>& bits)
185 : : {
186 [ + + ]: 38867 : for (unsigned i = 0; i < bits.size(); ++i)
187 : : {
188 [ + + ]: 38745 : if (bits[i] != mkFalse<T>(nm))
189 : : {
190 : 7130 : return false;
191 : : }
192 : : }
193 : 122 : return true;
194 : : }
195 : :
196 : : template <class T>
197 : 7130 : void inline rshift(NodeManager* nm, std::vector<T>& bits, unsigned amount)
198 : : {
199 [ + + ]: 287293 : for (unsigned i = 0; i < bits.size() - amount; ++i)
200 : : {
201 : 280163 : bits[i] = bits[i + amount];
202 : : }
203 [ + + ]: 14260 : for (unsigned i = bits.size() - amount; i < bits.size(); ++i)
204 : : {
205 : 7130 : bits[i] = mkFalse<T>(nm);
206 : : }
207 : 7130 : }
208 : :
209 : : template <class T>
210 : 14260 : void inline lshift(NodeManager* nm, std::vector<T>& bits, unsigned amount)
211 : : {
212 [ + + ]: 574586 : for (int i = (int)bits.size() - 1; i >= (int)amount; --i)
213 : : {
214 : 560326 : bits[i] = bits[i - amount];
215 : : }
216 [ + + ]: 28520 : for (unsigned i = 0; i < amount; ++i)
217 : : {
218 : 14260 : bits[i] = mkFalse<T>(nm);
219 : : }
220 : 14260 : }
221 : :
222 : : template <class T>
223 : 12202 : void inline makeZero(NodeManager* nm, std::vector<T>& bits, unsigned width)
224 : : {
225 [ - + ][ - + ]: 12202 : Assert(bits.size() == 0);
[ - - ]
226 [ + + ]: 343366 : for (unsigned i = 0; i < width; ++i)
227 : : {
228 : 331164 : bits.push_back(mkFalse<T>(nm));
229 : : }
230 : 12202 : }
231 : :
232 : : /**
233 : : * Constructs a simple ripple carry adder
234 : : *
235 : : * @param a first term to be added
236 : : * @param b second term to be added
237 : : * @param res the result
238 : : * @param carry the carry-in bit
239 : : *
240 : : * @return the carry-out
241 : : */
242 : : template <class T>
243 : 30265 : T inline rippleCarryAdder(const std::vector<T>& a,
244 : : const std::vector<T>& b,
245 : : std::vector<T>& res,
246 : : T carry)
247 : : {
248 [ + - ][ + - ]: 30265 : Assert(a.size() == b.size() && res.size() == 0);
[ - + ][ - + ]
[ - - ]
249 : :
250 [ + + ]: 993323 : for (unsigned i = 0; i < a.size(); ++i)
251 : : {
252 : 1926116 : T sum = mkXor(mkXor(a[i], b[i]), carry);
253 [ + + ][ - - ]: 2889174 : carry = mkOr({mkAnd(a[i], b[i]), mkAnd(mkXor(a[i], b[i]), carry)});
254 : 963058 : res.push_back(sum);
255 : : }
256 : :
257 : 30265 : return carry;
258 : : }
259 : :
260 : : template <class T>
261 : 2524 : inline void shiftAddMultiplier(NodeManager* nm,
262 : : const std::vector<T>& a,
263 : : const std::vector<T>& b,
264 : : std::vector<T>& res)
265 : : {
266 [ + + ]: 23465 : for (unsigned i = 0; i < a.size(); ++i)
267 : : {
268 : 20941 : res.push_back(mkAnd(b[0], a[i]));
269 : : }
270 : :
271 [ + + ]: 20941 : for (unsigned k = 1; k < res.size(); ++k)
272 : : {
273 : 18417 : T carry_in = mkFalse<T>(nm);
274 : 18417 : T carry_out;
275 [ + + ]: 172721 : for (unsigned j = 0; j < res.size() - k; ++j)
276 : : {
277 : 308608 : T aj = mkAnd(b[k], a[j]);
278 [ + + ][ - - ]: 925824 : carry_out =
279 : 771520 : mkOr({mkAnd(res[j + k], aj), mkAnd(mkXor(res[j + k], aj), carry_in)});
280 : 154304 : res[j + k] = mkXor(mkXor(res[j + k], aj), carry_in);
281 : 154304 : carry_in = carry_out;
282 : : }
283 : : }
284 : 2524 : }
285 : :
286 : : template <class T>
287 : 28962 : T inline uLessThanBB(const std::vector<T>& a,
288 : : const std::vector<T>& b,
289 : : bool orEqual)
290 : : {
291 [ + - ][ + - ]: 28962 : Assert(a.size() && b.size());
[ - + ][ - + ]
[ - - ]
292 : :
293 : 57924 : T res = mkAnd(mkNot(a[0]), b[0]);
294 : :
295 [ - + ]: 28962 : if (orEqual)
296 : : {
297 : 0 : res = mkOr(res, mkIff(a[0], b[0]));
298 : : }
299 : :
300 [ + + ]: 230467 : for (unsigned i = 1; i < a.size(); ++i)
301 : : {
302 : : // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i])
303 [ + + ][ - - ]: 604515 : res = mkOr({mkAnd(mkIff(a[i], b[i]), res), mkAnd(mkNot(a[i]), b[i])});
304 : : }
305 : 28962 : return res;
306 : 0 : }
307 : :
308 : : template <class T>
309 : 14654 : T inline sLessThanBB(const std::vector<T>& a,
310 : : const std::vector<T>& b,
311 : : bool orEqual)
312 : : {
313 [ + - ][ + - ]: 14654 : Assert(a.size() && b.size());
[ - + ][ - + ]
[ - - ]
314 [ + + ]: 14654 : if (a.size() == 1)
315 : : {
316 [ - + ]: 2158 : if (orEqual)
317 : : {
318 : 0 : return mkOr({mkIff(a[0], b[0]), mkAnd(a[0], mkNot(b[0]))});
319 : : }
320 : :
321 : 2158 : return mkAnd(a[0], mkNot(b[0]));
322 : : }
323 : 12496 : unsigned n = a.size() - 1;
324 : 12496 : std::vector<T> a1, b1;
325 : 12496 : extractBits(a, a1, 0, n - 1);
326 : 12496 : extractBits(b, b1, 0, n - 1);
327 : :
328 : : // unsigned comparison of the first n-1 bits
329 : 12496 : T ures = uLessThanBB(a1, b1, orEqual);
330 : 99968 : T res = mkOr({// a b have the same sign
331 : 24992 : mkAnd(mkIff(a[n], b[n]), ures),
332 : : // a is negative and b positive
333 : 24992 : mkAnd(a[n], mkNot(b[n]))});
334 : 12496 : return res;
335 : 12496 : }
336 : :
337 : : } // namespace bv
338 : : } // namespace theory
339 : : } // namespace cvc5::internal
340 : :
341 : : #endif // CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
|
