From 33db5447e5e659628ff5845d907aec151765a8c6 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 21 Mar 2013 14:26:54 -0400 Subject: [PATCH] more equality constant evaluation --- src/theory/uf/equality_engine.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 2fcf43054..50c21a1e6 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -244,7 +244,9 @@ void EqualityEngine::subtermEvaluates(EqualityNodeId id) { Debug("equality::evaluation") << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): " << d_subtermsToEvaluate[id] << std::endl; Assert(!d_isInternal[id]); Assert(d_subtermsToEvaluate[id] > 0); - d_subtermsToEvaluate[id] --; + if ((-- d_subtermsToEvaluate[id]) == 0) { + d_evaluationQueue.push(id); + } d_subtermEvaluates.push_back(id); d_subtermEvaluatesSize = d_subtermEvaluates.size(); Debug("equality::evaluation") << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): new " << d_subtermsToEvaluate[id] << std::endl; @@ -296,6 +298,7 @@ void EqualityEngine::addTerm(TNode t) { d_subtermsToEvaluate[result] = t.getNumChildren(); for (unsigned i = 0; i < t.getNumChildren(); ++ i) { if (isConstant(getNodeId(t[i]))) { + Debug("equality::evaluation") << d_name << "::eq::addTerm(" << t << "): evaluatates " << t[i] << std::endl; subtermEvaluates(result); } } -- 2.30.2