From 1244d5a22ef196ce730ebf9fd94970419cbdcb8d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 16 Dec 2014 15:28:52 +0000 Subject: [PATCH] Python API: Added BVRedAnd, BVRedOr Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index db629cd2d..713226e23 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -3813,6 +3813,18 @@ def RepeatBitVec(n, a): _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx) +def BVRedAnd(a): + """Return the reduction-and expression of `a`.""" + if __debug__: + _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") + return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) + +def BVRedOr(a): + """Return the reduction-and expression of `a`.""" + if __debug__: + _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") + return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) + ######################################### # # Arrays