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 : : #include "expr/node.h"
20 : :
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : : namespace bv {
24 : :
25 : : template <class T> class TBitblaster;
26 : :
27 : : template <class T>
28 : : std::string toString (const std::vector<T>& bits);
29 : :
30 : : template <> inline
31 : 0 : std::string toString<Node> (const std::vector<Node>& bits) {
32 : 0 : std::ostringstream os;
33 [ - - ]: 0 : for (int i = bits.size() - 1; i >= 0; --i) {
34 : 0 : TNode bit = bits[i];
35 [ - - ]: 0 : if (bit.getKind() == Kind::CONST_BOOLEAN)
36 : : {
37 [ - - ]: 0 : os << (bit.getConst<bool>() ? "1" : "0");
38 : : }
39 : : else
40 : : {
41 : 0 : os << bit<< " ";
42 : : }
43 : 0 : }
44 : 0 : os <<"\n";
45 : 0 : return os.str();
46 : 0 : }
47 : :
48 : : template <class T>
49 : : T mkTrue(NodeManager* nm);
50 : : template <class T>
51 : : T mkFalse(NodeManager* nm);
52 : : template <class T> T mkNot(T a);
53 : : template <class T> T mkOr(T a, T b);
54 : : template <class T>
55 : : T mkOr(NodeManager* nm, const std::vector<T>& a);
56 : : template <class T> T mkAnd(T a, T b);
57 : : template <class T>
58 : : T mkAnd(NodeManager* nm, const std::vector<T>& a);
59 : : template <class T> T mkXor(T a, T b);
60 : : template <class T> T mkIff(T a, T b);
61 : : template <class T> T mkIte(T cond, T a, T b);
62 : :
63 : : template <>
64 : 98308 : inline Node mkTrue<Node>(NodeManager* nm)
65 : : {
66 : 196616 : return nm->mkConst<bool>(true);
67 : : }
68 : :
69 : : template <>
70 : 427513 : inline Node mkFalse<Node>(NodeManager* nm)
71 : : {
72 : 855026 : return nm->mkConst<bool>(false);
73 : : }
74 : :
75 : : template <> inline
76 : 467570 : Node mkNot<Node>(Node a) {
77 : 467570 : return NodeManager::mkNode(Kind::NOT, a);
78 : : }
79 : :
80 : : template <> inline
81 : 727629 : Node mkOr<Node>(Node a, Node b) {
82 : 727629 : return NodeManager::mkNode(Kind::OR, a, b);
83 : : }
84 : :
85 : : template <>
86 : : inline Node mkOr<Node>(NodeManager* nm, const std::vector<Node>& children)
87 : : {
88 : : Assert(children.size());
89 : : if (children.size() == 1) return children[0];
90 : : return nm->mkNode(Kind::OR, children);
91 : : }
92 : :
93 : : template <> inline
94 : 1449986 : Node mkAnd<Node>(Node a, Node b) {
95 : 1449986 : return NodeManager::mkNode(Kind::AND, a, b);
96 : : }
97 : :
98 : : template <>
99 : 77539 : inline Node mkAnd<Node>(NodeManager* nm, const std::vector<Node>& children)
100 : : {
101 [ - + ][ - + ]: 77539 : Assert(children.size());
[ - - ]
102 [ + + ]: 77539 : if (children.size() == 1) return children[0];
103 : 50742 : return nm->mkNode(Kind::AND, children);
104 : : }
105 : :
106 : : template <> inline
107 : 1156339 : Node mkXor<Node>(Node a, Node b) {
108 : 1156339 : return NodeManager::mkNode(Kind::XOR, a, b);
109 : : }
110 : :
111 : : template <> inline
112 : 900147 : Node mkIff<Node>(Node a, Node b) {
113 : 900147 : return NodeManager::mkNode(Kind::EQUAL, a, b);
114 : : }
115 : :
116 : : template <> inline
117 : 314951 : Node mkIte<Node>(Node cond, Node a, Node b) {
118 : 314951 : return NodeManager::mkNode(Kind::ITE, cond, a, b);
119 : : }
120 : :
121 : : /*
122 : : Various helper functions that get called by the bitblasting procedures
123 : : */
124 : :
125 : : template <class T>
126 : 25134 : void inline extractBits(const std::vector<T>& b, std::vector<T>& dest, unsigned lo, unsigned hi) {
127 [ + - ][ + - ]: 25134 : Assert(lo < b.size() && hi < b.size() && lo <= hi);
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
128 [ + + ]: 203260 : for (unsigned i = lo; i <= hi; ++i) {
129 : 178126 : dest.push_back(b[i]);
130 : : }
131 : 25134 : }
132 : :
133 : : template <class T>
134 : 17430 : void inline negateBits(const std::vector<T>& bits, std::vector<T>& negated_bits) {
135 [ + + ]: 134460 : for(unsigned i = 0; i < bits.size(); ++i) {
136 : 117030 : negated_bits.push_back(mkNot(bits[i]));
137 : : }
138 : 17430 : }
139 : :
140 : : template <class T>
141 : 4932 : bool inline isZero(NodeManager* nm, const std::vector<T>& bits)
142 : : {
143 [ + + ]: 6981 : for(unsigned i = 0; i < bits.size(); ++i) {
144 [ + + ]: 6729 : if (bits[i] != mkFalse<T>(nm))
145 : : {
146 : 4680 : return false;
147 : : }
148 : : }
149 : 252 : return true;
150 : : }
151 : :
152 : : template <class T>
153 : 4680 : void inline rshift(NodeManager* nm, std::vector<T>& bits, unsigned amount)
154 : : {
155 [ + + ]: 54121 : for (unsigned i = 0; i < bits.size() - amount; ++i) {
156 : 49441 : bits[i] = bits[i+amount];
157 : : }
158 [ + + ]: 9360 : for(unsigned i = bits.size() - amount; i < bits.size(); ++i) {
159 : 4680 : bits[i] = mkFalse<T>(nm);
160 : : }
161 : 4680 : }
162 : :
163 : : template <class T>
164 : 9360 : void inline lshift(NodeManager* nm, std::vector<T>& bits, unsigned amount)
165 : : {
166 [ + + ]: 108242 : for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) {
167 : 98882 : bits[i] = bits[i-amount];
168 : : }
169 [ + + ]: 18720 : for(unsigned i = 0; i < amount; ++i) {
170 : 9360 : bits[i] = mkFalse<T>(nm);
171 : : }
172 : 9360 : }
173 : :
174 : : template <class T>
175 : 9976 : void inline makeZero(NodeManager* nm, std::vector<T>& bits, unsigned width)
176 : : {
177 [ - + ][ - + ]: 9976 : Assert(bits.size() == 0);
[ - - ]
178 [ + + ]: 102357 : for(unsigned i = 0; i < width; ++i) {
179 : 92381 : bits.push_back(mkFalse<T>(nm));
180 : : }
181 : 9976 : }
182 : :
183 : : /**
184 : : * Constructs a simple ripple carry adder
185 : : *
186 : : * @param a first term to be added
187 : : * @param b second term to be added
188 : : * @param res the result
189 : : * @param carry the carry-in bit
190 : : *
191 : : * @return the carry-out
192 : : */
193 : : template <class T>
194 : 22529 : T inline rippleCarryAdder(const std::vector<T>&a, const std::vector<T>& b, std::vector<T>& res, T carry) {
195 [ + - ][ + - ]: 22529 : Assert(a.size() == b.size() && res.size() == 0);
[ - + ][ - + ]
[ - - ]
196 : :
197 [ + + ]: 272412 : for (unsigned i = 0 ; i < a.size(); ++i) {
198 : 499766 : T sum = mkXor(mkXor(a[i], b[i]), carry);
199 : 749649 : carry = mkOr( mkAnd(a[i], b[i]),
200 : 499766 : mkAnd( mkXor(a[i], b[i]),
201 : : carry));
202 : 249883 : res.push_back(sum);
203 : : }
204 : :
205 : 22529 : return carry;
206 : : }
207 : :
208 : : template <class T>
209 : 2507 : inline void shiftAddMultiplier(NodeManager* nm,
210 : : const std::vector<T>& a,
211 : : const std::vector<T>& b,
212 : : std::vector<T>& res)
213 : : {
214 [ + + ]: 22516 : for (unsigned i = 0; i < a.size(); ++i) {
215 : 20009 : res.push_back(mkAnd(b[0], a[i]));
216 : : }
217 : :
218 [ + + ]: 20009 : for(unsigned k = 1; k < res.size(); ++k) {
219 : 17502 : T carry_in = mkFalse<T>(nm);
220 : 17502 : T carry_out;
221 [ + + ]: 149241 : for(unsigned j = 0; j < res.size() -k; ++j) {
222 : 263478 : T aj = mkAnd(b[k], a[j]);
223 : 263478 : carry_out = mkOr(mkAnd(res[j+k], aj),
224 : 131739 : mkAnd( mkXor(res[j+k], aj), carry_in));
225 : 131739 : res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
226 : 131739 : carry_in = carry_out;
227 : : }
228 : : }
229 : 2507 : }
230 : :
231 : : template <class T>
232 : 29784 : T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
233 [ + - ][ + - ]: 29784 : Assert(a.size() && b.size());
[ - + ][ - + ]
[ - - ]
234 : :
235 : 59568 : T res = mkAnd(mkNot(a[0]), b[0]);
236 : :
237 [ - + ]: 29784 : if(orEqual) {
238 : 0 : res = mkOr(res, mkIff(a[0], b[0]));
239 : : }
240 : :
241 [ + + ]: 223493 : for (unsigned i = 1; i < a.size(); ++i) {
242 : : // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i])
243 : 387418 : res = mkOr(mkAnd(mkIff(a[i], b[i]), res),
244 : 387418 : mkAnd(mkNot(a[i]), b[i]));
245 : : }
246 : 29784 : return res;
247 : 0 : }
248 : :
249 : : template <class T>
250 : 14964 : T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
251 [ + - ][ + - ]: 14964 : Assert(a.size() && b.size());
[ - + ][ - + ]
[ - - ]
252 [ + + ]: 14964 : if (a.size() == 1) {
253 [ - + ]: 2397 : if(orEqual) {
254 : 0 : return mkOr(mkIff(a[0], b[0]),
255 : 0 : mkAnd(a[0], mkNot(b[0])));
256 : : }
257 : :
258 : 2397 : return mkAnd(a[0], mkNot(b[0]));
259 : : }
260 : 12567 : unsigned n = a.size() - 1;
261 : 12567 : std::vector<T> a1, b1;
262 : 12567 : extractBits(a, a1, 0, n-1);
263 : 12567 : extractBits(b, b1, 0, n-1);
264 : :
265 : : // unsigned comparison of the first n-1 bits
266 : 12567 : T ures = uLessThanBB(a1, b1, orEqual);
267 : 62835 : T res = mkOr(// a b have the same sign
268 : 25134 : mkAnd(mkIff(a[n], b[n]),
269 : : ures),
270 : : // a is negative and b positive
271 : 12567 : mkAnd(a[n],
272 : 12567 : mkNot(b[n])));
273 : 12567 : return res;
274 : 12567 : }
275 : :
276 : : } // namespace bv
277 : : } // namespace theory
278 : : } // namespace cvc5::internal
279 : :
280 : : #endif // CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
|
