mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 08:17:37 +00:00
Code Activity

update examples to use arrays

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-02-19 13:57:43 -08:00
parent c94eb5dc88
commit ee03533c3a
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/python/z3/z3.py
View file

@ -5438,7 +5438,7 @@ def FiniteSetSubset(s1, s2):
def FiniteSetMap(f, set):
"""Apply function f to all elements of the finite set.
>>> f = Function('f', IntSort(), IntSort())
>>> f = Array('f', IntSort(), IntSort())
>>> a = Const('a', FiniteSetSort(IntSort()))
>>> FiniteSetMap(f, a)
set.map(f, a)
@ -5451,7 +5451,7 @@ def FiniteSetMap(f, set):
def FiniteSetFilter(f, set):
"""Filter a finite set using predicate f.
>>> f = Function('f', IntSort(), BoolSort())
>>> f = Array('f', IntSort(), BoolSort())
>>> a = Const('a', FiniteSetSort(IntSort()))
>>> FiniteSetFilter(f, a)
set.filter(f, a)