From: Dejan Jovanović <dejan@cs.nyu.edu>
Date: Thu, 21 Mar 2013 18:26:54 +0000 (-0400)
Subject: more equality constant evaluation
X-Git-Tag: cvc5-1.0.0~7377
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=33db5447e5e659628ff5845d907aec151765a8c6;p=cvc5.git

more equality constant evaluation
---

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);
 	}
       }