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

author	Andres Noetzli <andres.noetzli@gmail.com>
	Tue, 5 Jun 2018 02:28:44 +0000 (19:28 -0700)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 5 Jun 2018 02:28:44 +0000 (21:28 -0500)
commit	af5832b414fbee30904014aaf68a7f3b277b693d
tree	5b6738aa895913c2858ff8751c573c51c6bd7b99	tree
parent	1e8a4e25751263a923a8d4cfd4d404fc0d24aa03	commit \| diff

Only enable transcendentals if logic is N[I]RAT (#2052)

41 files changed:

src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/smt2/smt2.h		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
src/theory/logic_info.h		diff \| blob \| history
test/regress/Makefile.tests		diff \| blob \| history
test/regress/regress0/nl/nta/cos-sig-value.smt2		diff \| blob \| history
test/regress/regress0/nl/nta/exp-n0.5-lb.smt2		diff \| blob \| history
test/regress/regress0/nl/nta/exp-n0.5-ub.smt2		diff \| blob \| history
test/regress/regress0/nl/nta/exp1-ub.smt2		diff \| blob \| history
test/regress/regress0/nl/nta/sin-sym.smt2		diff \| blob \| history
test/regress/regress0/nl/nta/sqrt-simple.smt2		diff \| blob \| history
test/regress/regress0/nl/nta/tan-rewrite.smt2		diff \| blob \| history
test/regress/regress0/parser/shadow_fun_symbol_all.smt2	[new file with mode: 0644]	blob
test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/NAVIGATION2.smt2		diff \| blob \| history
test/regress/regress1/nl/arctan2-expdef.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/cos-bound.smt2		diff \| blob \| history
test/regress/regress1/nl/cos1-tc.smt2		diff \| blob \| history
test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2		diff \| blob \| history
test/regress/regress1/nl/exp-4.5-lt.smt2		diff \| blob \| history
test/regress/regress1/nl/exp1-lb.smt2		diff \| blob \| history
test/regress/regress1/nl/exp_monotone.smt2		diff \| blob \| history
test/regress/regress1/nl/mirko-050417.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/sin1-deq-sat.smt2		diff \| blob \| history
test/regress/regress1/nl/sin1-lb.smt2		diff \| blob \| history
test/regress/regress1/nl/sin1-sat.smt2		diff \| blob \| history
test/regress/regress1/nl/sin1-ub.smt2		diff \| blob \| history
test/regress/regress1/nl/sin2-lb.smt2		diff \| blob \| history
test/regress/regress1/nl/sin2-ub.smt2		diff \| blob \| history
test/regress/regress1/nl/sugar-ident-2.smt2		diff \| blob \| history
test/regress/regress1/nl/sugar-ident-3.smt2		diff \| blob \| history
test/regress/regress1/nl/sugar-ident.smt2		diff \| blob \| history
test/regress/regress1/nl/tan-rewrite2.smt2		diff \| blob \| history
test/unit/theory/logic_info_white.h		diff \| blob \| history

RSS Atom