1 /********************* */
2 /*! \file circuit_propagator.h
4 ** Original author: mdeters
5 ** Major contributors: none
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"
38 * The main purpose of the CircuitPropagator class is to maintain the
39 * state of the circuit for subsequent calls to propagate(), so that
40 * the same fact is not output twice, so that the same edge in the
41 * circuit isn't propagated twice, etc.
43 class CircuitPropagator
{
48 * Value of a particular node
50 enum AssignmentStatus
{
51 /** Node is currently unassigned */
53 /** Node is assigned to true */
55 /** Node is assigned to false */
59 /** Invert a set value */
60 static inline AssignmentStatus
neg(AssignmentStatus value
) {
61 Assert(value
!= UNASSIGNED
);
62 if (value
== ASSIGNED_TO_TRUE
) return ASSIGNED_TO_FALSE
;
63 else return ASSIGNED_TO_TRUE
;
68 /** Back edges from nodes to where they are used */
69 typedef std::hash_map
<TNode
, std::vector
<TNode
>, TNodeHashFunction
> BackEdgesMap
;
70 BackEdgesMap d_backEdges
;
72 /** The propagation queue */
73 std::vector
<TNode
> d_propagationQueue
;
75 /** Are we in conflict */
78 /** Map of substitutions */
79 std::vector
<Node
>& d_learnedLiterals
;
81 /** Nodes that have been attached already (computed forward edges for) */
82 // All the nodes we've visited so far
83 std::hash_set
<TNode
, TNodeHashFunction
> d_seen
;
86 * Assignment status of each node.
88 typedef std::hash_map
<TNode
, AssignmentStatus
, TNodeHashFunction
> AssignmentMap
;
89 AssignmentMap d_state
;
92 * Assign Node in circuit with the value and add it to the queue; note conflicts.
94 void assignAndEnqueue(TNode n
, bool value
) {
96 Debug("circuit-prop") << "CircuitPropagator::assign(" << n
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
98 if (n
.getKind() == kind::CONST_BOOLEAN
) {
99 // Assigning a constant to the opposite value is dumb
100 if (value
!= n
.getConst
<bool>()) {
106 // Get the current assignement
107 AssignmentStatus state
= d_state
[n
];
109 if(state
!= UNASSIGNED
) {
110 // If the node is already assigned we might have a conflict
111 if(value
!= (state
== ASSIGNED_TO_TRUE
)) {
115 // If unassigned, mark it as assigned
116 d_state
[n
] = value
? ASSIGNED_TO_TRUE
: ASSIGNED_TO_FALSE
;
117 // Add for further propagation
118 d_propagationQueue
.push_back(n
);
122 /** True iff Node is assigned in circuit (either true or false). */
123 bool isAssigned(TNode n
) const {
124 AssignmentMap::const_iterator i
= d_state
.find(n
);
125 return i
!= d_state
.end() && ((*i
).second
!= UNASSIGNED
);
128 /** True iff Node is assigned to the value. */
129 bool isAssignedTo(TNode n
, bool value
) const {
130 AssignmentMap::const_iterator i
= d_state
.find(n
);
131 if (i
== d_state
.end()) return false;
132 if (value
&& ((*i
).second
== ASSIGNED_TO_TRUE
)) return true;
133 if (!value
&& ((*i
).second
== ASSIGNED_TO_FALSE
)) return true;
137 /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */
138 bool getAssignment(TNode n
) const {
139 Assert(d_state
.find(n
) != d_state
.end() && d_state
.find(n
)->second
!= UNASSIGNED
);
140 return d_state
.find(n
)->second
== ASSIGNED_TO_TRUE
;
143 /** Predicate for use in STL functions. */
144 class IsAssigned
: public std::unary_function
<TNode
, bool> {
145 CircuitPropagator
& d_circuit
;
147 IsAssigned(CircuitPropagator
& circuit
) :
151 bool operator()(TNode in
) const {
152 return d_circuit
.isAssigned(in
);
154 };/* class IsAssigned */
156 /** Predicate for use in STL functions. */
157 class IsAssignedTo
: public std::unary_function
<TNode
, bool> {
158 CircuitPropagator
& d_circuit
;
161 IsAssignedTo(CircuitPropagator
& circuit
, bool value
) :
166 bool operator()(TNode in
) const {
167 return d_circuit
.isAssignedTo(in
, d_value
);
169 };/* class IsAssignedTo */
172 * Compute the map from nodes to the nodes that use it.
174 void computeBackEdges(TNode node
);
177 * Propagate new information forward in circuit to
178 * the parents of "in".
180 void propagateForward(TNode child
, bool assignment
);
183 * Propagate new information backward in circuit to
184 * the children of "in".
186 void propagateBackward(TNode parent
, bool assignment
);
188 /** Whether to perform forward propagation */
189 bool d_forwardPropagation
;
190 /** Whether to perform backward propagation */
191 bool d_backwardPropagation
;
192 /** Whether to perform expensive propagations */
193 bool d_expensivePropagation
;
197 * Construct a new CircuitPropagator with the given atoms and backEdges.
199 CircuitPropagator(std::vector
<Node
>& outLearnedLiterals
, bool enableForward
= true, bool enableBackward
= true, bool enableExpensive
= true) :
201 d_learnedLiterals(outLearnedLiterals
),
202 d_forwardPropagation(enableForward
),
203 d_backwardPropagation(enableBackward
),
204 d_expensivePropagation(enableExpensive
)
208 /** Assert for propagation */
209 void assert(TNode assertion
);
212 * Propagate through the asserted circuit propagator. New information discovered by the propagator
213 * are put in the subsitutions vector used in construction.
215 * @return true iff conflict found
217 bool propagate() CVC4_WARN_UNUSED_RESULT
;
219 };/* class CircuitPropagator */
221 }/* CVC4::theory::booleans namespace */
222 }/* CVC4::theory namespace */
223 }/* CVC4 namespace */
225 #endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */