projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cf4b6ea) | patch
Fix issues related to proofs of lemmas with duplicate conclusions in strings (#7366)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 15 Oct 2021 12:24:28 +0000 (07:24 -0500)
committerGitHub <noreply@github.com>
Fri, 15 Oct 2021 12:24:28 +0000 (12:24 +0000)
commitb4469530d2f6de599ddf7207a1914b88be49de5b
treec89ea3bb1abd21faa609986dd63aebcf9a9ebb07tree
parentcf4b6eab2f451a29cf0ca3b94b02c32c22b273a4commit | diff
Fix issues related to proofs of lemmas with duplicate conclusions in strings (#7366)

This makes string proof construction more robust by maintaining two separate proof inference constructors, one for facts and one for lemmas/conflicts. This avoids issues where 2 lemmas with the same conclusion (but possibly different explanations) are added in the same call to check.

This fixes one of the two issues related to proofs for #6973.
src/theory/strings/infer_proof_cons.cpp diff | blob | history
src/theory/strings/infer_proof_cons.h diff | blob | history
src/theory/strings/inference_manager.cpp diff | blob | history
src/theory/strings/inference_manager.h diff | blob | history
src/theory/strings/regexp_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 [new file with mode: 0644] blob