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/theory/rewriter.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/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 17 |
1 files changed, 16 insertions, 1 deletions
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); } |