projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ad4f264) | patch
Use new inference manager in transcendental solver (#5022)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 17 Sep 2020 13:54:02 +0000 (15:54 +0200)
committerGitHub <noreply@github.com>
Thu, 17 Sep 2020 13:54:02 +0000 (08:54 -0500)
commit92cdcc09e9a8bece8053c3aba9e68d0028b41a8e
tree9703a100b37e45e5167d2bc7fa4a4559561e9139tree
parentad4f264cbab0236607534ecd3414ebd8a36b69e6commit | diff
Use new inference manager in transcendental solver (#5022)

This refactors the transcendental solver to add lemmas to the new inference manager instead of using the old lemma collection scheme.
src/theory/arith/inference_manager.cpp diff | blob | history
src/theory/arith/inference_manager.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/transcendental_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental_solver.h diff | blob | history