1 /********************* */
2 /*! \file circuit_propagator.h
4 ** Original author: mdeters
5 ** Major contributors: dejan
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief A non-clausal circuit propagator for Boolean simplification
16 ** A non-clausal circuit propagator for Boolean simplification.
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
22 #define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
27 #include "theory/theory.h"
28 #include "context/context.h"
29 #include "util/hash.h"
30 #include "expr/node.h"
31 #include "context/cdhashset.h"
32 #include "context/cdhashmap.h"
33 #include "context/cdo.h"
41 * The main purpose of the CircuitPropagator class is to maintain the
42 * state of the circuit for subsequent calls to propagate(), so that
43 * the same fact is not output twice, so that the same edge in the
44 * circuit isn't propagated twice, etc.
46 class CircuitPropagator
{
51 * Value of a particular node
53 enum AssignmentStatus
{
54 /** Node is currently unassigned */
56 /** Node is assigned to true */
58 /** Node is assigned to false */
62 /** Invert a set value */
63 static inline AssignmentStatus
neg(AssignmentStatus value
) {
64 Assert(value
!= UNASSIGNED
);
65 if (value
== ASSIGNED_TO_TRUE
) return ASSIGNED_TO_FALSE
;
66 else return ASSIGNED_TO_TRUE
;
71 /** Back edges from nodes to where they are used */
72 typedef std::hash_map
<Node
, std::vector
<Node
>, NodeHashFunction
> BackEdgesMap
;
73 BackEdgesMap d_backEdges
;
75 /** The propagation queue */
76 std::vector
<TNode
> d_propagationQueue
;
78 /** A context-notify object that clears out stale data. */
80 class DataClearer
: context::ContextNotifyObj
{
83 void contextNotifyPop() {
84 Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
85 << "(size was " << d_data
.size() << ")" << std::endl
;
89 DataClearer(context::Context
* context
, T
& data
) :
90 context::ContextNotifyObj(context
),
93 };/* class DataClearer<T> */
96 * We have a propagation queue "clearer" object for when the user
97 * context pops. Normally the propagation queue should be empty,
98 * but this keeps us safe in case there's still some rubbish around
101 DataClearer
< std::vector
<TNode
> > d_propagationQueueClearer
;
103 /** Are we in conflict */
104 context::CDO
<bool> d_conflict
;
106 /** Map of substitutions */
107 std::vector
<Node
>& d_learnedLiterals
;
110 * Similar data clearer for learned literals.
112 DataClearer
< std::vector
<Node
> > d_learnedLiteralClearer
;
114 /** Nodes that have been attached already (computed forward edges for) */
115 // All the nodes we've visited so far
116 context::CDHashSet
<TNode
, TNodeHashFunction
> d_seen
;
119 * Assignment status of each node.
121 typedef context::CDHashMap
<TNode
, AssignmentStatus
, TNodeHashFunction
> AssignmentMap
;
122 AssignmentMap d_state
;
125 * Assign Node in circuit with the value and add it to the queue; note conflicts.
127 void assignAndEnqueue(TNode n
, bool value
) {
129 Trace("circuit-prop") << "CircuitPropagator::assign(" << n
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
131 if (n
.getKind() == kind::CONST_BOOLEAN
) {
132 // Assigning a constant to the opposite value is dumb
133 if (value
!= n
.getConst
<bool>()) {
139 // Get the current assignement
140 AssignmentStatus state
= d_state
[n
];
142 if(state
!= UNASSIGNED
) {
143 // If the node is already assigned we might have a conflict
144 if(value
!= (state
== ASSIGNED_TO_TRUE
)) {
148 // If unassigned, mark it as assigned
149 d_state
[n
] = value
? ASSIGNED_TO_TRUE
: ASSIGNED_TO_FALSE
;
150 // Add for further propagation
151 d_propagationQueue
.push_back(n
);
155 /** True iff Node is assigned in circuit (either true or false). */
156 bool isAssigned(TNode n
) const {
157 AssignmentMap::const_iterator i
= d_state
.find(n
);
158 return i
!= d_state
.end() && ((*i
).second
!= UNASSIGNED
);
161 /** True iff Node is assigned to the value. */
162 bool isAssignedTo(TNode n
, bool value
) const {
163 AssignmentMap::const_iterator i
= d_state
.find(n
);
164 if (i
== d_state
.end()) return false;
165 if (value
&& ((*i
).second
== ASSIGNED_TO_TRUE
)) return true;
166 if (!value
&& ((*i
).second
== ASSIGNED_TO_FALSE
)) return true;
170 /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */
171 bool getAssignment(TNode n
) const {
172 AssignmentMap::iterator i
= d_state
.find(n
);
173 Assert(i
!= d_state
.end() && (*i
).second
!= UNASSIGNED
);
174 return (*i
).second
== ASSIGNED_TO_TRUE
;
177 /** Predicate for use in STL functions. */
178 class IsAssigned
: public std::unary_function
<TNode
, bool> {
179 CircuitPropagator
& d_circuit
;
181 IsAssigned(CircuitPropagator
& circuit
) :
185 bool operator()(TNode in
) const {
186 return d_circuit
.isAssigned(in
);
188 };/* class IsAssigned */
190 /** Predicate for use in STL functions. */
191 class IsAssignedTo
: public std::unary_function
<TNode
, bool> {
192 CircuitPropagator
& d_circuit
;
195 IsAssignedTo(CircuitPropagator
& circuit
, bool value
) :
200 bool operator()(TNode in
) const {
201 return d_circuit
.isAssignedTo(in
, d_value
);
203 };/* class IsAssignedTo */
206 * Compute the map from nodes to the nodes that use it.
208 void computeBackEdges(TNode node
);
211 * Propagate new information forward in circuit to
212 * the parents of "in".
214 void propagateForward(TNode child
, bool assignment
);
217 * Propagate new information backward in circuit to
218 * the children of "in".
220 void propagateBackward(TNode parent
, bool assignment
);
222 /** Whether to perform forward propagation */
223 const bool d_forwardPropagation
;
225 /** Whether to perform backward propagation */
226 const bool d_backwardPropagation
;
230 * Construct a new CircuitPropagator.
232 CircuitPropagator(context::Context
* context
, std::vector
<Node
>& outLearnedLiterals
,
233 bool enableForward
= true, bool enableBackward
= true) :
235 d_propagationQueue(),
236 d_propagationQueueClearer(context
, d_propagationQueue
),
237 d_conflict(context
, false),
238 d_learnedLiterals(outLearnedLiterals
),
239 d_learnedLiteralClearer(context
, outLearnedLiterals
),
242 d_forwardPropagation(enableForward
),
243 d_backwardPropagation(enableBackward
) {
246 /** Assert for propagation */
247 void assert(TNode assertion
);
250 * Propagate through the asserted circuit propagator. New information discovered by the propagator
251 * are put in the subsitutions vector used in construction.
253 * @return true iff conflict found
255 bool propagate() CVC4_WARN_UNUSED_RESULT
;
257 };/* class CircuitPropagator */
259 }/* CVC4::theory::booleans namespace */
260 }/* CVC4::theory namespace */
261 }/* CVC4 namespace */
263 #endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */