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 /src/theory/arith/nonlinear_extension.cpp | |
| 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 'src/theory/arith/nonlinear_extension.cpp')
0 files changed, 0 insertions, 0 deletions