GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_rewrite_rules_core.h Lines: 144 144 100.0 %
Date: 2021-03-23 Branches: 265 460 57.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_rewrite_rules_core.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Liana Hadarean, Clark Barrett
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#pragma once
21
22
#include "theory/bv/theory_bv_rewrite_rules.h"
23
#include "theory/bv/theory_bv_utils.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace bv {
28
29
/* -------------------------------------------------------------------------- */
30
31
template<> inline
32
402458
bool RewriteRule<ConcatFlatten>::applies(TNode node) {
33
402458
  return (node.getKind() == kind::BITVECTOR_CONCAT);
34
}
35
36
template<> inline
37
201229
Node RewriteRule<ConcatFlatten>::apply(TNode node) {
38
201229
  Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
39
402458
  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
40
402458
  std::vector<Node> processing_stack;
41
201229
  processing_stack.push_back(node);
42
1726275
  while (!processing_stack.empty()) {
43
1525046
    Node current = processing_stack.back();
44
762523
    processing_stack.pop_back();
45
762523
    if (current.getKind() == kind::BITVECTOR_CONCAT) {
46
767242
      for (int i = current.getNumChildren() - 1; i >= 0; i--)
47
561294
        processing_stack.push_back(current[i]);
48
    } else {
49
556575
      result << current;
50
    }
51
  }
52
201229
  Node resultNode = result;
53
201229
  Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << resultNode << ")" << std::endl;
54
402458
  return resultNode;
55
}
56
57
/* -------------------------------------------------------------------------- */
58
59
template<> inline
60
402458
bool RewriteRule<ConcatExtractMerge>::applies(TNode node) {
61
402458
  return (node.getKind() == kind::BITVECTOR_CONCAT);
62
}
63
64
template<> inline
65
201229
Node RewriteRule<ConcatExtractMerge>::apply(TNode node) {
66
67
201229
  Debug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
68
69
402458
  std::vector<Node> mergedExtracts;
70
71
402458
  Node current = node[0];
72
201229
  bool mergeStarted = false;
73
201229
  unsigned currentHigh = 0;
74
201229
  unsigned currentLow  = 0;
75
76
556575
  for(size_t i = 1, end = node.getNumChildren(); i < end; ++ i) {
77
    // The next candidate for merging
78
429890
    Node next = node[i];
79
    // If the current is not an extract we just go to the next
80
636148
    if (current.getKind() != kind::BITVECTOR_EXTRACT) {
81
280802
      mergedExtracts.push_back(current);
82
280802
      current = next;
83
280802
      continue;
84
    }
85
    // If it is an extract and the first one, get the extract parameters
86
74544
    else if (!mergeStarted) {
87
74510
      currentHigh = utils::getExtractHigh(current);
88
74510
      currentLow = utils::getExtractLow(current);
89
    }
90
91
    // If the next one can be merged, try to merge
92
74544
    bool merged = false;
93
74544
    if (next.getKind() == kind::BITVECTOR_EXTRACT && current[0] == next[0]) {
94
      // x[i : j] @ x[j - 1 : k] -> c x[i : k]
95
22436
      unsigned nextHigh = utils::getExtractHigh(next);
96
22436
      unsigned nextLow  = utils::getExtractLow(next);
97
22436
      if(nextHigh + 1 == currentLow) {
98
81
        currentLow = nextLow;
99
81
        mergeStarted = true;
100
81
        merged = true;
101
      }
102
    }
103
    // If we haven't merged anything, add the previous merge and continue with the next
104
74544
    if (!merged) {
105
74463
      if (!mergeStarted) mergedExtracts.push_back(current);
106
10
      else mergedExtracts.push_back(utils::mkExtract(current[0], currentHigh, currentLow));
107
74463
      current = next;
108
74463
      mergeStarted = false;
109
    }
110
  }
111
112
  // Add the last child
113
201229
  if (!mergeStarted) mergedExtracts.push_back(current);
114
47
  else mergedExtracts.push_back(utils::mkExtract(current[0], currentHigh, currentLow));
115
116
  // Return the result
117
402458
  return utils::mkConcat(mergedExtracts);
118
}
119
120
/* -------------------------------------------------------------------------- */
121
122
template<> inline
123
402423
bool RewriteRule<ConcatConstantMerge>::applies(TNode node) {
124
402423
  return node.getKind() == kind::BITVECTOR_CONCAT;
125
}
126
127
template<> inline
128
201194
Node RewriteRule<ConcatConstantMerge>::apply(TNode node) {
129
130
201194
  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
131
132
402388
  std::vector<Node> mergedConstants;
133
711577
  for (unsigned i = 0, end = node.getNumChildren(); i < end;) {
134
510383
    if (node[i].getKind() != kind::CONST_BITVECTOR) {
135
      // If not a constant, just add it
136
337149
      mergedConstants.push_back(node[i]);
137
337149
      ++i;
138
    } else {
139
      // Find the longest sequence of constants
140
173234
      unsigned j = i + 1;
141
265386
      while (j < end) {
142
142117
        if (node[j].getKind() != kind::CONST_BITVECTOR) {
143
96041
          break;
144
        } else {
145
46076
          ++ j;
146
        }
147
      }
148
      // Append all the constants
149
346468
      BitVector current = node[i].getConst<BitVector>();
150
219310
      for (unsigned k = i + 1; k < j; ++ k) {
151
46076
        current = current.concat(node[k].getConst<BitVector>());
152
      }
153
      // Add the new merged constant
154
173234
      mergedConstants.push_back(utils::mkConst(current));
155
173234
      i = j;
156
    }
157
  }
158
159
201194
  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;
160
161
402388
  return utils::mkConcat(mergedConstants);
162
}
163
164
/* -------------------------------------------------------------------------- */
165
166
template<> inline
167
684984
bool RewriteRule<ExtractWhole>::applies(TNode node) {
168
684984
  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
169
220274
  unsigned length = utils::getSize(node[0]);
170
220274
  unsigned extractHigh = utils::getExtractHigh(node);
171
220274
  if (extractHigh != length - 1) return false;
172
83223
  unsigned extractLow  = utils::getExtractLow(node);
173
83223
  if (extractLow != 0) return false;
174
14383
  return true;
175
}
176
177
template<> inline
178
10671
Node RewriteRule<ExtractWhole>::apply(TNode node) {
179
10671
  Debug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
180
10671
  return node[0];
181
}
182
183
/* -------------------------------------------------------------------------- */
184
185
template<> inline
186
230159
bool RewriteRule<ExtractConstant>::applies(TNode node) {
187
230159
  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
188
230159
  if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
189
118610
  return true;
190
}
191
192
template<> inline
193
59305
Node RewriteRule<ExtractConstant>::apply(TNode node) {
194
59305
  Debug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
195
118610
  Node child = node[0];
196
118610
  BitVector childValue = child.getConst<BitVector>();
197
118610
  return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node)));
198
}
199
200
/* -------------------------------------------------------------------------- */
201
202
template<> inline
203
190292
bool RewriteRule<ExtractConcat>::applies(TNode node) {
204
  //Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
205
190292
  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
206
190292
  if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false;
207
16496
  return true;
208
}
209
210
template<> inline
211
8248
Node RewriteRule<ExtractConcat>::apply(TNode node) {
212
8248
  Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
213
8248
  int extract_high = utils::getExtractHigh(node);
214
8248
  int extract_low = utils::getExtractLow(node);
215
216
16496
  std::vector<Node> resultChildren;
217
218
16496
  Node concat = node[0];
219
24601
  for (int i = concat.getNumChildren() - 1; i >= 0 && extract_high >= 0; i--) {
220
32706
    Node concatChild = concat[i];
221
16353
    int concatChildSize = utils::getSize(concatChild);
222
16353
    if (extract_low < concatChildSize) {
223
14436
      int extract_start = extract_low < 0 ? 0 : extract_low;
224
14436
      int extract_end = extract_high < concatChildSize ? extract_high : concatChildSize - 1;
225
14436
      resultChildren.push_back(utils::mkExtract(concatChild, extract_end, extract_start));
226
    }
227
16353
    extract_low -= concatChildSize;
228
16353
    extract_high -= concatChildSize;
229
  }
230
231
8248
  std::reverse(resultChildren.begin(), resultChildren.end());
232
233
16496
  return utils::mkConcat(resultChildren);
234
}
235
236
/* -------------------------------------------------------------------------- */
237
238
template<> inline
239
172895
bool RewriteRule<ExtractExtract>::applies(TNode node) {
240
172895
  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
241
113590
  if (node[0].getKind() != kind::BITVECTOR_EXTRACT) return false;
242
4082
  return true;
243
}
244
245
template<> inline
246
2041
Node RewriteRule<ExtractExtract>::apply(TNode node) {
247
2041
  Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
248
249
  // x[i:j][k:l] ~>  x[k+j:l+j]
250
4082
  Node child = node[0];
251
2041
  unsigned k = utils::getExtractHigh(node);
252
2041
  unsigned l = utils::getExtractLow(node);
253
2041
  unsigned j = utils::getExtractLow(child);
254
255
2041
  Node result = utils::mkExtract(child[0], k + j, l + j);
256
4082
  return result;
257
}
258
259
/* -------------------------------------------------------------------------- */
260
261
template<> inline
262
590316
bool RewriteRule<FailEq>::applies(TNode node) {
263
  //Debug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
264
590316
  if (node.getKind() != kind::EQUAL) return false;
265
590316
  if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
266
164421
  if (node[1].getKind() != kind::CONST_BITVECTOR) return false;
267
145049
  return node[0] != node[1];
268
}
269
270
template<> inline
271
70367
Node RewriteRule<FailEq>::apply(TNode node) {
272
70367
  return utils::mkFalse();
273
}
274
275
/* -------------------------------------------------------------------------- */
276
277
template<> inline
278
527591
bool RewriteRule<SimplifyEq>::applies(TNode node) {
279
527591
  if (node.getKind() != kind::EQUAL) return false;
280
457224
  return node[0] == node[1];
281
}
282
283
template<> inline
284
7642
Node RewriteRule<SimplifyEq>::apply(TNode node) {
285
7642
  Debug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
286
7642
  return utils::mkTrue();
287
}
288
289
/* -------------------------------------------------------------------------- */
290
291
template<> inline
292
565322
bool RewriteRule<ReflexivityEq>::applies(TNode node) {
293
565322
  return (node.getKind() == kind::EQUAL && node[0] < node[1]);
294
}
295
296
template<> inline
297
45373
Node RewriteRule<ReflexivityEq>::apply(TNode node) {
298
45373
  Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
299
45373
  Node res = node[1].eqNode(node[0]);
300
45373
  return res;
301
}
302
303
}
304
}
305
}