From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 2 Mar 2012 20:12:44 +0000 (+0000)
Subject: committing the TNode/Node fix that was in the kind-backend branch; there's still... 
X-Git-Tag: cvc5-1.0.0~8289
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=53176a3d39935bd77f1c057d0b806c380b346e23;p=cvc5.git

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
---

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 */