diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-09-19 20:06:27 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-09-19 20:06:27 +0000 |
commit | 26da597e228537d78d306676b4b79e9b3703900d (patch) | |
tree | 551ab8b61c011a624ad0ae92cfcb930c64ef5948 | |
parent | 95901566948b3da00e8dea6a9c022fe027a2ea92 (diff) |
fix for bug 370.
some internal nodes in eq engine were treated as constants incorrectly
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index b9114cb51..c2647902c 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -176,6 +176,7 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId } else { // If it's there, we need to merge these two Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup exists, adding to queue" << std::endl; + Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup = " << d_nodes[find->second] << std::endl; enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null())); } @@ -211,7 +212,7 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { // Mark the no-individual trigger d_nodeIndividualTrigger.push_back(+null_set_id); // Mark non-constant by default - d_isConstant.push_back(node.isConst()); + d_isConstant.push_back(false); // Mark Boolean nodes d_isBoolean.push_back(false); // Mark the node as internal by default @@ -266,10 +267,12 @@ void EqualityEngine::addTerm(TNode t) { result = newApplicationNode(t, result, getNodeId(t[i]), false); } d_isInternal[result] = false; + d_isConstant[result] = t.isConst(); } else { // Otherwise we just create the new id result = newNode(t); d_isInternal[result] = false; + d_isConstant[result] = t.isConst(); } if (t.getType().isBoolean()) { @@ -1176,6 +1179,9 @@ void EqualityEngine::propagate() { continue; } + Debug("equality::internal") << d_name << "::eq::propagate(): t1: " << (d_isInternal[t1classId] ? "internal" : "proper") << std::endl; + Debug("equality::internal") << d_name << "::eq::propagate(): t2: " << (d_isInternal[t2classId] ? "internal" : "proper") << std::endl; + // Get the nodes of the representatives EqualityNode& node1 = getEqualityNode(t1classId); EqualityNode& node2 = getEqualityNode(t2classId); |