GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/bv_to_bool.cpp Lines: 158 161 98.1 %
Date: 2021-03-22 Branches: 378 926 40.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_to_bool.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Yoni Zohar, Liana Hadarean, Aina Niemetz
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 Preprocessing pass that lifts bit-vectors of size 1 to booleans.
13
 **
14
 ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
15
 ** Implemented recursively.
16
 **/
17
18
#include "preprocessing/passes/bv_to_bool.h"
19
20
#include <string>
21
#include <unordered_map>
22
#include <vector>
23
24
#include "expr/node.h"
25
#include "expr/node_visitor.h"
26
#include "preprocessing/assertion_pipeline.h"
27
#include "preprocessing/preprocessing_pass_context.h"
28
#include "smt/smt_statistics_registry.h"
29
#include "theory/bv/theory_bv_utils.h"
30
#include "theory/rewriter.h"
31
#include "theory/theory.h"
32
33
namespace CVC4 {
34
namespace preprocessing {
35
namespace passes {
36
37
using namespace std;
38
using namespace CVC4::theory;
39
40
8995
BVToBool::BVToBool(PreprocessingPassContext* preprocContext)
41
    : PreprocessingPass(preprocContext, "bv-to-bool"),
42
      d_liftCache(),
43
      d_boolCache(),
44
      d_one(bv::utils::mkOne(1)),
45
      d_zero(bv::utils::mkZero(1)),
46
8995
      d_statistics(){};
47
48
155
PreprocessingPassResult BVToBool::applyInternal(
49
    AssertionPipeline* assertionsToPreprocess)
50
{
51
155
  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
52
310
  std::vector<Node> new_assertions;
53
155
  liftBvToBool(assertionsToPreprocess->ref(), new_assertions);
54
600
  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
55
  {
56
445
    assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i]));
57
  }
58
310
  return PreprocessingPassResult::NO_CONFLICT;
59
}
60
61
1242
void BVToBool::addToLiftCache(TNode term, Node new_term)
62
{
63
1242
  Assert(new_term != Node());
64
1242
  Assert(!hasLiftCache(term));
65
1242
  Assert(term.getType() == new_term.getType());
66
1242
  d_liftCache[term] = new_term;
67
1242
}
68
69
225
Node BVToBool::getLiftCache(TNode term) const
70
{
71
225
  Assert(hasLiftCache(term));
72
225
  return d_liftCache.find(term)->second;
73
}
74
75
4034
bool BVToBool::hasLiftCache(TNode term) const
76
{
77
4034
  return d_liftCache.find(term) != d_liftCache.end();
78
}
79
80
146
void BVToBool::addToBoolCache(TNode term, Node new_term)
81
{
82
146
  Assert(new_term != Node());
83
146
  Assert(!hasBoolCache(term));
84
146
  Assert(bv::utils::getSize(term) == 1);
85
146
  Assert(new_term.getType().isBoolean());
86
146
  d_boolCache[term] = new_term;
87
146
}
88
89
92
Node BVToBool::getBoolCache(TNode term) const
90
{
91
92
  Assert(hasBoolCache(term));
92
92
  return d_boolCache.find(term)->second;
93
}
94
95
612
bool BVToBool::hasBoolCache(TNode term) const
96
{
97
612
  return d_boolCache.find(term) != d_boolCache.end();
98
}
99
2342
bool BVToBool::isConvertibleBvAtom(TNode node)
100
{
101
2342
  Kind kind = node.getKind();
102
2709
  return (kind == kind::EQUAL && node[0].getType().isBitVector()
103
2667
          && node[0].getType().getBitVectorSize() == 1
104
2460
          && node[1].getType().isBitVector()
105
2460
          && node[1].getType().getBitVectorSize() == 1
106
2460
          && node[0].getKind() != kind::BITVECTOR_EXTRACT
107
4802
          && node[1].getKind() != kind::BITVECTOR_EXTRACT);
108
}
109
110
282
bool BVToBool::isConvertibleBvTerm(TNode node)
111
{
112
282
  if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1)
113
    return false;
114
115
282
  Kind kind = node.getKind();
116
117
282
  if (kind == kind::CONST_BITVECTOR || kind == kind::ITE
118
106
      || kind == kind::BITVECTOR_AND
119
80
      || kind == kind::BITVECTOR_OR
120
80
      || kind == kind::BITVECTOR_NOT
121
78
      || kind == kind::BITVECTOR_XOR
122
76
      || kind == kind::BITVECTOR_COMP)
123
  {
124
212
    return true;
125
  }
126
127
70
  return false;
128
}
129
130
116
Node BVToBool::convertBvAtom(TNode node)
131
{
132
116
  Assert(node.getType().isBoolean() && node.getKind() == kind::EQUAL);
133
116
  Assert(bv::utils::getSize(node[0]) == 1);
134
116
  Assert(bv::utils::getSize(node[1]) == 1);
135
232
  Node a = convertBvTerm(node[0]);
136
232
  Node b = convertBvTerm(node[1]);
137
116
  Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
138
232
  Debug("bv-to-bool") << "BVToBool::convertBvAtom " << node << " => " << result
139
116
                      << "\n";
140
141
116
  ++(d_statistics.d_numAtomsLifted);
142
232
  return result;
143
}
144
145
374
Node BVToBool::convertBvTerm(TNode node)
146
{
147
374
  Assert(node.getType().isBitVector()
148
         && node.getType().getBitVectorSize() == 1);
149
150
374
  if (hasBoolCache(node)) return getBoolCache(node);
151
152
282
  NodeManager* nm = NodeManager::currentNM();
153
154
282
  if (!isConvertibleBvTerm(node))
155
  {
156
70
    ++(d_statistics.d_numTermsForcedLifted);
157
140
    Node result = nm->mkNode(kind::EQUAL, node, d_one);
158
70
    addToBoolCache(node, result);
159
140
    Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
160
70
                        << result << "\n";
161
70
    return result;
162
  }
163
164
212
  if (node.getNumChildren() == 0)
165
  {
166
134
    Assert(node.getKind() == kind::CONST_BITVECTOR);
167
268
    Node result = node == d_one ? bv::utils::mkTrue() : bv::utils::mkFalse();
168
    // addToCache(node, result);
169
268
    Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
170
134
                        << result << "\n";
171
134
    return result;
172
  }
173
174
78
  ++(d_statistics.d_numTermsLifted);
175
176
78
  Kind kind = node.getKind();
177
78
  if (kind == kind::ITE)
178
  {
179
84
    Node cond = liftNode(node[0]);
180
84
    Node true_branch = convertBvTerm(node[1]);
181
84
    Node false_branch = convertBvTerm(node[2]);
182
84
    Node result = nm->mkNode(kind::ITE, cond, true_branch, false_branch);
183
42
    addToBoolCache(node, result);
184
84
    Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
185
42
                        << result << "\n";
186
42
    return result;
187
  }
188
189
  Kind new_kind;
190
  // special case for XOR as it has to be binary
191
  // while BITVECTOR_XOR can be n-ary
192
36
  if (kind == kind::BITVECTOR_XOR)
193
  {
194
2
    new_kind = kind::XOR;
195
4
    Node result = convertBvTerm(node[0]);
196
4
    for (unsigned i = 1; i < node.getNumChildren(); ++i)
197
    {
198
4
      Node converted = convertBvTerm(node[i]);
199
2
      result = nm->mkNode(kind::XOR, result, converted);
200
    }
201
4
    Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
202
2
                        << result << "\n";
203
2
    return result;
204
  }
205
206
34
  if (kind == kind::BITVECTOR_COMP)
207
  {
208
12
    Node result = nm->mkNode(kind::EQUAL, node[0], node[1]);
209
6
    addToBoolCache(node, result);
210
12
    Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
211
6
                        << result << "\n";
212
6
    return result;
213
  }
214
215
28
  switch (kind)
216
  {
217
    case kind::BITVECTOR_OR: new_kind = kind::OR; break;
218
26
    case kind::BITVECTOR_AND: new_kind = kind::AND; break;
219
2
    case kind::BITVECTOR_NOT: new_kind = kind::NOT; break;
220
    default: Unhandled();
221
  }
222
223
56
  NodeBuilder<> builder(new_kind);
224
82
  for (unsigned i = 0; i < node.getNumChildren(); ++i)
225
  {
226
54
    builder << convertBvTerm(node[i]);
227
  }
228
229
56
  Node result = builder;
230
28
  addToBoolCache(node, result);
231
56
  Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => " << result
232
28
                      << "\n";
233
28
  return result;
234
}
235
236
2567
Node BVToBool::liftNode(TNode current)
237
{
238
2567
  Node result;
239
240
2567
  if (hasLiftCache(current))
241
  {
242
225
    result = getLiftCache(current);
243
  }
244
2342
  else if (isConvertibleBvAtom(current))
245
  {
246
116
    result = convertBvAtom(current);
247
116
    addToLiftCache(current, result);
248
  }
249
  else
250
  {
251
2226
    if (current.getNumChildren() == 0)
252
    {
253
1100
      result = current;
254
    }
255
    else
256
    {
257
2252
      NodeBuilder<> builder(current.getKind());
258
1126
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
259
      {
260
192
        builder << current.getOperator();
261
      }
262
3206
      for (unsigned i = 0; i < current.getNumChildren(); ++i)
263
      {
264
        // Recursively lift children
265
4160
        Node converted = liftNode(current[i]);
266
2080
        Assert(converted.getType() == current[i].getType());
267
2080
        builder << converted;
268
      }
269
1126
      result = builder;
270
1126
      addToLiftCache(current, result);
271
    }
272
  }
273
2567
  Assert(result != Node());
274
2567
  Assert(result.getType() == current.getType());
275
5134
  Debug("bv-to-bool") << "BVToBool::liftNode " << current << " => \n"
276
2567
                      << result << "\n";
277
2567
  return result;
278
}
279
280
155
void BVToBool::liftBvToBool(const std::vector<Node>& assertions,
281
                            std::vector<Node>& new_assertions)
282
{
283
600
  for (unsigned i = 0; i < assertions.size(); ++i)
284
  {
285
890
    Node new_assertion = liftNode(assertions[i]);
286
445
    new_assertions.push_back(Rewriter::rewrite(new_assertion));
287
890
    Trace("bv-to-bool") << "  " << assertions[i] << " => " << new_assertions[i]
288
445
                        << "\n";
289
  }
290
155
}
291
292
8995
BVToBool::Statistics::Statistics()
293
    : d_numTermsLifted("preprocessing::passes::BVToBool::NumTermsLifted", 0),
294
      d_numAtomsLifted("preprocessing::passes::BVToBool::NumAtomsLifted", 0),
295
      d_numTermsForcedLifted(
296
8995
          "preprocessing::passes::BVToBool::NumTermsForcedLifted", 0)
297
{
298
8995
  smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
299
8995
  smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
300
8995
  smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted);
301
8995
}
302
303
17984
BVToBool::Statistics::~Statistics()
304
{
305
8992
  smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted);
306
8992
  smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted);
307
8992
  smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
308
8992
}
309
310
311
}  // passes
312
}  // Preprocessing
313
26676
}  // CVC4