3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

This commit is contained in:
Nikolaj Bjorner 2014-12-16 11:21:24 -08:00
commit 18c3c1d9d6

View file

@ -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-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)
#########################################
#
# Arrays