CAL  3.0.0
An External Memory Decision Diagram Library
cal.h
1 
39 #ifndef _CAL
40 #define _CAL
41 
42 #include <stdio.h>
43 #include <stdlib.h>
44 #include <string.h>
45 #if HAVE_SYS_TYPES_H
46 # include <sys/types.h>
47 #endif
48 #if HAVE_SYS_TIME_H
49 # include <sys/time.h>
50 #endif
51 #if HAVE_SYS_RESOURCE_H
52 # include <sys/resource.h>
53 #endif
54 #if HAVE_UNISTD_H
55 # include <unistd.h>
56 #endif
57 #if HAVE_TIME_H
58 # include <time.h>
59 #endif
60 
61 #include <assert.h>
62 #include <math.h>
63 
64 #include "calMem.h"
65 
69 
74 
79 
80 #define CAL_BDD_TYPE_NONTERMINAL 0
81 #define CAL_BDD_TYPE_ZERO 1
82 #define CAL_BDD_TYPE_ONE 2
83 #define CAL_BDD_TYPE_POSVAR 3
84 #define CAL_BDD_TYPE_NEGVAR 4
85 #define CAL_BDD_TYPE_OVERFLOW 5
86 #define CAL_BDD_TYPE_CONSTANT 6
87 
88 #define CAL_BDD_UNDUMP_FORMAT 1
89 #define CAL_BDD_UNDUMP_OVERFLOW 2
90 #define CAL_BDD_UNDUMP_IOERROR 3
91 #define CAL_BDD_UNDUMP_EOF 4
92 
93 #define CAL_REORDER_NONE 0
94 #define CAL_REORDER_SIFT 1
95 #define CAL_REORDER_WINDOW 2
96 #define CAL_REORDER_METHOD_BF 0
97 #define CAL_REORDER_METHOD_DF 1
98 
101 
106 
107 typedef struct Cal_BddManagerStruct *Cal_BddManager;
108 typedef struct Cal_BddManagerStruct Cal_BddManager_t;
109 typedef struct CalBddNodeStruct *Cal_Bdd;
110 typedef unsigned short int Cal_BddId_t;
111 typedef unsigned short int Cal_BddIndex_t;
112 typedef char * (*Cal_VarNamingFn_t)(Cal_BddManager, Cal_Bdd, Cal_Pointer_t);
113 typedef char * (*Cal_TerminalIdFn_t)(Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t);
114 typedef struct Cal_BlockStruct *Cal_Block;
115 
118 
123 
124 enum Cal_BddOpEnum {CAL_AND, CAL_OR, CAL_XOR};
125 typedef enum Cal_BddOpEnum Cal_BddOp_t;
126 
129 
134 #ifndef EXTERN
135 #define EXTERN extern
136 #endif
137 
141 #define Cal_BddNamingFnNone ((char *(*)(Cal_BddManager, Cal_Bdd, Cal_Pointer_t))0)
142 
146 #define Cal_BddTerminalIdFnNone ((char *(*)(Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t))0)
147 
148 #define Cal_Assert(valid) assert(valid)
149 
152 
157 
169 EXTERN Cal_BddManager Cal_BddManagerInit();
170 
176 EXTERN int Cal_BddManagerQuit(Cal_BddManager bddManager);
177 
178 /*---------------------------------------------------------------------------*/
179 /* | Hooks and Parameters */
180 /*---------------------------------------------------------------------------*/
181 
187 EXTERN void * Cal_BddManagerGetHooks(Cal_BddManager bddManager);
188 
196 EXTERN void Cal_BddManagerSetHooks(Cal_BddManager bddManager, void *hooks);
197 
220 EXTERN void Cal_BddManagerSetParameters(Cal_BddManager bddManager,
221  long reorderingThreshold,
222  long maxForwardedNodes,
223  double repackAfterGCThreshold,
224  double tableRepackThreshold);
225 
226 /*---------------------------------------------------------------------------*/
227 /* | Statistics and Information */
228 /*---------------------------------------------------------------------------*/
229 
235 EXTERN unsigned long Cal_BddManagerGetNumNodes(Cal_BddManager bddManager);
236 
242 EXTERN unsigned long Cal_BddTotalSize(Cal_BddManager bddManager);
243 
247 EXTERN long Cal_BddVars(Cal_BddManager bddManager);
248 
256 EXTERN int Cal_BddOverflow(Cal_BddManager bddManager);
257 
261 EXTERN void Cal_BddStats(Cal_BddManager bddManager, FILE * fp);
262 
263 /*---------------------------------------------------------------------------*/
264 /* | Memory and Garbage Collection */
265 /*---------------------------------------------------------------------------*/
266 
274 EXTERN long Cal_BddNodeLimit(Cal_BddManager bddManager, long newLimit);
275 
282 EXTERN void Cal_BddSetGCMode(Cal_BddManager bddManager, int gcMode);
283 
292 EXTERN void Cal_BddManagerSetGCLimit(Cal_BddManager manager);
293 
301 EXTERN int Cal_BddManagerGC(Cal_BddManager bddManager);
302 
303 /*---------------------------------------------------------------------------*/
304 /* | Variable Reordering */
305 /*---------------------------------------------------------------------------*/
306 
312 EXTERN void Cal_BddDynamicReordering(Cal_BddManager bddManager,
313  int technique,
314  int method);
315 
323 EXTERN void Cal_BddReorder(Cal_BddManager bddManager);
324 
335 EXTERN Cal_Block Cal_BddNewVarBlock(Cal_BddManager bddManager,
336  Cal_Bdd variable,
337  long length);
338 
345 EXTERN void Cal_BddVarBlockReorderable(Cal_BddManager bddManager,
346  Cal_Block block,
347  int reorderable);
348 
349 /*---------------------------------------------------------------------------*/
350 /* | Association List */
351 /*---------------------------------------------------------------------------*/
352 
374 EXTERN int Cal_AssociationInit(Cal_BddManager bddManager,
375  Cal_Bdd *associationInfoUserBdds,
376  int pairs);
377 
386 EXTERN void Cal_AssociationQuit(Cal_BddManager bddManager, int associationId);
387 
397 EXTERN int Cal_AssociationSetCurrent(Cal_BddManager bddManager,
398  int associationId);
399 
408 EXTERN void Cal_TempAssociationInit(Cal_BddManager bddManager,
409  Cal_Bdd *associationInfoUserBdds,
410  int pairs);
411 
417 EXTERN void Cal_TempAssociationAugment(Cal_BddManager bddManager,
418  Cal_Bdd *associationInfoUserBdds,
419  int pairs);
420 
426 EXTERN void Cal_TempAssociationQuit(Cal_BddManager bddManager);
427 
428 /*---------------------------------------------------------------------------*/
429 /* | Save / Load of BDDs */
430 /*---------------------------------------------------------------------------*/
431 
442 EXTERN int Cal_BddDumpBdd(Cal_BddManager bddManager,
443  Cal_Bdd fUserBdd,
444  Cal_Bdd * userVars,
445  FILE * fp);
446 
469 EXTERN Cal_Bdd Cal_BddUndumpBdd(Cal_BddManager bddManager,
470  Cal_Bdd * userVars,
471  FILE * fp,
472  int * error);
473 
476 
481 
491 EXTERN void Cal_BddFree(Cal_BddManager bddManager, Cal_Bdd userBdd);
492 
503 EXTERN void Cal_BddUnFree(Cal_BddManager bddManager, Cal_Bdd userBdd);
504 
505 /*---------------------------------------------------------------------------*/
506 /* | Basic Constructors */
507 /*---------------------------------------------------------------------------*/
508 
512 EXTERN Cal_Bdd Cal_BddNull(Cal_BddManager bddManager);
513 
519 EXTERN Cal_Bdd Cal_BddOne(Cal_BddManager bddManager);
520 
526 EXTERN Cal_Bdd Cal_BddZero(Cal_BddManager bddManager);
527 
531 EXTERN Cal_Bdd Cal_BddManagerCreateNewVarFirst(Cal_BddManager bddManager);
532 
536 EXTERN Cal_Bdd Cal_BddManagerCreateNewVarLast(Cal_BddManager bddManager);
537 
542 EXTERN Cal_Bdd Cal_BddManagerCreateNewVarBefore(Cal_BddManager bddManager,
543  Cal_Bdd userBdd);
544 
549 EXTERN Cal_Bdd Cal_BddManagerCreateNewVarAfter(Cal_BddManager bddManager,
550  Cal_Bdd userBdd);
551 
558 EXTERN Cal_Bdd Cal_BddManagerGetVarWithIndex(Cal_BddManager bddManager,
559  Cal_BddIndex_t index);
560 
566 EXTERN Cal_Bdd Cal_BddManagerGetVarWithId(Cal_BddManager bddManager,
567  Cal_BddId_t id);
568 
569 /*---------------------------------------------------------------------------*/
570 /* | Predicates */
571 /*---------------------------------------------------------------------------*/
572 
576 EXTERN int Cal_BddIsBddNull(Cal_BddManager bddManager, Cal_Bdd userBdd);
577 
583 EXTERN int Cal_BddIsBddOne(Cal_BddManager bddManager, Cal_Bdd userBdd);
584 
590 EXTERN int Cal_BddIsBddZero(Cal_BddManager bddManager, Cal_Bdd userBdd);
591 
598 EXTERN int Cal_BddIsBddConst(Cal_BddManager bddManager, Cal_Bdd userBdd);
599 
603 EXTERN int Cal_BddIsCube(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
604 
608 EXTERN int Cal_BddIsEqual(Cal_BddManager bddManager,
609  Cal_Bdd userBdd1,
610  Cal_Bdd userBdd2);
611 
615 EXTERN int Cal_BddDependsOn(Cal_BddManager bddManager,
616  Cal_Bdd fUserBdd,
617  Cal_Bdd varUserBdd);
618 
626 EXTERN long Cal_BddSize(Cal_BddManager bddManager,
627  Cal_Bdd fUserBdd,
628  int negout);
629 
634 EXTERN long Cal_BddSizeMultiple(Cal_BddManager bddManager,
635  Cal_Bdd *fUserBddArray,
636  int negout);
637 
641 EXTERN void Cal_BddSupport(Cal_BddManager bddManager,
642  Cal_Bdd fUserBdd,
643  Cal_Bdd *support);
644 
653 EXTERN void Cal_BddProfile(Cal_BddManager bddManager,
654  Cal_Bdd fUserBdd,
655  long * levelCounts,
656  int negout);
657 
664 EXTERN void Cal_BddProfileMultiple(Cal_BddManager bddManager,
665  Cal_Bdd *fUserBddArray,
666  long * levelCounts,
667  int negout);
668 
678 EXTERN void Cal_BddFunctionProfile(Cal_BddManager bddManager,
679  Cal_Bdd fUserBdd,
680  long * funcCounts);
681 
688 EXTERN void Cal_BddFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, long * funcCounts);
689 
713 EXTERN void Cal_BddPrintBdd(Cal_BddManager bddManager,
714  Cal_Bdd fUserBdd,
715  Cal_VarNamingFn_t VarNamingFn,
716  Cal_TerminalIdFn_t TerminalIdFn,
717  Cal_Pointer_t env,
718  FILE *fp);
719 
729 EXTERN void Cal_BddPrintProfile(Cal_BddManager bddManager,
730  Cal_Bdd fUserBdd,
731  Cal_VarNamingFn_t varNamingProc,
732  char * env,
733  int lineLength,
734  FILE * fp);
735 
742 EXTERN void Cal_BddPrintProfileMultiple(Cal_BddManager bddManager,
743  Cal_Bdd *userBdds,
744  Cal_VarNamingFn_t varNamingProc,
745  char * env,
746  int lineLength,
747  FILE * fp);
748 
754 EXTERN void Cal_BddPrintFunctionProfile(Cal_BddManager bddManager,
755  Cal_Bdd f,
756  Cal_VarNamingFn_t varNamingProc,
757  char * env,
758  int lineLength,
759  FILE * fp);
760 
767 EXTERN void Cal_BddPrintFunctionProfileMultiple(Cal_BddManager bddManager,
768  Cal_Bdd *userBdds,
769  Cal_VarNamingFn_t varNamingProc,
770  char * env,
771  int lineLength,
772  FILE * fp);
773 
777 EXTERN void Cal_BddFunctionPrint(Cal_BddManager bddManager,
778  Cal_Bdd userBdd,
779  char *name);
780 
788 EXTERN Cal_Bdd Cal_BddIdentity(Cal_BddManager bddManager, Cal_Bdd userBdd);
789 
797 EXTERN Cal_Bdd Cal_BddGetRegular(Cal_BddManager bddManager, Cal_Bdd userBdd);
798 
806 EXTERN Cal_Bdd Cal_BddNot(Cal_BddManager bddManager, Cal_Bdd userBdd);
807 
811 EXTERN Cal_Bdd Cal_BddCompose(Cal_BddManager bddManager,
812  Cal_Bdd fUserBdd,
813  Cal_Bdd gUserBdd,
814  Cal_Bdd hUserBdd);
815 
823 EXTERN Cal_Bdd Cal_BddIntersects(Cal_BddManager bddManager,
824  Cal_Bdd fUserBdd,
825  Cal_Bdd gUserBdd);
826 
834 EXTERN Cal_Bdd Cal_BddImplies(Cal_BddManager bddManager,
835  Cal_Bdd fUserBdd,
836  Cal_Bdd gUserBdd);
837 
846 EXTERN Cal_Bdd Cal_BddITE(Cal_BddManager bddManager,
847  Cal_Bdd fUserBdd,
848  Cal_Bdd gUserBdd,
849  Cal_Bdd hUserBdd);
850 
854 EXTERN Cal_Bdd Cal_BddAnd(Cal_BddManager bddManager,
855  Cal_Bdd fUserBdd,
856  Cal_Bdd gUserBdd);
857 
863 EXTERN Cal_Bdd Cal_BddMultiwayAnd(Cal_BddManager bddManager,
864  Cal_Bdd *userBddArray);
865 
871 EXTERN Cal_Bdd Cal_BddNand(Cal_BddManager bddManager,
872  Cal_Bdd fUserBdd,
873  Cal_Bdd gUserBdd);
874 
878 EXTERN Cal_Bdd Cal_BddOr(Cal_BddManager bddManager,
879  Cal_Bdd fUserBdd,
880  Cal_Bdd gUserBdd);
881 
887 EXTERN Cal_Bdd Cal_BddMultiwayOr(Cal_BddManager bddManager,
888  Cal_Bdd *userBddArray);
889 
895 EXTERN Cal_Bdd Cal_BddNor(Cal_BddManager bddManager,
896  Cal_Bdd fUserBdd,
897  Cal_Bdd gUserBdd);
898 
902 EXTERN Cal_Bdd Cal_BddXor(Cal_BddManager bddManager,
903  Cal_Bdd fUserBdd,
904  Cal_Bdd gUserBdd);
905 
911 EXTERN Cal_Bdd Cal_BddMultiwayXor(Cal_BddManager bddManager,
912  Cal_Bdd *userBddArray);
913 
919 EXTERN Cal_Bdd Cal_BddXnor(Cal_BddManager bddManager,
920  Cal_Bdd fUserBdd,
921  Cal_Bdd gUserBdd);
922 
932 EXTERN Cal_Bdd * Cal_BddPairwiseAnd(Cal_BddManager bddManager,
933  Cal_Bdd *userBddArray);
934 
944 EXTERN Cal_Bdd * Cal_BddPairwiseOr(Cal_BddManager bddManager,
945  Cal_Bdd *userBddArray);
946 
956 EXTERN Cal_Bdd * Cal_BddPairwiseXor(Cal_BddManager bddManager,
957  Cal_Bdd *userBddArray);
958 
968 EXTERN Cal_Bdd Cal_BddSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
969 
982 EXTERN Cal_Bdd Cal_BddVarSubstitute(Cal_BddManager bddManager,
983  Cal_Bdd fUserBdd);
984 
993 EXTERN Cal_Bdd Cal_BddSwapVars(Cal_BddManager bddManager,
994  Cal_Bdd fUserBdd,
995  Cal_Bdd gUserBdd,
996  Cal_Bdd hUserBdd);
997 
1007 EXTERN Cal_Bdd Cal_BddExists(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
1008 
1018 EXTERN Cal_Bdd Cal_BddForAll(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
1019 
1027 EXTERN Cal_Bdd Cal_BddRelProd(Cal_BddManager bddManager,
1028  Cal_Bdd fUserBdd,
1029  Cal_Bdd gUserBdd);
1030 
1040 EXTERN Cal_Bdd Cal_BddCofactor(Cal_BddManager bddManager,
1041  Cal_Bdd fUserBdd,
1042  Cal_Bdd cUserBdd);
1043 
1054 EXTERN Cal_Bdd Cal_BddReduce(Cal_BddManager bddManager,
1055  Cal_Bdd fUserBdd,
1056  Cal_Bdd cUserBdd);
1057 
1068 EXTERN Cal_Bdd Cal_BddBetween(Cal_BddManager bddManager,
1069  Cal_Bdd fMinUserBdd,
1070  Cal_Bdd fMaxUserBdd);
1071 
1080 EXTERN Cal_Bdd Cal_BddSatisfy(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
1081 
1092 EXTERN Cal_Bdd Cal_BddSatisfySupport(Cal_BddManager bddManager,
1093  Cal_Bdd fUserBdd);
1094 
1101 EXTERN double Cal_BddSatisfyingFraction(Cal_BddManager bddManager,
1102  Cal_Bdd fUserBdd);
1103 
1104 /*---------------------------------------------------------------------------*/
1105 /* | Node Information and Traversal */
1106 /*---------------------------------------------------------------------------*/
1107 
1116 EXTERN int Cal_BddType(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
1117 
1123 EXTERN Cal_BddId_t Cal_BddGetIfIndex(Cal_BddManager bddManager,
1124  Cal_Bdd userBdd);
1125 
1131 EXTERN Cal_BddId_t Cal_BddGetIfId(Cal_BddManager bddManager, Cal_Bdd userBdd);
1132 
1138 EXTERN Cal_Bdd Cal_BddIf(Cal_BddManager bddManager, Cal_Bdd userBdd);
1139 
1146 EXTERN Cal_Bdd Cal_BddThen(Cal_BddManager bddManager, Cal_Bdd userBdd);
1147 
1154 EXTERN Cal_Bdd Cal_BddElse(Cal_BddManager bddManager, Cal_Bdd userBdd);
1155 
1158 
1163 
1171 EXTERN int Cal_PipelineInit(Cal_BddManager bddManager, Cal_BddOp_t bddOp);
1172 
1181 EXTERN void Cal_PipelineQuit(Cal_BddManager bddManager);
1182 
1189 EXTERN void Cal_PipelineSetDepth(Cal_BddManager bddManager, int depth);
1190 
1201 EXTERN int Cal_PipelineExecute(Cal_BddManager bddManager);
1202 
1209 EXTERN int Cal_BddIsProvisional(Cal_BddManager bddManager, Cal_Bdd userBdd);
1210 
1217 EXTERN Cal_Bdd Cal_PipelineCreateProvisionalBdd(Cal_BddManager bddManager,
1218  Cal_Bdd fUserBdd,
1219  Cal_Bdd gUserBdd);
1220 
1226 EXTERN Cal_Bdd Cal_PipelineUpdateProvisionalBdd(Cal_BddManager bddManager,
1227  Cal_Bdd provisionalBdd);
1228 
1231 
1234 
1235 #endif /* _CAL */
Cal_BddElse
EXTERN Cal_Bdd Cal_BddElse(Cal_BddManager bddManager, Cal_Bdd userBdd)
The negative cofactor of the argument BDD with respect to its top variable.
Cal_BddUnFree
EXTERN void Cal_BddUnFree(Cal_BddManager bddManager, Cal_Bdd userBdd)
Unfrees the argument BDD.
Cal_BddSatisfyingFraction
EXTERN double Cal_BddSatisfyingFraction(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
Fraction of valuations which make f true.
Cal_BddStats
EXTERN void Cal_BddStats(Cal_BddManager bddManager, FILE *fp)
Prints miscellaneous BDD statistics.
Cal_BddGetIfId
EXTERN Cal_BddId_t Cal_BddGetIfId(Cal_BddManager bddManager, Cal_Bdd userBdd)
Returns the id of the top variable of the argument BDD.
Cal_PipelineExecute
EXTERN int Cal_PipelineExecute(Cal_BddManager bddManager)
Executes a pipeline.
Cal_BddManagerGetVarWithIndex
EXTERN Cal_Bdd Cal_BddManagerGetVarWithIndex(Cal_BddManager bddManager, Cal_BddIndex_t index)
The variable with the specified index, null if no such variable exists.
Cal_BddPairwiseXor
EXTERN Cal_Bdd * Cal_BddPairwiseXor(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Logical XOR of BDD pairs in argument null-termiinated array of BDDs.
Cal_BddIsBddConst
EXTERN int Cal_BddIsBddConst(Cal_BddManager bddManager, Cal_Bdd userBdd)
Returns 1 if the argument BDD is either constant one or constant zero, otherwise returns 0.
Cal_BddSatisfySupport
EXTERN Cal_Bdd Cal_BddSatisfySupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
Returns a special cube contained in f.
Cal_BddManagerGC
EXTERN int Cal_BddManagerGC(Cal_BddManager bddManager)
Invokes the garbage collection at the manager level.
Cal_BddXor
EXTERN Cal_Bdd Cal_BddXor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Logical XOR of argument BDDs.
Cal_BddPairwiseAnd
EXTERN Cal_Bdd * Cal_BddPairwiseAnd(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Logical AND of BDD pairs in argument null-termiinated array of BDDs.
Cal_BddFree
EXTERN void Cal_BddFree(Cal_BddManager bddManager, Cal_Bdd userBdd)
Frees the argument BDD.
Cal_PipelineCreateProvisionalBdd
EXTERN Cal_Bdd Cal_PipelineCreateProvisionalBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Create a provisional BDD in the pipeline.
Cal_PipelineSetDepth
EXTERN void Cal_PipelineSetDepth(Cal_BddManager bddManager, int depth)
Set depth of a BDD pipeline.
Cal_BddSizeMultiple
EXTERN long Cal_BddSizeMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, int negout)
Similar to Cal_BddSize for a null-terminated array of BDDs and accounting for sharing of nodes.
Cal_BddIsEqual
EXTERN int Cal_BddIsEqual(Cal_BddManager bddManager, Cal_Bdd userBdd1, Cal_Bdd userBdd2)
Returns 1 if argument BDDs are equal, 0 otherwise.
Cal_BddCompose
EXTERN Cal_Bdd Cal_BddCompose(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd)
Substitute a BDD variable by a function.
Cal_BddIsProvisional
EXTERN int Cal_BddIsProvisional(Cal_BddManager bddManager, Cal_Bdd userBdd)
Returns 1, if the given user BDD is a provisional BDD node.
Cal_BddIdentity
EXTERN Cal_Bdd Cal_BddIdentity(Cal_BddManager bddManager, Cal_Bdd userBdd)
Duplicate of the argument BDD.
Cal_BddPrintFunctionProfileMultiple
EXTERN void Cal_BddPrintFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *userBdds, Cal_VarNamingFn_t varNamingProc, char *env, int lineLength, FILE *fp)
Similar to Cal_BddPrintFunctionProfile but displays a function profile for a set of BDDs.
Cal_TempAssociationQuit
EXTERN void Cal_TempAssociationQuit(Cal_BddManager bddManager)
Cleans up temporary association.
Cal_BddFunctionProfile
EXTERN void Cal_BddFunctionProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd, long *funcCounts)
The number of subfunctions of f which may be obtained by restricting variables with an index lower th...
Cal_AssociationInit
EXTERN int Cal_AssociationInit(Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs)
Creates or finds a variable association.
Cal_BddMultiwayXor
EXTERN Cal_Bdd Cal_BddMultiwayXor(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Logical XOR of BDDs in argument null-terminated array of BDDs.
Cal_BddPrintBdd
EXTERN void Cal_BddPrintBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_VarNamingFn_t VarNamingFn, Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env, FILE *fp)
Prints a BDD in the human readable form.
Cal_BddCofactor
EXTERN Cal_Bdd Cal_BddCofactor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd cUserBdd)
Generalized cofactor of f with respect to c.
Cal_BddProfileMultiple
EXTERN void Cal_BddProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, long *levelCounts, int negout)
Similar to Cal_BddProfile for a null-terminated array of BDDs and accounting for sharing of nodes.
Cal_BddMultiwayAnd
EXTERN Cal_Bdd Cal_BddMultiwayAnd(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Logical AND of BDDs in argument null-terminated array of BDDs.
Cal_BddVarBlockReorderable
EXTERN void Cal_BddVarBlockReorderable(Cal_BddManager bddManager, Cal_Block block, int reorderable)
Sets the reoderability of a particular block.
Cal_BddVarSubstitute
EXTERN Cal_Bdd Cal_BddVarSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
Substitute a set of variables by set of another variables.
Cal_BddSubstitute
EXTERN Cal_Bdd Cal_BddSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
Substitute a set of variables by functions.
Cal_BddDynamicReordering
EXTERN void Cal_BddDynamicReordering(Cal_BddManager bddManager, int technique, int method)
Specify dynamic reordering technique and method.
Cal_BddNodeLimit
EXTERN long Cal_BddNodeLimit(Cal_BddManager bddManager, long newLimit)
Sets the node limit to new_limit and returns the old limit.
Cal_BddManagerCreateNewVarLast
EXTERN Cal_Bdd Cal_BddManagerCreateNewVarLast(Cal_BddManager bddManager)
Create and obtain a new variable at the end of the variable order.
Cal_BddPrintFunctionProfile
EXTERN void Cal_BddPrintFunctionProfile(Cal_BddManager bddManager, Cal_Bdd f, Cal_VarNamingFn_t varNamingProc, char *env, int lineLength, FILE *fp)
Similar to Cal_BddPrintProfile but displays a function profile for f.
Cal_BddManagerGetVarWithId
EXTERN Cal_Bdd Cal_BddManagerGetVarWithId(Cal_BddManager bddManager, Cal_BddId_t id)
The variable with the specified id, null if no such variable exists.
Cal_TempAssociationInit
EXTERN void Cal_TempAssociationInit(Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs)
Sets the temporary variable association.
Cal_BddFunctionPrint
EXTERN void Cal_BddFunctionPrint(Cal_BddManager bddManager, Cal_Bdd userBdd, char *name)
Prints the function implemented by the argument BDD.
Cal_BddManagerCreateNewVarAfter
EXTERN Cal_Bdd Cal_BddManagerCreateNewVarAfter(Cal_BddManager bddManager, Cal_Bdd userBdd)
Create and obtain a new variable after the specified one in the variable order.
Cal_BddNand
EXTERN Cal_Bdd Cal_BddNand(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Logical NAND of argument BDDs.
Cal_BddOne
EXTERN Cal_Bdd Cal_BddOne(Cal_BddManager bddManager)
The BDD for the constant one.
Cal_BddDumpBdd
EXTERN int Cal_BddDumpBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd *userVars, FILE *fp)
Write a BDD to a file.
Cal_BddManagerSetGCLimit
EXTERN void Cal_BddManagerSetGCLimit(Cal_BddManager manager)
Sets the limit of the garbage collection.
Cal_BddUndumpBdd
EXTERN Cal_Bdd Cal_BddUndumpBdd(Cal_BddManager bddManager, Cal_Bdd *userVars, FILE *fp, int *error)
Reads a BDD from a file.
Cal_BddGetIfIndex
EXTERN Cal_BddId_t Cal_BddGetIfIndex(Cal_BddManager bddManager, Cal_Bdd userBdd)
Returns the index of the top variable of the argument BDD.
Cal_BddExists
EXTERN Cal_Bdd Cal_BddExists(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
Existentially quantification of some variables from the given BDD.
Cal_BddNot
EXTERN Cal_Bdd Cal_BddNot(Cal_BddManager bddManager, Cal_Bdd userBdd)
Complement of the argument BDD.
Cal_BddIsBddOne
EXTERN int Cal_BddIsBddOne(Cal_BddManager bddManager, Cal_Bdd userBdd)
Returns 1 if the argument BDD is constant one, 0 otherwise.
Cal_BddIntersects
EXTERN Cal_Bdd Cal_BddIntersects(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Computes a BDD that implies conjunction of f and g.
Cal_BddProfile
EXTERN void Cal_BddProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd, long *levelCounts, int negout)
The number of nodes at each level in f.
Cal_BddOverflow
EXTERN int Cal_BddOverflow(Cal_BddManager bddManager)
Returns 1 if the node limit has been exceeded, 0 otherwise.
Cal_BddPrintProfile
EXTERN void Cal_BddPrintProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_VarNamingFn_t varNamingProc, char *env, int lineLength, FILE *fp)
Displays the node profile for f on fp.
Cal_BddTotalSize
EXTERN unsigned long Cal_BddTotalSize(Cal_BddManager bddManager)
Returns the number of nodes in the Unique table.
Cal_BddManagerCreateNewVarBefore
EXTERN Cal_Bdd Cal_BddManagerCreateNewVarBefore(Cal_BddManager bddManager, Cal_Bdd userBdd)
Create and obtain a new variable before the specified one in the variable order.
Cal_BddSize
EXTERN long Cal_BddSize(Cal_BddManager bddManager, Cal_Bdd fUserBdd, int negout)
BDD size of fUserBdd.
Cal_BddPrintProfileMultiple
EXTERN void Cal_BddPrintProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *userBdds, Cal_VarNamingFn_t varNamingProc, char *env, int lineLength, FILE *fp)
Similar to Cal_BddPrintProfile but displays the profile for a set of BDDs.
Cal_BddPairwiseOr
EXTERN Cal_Bdd * Cal_BddPairwiseOr(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Logical OR of BDD pairs in argument null-termiinated array of BDDs.
Cal_PipelineInit
EXTERN int Cal_PipelineInit(Cal_BddManager bddManager, Cal_BddOp_t bddOp)
Initialize a BDD pipeline.
Cal_BddIf
EXTERN Cal_Bdd Cal_BddIf(Cal_BddManager bddManager, Cal_Bdd userBdd)
A BDD corresponding to the top variable of the given BDD.
Cal_BddZero
EXTERN Cal_Bdd Cal_BddZero(Cal_BddManager bddManager)
The BDD for the constant zero.
Cal_BddManagerGetNumNodes
EXTERN unsigned long Cal_BddManagerGetNumNodes(Cal_BddManager bddManager)
Returns the number of BDD nodes.
Cal_BddManagerCreateNewVarFirst
EXTERN Cal_Bdd Cal_BddManagerCreateNewVarFirst(Cal_BddManager bddManager)
Create and obtain a new variable at the start of the variable order.
Cal_BddNewVarBlock
EXTERN Cal_Block Cal_BddNewVarBlock(Cal_BddManager bddManager, Cal_Bdd variable, long length)
Creates and returns a variable block used for controlling dynamic reordering.
Cal_BddReduce
EXTERN Cal_Bdd Cal_BddReduce(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd cUserBdd)
A function that agrees with f for all valuations which satisfy c.
Cal_BddManagerInit
EXTERN Cal_BddManager Cal_BddManagerInit()
Creates and initializes a new BDD manager.
Cal_BddSatisfy
EXTERN Cal_Bdd Cal_BddSatisfy(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
A satisfying assignment of f.
Cal_AssociationQuit
EXTERN void Cal_AssociationQuit(Cal_BddManager bddManager, int associationId)
Deletes the variable association given by id.
Cal_BddBetween
EXTERN Cal_Bdd Cal_BddBetween(Cal_BddManager bddManager, Cal_Bdd fMinUserBdd, Cal_Bdd fMaxUserBdd)
A function that contains fMin and is contained in fMax.
Cal_BddType
EXTERN int Cal_BddType(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
The type of the given BDD (0, 1, +var, -var, overflow, nonterminal).
Cal_BddGetRegular
EXTERN Cal_Bdd Cal_BddGetRegular(Cal_BddManager bddManager, Cal_Bdd userBdd)
Returns a BDD with positive from a given BDD with arbitrary phase.
Cal_AssociationSetCurrent
EXTERN int Cal_AssociationSetCurrent(Cal_BddManager bddManager, int associationId)
Sets the current variable association to the one given.
Cal_PipelineUpdateProvisionalBdd
EXTERN Cal_Bdd Cal_PipelineUpdateProvisionalBdd(Cal_BddManager bddManager, Cal_Bdd provisionalBdd)
Update a provisional BDD obtained during pipelining.
Cal_BddVars
EXTERN long Cal_BddVars(Cal_BddManager bddManager)
Returns the number of BDD variables.
Cal_BddSupport
EXTERN void Cal_BddSupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd *support)
Returns the support of f as a null-terminated array of variables.
Cal_BddXnor
EXTERN Cal_Bdd Cal_BddXnor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Logical XNOR of argument BDDs.
Cal_BddSetGCMode
EXTERN void Cal_BddSetGCMode(Cal_BddManager bddManager, int gcMode)
Sets the garbage collection mode.
Cal_BddFunctionProfileMultiple
EXTERN void Cal_BddFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, long *funcCounts)
Similar to Cal_BddFunctionProfile for a null-terminated array of BDDs and accounting for sharing of n...
Cal_BddITE
EXTERN Cal_Bdd Cal_BddITE(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd)
Logical If-Then-Else.
Cal_BddReorder
EXTERN void Cal_BddReorder(Cal_BddManager bddManager)
Invoke the current dynamic reodering method.
Cal_BddIsBddZero
EXTERN int Cal_BddIsBddZero(Cal_BddManager bddManager, Cal_Bdd userBdd)
Returns 1 if the argument BDD is constant zero, 0 otherwise.
Cal_BddRelProd
EXTERN Cal_Bdd Cal_BddRelProd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Logical AND of the argument BDDs and existentially quantifying some variables from the product.
Cal_BddThen
EXTERN Cal_Bdd Cal_BddThen(Cal_BddManager bddManager, Cal_Bdd userBdd)
The positive cofactor of the argument BDD with respect to its top variable.
Cal_BddDependsOn
EXTERN int Cal_BddDependsOn(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd varUserBdd)
Returns 1 if f depends on var and returns 0 otherwise.
Cal_BddIsCube
EXTERN int Cal_BddIsCube(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
Returns 1 if the argument BDD is a cube, 0 otherwise.
Cal_BddManagerGetHooks
EXTERN void * Cal_BddManagerGetHooks(Cal_BddManager bddManager)
Returns the hooks field of the manager.
Cal_PipelineQuit
EXTERN void Cal_PipelineQuit(Cal_BddManager bddManager)
Resets the pipeline freeing all resources.
Cal_BddManagerQuit
EXTERN int Cal_BddManagerQuit(Cal_BddManager bddManager)
Frees the BDD manager and all the associated allocations.
Cal_TempAssociationAugment
EXTERN void Cal_TempAssociationAugment(Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs)
Adds to the temporary variable association.
Cal_BddForAll
EXTERN Cal_Bdd Cal_BddForAll(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
Universal quantification of some variables from the given BDD.
Cal_BddNor
EXTERN Cal_Bdd Cal_BddNor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Logical NOR of argument BDDs.
Cal_BddImplies
EXTERN Cal_Bdd Cal_BddImplies(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Computes a BDD that implies conjunction of f and Cal_BddNot(g).
Cal_BddOr
EXTERN Cal_Bdd Cal_BddOr(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Logical Or of argument BDDs.
Cal_BddMultiwayOr
EXTERN Cal_Bdd Cal_BddMultiwayOr(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Logical OR of BDDs in argument null-terminated array of BDDs.
Cal_BddNull
EXTERN Cal_Bdd Cal_BddNull(Cal_BddManager bddManager)
Returns the NULL BDD.
Cal_BddIsBddNull
EXTERN int Cal_BddIsBddNull(Cal_BddManager bddManager, Cal_Bdd userBdd)
1 if the argument BDD is NULL, 0 otherwise.
Cal_BddSwapVars
EXTERN Cal_Bdd Cal_BddSwapVars(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd)
The function obtained by swapping two variables.
Cal_BddAnd
EXTERN Cal_Bdd Cal_BddAnd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Logical AND of argument BDDs.
Cal_BddManagerSetHooks
EXTERN void Cal_BddManagerSetHooks(Cal_BddManager bddManager, void *hooks)
Sets the hooks field of the manager.
Cal_BddManagerSetParameters
EXTERN void Cal_BddManagerSetParameters(Cal_BddManager bddManager, long reorderingThreshold, long maxForwardedNodes, double repackAfterGCThreshold, double tableRepackThreshold)
Sets appropriate fields of BDD Manager.