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: cppext.cxx 33 DESCR: C++ extension of BDD package 34 AUTH: Jorn Lind 35 DATE: (C) august 1997 36*************************************************************************/ 37#include <string.h> 38#include <stdlib.h> 39#include <iomanip> 40#include "kernel.h" 41#include "bvec.h" 42 43using namespace std; 44 45 /* Formatting objects for iostreams */ 46#define IOFORMAT_SET 0 47#define IOFORMAT_TABLE 1 48#define IOFORMAT_DOT 2 49#define IOFORMAT_ALL 3 50#define IOFORMAT_FDDSET 4 51 52int bdd_ioformat::curformat = IOFORMAT_SET; 53bdd_ioformat bddset(IOFORMAT_SET); 54bdd_ioformat bddtable(IOFORMAT_TABLE); 55bdd_ioformat bdddot(IOFORMAT_DOT); 56bdd_ioformat bddall(IOFORMAT_ALL); 57bdd_ioformat fddset(IOFORMAT_FDDSET); 58 59 /* Constant true and false extension */ 60const bdd bddtruepp = bdd_true(); 61const bdd bddfalsepp = bdd_false(); 62 63 /* Internal prototypes */ 64static void bdd_printset_rec(ostream&, int, int*); 65static void bdd_printdot_rec(ostream&, int); 66static void fdd_printset_rec(ostream &, int, int *); 67 68 69static bddstrmhandler strmhandler_bdd; 70static bddstrmhandler strmhandler_fdd; 71 72 // Avoid calling C++ version of anodecount 73#undef bdd_anodecount 74 75/************************************************************************* 76 Setup (and shutdown) 77*************************************************************************/ 78 79#undef bdd_init 80 81int bdd_cpp_init(int n, int c) 82{ 83 int ok = bdd_init(n,c); 84 85 strmhandler_bdd = NULL; 86 strmhandler_fdd = NULL; 87 88 return ok; 89} 90 91 92/************************************************************************* 93 BDD C++ functions 94*************************************************************************/ 95 96bdd bdd_buildcube(int val, int width, const bdd *variables) 97{ 98 BDD *var = NEW(BDD,width); 99 BDD res; 100 int n; 101 102 // No need for ref.cou. since variables[n] holds the reference 103 for (n=0 ; n<width ; n++) 104 var[n] = variables[n].root; 105 106 res = bdd_buildcube(val, width, var); 107 108 free(var); 109 110 return res; 111} 112 113 114int bdd_setbddpairs(bddPair *pair, int *oldvar, const bdd *newvar, int size) 115{ 116 if (pair == NULL) 117 return 0; 118 119 for (int n=0,e=0 ; n<size ; n++) 120 if ((e=bdd_setbddpair(pair, oldvar[n], newvar[n].root)) < 0) 121 return e; 122 123 return 0; 124} 125 126 127int bdd_anodecountpp(const bdd *r, int num) 128{ 129 BDD *cpr = NEW(BDD,num); 130 int cou; 131 int n; 132 133 // No need for ref.cou. since r[n] holds the reference 134 for (n=0 ; n<num ; n++) 135 cpr[n] = r[n].root; 136 137 cou = bdd_anodecount(cpr,num); 138 139 free(cpr); 140 141 return cou; 142} 143 144/************************************************************************* 145 BDD class functions 146*************************************************************************/ 147 148bdd bdd::operator=(const bdd &r) 149{ 150 if (root != r.root) 151 { 152 bdd_delref(root); 153 root = r.root; 154 bdd_addref(root); 155 } 156 return *this; 157} 158 159 160bdd bdd::operator=(int r) 161{ 162 if (root != r) 163 { 164 bdd_delref(root); 165 root = r; 166 bdd_addref(root); 167 } 168 return *this; 169} 170 171 172/************************************************************************* 173 C++ iostream operators 174*************************************************************************/ 175 176/* 177NAME {* bdd\_strm\_hook *} 178SECTION {* kernel *} 179SHORT {* Specifies a printing callback handler *} 180PROTO {* bddstrmhandler bdd_strm_hook(bddstrmhandler handler) *} 181DESCR {* A printing callback handler for use with BDDs is used to 182 convert the BDD variable number into something readable by the 183 end user. Typically the handler will print a string name 184 instead of the number. A handler could look like this: 185 \begin{verbatim} 186void printhandler(ostream &o, int var) 187{ 188 extern char **names; 189 o << names[var]; 190} 191\end{verbatim} 192 193 \noindent 194 The handler can then be passed to BuDDy like this: 195 {\tt bdd\_strm\_hook(printhandler)}. 196 197 No default handler is supplied. The argument {\tt handler} may be 198 NULL if no handler is needed. *} 199RETURN {* The old handler *} 200ALSO {* bdd\_printset, bdd\_file\_hook, fdd\_strm\_hook *} 201*/ 202bddstrmhandler bdd_strm_hook(bddstrmhandler handler) 203{ 204 bddstrmhandler old = strmhandler_bdd; 205 strmhandler_bdd = handler; 206 return old; 207} 208 209 210ostream &operator<<(ostream &o, const bdd &r) 211{ 212 if (bdd_ioformat::curformat == IOFORMAT_SET) 213 { 214 if (r.root < 2) 215 { 216 o << (r.root == 0 ? "F" : "T"); 217 return o; 218 } 219 220 int *set = new int[bddvarnum]; 221 if (set == NULL) 222 { 223 bdd_error(BDD_MEMORY); 224 return o; 225 } 226 227 memset(set, 0, sizeof(int) * bddvarnum); 228 bdd_printset_rec(o, r.root, set); 229 delete[] set; 230 } 231 else 232 if (bdd_ioformat::curformat == IOFORMAT_TABLE) 233 { 234 o << "ROOT: " << r.root << "\n"; 235 if (r.root < 2) 236 return o; 237 238 bdd_mark(r.root); 239 240 for (int n=0 ; n<bddnodesize ; n++) 241 { 242 if (LEVEL(n) & MARKON) 243 { 244 BddNode *node = &bddnodes[n]; 245 246 LEVELp(node) &= MARKOFF; 247 248 o << "[" << setw(5) << n << "] "; 249 if (strmhandler_bdd) 250 strmhandler_bdd(o,bddlevel2var[LEVELp(node)]); 251 else 252 o << setw(3) << bddlevel2var[LEVELp(node)]; 253 o << " :"; 254 o << " " << setw(3) << LOWp(node); 255 o << " " << setw(3) << HIGHp(node); 256 o << "\n"; 257 } 258 } 259 } 260 else 261 if (bdd_ioformat::curformat == IOFORMAT_DOT) 262 { 263 o << "digraph G {\n"; 264 o << "0 [shape=box, label=\"0\", style=filled, shape=box, height=0.3, width=0.3];\n"; 265 o << "1 [shape=box, label=\"1\", style=filled, shape=box, height=0.3, width=0.3];\n"; 266 267 bdd_printdot_rec(o, r.root); 268 269 o << "}\n"; 270 271 bdd_unmark(r.root); 272 } 273 else 274 if (bdd_ioformat::curformat == IOFORMAT_FDDSET) 275 { 276 if (ISCONST(r.root)) 277 { 278 o << (r == 0 ? "F" : "T"); 279 return o; 280 } 281 282 int *set = new int[bddvarnum]; 283 if (set == NULL) 284 { 285 bdd_error(BDD_MEMORY); 286 return o; 287 } 288 289 memset(set, 0, sizeof(int) * bddvarnum); 290 fdd_printset_rec(o, r.root, set); 291 delete[] set; 292 } 293 294 return o; 295} 296 297 298/* 299NAME {* operator{\tt<<} *} 300SECTION {* fileio *} 301SHORT {* C++ output operator for BDDs *} 302PROTO {* ostream &operator<<(ostream &o, const bdd_ioformat &f) 303ostream &operator<<(ostream &o, const bdd &r) *} 304DESCR {* BDDs can be printed in various formats using the C++ iostreams 305 library. The formats are the those used in {\tt bdd\_printset}, 306 {\tt bdd\_printtable}, {\tt fdd\_printset} and {\tt bdd\_printdot}. 307 The format can be specified with the following format objects: 308 \begin{tabular}{ll}\\ 309 {\tt bddset } & BDD level set format \\ 310 {\tt bddtable } & BDD level table format \\ 311 {\tt bdddot } & Output for use with Dot \\ 312 {\tt bddall } & The whole node table \\ 313 {\tt fddset } & FDD level set format \\ 314 \end{tabular}\\ 315 316 \noindent 317 So a BDD {\tt x} can for example be printed as a table with the 318 command\\ 319 320 \indent {\tt cout << bddtable << x << endl}. 321 *} 322RETURN {* The specified output stream *} 323ALSO {* bdd\_strm\_hook, fdd\_strm\_hook *} 324*/ 325ostream &operator<<(ostream &o, const bdd_ioformat &f) 326{ 327 if (f.format == IOFORMAT_SET || f.format == IOFORMAT_TABLE || 328 f.format == IOFORMAT_DOT || f.format == IOFORMAT_FDDSET) 329 bdd_ioformat::curformat = f.format; 330 else 331 if (f.format == IOFORMAT_ALL) 332 { 333 for (int n=0 ; n<bddnodesize ; n++) 334 { 335 const BddNode *node = &bddnodes[n]; 336 337 if (LOWp(node) != -1) 338 { 339 o << "[" << setw(5) << n << "] "; 340 if (strmhandler_bdd) 341 strmhandler_bdd(o,bddlevel2var[LEVELp(node)]); 342 else 343 o << setw(3) << bddlevel2var[LEVELp(node)] << " :"; 344 o << " " << setw(3) << LOWp(node); 345 o << " " << setw(3) << HIGHp(node); 346 o << "\n"; 347 } 348 } 349 } 350 351 return o; 352} 353 354 355static void bdd_printset_rec(ostream& o, int r, int* set) 356{ 357 int n; 358 int first; 359 360 if (r == 0) 361 return; 362 else 363 if (r == 1) 364 { 365 o << "<"; 366 first = 1; 367 368 for (n=0 ; n<bddvarnum ; n++) 369 { 370 if (set[n] > 0) 371 { 372 if (!first) 373 o << ", "; 374 first = 0; 375 if (strmhandler_bdd) 376 strmhandler_bdd(o,bddlevel2var[n]); 377 else 378 o << bddlevel2var[n]; 379 o << ":" << (set[n]==2 ? 1 : 0); 380 } 381 } 382 383 o << ">"; 384 } 385 else 386 { 387 set[LEVEL(r)] = 1; 388 bdd_printset_rec(o, LOW(r), set); 389 390 set[LEVEL(r)] = 2; 391 bdd_printset_rec(o, HIGH(r), set); 392 393 set[LEVEL(r)] = 0; 394 } 395} 396 397 398static void bdd_printdot_rec(ostream& o, int r) 399{ 400 if (ISCONST(r) || MARKED(r)) 401 return; 402 403 o << r << "[label=\""; 404 if (strmhandler_bdd) 405 strmhandler_bdd(o,bddlevel2var[LEVEL(r)]); 406 else 407 o << bddlevel2var[LEVEL(r)]; 408 o << "\"];\n"; 409 o << r << " -> " << LOW(r) << "[style=dotted];\n"; 410 o << r << " -> " << HIGH(r) << "[style=filled];\n"; 411 412 SETMARK(r); 413 414 bdd_printdot_rec(o, LOW(r)); 415 bdd_printdot_rec(o, HIGH(r)); 416} 417 418 419static void fdd_printset_rec(ostream &o, int r, int *set) 420{ 421 int n,m,i; 422 int used = 0; 423 int *binval; 424 int ok, first; 425 426 if (r == 0) 427 return; 428 else 429 if (r == 1) 430 { 431 o << "<"; 432 first=1; 433 int fdvarnum = fdd_domainnum(); 434 435 for (n=0 ; n<fdvarnum ; n++) 436 { 437 int firstval=1; 438 used = 0; 439 int binsize = fdd_varnum(n); 440 int *vars = fdd_vars(n); 441 442 for (m=0 ; m<binsize ; m++) 443 if (set[vars[m]] != 0) 444 used = 1; 445 446 if (used) 447 { 448 if (!first) 449 o << ", "; 450 first = 0; 451 if (strmhandler_fdd) 452 strmhandler_fdd(o, n); 453 else 454 o << n; 455 o << ":"; 456 457 for (m=0 ; m<(1<<binsize) ; m++) 458 { 459 binval = fdddec2bin(n, m); 460 ok=1; 461 462 for (i=0 ; i<binsize && ok ; i++) 463 if (set[vars[i]] == 1 && binval[i] != 0) 464 ok = 0; 465 else 466 if (set[vars[i]] == 2 && binval[i] != 1) 467 ok = 0; 468 469 if (ok) 470 { 471 if (firstval) 472 o << m; 473 else 474 o << "/" << m; 475 firstval = 0; 476 } 477 478 free(binval); 479 } 480 } 481 } 482 483 o << ">"; 484 } 485 else 486 { 487 set[bddlevel2var[LEVEL(r)]] = 1; 488 fdd_printset_rec(o, LOW(r), set); 489 490 set[bddlevel2var[LEVEL(r)]] = 2; 491 fdd_printset_rec(o, HIGH(r), set); 492 493 set[bddlevel2var[LEVEL(r)]] = 0; 494 } 495} 496 497 498/*=[ FDD I/O functions ]================================================*/ 499 500/* 501NAME {* fdd\_strm\_hook *} 502SECTION {* fdd *} 503SHORT {* Specifies a printing callback handler *} 504PROTO {* bddstrmhandler fdd_strm_hook(bddstrmhandler handler) *} 505DESCR {* A printing callback handler for use with FDDs is used to 506 convert the FDD integer identifier into something readable by the 507 end user. Typically the handler will print a string name 508 instead of the identifier. A handler could look like this: 509 \begin{verbatim} 510void printhandler(ostream &o, int var) 511{ 512 extern char **names; 513 o << names[var]; 514} 515\end{verbatim} 516 517 \noindent 518 The handler can then be passed to BuDDy like this: 519 {\tt fdd\_strm\_hook(printhandler)}. 520 521 No default handler is supplied. The argument {\tt handler} may be 522 NULL if no handler is needed. *} 523RETURN {* The old handler *} 524ALSO {* fdd\_printset, bdd\_file\_hook *} 525*/ 526bddstrmhandler fdd_strm_hook(bddstrmhandler handler) 527{ 528 bddstrmhandler old = strmhandler_fdd; 529 strmhandler_fdd = handler; 530 return old; 531} 532 533 534/************************************************************************* 535 bvec functions 536*************************************************************************/ 537 538bvec bvec::operator=(const bvec &src) 539{ 540 if (&src != this) 541 { 542 bvec_free(roots); 543 roots = bvec_copy(src.roots); 544 } 545 return *this; 546} 547 548 549void bvec::set(int bitnum, const bdd &b) 550{ 551 bdd_delref(roots.bitvec[bitnum]); 552 roots.bitvec[bitnum] = b.root; 553 bdd_addref(roots.bitvec[bitnum]); 554} 555 556 557/*======================================================================*/ 558 559bvec bvec_map1(const bvec &a, 560 bdd (*fun)(const bdd &)) 561{ 562 bvec res; 563 int n; 564 565 res = bvec_false(a.bitnum()); 566 for (n=0 ; n < a.bitnum() ; n++) 567 res.set(n, fun(a[n])); 568 569 return res; 570} 571 572 573bvec bvec_map2(const bvec &a, const bvec &b, 574 bdd (*fun)(const bdd &, const bdd &)) 575{ 576 bvec res; 577 int n; 578 579 if (a.bitnum() != b.bitnum()) 580 { 581 bdd_error(BVEC_SIZE); 582 return res; 583 } 584 585 res = bvec_false(a.bitnum()); 586 for (n=0 ; n < a.bitnum() ; n++) 587 res.set(n, fun(a[n], b[n])); 588 589 return res; 590} 591 592 593bvec bvec_map3(const bvec &a, const bvec &b, const bvec &c, 594 bdd (*fun)(const bdd &, const bdd &, const bdd &)) 595{ 596 bvec res; 597 int n; 598 599 if (a.bitnum() != b.bitnum() || b.bitnum() != c.bitnum()) 600 { 601 bdd_error(BVEC_SIZE); 602 return res; 603 } 604 605 res = bvec_false(a.bitnum()); 606 for (n=0 ; n < a.bitnum() ; n++) 607 res.set(n, fun(a[n], b[n], c[n]) ); 608 609 return res; 610} 611 612 613/* EOF */ 614