Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Liana Hadarean, Aina Niemetz, Daniel Larraz
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 : : * Various utility functions for bit-blasting.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
19 : : #define CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
20 : :
21 : : #include <ostream>
22 : : #include "expr/node.h"
23 : :
24 : : namespace cvc5::internal {
25 : : namespace theory {
26 : : namespace bv {
27 : :
28 : : template <class T> class TBitblaster;
29 : :
30 : : template <class T>
31 : : std::string toString (const std::vector<T>& bits);
32 : :
33 : : template <> inline
34 : 0 : std::string toString<Node> (const std::vector<Node>& bits) {
35 : 0 : std::ostringstream os;
36 [ - - ]: 0 : for (int i = bits.size() - 1; i >= 0; --i) {
37 : 0 : TNode bit = bits[i];
38 [ - - ]: 0 : if (bit.getKind() == Kind::CONST_BOOLEAN)
39 : : {
40 [ - - ]: 0 : os << (bit.getConst<bool>() ? "1" : "0");
41 : : }
42 : : else
43 : : {
44 : 0 : os << bit<< " ";
45 : : }
46 : : }
47 : 0 : os <<"\n";
48 : 0 : return os.str();
49 : : }
50 : :
51 : : template <class T>
52 : : T mkTrue(NodeManager* nm);
53 : : template <class T>
54 : : T mkFalse(NodeManager* nm);
55 : : template <class T> T mkNot(T a);
56 : : template <class T> T mkOr(T a, T b);
57 : : template <class T>
58 : : T mkOr(NodeManager* nm, const std::vector<T>& a);
59 : : template <class T> T mkAnd(T a, T b);
60 : : template <class T>
61 : : T mkAnd(NodeManager* nm, const std::vector<T>& a);
62 : : template <class T> T mkXor(T a, T b);
63 : : template <class T> T mkIff(T a, T b);
64 : : template <class T> T mkIte(T cond, T a, T b);
65 : :
66 : : template <>
67 : 158979 : inline Node mkTrue<Node>(NodeManager* nm)
68 : : {
69 : 317958 : return nm->mkConst<bool>(true);
70 : : }
71 : :
72 : : template <>
73 : 415590 : inline Node mkFalse<Node>(NodeManager* nm)
74 : : {
75 : 831180 : return nm->mkConst<bool>(false);
76 : : }
77 : :
78 : : template <> inline
79 : 429156 : Node mkNot<Node>(Node a) {
80 : 429156 : return NodeManager::mkNode(Kind::NOT, a);
81 : : }
82 : :
83 : : template <> inline
84 : 1030460 : Node mkOr<Node>(Node a, Node b) {
85 : 1030460 : return NodeManager::mkNode(Kind::OR, a, b);
86 : : }
87 : :
88 : : template <>
89 : : inline Node mkOr<Node>(NodeManager* nm, const std::vector<Node>& children)
90 : : {
91 : : Assert(children.size());
92 : : if (children.size() == 1) return children[0];
93 : : return nm->mkNode(Kind::OR, children);
94 : : }
95 : :
96 : : template <> inline
97 : 1549020 : Node mkAnd<Node>(Node a, Node b) {
98 : 1549020 : return NodeManager::mkNode(Kind::AND, a, b);
99 : : }
100 : :
101 : : template <>
102 : 78885 : inline Node mkAnd<Node>(NodeManager* nm, const std::vector<Node>& children)
103 : : {
104 [ - + ][ - + ]: 78885 : Assert(children.size());
[ - - ]
105 [ + + ]: 78885 : if (children.size() == 1) return children[0];
106 : 51209 : return nm->mkNode(Kind::AND, children);
107 : : }
108 : :
109 : : template <> inline
110 : 1342130 : Node mkXor<Node>(Node a, Node b) {
111 : 1342130 : return NodeManager::mkNode(Kind::XOR, a, b);
112 : : }
113 : :
114 : : template <> inline
115 : 1040200 : Node mkIff<Node>(Node a, Node b) {
116 : 1040200 : return NodeManager::mkNode(Kind::EQUAL, a, b);
117 : : }
118 : :
119 : : template <> inline
120 : 287473 : Node mkIte<Node>(Node cond, Node a, Node b) {
121 : 287473 : return NodeManager::mkNode(Kind::ITE, cond, a, b);
122 : : }
123 : :
124 : : /*
125 : : Various helper functions that get called by the bitblasting procedures
126 : : */
127 : :
128 : : template <class T>
129 : 22824 : void inline extractBits(const std::vector<T>& b, std::vector<T>& dest, unsigned lo, unsigned hi) {
130 [ + - ][ + - ]: 45648 : Assert(lo < b.size() && hi < b.size() && lo <= hi);
[ + - ][ - + ]
[ - - ]
131 [ + + ]: 171732 : for (unsigned i = lo; i <= hi; ++i) {
132 : 148908 : dest.push_back(b[i]);
133 : : }
134 : 22824 : }
135 : :
136 : : template <class T>
137 : 16675 : void inline negateBits(const std::vector<T>& bits, std::vector<T>& negated_bits) {
138 [ + + ]: 122621 : for(unsigned i = 0; i < bits.size(); ++i) {
139 : 105946 : negated_bits.push_back(mkNot(bits[i]));
140 : : }
141 : 16675 : }
142 : :
143 : : template <class T>
144 : 5007 : bool inline isZero(NodeManager* nm, const std::vector<T>& bits)
145 : : {
146 [ + + ]: 7063 : for(unsigned i = 0; i < bits.size(); ++i) {
147 [ + + ]: 6823 : if (bits[i] != mkFalse<T>(nm))
148 : : {
149 : 4767 : return false;
150 : : }
151 : : }
152 : 240 : return true;
153 : : }
154 : :
155 : : template <class T>
156 : 4767 : void inline rshift(NodeManager* nm, std::vector<T>& bits, unsigned amount)
157 : : {
158 [ + + ]: 57130 : for (unsigned i = 0; i < bits.size() - amount; ++i) {
159 : 52363 : bits[i] = bits[i+amount];
160 : : }
161 [ + + ]: 9534 : for(unsigned i = bits.size() - amount; i < bits.size(); ++i) {
162 : 4767 : bits[i] = mkFalse<T>(nm);
163 : : }
164 : 4767 : }
165 : :
166 : : template <class T>
167 : 9534 : void inline lshift(NodeManager* nm, std::vector<T>& bits, unsigned amount)
168 : : {
169 [ + + ]: 114260 : for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) {
170 : 104726 : bits[i] = bits[i-amount];
171 : : }
172 [ + + ]: 19068 : for(unsigned i = 0; i < amount; ++i) {
173 : 9534 : bits[i] = mkFalse<T>(nm);
174 : : }
175 : 9534 : }
176 : :
177 : : template <class T>
178 : 9563 : void inline makeZero(NodeManager* nm, std::vector<T>& bits, unsigned width)
179 : : {
180 [ - + ][ - + ]: 9563 : Assert(bits.size() == 0);
[ - - ]
181 [ + + ]: 99919 : for(unsigned i = 0; i < width; ++i) {
182 : 90356 : bits.push_back(mkFalse<T>(nm));
183 : : }
184 : 9563 : }
185 : :
186 : : /**
187 : : * Constructs a simple ripple carry adder
188 : : *
189 : : * @param a first term to be added
190 : : * @param b second term to be added
191 : : * @param res the result
192 : : * @param carry the carry-in bit
193 : : *
194 : : * @return the carry-out
195 : : */
196 : : template <class T>
197 : 23068 : T inline rippleCarryAdder(const std::vector<T>&a, const std::vector<T>& b, std::vector<T>& res, T carry) {
198 [ + - ][ + - ]: 46136 : Assert(a.size() == b.size() && res.size() == 0);
[ - + ][ - - ]
199 : :
200 [ + + ]: 332842 : for (unsigned i = 0 ; i < a.size(); ++i) {
201 : 929322 : T sum = mkXor(mkXor(a[i], b[i]), carry);
202 : 929322 : carry = mkOr( mkAnd(a[i], b[i]),
203 : 619548 : mkAnd( mkXor(a[i], b[i]),
204 : : carry));
205 : 309774 : res.push_back(sum);
206 : : }
207 : :
208 : 23068 : return carry;
209 : : }
210 : :
211 : : template <class T>
212 : 2733 : inline void shiftAddMultiplier(NodeManager* nm,
213 : : const std::vector<T>& a,
214 : : const std::vector<T>& b,
215 : : std::vector<T>& res)
216 : : {
217 [ + + ]: 23775 : for (unsigned i = 0; i < a.size(); ++i) {
218 : 21042 : res.push_back(mkAnd(b[0], a[i]));
219 : : }
220 : :
221 [ + + ]: 21042 : for(unsigned k = 1; k < res.size(); ++k) {
222 : 36618 : T carry_in = mkFalse<T>(nm);
223 : 36618 : T carry_out;
224 [ + + ]: 154093 : for(unsigned j = 0; j < res.size() -k; ++j) {
225 : 407352 : T aj = mkAnd(b[k], a[j]);
226 : 271568 : carry_out = mkOr(mkAnd(res[j+k], aj),
227 : 135784 : mkAnd( mkXor(res[j+k], aj), carry_in));
228 : 135784 : res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
229 : 135784 : carry_in = carry_out;
230 : : }
231 : : }
232 : 2733 : }
233 : :
234 : : template <class T>
235 : 27188 : T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
236 [ + - ][ + - ]: 54376 : Assert(a.size() && b.size());
[ - + ][ - - ]
237 : :
238 : 54376 : T res = mkAnd(mkNot(a[0]), b[0]);
239 : :
240 [ - + ]: 27188 : if(orEqual) {
241 : 0 : res = mkOr(res, mkIff(a[0], b[0]));
242 : : }
243 : :
244 [ + + ]: 203426 : for (unsigned i = 1; i < a.size(); ++i) {
245 : : // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i])
246 : 352476 : res = mkOr(mkAnd(mkIff(a[i], b[i]), res),
247 : 352476 : mkAnd(mkNot(a[i]), b[i]));
248 : : }
249 : 27188 : return res;
250 : : }
251 : :
252 : : template <class T>
253 : 13607 : T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
254 [ + - ][ + - ]: 27214 : Assert(a.size() && b.size());
[ - + ][ - - ]
255 [ + + ]: 13607 : if (a.size() == 1) {
256 [ - + ]: 2195 : if(orEqual) {
257 : 0 : return mkOr(mkIff(a[0], b[0]),
258 : 0 : mkAnd(a[0], mkNot(b[0])));
259 : : }
260 : :
261 : 2195 : return mkAnd(a[0], mkNot(b[0]));
262 : : }
263 : 11412 : unsigned n = a.size() - 1;
264 : 22824 : std::vector<T> a1, b1;
265 : 11412 : extractBits(a, a1, 0, n-1);
266 : 11412 : extractBits(b, b1, 0, n-1);
267 : :
268 : : // unsigned comparison of the first n-1 bits
269 : 22824 : T ures = uLessThanBB(a1, b1, orEqual);
270 : 68472 : T res = mkOr(// a b have the same sign
271 : 22824 : mkAnd(mkIff(a[n], b[n]),
272 : : ures),
273 : : // a is negative and b positive
274 : 11412 : mkAnd(a[n],
275 : 11412 : mkNot(b[n])));
276 : 11412 : return res;
277 : : }
278 : :
279 : : } // namespace bv
280 : : } // namespace theory
281 : : } // namespace cvc5::internal
282 : :
283 : : #endif // CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
|
