Subject: [PATCH] gnu: python-pysmt: Update to 0.9.6.
From: Nguyễn Gia Phong <[email-masked]>
To: [email-masked]
Cc: Nguyễn Gia Phong <[email-masked]>
Date: Fri, 10 Jan 2025 21:59:21 +0900
List-Id: <debbugs-submit.debbugs.gnu.org>

* 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 <[email-masked]>
 ;;; Copyright © 2024 Markku Korkeala <[email-masked]>
 ;;; Copyright © 2025 Jordan Moore <[email-masked]>
+;;; Copyright © 2025 Nguyễn Gia Phong <[email-masked]>
 ;;;
 ;;; 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