Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment