diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-22 21:23:15 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-22 21:23:15 -0600 |
commit | 718f9f3263de8f549917211a0a700ba6c8bd0c4d (patch) | |
tree | 623c62429a4aa1a4541a362872d8c1660546df4c /src/theory | |
parent | b8bb85a0d0ca254081f216481974deed9d449aa5 (diff) |
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.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/theory.cpp | 16 |
1 files changed, 5 insertions, 11 deletions
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; |