mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Python API: Added BVRedAnd, BVRedOr
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
882dbfc706
commit
1244d5a22e
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue