diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-11-25 01:07:42 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-24 18:07:42 -0600 |
| commit | 2576297452114b9bc916c84a748a5337e595a323 (patch) | |
| tree | 8261a6df31098c4b1963b45f542bdcb85d71def1 /src/theory/arith/nl/nonlinear_extension.h | |
| parent | 07c7b873c5c2ee81cb2672428ca1de0d75bb1ae8 (diff) | |
Refactor transcendental solver (#5514)
The transcendental solver has grown over time, and a refactoring was due.
This PR splits the transcendental solver into five components:
a utility to compute taylor approximations
a common state for transcendental solvers
a solver for exponential function
a solver for sine function
a solver that wraps everything to a transcendental solver.
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.h')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 21b978a55..b563384a5 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -38,7 +38,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/stats.h" #include "theory/arith/nl/strategy.h" -#include "theory/arith/nl/transcendental_solver.h" +#include "theory/arith/nl/transcendental/transcendental_solver.h" #include "theory/ext_theory.h" #include "theory/uf/equality_engine.h" @@ -253,7 +253,7 @@ class NonlinearExtension * This is the subsolver responsible for running the procedure for * transcendental functions. */ - TranscendentalSolver d_trSlv; + transcendental::TranscendentalSolver d_trSlv; /** * Holds common lookup data for the checks implemented in the "nl-ext" * solvers (from Cimatti et al., TACAS 2017). |