me/guix
Archived
1
0
Fork 0
Code Activity

gnu: Add python-pysmt.

Browse source 
* 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.

Signed-off-by: jgart <jgart@dismail.de>
This commit is contained in:
Sören Tempel 2024-07-11 23:27:16 +02:00 • committed by jgart
parent 3ec1c66556
commit f69a5ede64
No known key found for this signature in database
GPG key ID: A52AA2B477B6DD35
4 changed files with 379 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
gnu/local.mk
View file

@ -1975,6 +1975,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 \

258
gnu/packages/patches/python-pysmt-fix-pow-return-type.patch Normal file
View file

@ -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

86
gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch Normal file
View file

@ -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)

33
gnu/packages/python-xyz.scm
View file

@ -33790,6 +33790,39 @@ instructions up to AVX-512 and SHA (including 3dnow!+, XOP, FMA3, FMA4, TBM
and BMI2).")
(license license:bsd-2))))
(define-public python-pysmt
(package
(name "python-pysmt")
(version "0.9.5")
(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"))))
(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")