mirrors/buildroot
0
0
Fork 0
mirror of https://git.busybox.net/buildroot.git synced 2024-12-03 18:33:48 +08:00
Code Issues Packages Projects Releases Wiki Activity
master
buildroot/package/z3/Config.in

46 lines
1.5 KiB
Plaintext
Raw Permalink Normal View History

package/z3: introduce _ARCH_SUPPORTS z3 package was initially added with a depends on !BR2_nios2. This was detected by testing with "./utils/test-pkg -a -p z3". It turned out that few other architectures are also not supported. The actual z3 requirement is to have a libc that provides <fenv.h> AND also provides all the four macros: FE_DOWNWARD, FE_TONEAREST, FE_TOWARDZERO, FE_UPWARD. Quoting glibc manual, or "man fenv": https://www.gnu.org/software/libc/manual/html_node/Rounding.html "fenv.h defines constants which you can use to refer to the various rounding modes. Each one will be defined if and only if the FPU supports the corresponding rounding mode." This patch introduces _ARCH_SUPPORTS to limit only to the architectures with a FPU that has those rounding modes. Fixes: - http://autobuild.buildroot.net/results/2809dd1ae2f3ada8ee7b3f3e388341c7cfb633fb Signed-off-by: Julien Olivain <ju.o@free.fr> Signed-off-by: Yann E. MORIN <yann.morin.1998@free.fr>
2022-12-07 07:10:34 +08:00
# 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
package/z3: new package Z3, also known as the Z3 Theorem Prover, is a cross-platform satisfiability modulo theories (SMT) solver. https://github.com/Z3Prover/z3 Signed-off-by: Julien Olivain <ju.o@free.fr> [yann.morin.1998@free.fr: - python bindings 'depends on' python, not 'select' it - fix check-package in test_z3.py ] Signed-off-by: Yann E. MORIN <yann.morin.1998@free.fr>
2022-11-19 20:05:18 +08:00
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
package/z3: introduce _ARCH_SUPPORTS z3 package was initially added with a depends on !BR2_nios2. This was detected by testing with "./utils/test-pkg -a -p z3". It turned out that few other architectures are also not supported. The actual z3 requirement is to have a libc that provides <fenv.h> AND also provides all the four macros: FE_DOWNWARD, FE_TONEAREST, FE_TOWARDZERO, FE_UPWARD. Quoting glibc manual, or "man fenv": https://www.gnu.org/software/libc/manual/html_node/Rounding.html "fenv.h defines constants which you can use to refer to the various rounding modes. Each one will be defined if and only if the FPU supports the corresponding rounding mode." This patch introduces _ARCH_SUPPORTS to limit only to the architectures with a FPU that has those rounding modes. Fixes: - http://autobuild.buildroot.net/results/2809dd1ae2f3ada8ee7b3f3e388341c7cfb633fb Signed-off-by: Julien Olivain <ju.o@free.fr> Signed-off-by: Yann E. MORIN <yann.morin.1998@free.fr>
2022-12-07 07:10:34 +08:00
depends on BR2_PACKAGE_Z3_ARCH_SUPPORTS
package/z3: new package Z3, also known as the Z3 Theorem Prover, is a cross-platform satisfiability modulo theories (SMT) solver. https://github.com/Z3Prover/z3 Signed-off-by: Julien Olivain <ju.o@free.fr> [yann.morin.1998@free.fr: - python bindings 'depends on' python, not 'select' it - fix check-package in test_z3.py ] Signed-off-by: Yann E. MORIN <yann.morin.1998@free.fr>
2022-11-19 20:05:18 +08:00
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
Reference in New Issue Copy Permalink