Array.pip()

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

Array.pip(SomePathIndexArray, SomeLength, SomePassThroughFunction)

• pip is push plus insert. The array is split at the nodes in SomePathIndexArray, and a slice of length SomeLength is pushed into these array indices, and the values are massaged with SomePassThroughFunction if provided.
• pip modifies the original array.
• SomePathIndexArray is array indices to refer to a specific cell in the array to be pip-ed.

Example: 1..10.pip(5,2)

1

2

3

4

5

6 7

8

9

10

MAGICSQUARE(3).pip([1,1],2).print()

[ [2,7,6 ],

[9, [5,1 ] ],

[4,3,8 ] ]

MAGICSQUARE(3).pip([1,1],2,x=>SUM(x)).print()

[ [2,7,6 ],

[9,6 ],

[4,3,8 ] ]