GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/bool_to_bv.cpp Lines: 179 185 96.8 %
Date: 2021-03-23 Branches: 420 807 52.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bool_to_bv.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Makai Mann, Yoni Zohar, 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 The BoolToBV preprocessing pass
13
 **
14
 **/
15
16
#include "preprocessing/passes/bool_to_bv.h"
17
18
#include <string>
19
20
#include "base/map_util.h"
21
#include "expr/node.h"
22
#include "preprocessing/assertion_pipeline.h"
23
#include "preprocessing/preprocessing_pass_context.h"
24
#include "smt/smt_statistics_registry.h"
25
#include "theory/bv/theory_bv_utils.h"
26
#include "theory/rewriter.h"
27
#include "theory/theory.h"
28
29
namespace CVC4 {
30
namespace preprocessing {
31
namespace passes {
32
using namespace CVC4::theory;
33
34
8997
BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
35
8997
    : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics()
36
{
37
62616
  d_boolToBVMode = options::boolToBitvector();
38
8997
};
39
40
12
PreprocessingPassResult BoolToBV::applyInternal(
41
    AssertionPipeline* assertionsToPreprocess)
42
{
43
12
  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
44
45
12
  size_t size = assertionsToPreprocess->size();
46
47
12
  if (d_boolToBVMode == options::BoolToBVMode::ALL)
48
  {
49
74
    for (size_t i = 0; i < size; ++i)
50
    {
51
132
      Node newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true);
52
66
      assertionsToPreprocess->replace(i, Rewriter::rewrite(newAssertion));
53
    }
54
  }
55
  else
56
  {
57
4
    Assert(d_boolToBVMode == options::BoolToBVMode::ITE);
58
24
    for (size_t i = 0; i < size; ++i)
59
    {
60
20
      assertionsToPreprocess->replace(
61
40
          i, Rewriter::rewrite(lowerIte((*assertionsToPreprocess)[i])));
62
    }
63
  }
64
65
12
  return PreprocessingPassResult::NO_CONFLICT;
66
}
67
68
158
void BoolToBV::updateCache(TNode n, TNode rebuilt)
69
{
70
  // check more likely case first
71
158
  if ((n.getKind() != kind::ITE) || !n[1].getType().isBitVector())
72
  {
73
154
    d_lowerCache[n] = rebuilt;
74
  }
75
  else
76
  {
77
4
    d_iteBVLowerCache[n] = rebuilt;
78
  }
79
158
}
80
81
1342
Node BoolToBV::fromCache(TNode n) const
82
{
83
  // check more likely case first
84
1342
  if (n.getKind() != kind::ITE)
85
  {
86
1326
    if (d_lowerCache.find(n) != d_lowerCache.end())
87
    {
88
734
      return d_lowerCache.at(n);
89
    }
90
  }
91
  else
92
  {
93
16
    if (d_iteBVLowerCache.find(n) != d_iteBVLowerCache.end())
94
    {
95
8
      return d_iteBVLowerCache.at(n);
96
    }
97
  }
98
600
  return n;
99
}
100
101
216
inline bool BoolToBV::inCache(const Node& n) const
102
{
103
216
  return (ContainsKey(d_lowerCache, n) || ContainsKey(d_iteBVLowerCache, n));
104
}
105
106
536
bool BoolToBV::needToRebuild(TNode n) const
107
{
108
  // check if any children were rebuilt
109
748
  for (const Node& nn : n)
110
  {
111
216
    if (inCache(nn))
112
    {
113
4
      return true;
114
    }
115
  }
116
532
  return false;
117
}
118
119
66
Node BoolToBV::lowerAssertion(const TNode& assertion, bool allowIteIntroduction)
120
{
121
  // first try to lower all the children
122
168
  for (const Node& c : assertion)
123
  {
124
102
    lowerNode(c, allowIteIntroduction);
125
  }
126
127
  // now try lowering the assertion, but don't force it with an ITE (even in mode all)
128
66
  lowerNode(assertion, false);
129
66
  Node newAssertion = fromCache(assertion);
130
132
  TypeNode newAssertionType = newAssertion.getType();
131
66
  if (newAssertionType.isBitVector())
132
  {
133
62
    Assert(newAssertionType.getBitVectorSize() == 1);
134
124
    newAssertion = NodeManager::currentNM()->mkNode(
135
124
        kind::EQUAL, newAssertion, bv::utils::mkOne(1));
136
62
    newAssertionType = newAssertion.getType();
137
  }
138
66
  Assert(newAssertionType.isBoolean());
139
132
  return newAssertion;
140
}
141
142
172
Node BoolToBV::lowerNode(const TNode& node, bool allowIteIntroduction)
143
{
144
344
  std::vector<TNode> to_visit;
145
172
  to_visit.push_back(node);
146
344
  std::unordered_set<TNode, TNodeHashFunction> visited;
147
148
2540
  while (!to_visit.empty())
149
  {
150
2368
    TNode n = to_visit.back();
151
1184
    to_visit.pop_back();
152
153
2368
    Debug("bool-to-bv") << "BoolToBV::lowerNode: Post-order traversal with "
154
2368
                        << n << " and visited = " << ContainsKey(visited, n)
155
1184
                        << std::endl;
156
157
    // Mark as visited
158
1184
    if (ContainsKey(visited, n))
159
    {
160
614
      visit(n, allowIteIntroduction);
161
    }
162
    else
163
    {
164
570
      visited.insert(n);
165
570
      to_visit.push_back(n);
166
167
      // insert children in reverse order so that they're processed in order
168
      //    important for rewriting which sorts by node id
169
      // NOTE: size_t is unsigned, so using underflow for termination condition
170
570
      size_t numChildren = n.getNumChildren();
171
1012
      for (size_t i = numChildren - 1; i < numChildren; --i)
172
      {
173
442
        to_visit.push_back(n[i]);
174
      }
175
    }
176
  }
177
178
344
  return fromCache(node);
179
}
180
181
614
void BoolToBV::visit(const TNode& n, bool allowIteIntroduction)
182
{
183
614
  Kind k = n.getKind();
184
185
  // easy case -- just replace boolean constant
186
614
  if (k == kind::CONST_BOOLEAN)
187
  {
188
10
    updateCache(n,
189
20
                (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1)
190
                                           : bv::utils::mkZero(1));
191
132
    return;
192
  }
193
194
604
  NodeManager* nm = NodeManager::currentNM();
195
604
  Kind new_kind = k;
196
604
  switch (k)
197
  {
198
38
    case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break;
199
10
    case kind::AND: new_kind = kind::BITVECTOR_AND; break;
200
4
    case kind::OR: new_kind = kind::BITVECTOR_OR; break;
201
26
    case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;
202
6
    case kind::XOR: new_kind = kind::BITVECTOR_XOR; break;
203
20
    case kind::IMPLIES: new_kind = kind::BITVECTOR_OR; break;
204
12
    case kind::ITE: new_kind = kind::BITVECTOR_ITE; break;
205
16
    case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break;
206
4
    case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break;
207
    case kind::BITVECTOR_ULE:
208
    case kind::BITVECTOR_UGT:
209
    case kind::BITVECTOR_UGE:
210
    case kind::BITVECTOR_SLE:
211
    case kind::BITVECTOR_SGT:
212
    case kind::BITVECTOR_SGE:
213
      // Should have been removed by rewriting.
214
      Unreachable();
215
468
    default: break;
216
  }
217
218
  // check if it's safe to lower or rebuild the node
219
  // Note: might have to rebuild to keep changes to children, even if this node
220
  // isn't being lowered
221
222
  // it's safe to lower if all the children are bit-vectors
223
604
  bool safe_to_lower =
224
604
      (new_kind != k);  // don't need to lower at all if kind hasn't changed
225
226
  // it's safe to rebuild if rebuilding doesn't change any of the types of the
227
  // children
228
604
  bool safe_to_rebuild = true;
229
230
998
  for (const Node& nn : n)
231
  {
232
434
    safe_to_lower = safe_to_lower && fromCache(nn).getType().isBitVector();
233
434
    safe_to_rebuild = safe_to_rebuild && (fromCache(nn).getType() == nn.getType());
234
235
    // if it's already not safe to do either, stop checking
236
434
    if (!safe_to_lower && !safe_to_rebuild)
237
    {
238
40
      break;
239
    }
240
  }
241
242
1208
  Debug("bool-to-bv") << "safe_to_lower = " << safe_to_lower
243
604
                      << ", safe_to_rebuild = " << safe_to_rebuild << std::endl;
244
245
604
  if (new_kind != k && safe_to_lower)
246
  {
247
    // lower to BV
248
104
    rebuildNode(n, new_kind);
249
104
    return;
250
  }
251
500
  else if (new_kind != k && allowIteIntroduction && fromCache(n).getType().isBoolean())
252
  {
253
    // lower to BV using an ITE
254
255
8
    if (safe_to_rebuild && needToRebuild(n))
256
    {
257
      // need to rebuild to keep changes made to descendants
258
      rebuildNode(n, k);
259
    }
260
261
8
    updateCache(n,
262
48
                nm->mkNode(kind::ITE,
263
16
                           fromCache(n),
264
16
                           bv::utils::mkOne(1),
265
16
                           bv::utils::mkZero(1)));
266
16
    Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
267
8
                        << " =>\n"
268
8
                        << fromCache(n) << std::endl;
269
8
    ++(d_statistics.d_numIntroducedItes);
270
8
    return;
271
  }
272
492
  else if (safe_to_rebuild && needToRebuild(n))
273
  {
274
    // rebuild to incorporate changes to children
275
    Assert(k == new_kind);
276
    rebuildNode(n, k);
277
  }
278
492
  else if (allowIteIntroduction && fromCache(n).getType().isBoolean())
279
  {
280
    // force booleans (which haven't already been converted) to bit-vector
281
    // needed to maintain the invariant that all boolean children
282
    // have been converted (even constants and variables) when forcing
283
    // with ITE introductions
284
32
    updateCache(
285
64
        n, nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1)));
286
64
    Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
287
32
                        << " =>\n"
288
32
                        << fromCache(n) << std::endl;
289
32
    ++(d_statistics.d_numIntroducedItes);
290
  }
291
  else
292
  {
293
    // do nothing
294
920
    Debug("bool-to-bv") << "BoolToBV::visit skipping: " << n
295
460
                        << std::endl;
296
  }
297
}
298
299
20
Node BoolToBV::lowerIte(const TNode& node)
300
{
301
40
  std::vector<TNode> visit;
302
20
  visit.push_back(node);
303
40
  std::unordered_set<TNode, TNodeHashFunction> visited;
304
305
316
  while (!visit.empty())
306
  {
307
296
    TNode n = visit.back();
308
148
    visit.pop_back();
309
310
296
    Debug("bool-to-bv") << "BoolToBV::lowerIte: Post-order traversal with " << n
311
296
                        << " and visited = " << ContainsKey(visited, n)
312
148
                        << std::endl;
313
314
    // Look for ITEs and mark visited
315
148
    if (!ContainsKey(visited, n))
316
    {
317
72
      if ((n.getKind() == kind::ITE) && n[1].getType().isBitVector())
318
      {
319
8
        Debug("bool-to-bv") << "BoolToBV::lowerIte: adding " << n[0]
320
4
                            << " to set of ite conditions" << std::endl;
321
        // don't force in this case -- forcing only introduces more ITEs
322
8
        Node loweredNode = lowerNode(n, false);
323
        // some of the lowered nodes might appear elsewhere but not in an ITE
324
        // reset the cache to prevent lowering them
325
        // the bit-vector ITEs are still tracked in d_iteBVLowerCache though
326
4
        d_lowerCache.clear();
327
      }
328
      else
329
      {
330
68
        visit.push_back(n);
331
68
        visited.insert(n);
332
        // insert in reverse order so that they're processed in order
333
128
        for (int i = n.getNumChildren() - 1; i >= 0; --i)
334
        {
335
60
          visit.push_back(n[i]);
336
        }
337
      }
338
    }
339
76
    else if (needToRebuild(n))
340
    {
341
      // Note: it's always safe to rebuild here, because we've only lowered
342
      //       ITEs of type bit-vector to BITVECTOR_ITE
343
4
      rebuildNode(n, n.getKind());
344
    }
345
    else
346
    {
347
144
      Debug("bool-to-bv")
348
72
          << "BoolToBV::lowerIte Skipping because don't need to rebuild: " << n
349
72
          << std::endl;
350
    }
351
  }
352
40
  return fromCache(node);
353
}
354
355
108
void BoolToBV::rebuildNode(const TNode& n, Kind new_kind)
356
{
357
108
  Kind k = n.getKind();
358
108
  NodeManager* nm = NodeManager::currentNM();
359
216
  NodeBuilder<> builder(new_kind);
360
361
216
  Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n
362
216
                      << " and new_kind = " << kindToString(new_kind)
363
108
                      << std::endl;
364
365
108
  if ((d_boolToBVMode == options::BoolToBVMode::ALL) && (new_kind != k))
366
  {
367
96
    ++(d_statistics.d_numTermsLowered);
368
  }
369
370
108
  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
371
  {
372
    builder << n.getOperator();
373
  }
374
375
  // special case IMPLIES because needs to be rewritten
376
108
  if ((k == kind::IMPLIES) && (new_kind != k))
377
  {
378
20
    builder << nm->mkNode(kind::BITVECTOR_NOT, fromCache(n[0]));
379
20
    builder << fromCache(n[1]);
380
  }
381
  else
382
  {
383
250
    for (const Node& nn : n)
384
    {
385
162
      builder << fromCache(nn);
386
    }
387
  }
388
389
216
  Debug("bool-to-bv") << "BoolToBV::rebuildNode " << n << " =>\n"
390
108
                      << builder << std::endl;
391
392
108
  updateCache(n, builder.constructNode());
393
108
}
394
395
8997
BoolToBV::Statistics::Statistics()
396
    : d_numIteToBvite("preprocessing::passes::BoolToBV::NumIteToBvite", 0),
397
      d_numTermsLowered("preprocessing::passes:BoolToBV::NumTermsLowered", 0),
398
      d_numIntroducedItes(
399
8997
          "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0)
400
{
401
8997
  smtStatisticsRegistry()->registerStat(&d_numIteToBvite);
402
8997
  if (options::boolToBitvector() == options::BoolToBVMode::ALL)
403
  {
404
    // these statistics wouldn't be correct in the ITE mode,
405
    // because it might discard rebuilt nodes if it fails to
406
    // convert a bool to width-one bit-vector (never forces)
407
8
    smtStatisticsRegistry()->registerStat(&d_numTermsLowered);
408
8
    smtStatisticsRegistry()->registerStat(&d_numIntroducedItes);
409
  }
410
8997
}
411
412
17988
BoolToBV::Statistics::~Statistics()
413
{
414
8994
  smtStatisticsRegistry()->unregisterStat(&d_numIteToBvite);
415
8994
  if (options::boolToBitvector() == options::BoolToBVMode::ALL)
416
  {
417
8
    smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
418
8
    smtStatisticsRegistry()->unregisterStat(&d_numIntroducedItes);
419
  }
420
8994
}
421
422
423
}  // namespace passes
424
}  // namespace preprocessing
425
80304
}  // namespace CVC4