mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
revert the revert
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
75a40d8f8e
commit
f048cb27ba
|
@ -1861,6 +1861,15 @@ class QuantifierRef(BoolRef):
|
|||
"""
|
||||
return Z3_is_lambda(self.ctx_ref(), self.ast)
|
||||
|
||||
def __getitem__(self, arg):
|
||||
"""Return the Z3 expression `self[arg]`.
|
||||
"""
|
||||
if z3_debug():
|
||||
_z3_assert(self.is_lambda(), "quantifier should be a lambda expression")
|
||||
arg = self.sort().domain().cast(arg)
|
||||
return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
|
||||
|
||||
|
||||
def weight(self):
|
||||
"""Return the weight annotation of `self`.
|
||||
|
||||
|
@ -4274,6 +4283,9 @@ class ArrayRef(ExprRef):
|
|||
def default(self):
|
||||
return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx)
|
||||
|
||||
def is_array_sort(a):
|
||||
return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
|
||||
|
||||
|
||||
def is_array(a):
|
||||
"""Return `True` if `a` is a Z3 array expression.
|
||||
|
@ -4412,7 +4424,7 @@ def Update(a, i, v):
|
|||
proved
|
||||
"""
|
||||
if z3_debug():
|
||||
_z3_assert(is_array(a), "First argument must be a Z3 array expression")
|
||||
_z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
|
||||
i = a.domain().cast(i)
|
||||
v = a.range().cast(v)
|
||||
ctx = a.ctx
|
||||
|
@ -4425,7 +4437,7 @@ def Default(a):
|
|||
proved
|
||||
"""
|
||||
if z3_debug():
|
||||
_z3_assert(is_array(a), "First argument must be a Z3 array expression")
|
||||
_z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
|
||||
return a.default()
|
||||
|
||||
|
||||
|
@ -4456,7 +4468,7 @@ def Select(a, i):
|
|||
True
|
||||
"""
|
||||
if z3_debug():
|
||||
_z3_assert(is_array(a), "First argument must be a Z3 array expression")
|
||||
_z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
|
||||
return a[i]
|
||||
|
||||
|
||||
|
@ -4511,7 +4523,7 @@ def Ext(a, b):
|
|||
"""
|
||||
ctx = a.ctx
|
||||
if z3_debug():
|
||||
_z3_assert(is_array(a) and is_array(b), "arguments must be arrays")
|
||||
_z3_assert(is_array_sort(a) and is_array(b), "arguments must be arrays")
|
||||
return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
|
||||
|
||||
def SetHasSize(a, k):
|
||||
|
|
Loading…
Reference in a new issue