projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 15a1c74) | patch
Eliminate rewriter from transcendental solver (#7772)
authorGereon Kremer <gkremer@stanford.edu>
Wed, 8 Dec 2021 22:48:36 +0000 (14:48 -0800)
committerGitHub <noreply@github.com>
Wed, 8 Dec 2021 22:48:36 +0000 (22:48 +0000)
commit0bcce88efaed441509c636640e19cf25a87a6be9
treed044770ed70396eb0324216594abf840783b4d62tree
parent15a1c744470514a9e1091989ad498b27cbca72f6commit | diff
Eliminate rewriter from transcendental solver (#7772)

This PR eliminates all static calls to the rewriter from the transcendental solver. We now either use the rewriter from the Env object or the theory evaluator. For this to work, the evaluator is extended to support division. In some places, the rewriting was removed altogether.
src/theory/arith/nl/transcendental/proof_checker.cpp diff | blob | history
src/theory/arith/nl/transcendental/sine_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/taylor_generator.cpp diff | blob | history
src/theory/arith/nl/transcendental/taylor_generator.h diff | blob | history
src/theory/arith/nl/transcendental/transcendental_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.h diff | blob | history
src/theory/evaluator.cpp diff | blob | history