Minor simplification to Theory::theoryOf (#5719)

This removes the special case of constants based on the observation that the theory that owns the type of a constant and the theory that owns its kind always should be the same.

This should lead to a small (maybe 1%) performance improvement, as this method is run ~191M times in our coverage build.

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 08ad8ac873e8b34b585212537f471157add516b3..9ab20e6cb35c9eabbcda2951af68eadaf575e8fd 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -158,10 +158,6 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
           tid = Theory::theoryOf(node.getType());
         }
       }
-      else if (node.isConst())
-      {
-        tid = Theory::theoryOf(node.getType());
-      }
       else if (node.getKind() == kind::EQUAL)
       {
         // Equality is owned by the theory that owns the domain
@@ -169,7 +165,9 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
       }
       else
       {
-        // Regular nodes are owned by the kind
+        // Regular nodes are owned by the kind. Notice that constants are a
+        // special case here, where the theory of the kind of a constant
+        // always coincides with the type of that constant.
         tid = kindToTheoryId(node.getKind());
       }
       break;
@@ -196,11 +194,6 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
           }
         }
       }
-      else if (node.isConst())
-      {
-        // Constants go to the theory of the type
-        tid = Theory::theoryOf(node.getType());
-      }
       else if (node.getKind() == kind::EQUAL)
       {  // Equality
         // If one of them is an ITE, it's irelevant, since they will get
@@ -260,7 +253,8 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
       }
       else
       {
-        // Regular nodes are owned by the kind
+        // Regular nodes are owned by the kind, which includes constants as a
+        // special case.
         tid = kindToTheoryId(node.getKind());
       }
     break;