projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 05d1181) | patch
Enable NL tangent planes by default (#8233)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 5 Mar 2022 00:47:13 +0000 (18:47 -0600)
committerGitHub <noreply@github.com>
Sat, 5 Mar 2022 00:47:13 +0000 (00:47 +0000)
commite099e59f544d204ff74b2a8f26994795a2d6fb3e
tree7098e249d235f8f93a7d42581bc74d1826f1f251tree
parent05d11815c049d1145884d510196e4e16a88931a0commit | diff
Enable NL tangent planes by default (#8233)

Fixes cvc5/cvc5-projects#215
Fixes cvc5/cvc5-projects#291
Fixes cvc5/cvc5-projects#292
Fixes cvc5/cvc5-projects#294
Fixes cvc5/cvc5-projects#297

Previously the concern was that this would interfere with e.g. quantifiers + non-linear. However, our strategy is now fair wrt other theories as we send lemmas at LAST_CALL effort, and is properly restricted by the nl-ext mode.

Moreover, this option increases our ability to solve problems (instead of saying "unknown") significantly, even for quantified logics like UFNIA.
src/options/arith_options.toml diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 diff | blob | history
test/regress/regress1/nl/proj-issue215.smt2 [new file with mode: 0644] blob
test/regress/regress1/nl/proj-issue279.smt2 [new file with mode: 0644] blob
test/regress/regress1/nl/proj-issue291.smt2 [new file with mode: 0644] blob
test/regress/regress1/nl/proj-issue292.smt2 [new file with mode: 0644] blob
test/regress/regress1/nl/proj-issue294.smt2 [new file with mode: 0644] blob
test/regress/regress1/nl/proj-issue297.smt2 [new file with mode: 0644] blob
test/regress/regress1/nl/proj-issue302.smt2 [new file with mode: 0644] blob