projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8fb135c) | patch
Enable --nl-cad by default (#5345)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 27 Oct 2020 12:57:55 +0000 (13:57 +0100)
committerGitHub <noreply@github.com>
Tue, 27 Oct 2020 12:57:55 +0000 (13:57 +0100)
commitb9c38b2a878841a1288b1e2279b1ecb74727eeab
treee5416dc913ffb226b67b3f956d7918ccc28e1e5etree
parent8fb135c25038c617679f96dd40dfba3d2585380ecommit | diff
Enable --nl-cad by default (#5345)

This PR enables `--nl-cad` for QF_NRA (and QF_UFNRA) by default to improve nonlinear arithmetic solving.
Furthermore, it takes care of disabling it when libpoly is not available. It also adds a fix to the CadSolver that avoids incorrect SATs in the presence of theory combination.
src/options/arith_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/arith/nl/cad_solver.cpp diff | blob | history
test/regress/regress1/nl/iand-native-1.smt2 diff | blob | history
test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 diff | blob | history