diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-10-28 19:35:35 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-28 13:35:35 -0500 |
| commit | a61f77fd58c8da0f38de4d094258f78f71774383 (patch) | |
| tree | 96b4f554fec6802b32eb69804d7c3e7169dd0a45 /src/theory/arith/nl/nonlinear_extension.h | |
| parent | b0dd5a3adc67d72a08ca9d8d3de208840a1001a3 (diff) | |
Split NlSolver in multiple subsolvers (#5315)
The NlSolver started as one place for nonlinear reasoning, but has grown significantly since. This PR splits the NlSolver class into multiple smaller classes.
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.h')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 25 |
1 files changed, 19 insertions, 6 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index cf45942c8..cd26a027f 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -28,12 +28,16 @@ #include "expr/node.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad_solver.h" +#include "theory/arith/nl/ext/factoring_check.h" +#include "theory/arith/nl/ext/monomial_bounds_check.h" +#include "theory/arith/nl/ext/monomial_check.h" +#include "theory/arith/nl/ext/split_zero_check.h" +#include "theory/arith/nl/ext/tangent_plane_check.h" #include "theory/arith/nl/ext_theory_callback.h" #include "theory/arith/nl/iand_solver.h" #include "theory/arith/nl/icp/icp_solver.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" -#include "theory/arith/nl/nl_solver.h" #include "theory/arith/nl/stats.h" #include "theory/arith/nl/strategy.h" #include "theory/arith/nl/transcendental_solver.h" @@ -256,12 +260,21 @@ class NonlinearExtension * transcendental functions. */ TranscendentalSolver d_trSlv; - /** The nonlinear extension object - * - * This is the subsolver responsible for running the procedure for - * constraints involving nonlinear mulitplication, Cimatti et al., TACAS 2017. + /** + * Holds common lookup data for the checks implemented in the "nl-ext" + * solvers (from Cimatti et al., TACAS 2017). */ - NlSolver d_nlSlv; + ExtState d_extState; + /** Solver for factoring lemmas. */ + FactoringCheck d_factoringSlv; + /** Solver for lemmas about monomial bounds. */ + MonomialBoundsCheck d_monomialBoundsSlv; + /** Solver for lemmas about monomials. */ + MonomialCheck d_monomialSlv; + /** Solver for lemmas that split multiplication at zero. */ + SplitZeroCheck d_splitZeroSlv; + /** Solver for tangent plane lemmas. */ + TangentPlaneCheck d_tangentPlaneSlv; /** The CAD-based solver */ CadSolver d_cadSlv; /** The ICP-based solver */ |