Package: guix-patches;
Reported by: Nguyễn Gia Phong <mcsinyx <at> disroot.org>
Date: Fri, 10 Jan 2025 13:00:02 UTC
Severity: normal
Tags: patch
Done: Leo Famulari <leo <at> famulari.name>
Bug is archived. No further changes may be made.
To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 75476 in the body.
You can then email your comments to 75476 AT debbugs.gnu.org in the normal way.
Toggle the display of automated, internal messages from the tracker.
View this report as an mbox folder, status mbox, maintainer mbox
lars <at> 6xq.net, marius <at> gnu.org, me <at> bonfacemunyoki.com, sharlatanus <at> gmail.com, tanguy <at> bioneland.org, jgart <at> dismail.de, guix-patches <at> gnu.org:bug#75476; Package guix-patches.
(Fri, 10 Jan 2025 13:00:03 GMT) Full text and rfc822 format available.Nguyễn Gia Phong <mcsinyx <at> disroot.org>:lars <at> 6xq.net, marius <at> gnu.org, me <at> bonfacemunyoki.com, sharlatanus <at> gmail.com, tanguy <at> bioneland.org, jgart <at> dismail.de, guix-patches <at> gnu.org.
(Fri, 10 Jan 2025 13:00:03 GMT) Full text and rfc822 format available.Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):
From: Nguyễn Gia Phong <mcsinyx <at> disroot.org> To: guix-patches <at> gnu.org Cc: Nguyễn Gia Phong <mcsinyx <at> disroot.org> Subject: [PATCH] gnu: python-pysmt: Update to 0.9.6. Date: Fri, 10 Jan 2025 21:59:21 +0900
* 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 <at> pisemsky.site>
;;; Copyright © 2024 Markku Korkeala <markku.korkeala <at> iki.fi>
;;; Copyright © 2025 Jordan Moore <lockbox <at> struct.foo>
+;;; Copyright © 2025 Nguyễn Gia Phong <mcsinyx <at> disroot.org>
;;;
;;; 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
guix-patches <at> gnu.org:bug#75476; Package guix-patches.
(Sun, 02 Feb 2025 15:09:02 GMT) Full text and rfc822 format available.Message #8 received at 75476 <at> debbugs.gnu.org (full text, mbox):
From: ngraves <at> ngraves.fr To: 75476 <at> debbugs.gnu.org Cc: Nguyễn Gia Phong <mcsinyx <at> disroot.org> Subject: [PATCH v2] gnu: python-pysmt: Update to 0.9.6. Date: Fri, 10 Jan 2025 21:59:21 +0900
* 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.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 aa91977391..799fcb0aae 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -2109,8 +2109,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 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/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 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/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 763b0fee77..dc175d7a49 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -161,6 +161,7 @@
;;; Copyright © 2024 Markku Korkeala <markku.korkeala <at> iki.fi>
;;; Copyright © 2025 Jordan Moore <lockbox <at> struct.foo>
;;; Copyright © 2025 Dariqq <dariqq <at> posteo.net>
+;;; Copyright © 2025 Nguyễn Gia Phong <mcsinyx <at> disroot.org>
;;;
;;; 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
guix-patches <at> gnu.org:bug#75476; Package guix-patches.
(Sun, 02 Feb 2025 15:10:02 GMT) Full text and rfc822 format available.Message #11 received at 75476 <at> debbugs.gnu.org (full text, mbox):
From: Nicolas Graves <ngraves <at> ngraves.fr> To: control <at> debbugs.gnu.org,75476 <at> debbugs.gnu.org Subject: QA review for 75476 Date: Sun, 02 Feb 2025 16:09:19 +0100
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
Leo Famulari <leo <at> famulari.name>:Nguyễn Gia Phong <mcsinyx <at> disroot.org>:Message #16 received at 75476-done <at> debbugs.gnu.org (full text, mbox):
From: Leo Famulari <leo <at> famulari.name> To: Nicolas Graves <ngraves <at> ngraves.fr>, Nguyễn Gia Phong <mcsinyx <at> disroot.org> Cc: 75476-done <at> debbugs.gnu.org Subject: Re: [bug#75476] QA review for 75476 Date: Sun, 2 Feb 2025 17:06:53 -0500
On Sun, Feb 02, 2025 at 04:09:19PM +0100, Nicolas Graves via Guix-patches via wrote: > 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 Thanks for patch Nguyễn! Pushed as commit fa0ab2f70fa3a363d84f9dd795f008e632d2c145: https://git.savannah.gnu.org/cgit/guix.git/commit/?id=4fccad83875cf8f5846b181525f814ce5c240ef9 And thanks to Nicolas for the review!
Debbugs Internal Request <help-debbugs <at> gnu.org>
to internal_control <at> debbugs.gnu.org.
(Mon, 03 Mar 2025 12:24:12 GMT) Full text and rfc822 format available.
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.