diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-20 10:05:05 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-20 10:05:05 -0800 |
commit | 4ef569cfd91bccabb6e704dcc4ecd55a9fa0a8ea (patch) | |
tree | e9853ed7f3731e9866d65f441e1b7293edb29168 /test/regress/regress0/nl | |
parent | 98962b4d3037c381fadc41e19f7ae9a1ddd82b7b (diff) |
Unrecursified and merged bv::utils::is(Core|Equality)Term. (#1605)
This unrecursifies and merges bv::utils::isCoreTerm and bv::utils::isEqualityTerm to avoid
code duplication.
In the best case, the recursive implementation visits less nodes. This can be achieved with
the non-recursive implementation, however, at the cost of increased code complexity.
In practice, on QF_BV the new implementation slightly improves performance.
Tested against the recursive implementation with a temporary assertion on regression
tests (bv::utils::isCoreTerm was tested with --bv-eq-slicer=auto).
Further tested on QF_BV with a TO of 300s (slight performance improvement).
Diffstat (limited to 'test/regress/regress0/nl')
0 files changed, 0 insertions, 0 deletions