projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 865d1ee) | patch
(proof-new) Proofs for regular expression elimination (#5361)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 30 Nov 2020 15:41:37 +0000 (09:41 -0600)
committerGitHub <noreply@github.com>
Mon, 30 Nov 2020 15:41:37 +0000 (09:41 -0600)
commitac6150d7992b5dd1cace8d8d6e0d308e4a741c12
treee8379438a90fdb24539578c04688f66d41ba7905tree
parent865d1ee48de8e4a21d1e97c707be46c34918367dcommit | 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.
src/expr/proof_rule.h diff | blob | history
src/theory/strings/proof_checker.cpp diff | blob | history
src/theory/strings/regexp_elim.cpp diff | blob | history
src/theory/strings/regexp_elim.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history