diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-15 01:45:27 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-14 23:45:27 -0800 |
| commit | 52b216f385c0b1c1a9bb0ab8541683d9e13a7f46 (patch) | |
| tree | 061f8e67ff0c9028b678575b4a34b7dc428a79a6 /src/expr/mkexpr | |
| parent | c0a7095f13547ac0c0d4c92670000ca875b7c349 (diff) | |
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.
Diffstat (limited to 'src/expr/mkexpr')
| -rwxr-xr-x | src/expr/mkexpr | 8 |
1 files changed, 0 insertions, 8 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 |