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.

4 files changed, 0 insertions, 32 deletions

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 010ec9a2e..c5f12f487 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -65,7 +65,6 @@ exportConstant_cases=
 
 typerules=
 construles=
-neverconstrules=
 
 seen_theory=false
 seen_theory_builtin=false
@@ -169,12 +168,6 @@ function construle {
 #line $lineno \"$kf\"
     return $2::computeIsConst(nodeManager, n);
 "
-  neverconstrules="${neverconstrules}
-#line $lineno \"$kf\"
-  case kind::$1:
-#line $lineno \"$kf\"
-    return false;
-"
 }
 
 function sort {
@@ -311,7 +304,6 @@ for var in \
     typechecker_includes \
     typerules \
     construles \
-    neverconstrules \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index de1d5475b..a8fc9d54c 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -91,10 +91,6 @@ bool NodeTemplate<ref_count>::isConst() const {
     Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
     return false;
   default:
-    if(expr::TypeChecker::neverIsConst(NodeManager::currentNM(), *this)){
-      Debug("isConst") << "Node::isConst() returning false, the kind is never const" << std::endl;
-      return false;
-    }
     if(getAttribute(IsConstComputedAttr())) {
       bool bval = getAttribute(IsConstAttr());
       Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index 8c03cea98..bf0229bf8 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -33,8 +33,6 @@ public:
 
  static bool computeIsConst(NodeManager* nodeManager, TNode n);
 
- static bool neverIsConst(NodeManager* nodeManager, TNode n);
-
 };/* class TypeChecker */
 
 }/* CVC4::expr namespace */
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 375fbd515..3ed12cf6a 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -77,23 +77,5 @@ ${construles}
 
 }/* TypeChecker::computeIsConst */
 
-bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n)
-{
-  Assert(n.getMetaKind() == kind::metakind::OPERATOR
-         || n.getMetaKind() == kind::metakind::PARAMETERIZED
-         || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
-
-  switch(n.getKind()) {
-${neverconstrules}
-
-#line 90 "${template}"
-
-    default:;
-  }
-
-  return true;
-
-}/* TypeChecker::neverIsConst */
-
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */