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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Wed, 16 Jun 2021 21:04:09 +0000 (14:04 -0700)
committer	GitHub <noreply@github.com>
	Wed, 16 Jun 2021 21:04:09 +0000 (21:04 +0000)
commit	b8d09076cfeb124bfaa6e1c3f0f37e3df1b1b516
tree	e634a4f8d9176a238b55a51e4b18d77c69c9895d	tree
parent	0f04a6c4cf618fb5914934bac5b5c6277f07127c	commit \| diff

Make symfpu a required dependency. (#6749)

63 files changed:

CMakeLists.txt		diff \| blob \| history
INSTALL.md		diff \| blob \| history
NEWS		diff \| blob \| history
configure.sh		diff \| blob \| history
examples/api/java/FloatingPointArith.java		diff \| blob \| history
examples/api/python/floating_point.py		diff \| blob \| history
src/CMakeLists.txt		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/python/cvc5.pxd		diff \| blob \| history
src/api/python/cvc5.pxi		diff \| blob \| history
src/base/configuration.cpp		diff \| blob \| history
src/base/configuration.h		diff \| blob \| history
src/base/configuration_private.h		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/theory/fp/fp_converter.cpp		diff \| blob \| history
src/theory/fp/fp_converter.h		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/fp/theory_fp_rewriter.cpp		diff \| blob \| history
src/theory/fp/theory_fp_type_rules.cpp		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
src/util/CMakeLists.txt		diff \| blob \| history
src/util/floatingpoint_literal_symfpu.cpp		diff \| blob \| history
src/util/floatingpoint_literal_symfpu.h	[new file with mode: 0644]	blob
src/util/floatingpoint_literal_symfpu.h.in	[deleted file]	blob \| history
src/util/floatingpoint_literal_symfpu_traits.cpp		diff \| blob \| history
src/util/floatingpoint_literal_symfpu_traits.h	[new file with mode: 0644]	blob
src/util/floatingpoint_literal_symfpu_traits.h.in	[deleted file]	blob \| history
test/api/issue4889.cpp		diff \| blob \| history
test/python/unit/api/test_solver.py		diff \| blob \| history
test/python/unit/api/test_sort.py		diff \| blob \| history
test/regress/README.md		diff \| blob \| history
test/regress/regress0/fp/abs-unsound.smt2		diff \| blob \| history
test/regress/regress0/fp/abs-unsound2.smt2		diff \| blob \| history
test/regress/regress0/fp/down-cast-RNA.smt2		diff \| blob \| history
test/regress/regress0/fp/ext-rew-test.smt2		diff \| blob \| history
test/regress/regress0/fp/from_sbv.smt2		diff \| blob \| history
test/regress/regress0/fp/from_ubv.smt2		diff \| blob \| history
test/regress/regress0/fp/issue-5524.smt2		diff \| blob \| history
test/regress/regress0/fp/issue3536.smt2		diff \| blob \| history
test/regress/regress0/fp/issue3582.smt2		diff \| blob \| history
test/regress/regress0/fp/issue3619.smt2		diff \| blob \| history
test/regress/regress0/fp/issue4277-assign-func.smt2		diff \| blob \| history
test/regress/regress0/fp/issue5511.smt2		diff \| blob \| history
test/regress/regress0/fp/issue5734.smt2		diff \| blob \| history
test/regress/regress0/fp/issue6164.smt2		diff \| blob \| history
test/regress/regress0/fp/rti_3_5_bug.smt2		diff \| blob \| history
test/regress/regress0/fp/simple.smt2		diff \| blob \| history
test/regress/regress0/fp/wrong-model.smt2		diff \| blob \| history
test/regress/regress0/issue5370.smt2		diff \| blob \| history
test/regress/regress0/parser/to_fp.smt2		diff \| blob \| history
test/regress/regress1/fp/rti_3_5_bug_report.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2		diff \| blob \| history
test/regress/regress1/rr-verify/fp-arith.sy		diff \| blob \| history
test/regress/regress1/rr-verify/fp-bool.sy		diff \| blob \| history
test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy		diff \| blob \| history
test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2		diff \| blob \| history
test/regress/regress2/sygus/min_IC_1.sy		diff \| blob \| history
test/unit/api/solver_black.cpp		diff \| blob \| history
test/unit/api/sort_black.cpp		diff \| blob \| history
test/unit/theory/logic_info_white.cpp		diff \| blob \| history
test/unit/util/CMakeLists.txt		diff \| blob \| history

RSS Atom