source: vis_dev/glu-2.3/src/calBdd/cal.h @ 77

Last change on this file since 77 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 14.4 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [cal.h]
4
5  PackageName [cal]
6
7  Synopsis    [Header CAL file for exported data structures and functions.]
8
9  Description []
10
11  SeeAlso     [optional]
12
13  Author      [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu)
14               Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu)]
15
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35  Revision    [$Id: cal.h,v 1.8 2002/09/08 21:22:16 fabio Exp $]
36
37******************************************************************************/
38
39#ifndef _CAL
40#define _CAL
41#include <stdio.h>
42#include <stdlib.h>
43#include <string.h>
44#if HAVE_SYS_TYPES_H
45#  include <sys/types.h>
46#endif
47#if HAVE_SYS_TIME_H
48#  include <sys/time.h>
49#endif
50#if HAVE_SYS_RESOURCE_H
51#  include <sys/resource.h>
52#endif
53#if HAVE_UNISTD_H
54#  include <unistd.h>
55#endif
56#if HAVE_TIME_H
57#  include <time.h>
58#endif
59
60#include <assert.h>
61#include <math.h>
62
63#include "calMem.h"
64/*---------------------------------------------------------------------------*/
65/* Constant declarations                                                     */
66/*---------------------------------------------------------------------------*/
67
68#ifndef EXTERN
69#  ifdef __cplusplus
70#    define EXTERN      extern "C"
71#  else
72#    define EXTERN      extern
73#  endif
74#endif
75
76#define CAL_BDD_TYPE_NONTERMINAL 0
77#define CAL_BDD_TYPE_ZERO 1
78#define CAL_BDD_TYPE_ONE 2
79#define CAL_BDD_TYPE_POSVAR 3
80#define CAL_BDD_TYPE_NEGVAR 4
81#define CAL_BDD_TYPE_OVERFLOW 5
82#define CAL_BDD_TYPE_CONSTANT 6
83
84#define CAL_BDD_UNDUMP_FORMAT 1
85#define CAL_BDD_UNDUMP_OVERFLOW 2
86#define CAL_BDD_UNDUMP_IOERROR 3
87#define CAL_BDD_UNDUMP_EOF 4
88
89#define CAL_REORDER_NONE 0
90#define CAL_REORDER_SIFT 1
91#define CAL_REORDER_WINDOW 2
92#define CAL_REORDER_METHOD_BF 0
93#define CAL_REORDER_METHOD_DF 1
94
95/*---------------------------------------------------------------------------*/
96/* Type declarations                                                         */
97/*---------------------------------------------------------------------------*/
98typedef struct Cal_BddManagerStruct *Cal_BddManager;
99typedef struct Cal_BddManagerStruct Cal_BddManager_t;
100typedef struct CalBddNodeStruct *Cal_Bdd;
101typedef unsigned short int Cal_BddId_t;
102typedef unsigned short int Cal_BddIndex_t;
103typedef char * (*Cal_VarNamingFn_t)(Cal_BddManager, Cal_Bdd, Cal_Pointer_t); 
104typedef char * (*Cal_TerminalIdFn_t)(Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t);     
105typedef struct Cal_BlockStruct *Cal_Block;
106
107/*---------------------------------------------------------------------------*/
108/* Stucture declarations                                                     */
109/*---------------------------------------------------------------------------*/
110enum Cal_BddOpEnum {CAL_AND, CAL_OR, CAL_XOR};
111typedef enum Cal_BddOpEnum Cal_BddOp_t;
112
113
114/*---------------------------------------------------------------------------*/
115/* Variable declarations                                                     */
116/*---------------------------------------------------------------------------*/
117
118/*---------------------------------------------------------------------------*/
119/* Macro declarations                                                        */
120/*---------------------------------------------------------------------------*/
121#define Cal_BddNamingFnNone ((char *(*)(Cal_BddManager, Cal_Bdd, Cal_Pointer_t))0)
122#define Cal_BddTerminalIdFnNone ((char *(*)(Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t))0)
123#ifdef _CAL_DEBUG_
124#define Cal_Assert(valid) assert(valid)
125#else
126#define Cal_Assert(ignore) ((void)0)
127#endif
128
129
130
131/**AutomaticStart*************************************************************/
132
133/*---------------------------------------------------------------------------*/
134/* Function prototypes                                                       */
135/*---------------------------------------------------------------------------*/
136
137EXTERN int Cal_BddIsEqual(Cal_BddManager bddManager, Cal_Bdd userBdd1, Cal_Bdd userBdd2);
138EXTERN int Cal_BddIsBddOne(Cal_BddManager bddManager, Cal_Bdd userBdd);
139EXTERN int Cal_BddIsBddZero(Cal_BddManager bddManager, Cal_Bdd userBdd);
140EXTERN int Cal_BddIsBddNull(Cal_BddManager bddManager, Cal_Bdd userBdd);
141EXTERN int Cal_BddIsBddConst(Cal_BddManager bddManager, Cal_Bdd userBdd);
142EXTERN Cal_Bdd Cal_BddIdentity(Cal_BddManager bddManager, Cal_Bdd userBdd);
143EXTERN Cal_Bdd Cal_BddOne(Cal_BddManager bddManager);
144EXTERN Cal_Bdd Cal_BddZero(Cal_BddManager bddManager);
145EXTERN Cal_Bdd Cal_BddNot(Cal_BddManager bddManager, Cal_Bdd userBdd);
146EXTERN Cal_BddId_t Cal_BddGetIfIndex(Cal_BddManager bddManager, Cal_Bdd userBdd);
147EXTERN Cal_BddId_t Cal_BddGetIfId(Cal_BddManager bddManager, Cal_Bdd userBdd);
148EXTERN Cal_Bdd Cal_BddIf(Cal_BddManager bddManager, Cal_Bdd userBdd);
149EXTERN Cal_Bdd Cal_BddThen(Cal_BddManager bddManager, Cal_Bdd userBdd);
150EXTERN Cal_Bdd Cal_BddElse(Cal_BddManager bddManager, Cal_Bdd userBdd);
151EXTERN void Cal_BddFree(Cal_BddManager bddManager, Cal_Bdd userBdd);
152EXTERN void Cal_BddUnFree(Cal_BddManager bddManager, Cal_Bdd userBdd);
153EXTERN Cal_Bdd Cal_BddGetRegular(Cal_BddManager bddManager, Cal_Bdd userBdd);
154EXTERN Cal_Bdd Cal_BddIntersects(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
155EXTERN Cal_Bdd Cal_BddImplies(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
156EXTERN unsigned long Cal_BddTotalSize(Cal_BddManager bddManager);
157EXTERN void Cal_BddStats(Cal_BddManager bddManager, FILE * fp);
158EXTERN void Cal_BddDynamicReordering(Cal_BddManager bddManager, int technique);
159EXTERN void Cal_BddReorder(Cal_BddManager bddManager);
160EXTERN int Cal_BddType(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
161EXTERN long Cal_BddVars(Cal_BddManager bddManager);
162EXTERN long Cal_BddNodeLimit(Cal_BddManager bddManager, long newLimit);
163EXTERN int Cal_BddOverflow(Cal_BddManager bddManager);
164EXTERN int Cal_BddIsCube(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
165EXTERN void * Cal_BddManagerGetHooks(Cal_BddManager bddManager);
166EXTERN void Cal_BddManagerSetHooks(Cal_BddManager bddManager, void *hooks);
167EXTERN int Cal_AssociationInit(Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs);
168EXTERN void Cal_AssociationQuit(Cal_BddManager bddManager, int associationId);
169EXTERN int Cal_AssociationSetCurrent(Cal_BddManager bddManager, int associationId);
170EXTERN void Cal_TempAssociationAugment(Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs);
171EXTERN void Cal_TempAssociationInit(Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs);
172EXTERN void Cal_TempAssociationQuit(Cal_BddManager bddManager);
173EXTERN Cal_Bdd Cal_BddCompose(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd);
174EXTERN Cal_Bdd Cal_BddITE(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd);
175EXTERN Cal_BddManager Cal_BddManagerInit(void);
176EXTERN int Cal_BddManagerQuit(Cal_BddManager bddManager);
177EXTERN void Cal_BddManagerSetParameters(Cal_BddManager bddManager, long reorderingThreshold, long maxForwardedNodes, double repackAfterGCThreshold, double tableRepackThreshold);
178EXTERN unsigned long Cal_BddManagerGetNumNodes(Cal_BddManager bddManager);
179EXTERN Cal_Bdd Cal_BddManagerCreateNewVarFirst(Cal_BddManager bddManager);
180EXTERN Cal_Bdd Cal_BddManagerCreateNewVarLast(Cal_BddManager bddManager);
181EXTERN Cal_Bdd Cal_BddManagerCreateNewVarBefore(Cal_BddManager bddManager, Cal_Bdd userBdd);
182EXTERN Cal_Bdd Cal_BddManagerCreateNewVarAfter(Cal_BddManager bddManager, Cal_Bdd userBdd);
183EXTERN Cal_Bdd Cal_BddManagerGetVarWithIndex(Cal_BddManager bddManager, Cal_BddIndex_t index);
184EXTERN Cal_Bdd Cal_BddManagerGetVarWithId(Cal_BddManager bddManager, Cal_BddId_t id);
185EXTERN Cal_Bdd Cal_BddAnd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
186EXTERN Cal_Bdd Cal_BddNand(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
187EXTERN Cal_Bdd Cal_BddOr(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
188EXTERN Cal_Bdd Cal_BddNor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
189EXTERN Cal_Bdd Cal_BddXor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
190EXTERN Cal_Bdd Cal_BddXnor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
191EXTERN Cal_Bdd * Cal_BddPairwiseAnd(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
192EXTERN Cal_Bdd * Cal_BddPairwiseOr(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
193EXTERN Cal_Bdd * Cal_BddPairwiseXor(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
194EXTERN Cal_Bdd Cal_BddMultiwayAnd(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
195EXTERN Cal_Bdd Cal_BddMultiwayOr(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
196EXTERN Cal_Bdd Cal_BddMultiwayXor(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
197EXTERN Cal_Bdd Cal_BddSatisfy(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
198EXTERN Cal_Bdd Cal_BddSatisfySupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
199EXTERN double Cal_BddSatisfyingFraction(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
200EXTERN long Cal_BddSize(Cal_BddManager bddManager, Cal_Bdd fUserBdd, int negout);
201EXTERN long Cal_BddSizeMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, int negout);
202EXTERN void Cal_BddProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd, long * levelCounts, int negout);
203EXTERN void Cal_BddProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, long * levelCounts, int negout);
204EXTERN void Cal_BddFunctionProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd, long * funcCounts);
205EXTERN void Cal_BddFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, long * funcCounts);
206EXTERN Cal_Bdd Cal_BddSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
207EXTERN void Cal_BddSupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd *support);
208EXTERN int Cal_BddDependsOn(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd varUserBdd);
209EXTERN Cal_Bdd Cal_BddSwapVars(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd);
210EXTERN Cal_Bdd Cal_BddVarSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
211EXTERN Cal_Block Cal_BddNewVarBlock(Cal_BddManager bddManager, Cal_Bdd variable, long length);
212EXTERN void Cal_BddVarBlockReorderable(Cal_BddManager bddManager, Cal_Block block, int reorderable);
213EXTERN Cal_Bdd Cal_BddUndumpBdd(Cal_BddManager bddManager, Cal_Bdd * userVars, FILE * fp, int * error);
214EXTERN int Cal_BddDumpBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd * userVars, FILE * fp);
215EXTERN void Cal_BddSetGCMode(Cal_BddManager bddManager, int gcMode);
216EXTERN int Cal_BddManagerGC(Cal_BddManager bddManager);
217EXTERN void Cal_BddManagerSetGCLimit(Cal_BddManager manager);
218EXTERN void Cal_MemFatal(char *message);
219EXTERN Cal_Address_t Cal_MemAllocation(void);
220EXTERN Cal_Pointer_t Cal_MemGetBlock(Cal_Address_t size);
221EXTERN void Cal_MemFreeBlock(Cal_Pointer_t p);
222EXTERN Cal_Pointer_t Cal_MemResizeBlock(Cal_Pointer_t p, Cal_Address_t newSize);
223EXTERN Cal_Pointer_t Cal_MemNewRec(Cal_RecMgr mgr);
224EXTERN void Cal_MemFreeRec(Cal_RecMgr mgr, Cal_Pointer_t rec);
225EXTERN Cal_RecMgr Cal_MemNewRecMgr(int size);
226EXTERN void Cal_MemFreeRecMgr(Cal_RecMgr mgr);
227EXTERN int Cal_PerformanceTest(Cal_BddManager bddManager, Cal_Bdd *outputBddArray, int numFunctions, int iteration, int seed, int andPerformanceFlag, int multiwayPerformanceFlag, int onewayPerformanceFlag, int quantifyPerformanceFlag, int composePerformanceFlag, int relprodPerformanceFlag, int swapPerformanceFlag, int substitutePerformanceFlag, int sanityCheckFlag, int computeMemoryOverheadFlag, int superscalarFlag);
228EXTERN void Cal_PipelineSetDepth(Cal_BddManager bddManager, int depth);
229EXTERN int Cal_PipelineInit(Cal_BddManager bddManager, Cal_BddOp_t bddOp);
230EXTERN Cal_Bdd Cal_PipelineCreateProvisionalBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
231EXTERN int Cal_PipelineExecute(Cal_BddManager bddManager);
232EXTERN Cal_Bdd Cal_PipelineUpdateProvisionalBdd(Cal_BddManager bddManager, Cal_Bdd provisionalBdd);
233EXTERN int Cal_BddIsProvisional(Cal_BddManager bddManager, Cal_Bdd userBdd);
234EXTERN void Cal_PipelineQuit(Cal_BddManager bddManager);
235EXTERN void Cal_BddPrintBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_VarNamingFn_t VarNamingFn, Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env, FILE *fp);
236EXTERN void Cal_BddPrintProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_VarNamingFn_t varNamingProc, char * env, int lineLength, FILE * fp);
237EXTERN void Cal_BddPrintProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *userBdds, Cal_VarNamingFn_t varNamingProc, char * env, int lineLength, FILE * fp);
238EXTERN void Cal_BddPrintFunctionProfile(Cal_BddManager bddManager, Cal_Bdd f, Cal_VarNamingFn_t varNamingProc, char * env, int lineLength, FILE * fp);
239EXTERN void Cal_BddPrintFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *userBdds, Cal_VarNamingFn_t varNamingProc, char * env, int lineLength, FILE * fp);
240EXTERN Cal_Bdd Cal_BddExists(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
241EXTERN Cal_Bdd Cal_BddRelProd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
242EXTERN Cal_Bdd Cal_BddForAll(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
243EXTERN Cal_Bdd Cal_BddCofactor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd cUserBdd);
244EXTERN Cal_Bdd Cal_BddReduce(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd cUserBdd);
245EXTERN Cal_Bdd Cal_BddBetween(Cal_BddManager bddManager, Cal_Bdd fMinUserBdd, Cal_Bdd fMaxUserBdd);
246EXTERN void Cal_ImageDump(Cal_BddManager_t *bddManager, FILE *fp);
247EXTERN void Cal_BddFunctionPrint(Cal_BddManager bddManager, Cal_Bdd userBdd, char *name);
248
249/**AutomaticEnd***************************************************************/
250
251#endif /* _CAL */
Note: See TracBrowser for help on using the repository browser.