projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: faa97a6) | patch
(proof-new) Proof production for term formula removal (#4687)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 27 Jul 2020 20:33:12 +0000 (15:33 -0500)
committerGitHub <noreply@github.com>
Mon, 27 Jul 2020 20:33:12 +0000 (13:33 -0700)
commitb90cfb462bde3e75c07bb14e2393ee8e4b4f4d42
tree4e7f89713008787557ae1293c6d0149e185c9b66tree
parentfaa97a6f1ee19760dfb0a79ad18c53afdff6b09acommit | diff
(proof-new) Proof production for term formula removal  (#4687)

This adds proof support in the term formula removal pass.

It also refactors this class heavily so that its interface is more intuitive and does not depend on AssertionPipeline.
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/preprocessing/passes/ite_removal.cpp diff | blob | history
src/smt/term_formula_removal.cpp diff | blob | history
src/smt/term_formula_removal.h diff | blob | history
src/theory/builtin/proof_checker.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_preprocessor.cpp diff | blob | history
src/theory/theory_preprocessor.h diff | blob | history