From patchwork Fri Jan 10 12:59:21 2025 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: "King, Spencer via Guix-patches\" via" X-Patchwork-Id: 36871 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id C2A0827BBE2; Fri, 10 Jan 2025 13:00:51 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-6.4 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,MAILING_LIST_MULTI,RCVD_IN_DNSWL_BLOCKED, RCVD_IN_VALIDITY_CERTIFIED,RCVD_IN_VALIDITY_RPBL,RCVD_IN_VALIDITY_SAFE, SPF_HELO_PASS,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 9924927BBE9 for ; Fri, 10 Jan 2025 13:00:46 +0000 (GMT) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1tWEcb-0004QH-MH; Fri, 10 Jan 2025 08:00:17 -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 ) id 1tWEcZ-0004Pc-2s for guix-patches@gnu.org; Fri, 10 Jan 2025 08:00:15 -0500 Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1tWEcY-0001qH-Nd; Fri, 10 Jan 2025 08:00:14 -0500 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=debbugs.gnu.org; s=debbugs-gnu-org; h=MIME-Version:Date:From:To:Subject; bh=+gHOkzzVdKApKBmvCzQjulQWqUWnnAUyPnkgpEPU0LE=; b=WABBVgQnwCv1UJFTw3pD9wCkZj3BnhSjBomROQwo2LJdDkwU55SjJ3oDeuAkoCeHOxVl7pGKiwo++vVmBWQSYlRWUiDlOX25GFu+1uyR7Um3cI5/srNUohH6lcbZajyPCO4GGq0+H+Isp4GdfBzB5MXnom7FV4TNZBkiLbHYAais3NTSetjO19ZbVEGtWqFPeL7rzqd3V2ianSLGN98Zt+C+7lu3SvXlvutfiqwWXFvNhs0L+E+gYuAyCB/j+qar5JEC7kaLq+kb8VS0ZRjm/i+yPmuUhSVv8q4La78b6kE14j3a/8gpw5LOBNkSj8dFYuTNMgW1feJ1TICtX5N63w==; Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1tWEcN-00009e-1H; Fri, 10 Jan 2025 08:00:03 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#75476] [PATCH] gnu: python-pysmt: Update to 0.9.6. Resent-From: =?utf-8?b?Tmd1eeG7hW4=?= Gia Phong Original-Sender: "Debbugs-submit" Resent-CC: lars@6xq.net, marius@gnu.org, me@bonfacemunyoki.com, sharlatanus@gmail.com, tanguy@bioneland.org, jgart@dismail.de, guix-patches@gnu.org Resent-Date: Fri, 10 Jan 2025 13:00:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 75476 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 75476@debbugs.gnu.org Cc: =?utf-8?b?Tmd1eeG7hW4=?= Gia Phong , Lars-Dominik Braun , Marius Bakke , Munyoki Kilyungi , Sharlatan Hellseher , Tanguy Le Carrour , jgart X-Debbugs-Original-To: guix-patches@gnu.org X-Debbugs-Original-Xcc: Lars-Dominik Braun , Marius Bakke , Munyoki Kilyungi , Sharlatan Hellseher , Tanguy Le Carrour , jgart Received: via spool by submit@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 ) id 1tWEcH-00008n-3s for submit@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 ) id 1tWEcE-00008X-Uc for submit@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 ) id 1tWEc9-0004IS-EV for guix-patches@gnu.org; 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 ) id 1tWEc6-0001aO-7e for guix-patches@gnu.org; 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== Date: Fri, 10 Jan 2025 21:59:21 +0900 Message-ID: <2ed2dee408f62e2498758555d01bb603dfa866f4.1736513961.git.mcsinyx@disroot.org> MIME-Version: 1.0 Received-SPF: pass client-ip=178.21.23.139; envelope-from=mcsinyx@disroot.org; 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-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-to: =?utf-8?b?Tmd1eeG7hW4=?= Gia Phong X-ACL-Warn: , =?utf-8?q?Nguy=E1=BB=85n_Gia_Phong_via_Guix-patches?= X-Patchwork-Original-From: guix-patches--- via From: "King, Spencer via Guix-patches\" via" Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches * 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 base-commit: 461d773adead955e2daead70cee4415f7f0f00be 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 ;;; Copyright © 2024 Markku Korkeala ;;; Copyright © 2025 Jordan Moore +;;; Copyright © 2025 Nguyễn Gia Phong ;;; ;;; 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