CAL 3.0.0
An External Memory Decision Diagram Library
Loading...
Searching...
No Matches
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
107typedef struct Cal_BddManagerStruct *Cal_BddManager;
108typedef struct Cal_BddManagerStruct Cal_BddManager_t;
109typedef struct CalBddNodeStruct *Cal_Bdd;
110typedef unsigned short int Cal_BddId_t;
111typedef unsigned short int Cal_BddIndex_t;
112typedef char * (*Cal_VarNamingFn_t)(Cal_BddManager, Cal_Bdd, Cal_Pointer_t);
113typedef char * (*Cal_TerminalIdFn_t)(Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t);
114typedef struct Cal_BlockStruct *Cal_Block;
115
118
123
124enum Cal_BddOpEnum {CAL_AND, CAL_OR, CAL_XOR};
125typedef 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
169EXTERN Cal_BddManager Cal_BddManagerInit();
170
176EXTERN int Cal_BddManagerQuit(Cal_BddManager bddManager);
177
178/*---------------------------------------------------------------------------*/
179/* | Hooks and Parameters */
180/*---------------------------------------------------------------------------*/
181
187EXTERN void * Cal_BddManagerGetHooks(Cal_BddManager bddManager);
188
196EXTERN void Cal_BddManagerSetHooks(Cal_BddManager bddManager, void *hooks);
197
220EXTERN 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
235EXTERN unsigned long Cal_BddManagerGetNumNodes(Cal_BddManager bddManager);
236
242EXTERN unsigned long Cal_BddTotalSize(Cal_BddManager bddManager);
243
247EXTERN long Cal_BddVars(Cal_BddManager bddManager);
248
256EXTERN int Cal_BddOverflow(Cal_BddManager bddManager);
257
261EXTERN void Cal_BddStats(Cal_BddManager bddManager, FILE * fp);
262
263/*---------------------------------------------------------------------------*/
264/* | Memory and Garbage Collection */
265/*---------------------------------------------------------------------------*/
266
274EXTERN long Cal_BddNodeLimit(Cal_BddManager bddManager, long newLimit);
275
282EXTERN void Cal_BddSetGCMode(Cal_BddManager bddManager, int gcMode);
283
292EXTERN void Cal_BddManagerSetGCLimit(Cal_BddManager manager);
293
301EXTERN int Cal_BddManagerGC(Cal_BddManager bddManager);
302
303/*---------------------------------------------------------------------------*/
304/* | Variable Reordering */
305/*---------------------------------------------------------------------------*/
306
312EXTERN void Cal_BddDynamicReordering(Cal_BddManager bddManager,
313 int technique,
314 int method);
315
323EXTERN void Cal_BddReorder(Cal_BddManager bddManager);
324
335EXTERN Cal_Block Cal_BddNewVarBlock(Cal_BddManager bddManager,
336 Cal_Bdd variable,
337 long length);
338
345EXTERN void Cal_BddVarBlockReorderable(Cal_BddManager bddManager,
346 Cal_Block block,
347 int reorderable);
348
349/*---------------------------------------------------------------------------*/
350/* | Association List */
351/*---------------------------------------------------------------------------*/
352
374EXTERN int Cal_AssociationInit(Cal_BddManager bddManager,
375 Cal_Bdd *associationInfoUserBdds,
376 int pairs);
377
386EXTERN void Cal_AssociationQuit(Cal_BddManager bddManager, int associationId);
387
397EXTERN int Cal_AssociationSetCurrent(Cal_BddManager bddManager,
398 int associationId);
399
408EXTERN void Cal_TempAssociationInit(Cal_BddManager bddManager,
409 Cal_Bdd *associationInfoUserBdds,
410 int pairs);
411
417EXTERN void Cal_TempAssociationAugment(Cal_BddManager bddManager,
418 Cal_Bdd *associationInfoUserBdds,
419 int pairs);
420
426EXTERN void Cal_TempAssociationQuit(Cal_BddManager bddManager);
427
428/*---------------------------------------------------------------------------*/
429/* | Save / Load of BDDs */
430/*---------------------------------------------------------------------------*/
431
442EXTERN int Cal_BddDumpBdd(Cal_BddManager bddManager,
443 Cal_Bdd fUserBdd,
444 Cal_Bdd * userVars,
445 FILE * fp);
446
469EXTERN Cal_Bdd Cal_BddUndumpBdd(Cal_BddManager bddManager,
470 Cal_Bdd * userVars,
471 FILE * fp,
472 int * error);
473
476
481
491EXTERN void Cal_BddFree(Cal_BddManager bddManager, Cal_Bdd userBdd);
492
503EXTERN void Cal_BddUnFree(Cal_BddManager bddManager, Cal_Bdd userBdd);
504
505/*---------------------------------------------------------------------------*/
506/* | Basic Constructors */
507/*---------------------------------------------------------------------------*/
508
512EXTERN Cal_Bdd Cal_BddNull(Cal_BddManager bddManager);
513
519EXTERN Cal_Bdd Cal_BddOne(Cal_BddManager bddManager);
520
526EXTERN Cal_Bdd Cal_BddZero(Cal_BddManager bddManager);
527
531EXTERN Cal_Bdd Cal_BddManagerCreateNewVarFirst(Cal_BddManager bddManager);
532
536EXTERN Cal_Bdd Cal_BddManagerCreateNewVarLast(Cal_BddManager bddManager);
537
542EXTERN Cal_Bdd Cal_BddManagerCreateNewVarBefore(Cal_BddManager bddManager,
543 Cal_Bdd userBdd);
544
549EXTERN Cal_Bdd Cal_BddManagerCreateNewVarAfter(Cal_BddManager bddManager,
550 Cal_Bdd userBdd);
551
558EXTERN Cal_Bdd Cal_BddManagerGetVarWithIndex(Cal_BddManager bddManager,
559 Cal_BddIndex_t index);
560
566EXTERN Cal_Bdd Cal_BddManagerGetVarWithId(Cal_BddManager bddManager,
567 Cal_BddId_t id);
568
569/*---------------------------------------------------------------------------*/
570/* | Predicates */
571/*---------------------------------------------------------------------------*/
572
576EXTERN int Cal_BddIsBddNull(Cal_BddManager bddManager, Cal_Bdd userBdd);
577
583EXTERN int Cal_BddIsBddOne(Cal_BddManager bddManager, Cal_Bdd userBdd);
584
590EXTERN int Cal_BddIsBddZero(Cal_BddManager bddManager, Cal_Bdd userBdd);
591
598EXTERN int Cal_BddIsBddConst(Cal_BddManager bddManager, Cal_Bdd userBdd);
599
603EXTERN int Cal_BddIsCube(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
604
608EXTERN int Cal_BddIsEqual(Cal_BddManager bddManager,
609 Cal_Bdd userBdd1,
610 Cal_Bdd userBdd2);
611
615EXTERN int Cal_BddDependsOn(Cal_BddManager bddManager,
616 Cal_Bdd fUserBdd,
617 Cal_Bdd varUserBdd);
618
626EXTERN long Cal_BddSize(Cal_BddManager bddManager,
627 Cal_Bdd fUserBdd,
628 int negout);
629
634EXTERN long Cal_BddSizeMultiple(Cal_BddManager bddManager,
635 Cal_Bdd *fUserBddArray,
636 int negout);
637
641EXTERN void Cal_BddSupport(Cal_BddManager bddManager,
642 Cal_Bdd fUserBdd,
643 Cal_Bdd *support);
644
653EXTERN void Cal_BddProfile(Cal_BddManager bddManager,
654 Cal_Bdd fUserBdd,
655 long * levelCounts,
656 int negout);
657
664EXTERN void Cal_BddProfileMultiple(Cal_BddManager bddManager,
665 Cal_Bdd *fUserBddArray,
666 long * levelCounts,
667 int negout);
668
678EXTERN void Cal_BddFunctionProfile(Cal_BddManager bddManager,
679 Cal_Bdd fUserBdd,
680 long * funcCounts);
681
688EXTERN void Cal_BddFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, long * funcCounts);
689
713EXTERN 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
729EXTERN 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
742EXTERN 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
754EXTERN 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
767EXTERN 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
777EXTERN void Cal_BddFunctionPrint(Cal_BddManager bddManager,
778 Cal_Bdd userBdd,
779 char *name);
780
788EXTERN Cal_Bdd Cal_BddIdentity(Cal_BddManager bddManager, Cal_Bdd userBdd);
789
797EXTERN Cal_Bdd Cal_BddGetRegular(Cal_BddManager bddManager, Cal_Bdd userBdd);
798
806EXTERN Cal_Bdd Cal_BddNot(Cal_BddManager bddManager, Cal_Bdd userBdd);
807
811EXTERN Cal_Bdd Cal_BddCompose(Cal_BddManager bddManager,
812 Cal_Bdd fUserBdd,
813 Cal_Bdd gUserBdd,
814 Cal_Bdd hUserBdd);
815
823EXTERN Cal_Bdd Cal_BddIntersects(Cal_BddManager bddManager,
824 Cal_Bdd fUserBdd,
825 Cal_Bdd gUserBdd);
826
834EXTERN Cal_Bdd Cal_BddImplies(Cal_BddManager bddManager,
835 Cal_Bdd fUserBdd,
836 Cal_Bdd gUserBdd);
837
846EXTERN Cal_Bdd Cal_BddITE(Cal_BddManager bddManager,
847 Cal_Bdd fUserBdd,
848 Cal_Bdd gUserBdd,
849 Cal_Bdd hUserBdd);
850
854EXTERN Cal_Bdd Cal_BddAnd(Cal_BddManager bddManager,
855 Cal_Bdd fUserBdd,
856 Cal_Bdd gUserBdd);
857
863EXTERN Cal_Bdd Cal_BddMultiwayAnd(Cal_BddManager bddManager,
864 Cal_Bdd *userBddArray);
865
871EXTERN Cal_Bdd Cal_BddNand(Cal_BddManager bddManager,
872 Cal_Bdd fUserBdd,
873 Cal_Bdd gUserBdd);
874
878EXTERN Cal_Bdd Cal_BddOr(Cal_BddManager bddManager,
879 Cal_Bdd fUserBdd,
880 Cal_Bdd gUserBdd);
881
887EXTERN Cal_Bdd Cal_BddMultiwayOr(Cal_BddManager bddManager,
888 Cal_Bdd *userBddArray);
889
895EXTERN Cal_Bdd Cal_BddNor(Cal_BddManager bddManager,
896 Cal_Bdd fUserBdd,
897 Cal_Bdd gUserBdd);
898
902EXTERN Cal_Bdd Cal_BddXor(Cal_BddManager bddManager,
903 Cal_Bdd fUserBdd,
904 Cal_Bdd gUserBdd);
905
911EXTERN Cal_Bdd Cal_BddMultiwayXor(Cal_BddManager bddManager,
912 Cal_Bdd *userBddArray);
913
919EXTERN Cal_Bdd Cal_BddXnor(Cal_BddManager bddManager,
920 Cal_Bdd fUserBdd,
921 Cal_Bdd gUserBdd);
922
932EXTERN Cal_Bdd * Cal_BddPairwiseAnd(Cal_BddManager bddManager,
933 Cal_Bdd *userBddArray);
934
944EXTERN Cal_Bdd * Cal_BddPairwiseOr(Cal_BddManager bddManager,
945 Cal_Bdd *userBddArray);
946
956EXTERN Cal_Bdd * Cal_BddPairwiseXor(Cal_BddManager bddManager,
957 Cal_Bdd *userBddArray);
958
968EXTERN Cal_Bdd Cal_BddSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
969
982EXTERN Cal_Bdd Cal_BddVarSubstitute(Cal_BddManager bddManager,
983 Cal_Bdd fUserBdd);
984
993EXTERN Cal_Bdd Cal_BddSwapVars(Cal_BddManager bddManager,
994 Cal_Bdd fUserBdd,
995 Cal_Bdd gUserBdd,
996 Cal_Bdd hUserBdd);
997
1007EXTERN Cal_Bdd Cal_BddExists(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
1008
1018EXTERN Cal_Bdd Cal_BddForAll(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
1019
1027EXTERN Cal_Bdd Cal_BddRelProd(Cal_BddManager bddManager,
1028 Cal_Bdd fUserBdd,
1029 Cal_Bdd gUserBdd);
1030
1040EXTERN Cal_Bdd Cal_BddCofactor(Cal_BddManager bddManager,
1041 Cal_Bdd fUserBdd,
1042 Cal_Bdd cUserBdd);
1043
1054EXTERN Cal_Bdd Cal_BddReduce(Cal_BddManager bddManager,
1055 Cal_Bdd fUserBdd,
1056 Cal_Bdd cUserBdd);
1057
1068EXTERN Cal_Bdd Cal_BddBetween(Cal_BddManager bddManager,
1069 Cal_Bdd fMinUserBdd,
1070 Cal_Bdd fMaxUserBdd);
1071
1080EXTERN Cal_Bdd Cal_BddSatisfy(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
1081
1092EXTERN Cal_Bdd Cal_BddSatisfySupport(Cal_BddManager bddManager,
1093 Cal_Bdd fUserBdd);
1094
1101EXTERN double Cal_BddSatisfyingFraction(Cal_BddManager bddManager,
1102 Cal_Bdd fUserBdd);
1103
1104/*---------------------------------------------------------------------------*/
1105/* | Node Information and Traversal */
1106/*---------------------------------------------------------------------------*/
1107
1116EXTERN int Cal_BddType(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
1117
1123EXTERN Cal_BddId_t Cal_BddGetIfIndex(Cal_BddManager bddManager,
1124 Cal_Bdd userBdd);
1125
1131EXTERN Cal_BddId_t Cal_BddGetIfId(Cal_BddManager bddManager, Cal_Bdd userBdd);
1132
1138EXTERN Cal_Bdd Cal_BddIf(Cal_BddManager bddManager, Cal_Bdd userBdd);
1139
1146EXTERN Cal_Bdd Cal_BddThen(Cal_BddManager bddManager, Cal_Bdd userBdd);
1147
1154EXTERN Cal_Bdd Cal_BddElse(Cal_BddManager bddManager, Cal_Bdd userBdd);
1155
1158
1163
1171EXTERN int Cal_PipelineInit(Cal_BddManager bddManager, Cal_BddOp_t bddOp);
1172
1181EXTERN void Cal_PipelineQuit(Cal_BddManager bddManager);
1182
1189EXTERN void Cal_PipelineSetDepth(Cal_BddManager bddManager, int depth);
1190
1201EXTERN int Cal_PipelineExecute(Cal_BddManager bddManager);
1202
1209EXTERN int Cal_BddIsProvisional(Cal_BddManager bddManager, Cal_Bdd userBdd);
1210
1217EXTERN Cal_Bdd Cal_PipelineCreateProvisionalBdd(Cal_BddManager bddManager,
1218 Cal_Bdd fUserBdd,
1219 Cal_Bdd gUserBdd);
1220
1226EXTERN 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_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_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_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_BddFree
EXTERN void Cal_BddFree(Cal_BddManager bddManager, Cal_Bdd userBdd)
Frees the argument BDD.
Cal_BddManagerGetHooks
EXTERN void * Cal_BddManagerGetHooks(Cal_BddManager bddManager)
Returns the hooks field of the manager.
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_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_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_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_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_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_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.