diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-30 09:41:37 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-30 09:41:37 -0600 |
| commit | ac6150d7992b5dd1cace8d8d6e0d308e4a741c12 (patch) | |
| tree | e8379438a90fdb24539578c04688f66d41ba7905 /src/expr/CMakeLists.txt | |
| parent | 865d1ee48de8e4a21d1e97c707be46c34918367d (diff) | |
(proof-new) Proofs for regular expression elimination (#5361)
Adds support for proofs for regular expression elimination in TheoryStrings::ppRewrite via a coarse-grained rule RE_ELIM.
This rule is updated by this PR to distinguish whether we apply aggressive elimination. Aggressive elimination is not currently supported, since it is non-deterministic due to generating fresh BOUND_VARIABLE.
Diffstat (limited to 'src/expr/CMakeLists.txt')
0 files changed, 0 insertions, 0 deletions