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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
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
|