summaryrefslogtreecommitdiff
path: root/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch
diff options
context:
space:
mode:
Diffstat (limited to 'gnu/packages/patches/python-pysmt-fix-pow-return-type.patch')
-rw-r--r--gnu/packages/patches/python-pysmt-fix-pow-return-type.patch258
1 files changed, 258 insertions, 0 deletions
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
+
generated by cgit v1.2.3 (git 2.46.0) at 2024-08-20 01:07:27 +0000