diff --git a/package/z3/Config.in b/package/z3/Config.in index 55b0e8bb3b..8cd3128687 100644 --- a/package/z3/Config.in +++ b/package/z3/Config.in @@ -1,11 +1,33 @@ +# 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 - # fenv.h lacks FE_INVALID, FE_OVERFLOW & FE_UNDERFLOW on nios2 - depends on !BR2_nios2 + 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.