projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f1a65be) | patch
Improve integration of CAD with nl-Ext (#6542)
authorGereon Kremer <nafur42@gmail.com>
Mon, 17 May 2021 15:18:57 +0000 (17:18 +0200)
committerGitHub <noreply@github.com>
Mon, 17 May 2021 15:18:57 +0000 (15:18 +0000)
commit63281fbfe093b1d5e375a378bb59761f77256d08
treeea4e7dc183ddfb23709c92f74b4d35f581ad8d32tree
parentf1a65bef2675495f09603901a7166f20221b0449commit | diff
Improve integration of CAD with nl-Ext (#6542)

This PR improves the integration of the CAD solver with the nl-ext solver in a simple way: we simply use a few of the simple linearization lemmas in combination with CAD by default, significantly improving the performance on QF_NRA.
58 files changed:
src/options/arith_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/strategy.cpp diff | blob | history
test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 diff | blob | history
test/regress/regress0/nl/coeff-sat.smt2 diff | blob | history
test/regress/regress0/nl/issue3003.smt2 diff | blob | history
test/regress/regress0/nl/issue5726-downpolys.smt2 diff | blob | history
test/regress/regress0/nl/issue5726-sqfactor.smt2 diff | blob | history
test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 diff | blob | history
test/regress/regress0/nl/mult-po.smt2 diff | blob | history
test/regress/regress0/nl/nia-wrong-tl.smt2 diff | blob | history
test/regress/regress0/nl/nta/cos-sig-value.smt2 diff | blob | history
test/regress/regress0/nl/nta/real-pi.smt2 diff | blob | history
test/regress/regress0/nl/nta/sin-sym.smt2 diff | blob | history
test/regress/regress0/nl/nta/tan-rewrite.smt2 diff | blob | history
test/regress/regress0/nl/real-div-ufnra.smt2 diff | blob | history
test/regress/regress0/nl/subs0-unsat-confirm.smt2 diff | blob | history
test/regress/regress0/nl/very-easy-sat.smt2 diff | blob | history
test/regress/regress0/nl/very-simple-unsat.smt2 diff | blob | history
test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 diff | blob | history
test/regress/regress1/nl/arrowsmith-050317.smt2 diff | blob | history
test/regress/regress1/nl/bad-050217.smt2 diff | blob | history
test/regress/regress1/nl/bug698.smt2 diff | blob | history
test/regress/regress1/nl/coeff-unsat-base.smt2 diff | blob | history
test/regress/regress1/nl/coeff-unsat.smt2 diff | blob | history
test/regress/regress1/nl/combine.smt2 diff | blob | history
test/regress/regress1/nl/cos-bound.smt2 diff | blob | history
test/regress/regress1/nl/cos1-tc.smt2 diff | blob | history
test/regress/regress1/nl/disj-eval.smt2 diff | blob | history
test/regress/regress1/nl/dist-big.smt2 diff | blob | history
test/regress/regress1/nl/div-mod-partial.smt2 diff | blob | history
test/regress/regress1/nl/exp-soundness-bound.smt2 diff | blob | history
test/regress/regress1/nl/exp_monotone.smt2 diff | blob | history
test/regress/regress1/nl/metitarski-1025.smt2 diff | blob | history
test/regress/regress1/nl/metitarski-3-4.smt2 diff | blob | history
test/regress/regress1/nl/metitarski_3_4_2e.smt2 diff | blob | history
test/regress/regress1/nl/mirko-050417.smt2 diff | blob | history
test/regress/regress1/nl/nl-help-unsat-quant.smt2 diff | blob | history
test/regress/regress1/nl/nl-unk-quant.smt2 diff | blob | history
test/regress/regress1/nl/ones.smt2 diff | blob | history
test/regress/regress1/nl/poly-1025.smt2 diff | blob | history
test/regress/regress1/nl/quant-nl.smt2 diff | blob | history
test/regress/regress1/nl/red-exp.smt2 diff | blob | history
test/regress/regress1/nl/rewriting-sums.smt2 diff | blob | history
test/regress/regress1/nl/shifting.smt2 diff | blob | history
test/regress/regress1/nl/shifting2.smt2 diff | blob | history
test/regress/regress1/nl/simple-mono-unsat.smt2 diff | blob | history
test/regress/regress1/nl/simple-mono.smt2 diff | blob | history
test/regress/regress1/nl/sin-compare-across-phase.smt2 diff | blob | history
test/regress/regress1/nl/sin-compare.smt2 diff | blob | history
test/regress/regress1/nl/sin-init-tangents.smt2 diff | blob | history
test/regress/regress1/nl/sin-sign.smt2 diff | blob | history
test/regress/regress1/nl/sin-sym2.smt2 diff | blob | history
test/regress/regress1/nl/tan-rewrite2.smt2 diff | blob | history
test/regress/regress1/nl/zero-subset.smt2 diff | blob | history
test/regress/regress2/nl/nt-lemmas-bad.smt2 diff | blob | history
test/regress/regress4/siegel-nl-bases.smt2 diff | blob | history