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>

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 <julien@vdg.name>
 F:	package/dieharder/

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"

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

package/z3/z3.hash

@@ -0,0 +1,3 @@
+# Locally calculated
+sha256  e3a82431b95412408a9c994466fad7252135c8ed3f719c986cd75c8c5f234c7e  z3-4.11.2.tar.gz
+sha256  e617cad2ab9347e3129c2b171e87909332174e17961c5c3412d0799469111337  LICENSE.txt

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))

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)

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

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)