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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 7 Feb 2018 15:12:59 +0000 (09:12 -0600)
committer	GitHub <noreply@github.com>
	Wed, 7 Feb 2018 15:12:59 +0000 (09:12 -0600)
commit	0533b9009d23a39bcc78ef85d6e98b62ef304351
tree	e32b823d509e1c9b54dfe4230d075b8396f48b9c	tree
parent	82066be04ce068b59b24526fbc8c9b4188503cae	commit \| diff

Add remaining transcendental functions (#1551)

15 files changed:

src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/kinds		diff \| blob \| history
src/theory/arith/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nonlinear_extension.h		diff \| blob \| history
src/theory/arith/normal_form.cpp		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
test/regress/regress0/nl/Makefile.am		diff \| blob \| history
test/regress/regress0/nl/nta/sugar-ident-2.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sugar-ident-3.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sugar-ident.smt2	[new file with mode: 0644]	blob