summaryrefslogtreecommitdiff
path: root/src/theory/booleans/circuit_propagator.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-03-02 20:12:44 +0000
committerMorgan Deters <mdeters@gmail.com>2012-03-02 20:12:44 +0000
commit53176a3d39935bd77f1c057d0b806c380b346e23 (patch)
treeefd600cfb11113f5cad6107c1f2f5766d0149467 /src/theory/booleans/circuit_propagator.cpp
parent730c6a6baa994a646af08c32151ba487d957d383 (diff)
committing the TNode/Node fix that was in the kind-backend branch; there's still something fishy here, I think I need to merge in a few more things to support incrementality properly. But this fixes "make check" for now
Diffstat (limited to 'src/theory/booleans/circuit_propagator.cpp')
-rw-r--r--src/theory/booleans/circuit_propagator.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 318fdecce..5f3f964de 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -201,11 +201,11 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) {
Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child << ", " << childAssignment << ")" << endl;
// Get the back any nodes where this is child
- const vector<TNode>& parents = d_backEdges.find(child)->second;
+ const vector<Node>& parents = d_backEdges.find(child)->second;
// Go through the parents and see if there is anything to propagate
- vector<TNode>::const_iterator parent_it = parents.begin();
- vector<TNode>::const_iterator parent_it_end = parents.end();
+ vector<Node>::const_iterator parent_it = parents.begin();
+ vector<Node>::const_iterator parent_it_end = parents.end();
for(; parent_it != parent_it_end && !d_conflict; ++ parent_it) {
// The current parent of the child
TNode parent = *parent_it;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback