projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4987fc9) | patch
(proof-new) Miscellaneous updates to strings from proof-new (#6557)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 18 May 2021 16:57:04 +0000 (11:57 -0500)
committerGitHub <noreply@github.com>
Tue, 18 May 2021 16:57:04 +0000 (16:57 +0000)
commitfe2cf3ad61eae43c381413a81f5d0137ba4c5903
treed657bf82eb752d1a0652bbd13afbbf0f5eec3ba3tree
parent4987fc9800830d37d22c7e4f31a3f258146cdf66commit | diff
(proof-new) Miscellaneous updates to strings from proof-new (#6557)

This includes:
(1) The type rule for `re.range` no longer insists on constant arguments, or a non-empty range. This is required for LFSC proof conversion, where re.range terms take arguments that are not (cvc5 internal) constants.
(2) Simplifications to reductions for indexof, which fixes proof checking errors in LFSC.
src/theory/strings/rewrites.cpp diff | blob | history
src/theory/strings/rewrites.h diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history
src/theory/strings/term_registry.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
src/theory/strings/theory_strings_type_rules.cpp diff | blob | history