From 52b216f385c0b1c1a9bb0ab8541683d9e13a7f46 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 15 Dec 2019 01:45:27 -0600 Subject: 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 -------- 1 file changed, 8 deletions(-) (limited to 'src/expr/mkexpr') 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 -- cgit v1.2.3