parker/construction.c

   1 // Constantinos Bartzis  bar@cs.uscb.edu
   2
   3 #include <dfa.h>
   4 #include <stdlib.h>
   5 #include <math.h>
   6
   7 int log_2(int x){
   8 int i;
   9 if(x<0)
  10    x*=-1;
  11 for(i=0;x>0;i++)
  12   x=x>>1;
  13 return i;
  14 }
  15
  16 struct map_ent{
  17               int i, ir; //state index
  18               int s, sr; //status: 0=not yet processed
  19                          //        1=to be expanded
  20                          //        2=done
  21                          //ir and sr are for the rejecting clone
  22               };
  23
  24 int *corresP;    //used by dfaEquivalence
  25
  26 //returns the gcd of integers x and y
  27 int gcd(int x, int y){
  28 int temp;
  29   while (y!=0){
  30     temp=x%y;
  31     x=y;
  32     y=temp;
  33     }
  34   if (x>0) return x;
  35   else return -x;
  36 }
  37
  38 //returns the sum of the coefficients for the non-zero bits up to the k-th
  39 //ith coefficient corresponds to the ith least-significant bit
  40 int count_ones(long n, int k, int *coeffs){
  41   int ones=0;
  42   for(k--;k>=0;k--){
  43     if(n&1) ones+=coeffs[k];
  44     n>>=1;
  45     }
  46 return ones;
  47 }
  48
  49 //Returns a string of length k containing the binary representation of i
  50 char *bintostr(unsigned long n, int k){
  51 char *str;
  52 str=(char *)malloc(k+1);
  53 str[k]='\0';
  54   for(k--;k>=0;k--){
  55     if(n&1) str[k]='1';
  56     else    str[k]='0';
  57     n>>=1;
  58   }
  59 return str;
  60 }
  61
  62
  63 //reduces the coefficients by dividing them with their gcd
  64 //kind: 0 for = ,  1 for <
  65 //returns 1 for contradictions
  66 int preprocess(int vars, int *coef, int *cons, int kind){
  67 int i;
  68 int temp=abs(coef[0]);
  69 for (i=1; i<vars; i++)
  70   temp=gcd(abs(coef[i]),temp);
  71 for (i=0; i<vars; i++)
  72   coef[i]=coef[i]/temp;
  73 if (kind==0){
  74   if (*cons%temp==0){
  75     *cons=*cons/temp;
  76     return 0;
  77     }
  78   else return 1;
  79   }
  80 if (kind==1){
  81   *cons=*cons+temp-1;
  82   if (*cons>=0) *cons=*cons/temp;
  83   else *cons=(*cons+1)/temp-1;
  84   return 0;
  85   }
  86 return 0;
  87 }
  88
  89
  90 //Constructs a DFA for the equation coeffs*variables+constant=0
  91 DFA *build_DFA_eq(int vars, int *coeffs, int constant, int *indices){
  92 int min, max, states, next_index, next_label, result, target,
  93 count, range;
  94 long i;
  95 unsigned long j, transitions;
  96 struct map_ent *map;
  97 char *statuces;
  98 DFA *equality, *temp;
  99 int *rev_map;
 100
 101 if (preprocess(vars, coeffs, &constant, 0)) return dfaFalse();
 102
 103 //initialization
 104
 105 min=0;
 106 max=0;
 107 for (i=0; i<vars; i++)
 108   if (coeffs[i]>0) max+=coeffs[i];
 109   else min+=coeffs[i];
 110
 111 range=max-min+1;
 112 if (constant>max) max=constant;
 113 else if(constant<min) min=constant;
 114 states=max-min+2;
 115 if(states>range*(log_2(constant)+1)+1)
 116    states=range*(log_2(constant)+1)+1;
 117
 118 rev_map=(int *)malloc((states+1)*sizeof(int));
 119 for(i=0;i<=states;i++)
 120   rev_map[i]=max+1;
 121
 122
 123 //This array maps state labels (carries) to state indices
 124 map = (struct map_ent *)malloc((max-min+2)*sizeof(struct map_ent)) -min;
 125 for(i=min; i<max+2; i++){
 126   map[i].s=0;
 127 //  map[i].i=-1;
 128   }
 129 map[constant].s=1; //the first state to be expanded
 130 next_index=0;            //the next available state index
 131 next_label=constant;     //the next available state label
 132 map[constant].i=0;
 133 rev_map[0]=constant;
 134 count=0;
 135
 136 transitions=1<<vars;  //number of transitions from each state
 137
 138 //Begin building
 139 dfaSetup(states, vars, indices);
 140
 141
 142 while(next_label<max+1){  //there is a state to expand (excuding sink)
 143   map[next_label].s=2;
 144   dfaAllocExceptions(transitions/2);
 145     for(j=0; j<transitions; j++){
 146       result=next_label+count_ones(j,vars,coeffs);
 147       if(!(result&1)){
 148         target=result/2;
 149         if(map[target].s==0){
 150            map[target].s=1;
 151            next_index++;
 152            map[target].i=next_index;
 153            rev_map[next_index]=target;
 154            }
 155         dfaStoreException(map[target].i,bintostr(j,vars));
 156         }
 157       }
 158   dfaStoreState(states-1);
 159   count++;
 160 //  for(next_label=min; (next_label<=max) &&
 161 //(map[next_label].i!=count); next_label++);
 162 //find next state to expand
 163   next_label=rev_map[count];
 164   }
 165 for(;count<states;count++){
 166   dfaAllocExceptions(0);
 167   dfaStoreState(states-1);
 168   }
 169
 170 //define accepting and rejecting states
 171 statuces=(char *)malloc(states+1);
 172 for(i=0;i<states;i++)
 173 statuces[i]='-';
 174 if (map[0].s==2) statuces[map[0].i]='+';
 175 statuces[states]='\0';
 176 temp=dfaBuild(statuces);
 177 equality=dfaMinimize(temp);
 178 dfaFree(temp);
 179 return equality;
 180 }
 181
 182
 183
 184 // Constructs a DFA for the equation coeffs*variables+constant=0
 185 // in two's complement arithmetic
 186 DFA *build_DFA_eq_2sc(int vars, int *coeffs, int constant, int *indices){
 187 int min, max, states, next_index, next_label, result, target, count;
 188 long i;
 189 unsigned long j, transitions;
 190 struct map_ent *map;
 191 char *statuces;
 192 DFA *equality, *temp;
 193
 194 if (preprocess(vars, coeffs, &constant, 0)) return dfaFalse();
 195
 196 //initialization
 197
 198 min=0;
 199 max=0;
 200 for (i=0; i<vars; i++)
 201   if (coeffs[i]>0) max+=coeffs[i];
 202   else min+=coeffs[i];
 203
 204 if (constant>max) max=constant;
 205 else if(constant<min) min=constant;
 206 states=2*max-2*min+3;
 207
 208
 209 //This array maps state labels (carries) to state indices
 210 map = (struct map_ent *)malloc(states*sizeof(struct map_ent)) -min;
 211 for(i=min; i<max+2; i++){
 212   map[i].s=0;
 213   map[i].sr=0;
 214   map[i].i=-1;
 215   map[i].ir=-1;
 216   }
 217
 218 map[constant].sr=1; //the first state to be expanded
 219 next_index=0;            //the next available state index
 220 next_label=constant;     //the next available state label
 221 map[constant].i=-1;
 222 map[constant].ir=0;
 223 count=0;
 224
 225 transitions=1<<vars;  //number of transitions from each state
 226
 227 //Begin building
 228 dfaSetup(states, vars, indices);
 229
 230
 231 while(next_label<max+1){  //there is a state to expand (excuding sink)
 232   if(map[next_label].i==count)
 233     map[next_label].s=2;
 234   else
 235     map[next_label].sr=2;
 236   dfaAllocExceptions(transitions/2);
 237     for(j=0; j<transitions; j++){
 238       result=next_label+count_ones(j,vars,coeffs);
 239       if(!(result&1)){
 240         target=result/2;
 241         if (target==next_label){
 242           if(map[target].s==0){
 243              map[target].s=1;
 244              next_index++;
 245              map[target].i=next_index;
 246              }
 247           dfaStoreException(map[target].i,bintostr(j,vars));
 248           }
 249         else {
 250           if(map[target].sr==0){
 251              map[target].sr=1;
 252              next_index++;
 253              map[target].ir=next_index;
 254              }
 255           dfaStoreException(map[target].ir,bintostr(j,vars));
 256           }
 257         }
 258       }
 259   dfaStoreState(states-1);
 260   count++;
 261   for(next_label=min; (next_label<=max) &&
 262 (map[next_label].i!=count)&&(map[next_label].ir!=count); next_label++);
 263 //find next state to expand
 264   }
 265 for(;count<states;count++){
 266   dfaAllocExceptions(0);
 267   dfaStoreState(states-1);
 268   }
 269
 270 //define accepting and rejecting states
 271 statuces=(char *)malloc(states+1);
 272 for(i=0;i<states;i++)
 273 statuces[i]='-';
 274 for(next_label=min;next_label<=max;next_label++)
 275   if (map[next_label].s==2) statuces[map[next_label].i]='+';
 276 statuces[states]='\0';
 277 temp=dfaBuild(statuces);
 278 equality=dfaMinimize(temp);
 279 dfaFree(temp);
 280 return equality;
 281 }
 282
 283 //Constructs a DFA for the inequation coeffs*variables+constant<0
 284 DFA *build_DFA_ineq(int vars, int *coeffs, int constant, int *indices){
 285 int min, max, states, next_index, next_label, result, target, count, range;
 286 long i, transitions, k;
 287 unsigned long j;
 288 struct map_ent *map;
 289 char *statuces;
 290 DFA *inequality, *temp;
 291 int *rev_map;
 292
 293 preprocess(vars, coeffs, &constant, 1);
 294
 295 //initialization
 296
 297 min=0;
 298 max=0;
 299 for (i=0; i<vars; i++)
 300   if (coeffs[i]>0) max+=coeffs[i];
 301   else min+=coeffs[i];
 302
 303 range=max-min+1;
 304 if (constant>max) max=constant;
 305 else if(constant<min) min=constant;
 306 states=max-min+1;
 307 if(states>range*(log_2(constant)+1))
 308    states=range*(log_2(constant)+1);
 309
 310 rev_map=(int *)malloc((states+1)*sizeof(int));
 311 for(i=0;i<=states;i++)
 312   rev_map[i]=max+1;
 313
 314 //This array maps state labels (carries) to state indices
 315 map = (struct map_ent *)malloc((max-min+1)*sizeof(struct map_ent)) -min;
 316 for(i=min; i<max+1; i++){
 317   map[i].s=0;
 318 //  map[i].i=-1;
 319   }
 320
 321 map[constant].s=1; //the first state to be expanded
 322 next_index=0;            //the next available state index
 323 next_label=constant;     //the next available state label
 324 map[constant].i=0;
 325 rev_map[0]=constant;
 326 count=0;
 327
 328 transitions=1<<vars;  //number of transitions from each state
 329
 330 //Begin building
 331 dfaSetup(states, vars, indices);
 332
 333
 334 while(next_label<max+1){  //there is a state to expand
 335   map[next_label].s=2;
 336   dfaAllocExceptions(transitions);
 337     for(j=0; j<transitions; j++){
 338       result=next_label+count_ones(j,vars,coeffs);
 339       if (result>=0) target=result/2;
 340       else target=(result-1)/2;
 341       if(map[target].s==0){
 342          map[target].s=1;
 343          next_index++;
 344          map[target].i=next_index;
 345          rev_map[next_index]=target;
 346          }
 347       dfaStoreException(map[target].i,bintostr(j,vars));
 348       }
 349   dfaStoreState(count);
 350   count++;
 351 //  for(next_label=min; (next_label<=max) &&
 352 //(map[next_label].i!=count); next_label++);
 353 //find next state to expand
 354   next_label=rev_map[count];
 355   }
 356 for(i=count;i<states;i++){
 357   dfaAllocExceptions(0);
 358   dfaStoreState(i);
 359   }
 360
 361 //define accepting and rejecting states
 362 statuces=(char *)malloc(states+1);
 363 for(i=0;i<count;i++){
 364   k=rev_map[i];
 365   if((k<0)&&(map[k].s==2))
 366     statuces[i]='+';
 367   else
 368     statuces[i]='-';
 369   }
 370 for(;i<states;i++)
 371 statuces[i]='0';
 372 statuces[states]='\0';
 373 temp=dfaBuild(statuces);
 374 temp->ns-=states-count;
 375 inequality=dfaMinimize(temp);
 376 return inequality;
 377 }
 378
 379
 380
 381 // Constructs a DFA for the inequation coeffs*variables+constant<0
 382 // in two's complement arithmetic
 383 DFA *build_DFA_ineq_2sc(int vars, int *coeffs, int constant, int *indices){
 384 int min, max, states, next_index, next_label, result, target, count;
 385 long i;
 386 unsigned long j, transitions;
 387 struct map_ent *map;
 388 char *statuces;
 389 DFA *inequality, *temp;
 390 int write1, overbits, label1, label2, co;
 391
 392 preprocess(vars, coeffs, &constant, 1);
 393
 394 //initialization
 395
 396 min=0;
 397 max=0;
 398 for (i=0; i<vars; i++)
 399   if (coeffs[i]>0) max+=coeffs[i];
 400   else min+=coeffs[i];
 401
 402 if (constant>max) max=constant;
 403 else if(constant<min) min=constant;
 404 states=max-min+1;
 405 overbits=ceil(log(states)/log(2));
 406 states*=2;
 407
 408 //This array maps state labels (carries) to state indices
 409 map = (struct map_ent *)malloc(states*sizeof(struct map_ent)) -min;
 410 for(i=min; i<max+1; i++){
 411   map[i].s=0;
 412   map[i].sr=0;
 413   map[i].i=-1;
 414   map[i].ir=-1;
 415   }
 416
 417 map[constant].sr=1; //the first state to be expanded
 418 next_index=0;            //the next available state index
 419 next_label=constant;     //the next available state label
 420 map[constant].i=-1;
 421 map[constant].ir=0;
 422 count=0;
 423
 424 transitions=1<<vars;  //number of transitions from each state
 425
 426 //Begin building
 427 dfaSetup(states, vars, indices);
 428
 429
 430 while(next_label<max+1){  //there is a state to expand (excuding sink)
 431   if(map[next_label].i==count)
 432     map[next_label].s=2;
 433   else
 434     map[next_label].sr=2;
 435   dfaAllocExceptions(transitions);
 436     for(j=0; j<transitions; j++){
 437       co=count_ones(j,vars,coeffs);
 438       result=next_label+co;
 439       if (result>=0) target=result/2;
 440       else target=(result-1)/2;
 441       write1=result&1;
 442       label1=next_label;
 443       label2=target;
 444
 445       while(label1!=label2){
 446         label1=label2;
 447         result=label1+co;
 448         if (result>=0) label2=result/2;
 449         else label2=(result-1)/2;
 450         write1=result&1;
 451         }
 452
 453       if (write1) {
 454         if(map[target].s==0){
 455            map[target].s=1;
 456            next_index++;
 457            map[target].i=next_index;
 458            }
 459         dfaStoreException(map[target].i,bintostr(j,vars));
 460         }
 461       else {
 462         if(map[target].sr==0){
 463            map[target].sr=1;
 464            next_index++;
 465            map[target].ir=next_index;
 466            }
 467         dfaStoreException(map[target].ir,bintostr(j,vars));
 468         }
 469       }
 470   dfaStoreState(count);
 471   count++;
 472   for(next_label=min; (next_label<=max) &&
 473 (map[next_label].i!=count)&&(map[next_label].ir!=count); next_label++);
 474 //find next state to expand
 475   }
 476 for(i=count;i<states;i++){
 477   dfaAllocExceptions(0);
 478   dfaStoreState(i);
 479   }
 480
 481 //define accepting and rejecting states
 482 statuces=(char *)malloc(states+1);
 483 for(i=0;i<states;i++)
 484 statuces[i]='-';
 485 for(next_label=min;next_label<=max;next_label++)
 486   if (map[next_label].s==2) statuces[map[next_label].i]='+';
 487 statuces[states]='\0';
 488 temp=dfaBuild(statuces);
 489 temp->ns-=states-count;
 490 inequality=dfaMinimize(temp);
 491 return inequality;
 492 }
 493
 494 //recursively checks if state sa of a is equivalent to state sb of b
 495 int check(DFA *a, DFA *b, bdd_ptr sa, bdd_ptr sb){
 496 int leafa, leafb, nexta, nextb;
 497 bdd_manager *abddm, *bbddm;
 498 unsigned indexa, indexb;
 499
 500 abddm=a->bddm;
 501 bbddm=b->bddm;
 502
 503 leafa=bdd_is_leaf(abddm, sa);
 504 leafb=bdd_is_leaf(bbddm, sb);
 505
 506 if (leafa && leafb) {     //both are leaf BDD nodes poining to next state
 507   nexta=bdd_leaf_value(abddm,sa);
 508   nextb=bdd_leaf_value(bbddm,sb);
 509   if (corresP[nexta]==-1){
 510      if (a->f[nexta]!=b->f[nextb]) return 0;
 511      corresP[nexta]=nextb;
 512      if (!check(a,b,a->q[nexta],b->q[nextb])) return 0;
 513      }
 514   else return corresP[nexta]==nextb;
 515   }
 516 else if (leafa || leafb){ //one is a leaf but the other is not
 517   return 0;
 518   }
 519 else {                    //both are internal BDD nodes
 520   LOAD_index(&abddm->node_table[sa], indexa);
 521   LOAD_index(&bbddm->node_table[sb], indexb);
 522   if(indexa!=indexb) return 0;
 523   return check(a,b,bdd_then(abddm,sa),bdd_then(bbddm,sb)) &&
 524          check(a,b,bdd_else(abddm,sa),bdd_else(bbddm,sb));
 525   }
 526 return 1;
 527 }
 528
 529
 530 // A DFA that accepts everything except for the null (empty) string
 531 DFA *dfaNotNullString(){
 532
 533 dfaSetup(2,0,NULL);
 534
 535 dfaAllocExceptions(0);
 536 dfaStoreState(1);
 537 dfaAllocExceptions(0);
 538 dfaStoreState(1);
 539
 540 return dfaBuild("-+");
 541 }
 542
 543
 544 //checks if L(A)=L(B)
 545 int dfaEquivalence(DFA *A, DFA *B){
 546 int i, nsa, nsb;
 547 DFA *a, *b, *temp, *t;
 548
 549
 550 if ((A->f[A->s]==1)&&(B->f[B->s]==-1)){
 551   t=dfaNotNullString();
 552   temp=dfaProduct(A,t,dfaAND);
 553   a=dfaMinimize(temp);
 554   dfaFree(temp);
 555   dfaFree(t);
 556   b=dfaMinimize(B);
 557   }
 558 else if ((A->f[A->s]==-1)&&(B->f[B->s]==1)){
 559   t=dfaNotNullString();
 560   temp=dfaProduct(B,t,dfaAND);
 561   b=dfaMinimize(temp);
 562   dfaFree(temp);
 563   dfaFree(t);
 564   a=dfaMinimize(A);
 565   }
 566 else{
 567   a=dfaMinimize(A);
 568   b=dfaMinimize(B);
 569   }
 570
 571 nsa=a->ns;
 572 nsb=b->ns;
 573 if(nsa!=nsb)
 574   return 0;
 575 corresP=(int *)malloc(nsa*sizeof(int));
 576 for(i=0;i<nsa;i++)
 577   corresP[i]=-1;
 578 corresP[a->s]=b->s;
 579 i= check(a, b, a->q[a->s], b->q[b->s]);
 580 free(corresP);
 581 dfaFree(a);
 582 dfaFree(b);
 583 return i;
 584 }
 585
 586