From 64b9a301ed88782de519a9c4bb3dcdbbadcc0ae0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Dec 2015 20:09:13 -0800 Subject: [PATCH] add python visitor example in response to Stackoverflow question Signed-off-by: Nikolaj Bjorner --- examples/python/visitor.py | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 examples/python/visitor.py diff --git a/examples/python/visitor.py b/examples/python/visitor.py new file mode 100644 index 000000000..9255c6a80 --- /dev/null +++ b/examples/python/visitor.py @@ -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 + +