Buildroot Archive on lore.kernel.org
 help / color / mirror / Atom feed
* [Buildroot] [PATCH next 1/1] package/z3: new package
@ 2022-11-19 12:05 Julien Olivain
  2022-11-20 14:03 ` Yann E. MORIN
  0 siblings, 1 reply; 2+ messages in thread
From: Julien Olivain @ 2022-11-19 12:05 UTC (permalink / raw)
  To: buildroot; +Cc: Julien Olivain

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>
---
Patch tested on branch next at commit 5f94d91 with commands:

    make check-package
    ...
    [No warning generated by this patch]

    python -m flake8 support/testing/tests/package/test_z3.py
    [no-output]

    support/testing/run-tests \
        -d dl -o output_folder \
        tests.package.test_z3.TestZ3
    ...
    OK

    ./utils/test-pkg -a -p z3
    ...
    44 builds, 26 skipped, 0 build failed, 0 legal-info failed, 0 show-info failed
---
 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      | 43 +++++++++++++++++++
 .../test_z3/rootfs-overlay/root/z3test.py     | 21 +++++++++
 .../test_z3/rootfs-overlay/root/z3test.smt2   |  8 ++++
 8 files changed, 123 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 <julien@vdg.name>
 F:	package/dieharder/
diff --git a/package/Config.in b/package/Config.in
index 52004de075..c3b540bd22 100644
--- a/package/Config.in
+++ b/package/Config.in
@@ -2189,6 +2189,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..a3f57f7f88
--- /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"
+	select BR2_PACKAGE_PYTHON3 # runtime
+	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..01aa81b1b6
--- /dev/null
+++ b/support/testing/tests/package/test_z3.py
@@ -0,0 +1,43 @@
+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_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..6ac53b98c5
--- /dev/null
+++ b/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py
@@ -0,0 +1,21 @@
+#! /usr/bin/env python3
+
+from z3 import *
+
+x = Real('x')
+y = Real('y')
+z = Real('z')
+s = 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 == 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)
-- 
2.38.1

_______________________________________________
buildroot mailing list
buildroot@buildroot.org
https://lists.buildroot.org/mailman/listinfo/buildroot

^ permalink raw reply related	[flat|nested] 2+ messages in thread
* Re: [Buildroot] [PATCH next 1/1] package/z3: new package
  2022-11-19 12:05 [Buildroot] [PATCH next 1/1] package/z3: new package Julien Olivain
@ 2022-11-20 14:03 ` Yann E. MORIN
  0 siblings, 0 replies; 2+ messages in thread
From: Yann E. MORIN @ 2022-11-20 14:03 UTC (permalink / raw)
  To: Julien Olivain; +Cc: buildroot

Julien, All,

On 2022-11-19 13:05 +0100, Julien Olivain spake thusly:
> 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>
[--SNIP--]
> diff --git a/package/z3/Config.in b/package/z3/Config.in
> new file mode 100644
> index 0000000000..a3f57f7f88
> --- /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"
> +	select BR2_PACKAGE_PYTHON3 # runtime

To me, it makes more sense that python bindings depend on python being
enabled, rather than forcing it. Indeed, if the python is not enabled
(either manually or because it is not selected by an application), then
there is no reason to enable it just to provide bindings.

And we do have that construct in at least a few other packages that
provide python bindings: libftdi1, libiio, ola... So I changed it to
match.  (yes, there are other packages that use select, but that's not a
reason to do things better nowadays! ;-) )

[--SNIP--]
> 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..6ac53b98c5
> --- /dev/null
> +++ b/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py
> @@ -0,0 +1,21 @@
> +#! /usr/bin/env python3
> +
> +from z3 import *

Not all of check-package/flake8 tests are run against files in the
runtime test-suite, but I have a hook that does it, and it reports:

    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:3:1: F403 'from z3 import *' used; unable to detect undefined names
    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:5:5: F405 'Real' may be undefined, or defined from star imports: z3
    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:6:5: F405 'Real' may be undefined, or defined from star imports: z3
    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:7:5: F405 'Real' may be undefined, or defined from star imports: z3
    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:8:5: F405 'Solver' may be undefined, or defined from star imports: z3
    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:20:17: F405 'sat' may be undefined, or defined from star imports: z3
    WARNING: 1     F403 'from z3 import *' used; unable to detect undefined names
    WARNING: 5     F405 'Real' may be undefined, or defined from star imports: z3

So I changed the test to import the whole z3 module, and to prefix
objects with z3.:

    x = z3.Real('x')

and so on...

Applied to next, thanks.

Regards,
Yann E. MORIN.

-- 
.-----------------.--------------------.------------------.--------------------.
|  Yann E. MORIN  | Real-Time Embedded | /"\ ASCII RIBBON | Erics' conspiracy: |
| +33 662 376 056 | Software  Designer | \ / CAMPAIGN     |  ___               |
| +33 561 099 427 `------------.-------:  X  AGAINST      |  \e/  There is no  |
| http://ymorin.is-a-geek.org/ | _/*\_ | / \ HTML MAIL    |   v   conspiracy.  |
'------------------------------^-------^------------------^--------------------'
_______________________________________________
buildroot mailing list
buildroot@buildroot.org
https://lists.buildroot.org/mailman/listinfo/buildroot

^ permalink raw reply	[flat|nested] 2+ messages in thread
end of thread, other threads:[~2022-11-20 14:04 UTC | newest]

Thread overview: 2+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2022-11-19 12:05 [Buildroot] [PATCH next 1/1] package/z3: new package Julien Olivain
2022-11-20 14:03 ` Yann E. MORIN

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox