Array Find Related Functions

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

Array Index Related Functions

find related functions generally use the parameters fn which is applied to elements, includefalse to pick the elements that returned a false for the function call, and a mode to use to return the value.

Mode can be "INDEX", "ELEMENT", "TRUE"/"TRUTH", "VALUE","INDEXELEMENT","INDEXELEMENTVALUE", etc. findx fn,mode,includefalse Applies a function and returns matches.

includeFalse keeps matches that returned false.

findi fn,includefalse Applies a function and returns indices of matches. finde fn,includefalse Applies a function and returns elements that matched. findie fn,includefalse Applies a function and returns index and elements that matched. findiev fn,includefalse Applies a function and returns index, elements that matched and result of the match. findiv fn,includefalse Applies a function and returns index, result of the match. findv fn,includefalse Applies a function and returns result of the match. findt fn,includefalse Applies a function and returns result of the match as true or false.

Note the different options to return just the indices of match (findi), findiv (return index and value), etc.

Notations for Find Functions

   ⒱  Find by Values        .findv
   ⒤  Find by Indices       .findi
   ⒠  Find by Elements      .finde