From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 23 Dec 2020 03:23:15 +0000 (-0600)
Subject: Minor simplification to Theory::theoryOf (#5719)
X-Git-Tag: cvc5-1.0.0~2408
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=718f9f3263de8f549917211a0a700ba6c8bd0c4d;p=cvc5.git

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 08ad8ac87..9ab20e6cb 100644
--- 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;