projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b0dd5a3) | patch
Split NlSolver in multiple subsolvers (#5315)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 28 Oct 2020 18:35:35 +0000 (19:35 +0100)
committerGitHub <noreply@github.com>
Wed, 28 Oct 2020 18:35:35 +0000 (13:35 -0500)
commita61f77fd58c8da0f38de4d094258f78f71774383
tree96b4f554fec6802b32eb69804d7c3e7169dd0a45tree
parentb0dd5a3adc67d72a08ca9d8d3de208840a1001a3commit | 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.
25 files changed:
src/CMakeLists.txt diff | blob | history
src/theory/arith/nl/ext/constraint.cpp [new file with mode: 0644] blob
src/theory/arith/nl/ext/constraint.h [new file with mode: 0644] blob
src/theory/arith/nl/ext/ext_state.cpp [new file with mode: 0644] blob
src/theory/arith/nl/ext/ext_state.h [new file with mode: 0644] blob
src/theory/arith/nl/ext/factoring_check.cpp [new file with mode: 0644] blob
src/theory/arith/nl/ext/factoring_check.h [new file with mode: 0644] blob
src/theory/arith/nl/ext/monomial.cpp [new file with mode: 0644] blob
src/theory/arith/nl/ext/monomial.h [new file with mode: 0644] blob
src/theory/arith/nl/ext/monomial_bounds_check.cpp [new file with mode: 0644] blob
src/theory/arith/nl/ext/monomial_bounds_check.h [new file with mode: 0644] blob
src/theory/arith/nl/ext/monomial_check.cpp [new file with mode: 0644] blob
src/theory/arith/nl/ext/monomial_check.h [new file with mode: 0644] blob
src/theory/arith/nl/ext/split_zero_check.cpp [new file with mode: 0644] blob
src/theory/arith/nl/ext/split_zero_check.h [new file with mode: 0644] blob
src/theory/arith/nl/ext/tangent_plane_check.cpp [new file with mode: 0644] blob
src/theory/arith/nl/ext/tangent_plane_check.h [new file with mode: 0644] blob
src/theory/arith/nl/nl_constraint.cpp [deleted file] blob | history
src/theory/arith/nl/nl_constraint.h [deleted file] blob | history
src/theory/arith/nl/nl_monomial.cpp [deleted file] blob | history
src/theory/arith/nl/nl_monomial.h [deleted file] blob | history
src/theory/arith/nl/nl_solver.cpp [deleted file] blob | history
src/theory/arith/nl/nl_solver.h [deleted file] blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.h diff | blob | history