From 1244d5a22ef196ce730ebf9fd94970419cbdcb8d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 16 Dec 2014 15:28:52 +0000 Subject: [PATCH 1/2] 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 From d53fdb284858f331b3d577067926a626d23e8571 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 16 Dec 2014 15:36:31 +0000 Subject: [PATCH 2/2] typo Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 713226e23..720335d41 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -3820,7 +3820,7 @@ def BVRedAnd(a): return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) def BVRedOr(a): - """Return the reduction-and expression of `a`.""" + """Return the reduction-or 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)