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