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: bdd.h 33 DESCR: C,C++ User interface for the BDD package 34 AUTH: Jorn Lind 35 DATE: (C) feb 1997 36*************************************************************************/ 37 38#ifndef _BDD_H 39#define _BDD_H 40 41 /* Allow this headerfile to define C++ constructs if requested */ 42#ifdef __cplusplus 43#define CPLUSPLUS 44#endif 45 46#include <stdio.h> 47 48/*=== Defined operators for apply calls ================================*/ 49 50#define bddop_and 0 51#define bddop_xor 1 52#define bddop_or 2 53#define bddop_nand 3 54#define bddop_nor 4 55#define bddop_imp 5 56#define bddop_biimp 6 57#define bddop_diff 7 58#define bddop_less 8 59#define bddop_invimp 9 60 61 /* Should *not* be used in bdd_apply calls !!! */ 62#define bddop_not 10 63#define bddop_simplify 11 64 65 66/*=== User BDD types ===================================================*/ 67 68typedef int BDD; 69 70#ifndef CPLUSPLUS 71typedef BDD bdd; 72#endif /* CPLUSPLUS */ 73 74 75typedef struct s_bddPair 76{ 77 BDD *result; 78 int last; 79 int id; 80 struct s_bddPair *next; 81} bddPair; 82 83 84/*=== Status information ===============================================*/ 85 86/* 87NAME {* bddStat *} 88SECTION {* kernel *} 89SHORT {* Status information about the bdd package *} 90PROTO {* typedef struct s_bddStat 91{ 92 long int produced; 93 int nodenum; 94 int maxnodenum; 95 int freenodes; 96 int minfreenodes; 97 int varnum; 98 int cachesize; 99 int gbcnum; 100} bddStat; *} 101DESCR {* The fields are \\[\baselineskip] \begin{tabular}{lp{10cm}} 102 {\tt produced} & total number of new nodes ever produced \\ 103 {\tt nodenum} & currently allocated number of bdd nodes \\ 104 {\tt maxnodenum} & user defined maximum number of bdd nodes \\ 105 {\tt freenodes} & number of currently free nodes \\ 106 {\tt minfreenodes} & minimum number of nodes that should be left after a 107 garbage collection. \\ 108 {\tt varnum} & number of defined bdd variables \\ 109 {\tt cachesize} & number of entries in the internal caches \\ 110 {\tt gbcnum} & number of garbage collections done until now 111 \end{tabular} *} 112ALSO {* bdd\_stats *} 113*/ 114typedef struct s_bddStat 115{ 116 long int produced; 117 int nodenum; 118 int maxnodenum; 119 int freenodes; 120 int minfreenodes; 121 int varnum; 122 int cachesize; 123 int gbcnum; 124} bddStat; 125 126 127/* 128NAME {* bddGbcStat *} 129SECTION {* kernel *} 130SHORT {* Status information about garbage collections *} 131PROTO {* typedef struct s_bddGbcStat 132{ 133 int nodes; 134 int freenodes; 135 long time; 136 long sumtime; 137 int num; 138} bddGbcStat; *} 139DESCR {* The fields are \\[\baselineskip] \begin{tabular}{ll} 140 {\tt nodes} & Total number of allocated nodes in the nodetable \\ 141 {\tt freenodes} & Number of free nodes in the nodetable \\ 142 {\tt time} & Time used for garbage collection this time \\ 143 {\tt sumtime} & Total time used for garbage collection \\ 144 {\tt num} & number of garbage collections done until now 145 \end{tabular} *} 146ALSO {* bdd\_gbc\_hook *} 147*/ 148typedef struct s_bddGbcStat 149{ 150 int nodes; 151 int freenodes; 152 long time; 153 long sumtime; 154 int num; 155} bddGbcStat; 156 157 158/* 159NAME {* bddCacheStat *} 160SECTION {* kernel *} 161SHORT {* Status information about cache usage *} 162PROTO {* typedef struct s_bddCacheStat 163{ 164 long unsigned int uniqueAccess; 165 long unsigned int uniqueChain; 166 long unsigned int uniqueHit; 167 long unsigned int uniqueMiss; 168 long unsigned int opHit; 169 long unsigned int opMiss; 170 long unsigned int swapCount; 171} bddCacheStat; *} 172DESCR {* The fields are \\[\baselineskip] \begin{tabular}{ll} 173 {\bf Name} & {\bf Number of } \\ 174 uniqueAccess & accesses to the unique node table \\ 175 uniqueChain & iterations through the cache chains in the unique node table\\ 176 uniqueHit & entries actually found in the unique node table \\ 177 uniqueMiss & entries not found in the unique node table \\ 178 opHit & entries found in the operator caches \\ 179 opMiss & entries not found in the operator caches \\ 180 swapCount & number of variable swaps in reordering \\ 181\end{tabular} *} 182ALSO {* bdd\_cachestats *} 183*/ 184typedef struct s_bddCacheStat 185{ 186 long unsigned int uniqueAccess; 187 long unsigned int uniqueChain; 188 long unsigned int uniqueHit; 189 long unsigned int uniqueMiss; 190 long unsigned int opHit; 191 long unsigned int opMiss; 192 long unsigned int swapCount; 193} bddCacheStat; 194 195/*=== BDD interface prototypes =========================================*/ 196 197/* 198NAME {* bdd\_relprod *} 199SECTION {* operator *} 200SHORT {* relational product *} 201PROTO {* #define bdd_relprod(a,b,var) bdd_appex(a,b,bddop_and,var) *} 202DESCR {* Calculates the relational product of {\tt a} and {\tt b} as 203 {\tt a AND b} with the variables in {\tt var} quantified out 204 afterwards. *} 205RETURN {* The relational product or {\tt bddfalse} on errors. *} 206ALSO {* bdd\_appex *} 207*/ 208#define bdd_relprod(a,b,var) bdd_appex((a),(b),bddop_and,(var)) 209 210 211 /* In file "kernel.c" */ 212 213#ifdef CPLUSPLUS 214extern "C" { 215#endif 216 217typedef void (*bddinthandler)(int); 218typedef void (*bddgbchandler)(int,bddGbcStat*); 219typedef void (*bdd2inthandler)(int,int); 220typedef int (*bddsizehandler)(void); 221typedef void (*bddfilehandler)(FILE *, int); 222 223extern bddinthandler bdd_error_hook(bddinthandler); 224extern bddgbchandler bdd_gbc_hook(bddgbchandler); 225extern bdd2inthandler bdd_resize_hook(bdd2inthandler); 226extern bddinthandler bdd_reorder_hook(bddinthandler); 227extern bddfilehandler bdd_file_hook(bddfilehandler); 228 229extern int bdd_init(int, int); 230extern void bdd_done(void); 231extern int bdd_setvarnum(int); 232extern int bdd_extvarnum(int); 233extern int bdd_isrunning(void); 234extern int bdd_setmaxnodenum(int); 235extern int bdd_setmaxincrease(int); 236extern int bdd_setminfreenodes(int); 237extern int bdd_getnodenum(void); 238extern int bdd_getallocnum(void); 239extern char* bdd_versionstr(void); 240extern int bdd_versionnum(void); 241extern void bdd_stats(bddStat *); 242extern void bdd_cachestats(bddCacheStat *); 243extern void bdd_fprintstat(FILE *); 244extern void bdd_printstat(void); 245extern void bdd_default_gbchandler(int, bddGbcStat *); 246extern void bdd_default_errhandler(int); 247extern const char *bdd_errstring(int); 248extern void bdd_clear_error(void); 249#ifndef CPLUSPLUS 250extern BDD bdd_true(void); 251extern BDD bdd_false(void); 252#endif 253extern int bdd_varnum(void); 254extern BDD bdd_ithvar(int); 255extern BDD bdd_nithvar(int); 256extern int bdd_var(BDD); 257extern BDD bdd_low(BDD); 258extern BDD bdd_high(BDD); 259extern int bdd_varlevel(int); 260extern BDD bdd_addref(BDD); 261extern BDD bdd_delref(BDD); 262extern void bdd_gbc(void); 263extern int bdd_scanset(BDD, int**, int*); 264extern BDD bdd_makeset(int *, int); 265extern bddPair* bdd_newpair(void); 266extern int bdd_setpair(bddPair*, int, int); 267extern int bdd_setpairs(bddPair*, int*, int*, int); 268extern int bdd_setbddpair(bddPair*, int, BDD); 269extern int bdd_setbddpairs(bddPair*, int*, BDD*, int); 270extern void bdd_resetpair(bddPair *); 271extern void bdd_freepair(bddPair*); 272 273 /* In bddop.c */ 274 275extern int bdd_setcacheratio(int); 276extern BDD bdd_buildcube(int, int, BDD *); 277extern BDD bdd_ibuildcube(int, int, int *); 278extern BDD bdd_not(BDD); 279extern BDD bdd_apply(BDD, BDD, int); 280extern BDD bdd_and(BDD, BDD); 281extern BDD bdd_or(BDD, BDD); 282extern BDD bdd_xor(BDD, BDD); 283extern BDD bdd_imp(BDD, BDD); 284extern BDD bdd_biimp(BDD, BDD); 285extern BDD bdd_ite(BDD, BDD, BDD); 286extern BDD bdd_restrict(BDD, BDD); 287extern BDD bdd_constrain(BDD, BDD); 288extern BDD bdd_replace(BDD, bddPair*); 289extern BDD bdd_compose(BDD, BDD, BDD); 290extern BDD bdd_veccompose(BDD, bddPair*); 291extern BDD bdd_simplify(BDD, BDD); 292extern BDD bdd_exist(BDD, BDD); 293extern BDD bdd_forall(BDD, BDD); 294extern BDD bdd_unique(BDD, BDD); 295extern BDD bdd_appex(BDD, BDD, int, BDD); 296extern BDD bdd_appall(BDD, BDD, int, BDD); 297extern BDD bdd_appuni(BDD, BDD, int, BDD); 298extern BDD bdd_support(BDD); 299extern BDD bdd_satone(BDD); 300extern BDD bdd_satoneset(BDD, BDD, BDD); 301extern BDD bdd_fullsatone(BDD); 302extern double bdd_satcount(BDD); 303extern double bdd_satcountset(BDD, BDD); 304extern double bdd_satcountln(BDD); 305extern double bdd_satcountlnset(BDD, BDD); 306extern int bdd_nodecount(BDD); 307extern int bdd_anodecount(BDD *, int); 308extern int* bdd_varprofile(BDD); 309extern double bdd_pathcount(BDD); 310 311 312/* In file "bddio.c" */ 313 314extern void bdd_printall(void); 315extern void bdd_fprintall(FILE *); 316extern void bdd_fprinttable(FILE *, BDD); 317extern void bdd_printtable(BDD); 318extern void bdd_fprintset(FILE *, BDD); 319extern void bdd_printset(BDD); 320extern int bdd_fnprintdot(char *, BDD); 321extern void bdd_fprintdot(FILE *, BDD); 322extern void bdd_printdot(BDD); 323extern int bdd_fnsave(char *, BDD); 324extern int bdd_save(FILE *, BDD); 325extern int bdd_fnload(char *, BDD *); 326extern int bdd_load(FILE *ifile, BDD *); 327 328/* In file reorder.c */ 329 330extern int bdd_swapvar(int v1, int v2); 331extern void bdd_default_reohandler(int); 332extern void bdd_reorder(int); 333extern int bdd_reorder_gain(void); 334extern bddsizehandler bdd_reorder_probe(bddsizehandler); 335extern void bdd_clrvarblocks(void); 336extern int bdd_addvarblock(BDD, int); 337extern int bdd_intaddvarblock(int, int, int); 338extern void bdd_varblockall(void); 339extern bddfilehandler bdd_blockfile_hook(bddfilehandler); 340extern int bdd_autoreorder(int); 341extern int bdd_autoreorder_times(int, int); 342extern int bdd_var2level(int); 343extern int bdd_level2var(int); 344extern int bdd_getreorder_times(void); 345extern int bdd_getreorder_method(void); 346extern void bdd_enable_reorder(void); 347extern void bdd_disable_reorder(void); 348extern int bdd_reorder_verbose(int); 349extern void bdd_setvarorder(int *); 350extern void bdd_printorder(void); 351extern void bdd_fprintorder(FILE *); 352 353#ifdef CPLUSPLUS 354} 355#endif 356 357 358/*=== BDD constants ====================================================*/ 359 360#ifndef CPLUSPLUS 361 362extern const BDD bddfalse; 363extern const BDD bddtrue; 364 365#endif /* CPLUSPLUS */ 366 367 368/*=== Reordering algorithms ============================================*/ 369 370#define BDD_REORDER_NONE 0 371#define BDD_REORDER_WIN2 1 372#define BDD_REORDER_WIN2ITE 2 373#define BDD_REORDER_SIFT 3 374#define BDD_REORDER_SIFTITE 4 375#define BDD_REORDER_WIN3 5 376#define BDD_REORDER_WIN3ITE 6 377#define BDD_REORDER_RANDOM 7 378 379#define BDD_REORDER_FREE 0 380#define BDD_REORDER_FIXED 1 381 382 383/*=== Error codes ======================================================*/ 384 385#define BDD_MEMORY (-1) /* Out of memory */ 386#define BDD_VAR (-2) /* Unknown variable */ 387#define BDD_RANGE (-3) /* Variable value out of range (not in domain) */ 388#define BDD_DEREF (-4) /* Removing external reference to unknown node */ 389#define BDD_RUNNING (-5) /* Called bdd_init() twice whithout bdd_done() */ 390#define BDD_FILE (-6) /* Some file operation failed */ 391#define BDD_FORMAT (-7) /* Incorrect file format */ 392#define BDD_ORDER (-8) /* Vars. not in order for vector based functions */ 393#define BDD_BREAK (-9) /* User called break */ 394#define BDD_VARNUM (-10) /* Different number of vars. for vector pair */ 395#define BDD_NODES (-11) /* Tried to set max. number of nodes to be fewer */ 396 /* than there already has been allocated */ 397#define BDD_OP (-12) /* Unknown operator */ 398#define BDD_VARSET (-13) /* Illegal variable set */ 399#define BDD_VARBLK (-14) /* Bad variable block operation */ 400#define BDD_DECVNUM (-15) /* Trying to decrease the number of variables */ 401#define BDD_REPLACE (-16) /* Replacing to already existing variables */ 402#define BDD_NODENUM (-17) /* Number of nodes reached user defined maximum */ 403#define BDD_ILLBDD (-18) /* Illegal bdd argument */ 404#define BDD_SIZE (-19) /* Illegal size argument */ 405 406#define BVEC_SIZE (-20) /* Mismatch in bitvector size */ 407#define BVEC_SHIFT (-21) /* Illegal shift-left/right parameter */ 408#define BVEC_DIVZERO (-22) /* Division by zero */ 409 410#define BDD_ERRNUM 24 411 412/************************************************************************* 413 If this file is included from a C++ compiler then the following 414 classes, wrappers and hacks are supplied. 415*************************************************************************/ 416#ifdef CPLUSPLUS 417#include <iostream> 418 419/*=== User BDD class ===================================================*/ 420 421class bvec; 422 423class bdd 424{ 425 public: 426 427 bdd(void) { root=0; } 428 bdd(const bdd &r) { bdd_addref(root=r.root); } 429 ~bdd(void) { bdd_delref(root); } 430 431 int id(void) const; 432 433 bdd operator=(const bdd &r); 434 435 bdd operator&(const bdd &r) const; 436 bdd operator&=(const bdd &r); 437 bdd operator^(const bdd &r) const; 438 bdd operator^=(const bdd &r); 439 bdd operator|(const bdd &r) const; 440 bdd operator|=(const bdd &r); 441 bdd operator!(void) const; 442 bdd operator>>(const bdd &r) const; 443 bdd operator>>=(const bdd &r); 444 bdd operator-(const bdd &r) const; 445 bdd operator-=(const bdd &r); 446 bdd operator>(const bdd &r) const; 447 bdd operator<(const bdd &r) const; 448 bdd operator<<(const bdd &r) const; 449 bdd operator<<=(const bdd &r); 450 int operator==(const bdd &r) const; 451 int operator!=(const bdd &r) const; 452 453private: 454 BDD root; 455 456 bdd(BDD r) { bdd_addref(root=r); } 457 bdd operator=(BDD r); 458 459 friend int bdd_init(int, int); 460 friend int bdd_setvarnum(int); 461 friend bdd bdd_true(void); 462 friend bdd bdd_false(void); 463 friend bdd bdd_ithvarpp(int); 464 friend bdd bdd_nithvarpp(int); 465 friend int bdd_var(const bdd &); 466 friend bdd bdd_low(const bdd &); 467 friend bdd bdd_high(const bdd &); 468 friend int bdd_scanset(const bdd &, int *&, int &); 469 friend bdd bdd_makesetpp(int *, int); 470 friend int bdd_setbddpair(bddPair*, int, const bdd &); 471 friend int bdd_setbddpairs(bddPair*, int*, const bdd *, int); 472 friend bdd bdd_buildcube(int, int, const bdd *); 473 friend bdd bdd_ibuildcubepp(int, int, int *); 474 friend bdd bdd_not(const bdd &); 475 friend bdd bdd_simplify(const bdd &, const bdd &); 476 friend bdd bdd_apply(const bdd &, const bdd &, int); 477 friend bdd bdd_and(const bdd &, const bdd &); 478 friend bdd bdd_or(const bdd &, const bdd &); 479 friend bdd bdd_xor(const bdd &, const bdd &); 480 friend bdd bdd_imp(const bdd &, const bdd &); 481 friend bdd bdd_biimp(const bdd &, const bdd &); 482 friend bdd bdd_ite(const bdd &, const bdd &, const bdd &); 483 friend bdd bdd_restrict(const bdd &, const bdd &); 484 friend bdd bdd_constrain(const bdd &, const bdd &); 485 friend bdd bdd_exist(const bdd &, const bdd &); 486 friend bdd bdd_forall(const bdd &, const bdd &); 487 friend bdd bdd_unique(const bdd &, const bdd &); 488 friend bdd bdd_appex(const bdd &, const bdd &, int, const bdd &); 489 friend bdd bdd_appall(const bdd &, const bdd &, int, const bdd &); 490 friend bdd bdd_appuni(const bdd &, const bdd &, int, const bdd &); 491 friend bdd bdd_replace(const bdd &, bddPair*); 492 friend bdd bdd_compose(const bdd &, const bdd &, int); 493 friend bdd bdd_veccompose(const bdd &, bddPair*); 494 friend bdd bdd_support(const bdd &); 495 friend bdd bdd_satone(const bdd &); 496 friend bdd bdd_satoneset(const bdd &, const bdd &, const bdd &); 497 friend bdd bdd_fullsatone(const bdd &); 498 friend double bdd_satcount(const bdd &); 499 friend double bdd_satcountset(const bdd &, const bdd &); 500 friend double bdd_satcountln(const bdd &); 501 friend double bdd_satcountlnset(const bdd &, const bdd &); 502 friend int bdd_nodecount(const bdd &); 503 friend int bdd_anodecountpp(const bdd *, int); 504 friend int* bdd_varprofile(const bdd &); 505 friend double bdd_pathcount(const bdd &); 506 507 friend void bdd_fprinttable(FILE *, const bdd &); 508 friend void bdd_printtable(const bdd &); 509 friend void bdd_fprintset(FILE *, const bdd &); 510 friend void bdd_printset(const bdd &); 511 friend void bdd_printdot(const bdd &); 512 friend int bdd_fnprintdot(char*, const bdd &); 513 friend void bdd_fprintdot(FILE*, const bdd &); 514 friend std::ostream &operator<<(std::ostream &, const bdd &); 515 friend int bdd_fnsave(char*, const bdd &); 516 friend int bdd_save(FILE*, const bdd &); 517 friend int bdd_fnload(char*, bdd &); 518 friend int bdd_load(FILE*, bdd &); 519 520 friend bdd fdd_ithvarpp(int, int); 521 friend bdd fdd_ithsetpp(int); 522 friend bdd fdd_domainpp(int); 523 friend int fdd_scanvar(const bdd &, int); 524 friend int* fdd_scanallvar(const bdd &); 525 friend bdd fdd_equalspp(int, int); 526 friend void fdd_printset(const bdd &); 527 friend void fdd_fprintset(FILE*, const bdd &); 528 friend bdd fdd_makesetpp(int*, int); 529 friend int fdd_scanset(const bdd &, int *&, int &); 530 531 friend int bdd_addvarblock(const bdd &, int); 532 533 friend class bvec; 534 friend bvec bvec_shlfixed(const bvec &e, int pos, const bdd &c); 535 friend bvec bvec_shl(const bvec &left, const bvec &right, const bdd &c); 536 friend bvec bvec_shrfixed(const bvec &e, int pos, const bdd &c); 537 friend bvec bvec_shr(const bvec &left, const bvec &right, const bdd &c); 538 friend bdd bvec_lth(const bvec &left, const bvec &right); 539 friend bdd bvec_lte(const bvec &left, const bvec &right); 540 friend bdd bvec_gth(const bvec &left, const bvec &right); 541 friend bdd bvec_gte(const bvec &left, const bvec &right); 542 friend bdd bvec_equ(const bvec &left, const bvec &right); 543 friend bdd bvec_neq(const bvec &left, const bvec &right); 544}; 545 546 547/*=== BDD constants ====================================================*/ 548 549extern const bdd bddfalsepp; 550extern const bdd bddtruepp; 551 552#define bddtrue bddtruepp 553#define bddfalse bddfalsepp 554 555/*=== C++ interface ====================================================*/ 556 557extern int bdd_cpp_init(int, int); 558 559inline void bdd_stats(bddStat& s) 560{ bdd_stats(&s); } 561 562inline bdd bdd_ithvarpp(int v) 563{ return bdd_ithvar(v); } 564 565inline bdd bdd_nithvarpp(int v) 566{ return bdd_nithvar(v); } 567 568inline int bdd_var(const bdd &r) 569{ return bdd_var(r.root); } 570 571inline bdd bdd_low(const bdd &r) 572{ return bdd_low(r.root); } 573 574inline bdd bdd_high(const bdd &r) 575{ return bdd_high(r.root); } 576 577inline int bdd_scanset(const bdd &r, int *&v, int &n) 578{ return bdd_scanset(r.root, &v, &n); } 579 580inline bdd bdd_makesetpp(int *v, int n) 581{ return bdd(bdd_makeset(v,n)); } 582 583inline int bdd_setbddpair(bddPair *p, int ov, const bdd &nv) 584{ return bdd_setbddpair(p,ov,nv.root); } 585 586 /* In bddop.c */ 587 588inline bdd bdd_replace(const bdd &r, bddPair *p) 589{ return bdd_replace(r.root, p); } 590 591inline bdd bdd_compose(const bdd &f, const bdd &g, int v) 592{ return bdd_compose(f.root, g.root, v); } 593 594inline bdd bdd_veccompose(const bdd &f, bddPair *p) 595{ return bdd_veccompose(f.root, p); } 596 597inline bdd bdd_restrict(const bdd &r, const bdd &var) 598{ return bdd_restrict(r.root, var.root); } 599 600inline bdd bdd_constrain(const bdd &f, const bdd &c) 601{ return bdd_constrain(f.root, c.root); } 602 603inline bdd bdd_simplify(const bdd &d, const bdd &b) 604{ return bdd_simplify(d.root, b.root); } 605 606inline bdd bdd_ibuildcubepp(int v, int w, int *a) 607{ return bdd_ibuildcube(v,w,a); } 608 609inline bdd bdd_not(const bdd &r) 610{ return bdd_not(r.root); } 611 612inline bdd bdd_apply(const bdd &l, const bdd &r, int op) 613{ return bdd_apply(l.root, r.root, op); } 614 615inline bdd bdd_and(const bdd &l, const bdd &r) 616{ return bdd_apply(l.root, r.root, bddop_and); } 617 618inline bdd bdd_or(const bdd &l, const bdd &r) 619{ return bdd_apply(l.root, r.root, bddop_or); } 620 621inline bdd bdd_xor(const bdd &l, const bdd &r) 622{ return bdd_apply(l.root, r.root, bddop_xor); } 623 624inline bdd bdd_imp(const bdd &l, const bdd &r) 625{ return bdd_apply(l.root, r.root, bddop_imp); } 626 627inline bdd bdd_biimp(const bdd &l, const bdd &r) 628{ return bdd_apply(l.root, r.root, bddop_biimp); } 629 630inline bdd bdd_ite(const bdd &f, const bdd &g, const bdd &h) 631{ return bdd_ite(f.root, g.root, h.root); } 632 633inline bdd bdd_exist(const bdd &r, const bdd &var) 634{ return bdd_exist(r.root, var.root); } 635 636inline bdd bdd_forall(const bdd &r, const bdd &var) 637{ return bdd_forall(r.root, var.root); } 638 639inline bdd bdd_unique(const bdd &r, const bdd &var) 640{ return bdd_unique(r.root, var.root); } 641 642inline bdd bdd_appex(const bdd &l, const bdd &r, int op, const bdd &var) 643{ return bdd_appex(l.root, r.root, op, var.root); } 644 645inline bdd bdd_appall(const bdd &l, const bdd &r, int op, const bdd &var) 646{ return bdd_appall(l.root, r.root, op, var.root); } 647 648inline bdd bdd_appuni(const bdd &l, const bdd &r, int op, const bdd &var) 649{ return bdd_appuni(l.root, r.root, op, var.root); } 650 651inline bdd bdd_support(const bdd &r) 652{ return bdd_support(r.root); } 653 654inline bdd bdd_satone(const bdd &r) 655{ return bdd_satone(r.root); } 656 657inline bdd bdd_satoneset(const bdd &r, const bdd &var, const bdd &pol) 658{ return bdd_satoneset(r.root, var.root, pol.root); } 659 660inline bdd bdd_fullsatone(const bdd &r) 661{ return bdd_fullsatone(r.root); } 662 663inline double bdd_satcount(const bdd &r) 664{ return bdd_satcount(r.root); } 665 666inline double bdd_satcountset(const bdd &r, const bdd &varset) 667{ return bdd_satcountset(r.root, varset.root); } 668 669inline double bdd_satcountln(const bdd &r) 670{ return bdd_satcountln(r.root); } 671 672inline double bdd_satcountlnset(const bdd &r, const bdd &varset) 673{ return bdd_satcountlnset(r.root, varset.root); } 674 675inline int bdd_nodecount(const bdd &r) 676{ return bdd_nodecount(r.root); } 677 678inline int* bdd_varprofile(const bdd &r) 679{ return bdd_varprofile(r.root); } 680 681inline double bdd_pathcount(const bdd &r) 682{ return bdd_pathcount(r.root); } 683 684 685 /* I/O extensions */ 686 687inline void bdd_fprinttable(FILE *file, const bdd &r) 688{ bdd_fprinttable(file, r.root); } 689 690inline void bdd_printtable(const bdd &r) 691{ bdd_printtable(r.root); } 692 693inline void bdd_fprintset(FILE *file, const bdd &r) 694{ bdd_fprintset(file, r.root); } 695 696inline void bdd_printset(const bdd &r) 697{ bdd_printset(r.root); } 698 699inline void bdd_printdot(const bdd &r) 700{ bdd_printdot(r.root); } 701 702inline void bdd_fprintdot(FILE* ofile, const bdd &r) 703{ bdd_fprintdot(ofile, r.root); } 704 705inline int bdd_fnprintdot(char* fname, const bdd &r) 706{ return bdd_fnprintdot(fname, r.root); } 707 708inline int bdd_fnsave(char *fname, const bdd &r) 709{ return bdd_fnsave(fname, r.root); } 710 711inline int bdd_save(FILE *ofile, const bdd &r) 712{ return bdd_save(ofile, r.root); } 713 714inline int bdd_fnload(char *fname, bdd &r) 715{ int lr,e; e=bdd_fnload(fname, &lr); r=bdd(lr); return e; } 716 717inline int bdd_load(FILE *ifile, bdd &r) 718{ int lr,e; e=bdd_load(ifile, &lr); r=bdd(lr); return e; } 719 720inline int bdd_addvarblock(const bdd &v, int f) 721{ return bdd_addvarblock(v.root, f); } 722 723 /* Hack to allow for overloading */ 724#define bdd_init bdd_cpp_init 725#define bdd_ithvar bdd_ithvarpp 726#define bdd_nithvar bdd_nithvarpp 727#define bdd_makeset bdd_makesetpp 728#define bdd_ibuildcube bdd_ibuildcubepp 729#define bdd_anodecount bdd_anodecountpp 730 731/*=== Inline C++ functions =============================================*/ 732 733inline int bdd::id(void) const 734{ return root; } 735 736inline bdd bdd::operator&(const bdd &r) const 737{ return bdd_apply(*this,r,bddop_and); } 738 739inline bdd bdd::operator&=(const bdd &r) 740{ return (*this=bdd_apply(*this,r,bddop_and)); } 741 742inline bdd bdd::operator^(const bdd &r) const 743{ return bdd_apply(*this,r,bddop_xor); } 744 745inline bdd bdd::operator^=(const bdd &r) 746{ return (*this=bdd_apply(*this,r,bddop_xor)); } 747 748inline bdd bdd::operator|(const bdd &r) const 749{ return bdd_apply(*this,r,bddop_or); } 750 751inline bdd bdd::operator|=(const bdd &r) 752{ return (*this=bdd_apply(*this,r,bddop_or)); } 753 754inline bdd bdd::operator!(void) const 755{ return bdd_not(*this);} 756 757inline bdd bdd::operator>>(const bdd &r) const 758{ return bdd_apply(*this,r,bddop_imp); } 759 760inline bdd bdd::operator>>=(const bdd &r) 761{ return (*this=bdd_apply(*this,r,bddop_imp)); } 762 763inline bdd bdd::operator-(const bdd &r) const 764{ return bdd_apply(*this,r,bddop_diff); } 765 766inline bdd bdd::operator-=(const bdd &r) 767{ return (*this=bdd_apply(*this,r,bddop_diff)); } 768 769inline bdd bdd::operator>(const bdd &r) const 770{ return bdd_apply(*this,r,bddop_diff); } 771 772inline bdd bdd::operator<(const bdd &r) const 773{ return bdd_apply(*this,r,bddop_less); } 774 775inline bdd bdd::operator<<(const bdd &r) const 776{ return bdd_apply(*this,r,bddop_invimp); } 777 778inline bdd bdd::operator<<=(const bdd &r) 779{ return (*this=bdd_apply(*this,r,bddop_invimp)); } 780 781inline int bdd::operator==(const bdd &r) const 782{ return r.root==root; } 783 784inline int bdd::operator!=(const bdd &r) const 785{ return r.root!=root; } 786 787inline bdd bdd_true(void) 788{ return 1; } 789 790inline bdd bdd_false(void) 791{ return 0; } 792 793 794/*=== Iostream printing ================================================*/ 795 796class bdd_ioformat 797{ 798 public: 799 bdd_ioformat(int f) { format=f; } 800 private: 801 bdd_ioformat(void) { } 802 int format; 803 static int curformat; 804 805 friend std::ostream &operator<<(std::ostream &, const bdd_ioformat &); 806 friend std::ostream &operator<<(std::ostream &, const bdd &); 807}; 808 809std::ostream &operator<<(std::ostream &, const bdd &); 810std::ostream &operator<<(std::ostream &, const bdd_ioformat &); 811 812extern bdd_ioformat bddset; 813extern bdd_ioformat bddtable; 814extern bdd_ioformat bdddot; 815extern bdd_ioformat bddall; 816extern bdd_ioformat fddset; 817 818typedef void (*bddstrmhandler)(std::ostream &, int); 819 820extern bddstrmhandler bdd_strm_hook(bddstrmhandler); 821 822#endif /* CPLUSPLUS */ 823 824#endif /* _BDD_H */ 825 826/* EOF */ 827