GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt_util/boolean_simplification.h Lines: 54 68 79.4 %
Date: 2021-03-22 Branches: 74 188 39.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file boolean_simplification.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, 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 Simple routines for Boolean simplification
13
 **
14
 ** Simple, commonly-used routines for Boolean simplification.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__BOOLEAN_SIMPLIFICATION_H
20
#define CVC4__BOOLEAN_SIMPLIFICATION_H
21
22
#include <vector>
23
#include <algorithm>
24
25
#include "base/check.h"
26
#include "expr/node.h"
27
28
namespace CVC4 {
29
30
/**
31
 * A class to contain a number of useful functions for simple
32
 * simplification of nodes.  One never uses it as an object (and
33
 * it cannot be constructed).  It is used as a namespace.
34
 */
35
class BooleanSimplification {
36
  // cannot construct one of these
37
  BooleanSimplification() = delete;
38
  BooleanSimplification(const BooleanSimplification&) = delete;
39
40
  static bool push_back_associative_commute_recursive(
41
      Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
42
      CVC4_WARN_UNUSED_RESULT;
43
44
 public:
45
  /**
46
   * The threshold for removing duplicates.  (See removeDuplicates().)
47
   */
48
  static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10;
49
50
  /**
51
   * Remove duplicate nodes from a vector, modifying it in-place.
52
   * If the vector has size >= DUPLICATE_REMOVAL_THRESHOLD, this
53
   * function is a no-op.
54
   */
55
24
  static void removeDuplicates(std::vector<Node>& buffer)
56
  {
57
24
    if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) {
58
24
      std::sort(buffer.begin(), buffer.end());
59
      std::vector<Node>::iterator new_end =
60
24
        std::unique(buffer.begin(), buffer.end());
61
24
      buffer.erase(new_end, buffer.end());
62
    }
63
24
  }
64
65
  /**
66
   * Takes a node with kind AND, collapses all AND and (NOT OR)-kinded
67
   * children of it (as far as possible---see
68
   * push_back_associative_commute()), removes duplicates, and returns
69
   * the resulting Node.
70
   */
71
8
  static Node simplifyConflict(Node andNode)
72
  {
73
8
    AssertArgument(!andNode.isNull(), andNode);
74
8
    AssertArgument(andNode.getKind() == kind::AND, andNode);
75
76
12
    std::vector<Node> buffer;
77
6
    push_back_associative_commute(andNode, buffer, kind::AND, kind::OR);
78
79
6
    removeDuplicates(buffer);
80
81
6
    if(buffer.size() == 1) {
82
      return buffer[0];
83
    }
84
85
12
    NodeBuilder<> nb(kind::AND);
86
6
    nb.append(buffer);
87
6
    return nb;
88
  }
89
90
  /**
91
   * Takes a node with kind OR, collapses all OR and (NOT AND)-kinded
92
   * children of it (as far as possible---see
93
   * push_back_associative_commute()), removes duplicates, and returns
94
   * the resulting Node.
95
   */
96
20
  static Node simplifyClause(Node orNode)
97
  {
98
20
    AssertArgument(!orNode.isNull(), orNode);
99
20
    AssertArgument(orNode.getKind() == kind::OR, orNode);
100
101
36
    std::vector<Node> buffer;
102
18
    push_back_associative_commute(orNode, buffer, kind::OR, kind::AND);
103
104
18
    removeDuplicates(buffer);
105
106
18
    Assert(buffer.size() > 0);
107
18
    if(buffer.size() == 1) {
108
      return buffer[0];
109
    }
110
111
36
    NodeBuilder<> nb(kind::OR);
112
18
    nb.append(buffer);
113
18
    return nb;
114
  }
115
116
  /**
117
   * Takes a node with kind IMPLIES, converts it to an OR, then
118
   * simplifies the result with simplifyClause().
119
   *
120
   * The input doesn't actually have to be Horn, it seems, but that's
121
   * the common case(?), hence the name.
122
   */
123
10
  static Node simplifyHornClause(Node implication)
124
  {
125
10
    AssertArgument(implication.getKind() == kind::IMPLIES, implication);
126
127
16
    TNode left = implication[0];
128
16
    TNode right = implication[1];
129
130
16
    Node notLeft = negate(left);
131
16
    Node clause = NodeBuilder<2>(kind::OR) << notLeft << right;
132
133
16
    return simplifyClause(clause);
134
  }
135
136
  /**
137
   * Aids in reforming a node.  Takes a node of (N-ary) kind k and
138
   * copies its children into an output vector, collapsing its k-kinded
139
   * children into it.  Also collapses negations of notK.  For example:
140
   *
141
   *   push_back_associative_commute( [OR [OR a b] [OR b c d] [NOT [AND e f]]],
142
   *                                  buffer, kind::OR, kind::AND )
143
   *   yields a "buffer" vector of [a b b c d e f]
144
   *
145
   * @param n the node to operate upon
146
   * @param buffer the output vector (must be empty on entry)
147
   * @param k the kind to collapse (should equal the kind of node n)
148
   * @param notK the "negation" of kind k (e.g. OR's negation is AND),
149
   * or kind::UNDEFINED_KIND if none.
150
   * @param negateChildren true if the children of the resulting node
151
   * (that is, the elements in buffer) should all be negated; you want
152
   * this if e.g. you're simplifying the (OR...) in (NOT (OR...)),
153
   * intending to make the result an AND.
154
   */
155
24
  static inline void push_back_associative_commute(Node n,
156
                                                   std::vector<Node>& buffer,
157
                                                   Kind k,
158
                                                   Kind notK,
159
                                                   bool negateChildren = false)
160
  {
161
24
    AssertArgument(buffer.empty(), buffer);
162
24
    AssertArgument(!n.isNull(), n);
163
24
    AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k);
164
24
    AssertArgument(notK != kind::NULL_EXPR, notK);
165
24
    AssertArgument(n.getKind() == k, n,
166
                   "expected node to have kind %s", kindToString(k).c_str());
167
168
    bool b CVC4_UNUSED =
169
24
      push_back_associative_commute_recursive(n, buffer, k, notK, false);
170
171
24
    if(buffer.size() == 0) {
172
      // all the TRUEs for an AND (resp FALSEs for an OR) were simplified away
173
      buffer.push_back(NodeManager::currentNM()->mkConst(k == kind::AND ? true : false));
174
    }
175
24
  }/* push_back_associative_commute() */
176
177
  /**
178
   * Negates a node, doing all the double-negation elimination
179
   * that's possible.
180
   *
181
   * @param n the node to negate (cannot be the null node)
182
   */
183
36
  static Node negate(TNode n)
184
  {
185
36
    AssertArgument(!n.isNull(), n);
186
187
34
    bool polarity = true;
188
68
    TNode base = n;
189
58
    while(base.getKind() == kind::NOT){
190
12
      base = base[0];
191
12
      polarity = !polarity;
192
    }
193
34
    if(n.isConst()) {
194
      return NodeManager::currentNM()->mkConst(!n.getConst<bool>());
195
    }
196
34
    if(polarity){
197
30
      return base.notNode();
198
    }else{
199
4
      return base;
200
    }
201
  }
202
203
  /**
204
   * Simplify an OR, AND, or IMPLIES.  This function is the identity
205
   * for all other kinds.
206
   */
207
  inline static Node simplify(TNode n)
208
  {
209
    switch(n.getKind()) {
210
    case kind::AND:
211
      return simplifyConflict(n);
212
213
    case kind::OR:
214
      return simplifyClause(n);
215
216
    case kind::IMPLIES:
217
      return simplifyHornClause(n);
218
219
    default:
220
      return n;
221
    }
222
  }
223
224
};/* class BooleanSimplification */
225
226
}/* CVC4 namespace */
227
228
#endif /* CVC4__BOOLEAN_SIMPLIFICATION_H */