[bug#69074] [PATCH v3 06/14] gnu: Add python-pysmt.

[soeren@soeren-tempel.net]

From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/patches/python-pysmt-fix-pow-return-type.patch:
New patch.
* gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch:
New patch.
* gnu/local.mk (dist_patch_DATA): Add them.
* gnu/packages/python-xyz.scm (python-pysmt): New variable.
---
 gnu/local.mk                                  |   2 +
 .../python-pysmt-fix-pow-return-type.patch    | 258 ++++++++++++++++++
 ...-pysmt-fix-smtlib-serialization-test.patch |  86 ++++++
 gnu/packages/python-xyz.scm                   |  32 +++
 4 files changed, 378 insertions(+)
 create mode 100644 gnu/packages/patches/python-pysmt-fix-pow-return-type.patch
 create mode 100644 gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch

diff --git a/gnu/local.mk b/gnu/local.mk
index 11f393dac0..3327161547 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1972,6 +1972,8 @@ dist_patch_DATA =						\
   %D%/packages/patches/python-pyan3-fix-absolute-path-bug.patch \
   %D%/packages/patches/python-pyan3-fix-positional-arguments.patch \
   %D%/packages/patches/python-pygpgme-fix-pinentry-tests.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
new file mode 100644
index 0000000000..0ec2d41b3c
--- /dev/null
+++ b/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch
@@ -0,0 +1,258 @@
+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
new file mode 100644
index 0000000000..eee555f807
--- /dev/null
+++ b/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch
@@ -0,0 +1,86 @@
+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 0033f4df0f..3e55b5f661 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -33804,6 +33804,38 @@ (define-public python-opcodes
 and BMI2).")
       (license license:bsd-2))))
 
+(define-public python-pysmt
+  (package
+    (name "python-pysmt")
+    (version "0.9.5")
+    (source
+     (origin
+       (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"))))
+    (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))
+    (propagated-inputs (list z3))
+    (home-page "https://github.com/pysmt/pysmt")
+    (synopsis
+     "Solver-agnostic library for SMT formula manipulation and solving")
+    (description
+     "This Python module provides a solver-agnostic abstraction for
+working with @acronym{SMT, Satisfiability Modulo Theory} formulas.  For example,
+it allows manipulation and solving such formulas.")
+    (license license:asl2.0)))
+
 (define-public python-rpyc
   (package
     (name "python-rpyc")