Modify equality engine to allow operators to be marked as external terms (#1082)

This is required for reasoning higher-order, since we may have equalities between functions, which are operators of APPLY_UF terms.

This commit gets around the previous 1% slowdown by modifying the changes to the equality engine to be minimal impact. Previously the "isInternal" flag could be reset to false after a term is marked as internal=true. This provides an interface for whether operators of a kind should be marked as internal=false from the start. When using higher-order, APPLY_UF operators will be marked as being external when the higher-order option ufHo is set to true.

This has <.001% impact on performance on QF smtlib : https://www.starexec.org/starexec/secure/details/job.jsp?id=24445

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index a73425a80ba80f5389ff79306d9c07ea34fcfc36..1378b4edf576ad9e99edec52706e6ad191fc3439 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -250,11 +250,17 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
   return newId;
 }
 
-void EqualityEngine::addFunctionKind(Kind fun, bool interpreted) {
+void EqualityEngine::addFunctionKind(Kind fun, bool interpreted, bool extOperator) {
   d_congruenceKinds |= fun;
-  if (interpreted && fun != kind::EQUAL) {
-    Debug("equality::evaluation") << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted " << std::endl;
-    d_congruenceKindsInterpreted |= fun;
+  if (fun != kind::EQUAL) {
+    if (interpreted) {
+      Debug("equality::evaluation") << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted " << std::endl;
+      d_congruenceKindsInterpreted |= fun;
+    }
+    if (extOperator) {
+      Debug("equality::extoperator") << d_name << "::eq::addFunctionKind(): " << fun << " is an external operator kind " << std::endl;
+      d_congruenceKindsExtOperators |= fun;
+    }
   }
 }
 
@@ -297,7 +303,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
   } else if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) {
     TNode tOp = t.getOperator();
     // Add the operator
-    addTermInternal(tOp, true);
+    addTermInternal(tOp, !isExternalOperatorKind(t.getKind()));
     result = getNodeId(tOp);
     // Add all the children and Curryfy
     bool isInterpreted = isInterpretedFunctionKind(t.getKind());

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 5be32ab908222dd9d4dec1ccc08264f11f0bcab7..9638b9f093bd65bd4e24fb29659bcec87b346896 100644 (file)
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -230,6 +230,9 @@ private:
   /** The map of kinds to be treated as interpreted function applications (for evaluation of constants) */
   KindMap d_congruenceKindsInterpreted;
 
+  /** The map of kinds with operators to be considered external (for higher-order) */
+  KindMap d_congruenceKindsExtOperators;
+
   /** Objects that need to be notified during equality path reconstruction */
   std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers;
 
@@ -714,9 +717,13 @@ public:
   }
 
   /**
-   * Add a kind to treat as function applications.
+   * Add a kind to treat as function applications. 
+   * When extOperator is true, this equality engine will treat the operators of this kind 
+   * as "external" e.g. not internal nodes (see d_isInternal). This means that we will 
+   * consider equivalence classes containing the operators of such terms, and "hasTerm" will
+   * return true.
    */
-  void addFunctionKind(Kind fun, bool interpreted = false);
+  void addFunctionKind(Kind fun, bool interpreted = false, bool extOperator = false);
 
   /**
    * Returns true if this kind is used for congruence closure.
@@ -732,6 +739,13 @@ public:
     return d_congruenceKindsInterpreted.tst(fun);
   }
 
+  /**
+   * Returns true if this kind has an operator that is considered external (e.g. not internal).
+   */
+  bool isExternalOperatorKind(Kind fun) const {
+    return d_congruenceKindsExtOperators.tst(fun);
+  }
+
   /**
    * Check whether the node is already in the database.
    */