X-Loop: help-debbugs@HIDDEN
Subject: [bug#75476] [PATCH] gnu: python-pysmt: Update to 0.9.6.
Resent-From: =?UTF-8?Q?Nguy=E1=BB=85n?= Gia Phong <mcsinyx@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: lars@HIDDEN, marius@HIDDEN, me@HIDDEN, sharlatanus@HIDDEN, tanguy@HIDDEN, jgart@HIDDEN, guix-patches@HIDDEN
Resent-Date: Fri, 10 Jan 2025 13:00:02 +0000
Resent-Message-ID: <handler.75476.B.1736513998550 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: report 75476
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: 75476 <at> debbugs.gnu.org
Cc: =?UTF-8?Q?Nguy=E1=BB=85n?= Gia Phong <mcsinyx@HIDDEN>, Lars-Dominik Braun <lars@HIDDEN>, Marius Bakke <marius@HIDDEN>, Munyoki Kilyungi <me@HIDDEN>, Sharlatan Hellseher <sharlatanus@HIDDEN>, Tanguy Le Carrour <tanguy@HIDDEN>, jgart <jgart@HIDDEN>
X-Debbugs-Original-To: guix-patches@HIDDEN
X-Debbugs-Original-Xcc: Lars-Dominik Braun <lars@HIDDEN>, Marius Bakke <marius@HIDDEN>, Munyoki Kilyungi <me@HIDDEN>, Sharlatan Hellseher <sharlatanus@HIDDEN>, Tanguy Le Carrour <tanguy@HIDDEN>, jgart <jgart@HIDDEN>
Received: via spool by submit <at> debbugs.gnu.org id=B.1736513998550
(code B ref -1); Fri, 10 Jan 2025 13:00:02 +0000
Received: (at submit) by debbugs.gnu.org; 10 Jan 2025 12:59:58 +0000
Received: from localhost ([127.0.0.1]:56672 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1tWEcH-00008n-3s
for submit <at> debbugs.gnu.org; Fri, 10 Jan 2025 07:59:58 -0500
Received: from lists.gnu.org ([2001:470:142::17]:51894)
by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.84_2) (envelope-from <mcsinyx@HIDDEN>)
id 1tWEcE-00008X-Uc
for submit <at> debbugs.gnu.org; Fri, 10 Jan 2025 07:59:56 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10])
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <mcsinyx@HIDDEN>)
id 1tWEc9-0004IS-EV
for guix-patches@HIDDEN; Fri, 10 Jan 2025 07:59:49 -0500
Received: from layka.disroot.org ([178.21.23.139])
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from <mcsinyx@HIDDEN>)
id 1tWEc6-0001aO-7e
for guix-patches@HIDDEN; Fri, 10 Jan 2025 07:59:49 -0500
Received: from mail01.disroot.lan (localhost [127.0.0.1])
by disroot.org (Postfix) with ESMTP id 12E2D25BEF;
Fri, 10 Jan 2025 13:59:42 +0100 (CET)
X-Virus-Scanned: SPAM Filter at disroot.org
Received: from layka.disroot.org ([127.0.0.1])
by localhost (disroot.org [127.0.0.1]) (amavis, port 10024) with ESMTP
id Wa53GN-qaHK5; Fri, 10 Jan 2025 13:59:34 +0100 (CET)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail;
t=1736513974; bh=bBfsffVOZf5L8gXoZ4na9MPErzElIAWgle0pqt2FR2I=;
h=From:To:Cc:Subject:Date;
b=VTQdyerSoGkOgqUvn6DCqfLauAFMytqz+k0YK1qyKE26kE3n/W9RobIR7z4KYbhL0
HBqn9iLzVL+K1BIpJ7aL07VfndXKy4ss7BwQHnJJ8HgMAWczJG7zqkWVr/7hZzv+Mh
RwS5H8/zNIZnKirZO2JyfLO0ME9RZQxlP6lXlK7p4Z+D2zLgB9OUW8kvjrvQtUENbs
NRucLyGZ/ouee8o0Am3nUTOYCgA+Vjn71G9m0Kf35UWSvFQ0WkHdf5+yAvV4u0u6n4
4uUvJAnInjq0TjkZwyOihwNjjJZvxL/i2SYYjS5Rl/C4th3Vy9LLkN4wKWRdKk6aVF
BMacTPOh7jgIw==
From: =?UTF-8?Q?Nguy=E1=BB=85n?= Gia Phong <mcsinyx@HIDDEN>
Date: Fri, 10 Jan 2025 21:59:21 +0900
Message-ID: <2ed2dee408f62e2498758555d01bb603dfa866f4.1736513961.git.mcsinyx@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Received-SPF: pass client-ip=178.21.23.139; envelope-from=mcsinyx@HIDDEN;
helo=layka.disroot.org
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1,
RCVD_IN_VALIDITY_CERTIFIED_BLOCKED=0.001, RCVD_IN_VALIDITY_RPBL_BLOCKED=0.001,
SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: 0.9 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.1 (/)
* gnu/packages/python-xyz.scm (python-pysmt): Update to 0.9.6.
* gnu/packages/patches/python-pysmt-fix-pow-return-type.patch:
Remove file.
* gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch:
Remove file.
* gnu/local.mk (dist_patch_DATA): Unregister them.
Change-Id: I4ecdad59abbb1c755a5be081cf3bf75992b36fb3
---
gnu/local.mk | 2 -
.../python-pysmt-fix-pow-return-type.patch | 258 ------------------
...-pysmt-fix-smtlib-serialization-test.patch | 86 ------
gnu/packages/python-xyz.scm | 9 +-
4 files changed, 4 insertions(+), 351 deletions(-)
delete mode 100644 gnu/packages/patches/python-pysmt-fix-pow-return-type.patch
delete mode 100644 gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 1d15be886da3..db2815dd2565 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -2104,8 +2104,6 @@ dist_patch_DATA = \
%D%/packages/patches/python-paste-remove-timing-test.patch \
%D%/packages/patches/python-pyan3-fix-absolute-path-bug.patch \
%D%/packages/patches/python-pyan3-fix-positional-arguments.patch \
- %D%/packages/patches/python-pysmt-fix-pow-return-type.patch \
- %D%/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch \
%D%/packages/patches/python-pytorch-fix-codegen.patch \
%D%/packages/patches/python-pytorch-runpath.patch \
%D%/packages/patches/python-pytorch-system-libraries.patch \
diff --git a/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch b/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch
deleted file mode 100644
index 0ec2d41b3c48..000000000000
--- a/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch
+++ /dev/null
@@ -1,258 +0,0 @@
-Backport of an upstream patch which fixes a test failure with our
-packaged version of the Z3 SMT solver.
-
-Taken from: https://github.com/pysmt/pysmt/commit/f522e8cd8f3e75ff85f5eae29b427e18a6701859
-
-diff --git a/pysmt/formula.py b/pysmt/formula.py
-index ea4b46c..6cb9cbf 100644
---- a/pysmt/formula.py
-+++ b/pysmt/formula.py
-@@ -252,11 +252,7 @@ class FormulaManager(object):
-
- if base.is_constant():
- val = base.constant_value() ** exponent.constant_value()
-- if base.is_constant(types.REAL):
-- return self.Real(val)
-- else:
-- assert base.is_constant(types.INT)
-- return self.Int(val)
-+ return self.Real(val)
- return self.create_node(node_type=op.POW, args=(base, exponent))
-
- def Div(self, left, right):
-diff --git a/pysmt/logics.py b/pysmt/logics.py
-index ef88dd6..9dc45b1 100644
---- a/pysmt/logics.py
-+++ b/pysmt/logics.py
-@@ -495,6 +495,12 @@ QF_NRA = Logic(name="QF_NRA",
- real_arithmetic=True,
- linear=False)
-
-+QF_NIRA = Logic(name="QF_NIRA",
-+ description="""Quantifier-free integer and real arithmetic.""",
-+ quantifier_free=True,
-+ integer_arithmetic=True,
-+ real_arithmetic=True,
-+ linear=False)
-
- QF_RDL = Logic(name="QF_RDL",
- description=\
-@@ -619,41 +625,41 @@ QF_AUFBVLIRA = Logic(name="QF_AUFBVLIRA",
- AUTO = Logic(name="Auto",
- description="Special logic used to indicate that the logic to be used depends on the formula.")
-
--SMTLIB2_LOGICS = frozenset([ AUFLIA,
-- AUFLIRA,
-- AUFNIRA,
-- ALIA,
-- LRA,
-- LIA,
-- NIA,
-- NRA,
-- UFLRA,
-- UFNIA,
-- UFLIRA,
-- QF_ABV,
-- QF_AUFBV,
-- QF_AUFLIA,
-- QF_ALIA,
-- QF_AX,
-- QF_BV,
-- QF_IDL,
-- QF_LIA,
-- QF_LRA,
-- QF_NIA,
-- QF_NRA,
-- QF_RDL,
-- QF_UF,
-- QF_UFBV ,
-- QF_UFIDL,
-- QF_UFLIA,
-- QF_UFLRA,
-- QF_UFNRA,
-- QF_UFNIA,
-- QF_UFLIRA,
-- QF_SLIA
-- ])
--
--LOGICS = SMTLIB2_LOGICS | frozenset([ QF_BOOL, BOOL, QF_AUFBVLIRA])
-+SMTLIB2_LOGICS = frozenset([AUFLIA,
-+ AUFLIRA,
-+ AUFNIRA,
-+ ALIA,
-+ LRA,
-+ LIA,
-+ NIA,
-+ NRA,
-+ UFLRA,
-+ UFNIA,
-+ UFLIRA,
-+ QF_ABV,
-+ QF_AUFBV,
-+ QF_AUFLIA,
-+ QF_ALIA,
-+ QF_AX,
-+ QF_BV,
-+ QF_IDL,
-+ QF_LIA,
-+ QF_LRA,
-+ QF_NIA,
-+ QF_NRA,
-+ QF_RDL,
-+ QF_UF,
-+ QF_UFBV,
-+ QF_UFIDL,
-+ QF_UFLIA,
-+ QF_UFLRA,
-+ QF_UFNRA,
-+ QF_UFNIA,
-+ QF_UFLIRA,
-+ QF_SLIA
-+ ])
-+
-+LOGICS = SMTLIB2_LOGICS | frozenset([QF_BOOL, BOOL, QF_AUFBVLIRA, QF_NIRA])
-
- QF_LOGICS = frozenset(_l for _l in LOGICS if _l.quantifier_free)
-
-@@ -668,8 +674,8 @@ PYSMT_LOGICS = frozenset([QF_BOOL, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFI
- QF_BV, QF_UFBV,
- QF_ABV, QF_AUFBV, QF_AUFLIA, QF_ALIA, QF_AX,
- QF_AUFBVLIRA,
-- QF_NRA, QF_NIA, UFBV, BV,
-- ])
-+ QF_NRA, QF_NIA, QF_NIRA, UFBV, BV,
-+ ])
-
- # PySMT Logics includes additional features:
- # - constant arrays: QF_AUFBV becomes QF_AUFBV*
-@@ -697,7 +703,6 @@ for l in PYSMT_LOGICS:
- ext_logics.add(nl)
-
-
--
- LOGICS = LOGICS | frozenset(ext_logics)
- PYSMT_LOGICS = PYSMT_LOGICS | frozenset(ext_logics)
-
-diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
-index 3fb42b9..210b771 100644
---- a/pysmt/solvers/z3.py
-+++ b/pysmt/solvers/z3.py
-@@ -595,6 +595,8 @@ class Z3Converter(Converter, DagWalker):
- None, None,
- 0, None,
- expr.ast)
-+ print("Z3: SMTLIB")
-+ print(s)
- stream_in = StringIO(s)
- r = parser.get_script(stream_in).get_last_formula(self.mgr)
- key = (askey(expr), None)
-diff --git a/pysmt/test/examples.py b/pysmt/test/examples.py
-index 73455ee..b653185 100644
---- a/pysmt/test/examples.py
-+++ b/pysmt/test/examples.py
-@@ -898,12 +898,12 @@ def get_full_example_formulae(environment=None):
- logic=pysmt.logics.QF_NRA
- ),
-
-- Example(hr="((p ^ 2) = 0)",
-- expr=Equals(Pow(p, Int(2)), Int(0)),
-+ Example(hr="((p ^ 2) = 0.0)",
-+ expr=Equals(Pow(p, Int(2)), Real(0)),
- is_valid=False,
- is_sat=True,
-- logic=pysmt.logics.QF_NIA
-- ),
-+ logic=pysmt.logics.QF_NIRA
-+ ),
-
- Example(hr="((r ^ 2.0) = 0.0)",
- expr=Equals(Pow(r, Real(2)), Real(0)),
-diff --git a/pysmt/test/test_back.py b/pysmt/test/test_back.py
-index bceb45b..7a0ad63 100644
---- a/pysmt/test/test_back.py
-+++ b/pysmt/test/test_back.py
-@@ -55,10 +55,10 @@ class TestBasic(TestCase):
- res = msat.converter.back(term)
- self.assertFalse(f == res)
-
-- def do_back(self, solver_name, z3_string_buffer=False):
-+ def do_back(self, solver_name, via_smtlib=False):
- for formula, _, _, logic in get_example_formulae():
- if logic.quantifier_free:
-- if logic.theory.custom_type and z3_string_buffer:
-+ if logic.theory.custom_type and via_smtlib:
- # Printing of declare-sort from Z3 is not conformant
- # with the SMT-LIB. We might consider extending our
- # parser.
-@@ -67,7 +67,7 @@ class TestBasic(TestCase):
- s = Solver(name=solver_name, logic=logic)
- term = s.converter.convert(formula)
- if solver_name == "z3":
-- if z3_string_buffer:
-+ if via_smtlib:
- res = s.converter.back_via_smtlib(term)
- else:
- res = s.converter.back(term)
-@@ -84,8 +84,8 @@ class TestBasic(TestCase):
-
- @skipIfSolverNotAvailable("z3")
- def test_z3_back_formulae(self):
-- self.do_back("z3", z3_string_buffer=False)
-- self.do_back("z3", z3_string_buffer=True)
-+ self.do_back("z3", via_smtlib=True)
-+ self.do_back("z3", via_smtlib=False)
-
-
- if __name__ == '__main__':
-diff --git a/pysmt/type_checker.py b/pysmt/type_checker.py
-index b700fcf..7ce05aa 100644
---- a/pysmt/type_checker.py
-+++ b/pysmt/type_checker.py
-@@ -33,6 +33,8 @@ class SimpleTypeChecker(walkers.DagWalker):
-
- def __init__(self, env=None):
- walkers.DagWalker.__init__(self, env=env)
-+ # Return None if the type cannot be computed rather than
-+ # raising an exception.
- self.be_nice = False
-
- def _get_key(self, formula, **kwargs):
-@@ -42,7 +44,7 @@ class SimpleTypeChecker(walkers.DagWalker):
- """ Returns the pysmt.types type of the formula """
- res = self.walk(formula)
- if not self.be_nice and res is None:
-- raise PysmtTypeError("The formula '%s' is not well-formed" \
-+ raise PysmtTypeError("The formula '%s' is not well-formed"
- % str(formula))
- return res
-
-@@ -114,7 +116,7 @@ class SimpleTypeChecker(walkers.DagWalker):
-
- def walk_bv_comp(self, formula, args, **kwargs):
- # We check that all children are BV and the same size
-- a,b = args
-+ a, b = args
- if a != b or (not a.is_bv_type()):
- return None
- return BVType(1)
-@@ -187,7 +189,7 @@ class SimpleTypeChecker(walkers.DagWalker):
- if args[0].is_bool_type():
- raise PysmtTypeError("The formula '%s' is not well-formed."
- "Equality operator is not supported for Boolean"
-- " terms. Use Iff instead." \
-+ " terms. Use Iff instead."
- % str(formula))
- elif args[0].is_bv_type():
- return self.walk_bv_to_bool(formula, args)
-@@ -324,10 +326,7 @@ class SimpleTypeChecker(walkers.DagWalker):
- def walk_pow(self, formula, args, **kwargs):
- if args[0] != args[1]:
- return None
-- # Exponent must be positive for INT
-- if args[0].is_int_type() and formula.arg(1).constant_value() < 0 :
-- return None
-- return args[0]
-+ return REAL
-
- # EOC SimpleTypeChecker
-
diff --git a/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch b/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch
deleted file mode 100644
index eee555f80783..000000000000
--- a/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch
+++ /dev/null
@@ -1,86 +0,0 @@
-Backport of an upstream patch fixing a test suite failure.
-
-Taken from: https://github.com/pysmt/pysmt/commit/a246669a487aff69f5da34570ef867841d18508a
-
-diff --git a/pysmt/test/smtlib/test_parser_examples.py b/pysmt/test/smtlib/test_parser_examples.py
-index cca4194..c0852be 100644
---- a/pysmt/test/smtlib/test_parser_examples.py
-+++ b/pysmt/test/smtlib/test_parser_examples.py
-@@ -29,6 +29,7 @@ from pysmt.shortcuts import Iff
- from pysmt.shortcuts import read_smtlib, write_smtlib, get_env
- from pysmt.exceptions import PysmtSyntaxError
-
-+
- class TestSMTParseExamples(TestCase):
-
- def test_parse_examples(self):
-@@ -41,7 +42,6 @@ class TestSMTParseExamples(TestCase):
- buf = StringIO()
- script_out = smtlibscript_from_formula(f_out)
- script_out.serialize(outstream=buf)
-- #print(buf)
-
- buf.seek(0)
- parser = SmtLibParser()
-@@ -49,7 +49,6 @@ class TestSMTParseExamples(TestCase):
- f_in = script_in.get_last_formula()
- self.assertEqual(f_in.simplify(), f_out.simplify())
-
--
- @skipIfNoSolverForLogic(logics.QF_BV)
- def test_parse_examples_bv(self):
- """For BV we represent a superset of the operators defined in SMT-LIB.
-@@ -108,7 +107,18 @@ class TestSMTParseExamples(TestCase):
- self.assertValid(Iff(f_in, f_out), f_in.serialize())
-
- def test_dumped_logic(self):
-- # Dumped logic matches the logic in the example
-+ # Dumped logic matches the logic in the example.
-+ #
-+ # There are a few cases where we use a logic
-+ # that does not exist in SMT-LIB, and the SMT-LIB
-+ # serialization logic will find a logic that
-+ # is more expressive. We need to adjust the test
-+ # for those cases (see rewrite dict below).
-+ rewrite = {
-+ logics.QF_BOOL: logics.QF_UF,
-+ logics.BOOL: logics.LRA,
-+ logics.QF_NIRA: logics.AUFNIRA,
-+ }
- fs = get_example_formulae()
-
- for (f_out, _, _, logic) in fs:
-@@ -121,14 +131,9 @@ class TestSMTParseExamples(TestCase):
- for cmd in script_in:
- if cmd.name == "set-logic":
- logic_in = cmd.args[0]
-- if logic == logics.QF_BOOL:
-- self.assertEqual(logic_in, logics.QF_UF)
-- elif logic == logics.BOOL:
-- self.assertEqual(logic_in, logics.LRA)
-- else:
-- self.assertEqual(logic_in, logic, script_in)
-+ self.assertEqual(logic_in, rewrite.get(logic, logic))
- break
-- else: # Loops exited normally
-+ else: # Loops exited normally
- print("-"*40)
- print(script_in)
-
-@@ -136,7 +141,7 @@ class TestSMTParseExamples(TestCase):
- fs = get_example_formulae()
-
- fdi, tmp_fname = mkstemp()
-- os.close(fdi) # Close initial file descriptor
-+ os.close(fdi) # Close initial file descriptor
- for (f_out, _, _, _) in fs:
- write_smtlib(f_out, tmp_fname)
- # with open(tmp_fname) as fin:
-@@ -197,7 +202,6 @@ class TestSMTParseExamples(TestCase):
- f_in = script.get_last_formula()
- self.assertSat(f_in)
-
--
- def test_int_promotion_define_fun(self):
- script = """
- (define-fun x () Int 8)
diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index ceb26960e3e7..201a75fa4fa7 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -160,6 +160,7 @@
;;; Copyright © 2024 Evgeny Pisemsky <mail@HIDDEN>
;;; Copyright © 2024 Markku Korkeala <markku.korkeala@HIDDEN>
;;; Copyright © 2025 Jordan Moore <lockbox@HIDDEN>
+;;; Copyright © 2025 Nguyễn Gia Phong <mcsinyx@HIDDEN>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -35655,26 +35656,24 @@ (define-public python-claripy
(define-public python-pysmt
(package
(name "python-pysmt")
- (version "0.9.5")
+ (version "0.9.6")
(source
(origin
;; Fetching from Git as pypi release doesn't include all test files.
(method git-fetch)
- (patches (search-patches "python-pysmt-fix-pow-return-type.patch"
- "python-pysmt-fix-smtlib-serialization-test.patch"))
(uri (git-reference
(url "https://github.com/pysmt/pysmt")
(commit (string-append "v" version))))
(file-name (git-file-name name version))
(sha256
- (base32 "0hrxv23y5ip4ijfx5pvbwc2fq4zg9jz42wc9zqgqm0g0mjc9ckvh"))))
+ (base32 "0jiw8pa6hfh9ajr953q187qgpdnk3bvaa3wmrxs8ilw5jc41sq8y"))))
(build-system pyproject-build-system)
(arguments
`(#:phases (modify-phases %standard-phases
(add-before 'check 'set-pysmt-solver
(lambda _
(setenv "PYSMT_SOLVER" "z3"))))))
- (native-inputs (list python-pytest))
+ (native-inputs (list python-setuptools python-wheel python-pytest))
(propagated-inputs (list z3))
(home-page "https://github.com/pysmt/pysmt")
(synopsis
base-commit: 461d773adead955e2daead70cee4415f7f0f00be
--
2.46.0
Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) Content-Type: text/plain; charset=utf-8 X-Loop: help-debbugs@HIDDEN From: help-debbugs@HIDDEN (GNU bug Tracking System) To: =?UTF-8?Q?Nguy=E1=BB=85n?= Gia Phong <mcsinyx@HIDDEN> Subject: bug#75476: Acknowledgement ([PATCH] gnu: python-pysmt: Update to 0.9.6.) Message-ID: <handler.75476.B.1736513998550.ack <at> debbugs.gnu.org> References: <2ed2dee408f62e2498758555d01bb603dfa866f4.1736513961.git.mcsinyx@HIDDEN> X-Gnu-PR-Message: ack 75476 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 75476 <at> debbugs.gnu.org Date: Fri, 10 Jan 2025 13:00:03 +0000 Thank you for filing a new bug report with debbugs.gnu.org. This is an automatically generated reply to let you know your message has been received. Your message is being forwarded to the package maintainers and other interested parties for their attention; they will reply in due course. As you requested using X-Debbugs-CC, your message was also forwarded to Lars-Dominik Braun <lars@HIDDEN>, Marius Bakke <marius@HIDDEN>, Munyoki= Kilyungi <me@HIDDEN>, Sharlatan Hellseher <sharlatanus@HIDDEN= om>, Tanguy Le Carrour <tanguy@HIDDEN>, jgart <jgart@HIDDEN> (after having been given a bug report number, if it did not have one). Your message has been sent to the package maintainer(s): guix-patches@HIDDEN If you wish to submit further information on this problem, please send it to 75476 <at> debbugs.gnu.org. Please do not send mail to help-debbugs@HIDDEN unless you wish to report a problem with the Bug-tracking system. --=20 75476: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D75476 GNU Bug Tracking System Contact help-debbugs@HIDDEN with problems
X-Loop: help-debbugs@HIDDEN
Subject: [bug#75476] [PATCH v2] gnu: python-pysmt: Update to 0.9.6.
References: <2ed2dee408f62e2498758555d01bb603dfa866f4.1736513961.git.mcsinyx@HIDDEN>
In-Reply-To: <2ed2dee408f62e2498758555d01bb603dfa866f4.1736513961.git.mcsinyx@HIDDEN>
Resent-From: ngraves@HIDDEN
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Sun, 02 Feb 2025 15:09:02 +0000
Resent-Message-ID: <handler.75476.B75476.17385089081103 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 75476
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: 75476 <at> debbugs.gnu.org
Cc: =?UTF-8?Q?Nguy=E1=BB=85n?= Gia Phong <mcsinyx@HIDDEN>
Received: via spool by 75476-submit <at> debbugs.gnu.org id=B75476.17385089081103
(code B ref 75476); Sun, 02 Feb 2025 15:09:02 +0000
Received: (at 75476) by debbugs.gnu.org; 2 Feb 2025 15:08:28 +0000
Received: from localhost ([127.0.0.1]:35821 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1teba6-0000HV-1L
for submit <at> debbugs.gnu.org; Sun, 02 Feb 2025 10:08:28 -0500
Received: from 3.mo576.mail-out.ovh.net ([188.165.52.203]:34771)
by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.84_2) (envelope-from <ngraves@HIDDEN>)
id 1teba0-0000HG-0x
for 75476 <at> debbugs.gnu.org; Sun, 02 Feb 2025 10:08:16 -0500
Received: from director6.ghost.mail-out.ovh.net (unknown [10.108.25.63])
by mo576.mail-out.ovh.net (Postfix) with ESMTP id 4YmCgF4Zb7z1rD5
for <75476 <at> debbugs.gnu.org>; Sun, 2 Feb 2025 15:08:09 +0000 (UTC)
Received: from ghost-submission-5b5ff79f4f-b6j4t (unknown [10.111.174.38])
by director6.ghost.mail-out.ovh.net (Postfix) with ESMTPS id C085C1FD36;
Sun, 2 Feb 2025 15:08:08 +0000 (UTC)
Received: from ngraves.fr ([37.59.142.105])
by ghost-submission-5b5ff79f4f-b6j4t with ESMTPSA
id HiLXEliKn2f8AwAAnLym/g
(envelope-from <ngraves@HIDDEN>); Sun, 02 Feb 2025 15:08:08 +0000
Authentication-Results: garm.ovh; auth=pass
(GARM-105G006d88cd71d-36d8-4ee8-b849-0eaf82435def,
0EB4F4ACF34A069A1D12270FF355DD325781616A) smtp.auth=ngraves@HIDDEN
X-OVh-ClientIp: 89.207.171.131
From: ngraves@HIDDEN
Date: Fri, 10 Jan 2025 21:59:21 +0900
Message-ID: <87plk0l6zs.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Ovh-Tracer-Id: 9968999253762826820
X-VR-SPAMSTATE: OK
X-VR-SPAMSCORE: 21
X-VR-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrgeefvddrtddtgddugeellecutefuodetggdotefrodftvfcurfhrohhfihhlvgemucfqggfjpdevjffgvefmvefgnecuuegrihhlohhuthemucehtddtnecuffgrthgvuchinhcuphgrshhtucdlvddumdenucfjughrpefhvfevufffkfggtgfgsehtqhertddttdejnecuhfhrohhmpehnghhrrghvvghssehnghhrrghvvghsrdhfrhenucggtffrrghtthgvrhhnpeetleehffefvddtffelkeffveelgeejudevveelkeejteejgfegjedtgedtffehleenucffohhmrghinhepghhithhhuhgsrdgtohhmnecukfhppeduvdejrddtrddtrddupdekledrvddtjedrudejuddrudefuddpfeejrdehledrudegvddruddtheenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhepihhnvghtpeduvdejrddtrddtrddupdhmrghilhhfrhhomhepnhhgrhgrvhgvshesnhhgrhgrvhgvshdrfhhrpdhnsggprhgtphhtthhopedupdhrtghpthhtohepjeehgeejieesuggvsggsuhhgshdrghhnuhdrohhrghdpoffvtefjohhsthepmhhoheejiegmpdhmohguvgepshhmthhpohhuth
DKIM-Signature: a=rsa-sha256; bh=JVqmnGZUBm0q4pTCSU3bC5phzI+uR8g0Ihrk1TjJQ9g=;
c=relaxed/relaxed; d=ngraves.fr; h=From;
s=ovhmo4487190-selector1; t=1738508889; v=1;
b=1C3h67eLvy3YfLwvTkqiw2/kmYplWMMO4OutRl/wOSEyw4JYwjiJN7ToXavwN8exORZ7sRwS
6iGKHiunnBsi6T8YGsefkapqJHs6vP7Atn11XLe6MXdDoeRRktxJaLMPgN5V678nUMz92SKmpKR
iAOPteT3vLulSg+UruzJGqnTULOneRyBDjTZQe/C2Rmu+vzEOBjUrThnRmMohYswNvKPC5n340f
yEIkKsCoZT4yK8pgLzcBzZMMENcxw8xq1DmWCafOMixBMz8tluCzUsATRa+D5S4rVcxlxNZ7q/5
AV/Z5haSztwOeJ7kRcAX/avsFnkFoINbpikfi2ilPEwUw==
X-Spam-Score: 2.1 (++)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: * gnu/packages/python-xyz.scm (python-pysmt): Update to
0.9.6.
* gnu/packages/patches/python-pysmt-fix-pow-return-type.patch: Remove file.
* gnu/packages/patches/python-pysmt-fix-smtlib-serialization- [...]
Content analysis details: (2.1 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
0.0 RCVD_IN_VALIDITY_CERTIFIED_BLOCKED RBL: ADMINISTRATOR NOTICE:
The query to Validity was blocked. See
https://knowledge.validity.com/hc/en-us/articles/20961730681243
for more information.
[188.165.52.203 listed in sa-accredit.habeas.com]
-0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at https://www.dnswl.org/,
no trust [188.165.52.203 listed in list.dnswl.org]
0.0 RCVD_IN_VALIDITY_RPBL_BLOCKED RBL: ADMINISTRATOR NOTICE: The
query to Validity was blocked. See
https://knowledge.validity.com/hc/en-us/articles/20961730681243
for more information.
[188.165.52.203 listed in bl.score.senderscore.com]
-0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2)
[188.165.52.203 listed in wl.mailspike.net]
2.1 DATE_IN_PAST_96_XX Date: is 96 hours or more before Received:
date -0.0 SPF_PASS SPF: sender matches SPF record
0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 1.1 (+)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: * gnu/packages/python-xyz.scm (python-pysmt): Update to 0.9.6.
* gnu/packages/patches/python-pysmt-fix-pow-return-type.patch: Remove file.
* gnu/packages/patches/python-pysmt-fix-smtlib-serialization- [...]
Content analysis details: (1.1 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
2.1 DATE_IN_PAST_96_XX Date: is 96 hours or more before Received:
date
-0.0 SPF_PASS SPF: sender matches SPF record
0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record
-1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list
manager
* gnu/packages/python-xyz.scm (python-pysmt): Update to 0.9.6.
* gnu/packages/patches/python-pysmt-fix-pow-return-type.patch:
Remove file.
* gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch:
Remove file.
* gnu/local.mk (dist_patch_DATA): Unregister them.
Change-Id: I4ecdad59abbb1c755a5be081cf3bf75992b36fb3
---
gnu/local.mk | 2 -
.../python-pysmt-fix-pow-return-type.patch | 258 ------------------
...-pysmt-fix-smtlib-serialization-test.patch | 86 ------
gnu/packages/python-xyz.scm | 7 +-
4 files changed, 3 insertions(+), 350 deletions(-)
delete mode 100644 gnu/packages/patches/python-pysmt-fix-pow-return-type.p=
atch
delete mode 100644 gnu/packages/patches/python-pysmt-fix-smtlib-serializat=
ion-test.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index aa91977391..799fcb0aae 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -2109,8 +2109,6 @@ dist_patch_DATA =3D \
%D%/packages/patches/python-paste-remove-timing-test.patch \
%D%/packages/patches/python-pyan3-fix-absolute-path-bug.patch \
%D%/packages/patches/python-pyan3-fix-positional-arguments.patch \
- %D%/packages/patches/python-pysmt-fix-pow-return-type.patch \
- %D%/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch \
%D%/packages/patches/python-pytorch-fix-codegen.patch \
%D%/packages/patches/python-pytorch-runpath.patch \
%D%/packages/patches/python-pytorch-system-libraries.patch \
diff --git a/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch b/=
gnu/packages/patches/python-pysmt-fix-pow-return-type.patch
deleted file mode 100644
index 0ec2d41b3c..0000000000
--- a/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch
+++ /dev/null
@@ -1,258 +0,0 @@
-Backport of an upstream patch which fixes a test failure with our
-packaged version of the Z3 SMT solver.
-
-Taken from: https://github.com/pysmt/pysmt/commit/f522e8cd8f3e75ff85f5eae2=
9b427e18a6701859
-
-diff --git a/pysmt/formula.py b/pysmt/formula.py
-index ea4b46c..6cb9cbf 100644
---- a/pysmt/formula.py
-+++ b/pysmt/formula.py
-@@ -252,11 +252,7 @@ class FormulaManager(object):
-
- if base.is_constant():
- val =3D base.constant_value() ** exponent.constant_value()
-- if base.is_constant(types.REAL):
-- return self.Real(val)
-- else:
-- assert base.is_constant(types.INT)
-- return self.Int(val)
-+ return self.Real(val)
- return self.create_node(node_type=3Dop.POW, args=3D(base, exponen=
t))
-
- def Div(self, left, right):
-diff --git a/pysmt/logics.py b/pysmt/logics.py
-index ef88dd6..9dc45b1 100644
---- a/pysmt/logics.py
-+++ b/pysmt/logics.py
-@@ -495,6 +495,12 @@ QF_NRA =3D Logic(name=3D"QF_NRA",
- real_arithmetic=3DTrue,
- linear=3DFalse)
-
-+QF_NIRA =3D Logic(name=3D"QF_NIRA",
-+ description=3D"""Quantifier-free integer and real arithme=
tic.""",
-+ quantifier_free=3DTrue,
-+ integer_arithmetic=3DTrue,
-+ real_arithmetic=3DTrue,
-+ linear=3DFalse)
-
- QF_RDL =3D Logic(name=3D"QF_RDL",
- description=3D\
-@@ -619,41 +625,41 @@ QF_AUFBVLIRA =3D Logic(name=3D"QF_AUFBVLIRA",
- AUTO =3D Logic(name=3D"Auto",
- description=3D"Special logic used to indicate that the logic=
to be used depends on the formula.")
-
--SMTLIB2_LOGICS =3D frozenset([ AUFLIA,
-- AUFLIRA,
-- AUFNIRA,
-- ALIA,
-- LRA,
-- LIA,
-- NIA,
-- NRA,
-- UFLRA,
-- UFNIA,
-- UFLIRA,
-- QF_ABV,
-- QF_AUFBV,
-- QF_AUFLIA,
-- QF_ALIA,
-- QF_AX,
-- QF_BV,
-- QF_IDL,
-- QF_LIA,
-- QF_LRA,
-- QF_NIA,
-- QF_NRA,
-- QF_RDL,
-- QF_UF,
-- QF_UFBV ,
-- QF_UFIDL,
-- QF_UFLIA,
-- QF_UFLRA,
-- QF_UFNRA,
-- QF_UFNIA,
-- QF_UFLIRA,
-- QF_SLIA
-- ])
--
--LOGICS =3D SMTLIB2_LOGICS | frozenset([ QF_BOOL, BOOL, QF_AUFBVLIRA])
-+SMTLIB2_LOGICS =3D frozenset([AUFLIA,
-+ AUFLIRA,
-+ AUFNIRA,
-+ ALIA,
-+ LRA,
-+ LIA,
-+ NIA,
-+ NRA,
-+ UFLRA,
-+ UFNIA,
-+ UFLIRA,
-+ QF_ABV,
-+ QF_AUFBV,
-+ QF_AUFLIA,
-+ QF_ALIA,
-+ QF_AX,
-+ QF_BV,
-+ QF_IDL,
-+ QF_LIA,
-+ QF_LRA,
-+ QF_NIA,
-+ QF_NRA,
-+ QF_RDL,
-+ QF_UF,
-+ QF_UFBV,
-+ QF_UFIDL,
-+ QF_UFLIA,
-+ QF_UFLRA,
-+ QF_UFNRA,
-+ QF_UFNIA,
-+ QF_UFLIRA,
-+ QF_SLIA
-+ ])
-+
-+LOGICS =3D SMTLIB2_LOGICS | frozenset([QF_BOOL, BOOL, QF_AUFBVLIRA, QF_NI=
RA])
-
- QF_LOGICS =3D frozenset(_l for _l in LOGICS if _l.quantifier_free)
-
-@@ -668,8 +674,8 @@ PYSMT_LOGICS =3D frozenset([QF_BOOL, QF_IDL, QF_LIA, Q=
F_LRA, QF_RDL, QF_UF, QF_UFI
- QF_BV, QF_UFBV,
- QF_ABV, QF_AUFBV, QF_AUFLIA, QF_ALIA, QF_AX,
- QF_AUFBVLIRA,
-- QF_NRA, QF_NIA, UFBV, BV,
-- ])
-+ QF_NRA, QF_NIA, QF_NIRA, UFBV, BV,
-+ ])
-
- # PySMT Logics includes additional features:
- # - constant arrays: QF_AUFBV becomes QF_AUFBV*
-@@ -697,7 +703,6 @@ for l in PYSMT_LOGICS:
- ext_logics.add(nl)
-
-
--
- LOGICS =3D LOGICS | frozenset(ext_logics)
- PYSMT_LOGICS =3D PYSMT_LOGICS | frozenset(ext_logics)
-
-diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
-index 3fb42b9..210b771 100644
---- a/pysmt/solvers/z3.py
-+++ b/pysmt/solvers/z3.py
-@@ -595,6 +595,8 @@ class Z3Converter(Converter, DagWalker):
- None, None,
- 0, None,
- expr.ast)
-+ print("Z3: SMTLIB")
-+ print(s)
- stream_in =3D StringIO(s)
- r =3D parser.get_script(stream_in).get_last_formula(self.mgr)
- key =3D (askey(expr), None)
-diff --git a/pysmt/test/examples.py b/pysmt/test/examples.py
-index 73455ee..b653185 100644
---- a/pysmt/test/examples.py
-+++ b/pysmt/test/examples.py
-@@ -898,12 +898,12 @@ def get_full_example_formulae(environment=3DNone):
- logic=3Dpysmt.logics.QF_NRA
- ),
-
-- Example(hr=3D"((p ^ 2) =3D 0)",
-- expr=3DEquals(Pow(p, Int(2)), Int(0)),
-+ Example(hr=3D"((p ^ 2) =3D 0.0)",
-+ expr=3DEquals(Pow(p, Int(2)), Real(0)),
- is_valid=3DFalse,
- is_sat=3DTrue,
-- logic=3Dpysmt.logics.QF_NIA
-- ),
-+ logic=3Dpysmt.logics.QF_NIRA
-+ ),
-
- Example(hr=3D"((r ^ 2.0) =3D 0.0)",
- expr=3DEquals(Pow(r, Real(2)), Real(0)),
-diff --git a/pysmt/test/test_back.py b/pysmt/test/test_back.py
-index bceb45b..7a0ad63 100644
---- a/pysmt/test/test_back.py
-+++ b/pysmt/test/test_back.py
-@@ -55,10 +55,10 @@ class TestBasic(TestCase):
- res =3D msat.converter.back(term)
- self.assertFalse(f =3D=3D res)
-
-- def do_back(self, solver_name, z3_string_buffer=3DFalse):
-+ def do_back(self, solver_name, via_smtlib=3DFalse):
- for formula, _, _, logic in get_example_formulae():
- if logic.quantifier_free:
-- if logic.theory.custom_type and z3_string_buffer:
-+ if logic.theory.custom_type and via_smtlib:
- # Printing of declare-sort from Z3 is not conformant
- # with the SMT-LIB. We might consider extending our
- # parser.
-@@ -67,7 +67,7 @@ class TestBasic(TestCase):
- s =3D Solver(name=3Dsolver_name, logic=3Dlogic)
- term =3D s.converter.convert(formula)
- if solver_name =3D=3D "z3":
-- if z3_string_buffer:
-+ if via_smtlib:
- res =3D s.converter.back_via_smtlib(term)
- else:
- res =3D s.converter.back(term)
-@@ -84,8 +84,8 @@ class TestBasic(TestCase):
-
- @skipIfSolverNotAvailable("z3")
- def test_z3_back_formulae(self):
-- self.do_back("z3", z3_string_buffer=3DFalse)
-- self.do_back("z3", z3_string_buffer=3DTrue)
-+ self.do_back("z3", via_smtlib=3DTrue)
-+ self.do_back("z3", via_smtlib=3DFalse)
-
-
- if __name__ =3D=3D '__main__':
-diff --git a/pysmt/type_checker.py b/pysmt/type_checker.py
-index b700fcf..7ce05aa 100644
---- a/pysmt/type_checker.py
-+++ b/pysmt/type_checker.py
-@@ -33,6 +33,8 @@ class SimpleTypeChecker(walkers.DagWalker):
-
- def __init__(self, env=3DNone):
- walkers.DagWalker.__init__(self, env=3Denv)
-+ # Return None if the type cannot be computed rather than
-+ # raising an exception.
- self.be_nice =3D False
-
- def _get_key(self, formula, **kwargs):
-@@ -42,7 +44,7 @@ class SimpleTypeChecker(walkers.DagWalker):
- """ Returns the pysmt.types type of the formula """
- res =3D self.walk(formula)
- if not self.be_nice and res is None:
-- raise PysmtTypeError("The formula '%s' is not well-formed" \
-+ raise PysmtTypeError("The formula '%s' is not well-formed"
- % str(formula))
- return res
-
-@@ -114,7 +116,7 @@ class SimpleTypeChecker(walkers.DagWalker):
-
- def walk_bv_comp(self, formula, args, **kwargs):
- # We check that all children are BV and the same size
-- a,b =3D args
-+ a, b =3D args
- if a !=3D b or (not a.is_bv_type()):
- return None
- return BVType(1)
-@@ -187,7 +189,7 @@ class SimpleTypeChecker(walkers.DagWalker):
- if args[0].is_bool_type():
- raise PysmtTypeError("The formula '%s' is not well-formed."
- "Equality operator is not supported for =
Boolean"
-- " terms. Use Iff instead." \
-+ " terms. Use Iff instead."
- % str(formula))
- elif args[0].is_bv_type():
- return self.walk_bv_to_bool(formula, args)
-@@ -324,10 +326,7 @@ class SimpleTypeChecker(walkers.DagWalker):
- def walk_pow(self, formula, args, **kwargs):
- if args[0] !=3D args[1]:
- return None
-- # Exponent must be positive for INT
-- if args[0].is_int_type() and formula.arg(1).constant_value() < 0 :
-- return None
-- return args[0]
-+ return REAL
-
- # EOC SimpleTypeChecker
-
diff --git a/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-tes=
t.patch b/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.p=
atch
deleted file mode 100644
index eee555f807..0000000000
--- a/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch
+++ /dev/null
@@ -1,86 +0,0 @@
-Backport of an upstream patch fixing a test suite failure.
-
-Taken from: https://github.com/pysmt/pysmt/commit/a246669a487aff69f5da3457=
0ef867841d18508a
-
-diff --git a/pysmt/test/smtlib/test_parser_examples.py b/pysmt/test/smtlib=
/test_parser_examples.py
-index cca4194..c0852be 100644
---- a/pysmt/test/smtlib/test_parser_examples.py
-+++ b/pysmt/test/smtlib/test_parser_examples.py
-@@ -29,6 +29,7 @@ from pysmt.shortcuts import Iff
- from pysmt.shortcuts import read_smtlib, write_smtlib, get_env
- from pysmt.exceptions import PysmtSyntaxError
-
-+
- class TestSMTParseExamples(TestCase):
-
- def test_parse_examples(self):
-@@ -41,7 +42,6 @@ class TestSMTParseExamples(TestCase):
- buf =3D StringIO()
- script_out =3D smtlibscript_from_formula(f_out)
- script_out.serialize(outstream=3Dbuf)
-- #print(buf)
-
- buf.seek(0)
- parser =3D SmtLibParser()
-@@ -49,7 +49,6 @@ class TestSMTParseExamples(TestCase):
- f_in =3D script_in.get_last_formula()
- self.assertEqual(f_in.simplify(), f_out.simplify())
-
--
- @skipIfNoSolverForLogic(logics.QF_BV)
- def test_parse_examples_bv(self):
- """For BV we represent a superset of the operators defined in SMT=
-LIB.
-@@ -108,7 +107,18 @@ class TestSMTParseExamples(TestCase):
- self.assertValid(Iff(f_in, f_out), f_in.serialize())
-
- def test_dumped_logic(self):
-- # Dumped logic matches the logic in the example
-+ # Dumped logic matches the logic in the example.
-+ #
-+ # There are a few cases where we use a logic
-+ # that does not exist in SMT-LIB, and the SMT-LIB
-+ # serialization logic will find a logic that
-+ # is more expressive. We need to adjust the test
-+ # for those cases (see rewrite dict below).
-+ rewrite =3D {
-+ logics.QF_BOOL: logics.QF_UF,
-+ logics.BOOL: logics.LRA,
-+ logics.QF_NIRA: logics.AUFNIRA,
-+ }
- fs =3D get_example_formulae()
-
- for (f_out, _, _, logic) in fs:
-@@ -121,14 +131,9 @@ class TestSMTParseExamples(TestCase):
- for cmd in script_in:
- if cmd.name =3D=3D "set-logic":
- logic_in =3D cmd.args[0]
-- if logic =3D=3D logics.QF_BOOL:
-- self.assertEqual(logic_in, logics.QF_UF)
-- elif logic =3D=3D logics.BOOL:
-- self.assertEqual(logic_in, logics.LRA)
-- else:
-- self.assertEqual(logic_in, logic, script_in)
-+ self.assertEqual(logic_in, rewrite.get(logic, logic))
- break
-- else: # Loops exited normally
-+ else: # Loops exited normally
- print("-"*40)
- print(script_in)
-
-@@ -136,7 +141,7 @@ class TestSMTParseExamples(TestCase):
- fs =3D get_example_formulae()
-
- fdi, tmp_fname =3D mkstemp()
-- os.close(fdi) # Close initial file descriptor
-+ os.close(fdi) # Close initial file descriptor
- for (f_out, _, _, _) in fs:
- write_smtlib(f_out, tmp_fname)
- # with open(tmp_fname) as fin:
-@@ -197,7 +202,6 @@ class TestSMTParseExamples(TestCase):
- f_in =3D script.get_last_formula()
- self.assertSat(f_in)
-
--
- def test_int_promotion_define_fun(self):
- script =3D """
- (define-fun x () Int 8)
diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 763b0fee77..dc175d7a49 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -161,6 +161,7 @@
;;; Copyright =C2=A9 2024 Markku Korkeala <markku.korkeala@HIDDEN>
;;; Copyright =C2=A9 2025 Jordan Moore <lockbox@HIDDEN>
;;; Copyright =C2=A9 2025 Dariqq <dariqq@HIDDEN>
+;;; Copyright =C2=A9 2025 Nguy=E1=BB=85n Gia Phong <mcsinyx@HIDDEN>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -36112,19 +36113,17 @@ (define-public python-claripy
(define-public python-pysmt
(package
(name "python-pysmt")
- (version "0.9.5")
+ (version "0.9.6")
(source
(origin
;; Fetching from Git as pypi release doesn't include all test files.
(method git-fetch)
- (patches (search-patches "python-pysmt-fix-pow-return-type.patch"
- "python-pysmt-fix-smtlib-serialization-test.patch"))
(uri (git-reference
(url "https://github.com/pysmt/pysmt")
(commit (string-append "v" version))))
(file-name (git-file-name name version))
(sha256
- (base32 "0hrxv23y5ip4ijfx5pvbwc2fq4zg9jz42wc9zqgqm0g0mjc9ckvh"))))
+ (base32 "0jiw8pa6hfh9ajr953q187qgpdnk3bvaa3wmrxs8ilw5jc41sq8y"))))
(build-system pyproject-build-system)
(arguments
`(#:phases (modify-phases %standard-phases
--
2.48.1
--
Best regards,
Nicolas Graves
X-Loop: help-debbugs@HIDDEN
Subject: [bug#75476] QA review for 75476
References: <2ed2dee408f62e2498758555d01bb603dfa866f4.1736513961.git.mcsinyx@HIDDEN>
In-Reply-To: <2ed2dee408f62e2498758555d01bb603dfa866f4.1736513961.git.mcsinyx@HIDDEN>
Resent-From: Nicolas Graves <ngraves@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Sun, 02 Feb 2025 15:10:02 +0000
Resent-Message-ID: <handler.75476.B75476.17385089661229 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 75476
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: control <at> debbugs.gnu.org,75476 <at> debbugs.gnu.org
Received: via spool by 75476-submit <at> debbugs.gnu.org id=B75476.17385089661229
(code B ref 75476); Sun, 02 Feb 2025 15:10:02 +0000
Received: (at 75476) by debbugs.gnu.org; 2 Feb 2025 15:09:26 +0000
Received: from localhost ([127.0.0.1]:35831 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1tebbB-0000Jg-Qy
for submit <at> debbugs.gnu.org; Sun, 02 Feb 2025 10:09:26 -0500
Received: from 1.mo560.mail-out.ovh.net ([46.105.63.121]:45045)
by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.84_2) (envelope-from <ngraves@HIDDEN>)
id 1tebb8-0000JM-JI
for 75476 <at> debbugs.gnu.org; Sun, 02 Feb 2025 10:09:24 -0500
Received: from director11.ghost.mail-out.ovh.net (unknown [10.109.139.183])
by mo560.mail-out.ovh.net (Postfix) with ESMTP id 4YmChc5Bm8z1bm9
for <75476 <at> debbugs.gnu.org>; Sun, 2 Feb 2025 15:09:20 +0000 (UTC)
Received: from ghost-submission-5b5ff79f4f-d2fmc (unknown [10.110.178.131])
by director11.ghost.mail-out.ovh.net (Postfix) with ESMTPS id 2EE741FE4B;
Sun, 2 Feb 2025 15:09:20 +0000 (UTC)
Received: from ngraves.fr ([37.59.142.113])
by ghost-submission-5b5ff79f4f-d2fmc with ESMTPSA
id OG0fN5+Kn2d/uQUAuLUdPw
(envelope-from <ngraves@HIDDEN>); Sun, 02 Feb 2025 15:09:20 +0000
Authentication-Results: garm.ovh; auth=pass
(GARM-113S00746bc9cbf-1dd1-4701-b737-cad0d34d4902,
0EB4F4ACF34A069A1D12270FF355DD325781616A) smtp.auth=ngraves@HIDDEN
X-OVh-ClientIp: 89.207.171.131
From: Nicolas Graves <ngraves@HIDDEN>
Date: Sun, 02 Feb 2025 16:09:19 +0100
Message-ID: <87msf4l6xs.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain
X-Ovh-Tracer-Id: 9988983973794669239
X-VR-SPAMSTATE: OK
X-VR-SPAMSCORE: 0
X-VR-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrgeefvddrtddtgdduhedttdcutefuodetggdotefrodftvfcurfhrohhfihhlvgemucfqggfjpdevjffgvefmvefgnecuuegrihhlohhuthemucehtddtnecunecujfgurhephffvufffkfggtgesthdtredttddttdenucfhrhhomheppfhitgholhgrshcuifhrrghvvghsuceonhhgrhgrvhgvshesnhhgrhgrvhgvshdrfhhrqeenucggtffrrghtthgvrhhnpeeujeelieeljeffhfelteejtdeljeehveduffelvefgudefkeehgfdvvdevgeevfeenucfkphepuddvjedrtddrtddruddpkeelrddvtdejrddujedurddufedupdefjedrheelrddugedvrdduudefnecuvehluhhsthgvrhfuihiivgeptdenucfrrghrrghmpehinhgvthepuddvjedrtddrtddruddpmhgrihhlfhhrohhmpehnghhrrghvvghssehnghhrrghvvghsrdhfrhdpnhgspghrtghpthhtohepuddprhgtphhtthhopeejheegjeeiseguvggssghughhsrdhgnhhurdhorhhgpdfovfetjfhoshhtpehmohehiedtmgdpmhhouggvpehsmhhtphhouhht
DKIM-Signature: a=rsa-sha256; bh=SgTTuA2hL1ArmwC6JQASj0V++mgIVVW44Z0vwxfzOz4=;
c=relaxed/relaxed; d=ngraves.fr; h=From;
s=ovhmo4487190-selector1; t=1738508960; v=1;
b=qUtBSpElt01gfhcjk6BUFrL4gGbuqX0xBWYdCGPUKnuBfW+FFSN1lOjsjhmtdd4BLw8EKMUr
kleX4TagA9zZD+ttWOh2XFtwVZM5fXomgLU9w7ZxNpAcInlO+Wz7UhYrIqLJcBCX9gGC5MRBTzE
PJGnCEo1kJChHNg4+8o+KJp8msSFU8GHh3icrfyW4h2+hGgCCOjeAapkCWeBDhl3QAu+rb4cOrK
7DD88pb/72ISDWow1MJP2l9eH1LQAfA82hxWqHNyb+Y/oa2O5hngpzXzmpc3o1f7pr1aLaKc2JE
O5EDzeJzQDix42oUEE1q3Ubsd2sLmAB7NCoroYoChTBWA==
X-Spam-Score: -0.0 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)
user guix
usertag 75476 + reviewed-looks-good
thanks
Guix QA review form submission:
I've just resent a version to fix git conflicts. Tested on x86-64, lints too. LGTM.
Items marked as checked: Lint warnings, Package builds, Commit messages
--
Best regards,
Nicolas Graves
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997 nCipher Corporation Ltd,
1994-97 Ian Jackson.