bddx.h 33.4 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
/*========================================================================
Alexandre Duret-Lutz's avatar
.    
Alexandre Duret-Lutz committed
2
	       Copyright (C) 1996-2003 by Jorn Lind-Nielsen
3
			    All rights reserved
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

    Permission is hereby granted, without written agreement and without
    license or royalty fees, to use, reproduce, prepare derivative
    works, distribute, and display this software and its documentation
    for any purpose, provided that (1) the above copyright notice and
    the following two paragraphs appear in all copies of the source code
    and (2) redistributions, including without limitation binaries,
    reproduce these notices in the supporting documentation. Substantial
    modifications to this software may be copyrighted by their authors
    and need not follow the licensing terms described here, provided
    that the new terms are clearly indicated in all files where they apply.

    IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
    SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
    INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
    SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
    ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

    JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
    BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
    FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
    ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
    OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
    MODIFICATIONS.
========================================================================*/

/*************************************************************************
Alexandre Duret-Lutz's avatar
.    
Alexandre Duret-Lutz committed
31
  $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.6 2003/08/06 14:19:29 aduret Exp $
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
32
33
34
35
36
37
  FILE:  bdd.h
  DESCR: C,C++ User interface for the BDD package
  AUTH:  Jorn Lind
  DATE:  (C) feb 1997
*************************************************************************/

38
39
#ifndef _BDDX_H
#define _BDDX_H
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
40

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
41
42
43
44
#if __GNUC__ >= 3
#define __purefn __attribute__((__pure__))
#define __constfn __attribute__((__const__))
#define __noreturnfn __attribute__((__noreturn__))
45
46
#define __likely(expr)   __builtin_expect(!!(expr), 1)
#define __unlikely(expr) __builtin_expect(!!(expr), 0)
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
47
48
49
50
#else
#define __purefn
#define __constfn
#define __noreturnfn
51
52
#define __likely(expr) (expr)
#define __unlikely(expr) (expr)
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
53
54
#endif

55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
#if defined _WIN32 || defined __CYGWIN__
  #define BUDDY_HELPER_DLL_IMPORT __declspec(dllimport)
  #define BUDDY_HELPER_DLL_EXPORT __declspec(dllexport)
  #define BUDDY_HELPER_DLL_LOCAL
#else
  #if __GNUC__ >= 4
    #define BUDDY_HELPER_DLL_IMPORT __attribute__ ((visibility ("default")))
    #define BUDDY_HELPER_DLL_EXPORT __attribute__ ((visibility ("default")))
    #define BUDDY_HELPER_DLL_LOCAL  __attribute__ ((visibility ("hidden")))
  #else
    #define BUDDY_HELPER_DLL_IMPORT
    #define BUDDY_HELPER_DLL_EXPORT
    #define BUDDY_HELPER_DLL_LOCAL
  #endif
#endif

// BUDDY_API is used for the public API symbols. It either DLL imports
// or DLL exports (or does nothing for static build) BUDDY_LOCAL is
// used for non-api symbols.
#ifdef BUDDY_DLL
  #ifdef BUDDY_DLL_EXPORTS
    #define BUDDY_API BUDDY_HELPER_DLL_EXPORT
  #else
    #define BUDDY_API BUDDY_HELPER_DLL_IMPORT
  #endif
  #define BUDDY_LOCAL BUDDY_HELPER_DLL_LOCAL
#else
  #define BUDDY_API
  #define BUDDY_LOCAL
#endif
#define BUDDY_API_VAR extern BUDDY_API

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
   /* Allow this headerfile to define C++ constructs if requested */
#ifdef __cplusplus
#define CPLUSPLUS
#endif

#include <stdio.h>

/*=== Defined operators for apply calls ================================*/

#define bddop_and       0
#define bddop_xor       1
#define bddop_or        2
#define bddop_nand      3
#define bddop_nor       4
#define bddop_imp       5
#define bddop_biimp     6
#define bddop_diff      7
#define bddop_less      8
#define bddop_invimp    9

   /* Should *not* be used in bdd_apply calls !!! */
#define bddop_not      10
#define bddop_simplify 11


/*=== User BDD types ===================================================*/

typedef int BDD;

#ifndef CPLUSPLUS
typedef BDD bdd;
#endif /* CPLUSPLUS */


typedef struct s_bddPair
{
   BDD *result;
   int last;
   int id;
   struct s_bddPair *next;
} bddPair;


/*=== Status information ===============================================*/

/*
NAME    {* bddStat *}
SECTION {* kernel *}
SHORT   {* Status information about the bdd package *}
PROTO   {* typedef struct s_bddStat
{
   long int produced;
   int nodenum;
   int maxnodenum;
   int freenodes;
   int minfreenodes;
   int varnum;
   int cachesize;
   int gbcnum;
} bddStat;  *}
DESCR   {* The fields are \\[\baselineskip] \begin{tabular}{lp{10cm}}
  {\tt produced}     & total number of new nodes ever produced \\
  {\tt nodenum}      & currently allocated number of bdd nodes \\
  {\tt maxnodenum}   & user defined maximum number of bdd nodes \\
  {\tt freenodes}    & number of currently free nodes \\
  {\tt minfreenodes} & minimum number of nodes that should be left after a
153
		       garbage collection. \\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
  {\tt varnum}       & number of defined bdd variables \\
  {\tt cachesize}    & number of entries in the internal caches \\
  {\tt gbcnum}       & number of garbage collections done until now
  \end{tabular} *}
ALSO    {* bdd\_stats *}
*/
typedef struct s_bddStat
{
   long int produced;
   int nodenum;
   int maxnodenum;
   int freenodes;
   int minfreenodes;
   int varnum;
   int cachesize;
   int gbcnum;
} bddStat;


/*
NAME    {* bddGbcStat *}
SECTION {* kernel *}
SHORT   {* Status information about garbage collections *}
PROTO   {* typedef struct s_bddGbcStat
{
   int nodes;
   int freenodes;
   long time;
   long sumtime;
   int num;
} bddGbcStat;  *}
DESCR   {* The fields are \\[\baselineskip] \begin{tabular}{ll}
  {\tt nodes}     & Total number of allocated nodes in the nodetable \\
  {\tt freenodes} & Number of free nodes in the nodetable \\
  {\tt time}      & Time used for garbage collection this time \\
  {\tt sumtime}   & Total time used for garbage collection \\
  {\tt num}       & number of garbage collections done until now
  \end{tabular} *}
ALSO    {* bdd\_gbc\_hook *}
*/
typedef struct s_bddGbcStat
{
   int nodes;
   int freenodes;
   long time;
   long sumtime;
   int num;
} bddGbcStat;


/*
NAME    {* bddCacheStat *}
SECTION {* kernel *}
SHORT   {* Status information about cache usage *}
PROTO   {* typedef struct s_bddCacheStat
{
   long unsigned int uniqueAccess;
   long unsigned int uniqueChain;
   long unsigned int uniqueHit;
   long unsigned int uniqueMiss;
   long unsigned int opHit;
   long unsigned int opMiss;
   long unsigned int swapCount;
} bddCacheStat; *}
DESCR   {* The fields are \\[\baselineskip] \begin{tabular}{ll}
  {\bf Name}         & {\bf Number of } \\
  uniqueAccess & accesses to the unique node table \\
  uniqueChain  & iterations through the cache chains in the unique node table\\
  uniqueHit    & entries actually found in the the unique node table \\
  uniqueMiss   & entries not found in the the unique node table \\
  opHit        & entries found in the operator caches \\
  opMiss       & entries not found in the operator caches \\
  swapCount    & number of variable swaps in reordering \\
\end{tabular} *}
ALSO    {* bdd\_cachestats *}
*/
typedef struct s_bddCacheStat
{
   long unsigned int uniqueAccess;
   long unsigned int uniqueChain;
   long unsigned int uniqueHit;
   long unsigned int uniqueMiss;
   long unsigned int opHit;
   long unsigned int opMiss;
   long unsigned int swapCount;
} bddCacheStat;

/*=== BDD interface prototypes =========================================*/

/*
NAME    {* bdd\_relprod *}
SECTION {* operator *}
SHORT   {* relational product *}
PROTO   {* #define bdd_relprod(a,b,var) bdd_appex(a,b,bddop_and,var) *}
DESCR   {* Calculates the relational product of {\tt a} and {\tt b} as
249
	   {\tt a AND b} with the variables in {\tt var} quantified out
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
	   afterwards. *}
RETURN  {* The relational product or {\tt bddfalse} on errors. *}
ALSO    {* bdd\_appex *}
*/
#define bdd_relprod(a,b,var) bdd_appex((a),(b),bddop_and,(var))


  /* In file "kernel.c" */

#ifdef CPLUSPLUS
extern "C" {
#endif

typedef void (*bddinthandler)(int);
typedef void (*bddgbchandler)(int,bddGbcStat*);
typedef void (*bdd2inthandler)(int,int);
typedef int  (*bddsizehandler)(void);
typedef void (*bddfilehandler)(FILE *, int);
typedef void (*bddallsathandler)(char*, int);
269

270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
BUDDY_API bddinthandler  bdd_error_hook(bddinthandler);
BUDDY_API bddgbchandler  bdd_gbc_hook(bddgbchandler);
BUDDY_API bdd2inthandler bdd_resize_hook(bdd2inthandler);
BUDDY_API bddinthandler  bdd_reorder_hook(bddinthandler);
BUDDY_API bddfilehandler bdd_file_hook(bddfilehandler);

BUDDY_API int      bdd_init(int, int);
BUDDY_API void     bdd_done(void);
BUDDY_API int      bdd_setvarnum(int);
BUDDY_API int      bdd_extvarnum(int);
BUDDY_API int      bdd_isrunning(void) __purefn;
BUDDY_API int      bdd_setmaxnodenum(int);
BUDDY_API int      bdd_setmaxincrease(int);
BUDDY_API int      bdd_setminfreenodes(int);
BUDDY_API int      bdd_getnodenum(void) __purefn;
BUDDY_API int      bdd_getallocnum(void) __purefn;
BUDDY_API char*    bdd_versionstr(void) __purefn;
BUDDY_API int      bdd_versionnum(void) __constfn;
BUDDY_API void     bdd_stats(bddStat *);
BUDDY_API void     bdd_cachestats(bddCacheStat *);
BUDDY_API void     bdd_fprintstat(FILE *);
BUDDY_API void     bdd_printstat(void);
BUDDY_API void     bdd_default_gbchandler(int, bddGbcStat *);
BUDDY_API void     bdd_default_errhandler(int) __noreturnfn;
BUDDY_API const char *bdd_errstring(int) __constfn;
BUDDY_API void     bdd_clear_error(void);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
296
#ifndef CPLUSPLUS
297
298
BUDDY_API BDD      bdd_true(void) __constfn;
BUDDY_API BDD      bdd_false(void) __constfn;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
299
#endif
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
BUDDY_API int      bdd_varnum(void) __purefn;
BUDDY_API BDD      bdd_ithvar(int) __purefn;
BUDDY_API BDD      bdd_nithvar(int) __purefn;
BUDDY_API int      bdd_var(BDD) __purefn;
BUDDY_API BDD      bdd_low(BDD) __purefn;
BUDDY_API BDD      bdd_high(BDD) __purefn;
BUDDY_API int      bdd_varlevel(int) __purefn;
BUDDY_API BDD      bdd_addref_nc(BDD);
BUDDY_API BDD      bdd_addref(BDD);
BUDDY_API BDD      bdd_delref_nc(BDD);
BUDDY_API BDD      bdd_delref(BDD);
BUDDY_API void     bdd_gbc(void);
BUDDY_API int      bdd_scanset(BDD, int**, int*);
BUDDY_API BDD      bdd_makeset(int *, int);
BUDDY_API bddPair* bdd_copypair(bddPair*);
BUDDY_API bddPair* bdd_mergepairs(bddPair*, bddPair*);
BUDDY_API bddPair* bdd_newpair(void);
BUDDY_API int      bdd_setpair(bddPair*, int, int);
BUDDY_API int      bdd_setpairs(bddPair*, int*, int*, int);
BUDDY_API int      bdd_setbddpair(bddPair*, int, BDD);
BUDDY_API int      bdd_setbddpairs(bddPair*, int*, BDD*, int);
BUDDY_API void     bdd_resetpair(bddPair *);
BUDDY_API void     bdd_freepair(bddPair*);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
323
324
325

  /* In bddop.c */

326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
BUDDY_API int      bdd_setcacheratio(int);
BUDDY_API BDD      bdd_buildcube(int, int, BDD *);
BUDDY_API BDD      bdd_ibuildcube(int, int, int *);
BUDDY_API BDD      bdd_not(BDD);
BUDDY_API BDD      bdd_apply(BDD, BDD, int);
BUDDY_API BDD      bdd_and(BDD, BDD);
BUDDY_API BDD      bdd_or(BDD, BDD);
BUDDY_API BDD      bdd_xor(BDD, BDD);
BUDDY_API BDD      bdd_imp(BDD, BDD);
BUDDY_API BDD      bdd_biimp(BDD, BDD);
BUDDY_API BDD      bdd_setxor(BDD, BDD);
BUDDY_API int      bdd_implies(BDD, BDD);
BUDDY_API BDD      bdd_ite(BDD, BDD, BDD);
BUDDY_API BDD      bdd_restrict(BDD, BDD);
BUDDY_API BDD      bdd_constrain(BDD, BDD);
BUDDY_API BDD      bdd_replace(BDD, bddPair*);
BUDDY_API BDD      bdd_compose(BDD, BDD, BDD);
BUDDY_API BDD      bdd_veccompose(BDD, bddPair*);
BUDDY_API BDD      bdd_simplify(BDD, BDD);
BUDDY_API BDD      bdd_exist(BDD, BDD);
BUDDY_API BDD      bdd_existcomp(BDD, BDD);
BUDDY_API BDD      bdd_forall(BDD, BDD);
BUDDY_API BDD      bdd_forallcomp(BDD, BDD);
BUDDY_API BDD      bdd_unique(BDD, BDD);
BUDDY_API BDD      bdd_uniquecomp(BDD, BDD);
BUDDY_API BDD      bdd_appex(BDD, BDD, int, BDD);
BUDDY_API BDD      bdd_appexcomp(BDD, BDD, int, BDD);
BUDDY_API BDD      bdd_appall(BDD, BDD, int, BDD);
BUDDY_API BDD      bdd_appallcomp(BDD, BDD, int, BDD);
BUDDY_API BDD      bdd_appuni(BDD, BDD, int, BDD);
BUDDY_API BDD      bdd_appunicomp(BDD, BDD, int, BDD);
BUDDY_API BDD      bdd_support(BDD);
BUDDY_API BDD      bdd_satone(BDD);
BUDDY_API BDD      bdd_satoneset(BDD, BDD, BDD);
BUDDY_API BDD      bdd_fullsatone(BDD);
BUDDY_API BDD	bdd_satprefix(BDD *);
BUDDY_API void     bdd_allsat(BDD r, bddallsathandler handler);
BUDDY_API double   bdd_satcount(BDD);
BUDDY_API double   bdd_satcountset(BDD, BDD);
BUDDY_API double   bdd_satcountln(BDD);
BUDDY_API double   bdd_satcountlnset(BDD, BDD);
BUDDY_API int      bdd_nodecount(BDD);
BUDDY_API int      bdd_anodecount(BDD *, int);
BUDDY_API int*     bdd_varprofile(BDD);
BUDDY_API double   bdd_pathcount(BDD);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
371

372

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
373
374
/* In file "bddio.c" */

375
376
377
378
379
380
381
382
383
384
385
386
387
BUDDY_API void     bdd_printall(void);
BUDDY_API void     bdd_fprintall(FILE *);
BUDDY_API void     bdd_fprinttable(FILE *, BDD);
BUDDY_API void     bdd_printtable(BDD);
BUDDY_API void     bdd_fprintset(FILE *, BDD);
BUDDY_API void     bdd_printset(BDD);
BUDDY_API int      bdd_fnprintdot(char *, BDD);
BUDDY_API void     bdd_fprintdot(FILE *, BDD);
BUDDY_API void     bdd_printdot(BDD);
BUDDY_API int      bdd_fnsave(char *, BDD);
BUDDY_API int      bdd_save(FILE *, BDD);
BUDDY_API int      bdd_fnload(char *, BDD *);
BUDDY_API int      bdd_load(FILE *ifile, BDD *);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
388
389
390

/* In file reorder.c */

391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
BUDDY_API int      bdd_swapvar(int v1, int v2);
BUDDY_API void     bdd_default_reohandler(int);
BUDDY_API void     bdd_reorder(int);
BUDDY_API int      bdd_reorder_gain(void) __purefn;
BUDDY_API bddsizehandler bdd_reorder_probe(bddsizehandler);
BUDDY_API void     bdd_clrvarblocks(void);
BUDDY_API int      bdd_addvarblock(BDD, int);
BUDDY_API int      bdd_intaddvarblock(int, int, int);
BUDDY_API void     bdd_varblockall(void);
BUDDY_API bddfilehandler bdd_blockfile_hook(bddfilehandler);
BUDDY_API int      bdd_autoreorder(int);
BUDDY_API int      bdd_autoreorder_times(int, int);
BUDDY_API int      bdd_var2level(int);
BUDDY_API int      bdd_level2var(int);
BUDDY_API int      bdd_getreorder_times(void) __purefn;
BUDDY_API int      bdd_getreorder_method(void) __purefn;
BUDDY_API void     bdd_enable_reorder(void);
BUDDY_API void     bdd_disable_reorder(void);
BUDDY_API int      bdd_reorder_verbose(int);
BUDDY_API void     bdd_setvarorder(int *);
BUDDY_API void     bdd_printorder(void);
BUDDY_API void     bdd_fprintorder(FILE *);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
413
414
415
416
417
418
419
420
421
422

#ifdef CPLUSPLUS
}
#endif


/*=== BDD constants ====================================================*/

#ifndef CPLUSPLUS

423
424
BUDDY_API_VAR const BDD bddfalse;
BUDDY_API_VAR const BDD bddtrue;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
425
426
427
428

#endif /* CPLUSPLUS */


429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
/*=== Reordering algorithms ============================================*/

#define BDD_REORDER_NONE     0
#define BDD_REORDER_WIN2     1
#define BDD_REORDER_WIN2ITE  2
#define BDD_REORDER_SIFT     3
#define BDD_REORDER_SIFTITE  4
#define BDD_REORDER_WIN3     5
#define BDD_REORDER_WIN3ITE  6
#define BDD_REORDER_RANDOM   7

#define BDD_REORDER_FREE     0
#define BDD_REORDER_FIXED    1


/*=== Error codes ======================================================*/

#define BDD_MEMORY (-1)   /* Out of memory */
#define BDD_VAR (-2)      /* Unknown variable */
#define BDD_RANGE (-3)    /* Variable value out of range (not in domain) */
#define BDD_DEREF (-4)    /* Removing external reference to unknown node */
#define BDD_RUNNING (-5)  /* Called bdd_init() twice whithout bdd_done() */
#define BDD_FILE (-6)     /* Some file operation failed */
#define BDD_FORMAT (-7)   /* Incorrect file format */
#define BDD_ORDER (-8)    /* Vars. not in order for vector based functions */
#define BDD_BREAK (-9)    /* User called break */
#define BDD_VARNUM (-10)  /* Different number of vars. for vector pair */
#define BDD_NODES (-11)   /* Tried to set max. number of nodes to be fewer */
			  /* than there already has been allocated */
#define BDD_OP (-12)      /* Unknown operator */
#define BDD_VARSET (-13)  /* Illegal variable set */
#define BDD_VARBLK (-14)  /* Bad variable block operation */
#define BDD_DECVNUM (-15) /* Trying to decrease the number of variables */
#define BDD_REPLACE (-16) /* Replacing to already existing variables */
#define BDD_NODENUM (-17) /* Number of nodes reached user defined maximum */
#define BDD_ILLBDD (-18)  /* Illegal bdd argument */
#define BDD_SIZE (-19)    /* Illegal size argument */

#define BVEC_SIZE (-20)    /* Mismatch in bitvector size */
#define BVEC_SHIFT (-21)   /* Illegal shift-left/right parameter */
#define BVEC_DIVZERO (-22) /* Division by zero */

#define BDD_INVMERGE (-23) /* Merging clashing rewriting rules */

#define BDD_ERRNUM 25

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
475
476
477
478
479
480
481
482
483
/*************************************************************************
   If this file is included from a C++ compiler then the following
   classes, wrappers and hacks are supplied.
*************************************************************************/
#ifdef CPLUSPLUS
#include <iostream>

/*=== User BDD class ===================================================*/

484
class BUDDY_API bvec;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
485

486
487
488
class BUDDY_API bddxfalse;
class BUDDY_API bddxtrue;

489
class BUDDY_API bdd
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
490
491
492
{
 public:

493
494
495
496
   bdd(void) noexcept
   {
     root=0;
   }
497

498
499
500
501
502
503
504
   bdd(const bdd &r) noexcept
   {
     root=r.root;
     if (root > 1)
       bdd_addref_nc(root);
   }

505
506
507
508
509
510
511
512
513
514
   bdd(const bddxfalse &) noexcept
   {
     root = 0;
   }

   bdd(const bddxtrue &) noexcept
   {
     root = 1;
   }

515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
   bdd(bdd&& r) noexcept
   {
     root=r.root;
     r.root = 0;
   }

   ~bdd(void) noexcept
   {
     if (root > 1)
       bdd_delref_nc(root);
   }

   int id(void) const noexcept;

   bdd& operator=(const bdd &r) noexcept;
   bdd& operator=(bdd&& r) noexcept;
531

532
533
534
   bdd& operator=(const bddxtrue&) noexcept;
   bdd& operator=(const bddxfalse&) noexcept;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
535
   bdd operator&(const bdd &r) const;
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
536
   bdd& operator&=(const bdd &r);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
537
   bdd operator^(const bdd &r) const;
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
538
   bdd& operator^=(const bdd &r);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
539
   bdd operator|(const bdd &r) const;
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
540
   bdd& operator|=(const bdd &r);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
541
542
   bdd operator!(void) const;
   bdd operator>>(const bdd &r) const;
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
543
   bdd& operator>>=(const bdd &r);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
544
   bdd operator-(const bdd &r) const;
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
545
   bdd& operator-=(const bdd &r);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
546
547
548
   bdd operator>(const bdd &r) const;
   bdd operator<(const bdd &r) const;
   bdd operator<<(const bdd &r) const;
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
549
   bdd& operator<<=(const bdd &r);
550
   int operator==(const bdd &r) const noexcept;
551
552
   int operator==(const bddxfalse&) const noexcept;
   int operator==(const bddxtrue&) const noexcept;
553
   int operator!=(const bdd &r) const noexcept;
554
555
   int operator!=(const bddxfalse&) const noexcept;
   int operator!=(const bddxtrue&) const noexcept;
556

557
protected:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
558
559
   BDD root;

560
561
   bdd(BDD r) noexcept { root=r; if (root > 1) bdd_addref_nc(root); }
   bdd& operator=(BDD r) noexcept;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
562
563
564

   friend int      bdd_init(int, int);
   friend int      bdd_setvarnum(int);
565
566
   friend bddxtrue bdd_true(void);
   friend bddxfalse bdd_false(void);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
   friend bdd      bdd_ithvarpp(int);
   friend bdd      bdd_nithvarpp(int);
   friend int      bdd_var(const bdd &);
   friend bdd      bdd_low(const bdd &);
   friend bdd      bdd_high(const bdd &);
   friend int      bdd_scanset(const bdd &, int *&, int &);
   friend bdd      bdd_makesetpp(int *, int);
   friend int      bdd_setbddpair(bddPair*, int, const bdd &);
   friend int      bdd_setbddpairs(bddPair*, int*, const bdd *, int);
   friend bdd      bdd_buildcube(int, int, const bdd *);
   friend bdd      bdd_ibuildcubepp(int, int, int *);
   friend bdd      bdd_not(const bdd &);
   friend bdd      bdd_simplify(const bdd &, const bdd &);
   friend bdd      bdd_apply(const bdd &, const bdd &, int);
   friend bdd      bdd_and(const bdd &, const bdd &);
   friend bdd      bdd_or(const bdd &, const bdd &);
   friend bdd      bdd_xor(const bdd &, const bdd &);
   friend bdd      bdd_imp(const bdd &, const bdd &);
   friend bdd      bdd_biimp(const bdd &, const bdd &);
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
586
   friend bdd      bdd_setxor(const bdd &, const bdd &);
587
   friend int      bdd_implies(const bdd &, const bdd &) noexcept;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
588
589
590
591
   friend bdd      bdd_ite(const bdd &, const bdd &, const bdd &);
   friend bdd      bdd_restrict(const bdd &, const bdd &);
   friend bdd      bdd_constrain(const bdd &, const bdd &);
   friend bdd      bdd_exist(const bdd &, const bdd &);
592
   friend bdd      bdd_existcomp(const bdd &, const bdd &);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
593
   friend bdd      bdd_forall(const bdd &, const bdd &);
594
   friend bdd      bdd_forallcomp(const bdd &, const bdd &);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
595
   friend bdd      bdd_unique(const bdd &, const bdd &);
596
   friend bdd      bdd_uniquecomp(const bdd &, const bdd &);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
597
   friend bdd      bdd_appex(const bdd &, const bdd &, int, const bdd &);
598
   friend bdd      bdd_appexcomp(const bdd &, const bdd &, int, const bdd &);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
599
   friend bdd      bdd_appall(const bdd &, const bdd &, int, const bdd &);
600
   friend bdd      bdd_appallcomp(const bdd &, const bdd &, int, const bdd &);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
601
   friend bdd      bdd_appuni(const bdd &, const bdd &, int, const bdd &);
602
   friend bdd      bdd_appunicomp(const bdd &, const bdd &, int, const bdd &);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
603
604
605
606
607
608
609
   friend bdd      bdd_replace(const bdd &, bddPair*);
   friend bdd      bdd_compose(const bdd &, const bdd &, int);
   friend bdd      bdd_veccompose(const bdd &, bddPair*);
   friend bdd      bdd_support(const bdd &);
   friend bdd      bdd_satone(const bdd &);
   friend bdd      bdd_satoneset(const bdd &, const bdd &, const bdd &);
   friend bdd      bdd_fullsatone(const bdd &);
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
610
   friend bdd      bdd_satprefix(bdd &);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
611
612
613
614
615
616
617
618
619
   friend void     bdd_allsat(const bdd &r, bddallsathandler handler);
   friend double   bdd_satcount(const bdd &);
   friend double   bdd_satcountset(const bdd &, const bdd &);
   friend double   bdd_satcountln(const bdd &);
   friend double   bdd_satcountlnset(const bdd &, const bdd &);
   friend int      bdd_nodecount(const bdd &);
   friend int      bdd_anodecountpp(const bdd *, int);
   friend int*     bdd_varprofile(const bdd &);
   friend double   bdd_pathcount(const bdd &);
620

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
621
622
623
624
625
626
627
628
629
630
631
632
   friend void   bdd_fprinttable(FILE *, const bdd &);
   friend void   bdd_printtable(const bdd &);
   friend void   bdd_fprintset(FILE *, const bdd &);
   friend void   bdd_printset(const bdd &);
   friend void   bdd_printdot(const bdd &);
   friend int    bdd_fnprintdot(char*, const bdd &);
   friend void   bdd_fprintdot(FILE*, const bdd &);
   friend std::ostream &operator<<(std::ostream &, const bdd &);
   friend int    bdd_fnsave(char*, const bdd &);
   friend int    bdd_save(FILE*, const bdd &);
   friend int    bdd_fnload(char*, bdd &);
   friend int    bdd_load(FILE*, bdd &);
633

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
   friend bdd    fdd_ithvarpp(int, int);
   friend bdd    fdd_ithsetpp(int);
   friend bdd    fdd_domainpp(int);
   friend int    fdd_scanvar(const bdd &, int);
   friend int*   fdd_scanallvar(const bdd &);
   friend bdd    fdd_equalspp(int, int);
   friend void   fdd_printset(const bdd &);
   friend void   fdd_fprintset(FILE*, const bdd &);
   friend bdd    fdd_makesetpp(int*, int);
   friend int    fdd_scanset(const bdd &, int *&, int &);

   friend int    bdd_addvarblock(const bdd &, int);

   friend class bvec;
   friend bvec bvec_ite(const bdd& a, const bvec& b, const bvec& c);
   friend bvec bvec_shlfixed(const bvec &e, int pos, const bdd &c);
   friend bvec bvec_shl(const bvec &left, const bvec &right, const bdd &c);
   friend bvec bvec_shrfixed(const bvec &e, int pos, const bdd &c);
   friend bvec bvec_shr(const bvec &left, const bvec &right, const bdd &c);
   friend bdd  bvec_lth(const bvec &left, const bvec &right);
   friend bdd  bvec_lte(const bvec &left, const bvec &right);
   friend bdd  bvec_gth(const bvec &left, const bvec &right);
   friend bdd  bvec_gte(const bvec &left, const bvec &right);
   friend bdd  bvec_equ(const bvec &left, const bvec &right);
   friend bdd  bvec_neq(const bvec &left, const bvec &right);
};

661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
class bddxfalse: public bdd
{
public:
  bddxfalse(void) noexcept
    {
      root=0;
    }
};

class bddxtrue: public bdd
{
public:
  bddxtrue(void) noexcept
    {
      root=1;
    }
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
678
679
680

/*=== BDD constants ====================================================*/

681
682
BUDDY_API_VAR const bddxfalse bddfalsepp;
BUDDY_API_VAR const bddxtrue bddtruepp;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
683
684
685
686
687
688

#define bddtrue bddtruepp
#define bddfalse bddfalsepp

/*=== C++ interface ====================================================*/

689
BUDDY_API int bdd_cpp_init(int, int);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761

inline void bdd_stats(bddStat& s)
{ bdd_stats(&s); }

inline bdd bdd_ithvarpp(int v)
{ return bdd_ithvar(v); }

inline bdd bdd_nithvarpp(int v)
{ return bdd_nithvar(v); }

inline int bdd_var(const bdd &r)
{ return bdd_var(r.root); }

inline bdd bdd_low(const bdd &r)
{ return bdd_low(r.root); }

inline bdd bdd_high(const bdd &r)
{ return bdd_high(r.root); }

inline int bdd_scanset(const bdd &r, int *&v, int &n)
{ return bdd_scanset(r.root, &v, &n); }

inline bdd bdd_makesetpp(int *v, int n)
{ return bdd(bdd_makeset(v,n)); }

inline int bdd_setbddpair(bddPair *p, int ov, const bdd &nv)
{ return bdd_setbddpair(p,ov,nv.root); }

   /* In bddop.c */

inline bdd bdd_replace(const bdd &r, bddPair *p)
{ return bdd_replace(r.root, p); }

inline bdd bdd_compose(const bdd &f, const bdd &g, int v)
{ return bdd_compose(f.root, g.root, v); }

inline bdd bdd_veccompose(const bdd &f, bddPair *p)
{ return bdd_veccompose(f.root, p); }

inline bdd bdd_restrict(const bdd &r, const bdd &var)
{ return bdd_restrict(r.root, var.root); }

inline bdd bdd_constrain(const bdd &f, const bdd &c)
{ return bdd_constrain(f.root, c.root); }

inline bdd bdd_simplify(const bdd &d, const bdd &b)
{ return bdd_simplify(d.root, b.root); }

inline bdd bdd_ibuildcubepp(int v, int w, int *a)
{ return bdd_ibuildcube(v,w,a); }

inline bdd bdd_not(const bdd &r)
{ return bdd_not(r.root); }

inline bdd bdd_apply(const bdd &l, const bdd &r, int op)
{ return bdd_apply(l.root, r.root, op); }

inline bdd bdd_and(const bdd &l, const bdd &r)
{ return bdd_apply(l.root, r.root, bddop_and); }

inline bdd bdd_or(const bdd &l, const bdd &r)
{ return bdd_apply(l.root, r.root, bddop_or); }

inline bdd bdd_xor(const bdd &l, const bdd &r)
{ return bdd_apply(l.root, r.root, bddop_xor); }

inline bdd bdd_imp(const bdd &l, const bdd &r)
{ return bdd_apply(l.root, r.root, bddop_imp); }

inline bdd bdd_biimp(const bdd &l, const bdd &r)
{ return bdd_apply(l.root, r.root, bddop_biimp); }

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
762
763
764
inline bdd bdd_setxor(const bdd &l, const bdd &r)
{ return bdd_setxor(l.root, r.root); }

765
inline int bdd_implies(const bdd &l, const bdd &r) noexcept
766
767
{ return bdd_implies(l.root, r.root); }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
768
769
770
771
772
773
inline bdd bdd_ite(const bdd &f, const bdd &g, const bdd &h)
{ return bdd_ite(f.root, g.root, h.root); }

inline bdd bdd_exist(const bdd &r, const bdd &var)
{ return bdd_exist(r.root, var.root); }

774
775
776
inline bdd bdd_existcomp(const bdd &r, const bdd &var)
{ return bdd_existcomp(r.root, var.root); }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
777
778
779
inline bdd bdd_forall(const bdd &r, const bdd &var)
{ return bdd_forall(r.root, var.root); }

780
781
782
inline bdd bdd_forallcomp(const bdd &r, const bdd &var)
{ return bdd_forallcomp(r.root, var.root); }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
783
784
785
inline bdd bdd_unique(const bdd &r, const bdd &var)
{ return bdd_unique(r.root, var.root); }

786
787
788
inline bdd bdd_uniquecomp(const bdd &r, const bdd &var)
{ return bdd_uniquecomp(r.root, var.root); }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
789
790
791
inline bdd bdd_appex(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appex(l.root, r.root, op, var.root); }

792
793
794
inline bdd bdd_appexcomp(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appexcomp(l.root, r.root, op, var.root); }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
795
796
797
inline bdd bdd_appall(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appall(l.root, r.root, op, var.root); }

798
799
800
inline bdd bdd_appallcomp(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appallcomp(l.root, r.root, op, var.root); }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
801
802
803
inline bdd bdd_appuni(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appuni(l.root, r.root, op, var.root); }

804
805
806
inline bdd bdd_appunicomp(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appunicomp(l.root, r.root, op, var.root); }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
807
808
809
810
811
812
813
814
815
816
817
818
inline bdd bdd_support(const bdd &r)
{ return bdd_support(r.root); }

inline bdd bdd_satone(const bdd &r)
{ return bdd_satone(r.root); }

inline bdd bdd_satoneset(const bdd &r, const bdd &var, const bdd &pol)
{ return bdd_satoneset(r.root, var.root, pol.root); }

inline bdd bdd_fullsatone(const bdd &r)
{ return bdd_fullsatone(r.root); }

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
819
820
821
inline bdd bdd_satprefix(bdd &r)
{ int ro = r.root; bdd res = bdd_satprefix(&ro); r = bdd(ro); return res; }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
inline void bdd_allsat(const bdd &r, bddallsathandler handler)
{ bdd_allsat(r.root, handler); }

inline double bdd_satcount(const bdd &r)
{ return bdd_satcount(r.root); }

inline double bdd_satcountset(const bdd &r, const bdd &varset)
{ return bdd_satcountset(r.root, varset.root); }

inline double bdd_satcountln(const bdd &r)
{ return bdd_satcountln(r.root); }

inline double bdd_satcountlnset(const bdd &r, const bdd &varset)
{ return bdd_satcountlnset(r.root, varset.root); }

inline int bdd_nodecount(const bdd &r)
{ return bdd_nodecount(r.root); }

inline int* bdd_varprofile(const bdd &r)
{ return bdd_varprofile(r.root); }

inline double bdd_pathcount(const bdd &r)
{ return bdd_pathcount(r.root); }


   /* I/O extensions */

inline void bdd_fprinttable(FILE *file, const bdd &r)
{ bdd_fprinttable(file, r.root); }

inline void bdd_printtable(const bdd &r)
{ bdd_printtable(r.root); }

inline void bdd_fprintset(FILE *file, const bdd &r)
{ bdd_fprintset(file, r.root); }

inline void bdd_printset(const bdd &r)
{ bdd_printset(r.root); }

inline void bdd_printdot(const bdd &r)
{ bdd_printdot(r.root); }

inline void bdd_fprintdot(FILE* ofile, const bdd &r)
{ bdd_fprintdot(ofile, r.root); }

inline int bdd_fnprintdot(char* fname, const bdd &r)
{ return bdd_fnprintdot(fname, r.root); }

inline int bdd_fnsave(char *fname, const bdd &r)
{ return bdd_fnsave(fname, r.root); }

inline int bdd_save(FILE *ofile, const bdd &r)
{ return bdd_save(ofile, r.root); }

inline int bdd_fnload(char *fname, bdd &r)
{ int lr,e; e=bdd_fnload(fname, &lr); r=bdd(lr); return e; }

inline int bdd_load(FILE *ifile, bdd &r)
{ int lr,e; e=bdd_load(ifile, &lr); r=bdd(lr); return e; }

inline int bdd_addvarblock(const bdd &v, int f)
{ return bdd_addvarblock(v.root, f); }

   /* Hack to allow for overloading */
#define bdd_init bdd_cpp_init
#define bdd_ithvar bdd_ithvarpp
#define bdd_nithvar bdd_nithvarpp
#define bdd_makeset bdd_makesetpp
#define bdd_ibuildcube bdd_ibuildcubepp
#define bdd_anodecount bdd_anodecountpp

/*=== Inline C++ functions =============================================*/

895
inline int bdd::id(void) const noexcept
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
896
897
898
899
900
{ return root; }

inline bdd bdd::operator&(const bdd &r) const
{ return bdd_apply(*this,r,bddop_and); }

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
901
inline bdd& bdd::operator&=(const bdd &r)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
902
903
904
905
906
{ return (*this=bdd_apply(*this,r,bddop_and)); }

inline bdd bdd::operator^(const bdd &r) const
{ return bdd_apply(*this,r,bddop_xor); }

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
907
inline bdd& bdd::operator^=(const bdd &r)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
908
909
910
911
912
{ return (*this=bdd_apply(*this,r,bddop_xor)); }

inline bdd bdd::operator|(const bdd &r) const
{ return bdd_apply(*this,r,bddop_or); }

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
913
inline bdd& bdd::operator|=(const bdd &r)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
914
915
916
917
918
919
920
921
{ return (*this=bdd_apply(*this,r,bddop_or)); }

inline bdd bdd::operator!(void) const
{ return bdd_not(*this);}

inline bdd bdd::operator>>(const bdd &r) const
{ return bdd_apply(*this,r,bddop_imp); }

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
922
inline bdd& bdd::operator>>=(const bdd &r)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
923
924
925
926
927
{ return (*this=bdd_apply(*this,r,bddop_imp)); }

inline bdd bdd::operator-(const bdd &r) const
{ return bdd_apply(*this,r,bddop_diff); }

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
928
inline bdd& bdd::operator-=(const bdd &r)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
929
930
931
932
933
934
935
936
937
938
939
{ return (*this=bdd_apply(*this,r,bddop_diff)); }

inline bdd bdd::operator>(const bdd &r) const
{ return bdd_apply(*this,r,bddop_diff); }

inline bdd bdd::operator<(const bdd &r) const
{ return bdd_apply(*this,r,bddop_less); }

inline bdd bdd::operator<<(const bdd &r) const
{ return bdd_apply(*this,r,bddop_invimp); }

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
940
inline bdd& bdd::operator<<=(const bdd &r)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
941
942
{ return (*this=bdd_apply(*this,r,bddop_invimp)); }

943
inline int bdd::operator==(const bdd &r) const noexcept
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
944
945
{ return r.root==root; }

946
947
948
949
950
951
inline int bdd::operator==(const bddxfalse&) const noexcept
{ return root==0; }

inline int bdd::operator==(const bddxtrue&) const noexcept
{ return root==1; }

952
inline int bdd::operator!=(const bdd &r) const noexcept
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
953
954
{ return r.root!=root; }

955
956
957
958
959
960
inline int bdd::operator!=(const bddxfalse&) const noexcept
{ return root!=0; }

inline int bdd::operator!=(const bddxtrue&) const noexcept
{ return root!=1; }

961
inline bdd& bdd::operator=(const bdd &r) noexcept
962
963
964
965
966
967
968
969
970
971
972
973
{
  if (__likely(root != r.root))
    {
      if (root > 1)
	bdd_delref_nc(root);
      root = r.root;
      if (root > 1)
	bdd_addref_nc(root);
    }
  return *this;
}

974
975
976
977
978
979
980
981
982
983
inline bdd& bdd::operator=(bdd&& r) noexcept
{
  if (root > 1)
    bdd_delref_nc(root);
  root = r.root;
  r.root = 0;
  return *this;
}

inline bdd& bdd::operator=(int r) noexcept
984
985
986
987
988
989
990
991
992
993
994
995
{
  if (__likely(root != r))
    {
      if (root > 1)
	bdd_delref_nc(root);
      root = r;
      if (root > 1)
	bdd_addref_nc(root);
    }
  return *this;
}

996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
inline bdd& bdd::operator=(const bddxfalse &) noexcept
{
  if (root > 1)
    bdd_delref_nc(root);
  root = 0;
  return *this;
}

inline bdd& bdd::operator=(const bddxtrue &) noexcept
{
  if (root > 1)
    bdd_delref_nc(root);
  root = 1;
  return *this;
}

inline bddxtrue bdd_true(void)
{ return bddxtrue(); }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1014

1015
1016
inline bddxfalse bdd_false(void)
{ return bddxfalse(); }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1017
1018
1019
1020


/*=== Iostream printing ================================================*/

1021
class BUDDY_API bdd_ioformat
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1022
1023
1024
1025
{
 public:
   bdd_ioformat(int f) { format=f; }
 private:
1026
   BUDDY_LOCAL bdd_ioformat(void)  { }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1027
   int format;
1028
   BUDDY_LOCAL static int curformat;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1029
1030
1031
1032
1033

   friend std::ostream &operator<<(std::ostream &, const bdd_ioformat &);
   friend std::ostream &operator<<(std::ostream &, const bdd &);
};

1034
1035
BUDDY_API std::ostream &operator<<(std::ostream &, const bdd &);
BUDDY_API std::ostream &operator<<(std::ostream &, const bdd_ioformat &);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1036

1037
1038
1039
1040
1041
BUDDY_API_VAR bdd_ioformat bddset;
BUDDY_API_VAR bdd_ioformat bddtable;
BUDDY_API_VAR bdd_ioformat bdddot;
BUDDY_API_VAR bdd_ioformat bddall;
BUDDY_API_VAR bdd_ioformat fddset;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1042
1043
1044

typedef void (*bddstrmhandler)(std::ostream &, int);

1045
BUDDY_API bddstrmhandler bdd_strm_hook(bddstrmhandler);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1046
1047
1048

#endif /* CPLUSPLUS */

1049
#endif /* _BDDX_H */
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1050
1051

/* EOF */