// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// Given an array a[0..N-1], compute its maximum in time O(log(N)) using O(N) //
// processors. The algorithm is similar to list ranking making use of pointer //
// jumping which is done here by index expressions.                           //
// ************************************************************************** //

macro N = 19;
macro R = 128;
macro K = log(N);
macro WidthOfLevel(i,n) = (i==0 ? n : WidthOfLevel(i-1,(n+1)/2));
macro SumOfWidths(j) = sum(i=0..j) WidthOfLevel(i,N);
macro idm(i,j) = (i==0 ? j : j+SumOfWidths(i-1));
macro isArrayMax(a,x)   = forall(i=0..N-1) (a[i] <= x);
macro isArrayMin(a,x)   = forall(i=0..N-1) (a[i] >= x);
macro contains(a,x)     = exists(i=0..N-1) (a[i] == x);
macro max(x,y) = (x<=y ? y : x);

module Maximum_OlogN([N]int{R} ?a,int{R} max) {
    [SumOfWidths(K)]nat z;
    // first row determines the N operands z[idm(0,0..N-1)]
    for(j=0..N-1)
        z[idm(0,j)] = a[j];
    // deeper levels determine the balanced binary tree 
    for(i=0..K-1)
        let(w1 = WidthOfLevel(i,N))
        let(w2 = (w1+1)/2)
        for(j=0..w2-1)
            z[idm(i+1,j)] = (2*j+1==w1 
                            ? z[idm(i,2*j)] 
                            : max(z[idm(i,2*j)],z[idm(i,2*j+1)]));
    // determine the result
    max = z[idm(K,0)];
}
drivenby {
    for(i=0..N/2-1)
        a[i] = i;
    for(i=N/2..N-1)
        a[i] = N-1-i;
    assert(contains(a,max) & isArrayMax(a,max));
}