From 52b216f385c0b1c1a9bb0ab8541683d9e13a7f46 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 15 Dec 2019 01:45:27 -0600 Subject: [PATCH] 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. --- src/expr/mkexpr | 8 -------- src/expr/node.cpp | 4 ---- src/expr/type_checker.h | 2 -- src/expr/type_checker_template.cpp | 18 ------------------ src/theory/rewriter.cpp | 17 ++++++++++++++++- 5 files changed, 16 insertions(+), 33 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 @@ -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 de1d5475b..a8fc9d54c 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -91,10 +91,6 @@ bool NodeTemplate::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 */ 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); } -- 2.30.2