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