projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e848273) | patch
Update option --nl-ext to enable/disable incremental linearization solver only (...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 25 Jun 2020 12:15:06 +0000 (07:15 -0500)
committerGitHub <noreply@github.com>
Thu, 25 Jun 2020 12:15:06 +0000 (07:15 -0500)
commit1af865f3429c0dd5910b5a8d1e12d690c3623dfa
treeac996a942c79ebb083900226a7b7c0348ef9be3atree
parente8482734bb0cd0af285464a4c50b631234ea36eecommit | diff
Update option --nl-ext to enable/disable incremental linearization solver only (#4649)

Previously, this option disabled/enabled the entire non-linear solver. This is in preparation for new CAD techniques.

I am intentionally not renaming "--nl-ext" to e.g. "--nl-inc-lin" for the sake of not breaking user configurations.

It makes some minor changes to clean the interface in a few places and to not enable the non-linear solver in linear logics.
src/options/arith_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/arith/nl/nl_model.cpp diff | blob | history
src/theory/arith/nl/nl_model.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history