GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bitblast/bitblast_utils.h Lines: 96 108 88.9 %
Date: 2021-03-23 Branches: 144 382 37.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bitblast_utils.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Dejan Jovanovic, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Various utility functions for bit-blasting.
13
 **
14
 ** Various utility functions for bit-blasting.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
20
#define CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
21
22
23
#include <ostream>
24
#include "expr/node.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace bv {
29
30
template <class T> class TBitblaster;
31
32
template <class T>
33
std::string toString (const std::vector<T>& bits);
34
35
template <> inline
36
std::string toString<Node> (const std::vector<Node>& bits) {
37
  std::ostringstream os;
38
  for (int i = bits.size() - 1; i >= 0; --i) {
39
    TNode bit = bits[i];
40
    if (bit.getKind() == kind::CONST_BOOLEAN) {
41
      os << (bit.getConst<bool>() ? "1" : "0");
42
    } else {
43
      os << bit<< " ";
44
    }
45
  }
46
  os <<"\n";
47
  return os.str();
48
}
49
50
template <class T> T mkTrue();
51
template <class T> T mkFalse();
52
template <class T> T mkNot(T a);
53
template <class T> T mkOr(T a, T b);
54
template <class T> T mkOr(const std::vector<T>& a);
55
template <class T> T mkAnd(T a, T b);
56
template <class T> T mkAnd(const std::vector<T>& a);
57
template <class T> T mkXor(T a, T b);
58
template <class T> T mkIff(T a, T b);
59
template <class T> T mkIte(T cond, T a, T b);
60
61
62
template <> inline
63
61911
Node mkTrue<Node>() {
64
61911
  return NodeManager::currentNM()->mkConst<bool>(true);
65
}
66
67
template <> inline
68
235454
Node mkFalse<Node>() {
69
235454
  return NodeManager::currentNM()->mkConst<bool>(false);
70
}
71
72
template <> inline
73
338384
Node mkNot<Node>(Node a) {
74
338384
  return NodeManager::currentNM()->mkNode(kind::NOT, a);
75
}
76
77
template <> inline
78
559290
Node mkOr<Node>(Node a, Node b) {
79
559290
  return NodeManager::currentNM()->mkNode(kind::OR, a, b);
80
}
81
82
template <> inline
83
Node mkOr<Node>(const std::vector<Node>& children) {
84
  Assert(children.size());
85
  if (children.size() == 1)
86
    return children[0];
87
  return NodeManager::currentNM()->mkNode(kind::OR, children);
88
}
89
90
91
template <> inline
92
1049709
Node mkAnd<Node>(Node a, Node b) {
93
1049709
  return NodeManager::currentNM()->mkNode(kind::AND, a, b);
94
}
95
96
template <> inline
97
53651
Node mkAnd<Node>(const std::vector<Node>& children) {
98
53651
  Assert(children.size());
99
53651
  if (children.size() == 1)
100
16688
    return children[0];
101
36963
  return NodeManager::currentNM()->mkNode(kind::AND, children);
102
}
103
104
105
template <> inline
106
812168
Node mkXor<Node>(Node a, Node b) {
107
812168
  return NodeManager::currentNM()->mkNode(kind::XOR, a, b);
108
}
109
110
template <> inline
111
708434
Node mkIff<Node>(Node a, Node b) {
112
708434
  return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
113
}
114
115
template <> inline
116
195584
Node mkIte<Node>(Node cond, Node a, Node b) {
117
195584
  return NodeManager::currentNM()->mkNode(kind::ITE, cond, a, b);
118
}
119
120
/*
121
 Various helper functions that get called by the bitblasting procedures
122
 */
123
124
template <class T>
125
23756
void inline extractBits(const std::vector<T>& b, std::vector<T>& dest, unsigned lo, unsigned hi) {
126
23756
  Assert(lo < b.size() && hi < b.size() && lo <= hi);
127
173326
  for (unsigned i = lo; i <= hi; ++i) {
128
149570
    dest.push_back(b[i]);
129
  }
130
23756
}
131
132
template <class T>
133
10700
void inline negateBits(const std::vector<T>& bits, std::vector<T>& negated_bits) {
134
83827
  for(unsigned i = 0; i < bits.size(); ++i) {
135
73127
    negated_bits.push_back(mkNot(bits[i]));
136
  }
137
10700
}
138
139
template <class T>
140
4000
bool inline isZero(const std::vector<T>& bits) {
141
5486
  for(unsigned i = 0; i < bits.size(); ++i) {
142
5372
    if(bits[i] != mkFalse<T>()) {
143
3886
      return false;
144
    }
145
  }
146
114
  return true;
147
}
148
149
template <class T>
150
3886
void inline rshift(std::vector<T>& bits, unsigned amount) {
151
38916
  for (unsigned i = 0; i < bits.size() - amount; ++i) {
152
35030
    bits[i] = bits[i+amount];
153
  }
154
7772
  for(unsigned i = bits.size() - amount; i < bits.size(); ++i) {
155
3886
    bits[i] = mkFalse<T>();
156
  }
157
3886
}
158
159
template <class T>
160
7772
void inline lshift(std::vector<T>& bits, unsigned amount) {
161
77832
  for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) {
162
70060
    bits[i] = bits[i-amount];
163
  }
164
15544
  for(unsigned i = 0; i < amount; ++i) {
165
7772
    bits[i] = mkFalse<T>();
166
  }
167
7772
}
168
169
template <class T>
170
6836
void inline makeZero(std::vector<T>& bits, unsigned width) {
171
6836
  Assert(bits.size() == 0);
172
66413
  for(unsigned i = 0; i < width; ++i) {
173
59577
    bits.push_back(mkFalse<T>());
174
  }
175
6836
}
176
177
178
/**
179
 * Constructs a simple ripple carry adder
180
 *
181
 * @param a first term to be added
182
 * @param b second term to be added
183
 * @param res the result
184
 * @param carry the carry-in bit
185
 *
186
 * @return the carry-out
187
 */
188
template <class T>
189
16904
T inline rippleCarryAdder(const std::vector<T>&a, const std::vector<T>& b, std::vector<T>& res, T carry) {
190
16904
  Assert(a.size() == b.size() && res.size() == 0);
191
192
197095
  for (unsigned i = 0 ; i < a.size(); ++i) {
193
360382
    T sum = mkXor(mkXor(a[i], b[i]), carry);
194
540573
    carry = mkOr( mkAnd(a[i], b[i]),
195
360382
                  mkAnd( mkXor(a[i], b[i]),
196
                         carry));
197
180191
    res.push_back(sum);
198
  }
199
200
16904
  return carry;
201
}
202
203
template <class T>
204
1074
inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, std::vector<T>& res) {
205
206
10862
  for (unsigned i = 0; i < a.size(); ++i) {
207
9788
    res.push_back(mkAnd(b[0], a[i]));
208
  }
209
210
9788
  for(unsigned k = 1; k < res.size(); ++k) {
211
17428
  T carry_in = mkFalse<T>();
212
17428
  T carry_out;
213
98156
    for(unsigned j = 0; j < res.size() -k; ++j) {
214
178884
      T aj = mkAnd(b[k], a[j]);
215
178884
      carry_out = mkOr(mkAnd(res[j+k], aj),
216
89442
                       mkAnd( mkXor(res[j+k], aj), carry_in));
217
89442
      res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
218
89442
      carry_in = carry_out;
219
    }
220
  }
221
1074
}
222
223
template <class T>
224
26801
T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
225
26801
  Assert(a.size() && b.size());
226
227
26801
  T res = mkAnd(mkNot(a[0]), b[0]);
228
229
26801
  if(orEqual) {
230
    res = mkOr(res, mkIff(a[0], b[0]));
231
  }
232
233
176260
  for (unsigned i = 1; i < a.size(); ++i) {
234
    // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i])
235
298918
    res = mkOr(mkAnd(mkIff(a[i], b[i]), res),
236
298918
               mkAnd(mkNot(a[i]), b[i]));
237
  }
238
26801
  return res;
239
}
240
241
template <class T>
242
14454
T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
243
14454
  Assert(a.size() && b.size());
244
14454
  if (a.size() == 1) {
245
2576
    if(orEqual) {
246
      return  mkOr(mkIff(a[0], b[0]),
247
                   mkAnd(a[0], mkNot(b[0])));
248
    }
249
250
2576
    return mkAnd(a[0], mkNot(b[0]));
251
  }
252
11878
  unsigned n = a.size() - 1;
253
23756
  std::vector<T> a1, b1;
254
11878
  extractBits(a, a1, 0, n-1);
255
11878
  extractBits(b, b1, 0, n-1);
256
257
  // unsigned comparison of the first n-1 bits
258
23756
  T ures = uLessThanBB(a1, b1, orEqual);
259
59390
  T res = mkOr(// a b have the same sign
260
23756
               mkAnd(mkIff(a[n], b[n]),
261
                     ures),
262
               // a is negative and b positive
263
11878
               mkAnd(a[n],
264
11878
                     mkNot(b[n])));
265
11878
  return res;
266
}
267
268
}  // namespace bv
269
}  // namespace theory
270
}  // namespace CVC4
271
272
#endif  // CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H