Array.collect()

• << Z3 Home
• Z3 Language Documentation
• Listing of Z3 Array Manipulation Member Functions

Also same as Array.suchthat()

Related to

Array.filteroncondition= function (SomeTakeDropOrAllFlag, SomeFunction, SomeParameter)

Matches are applied to element or rows in an array with SomeFunctions and SomeParameter mentioned.

Related to 0 10 - takeall

1 11 - takewhile

2 12 - dropwhile

asvector versions work on elements/arrays at the top level. The simple versions work at every element level (goes into subarrays when need be).

Each element is used to match for the following:

Array.collectwhile=Array.filteroncondition.curry(0);

Array.suchthat=Array.filteroncondition.curry(0);

Array.collect=Array.suchthat;

Array.takewhile=Array.filteroncondition.curry(1);

Array.dropwhile=Array.filteroncondition.curry(2);

Each element at top level is used to match for the following:

Array.collectwhileasvector=Array.filteroncondition.curry(10);

Array.suchthatasvector=Array.filteroncondition.curry(10);

Array.collectasvector=Array.suchthatasvector;

Array.takewhileasvector=Array.filteroncondition.curry(11);

Array.dropwhileasvector=Array.filteroncondition.curry(12);

Array.splitwhile=Array.partitiononcondition.curry(0);

Array.splitwhileasvector=Array.partitiononcondition.curry(10);

To be documented in more detail.