1/*======================================================================== 2 Copyright (C) 1996-2001 by Jorn Lind-Nielsen 3 All rights reserved 4 5 Permission is hereby granted, without written agreement and without 6 license or royalty fees, to use, reproduce, prepare derivative 7 works, distribute, and display this software and its documentation 8 for any purpose, provided that (1) the above copyright notice and 9 the following two paragraphs appear in all copies of the source code 10 and (2) redistributions, including without limitation binaries, 11 reproduce these notices in the supporting documentation. Substantial 12 modifications to this software may be copyrighted by their authors 13 and need not follow the licensing terms described here, provided 14 that the new terms are clearly indicated in all files where they apply. 15 16 IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS 17 SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, 18 INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS 19 SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE 20 ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 21 22 JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING, 23 BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND 24 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 25 ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO 26 OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR 27 MODIFICATIONS. 28========================================================================*/ 29 30/************************************************************************* 31 $Header$ 32 FILE: bvec.c 33 DESCR: Boolean vector arithmetics using BDDs 34 AUTH: Jorn Lind 35 DATE: (C) may 1999 36*************************************************************************/ 37#include <stdlib.h> 38#include "kernel.h" 39#include "bvec.h" 40 41#define DEFAULT(v) { v.bitnum=0; v.bitvec=NULL; } 42 43/************************************************************************* 44*************************************************************************/ 45 46static bvec bvec_build(int bitnum, int isTrue) 47{ 48 bvec vec; 49 int n; 50 51 vec.bitvec = NEW(BDD,bitnum); 52 vec.bitnum = bitnum; 53 if (!vec.bitvec) 54 { 55 bdd_error(BDD_MEMORY); 56 vec.bitnum = 0; 57 return vec; 58 } 59 60 for (n=0 ; n<bitnum ; n++) 61 if (isTrue) 62 vec.bitvec[n] = BDDONE; 63 else 64 vec.bitvec[n] = BDDZERO; 65 66 return vec; 67} 68 69 70#if 0 71int bvec_val2bitnum(int val) 72{ 73 int bitnum=0; 74 75 while (val > 0) 76 { 77 val >>= 1; 78 bitnum++; 79 } 80 81 return bitnum; 82} 83#endif 84 85/* 86NAME {* bvec\_copy *} 87SECTION {* bvec *} 88SHORT {* create a copy of a bvec *} 89PROTO {* bvec bvec_copy(bvec src) *} 90DESCR {* Returns a copy of {\tt src}. The result is reference counted. *} 91ALSO {* bvec\_con *} 92*/ 93bvec bvec_copy(bvec src) 94{ 95 bvec dst; 96 int n; 97 98 if (src.bitnum == 0) 99 { 100 DEFAULT(dst); 101 return dst; 102 } 103 104 dst = bvec_build(src.bitnum,0); 105 106 for (n=0 ; n<src.bitnum ; n++) 107 dst.bitvec[n] = bdd_addref( src.bitvec[n] ); 108 dst.bitnum = src.bitnum; 109 110 return dst; 111} 112 113 114/* 115NAME {* bvec\_true *} 116SECTION {* bvec *} 117SHORT {* build a vector of constant true BDDs *} 118PROTO {* bvec bvec_true(int bitnum) *} 119DESCR {* Builds a boolean vector with {\tt bitnum} elements, each of which 120 are the constant true BDD. *} 121RETURN {* The boolean vector (which is already reference counted) *} 122ALSO {* bvec\_false, bvec\_con, bvec\_var *} 123*/ 124bvec bvec_true(int bitnum) 125{ 126 return bvec_build(bitnum, 1); 127} 128 129 130/* 131NAME {* bvec\_false *} 132SECTION {* bvec *} 133SHORT {* build a vector of constant false BDDs *} 134PROTO {* bvec bvec_false(int bitnum) *} 135DESCR {* Builds a boolean vector with {\tt bitnum} elements, each of which 136 are the constant false BDD. *} 137RETURN {* The boolean vector (which is already reference counted) *} 138ALSO {* bvec\_true, bvec\_con, bvec\_var *} 139*/ 140bvec bvec_false(int bitnum) 141{ 142 return bvec_build(bitnum, 0); 143} 144 145 146/* 147NAME {* bvec\_con *} 148SECTION {* bvec *} 149SHORT {* Build a boolean vector representing an integer value *} 150PROTO {* bvec bvec_con(int bitnum, int val) *} 151DESCR {* Builds a boolean vector that represents the value {\tt val} 152 using {\tt bitnum} bits. The value will be represented with the 153 LSB at the position 0 and the MSB at position {\tt bitnum}-1.*} 154RETURN {* The boolean vector (which is already reference counted) *} 155ALSO {* bvec\_true, bvec\_false, bvec\_var *} 156*/ 157bvec bvec_con(int bitnum, int val) 158{ 159 bvec v = bvec_build(bitnum,0); 160 int n; 161 162 for (n=0 ; n<v.bitnum ; n++) 163 { 164 if (val & 0x1) 165 v.bitvec[n] = bddtrue; 166 else 167 v.bitvec[n] = bddfalse; 168 169 val = val >> 1; 170 } 171 172 return v; 173} 174 175 176/* 177NAME {* bvec\_var *} 178SECTION {* bvec *} 179SHORT {* build a boolean vector with BDD variables *} 180PROTO {* bvec bvec_var(int bitnum, int offset, int step) *} 181DESCR {* Builds a boolean vector with the BDD variables $v_1, \ldots, 182 v_n$ as the elements. Each variable will be the variabled 183 numbered {\tt offset + N*step} where {\tt N} ranges from 0 to 184 {\tt bitnum}-1.*} 185RETURN {* The boolean vector (which is already reference counted) *} 186ALSO {* bvec\_true, bvec\_false, bvec\_con *} 187*/ 188bvec bvec_var(int bitnum, int offset, int step) 189{ 190 bvec v; 191 int n; 192 193 v = bvec_build(bitnum,0); 194 195 for (n=0 ; n<bitnum ; n++) 196 v.bitvec[n] = bdd_ithvar(offset+n*step); 197 198 return v; 199} 200 201 202/* 203NAME {* bvec\_varfdd *} 204SECTION {* bvec *} 205SHORT {* build a boolean vector from a FDD variable block *} 206PROTO {* bvec bvec_varfdd(int var) *} 207DESCR {* Builds a boolean vector which will include exactly the 208 variables used to define the FDD variable block {\tt var}. The 209 vector will have the LSB at position zero. *} 210RETURN {* The boolean vector (which is already reference counted) *} 211ALSO {* bvec\_var *} 212*/ 213bvec bvec_varfdd(int var) 214{ 215 bvec v; 216 int *bddvar = fdd_vars(var); 217 int varbitnum = fdd_varnum(var); 218 int n; 219 220 if (bddvar == NULL) 221 { 222 DEFAULT(v); 223 return v; 224 } 225 226 v = bvec_build(varbitnum,0); 227 228 for (n=0 ; n<v.bitnum ; n++) 229 v.bitvec[n] = bdd_ithvar(bddvar[n]); 230 231 return v; 232} 233 234 235/* 236NAME {* bvec\_varvec *} 237SECTION {* bvec *} 238SHORT {* build a boolean vector with the variables passed in an array *} 239PROTO {* bvec bvec_varvec(int bitnum, int *var) *} 240DESCR {* Builds a boolean vector with the BDD variables listed in 241 the array {\tt var}. The array must be of size {\tt bitnum}. *} 242RETURN {* The boolean vector (which is already reference counted) *} 243ALSO {* bvec\_var *} 244*/ 245bvec bvec_varvec(int bitnum, int *var) 246{ 247 bvec v; 248 int n; 249 250 v = bvec_build(bitnum,0); 251 252 for (n=0 ; n<bitnum ; n++) 253 v.bitvec[n] = bdd_ithvar(var[n]); 254 255 return v; 256} 257 258 259/* 260NAME {* bvec\_coerce *} 261SECTION {* bvec *} 262SHORT {* adjust the size of a boolean vector *} 263PROTO {* bvec bvec_coerce(int bitnum, bvec v) *} 264DESCR {* Build a boolean vector with {\tt bitnum} elements copied from 265 {\tt v}. If the number of elements in {\tt v} is greater than 266 {\tt bitnum} then the most significant bits are removed, otherwise 267 if number is smaller then the vector is padded with constant 268 false BDDs (zeros). *} 269RETURN {* The new boolean vector (which is already reference counted) *} 270*/ 271bvec bvec_coerce(int bitnum, bvec v) 272{ 273 bvec res = bvec_build(bitnum,0); 274 int minnum = MIN(bitnum, v.bitnum); 275 int n; 276 277 for (n=0 ; n<minnum ; n++) 278 res.bitvec[n] = bdd_addref( v.bitvec[n] ); 279 280 return res; 281} 282 283 284/* 285NAME {* bvec\_isconst *} 286SECTION {* bvec *} 287SHORT {* test a vector for constant true/false BDDs *} 288PROTO {* int bvec_isconst(bvec v) *} 289DESCR {* Returns non-zero if the vector {\tt v} consists of only constant 290 true or false BDDs. Otherwise zero is returned. This test should 291 prelude any call to {\tt bvec\_val}. *} 292ALSO {* bvec\_val, bvec\_con *} 293*/ 294int bvec_isconst(bvec e) 295{ 296 int n; 297 298 for (n=0 ; n<e.bitnum ; n++) 299 if (!ISCONST(e.bitvec[n])) 300 return 0; 301 302 return 1; 303} 304 305 306/* 307NAME {* bvec\_val *} 308SECTION {* bvec *} 309SHORT {* calculate the integer value represented by a boolean vector *} 310PROTO {* int bvec_val(bvec v) *} 311DESCR {* Calculates the value represented by the bits in {\tt v} assuming 312 that the vector {\tt v} consists of only constant true 313 or false BDDs. The LSB is assumed to be at position zero. *} 314RETURN {* The integer value represented by {\tt v}. *} 315ALSO {* bvec\_isconst, bvec\_con *} 316*/ 317int bvec_val(bvec e) 318{ 319 int n, val=0; 320 321 for (n=e.bitnum-1 ; n>=0 ; n--) 322 if (ISONE(e.bitvec[n])) 323 val = (val << 1) | 1; 324 else if (ISZERO(e.bitvec[n])) 325 val = val << 1; 326 else 327 return 0; 328 329 return val; 330} 331 332 333/*======================================================================*/ 334 335/* 336NAME {* bvec\_free *} 337SECTION {* bvec *} 338SHORT {* frees all memory used by a boolean vector *} 339PROTO {* void bvec_free(bvec v) *} 340DESCR {* Use this function to release any unused boolean vectors. The 341 decrease of the reference counts on the BDDs in {\tt v} is done 342 by {\tt bvec\_free}. *} 343*/ 344void bvec_free(bvec v) 345{ 346 bvec_delref(v); 347 free(v.bitvec); 348} 349 350 351/* 352NAME {* bvec\_addref *} 353SECTION {* bvec *} 354SHORT {* increase reference count of a boolean vector *} 355PROTO {* bvec bvec_addref(bvec v) *} 356DESCR {* Use this function to increase the reference count of all BDDs 357 in a {\tt v}. Please note that all boolean vectors returned 358 from BuDDy are reference counted from the beginning. *} 359RETURN {* The boolean vector {\tt v} *} 360ALSO {* bvec\_delref *} 361*/ 362bvec bvec_addref(bvec v) 363{ 364 int n; 365 366 for (n=0 ; n<v.bitnum ; n++) 367 bdd_addref(v.bitvec[n]); 368 369 return v; 370} 371 372 373/* 374NAME {* bvec\_delref *} 375SECTION {* bvec *} 376SHORT {* decrease the reference count of a boolean vector *} 377PROTO {* bvec bvec_delref(bvec v) *} 378DESCR {* Use this function to decrease the reference count of all the 379 BDDs in {\tt v}. *} 380RETURN {* The boolean vector {\tt v} *} 381ALSO {* bvec\_addref *} 382*/ 383bvec bvec_delref(bvec v) 384{ 385 int n; 386 387 for (n=0 ; n<v.bitnum ; n++) 388 bdd_delref(v.bitvec[n]); 389 390 return v; 391} 392 393 394/*======================================================================*/ 395 396/* 397NAME {* bvec\_map1 *} 398SECTION {* bvec *} 399SHORT {* map a function onto a boolean vector *} 400PROTO {* bvec bvec_map1(bvec a, bdd (*fun)(bdd)) *} 401DESCR {* Maps the function {\tt fun} onto all the elements in {\tt a}. The 402 value returned from {\tt fun} is stored in a new vector which 403 is then returned. An example of a mapping function is 404 {\tt bdd\_not} which can be used like this\\ 405 406 \indent {\tt bvec res = bvec\_map1(a, bdd\_not)}\\ 407 408 \noindent to negate all the BDDs in {\tt a}.*} 409RETURN {* The new vector (which is already reference counted) *} 410ALSO {* bvec\_map2, bvec\_map3 *} 411*/ 412bvec bvec_map1(bvec a, BDD (*fun)(BDD)) 413{ 414 bvec res; 415 int n; 416 417 res = bvec_build(a.bitnum,0); 418 for (n=0 ; n < a.bitnum ; n++) 419 res.bitvec[n] = bdd_addref( fun(a.bitvec[n]) ); 420 421 return res; 422} 423 424 425/* 426NAME {* bvec\_map2 *} 427SECTION {* bvec *} 428SHORT {* map a function onto a boolean vector *} 429PROTO {* bvec bvec_map2(bvec a, bvec b, bdd (*fun)(bdd,bdd)) *} 430DESCR {* Maps the function {\tt fun} onto all the elements in {\tt a} and 431 {\tt b}. The value returned from {\tt fun} is stored in a new 432 vector which is then returned. An example of a mapping function 433 is {\tt bdd\_and} which can be used like this\\ 434 435 \indent {\tt bvec res = bvec\_map2(a, b, bdd\_and)}\\ 436 437 \noindent to calculate the logical 'and' of all the BDDs in 438 {\tt a} and {\tt b}. *} 439RETURN {* The new vector (which is already reference counted) *} 440ALSO {* bvec\_map1, bvec\_map3 *} 441*/ 442bvec bvec_map2(bvec a, bvec b, BDD (*fun)(BDD,BDD)) 443{ 444 bvec res; 445 int n; 446 447 DEFAULT(res); 448 if (a.bitnum != b.bitnum) 449 { 450 bdd_error(BVEC_SIZE); 451 return res; 452 } 453 454 res = bvec_build(a.bitnum,0); 455 for (n=0 ; n < a.bitnum ; n++) 456 res.bitvec[n] = bdd_addref( fun(a.bitvec[n], b.bitvec[n]) ); 457 458 return res; 459} 460 461 462/* 463NAME {* bvec\_map3 *} 464SECTION {* bvec *} 465SHORT {* map a function onto a boolean vector *} 466PROTO {* bvec bvec_map3(bvec a, bvec b, bvec c, bdd (*fun)(bdd,bdd,bdd)) *} 467DESCR {* Maps the function {\tt fun} onto all the elements in {\tt a}, 468 {\tt b} and {\tt c}. The value returned from {\tt fun} is stored 469 in a new vector which is then returned. An example of a mapping 470 function is {\tt bdd\_ite} which can be used like this\\ 471 472 \indent {\tt bvec res = bvec\_map3(a, b, c, bdd\_ite) }\\ 473 474 \noindent to calculate the if-then-else function for each element 475 in {\tt a}, {\tt b} and {\tt c}. *} 476RETURN {* The new vector (which is already reference counted) *} 477ALSO {* bvec\_map1, bvec\_map2 *} 478*/ 479bvec bvec_map3(bvec a, bvec b, bvec c, BDD (*fun)(BDD,BDD,BDD)) 480{ 481 bvec res; 482 int n; 483 484 DEFAULT(res); 485 if (a.bitnum != b.bitnum || b.bitnum != c.bitnum) 486 { 487 bdd_error(BVEC_SIZE); 488 return res; 489 } 490 491 res = bvec_build(a.bitnum,0); 492 for (n=0 ; n < a.bitnum ; n++) 493 res.bitvec[n] = bdd_addref( fun(a.bitvec[n], b.bitvec[n], c.bitvec[n]) ); 494 495 return res; 496} 497 498 499/*======================================================================*/ 500 501/* 502NAME {* bvec\_add *} 503SECTION {* bvec *} 504SHORT {* builds a boolean vector for addition *} 505PROTO {* bvec bvec_add(bvec l, bvec r) *} 506DESCR {* Builds a new boolean vector that represents the addition of two 507 other vectors. Each element $x_i$ in the result will represent 508 the function 509 \[ x_i = l_i\ \mbox{xor}\ r_i\ \mbox{xor}\ c_{i-1} \] 510 where the carry in $c_i$ is 511 \[ c_i = (l_i\ \mbox{and}\ r_i)\ \mbox{or}\ (c_{i-1}\ \mbox{and} 512 \ (l_i\ \mbox{or}\ r_i)). \] 513 It is important for efficency that the BDD 514 variables used in {\tt l} and {\tt r} are interleaved. *} 515RETURN {* The result of the addition (which is already reference counted) *} 516ALSO {* bvec\_sub, bvec\_mul, bvec\_shl *} 517*/ 518bvec bvec_add(bvec l, bvec r) 519{ 520 bvec res; 521 BDD c = bddfalse; 522 int n; 523 524 525 if (l.bitnum == 0 || r.bitnum == 0) 526 { 527 DEFAULT(res); 528 return res; 529 } 530 531 if (l.bitnum != r.bitnum) 532 { 533 bdd_error(BVEC_SIZE); 534 DEFAULT(res); 535 return res; 536 } 537 538 res = bvec_build(l.bitnum,0); 539 540 for (n=0 ; n<res.bitnum ; n++) 541 { 542 BDD tmp1, tmp2, tmp3; 543 544 /* bitvec[n] = l[n] ^ r[n] ^ c; */ 545 tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_xor) ); 546 tmp2 = bdd_addref( bdd_apply(tmp1, c, bddop_xor) ); 547 bdd_delref(tmp1); 548 res.bitvec[n] = tmp2; 549 550 /* c = (l[n] & r[n]) | (c & (l[n] | r[n])); */ 551 tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_or) ); 552 tmp2 = bdd_addref( bdd_apply(c, tmp1, bddop_and) ); 553 bdd_delref(tmp1); 554 555 tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_and) ); 556 tmp3 = bdd_addref( bdd_apply(tmp1, tmp2, bddop_or) ); 557 bdd_delref(tmp1); 558 bdd_delref(tmp2); 559 560 bdd_delref(c); 561 c = tmp3; 562 } 563 564 bdd_delref(c); 565 566 return res; 567} 568 569 570/* 571NAME {* bvec\_sub *} 572SECTION {* bvec *} 573SHORT {* builds a boolean vector for subtraction *} 574PROTO {* bvec bvec_sub(bvec l, bvec r) *} 575DESCR {* Builds a new boolean vector that represents the subtraction of two 576 other vectors. Each element $x_i$ in the result will represent 577 the function 578 \[ x_i = l_i\ \mbox{xor}\ r_i\ \mbox{xor}\ c_{i-1} \] 579 where the carry in $c_i$ is 580 \[ c_i = (l_i\ \mbox{and}\ r_i\ \mbox{and}\ c_{i-1})\ 581 \mbox{or}\ (\mbox{not}\ l_i\ \mbox{and} 582 \ (r_i\ \mbox{or}\ c_{i-1})). \] 583 It is important for efficency that the BDD 584 variables used in {\tt l} and {\tt r} are interleaved. *} 585RETURN {* The result of the subtraction (which is already reference counted) *} 586ALSO {* bvec\_add, bvec\_mul, bvec\_shl *} 587*/ 588bvec bvec_sub(bvec l, bvec r) 589{ 590 bvec res; 591 BDD c = bddfalse; 592 int n; 593 594 if (l.bitnum == 0 || r.bitnum == 0) 595 { 596 DEFAULT(res); 597 return res; 598 } 599 600 if (l.bitnum != r.bitnum) 601 { 602 bdd_error(BVEC_SIZE); 603 DEFAULT(res); 604 return res; 605 } 606 607 res = bvec_build(l.bitnum,0); 608 609 for (n=0 ; n<res.bitnum ; n++) 610 { 611 BDD tmp1, tmp2, tmp3; 612 613 /* bitvec[n] = l[n] ^ r[n] ^ c; */ 614 tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_xor) ); 615 tmp2 = bdd_addref( bdd_apply(tmp1, c, bddop_xor) ); 616 bdd_delref(tmp1); 617 res.bitvec[n] = tmp2; 618 619 /* c = (l[n] & r[n] & c) | (!l[n] & (r[n] | c)); */ 620 tmp1 = bdd_addref( bdd_apply(r.bitvec[n], c, bddop_or) ); 621 tmp2 = bdd_addref( bdd_apply(l.bitvec[n], tmp1, bddop_less) ); 622 bdd_delref(tmp1); 623 624 tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_and) ); 625 tmp3 = bdd_addref( bdd_apply(tmp1, c, bddop_and) ); 626 bdd_delref(tmp1); 627 628 tmp1 = bdd_addref( bdd_apply(tmp3, tmp2, bddop_or) ); 629 bdd_delref(tmp2); 630 bdd_delref(tmp3); 631 632 bdd_delref(c); 633 c = tmp1; 634 } 635 636 bdd_delref(c); 637 638 return res; 639} 640 641 642/* 643NAME {* bvec\_mulfixed *} 644SECTION {* bvec *} 645SHORT {* builds a boolean vector for multiplication with a constant *} 646PROTO {* bvec bvec_mulfixed(bvec e, int c) *} 647DESCR {* Builds a boolean vector representing the multiplication 648 of {\tt e} and {\tt c}. *} 649RETURN {* The result of the multiplication (which is already reference counted) *} 650ALSO {* bvec\_mul, bvec\_div, bvec\_add, bvec\_shl *} 651*/ 652bvec bvec_mulfixed(bvec e, int c) 653{ 654 bvec res, next, rest; 655 int n; 656 657 if (e.bitnum == 0) 658 { 659 DEFAULT(res); 660 return res; 661 } 662 663 if (c == 0) 664 return bvec_build(e.bitnum,0); /* return false array (base case) */ 665 666 next = bvec_build(e.bitnum,0); 667 for (n=1 ; n<e.bitnum ; n++) 668 /* e[] is never deleted, so no ref.cou. */ 669 next.bitvec[n] = e.bitvec[n-1]; 670 671 rest = bvec_mulfixed(next, c>>1); 672 673 if (c & 0x1) 674 { 675 res = bvec_add(e, rest); 676 bvec_free(rest); 677 } 678 else 679 res = rest; 680 681 bvec_free(next); 682 683 return res; 684} 685 686 687/* 688NAME {* bvec\_mul *} 689SECTION {* bvec *} 690SHORT {* builds a boolean vector for multiplication *} 691PROTO {* bvec bvec_mul(bvec l, bvec r) *} 692DESCR {* Builds a boolean vector representing the multiplication 693 of {\tt l} and {\tt r}. *} 694RETURN {* The result of the multiplication (which is already reference counted) *} 695ALSO {* bvec\_mulfixed, bvec\_div, bvec\_add, bvec\_shl *} 696*/ 697bvec bvec_mul(bvec left, bvec right) 698{ 699 int n; 700 int bitnum = left.bitnum + right.bitnum; 701 bvec res; 702 bvec leftshifttmp; 703 bvec leftshift; 704 705 if (left.bitnum == 0 || right.bitnum == 0) 706 { 707 DEFAULT(res); 708 return res; 709 } 710 711 res = bvec_false(bitnum); 712 leftshifttmp = bvec_copy(left); 713 leftshift = bvec_coerce(bitnum, leftshifttmp); 714 715 /*bvec_delref(leftshifttmp);*/ 716 bvec_free(leftshifttmp); 717 718 for (n=0 ; n<right.bitnum ; n++) 719 { 720 bvec added = bvec_add(res, leftshift); 721 int m; 722 723 for (m=0 ; m<bitnum ; m++) 724 { 725 bdd tmpres = bdd_addref( bdd_ite(right.bitvec[n], 726 added.bitvec[m], res.bitvec[m]) ); 727 bdd_delref(res.bitvec[m]); 728 res.bitvec[m] = tmpres; 729 } 730 731 /* Shift 'leftshift' one bit left */ 732 bdd_delref(leftshift.bitvec[leftshift.bitnum-1]); 733 for (m=bitnum-1 ; m>=1 ; m--) 734 leftshift.bitvec[m] = leftshift.bitvec[m-1]; 735 leftshift.bitvec[0] = bddfalse; 736 737 /*bvec_delref(added);*/ 738 bvec_free(added); 739 } 740 741 /*bvec_delref(leftshift);*/ 742 bvec_free(leftshift); 743 744 return res; 745} 746 747static void bvec_div_rec(bvec divisor, bvec *remainder, bvec *result, int step) 748{ 749 int n; 750 BDD isSmaller = bdd_addref( bvec_lte(divisor, *remainder) ); 751 bvec newResult = bvec_shlfixed( *result, 1, isSmaller ); 752 bvec zero = bvec_build(divisor.bitnum, bddfalse); 753 bvec newRemainder, tmp, sub = bvec_build(divisor.bitnum, bddfalse); 754 755 for (n=0 ; n<divisor.bitnum ; n++) 756 sub.bitvec[n] = bdd_ite(isSmaller, divisor.bitvec[n], zero.bitvec[n]); 757 758 tmp = bvec_sub( *remainder, sub ); 759 newRemainder = bvec_shlfixed(tmp, 1, result->bitvec[divisor.bitnum-1]); 760 761 if (step > 1) 762 bvec_div_rec( divisor, &newRemainder, &newResult, step-1 ); 763 764 bvec_free(tmp); 765 bvec_free(sub); 766 bvec_free(zero); 767 bdd_delref(isSmaller); 768 769 bvec_free(*remainder); 770 bvec_free(*result); 771 *result = newResult; 772 *remainder = newRemainder; 773} 774 775 776/* 777NAME {* bvec\_divfixed *} 778SECTION {* bvec *} 779SHORT {* builds a boolean vector for division by a constant *} 780PROTO {* int bvec_div(bvec e, int c, bvec *res, bvec *rem) *} 781DESCR {* Builds a new boolean vector representing the integer division 782 of {\tt e} with {\tt c}. The result of the division will be stored 783 in {\tt res} and the remainder of the division will be stored in 784 {\tt rem}. Both vectors should be initialized as the function 785 will try to release the nodes used by them. If an error occurs then 786 the nodes will {\em not} be freed. *} 787RETURN {* Zero on success or a negative error code on error. *} 788ALSO {* bvec\_div, bvec\_mul, bvec\_add, bvec\_shl *} 789*/ 790int bvec_divfixed(bvec e, int c, bvec *res, bvec *rem) 791{ 792 if (c > 0) 793 { 794 bvec divisor = bvec_con(e.bitnum, c); 795 bvec tmp = bvec_build(e.bitnum, 0); 796 bvec tmpremainder = bvec_shlfixed(tmp, 1, e.bitvec[e.bitnum-1]); 797 bvec result = bvec_shlfixed(e, 1, bddfalse); 798 bvec remainder; 799 800 bvec_div_rec(divisor, &tmpremainder, &result, divisor.bitnum); 801 remainder = bvec_shrfixed(tmpremainder, 1, bddfalse); 802 803 bvec_free(tmp); 804 bvec_free(tmpremainder); 805 bvec_free(divisor); 806 807 *res = result; 808 *rem = remainder; 809 810 return 0; 811 } 812 813 return bdd_error(BVEC_DIVZERO); 814} 815 816#if 0 817void p(bvec x) 818{ 819 int n; 820 for (n=0 ; n<x.bitnum ; n++) 821 { 822 printf(" %d: ", n); 823 fdd_printset(x.bitvec[n]); 824 printf("\n"); 825 } 826} 827#endif 828 829/* 830NAME {* bvec\_div *} 831SECTION {* bvec *} 832SHORT {* builds a boolean vector for division *} 833PROTO {* int bvec_div(bvec l, bvec r, bvec *res, bvec *rem) *} 834DESCR {* Builds a new boolean vector representing the integer division 835 of {\tt l} with {\tt r}. The result of the division will be stored 836 in {\tt res} and the remainder of the division will be stored in 837 {\tt rem}. Both vectors should be initialized as the function 838 will try to release the nodes used by them. If an error occurs then 839 the nodes will {\em not} be freed.*} 840RETURN {* Zero on success or a negative error code on error. *} 841ALSO {* bvec\_mul, bvec\_divfixed, bvec\_add, bvec\_shl *} 842*/ 843int bvec_div(bvec left, bvec right, bvec *result, bvec *remainder) 844{ 845 int n, m; 846 int bitnum = left.bitnum + right.bitnum; 847 bvec res; 848 bvec rem; 849 bvec div, divtmp; 850 851 if (left.bitnum == 0 || right.bitnum == 0 || 852 left.bitnum != right.bitnum) 853 { 854 return bdd_error(BVEC_SIZE); 855 } 856 857 rem = bvec_coerce(bitnum, left); 858 divtmp = bvec_coerce(bitnum, right); 859 div = bvec_shlfixed(divtmp, left.bitnum, bddfalse); 860 861 /*bvec_delref(divtmp);*/ 862 bvec_free(divtmp); 863 864 res = bvec_false(right.bitnum); 865 866 for (n=0 ; n<right.bitnum+1 ; n++) 867 { 868 bdd divLteRem = bdd_addref( bvec_lte(div, rem) ); 869 bvec remSubDiv = bvec_sub(rem, div); 870 871 for (m=0 ; m<bitnum ; m++) 872 { 873 bdd remtmp = bdd_addref( bdd_ite(divLteRem, 874 remSubDiv.bitvec[m],rem.bitvec[m]) ); 875 bdd_delref( rem.bitvec[m] ); 876 rem.bitvec[m] = remtmp; 877 } 878 879 if (n > 0) 880 res.bitvec[right.bitnum-n] = divLteRem; 881 882 /* Shift 'div' one bit right */ 883 bdd_delref(div.bitvec[0]); 884 for (m=0 ; m<bitnum-1 ; m++) 885 div.bitvec[m] = div.bitvec[m+1]; 886 div.bitvec[bitnum-1] = bddfalse; 887 888 /*bvec_delref(remSubDiv);*/ 889 bvec_free(remSubDiv); 890 } 891 892 /*bvec_delref(*result);*/ 893 bvec_free(*result); 894 /*bvec_delref(*remainder);*/ 895 bvec_free(*remainder); 896 897 *result = res; 898 *remainder = bvec_coerce(right.bitnum, rem); 899 900 /*bvec_delref(rem);*/ 901 bvec_free(rem); 902 903 return 0; 904} 905 906 907/* 908NAME {* bvec\_shlfixed *} 909SECTION {* bvec *} 910SHORT {* shift left operation (fixed number of bits) *} 911PROTO {* bvec bvec_shlfixed(bvec v, int pos, BDD c) *} 912DESCR {* Builds a boolean vector that represents {\tt v} shifted {\tt pos} 913 times to the left. The new empty elements will be set to {\tt c}.*} 914RETURN {* The result of the operation (which is already reference counted) *} 915ALSO {* bvec\_add, bvec\_mul, bvec\_shl, bvec\_shr *} 916*/ 917bvec bvec_shlfixed(bvec e, int pos, BDD c) 918{ 919 bvec res; 920 int n, minnum = MIN(e.bitnum,pos); 921 922 if (pos < 0) 923 { 924 bdd_error(BVEC_SHIFT); 925 DEFAULT(res); 926 return res; 927 } 928 929 if (e.bitnum == 0) 930 { 931 DEFAULT(res); 932 return res; 933 } 934 935 res = bvec_build(e.bitnum,0); 936 937 for (n=0 ; n<minnum ; n++) 938 res.bitvec[n] = bdd_addref(c); 939 940 for (n=minnum ; n<e.bitnum ; n++) 941 res.bitvec[n] = bdd_addref(e.bitvec[n-pos]); 942 943 return res; 944} 945 946 947/* 948NAME {* bvec\_shl *} 949SECTION {* bvec *} 950SHORT {* shift left operation (symbolic) *} 951PROTO {* bvec bvec_shl(bvec l, bvec r, BDD c) *} 952DESCR {* Builds a boolean vector that represents {\tt l} shifted {\tt r} 953 times to the left. The new empty elements will be set to {\tt c}. 954 The shift operation is fully symbolic and the number of bits 955 shifted depends on the current value encoded by {\tt r}. *} 956RETURN {* The result of the operation (which is already reference counted) *} 957ALSO {* bvec\_add, bvec\_mul, bvec\_shlfixed, bvec\_shr *} 958*/ 959BVEC bvec_shl(BVEC l, BVEC r, BDD c) 960{ 961 BVEC res, val; 962 bdd tmp1, tmp2, rEquN; 963 int n, m; 964 965 if (l.bitnum == 0 || r.bitnum == 0) 966 { 967 DEFAULT(res); 968 return res; 969 } 970 971 res = bvec_build(l.bitnum, 0); 972 973 for (n=0 ; n<=l.bitnum ; n++) 974 { 975 val = bvec_con(r.bitnum, n); 976 rEquN = bdd_addref( bvec_equ(r, val) ); 977 978 for (m=0 ; m<l.bitnum ; m++) 979 { 980 /* Set the m'th new location to be the (m+n)'th old location */ 981 if (m-n >= 0) 982 tmp1 = bdd_addref( bdd_and(rEquN, l.bitvec[m-n]) ); 983 else 984 tmp1 = bdd_addref( bdd_and(rEquN, c) ); 985 tmp2 = bdd_addref( bdd_or(res.bitvec[m], tmp1) ); 986 bdd_delref(tmp1); 987 988 bdd_delref(res.bitvec[m]); 989 res.bitvec[m] = tmp2; 990 } 991 992 bdd_delref(rEquN); 993 /*bvec_delref(val);*/ 994 bvec_free(val); 995 } 996 997 /* At last make sure 'c' is shiftet in for r-values > l-bitnum */ 998 val = bvec_con(r.bitnum, l.bitnum); 999 rEquN = bvec_gth(r, val); 1000 tmp1 = bdd_addref( bdd_and(rEquN, c) ); 1001 1002 for (m=0 ; m<l.bitnum ; m++) 1003 { 1004 tmp2 = bdd_addref( bdd_or(res.bitvec[m], tmp1) ); 1005 1006 bdd_delref(res.bitvec[m]); 1007 res.bitvec[m] = tmp2; 1008 } 1009 1010 bdd_delref(tmp1); 1011 bdd_delref(rEquN); 1012 /*bvec_delref(val);*/ 1013 bvec_free(val); 1014 1015 return res; 1016} 1017 1018 1019/* 1020NAME {* bvec\_shrfixed *} 1021SECTION {* bvec *} 1022SHORT {* shift right operation *} 1023PROTO {* bvec bvec_shrfixed(bvec v, int pos, BDD c) *} 1024DESCR {* Builds a boolean vector that represents {\tt v} shifted {\tt pos} 1025 times to the right. The new empty elements will be set to {\tt c}.*} 1026RETURN {* The result of the operation (which is already reference counted) *} 1027ALSO {* bvec\_add, bvec\_mul, bvec\_shr, bvec\_shl *} 1028*/ 1029bvec bvec_shrfixed(bvec e, int pos, BDD c) 1030{ 1031 bvec res; 1032 int n, maxnum = MAX(0,e.bitnum-pos); 1033 1034 if (pos < 0) 1035 { 1036 bdd_error(BVEC_SHIFT); 1037 DEFAULT(res); 1038 return res; 1039 } 1040 1041 if (e.bitnum == 0) 1042 { 1043 DEFAULT(res); 1044 return res; 1045 } 1046 1047 res = bvec_build(e.bitnum,0); 1048 1049 for (n=maxnum ; n<e.bitnum ; n++) 1050 res.bitvec[n] = bdd_addref(c); 1051 1052 for (n=0 ; n<maxnum ; n++) 1053 res.bitvec[n] = bdd_addref(e.bitvec[n+pos]); 1054 1055 return res; 1056} 1057 1058 1059/* 1060NAME {* bvec\_shr *} 1061SECTION {* bvec *} 1062SHORT {* shift right operation (symbolic) *} 1063PROTO {* bvec bvec_shr(bvec l, bvec r, BDD c) *} 1064DESCR {* Builds a boolean vector that represents {\tt l} shifted {\tt r} 1065 times to the right. The new empty elements will be set to {\tt c}. 1066 The shift operation is fully symbolic and the number of bits 1067 shifted depends on the current value encoded by {\tt r}. *} 1068RETURN {* The result of the operation (which is already reference counted) *} 1069ALSO {* bvec\_add, bvec\_mul, bvec\_shl, bvec\_shrfixed *} 1070*/ 1071BVEC bvec_shr(BVEC l, BVEC r, BDD c) 1072{ 1073 BVEC res, val; 1074 bdd tmp1, tmp2, rEquN; 1075 int n, m; 1076 1077 if (l.bitnum == 0 || r.bitnum == 0) 1078 { 1079 DEFAULT(res); 1080 return res; 1081 } 1082 1083 res = bvec_build(l.bitnum, 0); 1084 1085 for (n=0 ; n<=l.bitnum ; n++) 1086 { 1087 val = bvec_con(r.bitnum, n); 1088 rEquN = bdd_addref( bvec_equ(r, val) ); 1089 1090 for (m=0 ; m<l.bitnum ; m++) 1091 { 1092 /* Set the m'th new location to be the (m+n)'th old location */ 1093 if (m+n <= 2) 1094 tmp1 = bdd_addref( bdd_and(rEquN, l.bitvec[m+n]) ); 1095 else 1096 tmp1 = bdd_addref( bdd_and(rEquN, c) ); 1097 tmp2 = bdd_addref( bdd_or(res.bitvec[m], tmp1) ); 1098 bdd_delref(tmp1); 1099 1100 bdd_delref(res.bitvec[m]); 1101 res.bitvec[m] = tmp2; 1102 } 1103 1104 bdd_delref(rEquN); 1105 /*bvec_delref(val);*/ 1106 bvec_free(val); 1107 } 1108 1109 /* At last make sure 'c' is shiftet in for r-values > l-bitnum */ 1110 val = bvec_con(r.bitnum, l.bitnum); 1111 rEquN = bvec_gth(r, val); 1112 tmp1 = bdd_addref( bdd_and(rEquN, c) ); 1113 1114 for (m=0 ; m<l.bitnum ; m++) 1115 { 1116 tmp2 = bdd_addref( bdd_or(res.bitvec[m], tmp1) ); 1117 1118 bdd_delref(res.bitvec[m]); 1119 res.bitvec[m] = tmp2; 1120 } 1121 1122 bdd_delref(tmp1); 1123 bdd_delref(rEquN); 1124 /*bvec_delref(val);*/ 1125 bvec_free(val); 1126 1127 return res; 1128} 1129 1130 1131/* 1132NAME {* bvec\_lth *} 1133SECTION {* bvec *} 1134SHORT {* calculates the truth value of $x < y$ *} 1135PROTO {* bdd bvec_lth(bvec l, bvec r) *} 1136DESCR {* Returns the BDD representing {\tt l < r} 1137 ({\em not} reference counted). Both vectors must have the 1138 same number of bits. *} 1139ALSO {* bvec\_lte, bvec\_gth, bvec\_gte, bvec\_equ, bvec\_neq *} 1140*/ 1141bdd bvec_lth(bvec l, bvec r) 1142{ 1143 BDD p = bddfalse; 1144 int n; 1145 1146 if (l.bitnum == 0 || r.bitnum == 0) 1147 return bddfalse; 1148 1149 if (l.bitnum != r.bitnum) 1150 { 1151 bdd_error(BVEC_SIZE); 1152 return p; 1153 } 1154 1155 for (n=0 ; n<l.bitnum ; n++) 1156 { 1157 /* p = (!l[n] & r[n]) | 1158 * bdd_apply(l[n], r[n], bddop_biimp) & p; */ 1159 1160 BDD tmp1 = bdd_addref(bdd_apply(l.bitvec[n],r.bitvec[n],bddop_less)); 1161 BDD tmp2 = bdd_addref(bdd_apply(l.bitvec[n],r.bitvec[n],bddop_biimp)); 1162 BDD tmp3 = bdd_addref( bdd_apply(tmp2, p, bddop_and) ); 1163 BDD tmp4 = bdd_addref( bdd_apply(tmp1, tmp3, bddop_or) ); 1164 bdd_delref(tmp1); 1165 bdd_delref(tmp2); 1166 bdd_delref(tmp3); 1167 bdd_delref(p); 1168 p = tmp4; 1169 } 1170 1171 return bdd_delref(p); 1172} 1173 1174 1175/* 1176NAME {* bvec\_lte *} 1177SECTION {* bvec *} 1178SHORT {* calculates the truth value of $x \leq y$ *} 1179PROTO {* bdd bvec_lte(bvec l, bvec r) *} 1180DESCR {* Returns the BDD representing {\tt l}$\leq${\tt r} 1181 ({\em not} reference counted). Both vectors must have the 1182 same number of bits. *} 1183ALSO {* bvec\_lth, bvec\_gth, bvec\_gte, bvec\_equ, bvec\_neq *} 1184*/ 1185bdd bvec_lte(bvec l, bvec r) 1186{ 1187 BDD p = bddtrue; 1188 int n; 1189 1190 if (l.bitnum == 0 || r.bitnum == 0) 1191 return bddfalse; 1192 1193 if (l.bitnum != r.bitnum) 1194 { 1195 bdd_error(BVEC_SIZE); 1196 return p; 1197 } 1198 1199 for (n=0 ; n<l.bitnum ; n++) 1200 { 1201 /* p = (!l[n] & r[n]) | 1202 * bdd_apply(l[n], r[n], bddop_biimp) & p; */ 1203 1204 BDD tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_less) ); 1205 BDD tmp2 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_biimp) ); 1206 BDD tmp3 = bdd_addref( bdd_apply(tmp2, p, bddop_and) ); 1207 BDD tmp4 = bdd_addref( bdd_apply(tmp1, tmp3, bddop_or) ); 1208 bdd_delref(tmp1); 1209 bdd_delref(tmp2); 1210 bdd_delref(tmp3); 1211 bdd_delref(p); 1212 p = tmp4; 1213 } 1214 1215 return bdd_delref(p); 1216} 1217 1218 1219/* 1220NAME {* bvec\_gth *} 1221SECTION {* bvec *} 1222SHORT {* calculates the truth value of $x > y$ *} 1223PROTO {* bdd bvec_gth(bvec l, bvec r) *} 1224DESCR {* Returns the BDD representing {\tt l > r} 1225 ({\em not} reference counted). Both vectors must have the 1226 same number of bits. *} 1227ALSO {* bvec\_lth, bvec\_lte, bvec\_gte, bvec\_equ, bvec\_neq *} 1228*/ 1229bdd bvec_gth(bvec l, bvec r) 1230{ 1231 BDD tmp = bdd_addref( bvec_lte(l,r) ); 1232 BDD p = bdd_not(tmp); 1233 bdd_delref(tmp); 1234 return p; 1235} 1236 1237 1238/* 1239NAME {* bvec\_gte *} 1240SECTION {* bvec *} 1241SHORT {* calculates the truth value of $x \geq y$ *} 1242PROTO {* bdd bvec_gte(bvec l, bvec r) *} 1243DESCR {* Returns the BDD representing {\tt l}$\geq${\tt r} 1244 ({\em not} reference counted). Both vectors must have the 1245 same number of bits. *} 1246ALSO {* bvec\_lth, bvec\_gth, bvec\_gth, bvec\_equ, bvec\_neq *} 1247*/ 1248bdd bvec_gte(bvec l, bvec r) 1249{ 1250 BDD tmp = bdd_addref( bvec_lth(l,r) ); 1251 BDD p = bdd_not(tmp); 1252 bdd_delref(tmp); 1253 return p; 1254} 1255 1256 1257/* 1258NAME {* bvec\_equ *} 1259SECTION {* bvec *} 1260SHORT {* calculates the truth value of $x = y$ *} 1261PROTO {* bdd bvec_equ(bvec l, bvec r) *} 1262DESCR {* Returns the BDD representing {\tt l = r} 1263 ({\em not} reference counted). Both vectors must have the 1264 same number of bits. *} 1265ALSO {* bvec\_lth, bvec\_lte, bvec\_gth, bvec\_gte, bvec\_neq *} 1266*/ 1267bdd bvec_equ(bvec l, bvec r) 1268{ 1269 BDD p = bddtrue; 1270 int n; 1271 1272 if (l.bitnum == 0 || r.bitnum == 0) 1273 return bddfalse; 1274 1275 if (l.bitnum != r.bitnum) 1276 { 1277 bdd_error(BVEC_SIZE); 1278 return p; 1279 } 1280 1281 for (n=0 ; n<l.bitnum ; n++) 1282 { 1283 BDD tmp1, tmp2; 1284 tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_biimp) ); 1285 tmp2 = bdd_addref( bdd_apply(tmp1, p, bddop_and) ); 1286 bdd_delref(tmp1); 1287 bdd_delref(p); 1288 p = tmp2; 1289 } 1290 1291 return bdd_delref(p); 1292} 1293 1294 1295/* 1296NAME {* bvec\_neq *} 1297SECTION {* bvec *} 1298SHORT {* calculates the truth value of $x \neq y$ *} 1299PROTO {* bdd bvec_neq(bvec l, bvec r) *} 1300DESCR {* Returns the BDD representing {\tt l}$\neq${\tt r} 1301 ({\em not} reference counted). Both vectors must have the 1302 same number of bits. *} 1303ALSO {* bvec\_lte, bvec\_lth, bvec\_gth, bvec\_gth, bvec\_equ *} 1304*/ 1305bdd bvec_neq(bvec l, bvec r) 1306{ 1307 BDD tmp = bdd_addref( bvec_equ(l,r) ); 1308 BDD p = bdd_not(tmp); 1309 bdd_delref(tmp); 1310 return p; 1311} 1312 1313 1314/* EOF */ 1315