projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bf682b9) | patch
Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NONLINEAR_M...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 5 Apr 2017 14:01:55 +0000 (09:01 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 5 Apr 2017 14:01:55 +0000 (09:01 -0500)
commitea54c6ed118928d8767c35e60d5de6c6ef877d00
treeefaf95f700378af40d92138dcf68ae947d6dd565tree
parentbf682b92e2bddcd490604f8a65c440b9c4c2f2f9commit | diff
Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver.
34 files changed:
src/options/arith_options diff | blob | history
src/theory/arith/nonlinear_extension.cpp diff | blob | history
src/theory/theory_model.cpp diff | blob | history
test/Makefile.am diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/nl/Makefile [new file with mode: 0644] blob
test/regress/regress0/nl/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/nl/bug698.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/coeff-sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/coeff-unsat-base.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/coeff-unsat.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/combine.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/disj-eval.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/dist-big.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/metitarski-1025.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/metitarski-3-4.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/metitarski_3_4_2e.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/mult-po.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/nia-wrong-tl.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/nl-help-unsat-quant.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/nl-unk-quant.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/nt-lemmas-bad.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/ones.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/poly-1025.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/quant-nl.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/red-exp.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/rewriting-sums.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/simple-mono-unsat.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/simple-mono.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/subs0-unsat-confirm.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/very-easy-sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/very-simple-unsat.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/zero-subset.smt2 [new file with mode: 0644] blob