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