Simple optimizations for the core rewriter (#3569)

In some SyGuS applications, the bottleneck is the rewriter.  This PR makes a few simple optimizations to the core rewriter, namely:
(1) Minimize the overhead of `theoryOf` calls, which take about 10-15% of the runtime in the rewriter.  This PR avoids many calls to `theoryOf` by the observation that nodes with zero children never rewrite, hence we can return the node itself immediately.  Furthermore, the `theoryOf` call can be simplified to hardcode the context under which we were using it: get the theory (based on type) where due to the above, we can assume that the node is not a variable.
The one (negligible) change in behavior due to this change is that nodes with more than one child for which `isConst` returns true (this is limited to the case of `APPLY_CONSTRUCTOR` in datatypes) lookup their theory based on the Kind, not their type, which should always be the same theory unless a theory had a way of constructing constant nodes of a type belonging to another theory.
(2) Remove deprecated infrastrastructure for a "neverIsConst" function, which was adding about a 1% of the runtime for some SyGuS benchmarks.

This makes SyGuS for some sets of benchmarks roughly 3% faster.

1 files changed, 16 insertions, 1 deletions

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 3380694e7..44d29d819 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -28,8 +28,17 @@ using namespace std;
 namespace CVC4 {
 namespace theory {
 
+// Note that this function is a simplified version of Theory::theoryOf for
+// (type-based) theoryOfMode. We expand and simplify it here for the sake of
+// efficiency.
 static TheoryId theoryOf(TNode node) {
-  return Theory::theoryOf(THEORY_OF_TYPE_BASED, node);
+  if (node.getKind() == kind::EQUAL)
+  {
+    // Equality is owned by the theory that owns the domain
+    return Theory::theoryOf(node[0].getType());
+  }
+  // Regular nodes are owned by the kind
+  return kindToTheoryId(node.getKind());
 }
 
 /**
@@ -72,6 +81,12 @@ struct RewriteStackElement {
 };
 
 Node Rewriter::rewrite(TNode node) {
+  if (node.getNumChildren() == 0)
+  {
+    // Nodes with zero children should never change via rewriting. We return
+    // eagerly for the sake of efficiency here.
+    return node;
+  }
   Rewriter& rewriter = getInstance();
   return rewriter.rewriteTo(theoryOf(node), node);
 }