605dce2aac
examples/Makefile.am, examples/Makefile.def, examples/adder/Makefile.am, examples/calculator/Makefile.am, examples/cmilner/Makefile.am, examples/fdd/Makefile.am, examples/internal/Makefile.am, examples/milner/Makefile.am, examples/money/Makefile.am, examples/queen/Makefile.am, examples/solitar/Makefile.am, m4/debug.m4, m4/gccwarns.m4, ChangeLog, INSTALL: New files. * config, makefile, src/makefile, doc/makefile, examples/adder/makefile, examples/calculator/makefile examples/cmilner/makefile, examples/fdd/makefile, examples/internal/makefile, examples/milner/makefile, examples/money/makefile, examples/queen/makefile, examples/solitare/makefile : Delete. * examples/adder/adder.cxx, examples/fdd/statespace.cxx, examples/internal/bddtest.cxx, examples/milner/milner.cxx, examples/money/money.cxx, examples/queen/queen.cxx, examples/solitare/solitare.cxx: Include iostream. * examples/calculator/parser.y: Rename as ... * examples/calculator/parser.yxx: ... this. Remove spurious comas in %token, %right, and %left arguments. * examples/calculator/parser.h: Rename as ... * examples/calculator/parser_.h: ... this, because the bison rule with output parser.h (not tokens.h) from parser.y. * examples/calculator/lexer.l: Rename as ... * examples/calculator/lexer.lxx: ... this. Include parser.h instead of tokens.h. * examples/calculator/slist.h (voidSList::voisSListElem, SList::ite): Fix friend usage. * src/kernel.h (DEFAULT_CLOCK): Default to 60 if not already defined. * README: Update build instruction, and file listing.
232 lines
7.8 KiB
C
232 lines
7.8 KiB
C
/*========================================================================
|
|
Copyright (C) 1996-2002 by Jorn Lind-Nielsen
|
|
All rights reserved
|
|
|
|
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.
|
|
========================================================================*/
|
|
|
|
/*************************************************************************
|
|
$Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.h,v 1.2 2003/05/05 13:45:07 aduret Exp $
|
|
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>
|
|
#include "bdd.h"
|
|
|
|
/*=== 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
|
|
|
|
|
|
/* 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; }
|
|
|
|
|
|
/*=== SEMI-INTERNAL TYPES ==============================================*/
|
|
|
|
typedef struct s_BddNode /* Node table entry */
|
|
{
|
|
unsigned int refcou : 10;
|
|
unsigned int level : 22;
|
|
int low;
|
|
int high;
|
|
int hash;
|
|
int next;
|
|
} BddNode;
|
|
|
|
|
|
/*=== KERNEL VARIABLES =================================================*/
|
|
|
|
#ifdef CPLUSPLUS
|
|
extern "C" {
|
|
#endif
|
|
|
|
extern int bddrunning; /* Flag - package initialized */
|
|
extern int bdderrorcond; /* Some error condition was met */
|
|
extern int bddnodesize; /* Number of allocated nodes */
|
|
extern int bddmaxnodesize; /* Maximum allowed number of nodes */
|
|
extern int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */
|
|
extern BddNode* bddnodes; /* All of the bdd nodes */
|
|
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;
|
|
extern bddCacheStat bddcachestats;
|
|
|
|
#ifdef CPLUSPLUS
|
|
}
|
|
#endif
|
|
|
|
|
|
/*=== KERNEL DEFINITIONS ===============================================*/
|
|
|
|
#define VERSION 22
|
|
|
|
#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)
|
|
|
|
/* 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 */
|
|
|
|
#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)))
|
|
#define TRIPLE(a,b,c) ((unsigned int)(PAIR((unsigned int)c,PAIR(a,b))))
|
|
|
|
|
|
/* 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)
|
|
|
|
/* Stacking for garbage collector */
|
|
#define INITREF bddrefstacktop = bddrefstack
|
|
#define PUSHREF(a) *(bddrefstacktop++) = (a)
|
|
#define READREF(a) *(bddrefstacktop-(a))
|
|
#define POPREF(a) bddrefstacktop -= (a)
|
|
|
|
#define BDDONE 1
|
|
#define BDDZERO 0
|
|
|
|
#ifndef CLOCKS_PER_SEC
|
|
/* 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
|
|
#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
|
|
|
|
extern int bdd_error(int);
|
|
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);
|
|
extern int bdd_reorder_ready(void);
|
|
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 */
|