projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a24a670) | patch
Refactor tangent plane lemmas (#5449)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 16 Nov 2020 17:51:58 +0000 (18:51 +0100)
committerGitHub <noreply@github.com>
Mon, 16 Nov 2020 17:51:58 +0000 (18:51 +0100)
commit2b504cd20b7cbbd0a3e7473162c7640907faf04d
treeff59deb3653d994e566fba02a3ef2b310c2319batree
parenta24a67080965f676335388c177d7eb8a9d3fdb13commit | diff
Refactor tangent plane lemmas (#5449)

The original lemma only proposed an implication for the tangent plane lemmas, while our implementation adds the inverse implication as well (in a somewhat verbose way).
This PR replaces this by simply constructing the equivalence.
src/theory/arith/nl/ext/tangent_plane_check.cpp diff | blob | history