projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e329083) | patch
(proof-new) Make nl-ext factoring lemmas proof producing. (#5698)
authorGereon Kremer <gkremer@stanford.edu>
Mon, 21 Dec 2020 16:20:23 +0000 (17:20 +0100)
committerGitHub <noreply@github.com>
Mon, 21 Dec 2020 16:20:23 +0000 (17:20 +0100)
commit708c5a14bca031100b05000ddae65a9828d76da0
tree00377865533d680d6530b0d21a78074eb4d6cb4ctree
parente32908362d75acad3cce28cf725eb781d1556e6fcommit | diff
(proof-new) Make nl-ext factoring lemmas proof producing. (#5698)

This PR adds proofs for the lemmas from the nonlinear factoring check.
src/theory/arith/nl/ext/factoring_check.cpp diff | blob | history
src/theory/arith/nl/ext/factoring_check.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history