git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 24 Nov 2017 12:44:46 +0000 (06:44 -0600)
committer	GitHub <noreply@github.com>
	Fri, 24 Nov 2017 12:44:46 +0000 (06:44 -0600)
commit	bb095659fb12e3733a73f1be31769ff5b5eb6055
tree	d9e6e40196e80c0bce9983ed00791df32cfd7396	tree
parent	612509379a1417f8d4a5e001ff143ba819f5516f	commit \| diff

Implement tangent and secant planes for transcendental functions (#1401)

15 files changed:

src/options/arith_options		diff \| blob \| history
src/theory/arith/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nonlinear_extension.h		diff \| blob \| history
test/regress/regress0/nl/Makefile.am		diff \| blob \| history
test/regress/regress0/nl/nta/NAVIGATION2.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/exp-4.5-lt.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/exp-n0.5-lb.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/exp-n0.5-ub.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/exp1-lb.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/exp1-ub.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sin1-lb.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sin1-ub.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sin2-lb.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sin2-ub.smt2	[new file with mode: 0644]	blob