1 /********************* */
2 /*! \file circuit_propagator.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 A non-clausal circuit propagator for Boolean simplification
13 **
14 ** A non-clausal circuit propagator for Boolean simplification.
15 **/
16
17 #include "theory/booleans/circuit_propagator.h"
18
19 #include <stack>
20 #include <vector>
21 #include <algorithm>
22
23 #include "expr/node_algorithm.h"
24 #include "util/utility.h"
25
26 using namespace std;
27
28 namespace CVC4 {
29 namespace theory {
30 namespace booleans {
31
assertTrue(TNode assertion)32 void CircuitPropagator::assertTrue(TNode assertion)
33 {
34 if (assertion.getKind() == kind::AND) {
35 for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) {
36 assertTrue(assertion[i]);
37 }
38 } else {
39 // Analyze the assertion for back-edges and all that
40 computeBackEdges(assertion);
41 // Assign the given assertion to true
42 assignAndEnqueue(assertion, true);
43 }
44 }
45
computeBackEdges(TNode node)46 void CircuitPropagator::computeBackEdges(TNode node) {
47
48 Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")" << endl;
49
50 // Vector of nodes to visit
51 vector<TNode> toVisit;
52
53 // Start with the top node
54 if (d_seen.find(node) == d_seen.end()) {
55 toVisit.push_back(node);
56 d_seen.insert(node);
57 }
58
59 // Initialize the back-edges for the root, so we don't have a special case
60 d_backEdges[node];
61
62 // Go through the visit list
63 for (unsigned i = 0; i < toVisit.size(); ++ i) {
64 // Node we need to visit
65 TNode current = toVisit[i];
66 Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(): processing " << current << endl;
67 Assert(d_seen.find(current) != d_seen.end());
68
69 // If this not an atom visit all the children and compute the back edges
70 if (Theory::theoryOf(current) == THEORY_BOOL) {
71 for (unsigned child = 0, child_end = current.getNumChildren(); child < child_end; ++ child) {
72 TNode childNode = current[child];
73 // Add the back edge
74 d_backEdges[childNode].push_back(current);
75 // Add to the queue if not seen yet
76 if (d_seen.find(childNode) == d_seen.end()) {
77 toVisit.push_back(childNode);
78 d_seen.insert(childNode);
79 }
80 }
81 }
82 }
83 }
84
propagateBackward(TNode parent,bool parentAssignment)85 void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) {
86
87 Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent << ", " << parentAssignment << ")" << endl;
88
89 // backward rules
90 switch(parent.getKind()) {
91 case kind::AND:
92 if (parentAssignment) {
93 // AND = TRUE: forall children c, assign(c = TRUE)
94 for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) {
95 assignAndEnqueue(*i, true);
96 }
97 } else {
98 // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE)
99 TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, true)));
100 if (holdout != parent.end()) {
101 assignAndEnqueue(*holdout, false);
102 }
103 }
104 break;
105 case kind::OR:
106 if (parentAssignment) {
107 // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
108 TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, false)));
109 if (holdout != parent.end()) {
110 assignAndEnqueue(*holdout, true);
111 }
112 } else {
113 // OR = FALSE: forall children c, assign(c = FALSE)
114 for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) {
115 assignAndEnqueue(*i, false);
116 }
117 }
118 break;
119 case kind::NOT:
120 // NOT = b: assign(c = !b)
121 assignAndEnqueue(parent[0], !parentAssignment);
122 break;
123 case kind::ITE:
124 if (isAssignedTo(parent[0], true)) {
125 // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
126 assignAndEnqueue(parent[1], parentAssignment);
127 } else if (isAssignedTo(parent[0], false)) {
128 // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
129 assignAndEnqueue(parent[2], parentAssignment);
130 } else if (isAssigned(parent[1]) && isAssigned(parent[2])) {
131 if (getAssignment(parent[1]) == parentAssignment && getAssignment(parent[2]) != parentAssignment) {
132 // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE)
133 assignAndEnqueue(parent[0], true);
134 } else if (getAssignment(parent[1]) != parentAssignment && getAssignment(parent[2]) == parentAssignment) {
135 // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE)
136 assignAndEnqueue(parent[0], false);
137 }
138 }
139 break;
140 case kind::EQUAL:
141 Assert( parent[0].getType().isBoolean() );
142 if (parentAssignment) {
143 // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment])
144 if (isAssigned(parent[0])) {
145 assignAndEnqueue(parent[1], getAssignment(parent[0]));
146 } else if (isAssigned(parent[1])) {
147 assignAndEnqueue(parent[0], getAssignment(parent[1]));
148 }
149 } else {
150 // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment])
151 if (isAssigned(parent[0])) {
152 assignAndEnqueue(parent[1], !getAssignment(parent[0]));
153 } else if (isAssigned(parent[1])) {
154 assignAndEnqueue(parent[0], !getAssignment(parent[1]));
155 }
156 }
157 break;
158 case kind::IMPLIES:
159 if (parentAssignment) {
160 if (isAssignedTo(parent[0], true)) {
161 // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE)
162 assignAndEnqueue(parent[1], true);
163 }
164 if (isAssignedTo(parent[1], false)) {
165 // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE)
166 assignAndEnqueue(parent[0], false);
167 }
168 } else {
169 // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE)
170 assignAndEnqueue(parent[0], true);
171 assignAndEnqueue(parent[1], false);
172 }
173 break;
174 case kind::XOR:
175 if (parentAssignment) {
176 if (isAssigned(parent[0])) {
177 // XOR x y = TRUE, and x assigned, assign(y = !assignment(x))
178 assignAndEnqueue(parent[1], !getAssignment(parent[0]));
179 } else if (isAssigned(parent[1])) {
180 // XOR x y = TRUE, and y assigned, assign(x = !assignment(y))
181 assignAndEnqueue(parent[0], !getAssignment(parent[1]));
182 }
183 } else {
184 if (isAssigned(parent[0])) {
185 // XOR x y = FALSE, and x assigned, assign(y = assignment(x))
186 assignAndEnqueue(parent[1], getAssignment(parent[0]));
187 } else if (isAssigned(parent[1])) {
188 // XOR x y = FALSE, and y assigned, assign(x = assignment(y))
189 assignAndEnqueue(parent[0], getAssignment(parent[1]));
190 }
191 }
192 break;
193 default:
194 Unhandled();
195 }
196 }
197
198
propagateForward(TNode child,bool childAssignment)199 void CircuitPropagator::propagateForward(TNode child, bool childAssignment) {
200
201 // The assignment we have
202 Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child << ", " << childAssignment << ")" << endl;
203
204 // Get the back any nodes where this is child
205 const vector<Node>& parents = d_backEdges.find(child)->second;
206
207 // Go through the parents and see if there is anything to propagate
208 vector<Node>::const_iterator parent_it = parents.begin();
209 vector<Node>::const_iterator parent_it_end = parents.end();
210 for(; parent_it != parent_it_end && !d_conflict; ++ parent_it) {
211 // The current parent of the child
212 TNode parent = *parent_it;
213 Assert(expr::hasSubterm(parent, child));
214
215 // Forward rules
216 switch(parent.getKind()) {
217 case kind::AND:
218 if (childAssignment) {
219 TNode::iterator holdout;
220 holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, true)));
221 if (holdout == parent.end()) { // all children are assigned TRUE
222 // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE)
223 assignAndEnqueue(parent, true);
224 } else if (isAssignedTo(parent, false)) {// the AND is FALSE
225 // is the holdout unique ?
226 TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, true)));
227 if (other == parent.end()) { // the holdout is unique
228 // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE)
229 assignAndEnqueue(*holdout, false);
230 }
231 }
232 } else {
233 // AND ...(x=FALSE)...: assign(AND = FALSE)
234 assignAndEnqueue(parent, false);
235 }
236 break;
237 case kind::OR:
238 if (childAssignment) {
239 // OR ...(x=TRUE)...: assign(OR = TRUE)
240 assignAndEnqueue(parent, true);
241 } else {
242 TNode::iterator holdout;
243 holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, false)));
244 if (holdout == parent.end()) { // all children are assigned FALSE
245 // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE)
246 assignAndEnqueue(parent, false);
247 } else if (isAssignedTo(parent, true)) {// the OR is TRUE
248 // is the holdout unique ?
249 TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, false)));
250 if (other == parent.end()) { // the holdout is unique
251 // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE)
252 assignAndEnqueue(*holdout, true);
253 }
254 }
255 }
256 break;
257
258 case kind::NOT:
259 // NOT (x=b): assign(NOT = !b)
260 assignAndEnqueue(parent, !childAssignment);
261 break;
262
263 case kind::ITE:
264 if (child == parent[0]) {
265 if (childAssignment) {
266 if (isAssigned(parent[1])) {
267 // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
268 assignAndEnqueue(parent, getAssignment(parent[1]));
269 }
270 } else {
271 if (isAssigned(parent[2])) {
272 // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
273 assignAndEnqueue(parent, getAssignment(parent[2]));
274 }
275 }
276 }
277 if (child == parent[1]) {
278 if (isAssignedTo(parent[0], true)) {
279 // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
280 assignAndEnqueue(parent, childAssignment);
281 }
282 }
283 if (child == parent[2]) {
284 Assert(child == parent[2]);
285 if (isAssignedTo(parent[0], false)) {
286 // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
287 assignAndEnqueue(parent, childAssignment);
288 }
289 }
290 break;
291 case kind::EQUAL:
292 Assert( parent[0].getType().isBoolean() );
293 if (isAssigned(parent[0]) && isAssigned(parent[1])) {
294 // IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment))
295 assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1]));
296 } else {
297 if (isAssigned(parent)) {
298 if (child == parent[0]) {
299 if (getAssignment(parent)) {
300 // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b)
301 assignAndEnqueue(parent[1], childAssignment);
302 } else {
303 // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b)
304 assignAndEnqueue(parent[1], !childAssignment);
305 }
306 } else {
307 Assert(child == parent[1]);
308 if (getAssignment(parent)) {
309 // IFF x y = b: if IFF is assigned to TRUE, assign(x = b)
310 assignAndEnqueue(parent[0], childAssignment);
311 } else {
312 // IFF x y = b y: if IFF is assigned to TRUE, assign(x = !b)
313 assignAndEnqueue(parent[0], !childAssignment);
314 }
315 }
316 }
317 }
318 break;
319 case kind::IMPLIES:
320 if (isAssigned(parent[0]) && isAssigned(parent[1])) {
321 // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
322 assignAndEnqueue(parent, !getAssignment(parent[0]) || getAssignment(parent[1]));
323 } else {
324 if (child == parent[0] && childAssignment && isAssignedTo(parent, true)) {
325 // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE)
326 assignAndEnqueue(parent[1], true);
327 }
328 if (child == parent[1] && !childAssignment && isAssignedTo(parent, true)) {
329 // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE)
330 assignAndEnqueue(parent[0], false);
331 }
332 // Note that IMPLIES == FALSE doesn't need any cases here
333 // because if that assignment has been done, we've already
334 // propagated all the children (in back-propagation).
335 }
336 break;
337 case kind::XOR:
338 if (isAssigned(parent)) {
339 if (child == parent[0]) {
340 // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR)
341 assignAndEnqueue(parent[1], childAssignment != getAssignment(parent));
342 } else {
343 Assert(child == parent[1]);
344 // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR))
345 assignAndEnqueue(parent[0], childAssignment != getAssignment(parent));
346 }
347 }
348 if (isAssigned(parent[0]) && isAssigned(parent[1])) {
349 assignAndEnqueue(parent, getAssignment(parent[0]) != getAssignment(parent[1]));
350 }
351 break;
352 default:
353 Unhandled();
354 }
355 }
356 }
357
propagate()358 bool CircuitPropagator::propagate() {
359
360 Debug("circuit-prop") << "CircuitPropagator::propagate()" << std::endl;
361
362 for(unsigned i = 0; i < d_propagationQueue.size() && !d_conflict; ++ i) {
363
364 // The current node we are propagating
365 TNode current = d_propagationQueue[i];
366 Debug("circuit-prop") << "CircuitPropagator::propagate(): processing " << current << std::endl;
367 bool assignment = getAssignment(current);
368 Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl;
369
370 // Is this an atom
371 bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar()
372 || (current.getKind() == kind::EQUAL
373 && (current[0].isVar() && current[1].isVar()));
374
375 // If an atom, add to the list for simplification
376 if (atom) {
377 Debug("circuit-prop") << "CircuitPropagator::propagate(): adding to learned: " << (assignment ? (Node)current : current.notNode()) << std::endl;
378 d_learnedLiterals.push_back(assignment ? (Node)current : current.notNode());
379 }
380
381 // Propagate this value to the children (if not an atom or a constant)
382 if (d_backwardPropagation && !atom && !current.isConst()) {
383 propagateBackward(current, assignment);
384 }
385 // Propagate this value to the parents
386 if (d_forwardPropagation) {
387 propagateForward(current, assignment);
388 }
389 }
390
391 // No conflict
392 return d_conflict;
393 }
394
395 }/* CVC4::theory::booleans namespace */
396 }/* CVC4::theory namespace */
397 }/* CVC4 namespace */
398