minitest347.sk

pragma options "--bnd-inline-amnt 5 --bnd-inbits 2 --bnd-cbits 3 ";


int BASE = 4;


int[2*N] mult(int N, int[N] x, int[N] y){
    int[2*N] out = 0;
    for(int i=0; i<N; ++i){
        for(int j=0; j<N; ++j){            
            int tmp = y[i] * x[j];
            tmp = out[j + i] + tmp;
            out[j + i] = tmp % BASE;
            out[j + i + 1] = out[j + i + 1] + (tmp / BASE); 
        }           
    }       
    return out;
}



int[2*N] karatsuba(int N, int[N] x, int[N] y)  implements mult  {
    if(N % 2 != 0){ return mult(N, x, y); }
    int No2 = N/2;
    int[No2] x1, x2, y1, y2;
    int[N]  a=0, b=0, c=0;
    int[2*N] out = 0;
    
    x1=x[0::No2];  x2=x[No2::No2];
    y1=y[0::No2];  y2=y[No2::No2];
    
    a = karatsuba(No2, x1, y1);
    b = karatsuba(No2, x2, y2);
    c = karatsuba(No2, poly1(No2, x1,x2,y1,y2), poly1(No2, x1,x2,y1,y2));
    
    out = a;
    out = plus(2*N, out, shiftVect(2*N, b, N));
    repeat(??){
        int[N] t = {| a | b | c |};
        out = plus(2*N,  out, shiftVect(2*N, {| t | minus(N, t) |}  , {|N | No2 | 0|} )  );    
    }
    out = normalize(2*N, out);
    return out;
}


int[N] plus(int N, int[N] x, int[N] y){ 
    int[N] out = 0;
    for(int i = 0; i<N; ++i){
        int tmp = x[i] + y[i] + out[i];
        out[i] = tmp % BASE;
        if(i < N-1){
            out[i+1] =  tmp / BASE;
        }
    }   
    return out;
}

int[N] shiftVect(int N, int[N] in, int s){ 
        int[N] out = 0;
        for(int i=0; i<N; ++i){
            if(i >= s){
                out[i] = in[i-s];
            }
        }
        return out;
}

int[N] minus(int N, int[N] t){ 
    int[N] out = 0;
    for(int i=0; i<N; ++i){
        out[i] = -t[i]; 
    }   
    return out;
}


generator int[N] poly1(int N, int[N] a, int[N] b, int[N] c, int [N] d){
    int[N] out = 0;
    if(??){
        out = plus(N, out, {| a | minus(N,a) |}); 
    }
    if(??){
        out = plus(N, out, {| b | minus(N,b) |}); 
    }
    if(??){
        out = plus(N, out, {| c | minus(N,c) |}); 
    }
    if(??){
        out = plus(N, out, {| d | minus(N,d) |}); 
    }
    return out;
}

void print(int x){  
    if(x==0){ x = 5; }
}


    
int sgn(int i){ 
    return i >= 0 ? 1 : -1; 
}   
    
int[N] normalize(int N, int[N] in){ 
    int end = N-1;
    
    int[N] out = in;
    int s = 0;
    bit found = 0;
    for(int i = 0; i<N; ++i){
        if(!found && out[end-i]!=0){
            s = sgn(out[end-i]);
            found = 1;  
        }       
    }
    for(int i = 0; i<N-1; ++i){
        if(sgn(out[i]) != s){
            int t = BASE * s + out[i];
            out[i] = t;
            out[i+1] = out[i+1] - s; 
        }
    }       
    return out;
}




/*
*************** OUTPUT ********************
*/


void karatsuba (int N, int[N] x, int[N] y, ref int[2 * N] _out)  implements mult/*miniTestb347.sk:22*/
{
  _out = ((int[2 * N])0);
  if((N % 2) != 0)/*miniTestb347.sk:23*/
  {
    int[2 * N] _out_s8;
    mult(N, x, y, _out_s8);
    _out = _out_s8;
    return;
  }
  int No2 = N / 2;
  int[No2] x1;
  int[No2] x2;
  int[No2] y1;
  int[No2] y2;
  int[N] a;
  int[N] b;
  int[N] c;
  x1 = x[0::No2];
  x2 = x[No2::No2];
  y1 = y[0::No2];
  y2 = y[No2::No2];
  int[2 * No2] a_s10;
  karatsuba(No2, x1, y1, a_s10);
  a = ((int[N])a_s10);
  int[2 * No2] b_s12;
  karatsuba(No2, x2, y2, b_s12);
  b = ((int[N])b_s12);
  int[No2] c_s14 = ((int[No2])0);
  int[No2] out_s38;
  minus(No2, x1, out_s38);
  int[No2] out_s40;
  plus(No2, c_s14, out_s38, out_s40);
  c_s14 = ((int[No2])out_s40);
  int[No2] out_s45;
  plus(No2, c_s14, x2, out_s45);
  c_s14 = ((int[No2])out_s45);
  int[No2] c_s16 = ((int[No2])0);
  int[No2] out_s50;
  plus(No2, c_s16, y1, out_s50);
  c_s16 = ((int[No2])out_s50);
  int[No2] out_s53;
  minus(No2, y2, out_s53);
  int[No2] out_s55;
  plus(No2, c_s16, out_s53, out_s55);
  c_s16 = ((int[No2])out_s55);
  int[2 * No2] c_s18;
  karatsuba(No2, c_s14, c_s16, c_s18);
  c = ((int[N])c_s18);
  int[2 * N] out = ((int[2 * N])a);
  int[2 * N] out_s20;
  shiftVect(2 * N, b, N, out_s20);
  int[2 * N] out_s22;
  plus(2 * N, out, out_s20, out_s22);
  int[2 * N] out_s27;
  shiftVect(2 * N, c, No2, out_s27);
  int[2 * N] out_s29;
  plus(2 * N, out_s22, out_s27, out_s29);
  int[2 * N] out_s27_0;
  shiftVect(2 * N, a, No2, out_s27_0);
  int[2 * N] out_s29_0;
  plus(2 * N, out_s29, out_s27_0, out_s29_0);
  int[2 * N] out_s27_1;
  shiftVect(2 * N, b, No2, out_s27_1);
  int[2 * N] out_s29_1;
  plus(2 * N, out_s29_0, out_s27_1, out_s29_1);
  int[2 * N] out_s31;
  normalize(2 * N, out_s29_1, out_s31);
  _out = out_s31;
  return;
}
/*miniTestb347.sk:69*/

void minus (int N, int[N] t, ref int[N] _out)/*miniTestb347.sk:69*/
{
  _out = ((int[N])0);
  _out = ((int[N])0);
  for(int i = 0; i < N; i = i + 1)/*Canonical*/
  {
    _out[i] = -(t[i]);
  }
  return;
}
/*miniTestb347.sk:7*/

void mult (int N, int[N] x, int[N] y, ref int[2 * N] _out)/*miniTestb347.sk:7*/
{
  _out = ((int[2 * N])0);
  _out = ((int[2 * N])0);
  for(int i = 0; i < N; i = i + 1)/*Canonical*/
  {
    for(int j = 0; j < N; j = j + 1)/*Canonical*/
    {
      int tmp = (y[i]) * (x[j]);
      tmp = (_out[j + i]) + tmp;
      _out[j + i] = tmp % 4;
      _out[(j + i) + 1] = (_out[(j + i) + 1]) + (tmp / 4);
    }
  }
  return;
}
/*miniTestb347.sk:105*/

void normalize (int N, int[N] in, ref int[N] _out)/*miniTestb347.sk:105*/
{
  _out = ((int[N])0);
  int end = N - 1;
  _out = in;
  bit found = 0;
  int s = 0;
  for(int i = 0; i < N; i = i + 1)/*Canonical*/
  {
    if((!(found)) && ((in[end - i]) != 0))/*miniTestb347.sk:112*/
    {
      int s_s33 = 0;
      sgn(in[end - i], s_s33);
      s = s_s33;
      found = 1;
    }
  }
  for(int i_0 = 0; i_0 < (N - 1); i_0 = i_0 + 1)/*Canonical*/
  {
    int _out_s35 = 0;
    sgn(_out[i_0], _out_s35);
    if(_out_s35 != s)/*miniTestb347.sk:118*/
    {
      int t;
      t = (4 * s) + (_out[i_0]);
      _out[i_0] = t;
      _out[i_0 + 1] = (_out[i_0 + 1]) - s;
    }
  }
  return;
}
/*miniTestb347.sk:47*/

void plus (int N, int[N] x, int[N] y, ref int[N] _out)/*miniTestb347.sk:47*/
{
  _out = ((int[N])0);
  _out = ((int[N])0);
  for(int i = 0; i < N; i = i + 1)/*Canonical*/
  {
    int tmp = ((x[i]) + (y[i])) + (_out[i]);
    _out[i] = tmp % 4;
    if(i < (N - 1))/*miniTestb347.sk:52*/
    {
      _out[i + 1] = tmp / 4;
    }
  }
  return;
}
/*miniTestb347.sk:101*/

void sgn (int i, ref int _out)/*miniTestb347.sk:101*/
{
  _out = 0;
  _out = (i >= 0 ? 1 : -1);
  return;
}
/*miniTestb347.sk:59*/

void shiftVect (int N, int[N] in, int s, ref int[N] _out)/*miniTestb347.sk:59*/
{
  _out = ((int[N])0);
  _out = ((int[N])0);
  for(int i = 0; i < N; i = i + 1)/*Canonical*/
  {
    if(i >= s)/*miniTestb347.sk:62*/
    {
      _out[i] = in[i - s];
    }
  }
  return;
}