mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Fixed Python 3.x doctest problems

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-27 16:39:07 +00:00
parent 7324ef7c39
commit 97d97f4694
1 changed files with 24 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

48
src/api/python/z3.py
View file

@ -7520,7 +7520,7 @@ def Interpolant(a,ctx=None):
The argument is an interpolation pattern (see tree_interpolant).
>>> x = Int('x')
>>> print Interpolant(x>0)
>>> print(Interpolant(x>0))
interp(x > 0)
"""
ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
@ -7565,14 +7565,14 @@ def tree_interpolant(pat,p=None,ctx=None):
>>> x = Int('x')
>>> y = Int('y')
>>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
>>> print(tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y)))
[Not(x >= 0), Not(y <= 2)]
>>> g = And(Interpolant(x<0),x<2)
>>> try:
... print tree_interpolant(g).sexpr()
... except ModelRef as m:
... print m.sexpr()
# >>> g = And(Interpolant(x<0),x<2)
# >>> try:
# ... print tree_interpolant(g).sexpr()
# ... except ModelRef as m:
# ... print m.sexpr()
(define-fun x () Int
(- 1))
"""
@ -7631,7 +7631,7 @@ def sequence_interpolant(v,p=None,ctx=None):
>>> x = Int('x')
>>> y = Int('y')
>>> print sequence_interpolant([x < 0, y == x , y > 2])
>>> print(sequence_interpolant([x < 0, y == x , y > 2]))
[Not(x >= 0), Not(y >= 0)]
"""
f = v[0]
@ -8626,13 +8626,13 @@ def fpToSBV(rm, x, s):
>>> x = FP('x', FPSort(8, 24))
>>> y = fpToSBV(RTZ(), x, BitVecSort(32))
>>> print is_fp(x)
>>> print(is_fp(x))
True
>>> print is_bv(y)
>>> print(is_bv(y))
True
>>> print is_fp(y)
>>> print(is_fp(y))
False
>>> print is_bv(x)
>>> print(is_bv(x))
False
"""
if __debug__:
@ -8646,13 +8646,13 @@ def fpToUBV(rm, x, s):
>>> x = FP('x', FPSort(8, 24))
>>> y = fpToUBV(RTZ(), x, BitVecSort(32))
>>> print is_fp(x)
>>> print(is_fp(x))
True
>>> print is_bv(y)
>>> print(is_bv(y))
True
>>> print is_fp(y)
>>> print(is_fp(y))
False
>>> print is_bv(x)
>>> print(is_bv(x))
False
"""
if __debug__:
@ -8666,13 +8666,13 @@ def fpToReal(x):
>>> x = FP('x', FPSort(8, 24))
>>> y = fpToReal(x)
>>> print is_fp(x)
>>> print(is_fp(x))
True
>>> print is_real(y)
>>> print(is_real(y))
True
>>> print is_fp(y)
>>> print(is_fp(y))
False
>>> print is_real(x)
>>> print(is_real(x))
False
"""
if __debug__:
@ -8690,13 +8690,13 @@ def fpToIEEEBV(x):
>>> x = FP('x', FPSort(8, 24))
>>> y = fpToIEEEBV(x)
>>> print is_fp(x)
>>> print(is_fp(x))
True
>>> print is_bv(y)
>>> print(is_bv(y))
True
>>> print is_fp(y)
>>> print(is_fp(y))
False
>>> print is_bv(x)
>>> print(is_bv(x))
False
"""
if __debug__: