projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bdcb629) | patch
(proof-new) Prepare nonlinear extension and nl-ext for proofs. (#5697)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 17 Dec 2020 16:12:15 +0000 (17:12 +0100)
committerGitHub <noreply@github.com>
Thu, 17 Dec 2020 16:12:15 +0000 (17:12 +0100)
commit1753106f61bca87513a84493b643e2a7e245e0f5
treed2d24cb98a66c06a3c533eaaa56ed6462c9c713btree
parentbdcb62974f553acd47fdb04f8d95725489328139commit | diff
(proof-new) Prepare nonlinear extension and nl-ext for proofs. (#5697)

This PR prepares the nonlinear extension itself and the nl-ext part for proofs. In particular

    we add a proof checker for nl-ext
    we add a CDProofSet for nl-ext
src/CMakeLists.txt diff | blob | history
src/theory/arith/nl/ext/ext_state.cpp diff | blob | history
src/theory/arith/nl/ext/ext_state.h diff | blob | history
src/theory/arith/nl/ext/proof_checker.cpp [new file with mode: 0644] blob
src/theory/arith/nl/ext/proof_checker.h [new file with mode: 0644] blob
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history