mirror of
https://git.in.rschanz.org/ryan77627/guix.git
synced 2024-12-25 05:48:07 -05:00
87 lines
3.3 KiB
Diff
87 lines
3.3 KiB
Diff
|
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)
|