diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-03-02 20:12:44 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-03-02 20:12:44 +0000 |
| commit | 53176a3d39935bd77f1c057d0b806c380b346e23 (patch) | |
| tree | efd600cfb11113f5cad6107c1f2f5766d0149467 /src/theory | |
| parent | 730c6a6baa994a646af08c32151ba487d957d383 (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')
| -rw-r--r-- | src/theory/booleans/circuit_propagator.cpp | 6 | ||||
| -rw-r--r-- | src/theory/booleans/circuit_propagator.h | 2 |
2 files changed, 4 insertions, 4 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; diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index e1e3073ce..2f9a8f928 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -69,7 +69,7 @@ public: private: /** Back edges from nodes to where they are used */ - typedef std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction> BackEdgesMap; + typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; BackEdgesMap d_backEdges; /** The propagation queue */ |