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

author	ajreynol <andrew.j.reynolds@gmail.com>
	Mon, 10 Jul 2017 21:22:19 +0000 (16:22 -0500)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Mon, 10 Jul 2017 21:22:26 +0000 (16:22 -0500)
commit	2c0482cfb9b8164670cf56187e127d38c5d05bcf
tree	804f7806944b9175fdaea8cc919566ca302ddf09	tree
parent	0e513c05b2e0ae3b8e2d08514ccb8007258f963b	commit \| diff

Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.

35 files changed:

src/options/arith_options		diff \| blob \| history
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/arith_rewriter.h		diff \| blob \| history
src/theory/arith/congruence_manager.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_type_rules.h		diff \| blob \| history
test/regress/regress0/nl/Makefile.am		diff \| blob \| history
test/regress/regress0/nl/nta/arrowsmith-050317.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/bad-050217.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/cos-bound.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/cos-sig-value.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/dumortier-050317.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/exp_monotone.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/shifting.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/shifting2.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sin-compare-across-phase.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sin-compare.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sin-init-tangents.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sin-sign.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sin-sym.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/sin-sym2.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/tan-rewrite.smt2	[new file with mode: 0644]	blob
test/regress/regress0/nl/nta/tan-rewrite2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/Makefile.am		diff \| blob \| history
test/regress/regress1/nl/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress1/nl/mirko-050417.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/siegel-nl-bases.smt2	[new file with mode: 0644]	blob

RSS Atom