mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 09:56:15 +00:00
Code Activity

doc fix for interpolation bindings for python

Browse source
This commit is contained in:
Ken McMillan 2014-08-06 15:34:58 -07:00
parent 6880945435
commit e17af8a5de
1 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -7306,6 +7306,14 @@ def tree_interpolant(pat,p=None,ctx=None):
>>> y = Int('y') >>> y = Int('y')
>>> print tree_interpolant(And(Interp(x < 0), Interp(y > 2), x == y)) >>> print tree_interpolant(And(Interp(x < 0), Interp(y > 2), x == y))
[Not(x >= 0), Not(y <= 2)] [Not(x >= 0), Not(y <= 2)]
>>> g = And(Interp(x<0),x<2)
>>> try:
... print tree_interpolant(g).sexpr()
... except ModelRef as m:
... print m.sexpr()
(define-fun x () Int
(- 1))
""" """
f = pat f = pat
ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx)) ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
@ -7364,14 +7372,6 @@ def sequence_interpolant(v,p=None,ctx=None):
>>> y = Int('y') >>> 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)] [Not(x >= 0), Not(y >= 0)]
>>> g = And(Interp(x<0),x<2)
>>> try:
... print tree_interpolant(g).sexpr()
... except ModelRef as m:
... print m.sexpr()
(define-fun x () Int
(- 1))
""" """
f = v[0] f = v[0]
for i in range(1,len(v)): for i in range(1,len(v)):