From f90b10a0c8e7f292bbe6288452f6176d1d73e608 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Nov 2023 13:26:10 -0800 Subject: [PATCH] fix #7012 omitting constructor, simplifying operator definitions, omitting incorrect type annotations --- src/api/python/z3/z3.py | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 053fd7dd1..d029769e0 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1571,6 +1571,9 @@ class BoolRef(ExprRef): def sort(self): return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) + def __add__(self, other): + return If(self, 1, 0) + If(other, 1, 0) + def __rmul__(self, other): return self * other @@ -1584,6 +1587,17 @@ class BoolRef(ExprRef): if isinstance(other, BoolRef): other = If(other, 1, 0) return If(self, other, 0) + + def __and__(self, other): + return And(self, other) + + def __or__(self, other): + return Or(self, other) + + def __invert__(self): + return Not(self) + + def is_bool(a):