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/node.cpp | |
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/node.cpp')
-rw-r--r-- | src/expr/node.cpp | 4 |
1 files changed, 0 insertions, 4 deletions
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<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; |