1 /********************* */
2 /*! \file circuit_propagator.h
4 ** Original author: mdeters
5 ** Major contributors: dejan
6 ** Minor contributors (to current version): barrett
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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
25 #include "theory/theory.h"
26 #include "context/context.h"
27 #include "util/hash.h"
28 #include "expr/node.h"
29 #include "context/cdhashset.h"
30 #include "context/cdhashmap.h"
31 #include "context/cdo.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
{
49 * Value of a particular node
51 enum AssignmentStatus
{
52 /** Node is currently unassigned */
54 /** Node is assigned to true */
56 /** Node is assigned to false */
60 /** Invert a set value */
61 static inline AssignmentStatus
neg(AssignmentStatus value
) {
62 Assert(value
!= UNASSIGNED
);
63 if (value
== ASSIGNED_TO_TRUE
) return ASSIGNED_TO_FALSE
;
64 else return ASSIGNED_TO_TRUE
;
69 context::Context d_context
;
71 /** The propagation queue */
72 std::vector
<TNode
> d_propagationQueue
;
74 /** A context-notify object that clears out stale data. */
76 class DataClearer
: context::ContextNotifyObj
{
79 void contextNotifyPop() {
80 Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
81 << "(size was " << d_data
.size() << ")" << std::endl
;
85 DataClearer(context::Context
* context
, T
& data
) :
86 context::ContextNotifyObj(context
),
89 };/* class DataClearer<T> */
92 * We have a propagation queue "clearer" object for when the user
93 * context pops. Normally the propagation queue should be empty,
94 * but this keeps us safe in case there's still some rubbish around
97 DataClearer
< std::vector
<TNode
> > d_propagationQueueClearer
;
99 /** Are we in conflict */
100 context::CDO
<bool> d_conflict
;
102 /** Map of substitutions */
103 std::vector
<Node
>& d_learnedLiterals
;
106 * Similar data clearer for learned literals.
108 DataClearer
< std::vector
<Node
> > d_learnedLiteralClearer
;
110 /** Back edges from nodes to where they are used */
111 typedef std::hash_map
<Node
, std::vector
<Node
>, NodeHashFunction
> BackEdgesMap
;
112 BackEdgesMap d_backEdges
;
115 * Similar data clearer for back edges.
117 DataClearer
<BackEdgesMap
> d_backEdgesClearer
;
119 /** Nodes that have been attached already (computed forward edges for) */
120 // All the nodes we've visited so far
121 context::CDHashSet
<Node
, NodeHashFunction
> d_seen
;
124 * Assignment status of each node.
126 typedef context::CDHashMap
<TNode
, AssignmentStatus
, TNodeHashFunction
> AssignmentMap
;
127 AssignmentMap d_state
;
130 * Assign Node in circuit with the value and add it to the queue; note conflicts.
132 void assignAndEnqueue(TNode n
, bool value
) {
134 Trace("circuit-prop") << "CircuitPropagator::assign(" << n
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
136 if (n
.getKind() == kind::CONST_BOOLEAN
) {
137 // Assigning a constant to the opposite value is dumb
138 if (value
!= n
.getConst
<bool>()) {
144 // Get the current assignement
145 AssignmentStatus state
= d_state
[n
];
147 if(state
!= UNASSIGNED
) {
148 // If the node is already assigned we might have a conflict
149 if(value
!= (state
== ASSIGNED_TO_TRUE
)) {
153 // If unassigned, mark it as assigned
154 d_state
[n
] = value
? ASSIGNED_TO_TRUE
: ASSIGNED_TO_FALSE
;
155 // Add for further propagation
156 d_propagationQueue
.push_back(n
);
160 /** True iff Node is assigned in circuit (either true or false). */
161 bool isAssigned(TNode n
) const {
162 AssignmentMap::const_iterator i
= d_state
.find(n
);
163 return i
!= d_state
.end() && ((*i
).second
!= UNASSIGNED
);
166 /** True iff Node is assigned to the value. */
167 bool isAssignedTo(TNode n
, bool value
) const {
168 AssignmentMap::const_iterator i
= d_state
.find(n
);
169 if (i
== d_state
.end()) return false;
170 if (value
&& ((*i
).second
== ASSIGNED_TO_TRUE
)) return true;
171 if (!value
&& ((*i
).second
== ASSIGNED_TO_FALSE
)) return true;
175 /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */
176 bool getAssignment(TNode n
) const {
177 AssignmentMap::iterator i
= d_state
.find(n
);
178 Assert(i
!= d_state
.end() && (*i
).second
!= UNASSIGNED
);
179 return (*i
).second
== ASSIGNED_TO_TRUE
;
182 /** Predicate for use in STL functions. */
183 class IsAssigned
: public std::unary_function
<TNode
, bool> {
184 CircuitPropagator
& d_circuit
;
186 IsAssigned(CircuitPropagator
& circuit
) :
190 bool operator()(TNode in
) const {
191 return d_circuit
.isAssigned(in
);
193 };/* class IsAssigned */
195 /** Predicate for use in STL functions. */
196 class IsAssignedTo
: public std::unary_function
<TNode
, bool> {
197 CircuitPropagator
& d_circuit
;
200 IsAssignedTo(CircuitPropagator
& circuit
, bool value
) :
205 bool operator()(TNode in
) const {
206 return d_circuit
.isAssignedTo(in
, d_value
);
208 };/* class IsAssignedTo */
211 * Compute the map from nodes to the nodes that use it.
213 void computeBackEdges(TNode node
);
216 * Propagate new information forward in circuit to
217 * the parents of "in".
219 void propagateForward(TNode child
, bool assignment
);
222 * Propagate new information backward in circuit to
223 * the children of "in".
225 void propagateBackward(TNode parent
, bool assignment
);
227 /** Whether to perform forward propagation */
228 const bool d_forwardPropagation
;
230 /** Whether to perform backward propagation */
231 const bool d_backwardPropagation
;
235 * Construct a new CircuitPropagator.
237 CircuitPropagator(std::vector
<Node
>& outLearnedLiterals
,
238 bool enableForward
= true, bool enableBackward
= true) :
240 d_propagationQueue(),
241 d_propagationQueueClearer(&d_context
, d_propagationQueue
),
242 d_conflict(&d_context
, false),
243 d_learnedLiterals(outLearnedLiterals
),
244 d_learnedLiteralClearer(&d_context
, outLearnedLiterals
),
246 d_backEdgesClearer(&d_context
, d_backEdges
),
249 d_forwardPropagation(enableForward
),
250 d_backwardPropagation(enableBackward
) {
253 // Use custom context to ensure propagator is reset after use
255 { d_context
.push(); }
260 /** Assert for propagation */
261 void assertTrue(TNode assertion
);
264 * Propagate through the asserted circuit propagator. New information discovered by the propagator
265 * are put in the substitutions vector used in construction.
267 * @return true iff conflict found
269 bool propagate() CVC4_WARN_UNUSED_RESULT
;
271 };/* class CircuitPropagator */
273 }/* CVC4::theory::booleans namespace */
274 }/* CVC4::theory namespace */
275 }/* CVC4 namespace */
277 #endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */