git: 5c1f797943b0 - main - math/py-z3-solver: update 4.8.17 → 4.13.2
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Tue, 08 Oct 2024 03:44:44 UTC
The branch main has been updated by yuri:
URL: https://cgit.FreeBSD.org/ports/commit/?id=5c1f797943b07bb6cfae24800302cf16576826d1
commit 5c1f797943b07bb6cfae24800302cf16576826d1
Author: Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2024-10-08 00:10:58 +0000
Commit: Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2024-10-08 03:44:40 +0000
math/py-z3-solver: update 4.8.17 → 4.13.2
This fixes the problem from bug#280689.
PR: 280689
---
math/py-z3-solver/Makefile | 40 +++++++++++-------
math/py-z3-solver/distinfo | 6 +--
math/py-z3-solver/files/example-dog-cat-mouse.py | 18 ++++++++
math/py-z3-solver/files/example-eight-queens.py | 22 ++++++++++
math/py-z3-solver/files/example-kinematics.py | 25 +++++++++++
math/py-z3-solver/files/example-power-of-two.py | 15 +++++++
math/py-z3-solver/files/example-sudoku.py | 53 ++++++++++++++++++++++++
math/py-z3-solver/files/patch-CMakeLists.txt | 30 ++++++++++++++
math/py-z3-solver/files/patch-setup.py | 12 ------
math/py-z3-solver/pkg-plist | 11 +++++
10 files changed, 203 insertions(+), 29 deletions(-)
diff --git a/math/py-z3-solver/Makefile b/math/py-z3-solver/Makefile
index ba11090e2ea5..bbf694357a70 100644
--- a/math/py-z3-solver/Makefile
+++ b/math/py-z3-solver/Makefile
@@ -1,7 +1,6 @@
PORTNAME= z3-solver
DISTVERSIONPREFIX= z3-
-DISTVERSION= 4.8.17
-PORTREVISION= 1
+DISTVERSION= 4.13.2
CATEGORIES= math
PKGNAMEPREFIX= ${PYTHON_PKGNAMEPREFIX}
@@ -12,26 +11,39 @@ WWW= https://github.com/Z3Prover/z3
LICENSE= MIT
LICENSE_FILE= ${WRKSRC}/../../../LICENSE.txt
-BROKEN= Could not find libz3.so
-BROKEN_armv7= fails to compile on 13.1 and 14: clang crashes, see https://bugs.freebsd.org/bugzilla/show_bug.cgi?id=268009
-BROKEN_riscv64= fails to configure, see https://github.com/Z3Prover/z3/issues/6183
+LIB_DEPENDS= libz3.so:math/z3
-USES= cmake:indirect compiler:c++11-lang python
-USE_PYTHON= distutils autoplist
-
-NO_ARCH= yes
+USES= cmake python
+USE_PYTHON= flavors autoplist
USE_GITHUB= yes
GH_ACCOUNT= Z3Prover
GH_PROJECT= z3
-CFLAGS_armv7= -fPIC
-
WRKSRC_SUBDIR= src/api/python
+WRKSRC_top= ${WRKSRC}/../../..
-# CAVEAT: There should have LIB_DEPENDS=libz3.so:math/z3, but currently it rebuilds all code, see https://github.com/Z3Prover/z3/issues/1767
+TEST_ENV= ${MAKE_ENV} PYTHONPATH=${STAGEDIR}${PYTHONPREFIX_SITELIBDIR}
+
+NO_ARCH= yes
-post-patch: # https://github.com/Z3Prover/z3/issues/2131
- @${REINPLACE_CMD} 's|…|...|' ${WRKSRC}/../../ast/recfun_decl_plugin.h
+post-patch:
+ @${RLN} ${WRKSRC_top}/scripts ${WRKSRC}/scripts
+ @${RLN} ${WRKSRC_top}/src/api ${WRKSRC}/api
+
+do-test:
+.for t in z3 z3num
+ @cd ${WRKSRC_top} && \
+ ${CP} ${WRKSRC}/z3test.py . && \
+ ${ECHO} "==> running the test ${t}" && \
+ ${SETENV} ${TEST_ENV} ${PYTHON_CMD} z3test.py ${t} && \
+ ${ECHO} "... test ${t} succeeded"
+.endfor
+.for e in kinematics power-of-two dog-cat-mouse sudoku eight-queens
+ @cd ${WRKSRC}/../../.. && \
+ ${ECHO} "==> running the example ${e}" && \
+ ${SETENV} ${TEST_ENV} ${PYTHON_CMD} ${FILESDIR}/example-${e}.py && \
+ ${ECHO} "... example ${e} succeeded"
+.endfor
.include <bsd.port.mk>
diff --git a/math/py-z3-solver/distinfo b/math/py-z3-solver/distinfo
index 575d20c355c6..884770bddf55 100644
--- a/math/py-z3-solver/distinfo
+++ b/math/py-z3-solver/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1652241609
-SHA256 (Z3Prover-z3-z3-4.8.17_GH0.tar.gz) = 1e57637ce8d5212fd38453df28e2730a18e0a633f723682267be87f5b858a126
-SIZE (Z3Prover-z3-z3-4.8.17_GH0.tar.gz) = 5232392
+TIMESTAMP = 1728341031
+SHA256 (Z3Prover-z3-z3-4.13.2_GH0.tar.gz) = fd7dc6dd2633074f0a47670d6378b0e5c28c2c26f2b58aa23e9cd7f0bc9ba0dc
+SIZE (Z3Prover-z3-z3-4.13.2_GH0.tar.gz) = 5578178
diff --git a/math/py-z3-solver/files/example-dog-cat-mouse.py b/math/py-z3-solver/files/example-dog-cat-mouse.py
new file mode 100644
index 000000000000..861b8180f5f4
--- /dev/null
+++ b/math/py-z3-solver/files/example-dog-cat-mouse.py
@@ -0,0 +1,18 @@
+# example from https://ericpony.github.io/z3py-tutorial/guide-examples.htm
+
+from z3 import Ints, solve
+
+
+# Create 3 integer variables
+dog, cat, mouse = Ints('dog cat mouse')
+solve(dog >= 1, # at least one dog
+ cat >= 1, # at least one cat
+ mouse >= 1, # at least one mouse
+ # we want to buy 100 animals
+ dog + cat + mouse == 100,
+ # We have 100 dollars (10000 cents):
+ # dogs cost 15 dollars (1500 cents),
+ # cats cost 1 dollar (100 cents), and
+ # mice cost 25 cents
+ 1500 * dog + 100 * cat + 25 * mouse == 10000)
+
diff --git a/math/py-z3-solver/files/example-eight-queens.py b/math/py-z3-solver/files/example-eight-queens.py
new file mode 100644
index 000000000000..06eb2955fd02
--- /dev/null
+++ b/math/py-z3-solver/files/example-eight-queens.py
@@ -0,0 +1,22 @@
+# example from https://ericpony.github.io/z3py-tutorial/guide-examples.htm
+
+from z3 import Int, And, Distinct, If, solve, print_matrix
+
+
+# We know each queen must be in a different row.
+# So, we represent each queen by a single integer: the column position
+Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]
+
+# Each queen is in a column {1, ... 8 }
+val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]
+
+# At most one queen per column
+col_c = [ Distinct(Q) ]
+
+# Diagonal constraint
+diag_c = [ If(i == j,
+ True,
+ And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
+ for i in range(8) for j in range(i) ]
+
+solve(val_c + col_c + diag_c)
diff --git a/math/py-z3-solver/files/example-kinematics.py b/math/py-z3-solver/files/example-kinematics.py
new file mode 100644
index 000000000000..c1cfe30916af
--- /dev/null
+++ b/math/py-z3-solver/files/example-kinematics.py
@@ -0,0 +1,25 @@
+# example from https://ericpony.github.io/z3py-tutorial/guide-examples.htm
+
+from z3 import Reals, set_option, solve
+
+
+d, a, t, v_i, v_f = Reals('d a t v__i v__f')
+
+equations = [
+ d == v_i * t + (a*t**2)/2,
+ v_f == v_i + a*t,
+]
+
+# Given v_i, t and a, find d
+problem = [
+ v_i == 0,
+ t == 4.10,
+ a == 6
+]
+
+solve(equations + problem)
+
+# Display rationals in decimal notation
+set_option(rational_to_decimal=True)
+
+solve(equations + problem)
diff --git a/math/py-z3-solver/files/example-power-of-two.py b/math/py-z3-solver/files/example-power-of-two.py
new file mode 100644
index 000000000000..b7fdcd090f02
--- /dev/null
+++ b/math/py-z3-solver/files/example-power-of-two.py
@@ -0,0 +1,15 @@
+# example from https://ericpony.github.io/z3py-tutorial/guide-examples.htm
+
+from z3 import BitVec, And, Or, prove
+
+
+x = BitVec('x', 32)
+powers = [ 2**i for i in range(32) ]
+fast = And(x != 0, x & (x - 1) == 0)
+slow = Or([ x == p for p in powers ])
+print (fast)
+prove(fast == slow)
+
+print ("trying to prove buggy version...")
+fast = x & (x - 1) == 0
+prove(fast == slow)
diff --git a/math/py-z3-solver/files/example-sudoku.py b/math/py-z3-solver/files/example-sudoku.py
new file mode 100644
index 000000000000..e0a19b17bf6f
--- /dev/null
+++ b/math/py-z3-solver/files/example-sudoku.py
@@ -0,0 +1,53 @@
+# example from https://ericpony.github.io/z3py-tutorial/guide-examples.htm
+
+from z3 import Int, And, Distinct, If, Solver, sat, print_matrix
+
+
+# 9x9 matrix of integer variables
+X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
+ for i in range(9) ]
+
+# each cell contains a value in {1, ..., 9}
+cells_c = [ And(1 <= X[i][j], X[i][j] <= 9)
+ for i in range(9) for j in range(9) ]
+
+# each row contains a digit at most once
+rows_c = [ Distinct(X[i]) for i in range(9) ]
+
+# each column contains a digit at most once
+cols_c = [ Distinct([ X[i][j] for i in range(9) ])
+ for j in range(9) ]
+
+# each 3x3 square contains a digit at most once
+sq_c = [ Distinct([ X[3*i0 + i][3*j0 + j]
+ for i in range(3) for j in range(3) ])
+ for i0 in range(3) for j0 in range(3) ]
+
+sudoku_c = cells_c + rows_c + cols_c + sq_c
+
+# sudoku instance, we use '0' for empty cells
+instance = ((0,0,0,0,9,4,0,3,0),
+ (0,0,0,5,1,0,0,0,7),
+ (0,8,9,0,0,0,0,4,0),
+ (0,0,0,0,0,0,2,0,8),
+ (0,6,0,2,0,1,0,5,0),
+ (1,0,2,0,0,0,0,0,0),
+ (0,7,0,0,0,0,5,2,0),
+ (9,0,0,0,6,5,0,0,0),
+ (0,4,0,9,7,0,0,0,0))
+
+instance_c = [ If(instance[i][j] == 0,
+ True,
+ X[i][j] == instance[i][j])
+ for i in range(9) for j in range(9) ]
+
+s = Solver()
+s.add(sudoku_c + instance_c)
+if s.check() == sat:
+ m = s.model()
+ r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
+ for i in range(9) ]
+ print_matrix(r)
+else:
+ print ("failed to solve")
+
diff --git a/math/py-z3-solver/files/patch-CMakeLists.txt b/math/py-z3-solver/files/patch-CMakeLists.txt
new file mode 100644
index 000000000000..670b2e2e4e50
--- /dev/null
+++ b/math/py-z3-solver/files/patch-CMakeLists.txt
@@ -0,0 +1,30 @@
+--- CMakeLists.txt.orig 2024-10-07 22:51:28 UTC
++++ CMakeLists.txt
+@@ -1,4 +1,27 @@ message(STATUS "Emitting rules to build Z3 python bind
+ message(STATUS "Emitting rules to build Z3 python bindings")
++
++## portion of src/CMakeLists.txt
++set(Z3_API_HEADER_FILES_TO_SCAN
++ z3_api.h
++ z3_ast_containers.h
++ z3_algebraic.h
++ z3_polynomial.h
++ z3_rcf.h
++ z3_fixedpoint.h
++ z3_optimization.h
++ z3_fpa.h
++ z3_spacer.h
++)
++set(Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "")
++foreach (header_file ${Z3_API_HEADER_FILES_TO_SCAN})
++ set(full_path_api_header_file "${CMAKE_CURRENT_SOURCE_DIR}/api/${header_file}")
++ list(APPEND Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "${full_path_api_header_file}")
++ if (NOT EXISTS "${full_path_api_header_file}")
++ message(FATAL_ERROR "API header file \"${full_path_api_header_file}\" does not exist")
++ endif()
++endforeach()
++
++
+ ###############################################################################
+ # Add target to build python bindings for the build directory
+ ###############################################################################
diff --git a/math/py-z3-solver/files/patch-setup.py b/math/py-z3-solver/files/patch-setup.py
deleted file mode 100644
index af13eec6c882..000000000000
--- a/math/py-z3-solver/files/patch-setup.py
+++ /dev/null
@@ -1,12 +0,0 @@
---- setup.py.orig 2018-07-21 19:34:29 UTC
-+++ setup.py
-@@ -161,9 +161,5 @@ setup(
- keywords=['z3', 'smt', 'sat', 'prover', 'theorem'],
- packages=['z3'],
- include_package_data=True,
-- package_data={
-- 'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')]
-- },
-- data_files=[('bin',[os.path.join('bin',EXECUTABLE_FILE)])],
- cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg},
- )
diff --git a/math/py-z3-solver/pkg-plist b/math/py-z3-solver/pkg-plist
new file mode 100644
index 000000000000..f4db9c2982a4
--- /dev/null
+++ b/math/py-z3-solver/pkg-plist
@@ -0,0 +1,11 @@
+%%PYTHON_SITELIBDIR%%/z3/__init__.py
+%%PYTHON_SITELIBDIR%%/z3/z3.py
+%%PYTHON_SITELIBDIR%%/z3/z3consts.py
+%%PYTHON_SITELIBDIR%%/z3/z3core.py
+%%PYTHON_SITELIBDIR%%/z3/z3num.py
+%%PYTHON_SITELIBDIR%%/z3/z3poly.py
+%%PYTHON_SITELIBDIR%%/z3/z3printer.py
+%%PYTHON_SITELIBDIR%%/z3/z3rcf.py
+%%PYTHON_SITELIBDIR%%/z3/z3test.py
+%%PYTHON_SITELIBDIR%%/z3/z3types.py
+%%PYTHON_SITELIBDIR%%/z3/z3util.py