Toggle diff (414 lines)
diff --git a/gnu/local.mk b/gnu/local.mk
index fbdb285695..1946fdcbb6 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1925,6 +1925,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-runpath.patch \
%D%/packages/patches/python-pytorch-system-libraries.patch \
%D%/packages/patches/python-pytorch-1.9.0-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 5fe5c0d60a..055f7ea553 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -32303,6 +32303,40 @@ (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
+ (replace 'check
+ (lambda* (#:key tests? #:allow-other-keys)
+ (when tests?
+ (setenv "PYSMT_SOLVER" "z3")
+ (invoke "python" "-m" "pytest" "pysmt" "-v")))))))
+ (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 Satisfiability Modulo Theory (SMT) formulas For example,
+it allows manipulation and solving such formulas.")
+ (license license:asl2.0)))
+
(define-public python-rpyc
(package
(name "python-rpyc")
