projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6fdac54) | patch
Split initial exp lemma into separate lemmas. (#5622)
authorGereon Kremer <nafur42@gmail.com>
Wed, 9 Dec 2020 05:38:15 +0000 (06:38 +0100)
committerGitHub <noreply@github.com>
Wed, 9 Dec 2020 05:38:15 +0000 (23:38 -0600)
commit1eac626e6c23dca3a3bb92e0a62289aecb61fc02
tree0501228cac7e2dac226b42cfb9a635b2d9fd8685tree
parent6fdac54fe0153bb17eca1c01eb5bd45b9418c596commit | diff
Split initial exp lemma into separate lemmas. (#5622)

This PR refactors the initial lemmas for the exponential function, very similar to the sine lemmas.
src/theory/arith/nl/transcendental/exponential_solver.cpp diff | blob | history