1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
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)
|
