1# z3 supports arch for which libc fenv.h provides all four macros:
2# FE_DOWNWARD, FE_TONEAREST, FE_TOWARDZERO, FE_UPWARD
3# See for example in glibc https://sourceware.org/git/glibc.git
4# git grep -E '^[[:space:]]*#[[:space:]]*define[[:space:]]+FE_(TONEAREST|UPWARD|DOWNWARD|TOWARDZERO)' sysdeps/
5config BR2_PACKAGE_Z3_ARCH_SUPPORTS
6	bool
7	default y if BR2_aarch64 || BR2_aarch64_be
8	default y if BR2_arceb || BR2_arcle
9	default y if BR2_arm || BR2_armeb
10	default y if BR2_i386
11	default y if BR2_m68k
12	# BR2_microblaze has only FE_TONEAREST
13	default y if BR2_mips || BR2_mipsel || BR2_mips64 || BR2_mips64el
14	# BR2_nios2 has only FE_TONEAREST
15	default y if BR2_or1k
16	default y if BR2_powerpc || BR2_powerpc64 || BR2_powerpc64le
17	default y if BR2_riscv
18	default y if BR2_s390x
19	# BR2_sh has only FE_{TONEAREST,TOWARDZERO}
20	default y if BR2_sparc || BR2_sparc64
21	default y if BR2_x86_64
22	# BR2_xtensa supports only uclibc which does not have fenv.h
23
24config BR2_PACKAGE_Z3
25	bool "z3"
26	depends on BR2_INSTALL_LIBSTDCPP
27	depends on BR2_TOOLCHAIN_GCC_AT_LEAST_7 # c++17
28	# z3 needs fenv.h which is not provided by uclibc
29	depends on !BR2_TOOLCHAIN_USES_UCLIBC
30	depends on BR2_PACKAGE_Z3_ARCH_SUPPORTS
31	help
32	  Z3, also known as the Z3 Theorem Prover, is a cross-platform
33	  satisfiability modulo theories (SMT) solver.
34
35	  https://github.com/Z3Prover/z3
36
37if BR2_PACKAGE_Z3
38
39config BR2_PACKAGE_Z3_PYTHON
40	bool "Python bindings"
41	depends on BR2_PACKAGE_PYTHON3
42	select BR2_PACKAGE_PYTHON3_PYEXPAT # runtime
43	select BR2_PACKAGE_PYTHON_SETUPTOOLS # runtime
44
45endif
46