| 123456789101112131415161718192021222324252627282930313233343536373839404142434445 |
- # 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
|
