Merge branch 'next'

Signed-off-by: Peter Korsgaard <peter@korsgaard.com>

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)