Array.aggregate()

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

Array.aggregate (Columns,Function, Params)

Aggregates rows by unique values in column 1, with given function to columns with the parameters specified.

IM(4)

  .fillwith(1..4)
  .aggregate(3,SUM)

gives

1 16

Total of column 3 for each row where first row has a unique value, which in this case is 1.

1 2 3 4

1 2 3 4

1 2 3 4

1 2 3 4