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:  kernel.h
33  DESCR: Kernel specific definitions for BDD package
34  AUTH:  Jorn Lind
35  DATE:  (C) june 1997
36*************************************************************************/
37
38#ifndef _KERNEL_H
39#define _KERNEL_H
40
41/*=== Includes =========================================================*/
42
43#include <limits.h>
44#include <setjmp.h>
45#include "bdd.h"
46
47/*=== SANITY CHECKS ====================================================*/
48
49   /* Make sure we use at least 32 bit integers */
50#if (INT_MAX < 0x7FFFFFFF)
51#error The compiler does not support 4 byte integers!
52#endif
53
54
55   /* Sanity check argument and return eventual error code */
56#define CHECK(r)\
57   if (!bddrunning) return bdd_error(BDD_RUNNING);\
58   else if ((r) < 0  ||  (r) >= bddnodesize) return bdd_error(BDD_ILLBDD);\
59   else if (r >= 2 && LOW(r) == -1) return bdd_error(BDD_ILLBDD)\
60
61   /* Sanity check argument and return eventually the argument 'a' */
62#define CHECKa(r,a)\
63   if (!bddrunning) { bdd_error(BDD_RUNNING); return (a); }\
64   else if ((r) < 0  ||  (r) >= bddnodesize)\
65     { bdd_error(BDD_ILLBDD); return (a); }\
66   else if (r >= 2 && LOW(r) == -1)\
67     { bdd_error(BDD_ILLBDD); return (a); }
68
69#define CHECKn(r)\
70   if (!bddrunning) { bdd_error(BDD_RUNNING); return; }\
71   else if ((r) < 0  ||  (r) >= bddnodesize)\
72     { bdd_error(BDD_ILLBDD); return; }\
73   else if (r >= 2 && LOW(r) == -1)\
74     { bdd_error(BDD_ILLBDD); return; }
75
76
77/*=== SEMI-INTERNAL TYPES ==============================================*/
78
79typedef struct s_BddNode /* Node table entry */
80{
81   unsigned int refcou : 10;
82   unsigned int level  : 22;
83   int low;
84   int high;
85   int hash;
86   int next;
87} BddNode;
88
89
90/*=== KERNEL VARIABLES =================================================*/
91
92#ifdef CPLUSPLUS
93extern "C" {
94#endif
95
96extern int       bddrunning;         /* Flag - package initialized */
97extern int       bdderrorcond;       /* Some error condition was met */
98extern int       bddnodesize;        /* Number of allocated nodes */
99extern int       bddmaxnodesize;     /* Maximum allowed number of nodes */
100extern int       bddmaxnodeincrease; /* Max. # of nodes used to inc. table */
101extern BddNode*  bddnodes;           /* All of the bdd nodes */
102extern int       bddvarnum;          /* Number of defined BDD variables */
103extern int*      bddrefstack;        /* Internal node reference stack */
104extern int*      bddrefstacktop;     /* Internal node reference stack top */
105extern int*      bddvar2level;
106extern int*      bddlevel2var;
107extern jmp_buf   bddexception;
108extern int       bddreorderdisabled;
109extern int       bddresized;
110extern bddCacheStat bddcachestats;
111
112#ifdef CPLUSPLUS
113}
114#endif
115
116
117/*=== KERNEL DEFINITIONS ===============================================*/
118
119#define VERSION 20
120
121#define MAXVAR 0x1FFFFF
122#define MAXREF 0x3FF
123
124   /* Reference counting */
125#define DECREF(n) if (bddnodes[n].refcou<MAXREF) bddnodes[n].refcou--
126#define INCREF(n) if (bddnodes[n].refcou<MAXREF) bddnodes[n].refcou++
127#define DECREFp(n) if (n->refcou<MAXREF) n->refcou--
128#define INCREFp(n) if (n->refcou<MAXREF) n->refcou++
129#define HASREF(n) (bddnodes[n].refcou > 0)
130
131   /* Marking BDD nodes */
132#define MARKON   0x200000    /* Bit used to mark a node (1) */
133#define MARKOFF  0x1FFFFF    /* - unmark */
134#define MARKHIDE 0x1FFFFF
135#define SETMARK(n)  (bddnodes[n].level |= MARKON)
136#define UNMARK(n)   (bddnodes[n].level &= MARKOFF)
137#define MARKED(n)   (bddnodes[n].level & MARKON)
138#define SETMARKp(p) (node->level |= MARKON)
139#define UNMARKp(p)  (node->level &= MARKOFF)
140#define MARKEDp(p)  (node->level & MARKON)
141
142   /* Hashfunctions */
143
144#define PAIR(a,b)      ((unsigned int)((((unsigned int)a)+((unsigned int)b))*(((unsigned int)a)+((unsigned int)b)+((unsigned int)1))/((unsigned int)2)+((unsigned int)a)))
145#define TRIPLE(a,b,c)  ((unsigned int)(PAIR((unsigned int)c,PAIR(a,b))))
146
147
148   /* Inspection of BDD nodes */
149#define ISCONST(a) ((a) < 2)
150#define ISNONCONST(a) ((a) >= 2)
151#define ISONE(a)   ((a) == 1)
152#define ISZERO(a)  ((a) == 0)
153#define LEVEL(a)   (bddnodes[a].level)
154#define LOW(a)     (bddnodes[a].low)
155#define HIGH(a)    (bddnodes[a].high)
156#define LEVELp(p)   ((p)->level)
157#define LOWp(p)     ((p)->low)
158#define HIGHp(p)    ((p)->high)
159
160   /* Stacking for garbage collector */
161#define INITREF    bddrefstacktop = bddrefstack
162#define PUSHREF(a) *(bddrefstacktop++) = (a)
163#define READREF(a) *(bddrefstacktop-(a))
164#define POPREF(a)  bddrefstacktop -= (a)
165
166#define BDDONE 1
167#define BDDZERO 0
168
169#ifndef CLOCKS_PER_SEC
170#define CLOCKS_PER_SEC DEFAULT_CLOCK
171#endif
172
173#define DEFAULTMAXNODEINC 50000
174
175#define MIN(a,b) ((a) < (b) ? (a) : (b))
176#define MAX(a,b) ((a) > (b) ? (a) : (b))
177#define NEW(t,n) ( (t*)malloc(sizeof(t)*(n)) )
178
179
180/*=== KERNEL PROTOTYPES ================================================*/
181
182#ifdef CPLUSPLUS
183extern "C" {
184#endif
185
186extern int    bdd_error(int);
187extern int    bdd_makenode(unsigned int, int, int);
188extern int    bdd_noderesize(int);
189extern void   bdd_checkreorder(void);
190extern void   bdd_mark(int);
191extern void   bdd_mark_upto(int, int);
192extern void   bdd_markcount(int, int*);
193extern void   bdd_unmark(int);
194extern void   bdd_unmark_upto(int, int);
195extern void   bdd_register_pair(bddPair*);
196extern int   *fdddec2bin(int, int);
197
198extern int    bdd_operator_init(int);
199extern void   bdd_operator_done(void);
200extern void   bdd_operator_varresize(void);
201extern void   bdd_operator_reset(void);
202
203extern void   bdd_pairs_init(void);
204extern void   bdd_pairs_done(void);
205extern int    bdd_pairs_resize(int,int);
206extern void   bdd_pairs_vardown(int);
207
208extern void   bdd_fdd_init(void);
209extern void   bdd_fdd_done(void);
210
211extern void   bdd_reorder_init(void);
212extern void   bdd_reorder_done(void);
213extern int    bdd_reorder_ready(void);
214extern void   bdd_reorder_auto(void);
215extern int    bdd_reorder_vardown(int);
216extern int    bdd_reorder_varup(int);
217
218extern void   bdd_cpp_init(void);
219
220#ifdef CPLUSPLUS
221}
222#endif
223
224#endif /* _KERNEL_H */
225
226
227/* EOF */
228