From 2ad68ff8df71a485085b0b83ff494081e4d926b7 Mon Sep 17 00:00:00 2001 From: Julien Olivain Date: Sat, 19 Nov 2022 13:05:18 +0100 Subject: [PATCH] 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 [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 --- DEVELOPERS | 2 + package/Config.in | 1 + package/z3/Config.in | 23 ++++++++++ package/z3/z3.hash | 3 ++ package/z3/z3.mk | 22 ++++++++++ support/testing/tests/package/test_z3.py | 44 +++++++++++++++++++ .../test_z3/rootfs-overlay/root/z3test.py | 21 +++++++++ .../test_z3/rootfs-overlay/root/z3test.smt2 | 8 ++++ 8 files changed, 124 insertions(+) create mode 100644 package/z3/Config.in create mode 100644 package/z3/z3.hash create mode 100644 package/z3/z3.mk create mode 100644 support/testing/tests/package/test_z3.py create mode 100755 support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py create mode 100644 support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.smt2 diff --git a/DEVELOPERS b/DEVELOPERS index bc026da4aa..fb6b329087 100644 --- a/DEVELOPERS +++ b/DEVELOPERS @@ -1697,6 +1697,7 @@ F: package/python-gnupg/ F: package/python-pyalsa/ F: package/riscv-isa-sim/ F: package/tinycompress/ +F: package/z3/ F: package/zynaddsubfx/ F: support/testing/tests/package/sample_python_distro.py F: support/testing/tests/package/sample_python_gnupg.py @@ -1708,6 +1709,7 @@ F: support/testing/tests/package/test_ola/ F: support/testing/tests/package/test_python_distro.py F: support/testing/tests/package/test_python_gnupg.py F: support/testing/tests/package/test_python_pyalsa.py +F: support/testing/tests/package/test_z3.py N: Julien Viard de Galbert F: package/dieharder/ diff --git a/package/Config.in b/package/Config.in index c448e8bd97..7b18859d02 100644 --- a/package/Config.in +++ b/package/Config.in @@ -2190,6 +2190,7 @@ menu "Miscellaneous" source "package/wine/Config.in" source "package/xmrig/Config.in" source "package/xutil_util-macros/Config.in" + source "package/z3/Config.in" endmenu menu "Networking applications" diff --git a/package/z3/Config.in b/package/z3/Config.in new file mode 100644 index 0000000000..55b0e8bb3b --- /dev/null +++ b/package/z3/Config.in @@ -0,0 +1,23 @@ +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 + 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 diff --git a/package/z3/z3.hash b/package/z3/z3.hash new file mode 100644 index 0000000000..d38c5f1971 --- /dev/null +++ b/package/z3/z3.hash @@ -0,0 +1,3 @@ +# Locally calculated +sha256 e3a82431b95412408a9c994466fad7252135c8ed3f719c986cd75c8c5f234c7e z3-4.11.2.tar.gz +sha256 e617cad2ab9347e3129c2b171e87909332174e17961c5c3412d0799469111337 LICENSE.txt diff --git a/package/z3/z3.mk b/package/z3/z3.mk new file mode 100644 index 0000000000..2252e05395 --- /dev/null +++ b/package/z3/z3.mk @@ -0,0 +1,22 @@ +################################################################################ +# +# z3 +# +################################################################################ + +Z3_VERSION = 4.11.2 +Z3_SITE = $(call github,Z3Prover,z3,z3-$(Z3_VERSION)) +Z3_LICENSE = MIT +Z3_LICENSE_FILES = LICENSE.txt +Z3_INSTALL_STAGING = YES +Z3_SUPPORTS_IN_SOURCE_BUILD = NO + +ifeq ($(BR2_PACKAGE_Z3_PYTHON),y) +Z3_CONF_OPTS += \ + -DCMAKE_INSTALL_PYTHON_PKG_DIR=/usr/lib/python$(PYTHON3_VERSION_MAJOR)/site-packages \ + -DZ3_BUILD_PYTHON_BINDINGS=ON +else +Z3_CONF_OPTS += -DZ3_BUILD_PYTHON_BINDINGS=OFF +endif + +$(eval $(cmake-package)) diff --git a/support/testing/tests/package/test_z3.py b/support/testing/tests/package/test_z3.py new file mode 100644 index 0000000000..71b074a587 --- /dev/null +++ b/support/testing/tests/package/test_z3.py @@ -0,0 +1,44 @@ +import os + +import infra.basetest + + +class TestZ3(infra.basetest.BRTest): + # Need to use a different toolchain than the default due to + # z3 requiring fenv.h not provided by uclibc. + config = \ + """ + BR2_arm=y + BR2_TOOLCHAIN_EXTERNAL=y + BR2_TOOLCHAIN_EXTERNAL_BOOTLIN=y + BR2_TOOLCHAIN_EXTERNAL_BOOTLIN_ARMV5_EABI_GLIBC_STABLE=y + BR2_PACKAGE_PYTHON3=y + BR2_PACKAGE_Z3=y + BR2_PACKAGE_Z3_PYTHON=y + BR2_ROOTFS_OVERLAY="{}" + BR2_TARGET_ROOTFS_CPIO=y + # BR2_TARGET_ROOTFS_TAR is not set + """.format( + # overlay to add a z3 smt and python test scripts + infra.filepath("tests/package/test_z3/rootfs-overlay")) + + def test_run(self): + cpio_file = os.path.join(self.builddir, "images", "rootfs.cpio") + self.emulator.boot(arch="armv5", + kernel="builtin", + options=["-initrd", cpio_file]) + self.emulator.login() + + # Check program executes + cmd = "z3 --version" + self.assertRunOk(cmd) + + # Run a basic smt2 example + cmd = "z3 /root/z3test.smt2" + output, exit_code = self.emulator.run(cmd) + self.assertEqual(exit_code, 0) + self.assertEqual(output[0], "unsat") + + # Run a basic python example + cmd = "/root/z3test.py" + self.assertRunOk(cmd, timeout=10) diff --git a/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py b/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py new file mode 100755 index 0000000000..98b8e57b56 --- /dev/null +++ b/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py @@ -0,0 +1,21 @@ +#! /usr/bin/env python3 + +import z3 + +x = z3.Real('x') +y = z3.Real('y') +z = z3.Real('z') +s = z3.Solver() + +s.add(3 * x + 2 * y - z == 1) +s.add(2 * x - 2 * y + 4 * z == -2) +s.add(-x + y / 2 - z == 0) + +check = s.check() +model = s.model() + +print(check) +print(model) + +assert check == z3.sat +assert model[x] == 1 and model[y] == -2 and model[z] == -2 diff --git a/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.smt2 b/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.smt2 new file mode 100644 index 0000000000..08df9e27a2 --- /dev/null +++ b/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.smt2 @@ -0,0 +1,8 @@ +; From https://smtlib.cs.uiowa.edu/examples.shtml +; Basic Boolean example +(set-option :print-success false) +(set-logic QF_UF) +(declare-const p Bool) +(assert (and p (not p))) +(check-sat) ; returns 'unsat' +(exit)