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/CMakeLists.txt | |
| 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/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0c6cd8f50..20a208939 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -345,6 +345,22 @@ libcvc4_add_sources( theory/arith/nl/cad/projections.h theory/arith/nl/cad/variable_ordering.cpp theory/arith/nl/cad/variable_ordering.h + theory/arith/nl/ext/constraint.cpp + theory/arith/nl/ext/constraint.h + theory/arith/nl/ext/factoring_check.cpp + theory/arith/nl/ext/factoring_check.h + theory/arith/nl/ext/monomial.cpp + theory/arith/nl/ext/monomial.h + theory/arith/nl/ext/monomial_bounds_check.cpp + theory/arith/nl/ext/monomial_bounds_check.h + theory/arith/nl/ext/monomial_check.cpp + theory/arith/nl/ext/monomial_check.h + theory/arith/nl/ext/ext_state.cpp + theory/arith/nl/ext/ext_state.h + theory/arith/nl/ext/split_zero_check.cpp + theory/arith/nl/ext/split_zero_check.h + theory/arith/nl/ext/tangent_plane_check.cpp + theory/arith/nl/ext/tangent_plane_check.h theory/arith/nl/ext_theory_callback.cpp theory/arith/nl/ext_theory_callback.h theory/arith/nl/iand_solver.cpp @@ -357,18 +373,12 @@ libcvc4_add_sources( theory/arith/nl/icp/icp_solver.h theory/arith/nl/icp/intersection.cpp theory/arith/nl/icp/intersection.h - theory/arith/nl/nl_constraint.cpp - theory/arith/nl/nl_constraint.h theory/arith/nl/iand_table.cpp theory/arith/nl/iand_table.h theory/arith/nl/nl_lemma_utils.cpp theory/arith/nl/nl_lemma_utils.h theory/arith/nl/nl_model.cpp theory/arith/nl/nl_model.h - theory/arith/nl/nl_monomial.cpp - theory/arith/nl/nl_monomial.h - theory/arith/nl/nl_solver.cpp - theory/arith/nl/nl_solver.h theory/arith/nl/nonlinear_extension.cpp theory/arith/nl/nonlinear_extension.h theory/arith/nl/poly_conversion.cpp |