Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
s_rewriteStack in rewriter.cpp was not properly cleaned up. This commit
wraps s_rewriteStack in a std::unique_ptr to automatically free the
memory.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit makes the following minor refactors to src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h:
- Including options/bv_options.h: this is needed because this header file is being used.
- Marking all functions as inline: details in a discussion inside the PR.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This PR makes the skolem normalization in the string solver quite a bit
more aggressive by reducing more skolems to prefix and suffix skolems.
Experiments show that this PR significantly improves performance on CMU
benchmarks.
|
|
This commit adds a lemma that the value of `str.indexof(x, y, n)` must
be between -1 and `str.len(x)`.
|
|
|
|
|
|
|
|
|
|
|