mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
add python visitor example in response to Stackoverflow question
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
90a7f5a4a1
commit
64b9a301ed
29
examples/python/visitor.py
Normal file
29
examples/python/visitor.py
Normal file
|
@ -0,0 +1,29 @@
|
||||||
|
# Copyright (c) Microsoft Corporation 2015
|
||||||
|
|
||||||
|
from z3 import *
|
||||||
|
|
||||||
|
def visitor(e, seen):
|
||||||
|
if e in seen:
|
||||||
|
return
|
||||||
|
seen[e] = True
|
||||||
|
yield e
|
||||||
|
if is_app(e):
|
||||||
|
for ch in e.children():
|
||||||
|
for e in visitor(ch, seen):
|
||||||
|
yield e
|
||||||
|
return
|
||||||
|
if is_quantifier(e):
|
||||||
|
for e in visitor(e.body(), seen):
|
||||||
|
yield e
|
||||||
|
return
|
||||||
|
|
||||||
|
x, y = Ints('x y')
|
||||||
|
fml = x + x + y > 2
|
||||||
|
seen = {}
|
||||||
|
for e in visitor(fml, seen):
|
||||||
|
if is_const(e) and e.decl().kind() == Z3_OP_UNINTERPRETED:
|
||||||
|
print "Variable", e
|
||||||
|
else:
|
||||||
|
print e
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue