projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ad885db) | patch
Improve nonlinear solver (#7787)
authorGereon Kremer <gkremer@stanford.edu>
Mon, 13 Dec 2021 17:09:21 +0000 (09:09 -0800)
committerGitHub <noreply@github.com>
Mon, 13 Dec 2021 17:09:21 +0000 (17:09 +0000)
commitcb7c3b3575facae1ef9fbc433adfdf7260b379cf
tree00fea8bf9ac41754545a87648970f2665b8554f3tree
parentad885db118e388687be7f657ddc943e74a0a9601commit | diff
Improve nonlinear solver (#7787)

This PR does two things:

we remove splitting on shared values
we add variable elimination for the cad-based solver, exploiting equalities present in the input.
17 files changed:
src/CMakeLists.txt diff | blob | history
src/options/arith_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/arith/nl/cad/cdcac.cpp diff | blob | history
src/theory/arith/nl/cad/cdcac.h diff | blob | history
src/theory/arith/nl/cad/lazard_evaluation.cpp diff | blob | history
src/theory/arith/nl/cad/lazard_evaluation.h diff | blob | history
src/theory/arith/nl/cad_solver.cpp diff | blob | history
src/theory/arith/nl/cad_solver.h diff | blob | history
src/theory/arith/nl/equality_substitution.cpp [new file with mode: 0644] blob
src/theory/arith/nl/equality_substitution.h [new file with mode: 0644] blob
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/strategy.cpp diff | blob | history
src/theory/substitutions.cpp diff | blob | history
src/theory/substitutions.h diff | blob | history
test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 diff | blob | history
test/regress/regress1/nl/cos1-tc.smt2 diff | blob | history