From a2eb8245900c84607c7e55ac501b75fb6d0407dd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Jun 2016 12:07:13 +0100 Subject: [PATCH] Added __nonzero__ and __bool__ functions to Python Z3 ASTs to enable use of Python lists (and similar). Thanks to Vlad Shcherbina for the recommendation (see http://stackoverflow.com/questions/37669576/converting-z3-cnf-formula-into-list-of-lists-representation-using-z3py/37679447?noredirect=1#comment62859886_37679447)! --- src/api/python/z3.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index c9aa9beb5..ff6e91c4a 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -292,6 +292,19 @@ class AstRef(Z3PPObject): def __hash__(self): return self.hash() + def __nonzero__(self): + return self.__bool__() + + def __bool__(self): + if is_true(self): + return True + elif is_false(self): + return False + elif is_eq(self) and self.num_args() == 2: + return self.arg(0).eq(self.arg(1)) + else: + raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.") + def sexpr(self): """Return an string representing the AST node in s-expression notation.