GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/booleans/theory_bool_rewriter.cpp Lines: 220 229 96.1 %
Date: 2021-03-23 Branches: 863 1565 55.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bool_rewriter.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Dejan Jovanovic, Haniel Barbosa
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 <algorithm>
19
#include <unordered_set>
20
21
#include "expr/node_value.h"
22
#include "theory/booleans/theory_bool_rewriter.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace booleans {
27
28
11670938
RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) {
29
11670938
  return preRewrite(node);
30
}
31
32
/**
33
 * flattenNode looks for children of same kind, and if found merges
34
 * them into the parent.
35
 *
36
 * It simultaneously handles a couple of other optimizations:
37
 * - trivialNode - if found during exploration, return that node itself
38
 *    (like in case of OR, if "true" is found, makes sense to replace
39
 *     whole formula with "true")
40
 * - skipNode - as name suggests, skip them
41
 *    (like in case of OR, you may want to skip any "false" nodes found)
42
 *
43
 * Use a null node if you want to ignore any of the optimizations.
44
 */
45
849237
RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
46
{
47
  typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
48
49
1698474
  node_set visited;
50
849237
  visited.insert(skipNode);
51
52
1698474
  std::vector<TNode> toProcess;
53
849237
  toProcess.push_back(n);
54
55
849237
  Kind k = n.getKind();
56
  typedef std::vector<TNode> ChildList;
57
1698474
  ChildList childList;   //TNode should be fine, since 'n' is still there
58
59
2316163
  for (unsigned i = 0; i < toProcess.size(); ++ i) {
60
2948017
    TNode current = toProcess[i];
61
9707856
    for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) {
62
13826611
      TNode child = current[j];
63
8240930
      if(visited.find(child) != visited.end()) {
64
2641084
        continue;
65
5599846
      } else if(child == trivialNode) {
66
14165
        return RewriteResponse(REWRITE_DONE, trivialNode);
67
      } else {
68
5585681
        visited.insert(child);
69
5585681
        if(child.getKind() == k)
70
632484
          toProcess.push_back(child);
71
        else
72
4953197
          childList.push_back(child);
73
      }
74
    }
75
  }
76
835072
  if (childList.size() == 0) return RewriteResponse(REWRITE_DONE, skipNode);
77
711194
  if (childList.size() == 1) return RewriteResponse(REWRITE_AGAIN, childList[0]);
78
79
  /* Trickery to stay under number of children possible in a node */
80
566433
  NodeManager* nodeManager = NodeManager::currentNM();
81
566433
  if (childList.size() < expr::NodeValue::MAX_CHILDREN)
82
  {
83
1132866
    Node retNode = nodeManager->mkNode(k, childList);
84
566433
    return RewriteResponse(REWRITE_DONE, retNode);
85
  }
86
  else
87
  {
88
    Assert(childList.size()
89
           < static_cast<size_t>(expr::NodeValue::MAX_CHILDREN)
90
                 * static_cast<size_t>(expr::NodeValue::MAX_CHILDREN));
91
    NodeBuilder<> nb(k);
92
    ChildList::iterator cur = childList.begin(), next, en = childList.end();
93
    while (cur != en)
94
    {
95
      next = min(cur + expr::NodeValue::MAX_CHILDREN, en);
96
      nb << (nodeManager->mkNode(k, ChildList(cur, next)));
97
      cur = next;
98
    }
99
    return RewriteResponse(REWRITE_DONE, nb.constructNode());
100
  }
101
}
102
103
// Equality parity returns
104
// * 0 if no relation between a and b is found
105
// * 1 if a == b
106
// * 2 if a == not(b)
107
// * 3 or b == not(a)
108
4369515
inline int equalityParity(TNode a, TNode b){
109
4369515
  if(a == b){
110
10507
    return 1;
111
4359008
  }else if(a.getKind() == kind::NOT && a[0] == b){
112
120
    return 2;
113
4358888
  }else if(b.getKind() == kind::NOT && b[0] == a){
114
735
    return 3;
115
  }else{
116
4358153
    return 0;
117
  }
118
}
119
120
159485
inline Node makeNegation(TNode n){
121
159485
  bool even = false;
122
182107
  while(n.getKind() == kind::NOT){
123
11311
    n = n[0];
124
11311
    even = !even;
125
  }
126
159485
  if(even){
127
10863
    return n;
128
  } else {
129
148622
    if(n.isConst()){
130
18797
      return NodeManager::currentNM()->mkConst(!n.getConst<bool>());
131
    }else{
132
129825
      return n.notNode();
133
    }
134
  }
135
}
136
137
18390020
RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
138
18390020
  NodeManager* nodeManager = NodeManager::currentNM();
139
36780040
  Node tt = nodeManager->mkConst(true);
140
36780040
  Node ff = nodeManager->mkConst(false);
141
142
18390020
  switch(n.getKind()) {
143
3679858
  case kind::NOT: {
144
3679858
    if (n[0] == tt) return RewriteResponse(REWRITE_DONE, ff);
145
3603212
    if (n[0] == ff) return RewriteResponse(REWRITE_DONE, tt);
146
3502938
    if (n[0].getKind() == kind::NOT) return RewriteResponse(REWRITE_AGAIN, n[0][0]);
147
3366240
    break;
148
  }
149
4459786
  case kind::OR: {
150
4459786
    bool done = true;
151
4459786
    TNode::iterator i = n.begin(), iend = n.end();
152
32445604
    for(; i != iend; ++i) {
153
14106197
      if (*i == tt) return RewriteResponse(REWRITE_DONE, tt);
154
13992909
      if (*i == ff) done = false;
155
13992909
      if ((*i).getKind() == kind::OR) done = false;
156
    }
157
4346498
    if (!done) {
158
289441
      return flattenNode(n, /* trivialNode = */ tt, /* skipNode = */ ff);
159
    }
160
    // x v ... v x --> x
161
    unsigned ind, size;
162
4064681
    for (ind = 0, size = n.getNumChildren(); ind < size - 1; ++ind)
163
    {
164
4061157
      if (n[ind] != n[ind+1])
165
      {
166
4053533
        break;
167
      }
168
    }
169
4057057
    if (ind == size - 1)
170
    {
171
3524
      return RewriteResponse(REWRITE_AGAIN, n[0]);
172
    }
173
4053533
    break;
174
  }
175
4471682
  case kind::AND: {
176
4471682
    bool done = true;
177
4471682
    TNode::iterator i = n.begin(), iend = n.end();
178
56216676
    for(; i != iend; ++i) {
179
26208209
      if (*i == ff) return RewriteResponse(REWRITE_DONE, ff);
180
25872497
      if (*i == tt) done = false;
181
25872497
      if ((*i).getKind() == kind::AND) done = false;
182
    }
183
4135970
    if (!done) {
184
1119592
      RewriteResponse ret = flattenNode(n, /* trivialNode = */ ff, /* skipNode = */ tt);
185
559796
      Debug("bool-flatten") << n << ": " << ret.d_node << std::endl;
186
559796
      return ret;
187
    }
188
    // x ^ ... ^ x --> x
189
    unsigned ind, size;
190
3610056
    for (ind = 0, size = n.getNumChildren(); ind < size - 1; ++ind)
191
    {
192
3605399
      if (n[ind] != n[ind+1])
193
      {
194
3571517
        break;
195
      }
196
    }
197
3576174
    if (ind == size - 1)
198
    {
199
4657
      return RewriteResponse(REWRITE_AGAIN, n[0]);
200
    }
201
3571517
    break;
202
  }
203
478600
  case kind::IMPLIES: {
204
478600
    if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
205
476335
    if (n[0] == tt && n[1] == ff) return RewriteResponse(REWRITE_DONE, ff);
206
476224
    if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
207
467877
    if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
208
447776
    break;
209
  }
210
1633253
  case kind::EQUAL: {
211
    // rewrite simple cases of IFF
212
1633253
    if(n[0] == tt) {
213
      // IFF true x
214
29403
      return RewriteResponse(REWRITE_AGAIN, n[1]);
215
1603850
    } else if(n[1] == tt) {
216
      // IFF x true
217
30693
      return RewriteResponse(REWRITE_AGAIN, n[0]);
218
1573157
    } else if(n[0] == ff) {
219
      // IFF false x
220
49757
      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
221
1523400
    } else if(n[1] == ff) {
222
      // IFF x false
223
67188
      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
224
1456212
    } else if(n[0] == n[1]) {
225
      // IFF x x
226
24197
      return RewriteResponse(REWRITE_DONE, tt);
227
1432015
    } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
228
      // IFF (NOT x) x
229
805
      return RewriteResponse(REWRITE_DONE, ff);
230
1431210
    } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
231
      // IFF x (NOT x)
232
154
      return RewriteResponse(REWRITE_DONE, ff);
233
1431056
    } else if(n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) {
234
      // a : (= i x)
235
      // i : (= j k)
236
      // x : (= y z)
237
238
      // assume wlog k, z are constants and j is the same symbol as y
239
      // (iff (= j k) (= j z))
240
      // if k = z
241
      //  then (iff (= j k) (= j k)) => true
242
      // else
243
      //  (iff (= j k) (= j z)) <=> b
244
      //  b : (and (not (= j k)) (not (= j z)))
245
      //  (= j k) (= j z) | a b
246
      //  f       f       | t t
247
      //  f       t       | f f
248
      //  t       f       | f f
249
      //  t       t       | * f
250
      // * j cannot equal both k and z in a theory model
251
27475
      TNode t,c;
252
13745
      if (n[0][0].isConst()) {
253
1145
        c = n[0][0];
254
1145
        t = n[0][1];
255
      }
256
12600
      else if (n[0][1].isConst()) {
257
2279
        c = n[0][1];
258
2279
        t = n[0][0];
259
      }
260
13745
      bool matchesForm = false;
261
13745
      bool constantsEqual = false;
262
13745
      if (!c.isNull()) {
263
3424
        if (n[1][0] == t && n[1][1].isConst()) {
264
8
          matchesForm = true;
265
8
          constantsEqual = (n[1][1] == c);
266
        }
267
3416
        else if (n[1][1] == t && n[1][0].isConst()) {
268
7
          matchesForm = true;
269
7
          constantsEqual = (n[1][0] == c);
270
        }
271
      }
272
13745
      if(matchesForm){
273
15
        if(constantsEqual){
274
          return RewriteResponse(REWRITE_DONE, tt);
275
        }else{
276
30
          Cardinality kappa = t.getType().getCardinality();
277
30
          Cardinality two(2l);
278
15
          if(kappa.knownLessThanOrEqual(two)){
279
2
            return RewriteResponse(REWRITE_DONE, ff);
280
          }else{
281
26
            Node neitherEquality = (makeNegation(n[0])).andNode(makeNegation(n[1]));
282
13
            return RewriteResponse(REWRITE_AGAIN, neitherEquality);
283
          }
284
        }
285
      }
286
    }
287
1431041
    break;
288
  }
289
1077557
  case kind::XOR: {
290
    // rewrite simple cases of XOR
291
1077557
    if(n[0] == tt) {
292
      // XOR true x
293
4349
      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
294
1073208
    } else if(n[1] == tt) {
295
      // XOR x true
296
14504
      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
297
1058704
    } else if(n[0] == ff) {
298
      // XOR false x
299
33932
      return RewriteResponse(REWRITE_AGAIN, n[1]);
300
1024772
    } else if(n[1] == ff) {
301
      // XOR x false
302
99274
      return RewriteResponse(REWRITE_AGAIN, n[0]);
303
925498
    } else if(n[0] == n[1]) {
304
      // XOR x x
305
1231
      return RewriteResponse(REWRITE_DONE, ff);
306
924267
    } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
307
      // XOR (NOT x) x
308
36
      return RewriteResponse(REWRITE_DONE, tt);
309
924231
    } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
310
      // XOR x (NOT x)
311
155
      return RewriteResponse(REWRITE_DONE, tt);
312
    }
313
924076
    break;
314
  }
315
1753705
  case kind::ITE: {
316
    // non-Boolean-valued ITEs should have been removed in place of
317
    // a variable
318
    // rewrite simple cases of ITE
319
1753705
    if (n[0].isConst()) {
320
266815
      if (n[0] == tt) {
321
        // ITE true x y
322
43168
        Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[0] ==tt "
323
21584
                          << n << ": " << n[1] << std::endl;
324
21584
        return RewriteResponse(REWRITE_AGAIN, n[1]);
325
      } else {
326
245231
        Assert(n[0] == ff);
327
        // ITE false x y
328
490462
        Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[0] ==ff "
329
245231
                          << n << ": " << n[1] << std::endl;
330
245231
        return RewriteResponse(REWRITE_AGAIN, n[2]);
331
      }
332
1486890
    } else if (n[1].isConst()) {
333
377447
      if (n[1] == tt && n[2] == ff) {
334
8218
        Debug("bool-ite")
335
4109
            << "TheoryBoolRewriter::preRewrite_ITE: n[1] ==tt && n[2] == ff "
336
4109
            << n << ": " << n[0] << std::endl;
337
4109
        return RewriteResponse(REWRITE_AGAIN, n[0]);
338
      }
339
373338
      else if (n[1] == ff && n[2] == tt) {
340
7120
        Debug("bool-ite")
341
3560
            << "TheoryBoolRewriter::preRewrite_ITE: n[1] ==ff && n[2] == tt "
342
3560
            << n << ": " << n[0].notNode() << std::endl;
343
3560
        return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
344
      }
345
369778
      if (n[1] == tt || n[1] == ff)
346
      {
347
        // ITE C true y --> C v y
348
        // ITE C false y --> ~C ^ y
349
        Node resp =
350
155080
            n[1] == tt ? n[0].orNode(n[2]) : (n[0].negate()).andNode(n[2]);
351
155080
        Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[1] const "
352
77540
                          << n << ": " << resp << std::endl;
353
77540
        return RewriteResponse(REWRITE_AGAIN, resp);
354
      }
355
    }
356
357
1401681
    if (n[0].getKind() == kind::NOT)
358
    {
359
      // ite(not(c), x, y) ---> ite(c, y, x)
360
      return RewriteResponse(
361
70213
          REWRITE_AGAIN, nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1]));
362
    }
363
364
1331468
    if (n[2].isConst() && (n[2] == tt || n[2] == ff))
365
    {
366
      // ITE C x true --> ~C v x
367
      // ITE C x false --> C ^ x
368
      Node resp =
369
45342
          n[2] == tt ? (n[0].negate()).orNode(n[1]) : n[0].andNode(n[1]);
370
45342
      Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[2] const "
371
22671
                        << n << ": " << resp << std::endl;
372
22671
      return RewriteResponse(REWRITE_AGAIN, resp);
373
    }
374
375
    int parityTmp;
376
1308797
    if ((parityTmp = equalityParity(n[1], n[2])) != 0) {
377
13948
      Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]);
378
13948
      Debug("bool-ite")
379
6974
          << "TheoryBoolRewriter::preRewrite_ITE:  equalityParity n[1], n[2] "
380
6974
          << parityTmp << " " << n << ": " << resp << std::endl;
381
6974
      return RewriteResponse(REWRITE_AGAIN, resp);
382
    // Curiously, this rewrite affects several benchmarks dramatically, including copy_array and some simple_startup - disable for now
383
    // } else if (n[0].getKind() == kind::NOT) {
384
    //   return RewriteResponse(REWRITE_AGAIN, n[0][0].iteNode(n[2], n[1]));
385
1301823
    } else if(!n[1].isConst() && (parityTmp = equalityParity(n[0], n[1])) != 0){
386
      // (parityTmp == 1) if n[0] == n[1]
387
      // otherwise, n[0] == not(n[1]) or not(n[0]) == n[1]
388
389
      // if n[1] is constant this can loop, this is possible in prewrite
390
512
      Node resp = n[0].iteNode( (parityTmp == 1) ? tt : ff, n[2]);
391
512
      Debug("bool-ite")
392
256
          << "TheoryBoolRewriter::preRewrite_ITE: equalityParity n[0], n[1] "
393
256
          << parityTmp << " " << n << ": " << resp << std::endl;
394
256
      return RewriteResponse(REWRITE_AGAIN, resp);
395
1301567
    } else if(!n[2].isConst() && (parityTmp = equalityParity(n[0], n[2])) != 0){
396
      // (parityTmp == 1) if n[0] == n[2]
397
      // otherwise, n[0] == not(n[2]) or not(n[0]) == n[2]
398
644
      Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? ff : tt);
399
644
      Debug("bool-ite")
400
322
          << "TheoryBoolRewriter::preRewrite_ITE: equalityParity n[0], n[2] "
401
322
          << parityTmp << " " << n << ": " << resp << std::endl;
402
322
      return RewriteResponse(REWRITE_AGAIN, resp);
403
3717905
    } else if(n[1].getKind() == kind::ITE &&
404
2416660
              (parityTmp = equalityParity(n[0], n[1][0])) != 0){
405
      // (parityTmp == 1) then n : (ite c (ite c x y) z)
406
      // (parityTmp > 1)  then n : (ite c (ite (not c) x y) z) or
407
      // n: (ite (not c) (ite c x y) z)
408
4590
      Node resp = n[0].iteNode((parityTmp == 1) ? n[1][1] : n[1][2], n[2]);
409
4590
      Debug("bool-ite")
410
2295
          << "TheoryBoolRewriter::preRewrite: equalityParity n[0], n[1][0] "
411
2295
          << parityTmp << " " << n << ": " << resp << std::endl;
412
2295
      return RewriteResponse(REWRITE_AGAIN, resp);
413
4223054
    } else if(n[2].getKind() == kind::ITE &&
414
2924104
              (parityTmp = equalityParity(n[0], n[2][0])) != 0){
415
      // (parityTmp == 1) then n : (ite c x (ite c y z))
416
      // (parityTmp > 1)  then n : (ite c x (ite (not c) y z)) or
417
      // n: (ite (not c) x (ite c y z))
418
3030
      Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? n[2][2] : n[2][1]);
419
3030
      Debug("bool-ite")
420
1515
          << "TheoryBoolRewriter::preRewrite: equalityParity n[0], n[2][0] "
421
1515
          << parityTmp << " " << n << ": " << resp << std::endl;
422
1515
      return RewriteResponse(REWRITE_AGAIN, resp);
423
    }
424
1297435
    break;
425
  }
426
835579
  default:
427
835579
    return RewriteResponse(REWRITE_DONE, n);
428
  }
429
15091618
  return RewriteResponse(REWRITE_DONE, n);
430
}
431
432
}/* CVC4::theory::booleans namespace */
433
}/* CVC4::theory namespace */
434
26685
}/* CVC4 namespace */