# z3 supports arch for which libc fenv.h provides all four macros:
# FE_DOWNWARD, FE_TONEAREST, FE_TOWARDZERO, FE_UPWARD
# See for example in glibc https://sourceware.org/git/glibc.git
# git grep -E '^[[:space:]]*#[[:space:]]*define[[:space:]]+FE_(TONEAREST|UPWARD|DOWNWARD|TOWARDZERO)' sysdeps/
config BR2_PACKAGE_Z3_ARCH_SUPPORTS
	bool
	default y if BR2_aarch64 || BR2_aarch64_be
	default y if BR2_arceb || BR2_arcle
	default y if BR2_arm || BR2_armeb
	default y if BR2_i386
	default y if BR2_m68k
	# BR2_microblaze has only FE_TONEAREST
	default y if BR2_mips || BR2_mipsel || BR2_mips64 || BR2_mips64el
	# BR2_nios2 has only FE_TONEAREST
	default y if BR2_or1k
	default y if BR2_powerpc || BR2_powerpc64 || BR2_powerpc64le
	default y if BR2_riscv
	default y if BR2_s390x
	# BR2_sh has only FE_{TONEAREST,TOWARDZERO}
	default y if BR2_sparc || BR2_sparc64
	default y if BR2_x86_64
	# BR2_xtensa supports only uclibc which does not have fenv.h

config BR2_PACKAGE_Z3
	bool "z3"
	depends on BR2_INSTALL_LIBSTDCPP
	depends on BR2_TOOLCHAIN_GCC_AT_LEAST_7 # c++17
	# z3 needs fenv.h which is not provided by uclibc
	depends on !BR2_TOOLCHAIN_USES_UCLIBC
	depends on BR2_PACKAGE_Z3_ARCH_SUPPORTS
	help
	  Z3, also known as the Z3 Theorem Prover, is a cross-platform
	  satisfiability modulo theories (SMT) solver.

	  https://github.com/Z3Prover/z3

if BR2_PACKAGE_Z3

config BR2_PACKAGE_Z3_PYTHON
	bool "Python bindings"
	depends on BR2_PACKAGE_PYTHON3
	select BR2_PACKAGE_PYTHON3_PYEXPAT # runtime
	select BR2_PACKAGE_PYTHON_SETUPTOOLS # runtime

endif