From nobody Tue Oct 08 03:44:44 2024 X-Original-To: dev-commits-ports-main@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4XN22h1xkrz5YsHx; Tue, 08 Oct 2024 03:44:44 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "mxrelay.nyi.freebsd.org", Issuer "R11" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4XN22h1PsRz4Sg7; Tue, 8 Oct 2024 03:44:44 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1728359084; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=dhVjP4Gw7ffT2mfR0N7kMAO6Beu2O2VaYNbWuvCursg=; b=FmFUzuUzXayK8AYiyF0mbhIsDf9HL3qg7zjrhmrdBkeKorPM5GyfpsiWGs3K9GOsw8zcPX 2WqL0eQEg4sfKdk8GYeCMV8e9etH3nvDGClA0HIbXktBPzNwiO34xUSuV28fSw5fXpLlDI UbvlSiAAjqUeuGjALqpx58/Nwz1JfObhkodxYRzTYn6+it8xkcQNYREBkujS1jVOj18mwb NRfs3lGCSYu8O4XuuZ9wmGTlu6H3W5IKJ3KumcNqpgLqT3TTlSr8h35XpF0Z1TOPI8tM6T B7TWhvMFYJEbP2969V/JMPwxqqoKApuzNWOGRuo7kUPERgtAavKX2VO+4BXHWQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1728359084; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=dhVjP4Gw7ffT2mfR0N7kMAO6Beu2O2VaYNbWuvCursg=; b=xiyic8LrkTkJ5CwNg2D/RwmtBVngtbcJcwGWq0o86eS/w/jAp1+2gukPvm8WOcN/L0zfye e6ZkqlYjAW8ylNGmb6uA1XQrX4BAeDNMwsFcc4s/iN85KOe2HGLclvmICgc+nWO+IVSZav 3yxiM2uk8/XRR7EIUrtT96dEqzGgQveiw1DxkGsu6zqrGRwBlkNjjdPlOm4Y+TThtcMdLu GPCXOtwkpj/HEhiv4JHrqHZUsuaje1PQcfF13mCWLASfAvIPaOLWgpKOuMfgaJrgVXU30L Y272arI9Wa6rB3dw9sN38OKtmM5G1bfQgm0rf9CRTzS/x5UtP+k+p2gQGAyywA== ARC-Authentication-Results: i=1; mx1.freebsd.org; none ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1728359084; a=rsa-sha256; cv=none; b=jeWS2AhVWM+9N3yOVwK8GlFp8kLwPvIHxaDlwqIlPJf4S0ZKKCxnUvuVawSEPOnKh9IUO8 +YoRk0r10557wfkdsq1m7PB5ji8a+AQfEqKVVuvvSgzVgt2xHkERfdGm2ZGtH01rgfypNR 33vvBTDN9ZAPkWQXc7qmD5LMDOWBxG0uOETHzhNHTfRfcp1ECy17WtzRehsmFVnDIanyCB Yd+bvSkYGY8KuTCLcf0U2WQSW67rlgLjFxEBxOVlc0BIcvg+ZGAsAvLJEXvbwq6Ggoddni gD6hXxHGywuxheHcxU3aaa/i1XHmJJs2WEaQf6TUS60LVzo8X4GEy6npO9HbvA== Received: from gitrepo.freebsd.org (gitrepo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:5]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id 4XN22h0y1Kz1Cvd; Tue, 8 Oct 2024 03:44:44 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from gitrepo.freebsd.org ([127.0.1.44]) by gitrepo.freebsd.org (8.18.1/8.18.1) with ESMTP id 4983iiAF010300; Tue, 8 Oct 2024 03:44:44 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.18.1/8.18.1/Submit) id 4983iirg010297; Tue, 8 Oct 2024 03:44:44 GMT (envelope-from git) Date: Tue, 8 Oct 2024 03:44:44 GMT Message-Id: <202410080344.4983iirg010297@gitrepo.freebsd.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org From: Yuri Victorovich Subject: git: 5c1f797943b0 - main - math/py-z3-solver: update 4.8.17 =?utf-8?Q?=E2=86=92?= 4.13.2 List-Id: Commits to the main branch of the FreeBSD ports repository List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-main List-Help: List-Post: List-Subscribe: List-Unsubscribe: X-BeenThere: dev-commits-ports-main@freebsd.org Sender: owner-dev-commits-ports-main@FreeBSD.org MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Git-Committer: yuri X-Git-Repository: ports X-Git-Refname: refs/heads/main X-Git-Reftype: branch X-Git-Commit: 5c1f797943b07bb6cfae24800302cf16576826d1 Auto-Submitted: auto-generated The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=5c1f797943b07bb6cfae24800302cf16576826d1 commit 5c1f797943b07bb6cfae24800302cf16576826d1 Author: Yuri Victorovich AuthorDate: 2024-10-08 00:10:58 +0000 Commit: Yuri Victorovich 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 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