Adding evaluation of constant terms to the equality engine. Evaluation on a particular kind can be set by setting interpreted = true when calling addFunctionKind.

4 files changed, 232 insertions, 78 deletions

diff --git a/.cproject b/.cproject
index 299de0591..0e06c7a74 100644
--- a/.cproject
+++ b/.cproject
@@ -18,7 +18,7 @@
 					<folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath="">
 						<toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base">
 							<targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/>
-							<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="10" superClass="cdt.managedbuild.target.gnu.builder.base">
+							<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="3" superClass="cdt.managedbuild.target.gnu.builder.base">
 								<outputEntries>
 									<entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/>
 								</outputEntries>
@@ -55,8 +55,10 @@
 	<storageModule moduleId="cdtBuildSystem" version="4.0.0">
 		<project id="cvc4.null.1129006228" name="cvc4"/>
 	</storageModule>
-	<storageModule moduleId="refreshScope" versionNumber="1">
-		<resource resourceType="PROJECT" workspacePath="/cvc4-trunk"/>
+	<storageModule moduleId="refreshScope" versionNumber="2">
+		<configuration configurationName="Default">
+			<resource resourceType="PROJECT" workspacePath="/cvc4-trunk"/>
+		</configuration>
 	</storageModule>
 	<storageModule moduleId="scannerConfiguration">
 		<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/>
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index f11b1252b..385c2e555 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -35,7 +35,7 @@ EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
   if (d_useEqualityEngine) {
 
     // The kinds we are treating as function application in congruence
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
@@ -44,8 +44,8 @@ EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 636427ed1..f4d79b468 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -90,7 +90,9 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name)
 , d_nodesCount(context, 0)
 , d_assertedEqualitiesCount(context, 0)
 , d_equalityTriggersCount(context, 0)
+, d_nodesThatEvaluateSize(context, 0)
 , d_stats(name)
+, d_inPropagate(false)
 , d_triggerDatabaseSize(context, 0)
 , d_triggerTermSetUpdatesSize(context, 0)
 , d_deducedDisequalitiesSize(context, 0)
@@ -112,7 +114,9 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
 , d_nodesCount(context, 0)
 , d_assertedEqualitiesCount(context, 0)
 , d_equalityTriggersCount(context, 0)
+, d_nodesThatEvaluateSize(context, 0)
 , d_stats(name)
+, d_inPropagate(false)
 , d_triggerDatabaseSize(context, 0)
 , d_triggerTermSetUpdatesSize(context, 0)
 , d_deducedDisequalitiesSize(context, 0)
@@ -156,28 +160,9 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId
   // Add the lookup data, if it's not already there
   ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
   if (find == d_applicationLookup.end()) {
-    // When we backtrack, if the lookup is not there anymore, we'll add it again
     Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl;
     // Mark the normalization to the lookup
     storeApplicationLookup(funNormalized, funId);
-    // If an equality over constants we merge to false 
-    if (isEquality) {
-      if (d_isConstant[t1ClassId] && d_isConstant[t2ClassId] && t1ClassId != t2ClassId) {
-        Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl;
-        Assert(d_nodes[funId].getKind() == kind::EQUAL);
-        enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()), false);
-        // Also enqueue the symmetric one
-        TNode eq = d_nodes[funId];
-        Node symmetricEq = eq[1].eqNode(eq[0]);
-        if (hasTerm(symmetricEq)) {
-          EqualityNodeId symmFunId = getNodeId(symmetricEq);
-          enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()), false);              
-        }
-      }
-      if (t1ClassId == t2ClassId) {
-        enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()), false);
-      }
-    }
   } 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;
@@ -218,6 +203,8 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
   d_nodeIndividualTrigger.push_back(+null_set_id);
   // Mark non-constant by default
   d_isConstant.push_back(false);
+  // Makr non-evaluate by default
+  d_evaluates.push_back(false);
   // Mark Boolean nodes
   d_isBoolean.push_back(false);
   // Mark the node as internal by default
@@ -238,6 +225,14 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
   return newId;
 }
 
+void EqualityEngine::addFunctionKind(Kind fun, bool interpreted) {
+  d_congruenceKinds |= fun;
+  if (interpreted) {
+    Debug("equality::evaluation") << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted " << std::endl;
+    d_congruenceKindsInterpreted |= fun;
+  }
+}
+
 void EqualityEngine::addTerm(TNode t) {
 
   Debug("equality") << d_name << "::eq::addTerm(" << t << ")" << std::endl;
@@ -257,15 +252,20 @@ void EqualityEngine::addTerm(TNode t) {
   if (t.getKind() == kind::EQUAL) {
     addTerm(t[0]);
     addTerm(t[1]);
-    result = newApplicationNode(t, getNodeId(t[0]), getNodeId(t[1]), true);
+    EqualityNodeId t0id = getNodeId(t[0]);
+    EqualityNodeId t1id = getNodeId(t[1]);
+    result = newApplicationNode(t, t0id, t1id, true);
     d_isInternal[result] = false;
+
   } else if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) {
-    // Add the operator
     TNode tOp = t.getOperator();
+    // Add the operator
     addTerm(tOp);
-    // Add all the children and Curryfy
     result = getNodeId(tOp);
     d_isInternal[result] = true;
+    d_isConstant[result] = isInterpretedFunctionKind(t.getKind());
+    d_evaluates[result] = isInterpretedFunctionKind(t.getKind());
+    // Add all the children and Curryfy
     for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
       // Add the child
       addTerm(t[i]);
@@ -273,12 +273,19 @@ void EqualityEngine::addTerm(TNode t) {
       result = newApplicationNode(t, result, getNodeId(t[i]), false);
     }
     d_isInternal[result] = false;
-    d_isConstant[result] = t.isConst();
+    if (t.isConst()) {
+      d_isConstant[result] = true;
+      d_evaluates[result] = true;
+    }
   } else {
     // Otherwise we just create the new id
     result = newNode(t);
+    // Is this an operator
     d_isInternal[result] = false;
-    d_isConstant[result] = t.isConst();
+    if (t.isConst()) {
+      d_isConstant[result] = true;
+      d_evaluates[result] = true;
+    }
   }
 
   if (t.getType().isBoolean()) {
@@ -306,8 +313,11 @@ void EqualityEngine::addTerm(TNode t) {
     d_masterEqualityEngine->addTerm(t);
   }
 
+  // Empty the queue
   propagate();
 
+  Assert(hasTerm(t));
+  
   Debug("equality") << d_name << "::eq::addTerm(" << t << ") => " << result << std::endl;
 }
 
@@ -588,28 +598,6 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
         } else {
           // There is no representative, so we can add one, we remove this when backtracking
           storeApplicationLookup(funNormalized, funId);
-          // Note: both checks below we don't need to do in the above case as the normalized lookup
-          //       has already been checked for this
-          // Now, if we're constant and it's an equality, check if the other guy is also a constant
-          if (fun.isEquality) {
-            // If the equation normalizes to two constants, it's disequal
-            if (d_isConstant[aNormalized] && d_isConstant[bNormalized] && aNormalized != bNormalized) {
-              Assert(d_nodes[funId].getKind() == kind::EQUAL);
-              enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()), false);
-              // Also enqueue the symmetric one
-              TNode eq = d_nodes[funId];
-              Node symmetricEq = eq[1].eqNode(eq[0]);
-              if (hasTerm(symmetricEq)) {
-                EqualityNodeId symmFunId = getNodeId(symmetricEq);
-                enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()), false);              
-              }
-            }
-            // If the function normalizes to a = a, we merge it with true, we check that its not
-            // already there so as not to enqueue multiple times when several things get merged
-            if (aNormalized == bNormalized && getEqualityNode(funId).getFind() != d_trueId) {
-              enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()), false);                            
-            } 
-          }
         }
                   
         // Go to the next one in the use list
@@ -800,6 +788,12 @@ void EqualityEngine::backtrack() {
     d_applicationLookups.resize(d_applicationLookupsCount);
   }
 
+  if (d_nodesThatEvaluate.size() > d_nodesThatEvaluateSize) {
+    for(int i = d_nodesThatEvaluate.size() - 1, i_end = (int)d_nodesThatEvaluateSize; i >= i_end; --i) {
+      d_evaluates[d_nodesThatEvaluate[i]] = false;
+    }
+  }
+
   if (d_nodes.size() > d_nodesCount) {
     // Go down the nodes, check the application nodes and remove them from use-lists
     for(int i = d_nodes.size() - 1, i_end = (int)d_nodesCount; i >= i_end; -- i) {
@@ -822,6 +816,7 @@ void EqualityEngine::backtrack() {
     d_nodeTriggers.resize(d_nodesCount);
     d_nodeIndividualTrigger.resize(d_nodesCount);
     d_isConstant.resize(d_nodesCount);
+    d_evaluates.resize(d_nodesCount);
     d_isBoolean.resize(d_nodesCount);
     d_isInternal.resize(d_nodesCount);
     d_equalityGraph.resize(d_nodesCount);
@@ -840,6 +835,7 @@ void EqualityEngine::backtrack() {
     d_deducedDisequalityReasons.resize(d_deducedDisequalityReasonsSize);
     d_deducedDisequalities.resize(d_deducedDisequalitiesSize);
   }
+  
 }
 
 void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
@@ -994,7 +990,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               equalities.push_back(d_equalityEdges[currentEdge].getReason());
               break;
             case MERGED_THROUGH_REFLEXIVITY: {
-              // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
+              // x1 == x1 
               Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl;
               EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode;
               const FunctionApplication& eq = d_applications[eqId].original;
@@ -1008,22 +1004,24 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               break;              
             }
             case MERGED_THROUGH_CONSTANTS: {
-              // (a = b) == false because a and b are different constants
-              Debug("equality") << d_name << "::eq::getExplanation(): due to constants, going deeper" << std::endl;
-              EqualityNodeId eqId = currentNode == d_falseId ? edgeNode : currentNode;
-              const FunctionApplication& eq = d_applications[eqId].original;
-              Assert(eq.isEquality, "Must be an equality");
-              
+              // f(c1, ..., cn) = c semantically, we can just ignore it 
+              Debug("equality") << d_name << "::eq::getExplanation(): due to constants, explain the constants" << std::endl;
               Debug("equality") << push;
-              // Explain why a is a constant
-              Assert(isConstant(eq.a));
-              getExplanation(eq.a, getEqualityNode(eq.a).getFind(), equalities);
-              // Explain why b is a constant
-              Assert(isConstant(eq.b));
-              getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities);
+
+              // Get the node we interpreted
+              TNode interpreted = d_nodes[currentNode];
+              if (interpreted.isConst()) {
+                interpreted = d_nodes[edgeNode];
+              }
+
+              // Explain why a is a constant by explaining each argument
+              for (unsigned i = 0; i < interpreted.getNumChildren(); ++ i) {
+                EqualityNodeId childId = getNodeId(interpreted[i]);
+                Assert(isConstant(childId));
+                getExplanation(childId, getEqualityNode(childId).getFind(), equalities);
+              }
+
               Debug("equality") << pop;
-              // If the constants were merged, we're in trouble
-              Assert(getEqualityNode(eq.a).getFind() != getEqualityNode(eq.b).getFind());
 
               break;
             }
@@ -1172,20 +1170,91 @@ void EqualityEngine::addTriggerEqualityInternal(TNode t1, TNode t2, TNode trigge
   Debug("equality") << d_name << "::eq::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
 }
 
+Node EqualityEngine::evaluateTerm(TNode node) {
+  Debug("equality::evaluation") << d_name << "::eq::evaluateTerm(" << node << ")" << std::endl;
+  NodeBuilder<> builder;
+  builder << node.getKind();
+  if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    builder << node.getOperator();
+  }
+  for (unsigned i = 0; i < node.getNumChildren(); ++ i) {
+    TNode child = node[i];
+    TNode childRep = getRepresentative(child);
+    Debug("equality::evaluation") << d_name << "::eq::evaluateTerm: " << child << " -> " << childRep << std::endl;
+    Assert(childRep.isConst());
+    builder << childRep;
+  }
+  Node newNode = builder;
+  return Rewriter::rewrite(newNode);
+}
+
+void EqualityEngine::processEvaluationQueue() {
+
+  Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): start" << std::endl;
+
+  while (!d_evaluationQueue.empty()) {
+    // Get the node
+    EqualityNodeId id = d_evaluationQueue.front();
+    d_evaluationQueue.pop();
+    
+    // Replace the children with their representatives (must be constants)
+    Node nodeEvaluated = evaluateTerm(d_nodes[id]);
+    Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): " << d_nodes[id] << " evaluates to " << nodeEvaluated << std::endl;
+    Assert(nodeEvaluated.isConst());
+    addTerm(nodeEvaluated);
+    EqualityNodeId nodeEvaluatedId = getNodeId(nodeEvaluated);
+
+    // Enqueue the semantic equality
+    enqueue(MergeCandidate(id, nodeEvaluatedId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+  }
+
+  Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): done" << std::endl;
+}
+
+void EqualityEngine::evaluateApplication(const FunctionApplication& funNormalized, EqualityNodeId funId) {
+
+  // Evaluate special for equality and other
+  if (!funNormalized.isEquality) {
+    // We can't add new terms 
+    d_evaluationQueue.push(funId);
+  } else {
+    if (funNormalized.a != funNormalized.b) {
+      // We don't enqueue fun -> true, as this is convered with reflexivity
+      enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+    }
+  }
+}
+
 void EqualityEngine::propagate() {
 
+  if (d_inPropagate) {
+    // We're already in propagate, go back
+    return;
+  } 
+  
+  // Make sure we don't get in again
+  ScopedBool inPropagate(d_inPropagate, true);
+  
   Debug("equality") << d_name << "::eq::propagate()" << std::endl;
 
-  while (!d_propagationQueue.empty()) {
-
-    // The current merge candidate
-    const MergeCandidate current = d_propagationQueue.front();
-    d_propagationQueue.pop_front();
+  while (!d_propagationQueue.empty() || !d_evaluationQueue.empty()) {
 
     if (d_done) {
       // If we're done, just empty the queue
+      while (!d_propagationQueue.empty()) d_propagationQueue.pop_front();
+      while (!d_evaluationQueue.empty()) d_evaluationQueue.pop();
       continue;
     }
+    
+    // Process any evaluation requests
+    if (!d_evaluationQueue.empty()) {
+      processEvaluationQueue();
+      continue;
+    }
+    
+    // The current merge candidate
+    const MergeCandidate current = d_propagationQueue.front();
+    d_propagationQueue.pop_front();
 
     // Get the representatives
     EqualityNodeId t1classId = getEqualityNode(current.t1Id).getFind();
@@ -1547,6 +1616,23 @@ void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized,
   Debug("equality::backtrack") << "d_applicationLookupsCount = " << d_applicationLookupsCount << std::endl;
   Debug("equality::backtrack") << "d_applicationLookups.size() = " << d_applicationLookups.size() << std::endl;
   Assert(d_applicationLookupsCount == d_applicationLookups.size());
+
+  // If an equality over constants we merge to false
+  if (funNormalized.isEquality && funNormalized.a == funNormalized.b) {
+    enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()));
+  }
+
+  // Now check for application evaluation
+  if (!d_evaluates[funId]) {
+    if (d_evaluates[funNormalized.a] && d_evaluates[funNormalized.b]) {
+      // Depending on the "internal"
+      if (d_isInternal[funId]) {
+        setEvaluates(funId);
+      } else {
+        evaluateApplication(funNormalized, funId);
+      }
+    }
+  }
 }
 
 void EqualityEngine::getUseListTerms(TNode t, std::set<TNode>& output) {
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 9bc2cb61c..3d80c486a 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -233,6 +233,9 @@ private:
   /** The map of kinds to be treated as function applications */
   KindMap d_congruenceKinds;
 
+  /** The map of kinds to be treated as interpreted function applications (for evaluation of constants) */
+  KindMap d_congruenceKindsInterpreted;
+
   /** Map from nodes to their ids */
   __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
 
@@ -415,6 +418,65 @@ private:
   std::vector<bool> d_isConstant;
 
   /**
+   * Map from ids to whether they evaluate. A node evaluates 
+   * (1) if it is a constant
+   * (2) if it is internal and it's children evaluate
+   * (3) if it is non-internal and it's children are constants
+   * 
+   * Example:
+   * 
+   *  f(x) + g(y)
+   * 
+   * If f and g are interpreted, in the context x = 0, the nodes 
+   * f(x) and g(y) evaluate, but not f(x) + g(y). The term f(x) + g(y) 
+   * evaluates if we evaluate f(0) and g(0) to constants c1 and c2.
+   */
+  std::vector<bool> d_evaluates;
+  
+  /** 
+   * For nodes that we need to postpone evaluation.
+   */
+  std::queue<EqualityNodeId> d_evaluationQueue;
+  
+  /**
+   * Evaluate all terms in the evaluation queue.
+   */
+  void processEvaluationQueue();
+  
+  /** 
+   * Check whether the node evaluates in the current context 
+   */
+  bool evaluates(EqualityNodeId id) const {
+    return d_evaluates[id];
+  }
+
+  /** Vector of nodes that evaluate. */
+  std::vector<EqualityNodeId> d_nodesThatEvaluate;
+
+  /** Size of the nodes that evaluate vector. */
+  context::CDO<unsigned> d_nodesThatEvaluateSize;
+  
+  /** Set the node evaluate flag */
+  void setEvaluates(EqualityNodeId id) {
+    Assert(!d_evaluates[id]);
+    d_evaluates[id] = true;
+    d_nodesThatEvaluate.push_back(id);
+    d_nodesThatEvaluateSize = d_nodesThatEvaluate.size();
+  }
+
+  /** 
+   * Propagate something that evaluates.
+   * @param fragile if true, no new terms are added, but 
+   */
+  void evaluateApplication(const FunctionApplication& funNormalized, EqualityNodeId funId);
+
+  /**
+   * Returns the evaluation of the term when all (direct) children are replaced with 
+   * the constant representatives.
+   */
+  Node evaluateTerm(TNode node);
+  
+  /**
    * Returns true if it's a constant
    */
   bool isConstant(EqualityNodeId id) const {
@@ -451,10 +513,13 @@ private:
 
   /** Enqueue to the propagation queue */
   void enqueue(const MergeCandidate& candidate, bool back = true);
-
+  
   /** Do the propagation */
   void propagate();
 
+  /** Are we in propagate */
+  bool d_inPropagate;
+
   /**
    * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
    * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
@@ -674,20 +739,21 @@ public:
   /**
    * Add a kind to treat as function applications.
    */
-  void addFunctionKind(Kind fun) {
-    d_congruenceKinds |= fun;
-  }
+  void addFunctionKind(Kind fun, bool interpreted = false);
 
   /**
    * Returns true if this kind is used for congruence closure.
    */
-  bool isFunctionKind(Kind fun) {
+  bool isFunctionKind(Kind fun) const {
     return d_congruenceKinds.tst(fun);
   }
 
   /**
-   * Adds a function application term to the database.
+   * Returns true if this kind is used for congruencce closure + evaluation of constants.
    */
+  bool isInterpretedFunctionKind(Kind fun) const {
+    return d_congruenceKindsInterpreted.tst(fun);
+  }
 
   /**
    * Check whether the node is already in the database.