projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4669bb1) | patch
Remove quadratic solving in NlModel (#7542)
authorGereon Kremer <nafur42@gmail.com>
Fri, 5 Nov 2021 14:15:49 +0000 (07:15 -0700)
committerGitHub <noreply@github.com>
Fri, 5 Nov 2021 14:15:49 +0000 (14:15 +0000)
commit71cab467df779fc1a52e8a5f981132f49d9d3182
treee375077c42c8c4a4388147fa282d8cb551596f0etree
parent4669bb1ab2fce322cd8e3e172e57f0aa3006e1d7commit | diff
Remove quadratic solving in NlModel (#7542)

This PR removes obsolete code from NlModel concerned with solving quadratic equations. This code is only used on nonlinear real problems where the cad solver is not used.
src/theory/arith/nl/nl_model.cpp diff | blob | history
src/theory/arith/nl/nl_model.h diff | blob | history
test/regress/regress0/nl/sqrt2-value.smt2 diff | blob | history
test/regress/regress1/quantifiers/issue6607-witness-te.smt2 diff | blob | history