projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f5f14bd) | patch
Extend proof step buffer to optionally ensure unique conclusions (#8017)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 2 Feb 2022 14:46:48 +0000 (08:46 -0600)
committerGitHub <noreply@github.com>
Wed, 2 Feb 2022 14:46:48 +0000 (14:46 +0000)
commit908f725bf8bc70d53a7aa87e9d890f7b62a633a2
tree7ea2f57e5c929b6fd0733d582abed5ec35bda509tree
parentf5f14bdd28eeed3a66b0c627968402e5ac2c68dbcommit | diff
Extend proof step buffer to optionally ensure unique conclusions (#8017)

Fixes cvc5/cvc5-projects#439.

This extended (theory) proof step buffer with options for discarding duplicate conclusions. This option is now used in the strings theory proof construction, which may have duplication of conclusions due to purification. It simplifies some of the logic regarding popStep in this utility which is required due to the new policy.
src/proof/proof_step_buffer.cpp diff | blob | history
src/proof/proof_step_buffer.h diff | blob | history
src/proof/theory_proof_step_buffer.cpp diff | blob | history
src/proof/theory_proof_step_buffer.h diff | blob | history
src/theory/strings/infer_proof_cons.cpp diff | blob | history
src/theory/strings/infer_proof_cons.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress2/strings/proj-439-cyclic-str-ipc.smt2 [new file with mode: 0644] blob