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.

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 010ec9a2e01f7878f08ee4268128a052419f7005..c5f12f4875e94902a1c5a4e462b66d07c0254bf3 100755 (executable)
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -65,7 +65,6 @@ exportConstant_cases=
 
 typerules=
 construles=
-neverconstrules=
 
 seen_theory=false
 seen_theory_builtin=false
@@ -168,12 +167,6 @@ function construle {
   case kind::$1:
 #line $lineno \"$kf\"
     return $2::computeIsConst(nodeManager, n);
-"
-  neverconstrules="${neverconstrules}
-#line $lineno \"$kf\"
-  case kind::$1:
-#line $lineno \"$kf\"
-    return false;
 "
 }
 
@@ -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 de1d5475ba2b84b1a6c19fc51b20185f84e29c8a..a8fc9d54c95c2f1ebe14f0ce1d19a59114988239 100644 (file)
--- 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 8c03cea98dd921d4e5ac1a422bcb6ed29ac479fd..bf0229bf8970e93c781fecf60b0906df121e5dec 100644 (file)
--- 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 375fbd515936cfd2f823cc57e72661d8288e4652..3ed12cf6a61953fe45f0def4831d885ffb4c7e7a 100644 (file)
--- 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 */

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 3380694e7f944f762f1e2243f08f12bab2684191..44d29d8197a7536c4a2f2154b8821b7ea0615b0e 100644 (file)
--- 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);
 }