kernel.h 9.18 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
/*========================================================================
2
	       Copyright (C) 1996-2002 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/kernel.h,v 1.5 2004/06/28 15:22:13 adl Exp $
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
32
33
34
35
36
37
38
39
40
41
42
43
44
  FILE:  kernel.h
  DESCR: Kernel specific definitions for BDD package
  AUTH:  Jorn Lind
  DATE:  (C) june 1997
*************************************************************************/

#ifndef _KERNEL_H
#define _KERNEL_H

/*=== Includes =========================================================*/

#include <limits.h>
#include <setjmp.h>
45
#include "bddx.h"
46
47
48
#ifdef HAVE_CONFIG_H
# include "config.h"
#endif
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
49
50
51
52
53
54
55
56

/*=== SANITY CHECKS ====================================================*/

   /* Make sure we use at least 32 bit integers */
#if (INT_MAX < 0x7FFFFFFF)
#error The compiler does not support 4 byte integers!
#endif

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
57
58
59
60
#ifdef NDEBUG
#define CHECK(r) (void)(r);
#define CHECKa(r,a) (void)(r); (void)(a);
#define CHECKn(r) (void)(r);
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
61
#define CHECKnc(r) (void)(r);
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
62
#else
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
   /* Sanity check argument and return eventual error code */
#define CHECK(r)\
   if (!bddrunning) return bdd_error(BDD_RUNNING);\
   else if ((r) < 0  ||  (r) >= bddnodesize) return bdd_error(BDD_ILLBDD);\
   else if (r >= 2 && LOW(r) == -1) return bdd_error(BDD_ILLBDD)\

   /* Sanity check argument and return eventually the argument 'a' */
#define CHECKa(r,a)\
   if (!bddrunning) { bdd_error(BDD_RUNNING); return (a); }\
   else if ((r) < 0  ||  (r) >= bddnodesize)\
     { bdd_error(BDD_ILLBDD); return (a); }\
   else if (r >= 2 && LOW(r) == -1)\
     { bdd_error(BDD_ILLBDD); return (a); }

#define CHECKn(r)\
   if (!bddrunning) { bdd_error(BDD_RUNNING); return; }\
   else if ((r) < 0  ||  (r) >= bddnodesize)\
     { bdd_error(BDD_ILLBDD); return; }\
   else if (r >= 2 && LOW(r) == -1)\
     { bdd_error(BDD_ILLBDD); return; }
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
83
84
85
86
87
88

   /* r is non-constant */
#define CHECKnc(r)\
   if (root < 2) \
      return bdd_error(BDD_ILLBDD)

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
89
#endif
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
90

91
92
93
94
95
96
97
98
99
100
101
/*=== SEMI-INTERNAL TYPES ==============================================*/

typedef struct s_BddNode /* Node table entry */
{
   unsigned int refcou : 10;
   unsigned int level  : 22;
   int low;
   int high;
   int next;
} BddNode;

102
103
/* This structure is used during initialization of the above
   structure, to help gcc vectorize the initializing loop. */
104
105
106
107
108
109
110
typedef struct s_BddNodeInit
{
   int z;
   int low;
   int high;
   int next;
} BddNodeInit;
111

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
112
113
114
115
116
/*=== KERNEL VARIABLES =================================================*/

#ifdef CPLUSPLUS
extern "C" {
#endif
117

118
extern int       bddrunning;         /* Flag - package initialized */
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
119
extern int       bdderrorcond;       /* Some error condition was met */
120
extern int       bddnodesize;        /* Number of allocated nodes */
121
extern int       bddhashsize;        /* Size of node hash tableq */
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
122
123
extern int       bddmaxnodesize;     /* Maximum allowed number of nodes */
extern int       bddmaxnodeincrease; /* Max. # of nodes used to inc. table */
124
extern BddNode*  bddnodes;           /* All of the bdd nodes */
125
extern int*      bddhash;            /* Unicity hash table */
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
126
127
128
129
130
131
132
133
extern int       bddvarnum;          /* Number of defined BDD variables */
extern int*      bddrefstack;        /* Internal node reference stack */
extern int*      bddrefstacktop;     /* Internal node reference stack top */
extern int*      bddvar2level;
extern int*      bddlevel2var;
extern jmp_buf   bddexception;
extern int       bddreorderdisabled;
extern int       bddresized;
134
extern int       bddcachesize;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
135
extern bddCacheStat bddcachestats;
136

137
138
139
  /* from reorder.c */
extern int bddreordermethod;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
140
141
142
#ifdef CPLUSPLUS
}
#endif
143

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
144
145
146

/*=== KERNEL DEFINITIONS ===============================================*/

147
148
149
150
151
152
153
154
155
156
#define MAXVAR 0x1FFFFF
#define MAXREF 0x3FF

   /* Reference counting */
#define DECREF(n) if (bddnodes[n].refcou!=MAXREF && bddnodes[n].refcou>0) bddnodes[n].refcou--
#define INCREF(n) if (bddnodes[n].refcou<MAXREF) bddnodes[n].refcou++
#define DECREFp(n) if (n->refcou!=MAXREF && n->refcou>0) n->refcou--
#define INCREFp(n) if (n->refcou<MAXREF) n->refcou++
#define HASREF(n) (bddnodes[n].refcou > 0)

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
157
158
159
160
161
162
163
164
165
166
167
168
169
   /* Marking BDD nodes */
#define MARKON   0x200000    /* Bit used to mark a node (1) */
#define MARKOFF  0x1FFFFF    /* - unmark */
#define MARKHIDE 0x1FFFFF
#define SETMARK(n)  (bddnodes[n].level |= MARKON)
#define UNMARK(n)   (bddnodes[n].level &= MARKOFF)
#define MARKED(n)   (bddnodes[n].level & MARKON)
#define SETMARKp(p) (node->level |= MARKON)
#define UNMARKp(p)  (node->level &= MARKOFF)
#define MARKEDp(p)  (node->level & MARKON)

   /* Hashfunctions */

170
171
#define PAIR(a,b)     (((unsigned)a)+((unsigned)b)*12582917U)
#define TRIPLE(a,b,c) (((unsigned)a)+((unsigned)b)*12582917U+((unsigned)c)*4256249U)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
172

173
174
175
176
177
178
179
180
181
182
183
184
   /* Inspection of BDD nodes */
#define ISCONST(a) ((a) < 2)
#define ISNONCONST(a) ((a) >= 2)
#define ISONE(a)   ((a) == 1)
#define ISZERO(a)  ((a) == 0)
#define LEVEL(a)   (bddnodes[a].level)
#define LOW(a)     (bddnodes[a].low)
#define HIGH(a)    (bddnodes[a].high)
#define LEVELp(p)   ((p)->level)
#define LOWp(p)     ((p)->low)
#define HIGHp(p)    ((p)->high)

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
185
186
   /* Stacking for garbage collector */
#define INITREF    bddrefstacktop = bddrefstack
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
/*
** The following (original) definition of PUSHREF is incorrect
** when (a) can trigger a garbage collect:
**
**   #define PUSHREF(a) *(bddrefstacktop++) = (a)
**
** The reason is that bddrefstacktop can be incremented before computing
** (a) and assigning its value to bddrefstacktop[-1].  So if the garbage
** collector is triggered during the computation of (a), it will find
** uninitialized values in the stack.
**
** Such a situation occur in most algorithms of the form:
**
**   static int restrict_rec(int r) {
**     // ...
**     PUSHREF( restrict_rec(LOW(r)) );
**     PUSHREF( restrict_rec(HIGH(r)) );
**     res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
**     POPREF(2);
**
** Using a function forces the value of a to be computed before pushing
** it to the stack.
*/
static inline int PUSHREF(int a)
{
  return *bddrefstacktop++ = a;
}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
214
215
216
217
218
219
220
#define READREF(a) *(bddrefstacktop-(a))
#define POPREF(a)  bddrefstacktop -= (a)

#define BDDONE 1
#define BDDZERO 0

#ifndef CLOCKS_PER_SEC
221
222
223
224
225
226
  /* Pass `CPPFLAGS=-DDEFAULT_CLOCK=1000' as an argument to ./configure
     to override this setting.  */
# ifndef DEFAULT_CLOCK
#  define DEFAULT_CLOCK 60
# endif
# define CLOCKS_PER_SEC DEFAULT_CLOCK
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
227
228
229
230
231
232
233
234
235
236
237
238
239
240
#endif

#define DEFAULTMAXNODEINC 50000

#define MIN(a,b) ((a) < (b) ? (a) : (b))
#define MAX(a,b) ((a) > (b) ? (a) : (b))
#define NEW(t,n) ( (t*)malloc(sizeof(t)*(n)) )


/*=== KERNEL PROTOTYPES ================================================*/

#ifdef CPLUSPLUS
extern "C" {
#endif
241

242
extern int    bdd_error(int);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
extern int    bdd_makenode(unsigned int, int, int);
extern int    bdd_noderesize(int);
extern void   bdd_checkreorder(void);
extern void   bdd_mark(int);
extern void   bdd_mark_upto(int, int);
extern void   bdd_markcount(int, int*);
extern void   bdd_unmark(int);
extern void   bdd_unmark_upto(int, int);
extern void   bdd_register_pair(bddPair*);
extern int   *fdddec2bin(int, int);

extern int    bdd_operator_init(int);
extern void   bdd_operator_done(void);
extern void   bdd_operator_varresize(void);
extern void   bdd_operator_reset(void);

extern void   bdd_pairs_init(void);
extern void   bdd_pairs_done(void);
extern int    bdd_pairs_resize(int,int);
extern void   bdd_pairs_vardown(int);

extern void   bdd_fdd_init(void);
extern void   bdd_fdd_done(void);

extern void   bdd_reorder_init(void);
extern void   bdd_reorder_done(void);
Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
269
extern int    bdd_reorder_ready(void) __purefn;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
270
271
272
273
274
275
276
277
278
279
280
281
282
283
extern void   bdd_reorder_auto(void);
extern int    bdd_reorder_vardown(int);
extern int    bdd_reorder_varup(int);

extern void   bdd_cpp_init(void);

#ifdef CPLUSPLUS
}
#endif

#endif /* _KERNEL_H */


/* EOF */