projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7d4c7be) | patch
(proof-new) Setup proof infrastructure for transcendental solver (#5703)
authorGereon Kremer <gkremer@stanford.edu>
Fri, 18 Dec 2020 17:11:51 +0000 (18:11 +0100)
committerGitHub <noreply@github.com>
Fri, 18 Dec 2020 17:11:51 +0000 (11:11 -0600)
commit39df95de07a85121f5f12404afcaae48d90e0a67
treeef98badf202e22a6357cc2717d5e21780168549ctree
parent7d4c7be8cbe1ac3b68c3bb5e2b08143f8324b5a1commit | diff
(proof-new) Setup proof infrastructure for transcendental solver (#5703)

This PR introduces the infrastructure for adding proofs to the transcendental solver:

a CDProofSet to easily create new proofs
a proof checker
src/CMakeLists.txt diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/transcendental/proof_checker.cpp [new file with mode: 0644] blob
src/theory/arith/nl/transcendental/proof_checker.h [new file with mode: 0644] blob
src/theory/arith/nl/transcendental/transcendental_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_solver.h diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.h diff | blob | history