projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6f5e85a) | patch
Fix LFSC proof construction for concat clash of sequences (#8739)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 17 May 2022 19:16:56 +0000 (14:16 -0500)
committerGitHub <noreply@github.com>
Tue, 17 May 2022 19:16:56 +0000 (19:16 +0000)
commit55392bd73a7af71411a3157520b758623f2f4723
treeaf5483d9df1471b2d5735ff2c695a62ab85c79cftree
parent6f5e85af48265e6fc478cb695bb40ab9ce6661d5commit | diff
Fix LFSC proof construction for concat clash of sequences (#8739)

Changes the internal proof calculus to require an explicit disequality between character constants for clashing sequences.

Makes it so that the disequality is expanded prior to proof post-processing, so that character clashing is properly expanded as it may require rewriting.
src/proof/lfsc/lfsc_post_processor.cpp diff | blob | history
src/proof/proof_rule.h diff | blob | history
src/theory/strings/infer_proof_cons.cpp diff | blob | history
src/theory/strings/proof_checker.cpp diff | blob | history
test/regress/cli/regress0/seq/seq-types.smt2 diff | blob | history