projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9b099b7) | patch
Add proof for split zero check. (#5699)
authorGereon Kremer <gkremer@stanford.edu>
Fri, 18 Dec 2020 07:26:55 +0000 (08:26 +0100)
committerGitHub <noreply@github.com>
Fri, 18 Dec 2020 07:26:55 +0000 (08:26 +0100)
commit0ae11d1abec9017784eefa2252d8e8ea7dfb4f74
treeeaca05442c315dcd9956047ebb6f5eaa63c56102tree
parent9b099b715cec0dc60048fdc64b4d61b977d14096commit | diff
Add proof for split zero check. (#5699)

This PR adds a proof for the nl-ext check to split at zero. As we can use the SPLIT rule, this requires no new proof rule.
src/theory/arith/nl/ext/split_zero_check.cpp diff | blob | history
src/theory/arith/nl/ext/split_zero_check.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history