1 /********************* */
2 /*! \file circuit_propagator.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Dejan Jovanovic, Clark Barrett
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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
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
;
67 typedef std::hash_map
<Node
, std::vector
<Node
>, NodeHashFunction
> BackEdgesMap
;
71 context::Context d_context
;
73 /** The propagation queue */
74 std::vector
<TNode
> d_propagationQueue
;
76 /** A context-notify object that clears out stale data. */
78 class DataClearer
: context::ContextNotifyObj
{
81 void contextNotifyPop() {
82 Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
83 << "(size was " << d_data
.size() << ")" << std::endl
;
87 DataClearer(context::Context
* context
, T
& data
) :
88 context::ContextNotifyObj(context
),
91 };/* class DataClearer<T> */
94 * We have a propagation queue "clearer" object for when the user
95 * context pops. Normally the propagation queue should be empty,
96 * but this keeps us safe in case there's still some rubbish around
99 DataClearer
< std::vector
<TNode
> > d_propagationQueueClearer
;
101 /** Are we in conflict? */
102 context::CDO
<bool> d_conflict
;
104 /** Map of substitutions */
105 std::vector
<Node
>& d_learnedLiterals
;
108 * Similar data clearer for learned literals.
110 DataClearer
< std::vector
<Node
> > d_learnedLiteralClearer
;
113 * Back edges from nodes to where they are used.
115 BackEdgesMap d_backEdges
;
118 * Similar data clearer for back edges.
120 DataClearer
<BackEdgesMap
> d_backEdgesClearer
;
122 /** Nodes that have been attached already (computed forward edges for) */
123 // All the nodes we've visited so far
124 context::CDHashSet
<Node
, NodeHashFunction
> d_seen
;
127 * Assignment status of each node.
129 typedef context::CDHashMap
<TNode
, AssignmentStatus
, TNodeHashFunction
> AssignmentMap
;
130 AssignmentMap d_state
;
133 * Assign Node in circuit with the value and add it to the queue; note conflicts.
135 void assignAndEnqueue(TNode n
, bool value
) {
137 Trace("circuit-prop") << "CircuitPropagator::assign(" << n
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
139 if (n
.getKind() == kind::CONST_BOOLEAN
) {
140 // Assigning a constant to the opposite value is dumb
141 if (value
!= n
.getConst
<bool>()) {
147 // Get the current assignment
148 AssignmentStatus state
= d_state
[n
];
150 if(state
!= UNASSIGNED
) {
151 // If the node is already assigned we might have a conflict
152 if(value
!= (state
== ASSIGNED_TO_TRUE
)) {
156 // If unassigned, mark it as assigned
157 d_state
[n
] = value
? ASSIGNED_TO_TRUE
: ASSIGNED_TO_FALSE
;
158 // Add for further propagation
159 d_propagationQueue
.push_back(n
);
164 /** True iff Node is assigned in circuit (either true or false). */
165 bool isAssigned(TNode n
) const {
166 AssignmentMap::const_iterator i
= d_state
.find(n
);
167 return i
!= d_state
.end() && ((*i
).second
!= UNASSIGNED
);
170 /** True iff Node is assigned to the value. */
171 bool isAssignedTo(TNode n
, bool value
) const {
172 AssignmentMap::const_iterator i
= d_state
.find(n
);
173 if (i
== d_state
.end()) return false;
174 if (value
&& ((*i
).second
== ASSIGNED_TO_TRUE
)) return true;
175 if (!value
&& ((*i
).second
== ASSIGNED_TO_FALSE
)) return true;
179 /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */
180 bool getAssignment(TNode n
) const {
181 AssignmentMap::iterator i
= d_state
.find(n
);
182 Assert(i
!= d_state
.end() && (*i
).second
!= UNASSIGNED
);
183 return (*i
).second
== ASSIGNED_TO_TRUE
;
187 /** Predicate for use in STL functions. */
188 class IsAssigned
: public std::unary_function
<TNode
, bool> {
189 CircuitPropagator
& d_circuit
;
191 IsAssigned(CircuitPropagator
& circuit
) :
195 bool operator()(TNode in
) const {
196 return d_circuit
.isAssigned(in
);
198 };/* class IsAssigned */
200 /** Predicate for use in STL functions. */
201 class IsAssignedTo
: public std::unary_function
<TNode
, bool> {
202 CircuitPropagator
& d_circuit
;
205 IsAssignedTo(CircuitPropagator
& circuit
, bool value
) :
210 bool operator()(TNode in
) const {
211 return d_circuit
.isAssignedTo(in
, d_value
);
213 };/* class IsAssignedTo */
216 * Compute the map from nodes to the nodes that use it.
218 void computeBackEdges(TNode node
);
221 * Propagate new information forward in circuit to
222 * the parents of "in".
224 void propagateForward(TNode child
, bool assignment
);
227 * Propagate new information backward in circuit to
228 * the children of "in".
230 void propagateBackward(TNode parent
, bool assignment
);
232 /** Whether to perform forward propagation */
233 const bool d_forwardPropagation
;
235 /** Whether to perform backward propagation */
236 const bool d_backwardPropagation
;
240 * Construct a new CircuitPropagator.
242 CircuitPropagator(std::vector
<Node
>& outLearnedLiterals
,
243 bool enableForward
= true, bool enableBackward
= true) :
245 d_propagationQueue(),
246 d_propagationQueueClearer(&d_context
, d_propagationQueue
),
247 d_conflict(&d_context
, false),
248 d_learnedLiterals(outLearnedLiterals
),
249 d_learnedLiteralClearer(&d_context
, outLearnedLiterals
),
251 d_backEdgesClearer(&d_context
, d_backEdges
),
254 d_forwardPropagation(enableForward
),
255 d_backwardPropagation(enableBackward
) {
258 // Use custom context to ensure propagator is reset after use
260 { d_context
.push(); }
265 /** Assert for propagation */
266 void assertTrue(TNode assertion
);
269 * Propagate through the asserted circuit propagator. New information discovered by the propagator
270 * are put in the substitutions vector used in construction.
272 * @return true iff conflict found
274 bool propagate() CVC4_WARN_UNUSED_RESULT
;
277 * Get the back edges of this circuit.
279 const BackEdgesMap
& getBackEdges() const {
283 };/* class CircuitPropagator */
285 }/* CVC4::theory::booleans namespace */
286 }/* CVC4::theory namespace */
287 }/* CVC4 namespace */
289 #endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */