projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0ae11d1) | patch
(proof-new) Add proof for tangent plane lemmas (#5700)
authorGereon Kremer <gkremer@stanford.edu>
Fri, 18 Dec 2020 07:59:43 +0000 (08:59 +0100)
committerGitHub <noreply@github.com>
Fri, 18 Dec 2020 07:59:43 +0000 (08:59 +0100)
commit8a2a526b2dab5d6efaf1435afcc1b7be113a86bf
tree135adecb0499c819ccec965721261a891be33396tree
parent0ae11d1abec9017784eefa2252d8e8ea7dfb4f74commit | diff
(proof-new) Add proof for tangent plane lemmas (#5700)

This PR adds a proof for the tangent plane lemmas from nl-ext.
As this lemma uses some insight about the tangent plane of a multiplication term, this PR adds a new proof rule.
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/theory/arith/nl/ext/tangent_plane_check.cpp diff | blob | history