1 /********************* */
2 /*! \file circuit_propagator.h
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Morgan Deters, Dejan Jovanovic
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
12 ** \brief A non-clausal circuit propagator for Boolean simplification
14 ** A non-clausal circuit propagator for Boolean simplification.
17 #include "cvc4_private.h"
19 #ifndef CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
20 #define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
23 #include <unordered_map>
26 #include "context/cdhashmap.h"
27 #include "context/cdhashset.h"
28 #include "context/cdo.h"
29 #include "context/context.h"
30 #include "expr/node.h"
31 #include "theory/theory.h"
32 #include "util/hash.h"
39 * The main purpose of the CircuitPropagator class is to maintain the
40 * state of the circuit for subsequent calls to propagate(), so that
41 * the same fact is not output twice, so that the same edge in the
42 * circuit isn't propagated twice, etc.
44 class CircuitPropagator
48 * Value of a particular node
52 /** Node is currently unassigned */
54 /** Node is assigned to true */
56 /** Node is assigned to false */
60 typedef std::unordered_map
<Node
, std::vector
<Node
>, NodeHashFunction
>
64 * Construct a new CircuitPropagator.
66 CircuitPropagator(bool enableForward
= true, bool enableBackward
= true)
69 d_propagationQueueClearer(&d_context
, d_propagationQueue
),
70 d_conflict(&d_context
, false),
72 d_learnedLiteralClearer(&d_context
, d_learnedLiterals
),
74 d_backEdgesClearer(&d_context
, d_backEdges
),
77 d_forwardPropagation(enableForward
),
78 d_backwardPropagation(enableBackward
),
83 /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */
84 bool getAssignment(TNode n
) const
86 AssignmentMap::iterator i
= d_state
.find(n
);
87 Assert(i
!= d_state
.end() && (*i
).second
!= UNASSIGNED
);
88 return (*i
).second
== ASSIGNED_TO_TRUE
;
91 // Use custom context to ensure propagator is reset after use
92 void initialize() { d_context
.push(); }
94 void setNeedsFinish(bool value
) { d_needsFinish
= value
; }
96 bool getNeedsFinish() { return d_needsFinish
; }
98 std::vector
<Node
>& getLearnedLiterals() { return d_learnedLiterals
; }
100 void finish() { d_context
.pop(); }
102 /** Assert for propagation */
103 void assertTrue(TNode assertion
);
106 * Propagate through the asserted circuit propagator. New information
107 * discovered by the propagator are put in the substitutions vector used in
110 * @return true iff conflict found
112 bool propagate() CVC4_WARN_UNUSED_RESULT
;
115 * Get the back edges of this circuit.
117 const BackEdgesMap
& getBackEdges() const { return d_backEdges
; }
119 /** Invert a set value */
120 static inline AssignmentStatus
neg(AssignmentStatus value
)
122 Assert(value
!= UNASSIGNED
);
123 if (value
== ASSIGNED_TO_TRUE
)
124 return ASSIGNED_TO_FALSE
;
126 return ASSIGNED_TO_TRUE
;
129 /** True iff Node is assigned in circuit (either true or false). */
130 bool isAssigned(TNode n
) const
132 AssignmentMap::const_iterator i
= d_state
.find(n
);
133 return i
!= d_state
.end() && ((*i
).second
!= UNASSIGNED
);
136 /** True iff Node is assigned to the value. */
137 bool isAssignedTo(TNode n
, bool value
) const
139 AssignmentMap::const_iterator i
= d_state
.find(n
);
140 if (i
== d_state
.end()) return false;
141 if (value
&& ((*i
).second
== ASSIGNED_TO_TRUE
)) return true;
142 if (!value
&& ((*i
).second
== ASSIGNED_TO_FALSE
)) return true;
147 /** A context-notify object that clears out stale data. */
149 class DataClearer
: context::ContextNotifyObj
152 DataClearer(context::Context
* context
, T
& data
)
153 : context::ContextNotifyObj(context
), d_data(data
)
158 void contextNotifyPop() override
160 Trace("circuit-prop")
161 << "CircuitPropagator::DataClearer: clearing data "
162 << "(size was " << d_data
.size() << ")" << std::endl
;
168 }; /* class DataClearer<T> */
170 /** Predicate for use in STL functions. */
171 class IsAssigned
: public std::unary_function
<TNode
, bool>
173 CircuitPropagator
& d_circuit
;
176 IsAssigned(CircuitPropagator
& circuit
) : d_circuit(circuit
) {}
178 bool operator()(TNode in
) const { return d_circuit
.isAssigned(in
); }
179 }; /* class IsAssigned */
181 /** Predicate for use in STL functions. */
182 class IsAssignedTo
: public std::unary_function
<TNode
, bool>
184 CircuitPropagator
& d_circuit
;
188 IsAssignedTo(CircuitPropagator
& circuit
, bool value
)
189 : d_circuit(circuit
), d_value(value
)
193 bool operator()(TNode in
) const
195 return d_circuit
.isAssignedTo(in
, d_value
);
197 }; /* class IsAssignedTo */
200 * Assignment status of each node.
202 typedef context::CDHashMap
<TNode
, AssignmentStatus
, TNodeHashFunction
>
206 * Assign Node in circuit with the value and add it to the queue; note
209 void assignAndEnqueue(TNode n
, bool value
)
211 Trace("circuit-prop") << "CircuitPropagator::assign(" << n
<< ", "
212 << (value
? "true" : "false") << ")" << std::endl
;
214 if (n
.getKind() == kind::CONST_BOOLEAN
)
216 // Assigning a constant to the opposite value is dumb
217 if (value
!= n
.getConst
<bool>())
224 // Get the current assignment
225 AssignmentStatus state
= d_state
[n
];
227 if (state
!= UNASSIGNED
)
229 // If the node is already assigned we might have a conflict
230 if (value
!= (state
== ASSIGNED_TO_TRUE
))
237 // If unassigned, mark it as assigned
238 d_state
[n
] = value
? ASSIGNED_TO_TRUE
: ASSIGNED_TO_FALSE
;
239 // Add for further propagation
240 d_propagationQueue
.push_back(n
);
245 * Compute the map from nodes to the nodes that use it.
247 void computeBackEdges(TNode node
);
250 * Propagate new information forward in circuit to
251 * the parents of "in".
253 void propagateForward(TNode child
, bool assignment
);
256 * Propagate new information backward in circuit to
257 * the children of "in".
259 void propagateBackward(TNode parent
, bool assignment
);
261 context::Context d_context
;
263 /** The propagation queue */
264 std::vector
<TNode
> d_propagationQueue
;
267 * We have a propagation queue "clearer" object for when the user
268 * context pops. Normally the propagation queue should be empty,
269 * but this keeps us safe in case there's still some rubbish around
272 DataClearer
<std::vector
<TNode
> > d_propagationQueueClearer
;
274 /** Are we in conflict? */
275 context::CDO
<bool> d_conflict
;
277 /** Map of substitutions */
278 std::vector
<Node
> d_learnedLiterals
;
281 * Similar data clearer for learned literals.
283 DataClearer
<std::vector
<Node
>> d_learnedLiteralClearer
;
286 * Back edges from nodes to where they are used.
288 BackEdgesMap d_backEdges
;
291 * Similar data clearer for back edges.
293 DataClearer
<BackEdgesMap
> d_backEdgesClearer
;
295 /** Nodes that have been attached already (computed forward edges for) */
296 // All the nodes we've visited so far
297 context::CDHashSet
<Node
, NodeHashFunction
> d_seen
;
299 AssignmentMap d_state
;
301 /** Whether to perform forward propagation */
302 const bool d_forwardPropagation
;
304 /** Whether to perform backward propagation */
305 const bool d_backwardPropagation
;
307 /* Does the current state require a call to finish()? */
310 }; /* class CircuitPropagator */
312 } // namespace booleans
313 } // namespace theory
316 #endif /* CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */