projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 060eedc) | patch
(proof-new) Generalize single step helper in eager proof generator (#5046)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 9 Sep 2020 20:11:01 +0000 (15:11 -0500)
committerGitHub <noreply@github.com>
Wed, 9 Sep 2020 20:11:01 +0000 (15:11 -0500)
commit9a939deab1a788b29b573ae7fb72a6088a1d7edf
treed403a57bac514c9e1320cdc171597c977b952ee0tree
parent060eedcd5fdb0316d323c4528402034629285b97commit | diff
(proof-new) Generalize single step helper in eager proof generator (#5046)

This allows single step proofs to have premises, closed by a SCOPE. This will be useful for array lemmas.
src/theory/combination_care_graph.cpp diff | blob | history
src/theory/eager_proof_generator.cpp diff | blob | history
src/theory/eager_proof_generator.h diff | blob | history
src/theory/strings/term_registry.cpp diff | blob | history