Simple optimizations for the core rewriter (#3569)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 15 Dec 2019 07:45:27 +0000 (01:45 -0600)
committerAndres Noetzli <andres.noetzli@gmail.com>
Sun, 15 Dec 2019 07:45:27 +0000 (23:45 -0800)
commit52b216f385c0b1c1a9bb0ab8541683d9e13a7f46
tree061f8e67ff0c9028b678575b4a34b7dc428a79a6
parentc0a7095f13547ac0c0d4c92670000ca875b7c349
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
src/expr/node.cpp
src/expr/type_checker.h
src/expr/type_checker_template.cpp
src/theory/rewriter.cpp