Array Index Related Functions

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

Array Index Related Functions

Array.before() Array.beforex() Array.after() Array.afterx() Array.around() Array.aroundx() Array.ith() Array.nth()

Extracts all elements before or after or around an index. Functions ending in x include the index also.

The member function ith provide the elements at the indices provided, with zero indexed indices. The member function nth provide the elements at the indices provided, with 1 indexed indices.

These member functions can be called with special symbols also.

Note all array functions have an equivalent in Global space. For example Array.after can also be called as After(array, param1, param2,...) etc.

Notation for Index Based Operators

⪪   before
⪬   beforex
⪫   after
⪭   afterx
⪥   around
Ⓘ   ith
Ⓝ   nth	

These symbols also can be used in place of the function names.