projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 27413a4) | patch
(proof-new) Improve interfaces to proof generators (#4803)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 Aug 2020 19:48:31 +0000 (14:48 -0500)
committerGitHub <noreply@github.com>
Wed, 12 Aug 2020 19:48:31 +0000 (14:48 -0500)
commit2174ab36023326cd998565bbf35d31c38bc10594
treea61a1cb1cc00faa1339adf315fd4037b0ca08b1atree
parent27413a45e28001f6155d529a59d679556cdc011ecommit | diff
(proof-new) Improve interfaces to proof generators (#4803)

This includes configurable naming and a caching policy for term conversion proof generator.

Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.
16 files changed:
src/expr/lazy_proof.cpp diff | blob | history
src/expr/lazy_proof.h diff | blob | history
src/expr/proof.cpp diff | blob | history
src/expr/proof.h diff | blob | history
src/expr/proof_generator.cpp diff | blob | history
src/expr/proof_generator.h diff | blob | history
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/expr/term_conversion_proof_generator.cpp diff | blob | history
src/expr/term_conversion_proof_generator.h diff | blob | history
src/options/smt_options.toml diff | blob | history
src/smt/term_formula_removal.cpp diff | blob | history
src/smt/term_formula_removal.h diff | blob | history
src/smt/witness_form.cpp diff | blob | history
src/theory/eager_proof_generator.cpp diff | blob | history
src/theory/eager_proof_generator.h diff | blob | history