src/cuPort/cuPort.c File Reference
#include "cuPortInt.h"
Go to the source code of this file.
Function Documentation
| bdd_node* bdd_add_apply | ( | bdd_manager * | mgr, | |
| bdd_node *(*)(bdd_manager *, bdd_node **, bdd_node **) | operation, | |||
| bdd_node * | fn1, | |||
| bdd_node * | fn2 | |||
| ) |
Function********************************************************************
Synopsis [Performs the apply operation on ADds]
SideEffects []
| bdd_node* bdd_add_apply_recur | ( | bdd_manager * | mgr, | |
| bdd_node *(*)(bdd_manager *, bdd_node **, bdd_node **) | operation, | |||
| bdd_node * | fn1, | |||
| bdd_node * | fn2 | |||
| ) |
Function********************************************************************
Synopsis [Implements the recursive call of bdd_add_apply.]
Description [Implements the recursive call of bdd_add_apply. This should be used only in recursive procedures where the order of the variables needs to remain constant during the entire operation of the procedure. Returns a pointer to the result if successful. NULL is returned if reordering takes place or if memory is exhausted.]
SideEffects []
| bdd_node* bdd_add_bdd_strict_threshold | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| BDD_VALUE_TYPE | value | |||
| ) |
Function********************************************************************
Synopsis [Converts an ADD to a BDD by replacing all discriminants strictly greater than value with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.]
SideEffects []
Definition at line 4626 of file cuPort.c.
04630 { 04631 DdNode *result; 04632 result = Cudd_addBddStrictThreshold((DdManager *) mgr, (DdNode *) f, 04633 (CUDD_VALUE_TYPE)value); 04634 04635 return(result); 04636 04637 } /* end of bdd_add_bdd_strict_threshold */
| bdd_node* bdd_add_bdd_threshold | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| BDD_VALUE_TYPE | value | |||
| ) |
Function********************************************************************
Synopsis [Converts an ADD to a BDD by replacing all discriminants greater than or equal to value with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.]
SideEffects []
Definition at line 4602 of file cuPort.c.
04606 { 04607 DdNode *result; 04608 result = Cudd_addBddThreshold((DdManager *) mgr, (DdNode *) f, 04609 (CUDD_VALUE_TYPE)value); 04610 04611 return(result); 04612 04613 } /* end of bdd_add_bdd_threshold */
| bdd_node* bdd_add_cmpl | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
Function********************************************************************
Synopsis [Computes the complement of an ADD a la C language.]
SideEffects []
| bdd_node* bdd_add_compose | ( | bdd_manager * | mgr, | |
| bdd_node * | fn1, | |||
| bdd_node * | fn2, | |||
| int | var | |||
| ) |
Function********************************************************************
Synopsis [Performs compose operation on ADds]
SideEffects []
| bdd_node* bdd_add_compute_cube | ( | bdd_manager * | mgr, | |
| bdd_node ** | vars, | |||
| int * | phase, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [Computes the cube of an array of ADD variables. If non-null, the phase argument indicates which literal of each variable should appear in the cube. If phase\[i\] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects []
| bdd_node* bdd_add_const | ( | bdd_manager * | mgr, | |
| BDD_VALUE_TYPE | c | |||
| ) |
Function********************************************************************
Synopsis [Returns the ADD for constant c.]
Description [Returns the ADD for constant c if successful. NULL otherwise.]
SideEffects []
Definition at line 4537 of file cuPort.c.
04538 { 04539 DdNode *result; 04540 result = Cudd_addConst((DdManager *)mgr, (CUDD_VALUE_TYPE)c); 04541 04542 return(result); 04543 04544 } /* end of bdd_add_const */
| bdd_node* bdd_add_divide | ( | bdd_manager * | mgr, | |
| bdd_node ** | fn1, | |||
| bdd_node ** | fn2 | |||
| ) |
Function********************************************************************
Synopsis [Performs the divide operation on ADDs]
SideEffects []
| bdd_node* bdd_add_exist_abstract | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node * | vars | |||
| ) |
Function********************************************************************
Synopsis [Existentially abstracts out the variables from the function]
SideEffects []
| bdd_node* bdd_add_find_max | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
Function********************************************************************
Synopsis [Finds the maximum discriminant of f. Returns a pointer to a constant ADD.]
SideEffects []
Definition at line 4336 of file cuPort.c.
04337 { 04338 DdNode *result; 04339 result = Cudd_addFindMax((DdManager *)mgr, (DdNode *)f); 04340 04341 return(result); 04342 04343 } /* end of bdd_add_find_max */
| bdd_node* bdd_add_general_vector_compose | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | vectorOn, | |||
| bdd_node ** | vectorOff | |||
| ) |
Function********************************************************************
Synopsis [Composes an ADD with a vector of ADDs.]
SideEffects []
| bdd_node* bdd_add_hamming | ( | bdd_manager * | mgr, | |
| bdd_node ** | xVars, | |||
| bdd_node ** | yVars, | |||
| int | nVars | |||
| ) |
Function********************************************************************
Synopsis [Computes the hamming distance ADD between two sets of variables.]
SideEffects []
| int bdd_add_hook | ( | bdd_manager * | mgr, | |
| int(*)(bdd_manager *, char *, void *) | procedure, | |||
| bdd_hook_type_t | whichHook | |||
| ) |
Function********************************************************************
Synopsis [Adds a function to a hook.]
SideEffects []
Definition at line 3183 of file cuPort.c.
03187 { 03188 int retval; 03189 Cudd_HookType hook; 03190 switch (whichHook) { 03191 case BDD_PRE_GC_HOOK: hook = CUDD_PRE_GC_HOOK; break; 03192 case BDD_POST_GC_HOOK: hook = CUDD_POST_GC_HOOK; break; 03193 case BDD_PRE_REORDERING_HOOK: hook = CUDD_PRE_REORDERING_HOOK; break; 03194 case BDD_POST_REORDERING_HOOK: hook = CUDD_POST_REORDERING_HOOK; break; 03195 default: fprintf(stderr, "Dont know which hook"); return 0; 03196 } 03197 03198 retval = Cudd_AddHook((DdManager *)mgr, (DD_HFP)procedure, hook); 03199 return retval; 03200 03201 } /* end of bdd_add_hook */
| bdd_node* bdd_add_ite | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g, | |||
| bdd_node * | h | |||
| ) |
Function********************************************************************
Synopsis [Performs the ITE operation for ADDs.]
SideEffects []
| bdd_node* bdd_add_ith_var | ( | bdd_manager * | mgr, | |
| int | i | |||
| ) |
Function********************************************************************
Synopsis [Gets the ith add variable in the manager ]
SideEffects []
Definition at line 4120 of file cuPort.c.
04121 { 04122 DdNode *result; 04123 result = Cudd_addIthVar((DdManager *)mgr, i); 04124 return(result); 04125 04126 } /* end of bdd_add_ith_var */
| bdd_node* bdd_add_matrix_multiply | ( | bdd_manager * | mgr, | |
| bdd_node * | A, | |||
| bdd_node * | B, | |||
| bdd_node ** | z, | |||
| int | nz | |||
| ) |
Function********************************************************************
Synopsis [Multiply two matrices represented by A and B. A is assumed to depend on x (rows) and z (columns). B is assumed to depend on z (rows) and y (columns). The product depends on x and y. Only z needs to be explicitly identified.]
SideEffects []
| bdd_node* bdd_add_minus | ( | bdd_manager * | mgr, | |
| bdd_node ** | fn1, | |||
| bdd_node ** | fn2 | |||
| ) |
Function********************************************************************
Synopsis [Integer and floating point subtraction.Returns NULL if not a terminal case; f-g otherwise.]
SideEffects []
| bdd_node* bdd_add_nonsim_compose | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node ** | vector | |||
| ) |
Function********************************************************************
Synopsis [Performs the non-simple compose on ADds]
SideEffects []
| bdd_node* bdd_add_permute | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| int * | permut | |||
| ) |
Function********************************************************************
Synopsis [Permutes the variables in a given function using the permut array..]
SideEffects []
Definition at line 3814 of file cuPort.c.
03818 { 03819 DdNode *result; 03820 result = Cudd_addPermute((DdManager *)mgr, (DdNode *)fn, permut); 03821 return(result); 03822 03823 } /* end of bdd_add_permute */
| bdd_node* bdd_add_plus | ( | bdd_manager * | mgr, | |
| bdd_node ** | fn1, | |||
| bdd_node ** | fn2 | |||
| ) |
Function********************************************************************
Synopsis [Integer and floating point addition.Returns NULL if not a terminal case; f+g otherwise.]
SideEffects []
| bdd_node* bdd_add_residue | ( | bdd_manager * | mgr, | |
| int | n, | |||
| int | m, | |||
| int | options, | |||
| int | top | |||
| ) |
Function********************************************************************
Synopsis [Computes the residue ADD of n variables with respect to m]
SideEffects []
Definition at line 3952 of file cuPort.c.
03958 { 03959 DdNode *result; 03960 result = Cudd_addResidue((DdManager *)mgr, n, m, options, top); 03961 return(result); 03962 03963 } /* end of bdd_add_residue */
| bdd_node* bdd_add_roundoff | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| int | N | |||
| ) |
Function********************************************************************
Synopsis [Rounds off the discriminants of an ADD.]
SideEffects []
| bdd_node* bdd_add_swap_variables | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [Swap two sets of variables in ADD f]
SideEffects []
| bdd_node* bdd_add_times | ( | bdd_manager * | mgr, | |
| bdd_node ** | fn1, | |||
| bdd_node ** | fn2 | |||
| ) |
Function********************************************************************
Synopsis [Performs the times (multiplication operation) on Adds]
SideEffects []
| BDD_VALUE_TYPE bdd_add_value | ( | bdd_node * | f | ) |
Function********************************************************************
Synopsis [Returns the value of the ADD node.]
Description [Returns the value of the ADD node.]
SideEffects []
| bdd_node* bdd_add_vector_compose | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node ** | vector | |||
| ) |
Function********************************************************************
Synopsis [Performs the vector compose on ADds]
SideEffects []
| bdd_node* bdd_add_xnor | ( | bdd_manager * | mgr, | |
| bdd_node ** | fn1, | |||
| bdd_node ** | fn2 | |||
| ) |
Function********************************************************************
Synopsis [Performs the xnor ( operation) on Adds]
SideEffects []
Function********************************************************************
Synopsis [And of two BDDs.]
SideEffects []
Definition at line 325 of file cuPort.c.
00330 { 00331 DdManager *dd; 00332 DdNode *newf, *newg, *fandg; 00333 00334 /* Make sure both BDDs belong to the same manager. */ 00335 assert(f->mgr == g->mgr); 00336 00337 /* Modify the phases of the operands according to the parameters. */ 00338 newf = Cudd_NotCond(f->node,!f_phase); 00339 newg = Cudd_NotCond(g->node,!g_phase); 00340 00341 /* Perform the AND operation. */ 00342 dd = f->mgr; 00343 fandg = Cudd_bddAnd(f->mgr,newf,newg); 00344 if (fandg == NULL) return(NULL); 00345 cuddRef(fandg); 00346 00347 return(bdd_construct_bdd_t(dd,fandg)); 00348 00349 } /* end of bdd_and */
Function********************************************************************
Synopsis [And of a BDD and an array of BDDs.]
SideEffects []
Definition at line 400 of file cuPort.c.
00405 { 00406 bdd_t *g; 00407 DdNode *result, *temp; 00408 int i; 00409 DdNode *newf, *newg; 00410 00411 /* Modify the phases of the operands according to the parameters. */ 00412 newf = Cudd_NotCond(f->node,!f_phase); 00413 00414 Cudd_Ref(result = newf); 00415 00416 for (i = 0; i < array_n(g_array); i++) { 00417 g = array_fetch(bdd_t *, g_array, i); 00418 00419 /* Modify the phases of the operands according to the parameters. */ 00420 newg = Cudd_NotCond(g->node,!g_phase); 00421 00422 temp = Cudd_bddAnd(f->mgr, result, newg); 00423 if (temp == NULL) { 00424 Cudd_RecursiveDeref(f->mgr, result); 00425 return(NULL); 00426 } 00427 cuddRef(temp); 00428 Cudd_RecursiveDeref(f->mgr, result); 00429 result = temp; 00430 } 00431 00432 return(bdd_construct_bdd_t(f->mgr,result)); 00433 00434 } /* end of bdd_and_array */
Function********************************************************************
Synopsis [Abstracts variables from the product of two BDDs.]
SideEffects []
Definition at line 708 of file cuPort.c.
00712 { 00713 int i; 00714 bdd_t *variable; 00715 DdNode *cube, *tmpDd, *result; 00716 DdManager *mgr; 00717 00718 /* Make sure both operands belong to the same manager. */ 00719 assert(f->mgr == g->mgr); 00720 00721 /* CUDD needs the smoothing variables passed as a cube. 00722 * Therefore we must build that cube from the indices of variables 00723 * in the array before calling the procedure. 00724 */ 00725 mgr = f->mgr; 00726 Cudd_Ref(cube = DD_ONE(mgr)); 00727 for (i = 0; i < array_n(smoothing_vars); i++) { 00728 variable = array_fetch(bdd_t *,smoothing_vars,i); 00729 00730 /* Make sure the variable belongs to the same manager. */ 00731 assert(mgr == variable->mgr); 00732 00733 tmpDd = Cudd_bddAnd(mgr,cube,variable->node); 00734 if (tmpDd == NULL) { 00735 Cudd_RecursiveDeref(mgr,cube); 00736 return(NULL); 00737 } 00738 cuddRef(tmpDd); 00739 Cudd_RecursiveDeref(mgr, cube); 00740 cube = tmpDd; 00741 } 00742 00743 /* Perform the smoothing */ 00744 result = Cudd_bddAndAbstract(mgr,f->node,g->node,cube); 00745 if (result == NULL) { 00746 Cudd_RecursiveDeref(mgr, cube); 00747 return(NULL); 00748 } 00749 cuddRef(result); 00750 /* Get rid of temporary results. */ 00751 Cudd_RecursiveDeref(mgr, cube); 00752 00753 /* Build the bdd_t structure for the result */ 00754 return(bdd_construct_bdd_t(mgr,result)); 00755 00756 } /* end of bdd_and_smooth */
Function********************************************************************
Synopsis [Abstracts variables from the product of two BDDs.]
SideEffects []
Definition at line 832 of file cuPort.c.
00833 { 00834 DdNode *result; 00835 DdManager *mgr; 00836 00837 /* Make sure both operands belong to the same manager. */ 00838 assert(f->mgr == g->mgr); 00839 00840 /* The Boulder package needs the smothing variables passed as a cube. 00841 * Therefore we must build that cube from the indices of variables 00842 * in the array before calling the procedure. 00843 */ 00844 mgr = f->mgr; 00845 00846 /* Perform the smoothing */ 00847 result = Cudd_bddAndAbstract(mgr,f->node,g->node,cube->node); 00848 if (result == NULL) 00849 return(NULL); 00850 cuddRef(result); 00851 00852 /* Build the bdd_t structure for the result */ 00853 return(bdd_construct_bdd_t(mgr,result)); 00854 00855 } /* end of bdd_and_smooth_with_cube */
| bdd_t* bdd_and_smooth_with_limit | ( | bdd_t * | f, | |
| bdd_t * | g, | |||
| array_t * | smoothing_vars, | |||
| unsigned int | limit | |||
| ) |
Function********************************************************************
Synopsis [Abstracts variables from the product of two BDDs with limit on new nodes.]
Description [If more new nodes than specified by limit must be created, this function returns NULL. The caller must be prepared for this occurrence.]
SideEffects []
Definition at line 772 of file cuPort.c.
00777 { 00778 int i; 00779 bdd_t *variable; 00780 DdNode *cube, *tmpDd, *result; 00781 DdManager *mgr; 00782 00783 /* Make sure both operands belong to the same manager. */ 00784 assert(f->mgr == g->mgr); 00785 00786 /* CUDD needs the smothing variables passed as a cube. 00787 * Therefore we must build that cube from the indices of variables 00788 * in the array before calling the procedure. 00789 */ 00790 mgr = f->mgr; 00791 Cudd_Ref(cube = DD_ONE(mgr)); 00792 for (i = 0; i < array_n(smoothing_vars); i++) { 00793 variable = array_fetch(bdd_t *,smoothing_vars,i); 00794 00795 /* Make sure the variable belongs to the same manager. */ 00796 assert(mgr == variable->mgr); 00797 00798 tmpDd = Cudd_bddAnd(mgr,cube,variable->node); 00799 if (tmpDd == NULL) { 00800 Cudd_RecursiveDeref(mgr,cube); 00801 return(NULL); 00802 } 00803 cuddRef(tmpDd); 00804 Cudd_RecursiveDeref(mgr, cube); 00805 cube = tmpDd; 00806 } 00807 00808 /* Perform the smoothing */ 00809 result = Cudd_bddAndAbstractLimit(mgr,f->node,g->node,cube,limit); 00810 if (result == NULL) { 00811 Cudd_RecursiveDeref(mgr, cube); 00812 return(NULL); 00813 } 00814 cuddRef(result); 00815 /* Get rid of temporary results. */ 00816 Cudd_RecursiveDeref(mgr, cube); 00817 00818 /* Build the bdd_t structure for the result */ 00819 return(bdd_construct_bdd_t(mgr,result)); 00820 00821 } /* end of bdd_and_smooth_with_limit */
| bdd_t* bdd_and_with_limit | ( | bdd_t * | f, | |
| bdd_t * | g, | |||
| boolean | f_phase, | |||
| boolean | g_phase, | |||
| unsigned int | limit | |||
| ) |
Function********************************************************************
Synopsis [And of two BDDs with limit on new nodes.]
Description [If more new nodes than specified by limit must be created, this function returns NULL. The caller must be prepared for this occurrence.]
SideEffects []
Definition at line 364 of file cuPort.c.
00370 { 00371 DdManager *dd; 00372 DdNode *newf, *newg, *fandg; 00373 00374 /* Make sure both BDDs belong to the same manager. */ 00375 assert(f->mgr == g->mgr); 00376 00377 /* Modify the phases of the operands according to the parameters. */ 00378 newf = Cudd_NotCond(f->node,!f_phase); 00379 newg = Cudd_NotCond(g->node,!g_phase); 00380 00381 /* Perform the AND operation. */ 00382 dd = f->mgr; 00383 fandg = Cudd_bddAndLimit(f->mgr,newf,newg,limit); 00384 if (fandg == NULL) return(NULL); 00385 cuddRef(fandg); 00386 00387 return(bdd_construct_bdd_t(dd,fandg)); 00388 00389 } /* end of bdd_and_with_limit */
Function********************************************************************
Synopsis [Compares the ratios of the minterms of 2 bdds and two numbers. The ratio compared is ((Min(f1)/f1Num)/(Min(f2)/f2Num)). The procedure returns 1 if the ratio is greater than 1, 0 if they are equal and -1 if the ratio is less than 1. ]
SideEffects []
Definition at line 6757 of file cuPort.c.
06763 { 06764 int result; 06765 DdApaNumber f1Min, f2Min; 06766 int digits1, digits2; 06767 06768 f1Min = Cudd_ApaCountMinterm((DdManager *)f1->mgr, (DdNode *)f1->node, nvars, &digits1); 06769 f2Min = Cudd_ApaCountMinterm((DdManager *)f2->mgr, (DdNode *)f2->node, nvars, &digits2); 06770 06771 result = Cudd_ApaCompareRatios(digits1, f1Min, f1Num, digits2, f2Min, f2Num); 06772 return(result); 06773 06774 } /* end of bdd_apa_compare_ratios */
| bdd_t* bdd_approx_biased_rua | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| bdd_t * | bias, | |||
| int | numVars, | |||
| int | threshold, | |||
| double | quality, | |||
| double | qualityBias | |||
| ) |
Function********************************************************************
Synopsis [Subset (superset) operator.]
Description [It computes a bdd which is a subset (superset) of the given operand and it has less nodes.The bdd chooses to preserve nodes that contribute a large number and throws away those that contribute fewer minterms and dominate a large number of nodes. Some nodes may be remapped to existing nodes in the BDD. approxDir specifies over/under approximation. numVars is the number of variables in the true support of f. threshold is a limit specified on the number of nodes. safe is a parameter to ensure that the result is never larger than the operand. quality is a factor that affects replacement of nodes: 1 is the default value. Values for quality imply that the ratio of the density of the result with replaced nodes to the original bdd is equal to the value. Refer Shiple, Somenzi DAC98. The only difference between this function and bdd_approx_remap_ua is that this function takes a bias BDD and tries to lean the approximation towards the bias]
SideEffects [none]
Definition at line 1808 of file cuPort.c.
01816 { 01817 DdNode *result; 01818 bdd_t *output; 01819 01820 assert(bias->mgr == f->mgr); 01821 switch (approxDir) { 01822 case BDD_OVER_APPROX: 01823 result = Cudd_BiasedOverApprox((DdManager *)f->mgr, (DdNode *)f->node, (DdNode *)bias->node, numVars, threshold, quality, qualityBias); 01824 break; 01825 case BDD_UNDER_APPROX: 01826 result = Cudd_BiasedUnderApprox((DdManager *)f->mgr, (DdNode *)f->node, (DdNode *)bias->node, numVars, threshold, quality, qualityBias); 01827 break; 01828 default: 01829 result = NULL; 01830 } 01831 01832 if (result == NULL) return(NULL); 01833 cuddRef(result); 01834 01835 output = bdd_construct_bdd_t((DdManager *)f->mgr,result); 01836 return(output); 01837 01838 } /* end of bdd_approx_biased_rua */
| bdd_t* bdd_approx_compress | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| int | numVars, | |||
| int | threshold | |||
| ) |
Function********************************************************************
Synopsis [Subset (superset) operator.]
Description [It computes a bdd which is a subset (superset) of the given operand and it has less nodes. approxDir specifies over/under approximation. The number of variables is an estimate of the support of the operand, and threshold is the maximum number of vertices allowed in the result. It applies short paths with the given threshold first and then uses remap_ua to increase density.]
SideEffects [none]
Definition at line 1856 of file cuPort.c.
01861 { 01862 DdNode *result; 01863 bdd_t *output; 01864 01865 switch (approxDir) { 01866 case BDD_OVER_APPROX: 01867 result = Cudd_SupersetCompress(f->mgr, f->node, numVars, threshold); 01868 break; 01869 case BDD_UNDER_APPROX: 01870 result = Cudd_SubsetCompress(f->mgr, f->node, numVars, threshold); 01871 break; 01872 default: 01873 result = NULL; 01874 } 01875 01876 if (result == NULL) return(NULL); 01877 cuddRef(result); 01878 01879 output = bdd_construct_bdd_t(f->mgr,result); 01880 return(output); 01881 01882 } /* end of bdd_approx_compress */
| int bdd_approx_decomp | ( | bdd_t * | f, | |
| bdd_partition_type_t | partType, | |||
| bdd_t *** | conjArray | |||
| ) |
Function********************************************************************
Synopsis [Computes 2 partitions of a function.]
Description [Computes 2 partitions of a function. Picks a subset of a function and minimizes the rest of the function w.r.t. the subset. returns 2 conjuncts(disjuncts).]
SideEffects []
Definition at line 6268 of file cuPort.c.
06269 { 06270 DdNode **ddArray = NULL; 06271 int i, num = 0; 06272 bdd_t *result; 06273 06274 switch (partType) { 06275 case BDD_CONJUNCTS: 06276 num = Cudd_bddApproxConjDecomp(f->mgr, f->node, &ddArray); 06277 break; 06278 case BDD_DISJUNCTS: 06279 num = Cudd_bddApproxDisjDecomp(f->mgr, f->node, &ddArray); 06280 break; 06281 } 06282 if ((ddArray == NULL) || (!num)) { 06283 return 0; 06284 } 06285 06286 *conjArray = ALLOC(bdd_t *, num); 06287 if ((*conjArray) == NULL) goto outOfMem; 06288 for (i = 0; i < num; i++) { 06289 result = ALLOC(bdd_t, 1); 06290 if (result == NULL) { 06291 FREE(*conjArray); 06292 goto outOfMem; 06293 } 06294 result->mgr = f->mgr; 06295 result->node = ddArray[i]; 06296 result->free = FALSE; 06297 (*conjArray)[i] = result; 06298 } 06299 FREE(ddArray); 06300 return (num); 06301 06302 outOfMem: 06303 for (i = 0; i < num; i++) { 06304 Cudd_RecursiveDeref((DdManager *)f->mgr,(DdNode *)ddArray[i]); 06305 } 06306 FREE(ddArray); 06307 return(0); 06308 06309 } /* end of bdd_approx_decomp */
| bdd_t* bdd_approx_hb | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| int | numVars, | |||
| int | threshold | |||
| ) |
Function********************************************************************
Synopsis [Subset (superset) operator.]
Description [It computes a bdd which is a subset (superset) of the given operand and has less nodes. approxDir specifies over/under approximation. The number of variables is an estimate of the support of the operand, and threshold is the maximum number of vertices allowed in the result. The technique applied to eliminate nodes is to remove a child of a node, starting with the root, that contribute to fewer minterms than the other child. Refer to Ravi & Somenzi ICCAD95.]
SideEffects [none]
Definition at line 1605 of file cuPort.c.
01610 { 01611 DdNode *result; 01612 bdd_t *output; 01613 01614 switch (approxDir) { 01615 case BDD_OVER_APPROX: 01616 result = Cudd_SupersetHeavyBranch(f->mgr, f->node, numVars, threshold); 01617 break; 01618 case BDD_UNDER_APPROX: 01619 result = Cudd_SubsetHeavyBranch(f->mgr, f->node, numVars, threshold); 01620 break; 01621 default: 01622 result = NULL; 01623 } 01624 if (result == NULL) return(NULL); 01625 cuddRef(result); 01626 01627 output = bdd_construct_bdd_t(f->mgr,result); 01628 return(output); 01629 01630 } /* end of bdd_approx_hb */
| bdd_t* bdd_approx_remap_ua | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| int | numVars, | |||
| int | threshold, | |||
| double | quality | |||
| ) |
Function********************************************************************
Synopsis [Subset (superset) operator.]
Description [It computes a bdd which is a subset (superset) of the given operand and it has less nodes.The bdd chooses to preserve nodes that contribute a large number and throws away those that contribute fewer minterms and dominate a large number of nodes. Some nodes may be remapped to existing nodes in the BDD. approxDir specifies over/under approximation. numVars is the number of variables in the true support of f. threshold is a limit specified on the number of nodes. safe is a parameter to ensure that the result is never larger than the operand. quality is a factor that affects replacement of nodes: 1 is the default value. Values for quality imply that the ratio of the density of the result with replaced nodes to the original bdd is equal to the value. Refer to Shiple, Somenzi DAC98. ]
SideEffects [none]
Definition at line 1754 of file cuPort.c.
01760 { 01761 DdNode *result; 01762 bdd_t *output; 01763 01764 switch (approxDir) { 01765 case BDD_OVER_APPROX: 01766 result = Cudd_RemapOverApprox((DdManager *)f->mgr, (DdNode *)f->node, numVars, threshold, quality); 01767 break; 01768 case BDD_UNDER_APPROX: 01769 result = Cudd_RemapUnderApprox((DdManager *)f->mgr, (DdNode *)f->node, numVars, threshold, quality); 01770 break; 01771 default: 01772 result = NULL; 01773 } 01774 01775 if (result == NULL) return(NULL); 01776 cuddRef(result); 01777 01778 output = bdd_construct_bdd_t((DdManager *)f->mgr,result); 01779 return(output); 01780 01781 } /* end of bdd_approx_remap_ua */
| bdd_t* bdd_approx_sp | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| int | numVars, | |||
| int | threshold, | |||
| int | hardlimit | |||
| ) |
Function********************************************************************
Synopsis [Subset (superset) operator.]
Description [It computes a bdd which is a subset (superset) of the given operand and it has less nodes. approxDir specifies over/under approximation. The number of variables is an estimate of the support of the operand, and threshold is the maximum number of vertices allowed in the result. If unsure, pass NULL for the number of variables. The method used is to extract the smallest cubes in the bdd which also correspond to the shortest paths in the bdd to the constant 1. hardlimit indicates that the node limit is strict. Refer to Ravi and Somenzi ICCAD95.]
SideEffects [none]
Definition at line 1651 of file cuPort.c.
01657 { 01658 DdNode *result; 01659 bdd_t *output; 01660 01661 switch (approxDir) { 01662 case BDD_OVER_APPROX: 01663 result = Cudd_SupersetShortPaths(f->mgr, f->node, numVars, threshold, hardlimit); 01664 break; 01665 case BDD_UNDER_APPROX: 01666 result = Cudd_SubsetShortPaths(f->mgr, f->node, numVars, threshold, hardlimit); 01667 break; 01668 default: 01669 result = NULL; 01670 } 01671 01672 if (result == NULL) return(NULL); 01673 cuddRef(result); 01674 01675 output = bdd_construct_bdd_t(f->mgr,result); 01676 return(output); 01677 01678 } /* end of bdd_approx_sp */
| bdd_t* bdd_approx_ua | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| int | numVars, | |||
| int | threshold, | |||
| int | safe, | |||
| double | quality | |||
| ) |
Function********************************************************************
Synopsis [Subset (superset) operator.]
Description [It computes a bdd which is a subset (superset) of the given operand and it has less nodes. The bdd chooses to preserve nodes that contribute a large number and throws away those that contribute fewer minterms and dominate a large number of nodes. approxDir specifies over/under approximation. numVars is the number of variables in the true support of f. threshold is a limit specified on the number of nodes. safe is a parameter to ensure that the result is never larger than the operand. quality is a factor that affects replacement of nodes: 1 is the default value. Values for quality imply that the ratio of the density of the result of replaced nodes to the original original is equal to the value. Refer to Shiple thesis.]
SideEffects [none]
Definition at line 1702 of file cuPort.c.
01709 { 01710 DdNode *result; 01711 bdd_t *output; 01712 01713 switch (approxDir) { 01714 case BDD_OVER_APPROX: 01715 result = Cudd_OverApprox(f->mgr, f->node, numVars, threshold, safe, quality); 01716 break; 01717 case BDD_UNDER_APPROX: 01718 result = Cudd_UnderApprox(f->mgr, f->node, numVars, threshold, safe, quality); 01719 break; 01720 default: 01721 result = NULL; 01722 } 01723 if (result == NULL) return(NULL); 01724 cuddRef(result); 01725 01726 output = bdd_construct_bdd_t(f->mgr,result); 01727 return(output); 01728 01729 } /* end of bdd_approx_ua */
| bdd_node* bdd_bdd_and | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Computes the conjunction of two BDDs f and g.]
SideEffects []
| bdd_node* bdd_bdd_and_abstract | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g, | |||
| bdd_node * | cube | |||
| ) |
Function********************************************************************
Synopsis [Takes the AND of two BDDs and simultaneously abstracts the variables in cube.]
SideEffects []
| bdd_node* bdd_bdd_and_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Recursive procedure to compute AND of two bdd_nodes.]
Description [Recursive procedure to compute AND of two bdd_nodes. Returns the pointer to the BDD on success. The reference count of the result is not incremented. NULL is returned in case of reordering or if memory is exhausted.]
SideEffects []
| bdd_node* bdd_bdd_boolean_diff | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| int | x | |||
| ) |
Function********************************************************************
Synopsis [Computes the boolean difference of f w.r.t to variable x.]
SideEffects []
Definition at line 6992 of file cuPort.c.
06993 { 06994 return ((bdd_node *)Cudd_bddBooleanDiff((DdManager *)mgr,(DdNode *)f,x)); 06995 06996 } /* end of bdd_bdd_boolean_diff */
| bdd_node* bdd_bdd_cofactor | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Returns the cofactor of f w.r.t g]
Description [Returns the cofactor of f w.r.t g]
SideEffects []
| bdd_node* bdd_bdd_compute_cube | ( | bdd_manager * | mgr, | |
| bdd_node ** | vars, | |||
| int * | phase, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [Computes the cube of an array of BDD variables.If non-null, the phase argument indicates which literal of each variable should appear in the cube. If phase\[i\] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects []
| bdd_node* bdd_bdd_constrain | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | c | |||
| ) |
Function********************************************************************
Synopsis [Performs the constrain operation.]
SideEffects []
| bdd_node* bdd_bdd_cprojection | ( | bdd_manager * | mgr, | |
| bdd_node * | R, | |||
| bdd_node * | Y | |||
| ) |
Function********************************************************************
Synopsis [Computes the compatible projection of R w.r.t. cube Y.]
Description [Computes the compatible projection of relation R with respect to cube Y.]
SideEffects [None]
Function********************************************************************
Synopsis [Returns the else child of f.]
Description [Returns the else child of f. This is different from bdd_else.]
SideEffects []
SeeAlso [bdd_else]
| bdd_node* bdd_bdd_exist_abstract | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node * | cube | |||
| ) |
Function********************************************************************
Synopsis [Existentially abstracts out the variables from the function. Here the fn is assumed to be a BDD function.]
SideEffects []
| bdd_node* bdd_bdd_ite | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g, | |||
| bdd_node * | h | |||
| ) |
Function********************************************************************
Synopsis [Returns the ITE of f,g and h]
Description [Returns the ITE of f,g and h]
SideEffects []
| bdd_node* bdd_bdd_ith_var | ( | bdd_manager * | mgr, | |
| int | i | |||
| ) |
Function********************************************************************
Synopsis [Get the ith bdd node in the manager.]
SideEffects []
Definition at line 4217 of file cuPort.c.
04218 { 04219 DdNode *result; 04220 result = Cudd_bddIthVar((DdManager *)mgr, i); 04221 04222 return(result); 04223 04224 } /* end of bdd_bdd_ith_var */
| int bdd_bdd_leq | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_bdd_new_var | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns a new BDD variable.]
SideEffects []
Definition at line 4854 of file cuPort.c.
04855 { 04856 DdNode *result; 04857 result = Cudd_bddNewVar((DdManager *)mgr); 04858 04859 return(result); 04860 04861 } /* end of bdd_bdd_new_var */
| bdd_node* bdd_bdd_or | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Computes the disjunction of two BDDs f and g.]
SideEffects []
| bdd_node* bdd_bdd_permute | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| int * | permut | |||
| ) |
Function********************************************************************
Synopsis [Permutes the variables in a given function using the permut array..]
SideEffects []
Definition at line 3834 of file cuPort.c.
03838 { 03839 DdNode *result; 03840 result = Cudd_bddPermute((DdManager *)mgr, (DdNode *)fn, permut); 03841 return(result); 03842 03843 } /* end of bdd_bdd_permute */
Function********************************************************************
Synopsis [Pick arbitrary number of minterms evenly distributed from the onset of f.]
SideEffects []
Definition at line 4732 of file cuPort.c.
04737 { 04738 int i; 04739 DdNode **minterms, **vars; 04740 bdd_t *var; 04741 array_t *resultArray; 04742 04743 vars = ALLOC(DdNode *, n); 04744 if (vars == NULL) 04745 return((array_t *)NULL); 04746 for (i = 0; i < n; i++) { 04747 var = array_fetch(bdd_t *, varsArray, i); 04748 vars[i] = var->node; 04749 } 04750 04751 minterms = (DdNode **)Cudd_bddPickArbitraryMinterms((DdManager *)f->mgr, 04752 (DdNode *)f->node, (DdNode **)vars, n, k); 04753 04754 resultArray = array_alloc(bdd_t *, k); 04755 for (i = 0; i < k; i++) { 04756 cuddRef(minterms[i]); 04757 array_insert(bdd_t *, resultArray, i, 04758 bdd_construct_bdd_t(f->mgr,minterms[i])); 04759 } 04760 04761 FREE(vars); 04762 FREE(minterms); 04763 return(resultArray); 04764 04765 } /* end of bdd_bdd_pick_arbitrary_minterms */
| int bdd_bdd_pick_one_cube | ( | bdd_manager * | mgr, | |
| bdd_node * | node, | |||
| char * | string | |||
| ) |
Function********************************************************************
Synopsis [Picks one on-set cube randomly from the given DD. The cube is written into an array of characters. The array must have at least as many entries as there are variables. Returns 1 if successful; 0 otherwise.]
SideEffects []
Definition at line 4356 of file cuPort.c.
04357 { 04358 return(Cudd_bddPickOneCube((DdManager *)mgr, (DdNode *)node, string)); 04359 04360 } /* end of bdd_bdd_pick_one_cube */
| bdd_node* bdd_bdd_pick_one_minterm | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | vars, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [Pick a random minterm from the onset of f.]
SideEffects []
| bdd_node* bdd_bdd_restrict | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | c | |||
| ) |
Function********************************************************************
Synopsis [Performs the restrict operation.]
SideEffects []
| bdd_node* bdd_bdd_support | ( | bdd_manager * | mgr, | |
| bdd_node * | F | |||
| ) |
Function********************************************************************
Synopsis [Returns the BDD of the variables on which F depends.]
SideEffects []
Definition at line 6955 of file cuPort.c.
06956 { 06957 return((bdd_node *)Cudd_Support((DdManager *)mgr,(DdNode *)F)); 06958 06959 } /* end of bdd_bdd_support */
| int bdd_bdd_support_size | ( | bdd_manager * | mgr, | |
| bdd_node * | F | |||
| ) |
Function********************************************************************
Synopsis [Count the variables on which a DD depends.]
SideEffects []
Definition at line 6940 of file cuPort.c.
06941 { 06942 return(Cudd_SupportSize((DdManager *)mgr,(DdNode *)F)); 06943 06944 } /* end of bdd_bdd_support_size */
| bdd_node* bdd_bdd_swap_variables | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [Swaps two sets of variables of the same size (x and y) in the BDD f.]
SideEffects []
Function********************************************************************
Synopsis [Returns the then child of f.]
Description [Returns the then child of f. This is different from bdd_then.]
SideEffects [none]
SeeAlso [bdd_then]
| bdd_node* bdd_bdd_to_add | ( | bdd_manager * | mgr, | |
| bdd_node * | fn | |||
| ) |
Function********************************************************************
Synopsis [Converts a bdd to an add.]
SideEffects []
| bdd_node* bdd_bdd_univ_abstract | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node * | vars | |||
| ) |
Function********************************************************************
Synopsis [Universally abstracts out the variables from the function]
SideEffects []
| bdd_node* bdd_bdd_vector_compose | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | vector | |||
| ) |
Function********************************************************************
Synopsis [Composes a BDD with a vector of BDDs.Given a vector of BDDs, creates a new BDD by substituting the BDDs for the variables of the BDD f.]
SideEffects []
| bdd_node* bdd_bdd_vector_support | ( | bdd_manager * | mgr, | |
| bdd_node ** | F, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [Finds the variables on which a set of DDs depends.]
SideEffects []
Definition at line 6910 of file cuPort.c.
06911 { 06912 return((bdd_node *)Cudd_VectorSupport((DdManager *)mgr,(DdNode **)F,n)); 06913 06914 } /* end of bdd_bdd_vector_support */
| int bdd_bdd_vector_support_size | ( | bdd_manager * | mgr, | |
| bdd_node ** | F, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [Count the variables on which a set of DDs depend.]
SideEffects []
Definition at line 6925 of file cuPort.c.
06926 { 06927 return(Cudd_VectorSupportSize((DdManager *)mgr,(DdNode **)F,n)); 06928 06929 } /* end of bdd_bdd_vector_support_size */
| bdd_node* bdd_bdd_xnor | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Computes the exclusive-nor of f and g.]
SideEffects []
| bdd_node* bdd_bdd_xor | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Computes the exclusive-or of f and g.]
SideEffects []
Function********************************************************************
Synopsis [Return a minimum size BDD between bounds.]
SideEffects []
Definition at line 994 of file cuPort.c.
00995 { 00996 bdd_t *care_set, *ret; 00997 00998 if (bdd_equal(f_min, f_max)) { 00999 return (bdd_dup(f_min)); 01000 } 01001 care_set = bdd_or(f_min, f_max, 1, 0); 01002 ret = bdd_minimize(f_min, care_set); 01003 bdd_free(care_set); 01004 /* The size of ret is never larger than the size of f_min. We need 01005 ** only to check ret against f_max. */ 01006 if (bdd_size(f_max) <= bdd_size(ret)) { 01007 bdd_free(ret); 01008 return(bdd_dup(f_max)); 01009 } else { 01010 return(ret); 01011 } 01012 01013 } /* end of bdd_between */
| int bdd_bind_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Prevents sifting of a variable.]
Description [This function sets a flag to prevent sifting of a variable. Returns 1 if successful; 0 otherwise (i.e., invalid variable index).]
SideEffects [Changes the "bindVar" flag in DdSubtable.]
Definition at line 7344 of file cuPort.c.
07345 { 07346 return Cudd_bddBindVar((DdManager *) mgr, index); 07347 07348 } /* end of bdd_bind_var */
| int bdd_check_zero_ref | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Performs the zero reference count check on the manager.]
SideEffects []
Definition at line 4015 of file cuPort.c.
04016 { 04017 int result; 04018 result = Cudd_CheckZeroRef((DdManager *)mgr); 04019 return(result); 04020 04021 } /* end of bdd_check_zero_ref */
| bdd_t* bdd_clipping_and_smooth | ( | bdd_t * | f, | |
| bdd_t * | g, | |||
| array_t * | smoothing_vars, | |||
| int | maxDepth, | |||
| int | over | |||
| ) |
Function********************************************************************
Synopsis [Abstracts variables from the product of two BDDs. Computation is clipped at a certain depth.]
Description [Abstracts variables from the product of two BDDs. Computation is clipped at a certain depth. This procedure is similar to bdd_and_smooth but large depth recursions are avoided. maxDepth specifies the recursion depth. over specifies which kind of approximation is used 0 - under approximation and 1 - for over approximation. ]
SideEffects []
Definition at line 874 of file cuPort.c.
00880 { 00881 int i; 00882 bdd_t *variable; 00883 DdNode *cube,*tmpDd,*result; 00884 DdManager *mgr; 00885 00886 /* Make sure both operands belong to the same manager. */ 00887 assert(f->mgr == g->mgr); 00888 00889 /* The Boulder package needs the smothing variables passed as a cube. 00890 * Therefore we must build that cube from the indices of variables 00891 * in the array before calling the procedure. 00892 */ 00893 mgr = f->mgr; 00894 Cudd_Ref(cube = DD_ONE(mgr)); 00895 for (i = 0; i < array_n(smoothing_vars); i++) { 00896 variable = array_fetch(bdd_t *,smoothing_vars,i); 00897 00898 /* Make sure the variable belongs to the same manager. */ 00899 assert(mgr == variable->mgr); 00900 00901 tmpDd = Cudd_bddAnd(mgr,cube,variable->node); 00902 if (tmpDd == NULL) { 00903 Cudd_RecursiveDeref(mgr,cube); 00904 return(NULL); 00905 } 00906 cuddRef(tmpDd); 00907 Cudd_RecursiveDeref(mgr, cube); 00908 cube = tmpDd; 00909 } 00910 00911 /* Perform the smoothing */ 00912 result = Cudd_bddClippingAndAbstract(mgr,f->node,g->node,cube, maxDepth, over); 00913 if (result == NULL) { 00914 Cudd_RecursiveDeref(mgr, cube); 00915 return(NULL); 00916 } 00917 cuddRef(result); 00918 /* Get rid of temporary results. */ 00919 Cudd_RecursiveDeref(mgr, cube); 00920 00921 /* Build the bdd_t structure for the result */ 00922 return(bdd_construct_bdd_t(mgr,result)); 00923 00924 } /* end of bdd_clipping_and_smooth */
Function********************************************************************
Synopsis [Returns a BDD included in f at minimum distance from g.]
SideEffects [The distance is returned as a side effect in dist.]
Definition at line 2413 of file cuPort.c.
02417 { 02418 DdNode *result; 02419 02420 /* Make sure both operands belong to the same manager. */ 02421 assert(f->mgr == g->mgr); 02422 02423 result = Cudd_bddClosestCube(f->mgr,f->node,g->node,dist); 02424 if (result == NULL) return(NULL); 02425 cuddRef(result); 02426 return(bdd_construct_bdd_t(f->mgr,result)); 02427 02428 } /* end of bdd_closest_cube */
| double* bdd_cof_minterm | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [Computes the fraction of minterms in the on-set of all the positive cofactors of a BDD, called signatures.]
SideEffects [Creates an array of doubles as large as the number of variables in the manager + 1. The extra position is to the fraction of minterms in the on-set of the function.]
Definition at line 6462 of file cuPort.c.
06463 { 06464 double *signatures; 06465 signatures = Cudd_CofMinterm((DdManager *)f->mgr, (DdNode *)f->node); 06466 return (signatures); 06467 06468 } /* end of bdd_cof_minterm */
Function********************************************************************
Synopsis [Computes the cofactor of f with respect to g.]
SideEffects []
Definition at line 1102 of file cuPort.c.
01103 { 01104 DdNode *result; 01105 01106 /* Make sure both operands belong to the same manager */ 01107 assert(f->mgr == g->mgr); 01108 01109 /* We use Cudd_bddConstrain instead of Cudd_Cofactor for generality. */ 01110 result = Cudd_bddConstrain(f->mgr,f->node, 01111 g->node); 01112 if (result == NULL) return(NULL); 01113 cuddRef(result); 01114 return(bdd_construct_bdd_t(f->mgr,result)); 01115 01116 } /* end of bdd_cofactor */
Function********************************************************************
Synopsis [Computes the cofactor of f with respect to g.]
SideEffects []
Definition at line 1127 of file cuPort.c.
01128 { 01129 bdd_t *operand; 01130 DdNode *result, *temp; 01131 int i; 01132 01133 Cudd_Ref(result = f->node); 01134 01135 for (i = 0; i < array_n(bddArray); i++) { 01136 operand = array_fetch(bdd_t *, bddArray, i); 01137 temp = Cudd_bddConstrain(f->mgr, result, operand->node); 01138 if (temp == NULL) { 01139 Cudd_RecursiveDeref(f->mgr, result); 01140 return(NULL); 01141 } 01142 cuddRef(temp); 01143 Cudd_RecursiveDeref(f->mgr, result); 01144 result = temp; 01145 } 01146 01147 return(bdd_construct_bdd_t(f->mgr,result)); 01148 01149 } /* end of bdd_cofactor_array */
Function********************************************************************
Synopsis [Computes the cofactor of f with respect to g in a safe manner.]
Description [Performs safe minimization of a BDD. Given the BDD f of a function to be minimized and a BDD c representing the care set, Cudd_bddLICompaction produces the BDD of a function that agrees with f wherever c is 1. Safe minimization means that the size of the result is guaranteed not to exceed the size of f. This function is based on the DAC97 paper by Hong et al.. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects []
Definition at line 1194 of file cuPort.c.
01195 { 01196 DdNode *result; 01197 01198 /* Make sure both operands belong to the same manager */ 01199 assert(f->mgr == g->mgr); 01200 01201 result = Cudd_bddLICompaction(f->mgr,f->node, 01202 g->node); 01203 if (result == NULL) return(NULL); 01204 cuddRef(result); 01205 return(bdd_construct_bdd_t(f->mgr,result)); 01206 01207 } /* end of bdd_compact */
Function********************************************************************
Synopsis [Functional composition of a function by a variable.]
SideEffects []
Definition at line 1242 of file cuPort.c.
01243 { 01244 DdNode *result; 01245 01246 /* Make sure all operands belong to the same manager. */ 01247 assert(f->mgr == g->mgr); 01248 assert(f->mgr == v->mgr); 01249 01250 result = Cudd_bddCompose(f->mgr,f->node, 01251 g->node, 01252 (int)Cudd_Regular(v->node)->index); 01253 if (result == NULL) return(NULL); 01254 cuddRef(result); 01255 return(bdd_construct_bdd_t(f->mgr,result)); 01256 01257 } /* end of bdd_compose */
| bdd_t* bdd_compute_cube | ( | bdd_manager * | mgr, | |
| array_t * | vars | |||
| ) |
Function********************************************************************
Synopsis [Computes the cube of an array of mdd ids. The cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects []
Definition at line 1026 of file cuPort.c.
01027 { 01028 DdNode *result; 01029 DdNode **nodeArray; 01030 int i, id; 01031 01032 if (vars == NIL(array_t)) return NIL(bdd_t); 01033 if (array_n(vars) == 0) return NIL(bdd_t); 01034 /* create an array of DdNodes */ 01035 nodeArray = ALLOC(DdNode *, array_n(vars)); 01036 arrayForEachItem(int, vars, i, id) { 01037 assert(id < bdd_num_vars(mgr)); 01038 nodeArray[i] = Cudd_bddIthVar((DdManager *)mgr, id); 01039 } 01040 result = Cudd_bddComputeCube((DdManager *)mgr, (DdNode **)nodeArray, 01041 NULL, array_n(vars)); 01042 FREE(nodeArray); 01043 if (result == NULL) return(NULL); 01044 cuddRef(result); 01045 return(bdd_construct_bdd_t(mgr,result)); 01046 01047 } /* end of bdd_compute_cube */
| bdd_t* bdd_compute_cube_with_phase | ( | bdd_manager * | mgr, | |
| array_t * | vars, | |||
| array_t * | phase | |||
| ) |
Function********************************************************************
Synopsis [Computes the cube of an array of mdd ids. The phase if each variable is given in the phase array. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [none]
Definition at line 1060 of file cuPort.c.
01061 { 01062 DdNode *result; 01063 DdNode **nodeArray; 01064 int *phaseArray; 01065 int i, id, ph; 01066 01067 if (vars == NIL(array_t)) return NIL(bdd_t); 01068 if (array_n(vars) == 0) return NIL(bdd_t); 01069 if (phase != NIL(array_t) && array_n(vars) != array_n(phase)) 01070 return NIL(bdd_t); 01071 /* create an array of DdNodes */ 01072 nodeArray = ALLOC(DdNode *, array_n(vars)); 01073 phaseArray = NIL(int); 01074 if (phase != NIL(array_t)) phaseArray = ALLOC(int, array_n(phase)); 01075 arrayForEachItem(int, vars, i, id) { 01076 assert(id < bdd_num_vars(mgr)); 01077 nodeArray[i] = Cudd_bddIthVar((DdManager *)mgr, id); 01078 } 01079 arrayForEachItem(int, phase, i, ph) { 01080 assert(ph == 0 || ph == 1); 01081 phaseArray[i] = ph; 01082 } 01083 result = Cudd_bddComputeCube((DdManager *)mgr, (DdNode **)nodeArray, 01084 phaseArray, array_n(vars)); 01085 FREE(nodeArray); 01086 if (phaseArray != NIL(int)) FREE(phaseArray); 01087 if (result == NULL) return(NULL); 01088 cuddRef(result); 01089 return(bdd_construct_bdd_t(mgr,result)); 01090 01091 } /* end of bdd_compute_cube_with_phase */
Function********************************************************************
Synopsis [Universal Abstraction of Variables.]
SideEffects []
Definition at line 1317 of file cuPort.c.
01320 { 01321 int i; 01322 bdd_t *variable; 01323 DdNode *cube,*tmpDd,*result; 01324 DdManager *mgr; 01325 01326 /* The Boulder package needs the smothing variables passed as a cube. 01327 * Therefore we must build that cube from the indices of the variables 01328 * in the array before calling the procedure. 01329 */ 01330 mgr = f->mgr; 01331 Cudd_Ref(cube = DD_ONE(mgr)); 01332 for (i = 0; i < array_n(quantifying_vars); i++) { 01333 variable = array_fetch(bdd_t *,quantifying_vars,i); 01334 01335 /* Make sure the variable belongs to the same manager */ 01336 assert(mgr == variable->mgr); 01337 01338 tmpDd = Cudd_bddAnd(mgr,cube,variable->node); 01339 if (tmpDd == NULL) { 01340 Cudd_RecursiveDeref(mgr, cube); 01341 return(NULL); 01342 } 01343 cuddRef(tmpDd); 01344 Cudd_RecursiveDeref(mgr, cube); 01345 cube = tmpDd; 01346 } 01347 01348 /* Perform the consensus */ 01349 result = Cudd_bddUnivAbstract(mgr,f->node,cube); 01350 if (result == NULL) { 01351 Cudd_RecursiveDeref(mgr, cube); 01352 return(NULL); 01353 } 01354 cuddRef(result); 01355 /* Get rid of temporary results */ 01356 Cudd_RecursiveDeref(mgr, cube); 01357 01358 /* Build the bdd_t structure for the result */ 01359 return(bdd_construct_bdd_t(mgr,result)); 01360 01361 } /* end of bdd_consensus */
Function********************************************************************
Synopsis [Universal Abstraction of Variables.]
SideEffects []
Definition at line 1372 of file cuPort.c.
01375 { 01376 DdNode *result; 01377 DdManager *mgr; 01378 01379 mgr = f->mgr; 01380 /* Perform the consensus */ 01381 result = Cudd_bddUnivAbstract(mgr,f->node,cube->node); 01382 if (result == NULL) 01383 return(NULL); 01384 cuddRef(result); 01385 01386 /* Build the bdd_t structure for the result */ 01387 return(bdd_construct_bdd_t(mgr,result)); 01388 01389 } /* end of bdd_consensus_with_cube */
| bdd_t* bdd_construct_bdd_t | ( | bdd_manager * | mgr, | |
| bdd_node * | fn | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Builds the bdd_t structure.]
Description [Builds the bdd_t structure from manager and node. Assumes that the reference count of the node has already been increased. If it fails to create a new bdd_t structure it disposes of the node to simplify error handling for the caller. Returns a pointer to the newly created structure if successful; NULL otherwise.]
SideEffects []
Definition at line 113 of file cuPort.c.
00114 { 00115 bdd_t *result; 00116 00117 result = ALLOC(bdd_t, 1); 00118 if (result == NULL) { 00119 Cudd_RecursiveDeref((DdManager *)mgr,(DdNode *)fn); 00120 return(NULL); 00121 } 00122 result->mgr = (DdManager *) mgr; 00123 result->node = (DdNode *) fn; 00124 result->free = FALSE; 00125 return(result); 00126 00127 } /* end of bdd_construct_bdd_t */
Function********************************************************************
Synopsis [Computes the correlation of f and g.]
Description [Computes the correlation of f and g. If f == g, their correlation is 1. If f == g', their correlation is 0. Returns the fraction of minterms in the ON-set of the EXNOR of f and g.]
SideEffects [None]
| double bdd_count_minterm | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [Counts the number of minters in the on set of f which depends on atmost n variables.]
SideEffects []
Definition at line 4581 of file cuPort.c.
04582 { 04583 double result; 04584 result = Cudd_CountMinterm((DdManager *)mgr, (DdNode *)f, n); 04585 04586 return(result); 04587 04588 } /* end of bdd_count_minterm */
Function********************************************************************
Synopsis [Counts the number of minterms in the on set.]
SideEffects []
Definition at line 2549 of file cuPort.c.
02552 { 02553 return(Cudd_CountMinterm(f->mgr,f->node,array_n(var_array))); 02554 02555 } /* end of bdd_count_onset */
Function********************************************************************
Synopsis [The compatible projection function.]
Description [The compatible projection function. The reference minterm is chosen based on the phases of the quantifying variables. If all variables are in positive phase, the minterm 111...111 is used as reference.]
SideEffects []
Definition at line 1405 of file cuPort.c.
01408 { 01409 DdManager *dd; 01410 DdNode *cube; 01411 DdNode *res; 01412 bdd_t *fi; 01413 int nvars, i; 01414 01415 if (f == NULL) { 01416 fail ("bdd_cproject: invalid BDD"); 01417 } 01418 01419 nvars = array_n(quantifying_vars); 01420 if (nvars <= 0) { 01421 fail("bdd_cproject: no projection variables"); 01422 } 01423 dd = f->mgr; 01424 01425 cube = DD_ONE(dd); 01426 cuddRef(cube); 01427 for (i = nvars - 1; i >= 0; i--) { 01428 DdNode *tmpp; 01429 fi = array_fetch(bdd_t *, quantifying_vars, i); 01430 tmpp = Cudd_bddAnd(dd,fi->node,cube); 01431 if (tmpp == NULL) { 01432 Cudd_RecursiveDeref(dd,cube); 01433 return(NULL); 01434 } 01435 cuddRef(tmpp); 01436 Cudd_RecursiveDeref(dd,cube); 01437 cube = tmpp; 01438 } 01439 01440 res = Cudd_CProjection(dd,f->node,cube); 01441 if (res == NULL) { 01442 Cudd_RecursiveDeref(dd,cube); 01443 return(NULL); 01444 } 01445 cuddRef(res); 01446 Cudd_RecursiveDeref(dd,cube); 01447 01448 return(bdd_construct_bdd_t(dd,res)); 01449 01450 } /* end of bdd_cproject */
| bdd_t* bdd_create_variable | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Creates a new variable in the manager.]
SideEffects [Modifies the manager]
SeeAlso [bdd_create_variable_after]
Definition at line 199 of file cuPort.c.
00200 { 00201 DdNode *var; 00202 DdManager *dd = (DdManager *) mgr; 00203 DdNode *one = DD_ONE(dd); 00204 00205 if (dd->size >= CUDD_MAXINDEX -1) return(NULL); 00206 do { 00207 dd->reordered = 0; 00208 var = cuddUniqueInter(dd,dd->size,one,Cudd_Not(one)); 00209 } while (dd->reordered == 1); 00210 00211 if (var == NULL) return((bdd_t *)NULL); 00212 cuddRef(var); 00213 return(bdd_construct_bdd_t(dd,var)); 00214 00215 } /* end of bdd_create_variable */
| bdd_t* bdd_create_variable_after | ( | bdd_manager * | mgr, | |
| bdd_variableId | after_id | |||
| ) |
Function********************************************************************
Synopsis [Creates a new variable and positions it after the variable with the specified index.]
SideEffects [Modifies the manager.]
SeeAlso [bdd_create_variable]
Definition at line 229 of file cuPort.c.
00230 { 00231 DdNode *var; 00232 DdManager *dd = (DdManager *) mgr; 00233 int level; 00234 00235 if (after_id >= (bdd_variableId) dd->size) return(NULL); 00236 level = 1 + dd->perm[after_id]; 00237 var = Cudd_bddNewVarAtLevel(dd,level); 00238 if (var == NULL) return((bdd_t *)NULL); 00239 cuddRef(var); 00240 return(bdd_construct_bdd_t(dd,var)); 00241 00242 } /* end of bdd_create_variable_after */
| int bdd_debug_check | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Checks for inconsistencies in the BDD manager.]
Description [Checks for inconsistencies in the BDD manager.]
SideEffects [None]
SeeAlso [Cudd_DebugCheck]
Definition at line 6716 of file cuPort.c.
06717 { 06718 return Cudd_DebugCheck((DdManager *)mgr); 06719 06720 } /* end of bdd_debug_check */
| void bdd_deref | ( | bdd_node * | f | ) |
Function********************************************************************
Synopsis [Decreases the reference count of node.]
SideEffects []
Definition at line 4895 of file cuPort.c.
04896 { 04897 Cudd_Deref((DdNode *)f); 04898 04899 } /* end of bdd_deref */
| int bdd_disable_reordering_reporting | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Disables reporting of reordering stats.]
SideEffects []
Definition at line 3257 of file cuPort.c.
03258 { 03259 int retval; 03260 retval = Cudd_DisableReorderingReporting((DdManager *) mgr); 03261 return retval; 03262 03263 } /* end of bdd_disable_reordering_reporting */
| void bdd_discard_all_var_groups | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Frees the variable group tree of the manager.]
SideEffects [None]
Definition at line 7401 of file cuPort.c.
07402 { 07403 Cudd_FreeTree((DdManager *) mgr); 07404 07405 } /* end of bdd_discard_all_var_groups */
| void bdd_dump_blif | ( | bdd_manager * | mgr, | |
| int | nBdds, | |||
| bdd_node ** | bdds, | |||
| char ** | inames, | |||
| char ** | onames, | |||
| char * | model, | |||
| FILE * | fp | |||
| ) |
Function********************************************************************
Synopsis [Generates a blif file by dumpping BDDs. nBdds is the number of BDDs, bdds is the array of BDDs, inames is the array of primary input variable names, onames is the array of variable names of BDDs, and model is a model name in BLIF. inames, onames and model can be NULL.]
SideEffects []
Definition at line 6807 of file cuPort.c.
06815 { 06816 Cudd_DumpBlif((DdManager *)mgr, nBdds, (DdNode **)bdds, inames, onames, 06817 model, fp, 0); 06818 06819 } /* end of bdd_dump_blif */
| void bdd_dump_blif_body | ( | bdd_manager * | mgr, | |
| int | nBdds, | |||
| bdd_node ** | bdds, | |||
| char ** | inames, | |||
| char ** | onames, | |||
| FILE * | fp | |||
| ) |
Function********************************************************************
Synopsis [Generates a blif body by dumpping BDDs. nBdds is the number of BDDs, bdds is the array of BDDs, inames is the array of primary input variable names, onames is the array of variable names of BDDs, and inames, onames and model can be NULL. This function prints out only .names body.]
SideEffects []
Definition at line 6834 of file cuPort.c.
06841 { 06842 Cudd_DumpBlifBody((DdManager *)mgr, nBdds, (DdNode **)bdds, inames, onames, 06843 fp, 0); 06844 06845 } /* end of bdd_dump_blif_body */
| void bdd_dump_dot | ( | bdd_manager * | mgr, | |
| int | nBdds, | |||
| bdd_node ** | bdds, | |||
| char ** | inames, | |||
| char ** | onames, | |||
| FILE * | fp | |||
| ) |
Function********************************************************************
Synopsis [Generates a dot file by dumpping BDDs. nBdds is the number of BDDs, bdds is the array of BDDs, inames is the array of primary input variable names, and onames is the array of variable names of BDDs. inames, onames and model can be NULL.]
SideEffects []
Definition at line 6859 of file cuPort.c.
06866 { 06867 Cudd_DumpDot((DdManager *)mgr, nBdds, (DdNode **)bdds, inames, onames, fp); 06868 06869 } /* end of bdd_dump_dot */
| bdd_node* bdd_dxygtdxz | ( | bdd_manager * | mgr, | |
| int | N, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y, | |||
| bdd_node ** | z | |||
| ) |
Function********************************************************************
Synopsis [Generates a BDD for the function d(x,y) > d(x,z).]
Description [This function generates a BDD for the function d(x,y) > d(x,z); x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\], y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\], with 0 the most significant bit. The distance d(x,y) is defined as: {i=0}^{N-1}(|x_i - y_i| 2^{N-i-1}). The BDD is built bottom-up. It has 7*N-3 internal nodes, if the variables are ordered as follows: x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ]
SideEffects [None]
SeeAlso [bdd_xgty]
| void bdd_dynamic_reordering | ( | bdd_manager * | mgr_, | |
| bdd_reorder_type_t | algorithm_type, | |||
| bdd_reorder_verbosity_t | verbosity | |||
| ) |
Function********************************************************************
Synopsis [Reorders the BDD pool.]
SideEffects []
Definition at line 3317 of file cuPort.c.
03321 { 03322 DdManager *mgr; 03323 03324 mgr = (DdManager *)mgr_; 03325 03326 switch (algorithm_type) { 03327 case BDD_REORDER_SIFT: 03328 Cudd_AutodynEnable(mgr, CUDD_REORDER_SIFT); 03329 break; 03330 case BDD_REORDER_WINDOW: 03331 case BDD_REORDER_WINDOW3_CONV: 03332 Cudd_AutodynEnable(mgr, CUDD_REORDER_WINDOW3_CONV); 03333 break; 03334 case BDD_REORDER_NONE: 03335 Cudd_AutodynDisable(mgr); 03336 break; 03337 case BDD_REORDER_SAME: 03338 Cudd_AutodynEnable(mgr, CUDD_REORDER_SAME); 03339 break; 03340 case BDD_REORDER_RANDOM: 03341 Cudd_AutodynEnable(mgr, CUDD_REORDER_RANDOM); 03342 break; 03343 case BDD_REORDER_RANDOM_PIVOT: 03344 Cudd_AutodynEnable(mgr, CUDD_REORDER_RANDOM_PIVOT); 03345 break; 03346 case BDD_REORDER_SIFT_CONVERGE: 03347 Cudd_AutodynEnable(mgr,CUDD_REORDER_SIFT_CONVERGE); 03348 break; 03349 case BDD_REORDER_SYMM_SIFT: 03350 Cudd_AutodynEnable(mgr, CUDD_REORDER_SYMM_SIFT); 03351 break; 03352 case BDD_REORDER_SYMM_SIFT_CONV: 03353 Cudd_AutodynEnable(mgr, CUDD_REORDER_SYMM_SIFT_CONV); 03354 break; 03355 case BDD_REORDER_WINDOW2: 03356 Cudd_AutodynEnable(mgr, CUDD_REORDER_WINDOW2); 03357 break; 03358 case BDD_REORDER_WINDOW4: 03359 Cudd_AutodynEnable(mgr, CUDD_REORDER_WINDOW4); 03360 break; 03361 case BDD_REORDER_WINDOW2_CONV: 03362 Cudd_AutodynEnable(mgr, CUDD_REORDER_WINDOW2_CONV); 03363 break; 03364 case BDD_REORDER_WINDOW3: 03365 Cudd_AutodynEnable(mgr, CUDD_REORDER_WINDOW3); 03366 break; 03367 case BDD_REORDER_WINDOW4_CONV: 03368 Cudd_AutodynEnable(mgr, CUDD_REORDER_WINDOW4_CONV); 03369 break; 03370 case BDD_REORDER_GROUP_SIFT: 03371 Cudd_AutodynEnable(mgr, CUDD_REORDER_GROUP_SIFT); 03372 break; 03373 case BDD_REORDER_GROUP_SIFT_CONV: 03374 Cudd_AutodynEnable(mgr, CUDD_REORDER_GROUP_SIFT_CONV); 03375 break; 03376 case BDD_REORDER_ANNEALING: 03377 Cudd_AutodynEnable(mgr, CUDD_REORDER_ANNEALING); 03378 break; 03379 case BDD_REORDER_GENETIC: 03380 Cudd_AutodynEnable(mgr, CUDD_REORDER_GENETIC); 03381 break; 03382 case BDD_REORDER_EXACT: 03383 Cudd_AutodynEnable(mgr, CUDD_REORDER_EXACT); 03384 break; 03385 case BDD_REORDER_LAZY_SIFT: 03386 Cudd_AutodynEnable(mgr, CUDD_REORDER_LAZY_SIFT); 03387 break; 03388 default: 03389 fprintf(stderr,"CU DD Package: Reordering algorithm not considered\n"); 03390 } 03391 03392 if (verbosity == BDD_REORDER_NO_VERBOSITY) { 03393 (void) bdd_disable_reordering_reporting((DdManager *)mgr); 03394 } else if (verbosity == BDD_REORDER_VERBOSITY) { 03395 (void) bdd_enable_reordering_reporting((DdManager *)mgr); 03396 } 03397 03398 } /* end of bdd_dynamic_reordering */
| void bdd_dynamic_reordering_disable | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Disables dynamic reordering in the manager.]
SideEffects []
Definition at line 4032 of file cuPort.c.
04033 { 04034 Cudd_AutodynDisable((DdManager *)mgr); 04035 return; 04036 04037 } /* end of bdd_dynamic_reordering_disable */
| void bdd_dynamic_reordering_zdd | ( | bdd_manager * | mgr_, | |
| bdd_reorder_type_t | algorithm_type, | |||
| bdd_reorder_verbosity_t | verbosity | |||
| ) |
Function********************************************************************
Synopsis [Reorders the ZDD pool.]
SideEffects []
Definition at line 3409 of file cuPort.c.
03413 { 03414 DdManager *mgr; 03415 03416 mgr = (DdManager *)mgr_; 03417 03418 switch (algorithm_type) { 03419 case BDD_REORDER_SIFT: 03420 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_SIFT); 03421 break; 03422 case BDD_REORDER_WINDOW: 03423 case BDD_REORDER_WINDOW3_CONV: 03424 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_WINDOW3_CONV); 03425 break; 03426 case BDD_REORDER_NONE: 03427 Cudd_AutodynDisable(mgr); 03428 break; 03429 case BDD_REORDER_SAME: 03430 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_SAME); 03431 break; 03432 case BDD_REORDER_RANDOM: 03433 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_RANDOM); 03434 break; 03435 case BDD_REORDER_RANDOM_PIVOT: 03436 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_RANDOM_PIVOT); 03437 break; 03438 case BDD_REORDER_SIFT_CONVERGE: 03439 Cudd_AutodynEnableZdd(mgr,CUDD_REORDER_SIFT_CONVERGE); 03440 break; 03441 case BDD_REORDER_SYMM_SIFT: 03442 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_SYMM_SIFT); 03443 break; 03444 case BDD_REORDER_SYMM_SIFT_CONV: 03445 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_SYMM_SIFT_CONV); 03446 break; 03447 case BDD_REORDER_WINDOW2: 03448 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_WINDOW2); 03449 break; 03450 case BDD_REORDER_WINDOW4: 03451 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_WINDOW4); 03452 break; 03453 case BDD_REORDER_WINDOW2_CONV: 03454 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_WINDOW2_CONV); 03455 break; 03456 case BDD_REORDER_WINDOW3: 03457 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_WINDOW3); 03458 break; 03459 case BDD_REORDER_WINDOW4_CONV: 03460 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_WINDOW4_CONV); 03461 break; 03462 case BDD_REORDER_GROUP_SIFT: 03463 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_GROUP_SIFT); 03464 break; 03465 case BDD_REORDER_GROUP_SIFT_CONV: 03466 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_GROUP_SIFT_CONV); 03467 break; 03468 case BDD_REORDER_ANNEALING: 03469 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_ANNEALING); 03470 break; 03471 case BDD_REORDER_GENETIC: 03472 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_GENETIC); 03473 break; 03474 case BDD_REORDER_EXACT: 03475 Cudd_AutodynEnableZdd(mgr, CUDD_REORDER_EXACT); 03476 break; 03477 default: 03478 fprintf(stderr,"CU DD Package: Reordering algorithm not considered\n"); 03479 } 03480 if (verbosity == BDD_REORDER_NO_VERBOSITY) { 03481 (void) bdd_disable_reordering_reporting((DdManager *)mgr); 03482 } else if (verbosity == BDD_REORDER_VERBOSITY) { 03483 (void) bdd_enable_reordering_reporting((DdManager *)mgr); 03484 } 03485 03486 } /* end of bdd_dynamic_reordering_zdd */
| void bdd_dynamic_reordering_zdd_disable | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Disables dynamic reordering for ZDD in the manager.]
SideEffects []
Definition at line 4048 of file cuPort.c.
04049 { 04050 Cudd_AutodynDisableZdd((DdManager *)mgr); 04051 return; 04052 04053 } /* end of bdd_dynamic_reordering_zdd_disable */
Function********************************************************************
Synopsis [Returns the else branch of a BDD.]
SideEffects []
Definition at line 1461 of file cuPort.c.
01462 { 01463 DdNode *result; 01464 01465 result = Cudd_E(f->node); 01466 result = Cudd_NotCond(result,Cudd_IsComplement(f->node)); 01467 cuddRef(result); 01468 return(bdd_construct_bdd_t(f->mgr,result)); 01469 01470 } /* end of bdd_else */
| int bdd_enable_reordering_reporting | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Enables reporting of reordering stats.]
SideEffects []
Definition at line 3240 of file cuPort.c.
03241 { 03242 int retval; 03243 retval = Cudd_EnableReorderingReporting((DdManager *) mgr); 03244 return retval; 03245 03246 } /* end of bdd_enable_reordering_reporting */
| void bdd_end | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Terminates the bdd package.]
SideEffects []
Function********************************************************************
Synopsis [Counts the number of minterms in the on set.]
SideEffects []
Definition at line 2566 of file cuPort.c.
02570 { 02571 return(Cudd_EpdCountMinterm(f->mgr,f->node,array_n(var_array),epd)); 02572 02573 } /* end of bdd_epd_count_onset */
Function********************************************************************
Synopsis [Equality check with don't care conditions.]
Description [Returns 1 if f equals g wherever careSet is 1.]
SideEffects [None: No new nodes are created.]
| int bdd_equal_sup_norm | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node * | gn, | |||
| BDD_VALUE_TYPE | tolerance, | |||
| int | pr | |||
| ) |
Function********************************************************************
Synopsis [Compares two ADDs for equality within tolerance. pr is verbosity level.]
SideEffects []
Definition at line 4174 of file cuPort.c.
04180 { 04181 int result; 04182 result = Cudd_EqualSupNorm((DdManager *)mgr, (DdNode *)fn, 04183 (DdNode *)gn, (CUDD_VALUE_TYPE)tolerance, pr); 04184 return(result); 04185 04186 } /* end of bdd_equal_sup_norm */
Function********************************************************************
Synopsis [Estimates the size of the cofactor of f with respect to var in the specified phase. Return the number of nodes in the estimated size.]
SideEffects []
Definition at line 6481 of file cuPort.c.
06482 { 06483 return (Cudd_EstimateCofactor((DdManager *)f->mgr, (DdNode *)f->node, 06484 (int)bdd_top_var_id(var), phase)); 06485 06486 } /* end of bdd_estimate_cofactor */
Function********************************************************************
Synopsis [Extracts a BDD node from the bdd_t structure without making it regular.]
SideEffects []
Function********************************************************************
Synopsis [Finds the essential variable in a bdd f. Returns an array_t of vars which are the projection variables with the proper phase.]
SideEffects [Creates an array_t of bdd_t. Freed by the caller. ]
Definition at line 6528 of file cuPort.c.
06529 { 06530 DdNode *C, *result, *scan, *cube; 06531 array_t *varArray = NIL(array_t); 06532 bdd_t *var; 06533 06534 result = Cudd_FindEssential((DdManager *)f->mgr, (DdNode *)f->node); 06535 if (result == NULL) return NULL; 06536 cuddRef(result); 06537 06538 cube = result; 06539 C = Cudd_Regular(cube); 06540 varArray = array_alloc(bdd_t *, 0); 06541 while (!cuddIsConstant(C)) { 06542 var = bdd_var_with_index(f->mgr, C->index); 06543 scan = cuddT(C); 06544 if (Cudd_NotCond(scan, !Cudd_IsComplement(cube)) == DD_ONE(f->mgr)) { 06545 array_insert_last(bdd_t *, varArray, bdd_not(var)); 06546 bdd_free(var); 06547 scan = cuddE(C); 06548 } else { 06549 array_insert_last(bdd_t *, varArray, var); 06550 } 06551 cube = Cudd_NotCond(scan, Cudd_IsComplement(cube)); 06552 C = Cudd_Regular(cube); 06553 } 06554 06555 Cudd_RecursiveDeref((DdManager *)f->mgr,result); 06556 return varArray; 06557 06558 } /* end of bdd_find_essential */
Function********************************************************************
Synopsis [Finds the essential variables in a bdd f. Returns a cube of the variables.]
SideEffects [ ]
Definition at line 6570 of file cuPort.c.
06571 { 06572 DdNode *cube; 06573 bdd_t *result; 06574 06575 cube = Cudd_FindEssential((DdManager *)f->mgr, (DdNode *)f->node); 06576 if (cube == NULL) return NULL; 06577 cuddRef(cube); 06578 result = bdd_construct_bdd_t(f->mgr,cube); 06579 06580 return(result); 06581 06582 } /* end of bdd_find_essential_cube */
| void bdd_free | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [Deletes the BDD of f.]
SideEffects []
Definition at line 296 of file cuPort.c.
00297 { 00298 if (f == NULL) { 00299 fail("bdd_free: trying to free a NULL bdd_t"); 00300 } 00301 00302 if (f->free == TRUE) { 00303 fail("bdd_free: trying to free a freed bdd_t"); 00304 } 00305 00306 Cudd_RecursiveDeref(f->mgr,f->node); 00307 /* This is a bit overconservative. */ 00308 f->node = NULL; 00309 f->mgr = NULL; 00310 f->free = TRUE; 00311 FREE(f); 00312 return; 00313 00314 } /* end of bdd_free */
| int bdd_gen_decomp | ( | bdd_t * | f, | |
| bdd_partition_type_t | partType, | |||
| bdd_t *** | conjArray | |||
| ) |
Function********************************************************************
Synopsis [Computes 2 partitions of a function.]
Description [Computes 2 partitions of a function. Method based on DAC98 - Ravi, Somenzi. Picks decomposition points and replaces one child in each conjunct with 1 (0). returns 2 conjuncts(disjuncts).]
SideEffects []
Definition at line 6156 of file cuPort.c.
06157 { 06158 DdNode **ddArray = NULL; 06159 int i, num = 0; 06160 bdd_t *result; 06161 06162 switch (partType) { 06163 case BDD_CONJUNCTS: 06164 num = Cudd_bddGenConjDecomp(f->mgr, f->node, &ddArray); 06165 break; 06166 case BDD_DISJUNCTS: 06167 num = Cudd_bddGenDisjDecomp(f->mgr, f->node, &ddArray); 06168 break; 06169 } 06170 if ((ddArray == NULL) || (!num)) { 06171 return 0; 06172 } 06173 06174 *conjArray = ALLOC(bdd_t *, num); 06175 if ((*conjArray) == NULL) goto outOfMem; 06176 for (i = 0; i < num; i++) { 06177 result = ALLOC(bdd_t, 1); 06178 if (result == NULL) { 06179 FREE(*conjArray); 06180 goto outOfMem; 06181 } 06182 result->mgr = f->mgr; 06183 result->node = ddArray[i]; 06184 result->free = FALSE; 06185 (*conjArray)[i] = result; 06186 } 06187 FREE(ddArray); 06188 return (num); 06189 06190 outOfMem: 06191 for (i = 0; i < num; i++) { 06192 Cudd_RecursiveDeref((DdManager *)f->mgr,(DdNode *)ddArray[i]); 06193 } 06194 FREE(ddArray); 06195 return(0); 06196 06197 } /* end of bdd_gen_decomp */
| bdd_external_hooks* bdd_get_external_hooks | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Accesses the external_hooks field of the manager.]
SideEffects []
Definition at line 3168 of file cuPort.c.
03169 { 03170 return((bdd_external_hooks *)(((DdManager *)mgr)->hooks)); 03171 03172 } /* end of bdd_get_external_hooks */
| int bdd_get_free | ( | bdd_t * | f | ) |
| bdd_variableId bdd_get_id_from_level | ( | bdd_manager * | mgr, | |
| long | level | |||
| ) |
Function********************************************************************
Synopsis [Gets the id variable for one level in the BDD.]
SideEffects []
Definition at line 3514 of file cuPort.c.
03515 { 03516 int result; 03517 result = Cudd_ReadInvPerm((DdManager *) mgr, (int)level); 03518 return(result); 03519 03520 } /* end of bdd_get_id_from_level */
| int bdd_get_level_from_id | ( | bdd_manager * | mgr, | |
| int | id | |||
| ) |
Function********************************************************************
Synopsis [Gets the level of the ith variable in the manager ]
SideEffects []
Definition at line 4137 of file cuPort.c.
04138 { 04139 int level; 04140 level = Cudd_ReadPerm((DdManager *)mgr, id); 04141 return(level); 04142 04143 } /* end of bdd_get_level_from_id */
| bdd_manager* bdd_get_manager | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [Returns the node of the BDD.]
SideEffects [Sets is_complemented.]
Definition at line 2614 of file cuPort.c.
02617 { 02618 if (Cudd_IsComplement(f->node)) { 02619 *is_complemented = TRUE; 02620 return(Cudd_Regular(f->node)); 02621 } 02622 *is_complemented = FALSE; 02623 return(f->node); 02624 02625 } /* end of bdd_get_node */
| bdd_package_type_t bdd_get_package_name | ( | void | ) |
Function********************************************************************
Synopsis [Obtains the support of the BDD.]
SideEffects []
Definition at line 2636 of file cuPort.c.
02637 { 02638 int i, size, *support; 02639 var_set_t *result; 02640 02641 size = (unsigned int)Cudd_ReadSize((DdManager *)f->mgr); 02642 support = Cudd_SupportIndex(f->mgr,f->node); 02643 if (support == NULL) return(NULL); 02644 02645 result = var_set_new((int) f->mgr->size); 02646 for (i = 0; i < size; i++) { 02647 if (support[i]) 02648 var_set_set_elt(result, i); 02649 } 02650 FREE(support); 02651 02652 return(result); 02653 02654 } /* end of bdd_get_support */
| bdd_t* bdd_get_variable | ( | bdd_manager * | mgr, | |
| bdd_variableId | variable_ID | |||
| ) |
Function********************************************************************
Synopsis [Returns the BDD representing the variable with given ID.]
SideEffects []
Definition at line 253 of file cuPort.c.
00254 { 00255 DdNode *var; 00256 DdManager *dd = (DdManager *) mgr; 00257 DdNode *one = DD_ONE(dd); 00258 00259 if (variable_ID >= CUDD_MAXINDEX -1) return(NULL); 00260 do { 00261 dd->reordered = 0; 00262 var = cuddUniqueInter(dd,(int)variable_ID,one,Cudd_Not(one)); 00263 } while (dd->reordered == 1); 00264 00265 if (var == NULL) return((bdd_t *)NULL); 00266 cuddRef(var); 00267 return(bdd_construct_bdd_t(dd,var)); 00268 00269 } /* end of bdd_get_variable */
Function********************************************************************
Synopsis [Obtains the array of indices of an array of variables.]
SideEffects []
Definition at line 2711 of file cuPort.c.
02712 { 02713 int i; 02714 int index; 02715 bdd_t *var; 02716 array_t *result = array_alloc(int,array_n(var_array)); 02717 02718 for (i = 0; i < array_n(var_array); i++) { 02719 var = array_fetch(bdd_t *, var_array, i); 02720 index = Cudd_Regular(var->node)->index; 02721 (void) array_insert_last(int, result, index); 02722 } 02723 return(result); 02724 02725 } /* end of bdd_get_varids */
| bdd_node* bdd_indices_to_cube | ( | bdd_manager * | mgr, | |
| int * | idArray, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [Builds a cube of BDD variables from an array of indices.]
Description [Builds a cube of BDD variables from an array of indices. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [bdd_bdd_compute_cube]
Definition at line 4446 of file cuPort.c.
04447 { 04448 DdNode *result; 04449 result = Cudd_IndicesToCube((DdManager *)mgr, idArray, n); 04450 04451 return(result); 04452 04453 } /* end of bdd_indices_to_cube */
Function********************************************************************
Synopsis [Returns a BDD included in the intersection of f and g.]
SideEffects []
Definition at line 2388 of file cuPort.c.
02391 { 02392 DdNode *result; 02393 02394 /* Make sure both operands belong to the same manager. */ 02395 assert(f->mgr == g->mgr); 02396 02397 result = Cudd_bddIntersect(f->mgr,f->node,g->node); 02398 if (result == NULL) return(NULL); 02399 cuddRef(result); 02400 return(bdd_construct_bdd_t(f->mgr,result)); 02401 02402 } /* end of bdd_intersects */
| int bdd_is_complement | ( | bdd_node * | f | ) |
Function********************************************************************
Synopsis [Returns 1 if the bdd_node is complemented. 0 otherwise.]
Description [Returns 1 if the bdd_node is complemented. 0 otherwise.]]
SideEffects [none]
Definition at line 5447 of file cuPort.c.
05448 { 05449 return(Cudd_IsComplement((DdNode *)f)); 05450 05451 } /* end of bdd_is_complement */
| int bdd_is_constant | ( | bdd_node * | f | ) |
Function********************************************************************
Synopsis [Returns 1 if the bdd_node is a constant; 0 otherwise.]
Description [Returns 1 if the bdd_node is a constant; 0 otherwise.]
SideEffects [none]
Definition at line 5430 of file cuPort.c.
05431 { 05432 return(Cudd_IsConstant((DdNode *)f)); 05433 05434 } /* end of bdd_is_constant */
Function********************************************************************
Synopsis [Returns TRUE if the argument BDD is a cube; FALSE otherwise.]
SideEffects []
| int bdd_is_lazy_sift | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Checks whether lazy sifting is on.]
SideEffects [none]
Definition at line 7381 of file cuPort.c.
07382 { 07383 Cudd_ReorderingType method; 07384 07385 Cudd_ReorderingStatus((DdManager *) mgr, &method); 07386 if (method == CUDD_REORDER_LAZY_SIFT) 07387 return(1); 07388 return(0); 07389 07390 } /* end of bdd_is_lazy_sift */
| int bdd_is_ns_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is next state.]
SideEffects [none]
Definition at line 7163 of file cuPort.c.
07164 { 07165 return Cudd_bddIsNsVar((DdManager *) mgr, index); 07166 07167 } /* end of bdd_is_ns_var */
| int bdd_is_pi_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is primary input.]
SideEffects [none]
Definition at line 7133 of file cuPort.c.
07134 { 07135 return Cudd_bddIsPiVar((DdManager *) mgr, index); 07136 07137 } /* end of bdd_is_pi_var */
| int bdd_is_ps_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is present state.]
SideEffects [none]
Definition at line 7148 of file cuPort.c.
07149 { 07150 return Cudd_bddIsPsVar((DdManager *) mgr, index); 07151 07152 } /* end of bdd_is_ps_var */
Function********************************************************************
Synopsis [Checks whether a BDD is a support of f.]
SideEffects []
Definition at line 2665 of file cuPort.c.
02666 { 02667 return(bdd_is_support_var_id(f, bdd_top_var_id(var))); 02668 02669 } /* end of bdd_is_support_var */
| int bdd_is_support_var_id | ( | bdd_t * | f, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Checks whether a BDD index is a support of f.]
SideEffects []
Definition at line 2680 of file cuPort.c.
02681 { 02682 DdNode *support, *scan; 02683 02684 support = Cudd_Support(f->mgr,f->node); 02685 if (support == NULL) return(-1); 02686 cuddRef(support); 02687 02688 scan = support; 02689 while (!cuddIsConstant(scan)) { 02690 if (scan->index == index) { 02691 Cudd_RecursiveDeref(f->mgr,support); 02692 return(1); 02693 } 02694 scan = cuddT(scan); 02695 } 02696 Cudd_RecursiveDeref(f->mgr,support); 02697 02698 return(0); 02699 02700 } /* end of bdd_is_support_var_id */
Function********************************************************************
Synopsis [Checks a BDD for tautology.]
SideEffects []
| int bdd_is_var_hard_group | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is set to be a hard group.]
Description [Checks whether a variable is set to be a hard group. This function is used for lazy sifting.]
SideEffects [none]
Definition at line 7289 of file cuPort.c.
07290 { 07291 return Cudd_bddIsVarHardGroup((DdManager *) mgr, index); 07292 07293 } /* end of bdd_is_var_hard_group */
| int bdd_is_var_to_be_grouped | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is set to be grouped.]
Description [Checks whether a variable is set to be grouped. This function is used for lazy sifting.]
SideEffects [none]
Definition at line 7271 of file cuPort.c.
07272 { 07273 return Cudd_bddIsVarToBeGrouped((DdManager *) mgr, index); 07274 07275 } /* end of bdd_is_var_to_be_grouped */
| int bdd_is_var_to_be_ungrouped | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Sets a variable to be ungrouped.]
Description [Sets a variable to be ungrouped. This function is used for lazy sifting.]
SideEffects [none]
Definition at line 7307 of file cuPort.c.
07308 { 07309 return Cudd_bddIsVarToBeUngrouped((DdManager *) mgr, index); 07310 07311 } /* end of bdd_is_var_to_be_ungrouped */
| bdd_t* bdd_ite | ( | bdd_t * | i, | |
| bdd_t * | t, | |||
| bdd_t * | e, | |||
| boolean | i_phase, | |||
| boolean | t_phase, | |||
| boolean | e_phase | |||
| ) |
Function********************************************************************
Synopsis [ITE.]
SideEffects []
Definition at line 1481 of file cuPort.c.
01488 { 01489 DdNode *newi,*newt,*newe,*ite; 01490 01491 /* Make sure both bdds belong to the same mngr */ 01492 assert(i->mgr == t->mgr); 01493 assert(i->mgr == e->mgr); 01494 01495 /* Modify the phases of the operands according to the parameters */ 01496 if (!i_phase) { 01497 newi = Cudd_Not(i->node); 01498 } else { 01499 newi = i->node; 01500 } 01501 if (!t_phase) { 01502 newt = Cudd_Not(t->node); 01503 } else { 01504 newt = t->node; 01505 } 01506 if (!e_phase) { 01507 newe = Cudd_Not(e->node); 01508 } else { 01509 newe = e->node; 01510 } 01511 01512 /* Perform the ITE operation */ 01513 ite = Cudd_bddIte(i->mgr,newi,newt,newe); 01514 if (ite == NULL) return(NULL); 01515 cuddRef(ite); 01516 return(bdd_construct_bdd_t(i->mgr,ite)); 01517 01518 } /* end of bdd_ite */
| int bdd_iter_decomp | ( | bdd_t * | f, | |
| bdd_partition_type_t | partType, | |||
| bdd_t *** | conjArray | |||
| ) |
Function********************************************************************
Synopsis [Computes 2 partitions of a function.]
Description [Computes 2 partitions of a function. Picks a subset of a function and minimizes the rest of the function w.r.t. the subset. Performs this iteratively. returns 2 conjuncts(disjuncts).]
SideEffects []
Definition at line 6324 of file cuPort.c.
06325 { 06326 DdNode **ddArray; 06327 int i, num = 0; 06328 bdd_t *result; 06329 06330 switch (partType) { 06331 case BDD_CONJUNCTS: 06332 num = Cudd_bddIterConjDecomp(f->mgr, f->node, &ddArray); 06333 break; 06334 case BDD_DISJUNCTS: 06335 num = Cudd_bddIterDisjDecomp(f->mgr, f->node, &ddArray); 06336 break; 06337 } 06338 if ((ddArray == NULL) || (!num)) { 06339 return 0; 06340 } 06341 06342 *conjArray = ALLOC(bdd_t *, num); 06343 if ((*conjArray) == NULL) goto outOfMem; 06344 for (i = 0; i < num; i++) { 06345 result = ALLOC(bdd_t, 1); 06346 if (result == NULL) { 06347 FREE(*conjArray); 06348 goto outOfMem; 06349 } 06350 result->mgr = f->mgr; 06351 result->node = ddArray[i]; 06352 result->free = FALSE; 06353 (*conjArray)[i] = result; 06354 } 06355 FREE(ddArray); 06356 return (num); 06357 06358 outOfMem: 06359 for (i = 0; i < num; i++) { 06360 Cudd_RecursiveDeref((DdManager *)f->mgr,(DdNode *)ddArray[i]); 06361 } 06362 FREE(ddArray); 06363 return(0); 06364 06365 } /* end of bdd_iter_decomp */
Function********************************************************************
Synopsis [Tests for containment of f in g.]
SideEffects [None: No new nodes are created.]
Definition at line 2458 of file cuPort.c.
02463 { 02464 DdNode *newf, *newg; 02465 02466 /* Make sure both operands belong to the same manager. */ 02467 assert(f->mgr == g->mgr); 02468 newf = Cudd_NotCond(f->node, !f_phase); 02469 newg = Cudd_NotCond(g->node, !g_phase); 02470 02471 return(Cudd_bddLeq(f->mgr,newf,newg)); 02472 02473 } /* end of bdd_leq */
Function********************************************************************
Synopsis [Tests for containment of f in g.]
SideEffects []
Definition at line 2513 of file cuPort.c.
02518 { 02519 int i; 02520 bdd_t *g; 02521 boolean result; 02522 02523 arrayForEachItem(bdd_t *, g_array, i, g) { 02524 result = bdd_leq(f, g, f_phase, g_phase); 02525 if (g_phase) { 02526 if (!result) 02527 return(0); 02528 } else { 02529 if (result) 02530 return(1); 02531 } 02532 } 02533 if (g_phase) 02534 return(1); 02535 else 02536 return(0); 02537 02538 } /* end of bdd_leq_array */
| boolean bdd_lequal_mod_care_set | ( | bdd_t * | f, | |
| bdd_t * | g, | |||
| boolean | f_phase, | |||
| boolean | g_phase, | |||
| bdd_t * | careSet | |||
| ) |
Function********************************************************************
Synopsis [Implication check with don't care conditions.]
Description [Returns 1 if f implies g wherever careSet is 1.]
SideEffects [None: No new nodes are created.]
Definition at line 2486 of file cuPort.c.
02492 { 02493 DdNode *newf, *newg; 02494 02495 /* Make sure all operands belong to the same manager. */ 02496 assert(f->mgr == g->mgr && f->mgr == careSet->mgr); 02497 newf = Cudd_NotCond(f->node, !f_phase); 02498 newg = Cudd_NotCond(g->node, !g_phase); 02499 02500 return(Cudd_bddLeqUnless(f->mgr, newf, newg, Cudd_Not(careSet->node))); 02501 02502 } /* end of bdd_lequal_mod_care_set */
| bdd_node* bdd_make_bdd_from_zdd_cover | ( | bdd_manager * | mgr, | |
| bdd_node * | node | |||
| ) |
Function********************************************************************
Synopsis [Converts a ZDD cover to a BDD graph.]
SideEffects []
Definition at line 6880 of file cuPort.c.
06881 { 06882 return((bdd_node *)Cudd_MakeBddFromZddCover((DdManager *)mgr, (DdNode *)node)); 06883 06884 } /* end of bdd_make_bdd_from_zdd_cover */
Function********************************************************************
Synopsis [Restrict operator as described in Coudert et al. ICCAD90.]
Description [Restrict operator as described in Coudert et al. ICCAD90. Always returns a BDD not larger than the input f if successful; NULL otherwise.]
SideEffects [none]
Definition at line 1533 of file cuPort.c.
01534 { 01535 DdNode *result; 01536 bdd_t *output; 01537 01538 /* Make sure both operands belong to the same manager. */ 01539 assert(f->mgr == c->mgr); 01540 01541 result = Cudd_bddRestrict(f->mgr, f->node, c->node); 01542 if (result == NULL) return(NULL); 01543 cuddRef(result); 01544 01545 output = bdd_construct_bdd_t(f->mgr,result); 01546 return(output); 01547 01548 } /* end of bdd_minimize */
Function********************************************************************
Synopsis [Restrict operator as described in Coudert et al. ICCAD90.]
Description [Restrict operator as described in Coudert et al. ICCAD90. Always returns a BDD not larger than the input f if successful; NULL otherwise.]
SideEffects [none]
Definition at line 1563 of file cuPort.c.
01564 { 01565 bdd_t *operand; 01566 DdNode *result, *temp; 01567 int i; 01568 01569 Cudd_Ref(result = f->node); 01570 01571 for (i = 0; i < array_n(bddArray); i++) { 01572 operand = array_fetch(bdd_t *, bddArray, i); 01573 temp = Cudd_bddRestrict(f->mgr, result, operand->node); 01574 if (temp == NULL) { 01575 Cudd_RecursiveDeref(f->mgr, result); 01576 return(NULL); 01577 } 01578 cuddRef(temp); 01579 Cudd_RecursiveDeref(f->mgr, result); 01580 result = temp; 01581 } 01582 01583 return(bdd_construct_bdd_t(f->mgr,result)); 01584 01585 } /* end of bdd_minimize_array */
| bdd_t* bdd_multiway_and | ( | bdd_manager * | manager, | |
| array_t * | bddArray | |||
| ) |
Function********************************************************************
Synopsis [Takes the and of an array of functions.]
SideEffects [None]
Definition at line 445 of file cuPort.c.
00446 { 00447 DdManager *mgr; 00448 bdd_t *operand; 00449 DdNode *result, *temp; 00450 int i; 00451 00452 mgr = (DdManager *)manager; 00453 00454 Cudd_Ref(result = DD_ONE(mgr)); 00455 00456 for (i = 0; i < array_n(bddArray); i++) { 00457 operand = array_fetch(bdd_t *, bddArray, i); 00458 temp = Cudd_bddAnd(mgr, result, operand->node); 00459 if (temp == NULL) { 00460 Cudd_RecursiveDeref(mgr, result); 00461 return(NULL); 00462 } 00463 cuddRef(temp); 00464 Cudd_RecursiveDeref(mgr, result); 00465 result = temp; 00466 } 00467 00468 return(bdd_construct_bdd_t(mgr,result)); 00469 00470 } /* end of bdd_multiway_and */
| bdd_t* bdd_multiway_or | ( | bdd_manager * | manager, | |
| array_t * | bddArray | |||
| ) |
Function********************************************************************
Synopsis [Takes the or of an array of functions.]
SideEffects []
Definition at line 481 of file cuPort.c.
00482 { 00483 DdManager *mgr; 00484 bdd_t *operand; 00485 DdNode *result, *temp; 00486 int i; 00487 00488 mgr = (DdManager *)manager; 00489 Cudd_Ref(result = Cudd_Not(DD_ONE(mgr))); 00490 00491 for (i = 0; i < array_n(bddArray); i++) { 00492 operand = array_fetch(bdd_t *, bddArray, i); 00493 temp = Cudd_bddOr(mgr, result, operand->node); 00494 if (temp == NULL) { 00495 Cudd_RecursiveDeref(mgr, result); 00496 return(NULL); 00497 } 00498 cuddRef(temp); 00499 Cudd_RecursiveDeref(mgr, result); 00500 result = temp; 00501 } 00502 00503 return(bdd_construct_bdd_t(mgr,result)); 00504 00505 } /* end of bdd_multiway_or */
| bdd_t* bdd_multiway_xor | ( | bdd_manager * | manager, | |
| array_t * | bddArray | |||
| ) |
Function********************************************************************
Synopsis [Takes the xor of an array of functions.]
SideEffects [None]
Definition at line 516 of file cuPort.c.
00517 { 00518 DdManager *mgr; 00519 bdd_t *operand; 00520 DdNode *result, *temp; 00521 int i; 00522 00523 mgr = (DdManager *)manager; 00524 00525 Cudd_Ref(result = Cudd_Not(DD_ONE(mgr))); 00526 00527 for (i = 0; i < array_n(bddArray); i++) { 00528 operand = array_fetch(bdd_t *, bddArray, i); 00529 temp = Cudd_bddXor(mgr, result, operand->node); 00530 if (temp == NULL) { 00531 Cudd_RecursiveDeref(mgr, result); 00532 return(NULL); 00533 } 00534 cuddRef(temp); 00535 Cudd_RecursiveDeref(mgr, result); 00536 result = temp; 00537 } 00538 00539 return(bdd_construct_bdd_t(mgr,result)); 00540 00541 } /* end of bdd_multiway_xor */
Function********************************************************************
Synopsis [Builds a group of variables that should stay adjacent during reordering.]
Description [Builds a group of variables that should stay adjacent during reordering. The group is made up of n variables. The first variable in the group is f. The other variables are the n-1 variables following f in the order at the time of invocation of this function. Returns a handle to the variable group if successful; NULL otherwise.]
SideEffects [Modifies the variable tree.]
Definition at line 3577 of file cuPort.c.
03578 { 03579 DdManager *manager; 03580 DdNode *node; 03581 MtrNode *group; 03582 int index; 03583 03584 manager = (DdManager *) f->mgr; 03585 node = Cudd_Regular(f->node); 03586 index = node->index; 03587 if (index == CUDD_MAXINDEX) 03588 return(NULL); 03589 group = Cudd_MakeTreeNode(manager, index, n, MTR_DEFAULT); 03590 03591 return((bdd_block *) group); 03592 03593 } /* end of bdd_new_var_block */
| int bdd_node_read_index | ( | bdd_node * | f | ) |
Function********************************************************************
Synopsis [Returns the index of bdd_node f.]
Description [Returns the index of bdd_node f.]
SideEffects []
SeeAlso [bdd_top_var_id]
Definition at line 5716 of file cuPort.c.
05717 { 05718 return(Cudd_NodeReadIndex((DdNode *)f)); 05719 05720 } /* end of bdd_node_read_index */
| int bdd_node_size | ( | bdd_node * | f | ) |
Function********************************************************************
Synopsis [Computes the number of nodes of a BDD.]
SideEffects []
Definition at line 3103 of file cuPort.c.
03104 { 03105 return(Cudd_DagSize((DdNode *) f)); 03106 03107 } /* end of bdd_node_size */
Function********************************************************************
Synopsis [Negation.]
SideEffects []
Function********************************************************************
Synopsis [Returns the complement of a bdd_node.]
Description [Returns the complement of a bdd_node.]
SideEffects []
SeeAlso [bdd_not]
| unsigned int bdd_num_vars | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns the number of variables in the manager.]
SideEffects []
Definition at line 2736 of file cuPort.c.
02737 { 02738 unsigned int size; 02739 size = (unsigned int)Cudd_ReadSize((DdManager *)mgr); 02740 return(size); 02741 02742 } /* end of bdd_num_vars */
| int bdd_num_zdd_vars | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns the number of ZDD variables.]
Description [Returns the number of ZDD variables.]
SideEffects [none]
| bdd_t* bdd_one | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns the one BDD.]
SideEffects []
Function********************************************************************
Synopsis [Or of two BDDs.]
SideEffects []
Definition at line 1966 of file cuPort.c.
01971 { 01972 DdNode *newf,*newg,*forg; 01973 bdd_t *result; 01974 01975 /* Make sure both bdds belong to the same mngr */ 01976 assert(f->mgr == g->mgr); 01977 01978 /* Modify the phases of the operands according to the parameters */ 01979 if (f_phase) { 01980 newf = Cudd_Not(f->node); 01981 } else { 01982 newf = f->node; 01983 } 01984 if (g_phase) { 01985 newg = Cudd_Not(g->node); 01986 } else { 01987 newg = g->node; 01988 } 01989 01990 /* Perform the OR operation */ 01991 forg = Cudd_bddAnd(f->mgr,newf,newg); 01992 if (forg == NULL) return(NULL); 01993 forg = Cudd_Not(forg); 01994 cuddRef(forg); 01995 result = bdd_construct_bdd_t(f->mgr,forg); 01996 01997 return(result); 01998 01999 } /* end of bdd_or */
| array_t* bdd_pairwise_and | ( | bdd_manager * | manager, | |
| array_t * | bddArray1, | |||
| array_t * | bddArray2 | |||
| ) |
Function********************************************************************
Synopsis [Takes the pairwise and of two arrays of bdds of the same length.]
SideEffects [required]
Definition at line 604 of file cuPort.c.
00605 { 00606 DdManager *mgr; 00607 bdd_t *op1, *op2; 00608 bdd_t *unit; 00609 DdNode *result; 00610 array_t *resultArray; 00611 int i; 00612 00613 mgr = (DdManager *)manager; 00614 00615 if (array_n(bddArray1) != array_n(bddArray2)) { 00616 (void) fprintf(stderr, 00617 "bdd_pairwise_or: Arrays of different lengths.\n"); 00618 return(NULL); 00619 } 00620 00621 resultArray = array_alloc(bdd_t *, array_n(bddArray1)); 00622 for (i = 0; i < array_n(bddArray1); i++) { 00623 op1 = array_fetch(bdd_t *, bddArray1, i); 00624 op2 = array_fetch(bdd_t *, bddArray2, i); 00625 00626 result = Cudd_bddAnd(mgr, op1->node, op2->node); 00627 if (result == NULL) { 00628 int j; 00629 bdd_t *item; 00630 for (j = 0; j < array_n(resultArray); j++) { 00631 item = array_fetch(bdd_t *, resultArray, j); 00632 bdd_free(item); 00633 } 00634 array_free(resultArray); 00635 return((array_t *)NULL); 00636 } 00637 cuddRef(result); 00638 00639 unit = bdd_construct_bdd_t(mgr, result); 00640 array_insert(bdd_t *, resultArray, i, unit); 00641 } 00642 00643 return(resultArray); 00644 00645 } /* end of bdd_pairwise_and */
| array_t* bdd_pairwise_or | ( | bdd_manager * | manager, | |
| array_t * | bddArray1, | |||
| array_t * | bddArray2 | |||
| ) |
Function********************************************************************
Synopsis [Takes the pairwise or of two arrays of bdds of the same length.]
SideEffects [None]
Definition at line 552 of file cuPort.c.
00553 { 00554 DdManager *mgr; 00555 bdd_t *op1, *op2; 00556 bdd_t *unit; 00557 DdNode *result; 00558 array_t *resultArray; 00559 int i; 00560 00561 mgr = (DdManager *)manager; 00562 00563 if (array_n(bddArray1) != array_n(bddArray2)) { 00564 (void) fprintf(stderr, 00565 "bdd_pairwise_or: Arrays of different lengths.\n"); 00566 return(NULL); 00567 } 00568 00569 resultArray = array_alloc(bdd_t *, array_n(bddArray1)); 00570 for (i = 0; i < array_n(bddArray1); i++) { 00571 op1 = array_fetch(bdd_t *, bddArray1, i); 00572 op2 = array_fetch(bdd_t *, bddArray2, i); 00573 00574 result = Cudd_bddOr(mgr, op1->node, op2->node); 00575 if (result == NULL) { 00576 int j; 00577 bdd_t *item; 00578 for (j = 0; j < array_n(resultArray); j++) { 00579 item = array_fetch(bdd_t *, resultArray, j); 00580 bdd_free(item); 00581 } 00582 array_free(resultArray); 00583 return((array_t *)NULL); 00584 } 00585 cuddRef(result); 00586 00587 unit = bdd_construct_bdd_t(mgr, result); 00588 array_insert(bdd_t *, resultArray, i, unit); 00589 } 00590 00591 return(resultArray); 00592 00593 } /* end of bdd_pairwise_or */
| array_t* bdd_pairwise_xor | ( | bdd_manager * | manager, | |
| array_t * | bddArray1, | |||
| array_t * | bddArray2 | |||
| ) |
Function********************************************************************
Synopsis [Takes the pairwise xor of two arrays of bdds of the same length.]
SideEffects [required]
Definition at line 656 of file cuPort.c.
00657 { 00658 DdManager *mgr; 00659 bdd_t *op1, *op2; 00660 bdd_t *unit; 00661 DdNode *result; 00662 array_t *resultArray; 00663 int i; 00664 00665 mgr = (DdManager *)manager; 00666 00667 if (array_n(bddArray1) != array_n(bddArray2)) { 00668 (void) fprintf(stderr, 00669 "bdd_pairwise_or: Arrays of different lengths.\n"); 00670 return(NULL); 00671 } 00672 00673 resultArray = array_alloc(bdd_t *, array_n(bddArray1)); 00674 for (i = 0; i < array_n(bddArray1); i++) { 00675 op1 = array_fetch(bdd_t *, bddArray1, i); 00676 op2 = array_fetch(bdd_t *, bddArray2, i); 00677 00678 result = Cudd_bddXor(mgr, op1->node, op2->node); 00679 if (result == NULL) { 00680 int j; 00681 bdd_t *item; 00682 for (j = 0; j < array_n(resultArray); j++) { 00683 item = array_fetch(bdd_t *, resultArray, j); 00684 bdd_free(item); 00685 } 00686 array_free(resultArray); 00687 return((array_t *)NULL); 00688 } 00689 cuddRef(result); 00690 00691 unit = bdd_construct_bdd_t(mgr, result); 00692 array_insert(bdd_t *, resultArray, i, unit); 00693 } 00694 00695 return(resultArray); 00696 00697 } /* end of bdd_pairwise_xor */
Function********************************************************************
Synopsis [Pick a random minterm from the onset of f.]
SideEffects []
Definition at line 4701 of file cuPort.c.
04702 { 04703 DdNode **vars, *minterm; 04704 int i, n; 04705 04706 n = array_n(varsArray); 04707 vars = ALLOC(DdNode *, n); 04708 if (vars == NIL(DdNode *)) return NIL(bdd_t); 04709 for (i = 0; i < n; i++) { 04710 bdd_t *var = array_fetch(bdd_t *, varsArray, i); 04711 assert(f->mgr == var->mgr); 04712 vars[i] = var->node; 04713 } 04714 minterm = Cudd_bddPickOneMinterm(f->mgr, f->node, vars, n); 04715 cuddRef(minterm); 04716 FREE(vars); 04717 if (minterm == NIL(DdNode)) return NIL(bdd_t); 04718 return bdd_construct_bdd_t(f->mgr,minterm); 04719 04720 } /* end of bdd_pick_one_minterm */
| void* bdd_pointer | ( | bdd_t * | f | ) |
| void bdd_print | ( | bdd_t * | f | ) |
| int bdd_print_apa_minterm | ( | FILE * | fp, | |
| bdd_t * | f, | |||
| int | nvars, | |||
| int | precision | |||
| ) |
Function********************************************************************
Synopsis [Prints the minterns of f in the file stream fp. Precision can be specified in the last argument. Result is 1 if printing is successful, else 0.]
SideEffects []
| int bdd_print_cover | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [Prints cover of the bdd.]
Description [.]
SideEffects []
| int bdd_print_minterm | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [Prints minterms of the bdd.]
Description [.]
SideEffects []
| void bdd_print_stats | ( | bdd_manager * | mgr, | |
| FILE * | file | |||
| ) |
Function********************************************************************
Synopsis [Prints statistics about the package.]
SideEffects []
Definition at line 2768 of file cuPort.c.
02769 { 02770 Cudd_PrintInfo((DdManager *)mgr, file); 02771 02772 /* Print some guidance to the parameters */ 02773 (void) fprintf(file, "\nMore detailed information about the semantics "); 02774 (void) fprintf(file, "and values of these parameters\n"); 02775 (void) fprintf(file, "can be found in the documentation about the CU "); 02776 (void) fprintf(file, "Decision Diagram Package.\n"); 02777 02778 return; 02779 02780 } /* end of bdd_print_stats */
| bdd_node* bdd_priority_select | ( | bdd_manager * | mgr, | |
| bdd_node * | R, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y, | |||
| bdd_node ** | z, | |||
| bdd_node * | Pi, | |||
| int | n, | |||
| bdd_node *(*)(bdd_manager *, int, bdd_node **, bdd_node **, bdd_node **) | Pifunc | |||
| ) |
Function********************************************************************
Synopsis [Selects pairs from R using a priority function.]
Description [Selects pairs from a relation R(x,y) (given as a BDD) in such a way that a given x appears in one pair only. Uses a priority function to determine which y should be paired to a given x. bdd_priority_select returns a pointer to the selected function if successful; NULL otherwise. Three of the arguments--x, y, and z--are vectors of BDD variables. The first two are the variables on which R depends. The third is a vector of auxiliary variables, used during the computation. This vector is optional. If a NULL value is passed instead, bdd_priority_select will create the working variables on the fly. The sizes of x and y (and z if it is not NULL) should equal n. The priority function Pi can be passed as a BDD, or can be built by Cudd_PrioritySelect. If NULL is passed instead of a bdd_node *, parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the priority function. (Pifunc is a pointer to a C function.) If Pi is not NULL, then Pifunc is ignored. Pifunc should have the same interface as the standard priority functions (e.g., bdd_dxygtdxz).]
SideEffects [If called with z == NULL, will create new variables in the manager.]
SeeAlso [bdd_dxygtdxz bdd_xgty]
Definition at line 5932 of file cuPort.c.
05941 { 05942 DdNode *result; 05943 result = Cudd_PrioritySelect((DdManager *)mgr,(DdNode *)R, 05944 (DdNode **)x,(DdNode **)y, 05945 (DdNode **)z,(DdNode *)Pi, 05946 n,(DdNode *(*)(DdManager *, int, DdNode **, 05947 DdNode **, DdNode **))Pifunc); 05948 return (bdd_node *)result; 05949 05950 } /* end of bdd_priority_select */
| int bdd_ptrhash | ( | bdd_t * | f, | |
| int | size | |||
| ) |
Function********************************************************************
Synopsis [Returns the hash value of a bdd.]
SideEffects []
| bdd_node* bdd_read_background | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Read the background value of BDD manager.]
Description [Read the background value of BDD manager.]
SideEffects []
Definition at line 5980 of file cuPort.c.
05981 { 05982 DdNode *result; 05983 result = Cudd_ReadBackground((DdManager *)mgr); 05984 return (bdd_node *)result; 05985 05986 } /* end of bdd_read_background */
| BDD_VALUE_TYPE bdd_read_epsilon | ( | bdd_manager * | mgr | ) |
| bdd_node* bdd_read_logic_zero | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Reads constant logic zero bdd_node.]
SideEffects [bdd_zero]
Definition at line 4198 of file cuPort.c.
04199 { 04200 DdNode *result; 04201 result = Cudd_ReadLogicZero((DdManager *)mgr); 04202 04203 return(result); 04204 04205 } /* end of bdd_read_logic_zero */
Function********************************************************************
Synopsis [Reads the next field of a DdNode.]
Description [Reads the next field of a DdNode.]
SideEffects []
Definition at line 5733 of file cuPort.c.
05734 { 05735 return(((DdNode *)f)->next); 05736 05737 } /* end of bdd_read_next */
| int bdd_read_next_reordering | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns the threshold for the next dynamic reordering.]
SideEffects []
Definition at line 4943 of file cuPort.c.
04944 { 04945 return(Cudd_ReadNextReordering((DdManager *)mgr)); 04946 04947 } /* end of bdd_read_next_reordering */
| int bdd_read_node_count | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Reports the number of nodes in the manager.]
SideEffects []
Definition at line 6444 of file cuPort.c.
06445 { 06446 return(Cudd_ReadNodeCount((DdManager *)mgr)); 06447 06448 } /* end of bdd_read_node_count */
| bdd_node* bdd_read_one | ( | bdd_manager * | mgr | ) |
| int bdd_read_pair_index | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Reads a corresponding pair index for a given index.]
Description [Reads a corresponding pair index for a given index. These pair indices are present and next state variable.]
SideEffects [none]
Definition at line 7199 of file cuPort.c.
07200 { 07201 return Cudd_bddReadPairIndex((DdManager *) mgr, index); 07202 07203 } /* end of bdd_read_pair_index */
| int bdd_read_peak_live_node | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns the peak live node count.]
SideEffects []
Definition at line 7073 of file cuPort.c.
07074 { 07075 return(Cudd_ReadPeakLiveNodeCount((DdManager *) mgr)); 07076 07077 } /* end of bdd_read_peak_live_node */
| long bdd_read_peak_memory | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns the peak memory in use.]
SideEffects []
Definition at line 7058 of file cuPort.c.
07059 { 07060 return((long) Cudd_ReadMemoryInUse((DdManager *) mgr)); 07061 07062 } /* end of bdd_read_peak_memory */
| bdd_node* bdd_read_plus_infinity | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Reads the plus inifinity field of the BDD manager.]
Description [Reads the plus inifinity field of the BDD manager.]
SideEffects []
Definition at line 5894 of file cuPort.c.
05895 { 05896 DdNode *result; 05897 result = Cudd_ReadPlusInfinity((DdManager *)mgr); 05898 return (bdd_node *)result; 05899 05900 } /* end of bdd_read_plus_infinity */
| int bdd_read_reordered_field | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Read the reordered field of the manager.]
Description [Read the reordered field of the manager.]
SideEffects []
| int bdd_read_reorderings | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns the number of times reordering has occurred.]
SideEffects []
Definition at line 4928 of file cuPort.c.
04929 { 04930 return(Cudd_ReadReorderings((DdManager *)mgr)); 04931 04932 } /* end of bdd_read_reorderings */
| int bdd_read_zdd_level | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Returns the level of a of a bdd_node with index, index.]
Description [Returns the level of a of a bdd_node with index, index.]
SideEffects []
Definition at line 5556 of file cuPort.c.
05557 { 05558 return(Cudd_ReadPermZdd((DdManager *)mgr, index)); 05559 05560 } /* end of bdd_read_zdd_level */
| bdd_node* bdd_read_zero | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Read constant zero of the manager. This is different from the logical zero which is the complement of logical one.]
SideEffects [bdd_zero]
| void bdd_realign_disable | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Disables the alignment of BDD vars with that of corresponding ZDD vars.]
Description [Disables the alignment of BDD vars with that of corresponding ZDD vars.]
SideEffects []
Definition at line 5678 of file cuPort.c.
05679 { 05680 Cudd_bddRealignDisable((DdManager *)mgr); 05681 05682 } /* end of bdd_realign_disable */
| void bdd_realign_enable | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Enables the alignment of BDD vars with that of corresponding ZDD vars.]
Description [Enables the alignment of BDD vars with that of corresponding ZDD vars.]
SideEffects []
Definition at line 5659 of file cuPort.c.
05660 { 05661 Cudd_bddRealignEnable((DdManager *)mgr); 05662 05663 } /* end of bdd_realign_enable */
| int bdd_realignment_enabled | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns the value of the variable for the alignment of BDD vars with that of corresponding ZDD vars.]
Description [Returns the value of the variable for the alignment of BDD vars with that of corresponding ZDD vars.]
SideEffects []
Definition at line 5697 of file cuPort.c.
05698 { 05699 return(Cudd_bddRealignmentEnabled((DdManager *)mgr)); 05700 05701 } /* end of bdd_realignment_enabled */
| void bdd_recursive_deref | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
Function********************************************************************
Synopsis [Decreases the reference count of node.If f dies, recursively decreases the reference counts of its children. It is used to dispose of a DD that is no longer needed.]
SideEffects []
Definition at line 3872 of file cuPort.c.
03873 { 03874 Cudd_RecursiveDeref((DdManager *)mgr, (DdNode *)f); 03875 03876 } /* end of bdd_recursive_deref */
| void bdd_recursive_deref_zdd | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
Function********************************************************************
Synopsis [Recursively derefs a ZDD.]
Description [Recursively derefs a ZDD.]
SideEffects [bdd_recursive_deref]
Definition at line 5522 of file cuPort.c.
05523 { 05524 Cudd_RecursiveDerefZdd((DdManager *)mgr, (DdNode *)f); 05525 05526 } /* end of bdd_recursive_deref_zdd */
| void bdd_ref | ( | bdd_node * | fn | ) |
Function********************************************************************
Synopsis [Makes the bdd_node a regular one.]
Description [Makes the bdd_node a retular one.]
SideEffects [none]
Definition at line 5413 of file cuPort.c.
05414 { 05415 return(Cudd_Regular((DdNode *)f)); 05416 05417 } /* end of bdd_regular */
| int bdd_remove_hook | ( | bdd_manager * | mgr, | |
| int(*)(bdd_manager *, char *, void *) | procedure, | |||
| bdd_hook_type_t | whichHook | |||
| ) |
Function********************************************************************
Synopsis [Removes the function from the hook.]
SideEffects []
Definition at line 3212 of file cuPort.c.
03216 { 03217 int retval; 03218 Cudd_HookType hook; 03219 switch (whichHook) { 03220 case BDD_PRE_GC_HOOK: hook = CUDD_PRE_GC_HOOK; break; 03221 case BDD_POST_GC_HOOK: hook = CUDD_POST_GC_HOOK; break; 03222 case BDD_PRE_REORDERING_HOOK: hook = CUDD_PRE_REORDERING_HOOK; break; 03223 case BDD_POST_REORDERING_HOOK: hook = CUDD_POST_REORDERING_HOOK; break; 03224 default: fprintf(stderr, "Dont know which hook"); return 0; 03225 } 03226 retval = Cudd_RemoveHook((DdManager *)mgr, (DD_HFP)procedure, hook); 03227 return retval; 03228 03229 } /* end of bdd_remove_hook */
| void bdd_reorder | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Calls reordering explicitly.]
SideEffects []
Definition at line 3497 of file cuPort.c.
03498 { 03499 /* 10 = whatever (Verbatim from file ddTable.c) */ 03500 (void) Cudd_ReduceHeap((DdManager *)mgr,((DdManager *)mgr)->autoMethod,10); 03501 return; 03502 03503 } /* end of bdd_reorder */
| bdd_reorder_verbosity_t bdd_reordering_reporting | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [ Reporting of reordering stats.]
SideEffects []
Definition at line 3274 of file cuPort.c.
03275 { 03276 int retval; 03277 bdd_reorder_verbosity_t reorderVerbosity; 03278 retval = Cudd_ReorderingReporting((DdManager *) mgr); 03279 switch(retval) { 03280 case 0: reorderVerbosity = BDD_REORDER_NO_VERBOSITY; break; 03281 case 1: reorderVerbosity = BDD_REORDER_VERBOSITY; break; 03282 default: reorderVerbosity = BDD_REORDER_VERBOSITY_DEFAULT; break; 03283 } 03284 return reorderVerbosity; 03285 03286 } /* end of bdd_reordering_reporting */
| int bdd_reordering_status | ( | bdd_manager * | mgr, | |
| bdd_reorder_type_t * | method | |||
| ) |
Function********************************************************************
Synopsis []
SideEffects []
Definition at line 3640 of file cuPort.c.
03641 { 03642 int dyn; 03643 03644 dyn = Cudd_ReorderingStatus((DdManager *)mgr, (Cudd_ReorderingType *)method); 03645 switch (*method) { 03646 case CUDD_REORDER_SIFT: 03647 *method = BDD_REORDER_SIFT; 03648 break; 03649 case CUDD_REORDER_WINDOW3_CONV: 03650 *method = BDD_REORDER_WINDOW3_CONV; 03651 break; 03652 case CUDD_REORDER_NONE: 03653 *method = BDD_REORDER_NONE; 03654 break; 03655 case CUDD_REORDER_SAME: 03656 *method = BDD_REORDER_SAME; 03657 break; 03658 case CUDD_REORDER_RANDOM: 03659 *method = BDD_REORDER_RANDOM; 03660 break; 03661 case CUDD_REORDER_RANDOM_PIVOT: 03662 *method = BDD_REORDER_RANDOM_PIVOT; 03663 break; 03664 case CUDD_REORDER_SIFT_CONVERGE: 03665 *method = BDD_REORDER_SIFT_CONVERGE; 03666 break; 03667 case CUDD_REORDER_SYMM_SIFT: 03668 *method = BDD_REORDER_SYMM_SIFT; 03669 break; 03670 case CUDD_REORDER_SYMM_SIFT_CONV: 03671 *method = BDD_REORDER_SYMM_SIFT_CONV; 03672 break; 03673 case CUDD_REORDER_WINDOW2: 03674 *method = BDD_REORDER_WINDOW2; 03675 break; 03676 case CUDD_REORDER_WINDOW4: 03677 *method = BDD_REORDER_WINDOW4; 03678 break; 03679 case CUDD_REORDER_WINDOW2_CONV: 03680 *method = BDD_REORDER_WINDOW2_CONV; 03681 break; 03682 case CUDD_REORDER_WINDOW3: 03683 *method = BDD_REORDER_WINDOW3; 03684 break; 03685 case CUDD_REORDER_WINDOW4_CONV: 03686 *method = BDD_REORDER_WINDOW4_CONV; 03687 break; 03688 case CUDD_REORDER_GROUP_SIFT: 03689 *method = BDD_REORDER_GROUP_SIFT; 03690 break; 03691 case CUDD_REORDER_GROUP_SIFT_CONV: 03692 *method = BDD_REORDER_GROUP_SIFT_CONV; 03693 break; 03694 case CUDD_REORDER_ANNEALING: 03695 *method = BDD_REORDER_ANNEALING; 03696 break; 03697 case CUDD_REORDER_GENETIC: 03698 *method = BDD_REORDER_GENETIC; 03699 break; 03700 case CUDD_REORDER_EXACT: 03701 *method = BDD_REORDER_EXACT; 03702 break; 03703 default: 03704 break; 03705 } 03706 return(dyn); 03707 03708 } /* end of bdd_reordering_status */
| int bdd_reordering_zdd_status | ( | bdd_manager * | mgr, | |
| bdd_reorder_type_t * | method | |||
| ) |
Function********************************************************************
Synopsis []
SideEffects []
Definition at line 3719 of file cuPort.c.
03720 { 03721 int dyn; 03722 dyn = Cudd_ReorderingStatusZdd((DdManager *)mgr, (Cudd_ReorderingType *)method); 03723 switch (*method) { 03724 case CUDD_REORDER_SIFT: 03725 *method = BDD_REORDER_SIFT; 03726 break; 03727 case CUDD_REORDER_WINDOW3_CONV: 03728 *method = BDD_REORDER_WINDOW3_CONV; 03729 break; 03730 case CUDD_REORDER_NONE: 03731 *method = BDD_REORDER_NONE; 03732 break; 03733 case CUDD_REORDER_SAME: 03734 *method = BDD_REORDER_SAME; 03735 break; 03736 case CUDD_REORDER_RANDOM: 03737 *method = BDD_REORDER_RANDOM; 03738 break; 03739 case CUDD_REORDER_RANDOM_PIVOT: 03740 *method = BDD_REORDER_RANDOM_PIVOT; 03741 break; 03742 case CUDD_REORDER_SIFT_CONVERGE: 03743 *method = BDD_REORDER_SIFT_CONVERGE; 03744 break; 03745 case CUDD_REORDER_SYMM_SIFT: 03746 *method = BDD_REORDER_SYMM_SIFT; 03747 break; 03748 case CUDD_REORDER_SYMM_SIFT_CONV: 03749 *method = BDD_REORDER_SYMM_SIFT_CONV; 03750 break; 03751 case CUDD_REORDER_WINDOW2: 03752 *method = BDD_REORDER_WINDOW2; 03753 break; 03754 case CUDD_REORDER_WINDOW4: 03755 *method = BDD_REORDER_WINDOW4; 03756 break; 03757 case CUDD_REORDER_WINDOW2_CONV: 03758 *method = BDD_REORDER_WINDOW2_CONV; 03759 break; 03760 case CUDD_REORDER_WINDOW3: 03761 *method = BDD_REORDER_WINDOW3; 03762 break; 03763 case CUDD_REORDER_WINDOW4_CONV: 03764 *method = BDD_REORDER_WINDOW4_CONV; 03765 break; 03766 case CUDD_REORDER_GROUP_SIFT: 03767 *method = BDD_REORDER_GROUP_SIFT; 03768 break; 03769 case CUDD_REORDER_GROUP_SIFT_CONV: 03770 *method = BDD_REORDER_GROUP_SIFT_CONV; 03771 break; 03772 case CUDD_REORDER_ANNEALING: 03773 *method = BDD_REORDER_ANNEALING; 03774 break; 03775 case CUDD_REORDER_GENETIC: 03776 *method = BDD_REORDER_GENETIC; 03777 break; 03778 case CUDD_REORDER_EXACT: 03779 *method = BDD_REORDER_EXACT; 03780 break; 03781 default: 03782 break; 03783 } 03784 return(dyn); 03785 03786 } /* end of bdd_reordering_zdd_status */
| int bdd_reset_var_to_be_grouped | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Resets a variable not to be grouped.]
Description [Resets a variable not to be grouped. This function is used for lazy sifting.]
SideEffects [none]
Definition at line 7253 of file cuPort.c.
07254 { 07255 return Cudd_bddResetVarToBeGrouped((DdManager *) mgr, index); 07256 07257 } /* end of bdd_reset_var_to_be_grouped */
| void bdd_set_background | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
Function********************************************************************
Synopsis [Set the background value of BDD manager.]
Description [Set the background value of BDD manager.]
SideEffects []
Definition at line 5963 of file cuPort.c.
05964 { 05965 Cudd_SetBackground((DdManager *)mgr,(DdNode *)f); 05966 05967 } /* end of bdd_set_background */
| void bdd_set_gc_mode | ( | bdd_manager * | mgr, | |
| boolean | no_gc | |||
| ) |
Function********************************************************************
Synopsis [Turns on or off garbage collection.]
SideEffects []
Definition at line 3297 of file cuPort.c.
03298 { 03299 if (no_gc) { 03300 Cudd_DisableGarbageCollection((DdManager *) mgr); 03301 } else { 03302 Cudd_EnableGarbageCollection((DdManager *) mgr); 03303 } 03304 return; 03305 03306 } /* end of bdd_set_gc_mode */
Function********************************************************************
Synopsis [Sets the next field of a DdNode. This function should NOT be used by an external user. This is provided here as a patch. This will not be a part of any further release.]
Description [Sets the next field of a DdNode. This function should NOT be used by an external user. This is provided here as a patch. This will not be a part of any further release.]
SideEffects []
| void bdd_set_next_reordering | ( | bdd_manager * | mgr, | |
| int | next | |||
| ) |
Function********************************************************************
Synopsis [Sets the threshold for the next dynamic reordering.]
SideEffects []
Definition at line 4958 of file cuPort.c.
04959 { 04960 Cudd_SetNextReordering((DdManager *)mgr, next); 04961 04962 } /* end of bdd_set_next_reordering */
| int bdd_set_ns_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Sets a variable type to next state.]
SideEffects [none]
Definition at line 7118 of file cuPort.c.
07119 { 07120 return Cudd_bddSetNsVar((DdManager *) mgr, index); 07121 07122 } /* end of bdd_set_ns_var */
| int bdd_set_pair_index | ( | bdd_manager * | mgr, | |
| int | index, | |||
| int | pairidx | |||
| ) |
Function********************************************************************
Synopsis [Sets a corresponding pair index for a given index.]
Description [Sets a corresponding pair index for a given index. These pair indices are present and next state variable.]
SideEffects [none]
Definition at line 7181 of file cuPort.c.
07182 { 07183 return Cudd_bddSetPairIndex((DdManager *) mgr, index, pairidx); 07184 07185 } /* end of bdd_set_pair_index */
| int bdd_set_parameters | ( | bdd_manager * | mgr, | |
| avl_tree * | valueTable, | |||
| FILE * | file | |||
| ) |
Function********************************************************************
Synopsis [Sets the internal parameters of the package to the given values.]
Description [The CUDD package has a set of parameters that can be assigned different values. This function receives a table which maps strings to values and sets the parameters represented by the strings to the pertinent values. Some basic type checking is done. It returns 1 if everything is correct and 0 otherwise.]
SideEffects []
Definition at line 2797 of file cuPort.c.
02801 { 02802 Cudd_ReorderingType reorderMethod; 02803 Cudd_ReorderingType zddReorderMethod; 02804 st_table *newValueTable; 02805 st_generator *stgen; 02806 avl_generator *avlgen; 02807 char *paramName; 02808 char *paramValue; 02809 02810 /* Initial value of the variables. */ 02811 reorderMethod = CUDD_REORDER_SAME; 02812 zddReorderMethod = CUDD_REORDER_SAME; 02813 02814 /* Build a new table with the parameter names but with 02815 ** the prefix removed. */ 02816 newValueTable = st_init_table(st_ptrcmp, st_ptrhash); 02817 avl_foreach_item(valueTable, avlgen, AVL_FORWARD, (char **)¶mName, 02818 (char **)¶mValue) { 02819 if (strncmp(paramName, "BDD.", 4) == 0) { 02820 st_insert(newValueTable, (char *)¶mName[4], 02821 (char *)paramValue); 02822 } 02823 } 02824 02825 st_foreach_item(newValueTable, stgen, ¶mName, ¶mValue) { 02826 int uvalue; 02827 char *invalidChar; 02828 02829 invalidChar = NIL(char); 02830 02831 if (strcmp(paramName, "Hard limit for cache size") == 0) { 02832 02833 uvalue = strtol(paramValue, &invalidChar, 10); 02834 if (*invalidChar || uvalue < 0) { 02835 InvalidType(file, "Hard limit for cache size", 02836 "unsigned integer"); 02837 } 02838 else { 02839 Cudd_SetMaxCacheHard((DdManager *) mgr, (unsigned int) uvalue); 02840 } 02841 } 02842 else if (strcmp(paramName, "Cache hit threshold for resizing") == 0) { 02843 02844 uvalue = strtol(paramValue, &invalidChar, 10); 02845 if (*invalidChar || uvalue < 0) { 02846 InvalidType(file, "Cache hit threshold for resizing", 02847 "unsigned integer"); 02848 } 02849 else { 02850 Cudd_SetMinHit((DdManager *) mgr, (unsigned int) uvalue); 02851 } 02852 } 02853 else if (strcmp(paramName, "Garbage collection enabled") == 0) { 02854 if (strcmp(paramValue, "yes") == 0) { 02855 Cudd_EnableGarbageCollection((DdManager *) mgr); 02856 } 02857 else if (strcmp(paramValue, "no") == 0) { 02858 Cudd_DisableGarbageCollection((DdManager *) mgr); 02859 } 02860 else { 02861 InvalidType(file, "Garbage collection enabled", "(yes,no)"); 02862 } 02863 } 02864 else if (strcmp(paramName, "Limit for fast unique table growth") 02865 == 0) { 02866 02867 uvalue = strtol(paramValue, &invalidChar, 10); 02868 if (*invalidChar || uvalue < 0) { 02869 InvalidType(file, "Limit for fast unique table growth", 02870 "unsigned integer"); 02871 } 02872 else { 02873 Cudd_SetLooseUpTo((DdManager *) mgr, (unsigned int) uvalue); 02874 } 02875 } 02876 else if (strcmp(paramName, 02877 "Maximum number of variables sifted per reordering") 02878 == 0) { 02879 02880 uvalue = strtol(paramValue, &invalidChar, 10); 02881 if (*invalidChar || uvalue < 0) { 02882 InvalidType(file, "Maximum number of variables sifted per reordering", 02883 "unsigned integer"); 02884 } 02885 else { 02886 Cudd_SetSiftMaxVar((DdManager *) mgr, uvalue); 02887 } 02888 } 02889 else if (strcmp(paramName, 02890 "Maximum number of variable swaps per reordering") 02891 == 0) { 02892 02893 uvalue = strtol(paramValue, &invalidChar, 10); 02894 if (*invalidChar || uvalue < 0) { 02895 InvalidType(file, "Maximum number of variable swaps per reordering", 02896 "unsigned integer"); 02897 } 02898 else { 02899 Cudd_SetSiftMaxSwap((DdManager *) mgr, uvalue); 02900 } 02901 } 02902 else if (strcmp(paramName, 02903 "Maximum growth while sifting a variable") == 0) { 02904 double value; 02905 02906 value = strtod(paramValue, &invalidChar); 02907 if (*invalidChar) { 02908 InvalidType(file, "Maximum growth while sifting a variable", 02909 "real"); 02910 } 02911 else { 02912 Cudd_SetMaxGrowth((DdManager *) mgr, value); 02913 } 02914 } 02915 else if (strcmp(paramName, "Dynamic reordering of BDDs enabled") 02916 == 0) { 02917 if (strcmp(paramValue, "yes") == 0) { 02918 Cudd_AutodynEnable((DdManager *) mgr, reorderMethod); 02919 } 02920 else if (strcmp(paramValue, "no") == 0) { 02921 Cudd_AutodynDisable((DdManager *) mgr); 02922 } 02923 else { 02924 InvalidType(file, "Dynamic reordering of BDDs enabled", 02925 "(yes,no)"); 02926 } 02927 } 02928 else if (strcmp(paramName, "Default BDD reordering method") == 0) { 02929 Cudd_ReorderingType reorderInt; 02930 02931 reorderMethod = (Cudd_ReorderingType) strtol(paramValue, 02932 &invalidChar, 10); 02933 if (*invalidChar || reorderMethod < 0) { 02934 InvalidType(file, "Default BDD reordering method", "integer"); 02935 } 02936 else { 02937 if (Cudd_ReorderingStatus((DdManager *) mgr, &reorderInt)) { 02938 Cudd_AutodynEnable((DdManager *) mgr, reorderMethod); 02939 } 02940 } 02941 } 02942 else if (strcmp(paramName, "Dynamic reordering of ZDDs enabled") 02943 == 0) { 02944 if (strcmp(paramValue, "yes") == 0) { 02945 Cudd_AutodynEnableZdd((DdManager *) mgr, zddReorderMethod); 02946 } 02947 else if (strcmp(paramValue, "no") == 0) { 02948 Cudd_AutodynDisableZdd((DdManager *) mgr); 02949 } 02950 else { 02951 InvalidType(file, "Dynamic reordering of ZDDs enabled", "(yes,no)"); 02952 } 02953 } 02954 else if (strcmp(paramName, "Default ZDD reordering method") == 0) { 02955 Cudd_ReorderingType reorderInt; 02956 02957 zddReorderMethod = (Cudd_ReorderingType) strtol(paramValue, 02958 &invalidChar, 10); 02959 if (*invalidChar || zddReorderMethod < 0) { 02960 InvalidType(file, "Default ZDD reordering method", "integer"); 02961 } 02962 else { 02963 if (Cudd_ReorderingStatusZdd((DdManager *) mgr, &reorderInt)) { 02964 Cudd_AutodynEnableZdd((DdManager *) mgr, zddReorderMethod); 02965 } 02966 } 02967 } 02968 else if (strcmp(paramName, "Realignment of ZDDs to BDDs enabled") 02969 == 0) { 02970 if (strcmp(paramValue, "yes") == 0) { 02971 Cudd_zddRealignEnable((DdManager *) mgr); 02972 } 02973 else if (strcmp(paramValue, "no") == 0) { 02974 Cudd_zddRealignDisable((DdManager *) mgr); 02975 } 02976 else { 02977 InvalidType(file, "Realignment of ZDDs to BDDs enabled", 02978 "(yes,no)"); 02979 } 02980 } 02981 else if (strcmp(paramName, 02982 "Dead node counted in triggering reordering") == 0) { 02983 if (strcmp(paramValue, "yes") == 0) { 02984 Cudd_TurnOnCountDead((DdManager *) mgr); 02985 } 02986 else if (strcmp(paramValue, "no") == 0) { 02987 Cudd_TurnOffCountDead((DdManager *) mgr); 02988 } 02989 else { 02990 InvalidType(file, 02991 "Dead node counted in triggering reordering", 02992 "(yes,no)"); 02993 } 02994 } 02995 else if (strcmp(paramName, "Group checking criterion") == 0) { 02996 02997 uvalue = strtol(paramValue, &invalidChar, 10); 02998 if (*invalidChar || uvalue < 0) { 02999 InvalidType(file, "Group checking criterion", "integer"); 03000 } 03001 else { 03002 Cudd_SetGroupcheck((DdManager *) mgr, (Cudd_AggregationType) uvalue); 03003 } 03004 } 03005 else if (strcmp(paramName, "Recombination threshold") == 0) { 03006 03007 uvalue = strtol(paramValue, &invalidChar, 10); 03008 if (*invalidChar || uvalue < 0) { 03009 InvalidType(file, "Recombination threshold", "integer"); 03010 } 03011 else { 03012 Cudd_SetRecomb((DdManager *) mgr, uvalue); 03013 } 03014 } 03015 else if (strcmp(paramName, "Symmetry violation threshold") == 0) { 03016 03017 uvalue = strtol(paramValue, &invalidChar, 10); 03018 if (*invalidChar || uvalue < 0) { 03019 InvalidType(file, "Symmetry violation threshold", "integer"); 03020 } 03021 else { 03022 Cudd_SetSymmviolation((DdManager *) mgr, uvalue); 03023 } 03024 } 03025 else if (strcmp(paramName, "Arc violation threshold") == 0) { 03026 03027 uvalue = strtol(paramValue, &invalidChar, 10); 03028 if (*invalidChar || uvalue < 0) { 03029 InvalidType(file, "Arc violation threshold", "integer"); 03030 } 03031 else { 03032 Cudd_SetArcviolation((DdManager *) mgr, uvalue); 03033 } 03034 } 03035 else if (strcmp(paramName, "GA population size") == 0) { 03036 03037 uvalue = strtol(paramValue, &invalidChar, 10); 03038 if (*invalidChar || uvalue < 0) { 03039 InvalidType(file, "GA population size", "integer"); 03040 } 03041 else { 03042 Cudd_SetPopulationSize((DdManager *) mgr, uvalue); 03043 } 03044 } 03045 else if (strcmp(paramName, "Number of crossovers for GA") == 0) { 03046 03047 uvalue = strtol(paramValue, &invalidChar, 10); 03048 if (*invalidChar || uvalue < 0) { 03049 InvalidType(file, "Number of crossovers for GA", "integer"); 03050 } 03051 else { 03052 Cudd_SetNumberXovers((DdManager *) mgr, uvalue); 03053 } 03054 } 03055 else if (strcmp(paramName, "Next reordering threshold") == 0) { 03056 03057 uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10); 03058 if (*invalidChar || uvalue < 0) { 03059 InvalidType(file, "Next reordering threshold", "integer"); 03060 } 03061 else { 03062 Cudd_SetNextReordering((DdManager *) mgr, uvalue); 03063 } 03064 } 03065 else { 03066 (void) fprintf(file, "Warning: Parameter %s not recognized.", 03067 paramName); 03068 (void) fprintf(file, " Ignored.\n"); 03069 } 03070 } /* end of st_foreach_item */ 03071 03072 /* Clean up. */ 03073 st_free_table(newValueTable); 03074 03075 return(1); 03076 03077 } /* end of bdd_set_parameters */
| int bdd_set_pi_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Sets a variable type to primary input.]
SideEffects [none]
Definition at line 7088 of file cuPort.c.
07089 { 07090 return Cudd_bddSetPiVar((DdManager *) mgr, index); 07091 07092 } /* bdd_set_pi_var */
| int bdd_set_ps_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Sets a variable type to present state.]
SideEffects [none]
Definition at line 7103 of file cuPort.c.
07104 { 07105 return Cudd_bddSetPsVar((DdManager *) mgr, index); 07106 07107 } /* end of bdd_set_ps_var */
| void bdd_set_reordered_field | ( | bdd_manager * | mgr, | |
| int | n | |||
| ) |
Function********************************************************************
Synopsis [Set the reordered field of the manager.This is NOT to be used by an external user. This function will not be a part of future release.]
Description [Set the reordered field of the manager.This is NOT to be used by an external user. This function will not be a part of future release.]
SideEffects []
Definition at line 5792 of file cuPort.c.
05793 { 05794 ((DdManager *)mgr)->reordered = n; 05795 05796 } /* end of bdd_set_reordered_field */
| int bdd_set_var_hard_group | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Sets a variable to be a hard group.]
Description [Sets a variable to be a hard group. This function is used for lazy sifting.]
SideEffects [none]
Definition at line 7235 of file cuPort.c.
07236 { 07237 return Cudd_bddSetVarHardGroup((DdManager *) mgr, index); 07238 07239 } /* end of bdd_set_var_hard_group */
| int bdd_set_var_to_be_grouped | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Sets a variable to be grouped.]
Description [Sets a variable to be grouped. This function is used for lazy sifting.]
SideEffects [none]
Definition at line 7217 of file cuPort.c.
07218 { 07219 return Cudd_bddSetVarToBeGrouped((DdManager *) mgr, index); 07220 07221 } /* end of bdd_set_var_to_be_grouped */
| int bdd_set_var_to_be_ungrouped | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Sets a variable to be ungrouped.]
Description [Sets a variable to be ungrouped. This function is used for lazy sifting.]
SideEffects [none]
Definition at line 7325 of file cuPort.c.
07326 { 07327 return Cudd_bddSetVarToBeUngrouped((DdManager *) mgr, index); 07328 07329 } /* end of bdd_set_var_to_be_ungrouped */
Function********************************************************************
Synopsis [Finds a shortest path in a DD.]
Description [Finds a shortest path in a DD. f is the DD we want to get the shortest path for; weight\[i\] is the weight of the THEN arc coming from the node whose index is i. If weight is NULL, then unit weights are assumed for all THEN arcs. All ELSE arcs have 0 weight. If non-NULL, both weight and support should point to arrays with at least as many entries as there are variables in the manager. Returns the shortest path as the BDD of a cube.]
SideEffects [support contains on return the true support of f. If support is NULL on entry, then Cudd_ShortestPath does not compute the true support info. length contains the length of the path.]
Definition at line 1903 of file cuPort.c.
01908 { 01909 DdNode *result; 01910 bdd_t *output; 01911 01912 result = Cudd_ShortestPath(f->mgr, f->node, weight, support, length); 01913 if (result == NULL) return(NULL); 01914 cuddRef(result); 01915 01916 output = bdd_construct_bdd_t(f->mgr,result); 01917 return(output); 01918 01919 } /* end of bdd_shortest_path */
| int bdd_shuffle_heap | ( | bdd_manager * | mgr, | |
| int * | permut | |||
| ) |
Function********************************************************************
Synopsis [Shuffles the variables in the manager in the given order.]
SideEffects []
Definition at line 4081 of file cuPort.c.
04082 { 04083 int result; 04084 result = Cudd_ShuffleHeap((DdManager *)mgr, permut); 04085 return(result); 04086 04087 } /* end of bdd_shuffle_heap */
| int bdd_size | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [Computes the number of nodes of a BDD.]
SideEffects []
Definition at line 3088 of file cuPort.c.
03089 { 03090 return(Cudd_DagSize(f->node)); 03091 03092 } /* end of bdd_size */
| long bdd_size_multiple | ( | array_t * | bddArray | ) |
Function********************************************************************
Synopsis [Computes the shared size of an array of BDDs.]
Description [Computes the shared size of an array of BDDs. Returns CUDD_OUT_OF_MEM in case of failure.]
SideEffects []
Definition at line 3121 of file cuPort.c.
03122 { 03123 DdNode **nodeArray; 03124 bdd_t *bddUnit; 03125 long result; 03126 int i; 03127 03128 nodeArray = ALLOC(DdNode *, array_n(bddArray)); 03129 if (nodeArray == NULL) return(CUDD_OUT_OF_MEM); 03130 for (i = 0; i < array_n(bddArray); i++) { 03131 bddUnit = array_fetch(bdd_t *, bddArray, i); 03132 nodeArray[i] = bddUnit->node; 03133 } 03134 03135 result = Cudd_SharingSize(nodeArray,array_n(bddArray)); 03136 03137 /* Clean up */ 03138 FREE(nodeArray); 03139 03140 return(result); 03141 03142 } /* end of bdd_size_multiple */
Function********************************************************************
Synopsis [Existential abstraction of variables.]
SideEffects []
Definition at line 2010 of file cuPort.c.
02013 { 02014 int i; 02015 bdd_t *variable; 02016 DdNode *cube,*tmpDd,*result; 02017 DdManager *mgr; 02018 DdNode **vars; 02019 int nVars, level; 02020 02021 /* The Boulder package needs the smoothing variables passed as a cube. 02022 * Therefore we must build that cube from the indices of the variables 02023 * in the array before calling the procedure. 02024 */ 02025 mgr = f->mgr; 02026 nVars = mgr->size; 02027 vars = ALLOC(DdNode *, sizeof(DdNode *) * nVars); 02028 memset(vars, 0, sizeof(DdNode *) * nVars); 02029 for (i = 0; i < array_n(smoothing_vars); i++) { 02030 variable = array_fetch(bdd_t *,smoothing_vars,i); 02031 02032 /* Make sure the variable belongs to the same manager. */ 02033 assert(mgr == variable->mgr); 02034 02035 level = Cudd_ReadPerm(mgr, Cudd_NodeReadIndex(variable->node)); 02036 vars[level] = variable->node; 02037 } 02038 Cudd_Ref(cube = DD_ONE(mgr)); 02039 for (i = nVars - 1; i >= 0; i--) { 02040 if (!vars[i]) 02041 continue; 02042 tmpDd = Cudd_bddAnd(mgr,cube,vars[i]); 02043 if (tmpDd == NULL) { 02044 Cudd_RecursiveDeref(mgr, cube); 02045 return(NULL); 02046 } 02047 cuddRef(tmpDd); 02048 Cudd_RecursiveDeref(mgr, cube); 02049 cube = tmpDd; 02050 } 02051 FREE(vars); 02052 02053 /* Perform the smoothing */ 02054 result = Cudd_bddExistAbstract(mgr,f->node,cube); 02055 if (result == NULL) { 02056 Cudd_RecursiveDeref(mgr, cube); 02057 return(NULL); 02058 } 02059 cuddRef(result); 02060 02061 /* Get rid of temporary results */ 02062 Cudd_RecursiveDeref(mgr, cube); 02063 02064 /* Build the bdd_t structure for the result */ 02065 return(bdd_construct_bdd_t(mgr,result)); 02066 02067 } /* end of bdd_smooth */
Function********************************************************************
Synopsis [Existential abstraction of variables.]
SideEffects []
Definition at line 2078 of file cuPort.c.
02079 { 02080 DdNode *result; 02081 DdManager *mgr; 02082 02083 mgr = f->mgr; 02084 02085 /* Perform the smoothing */ 02086 result = Cudd_bddExistAbstract(mgr,f->node,cube->node); 02087 if (result == NULL) 02088 return(NULL); 02089 cuddRef(result); 02090 02091 /* Build the bdd_t structure for the result */ 02092 return(bdd_construct_bdd_t(mgr,result)); 02093 02094 } /* end of bdd_smooth_with_cube */
Function********************************************************************
Synopsis [Solves a Boolean equation.]
SideEffects [The array passed in g is filled with the solutions.]
Definition at line 6376 of file cuPort.c.
06380 { 06381 int i; 06382 bdd_t *variable; 06383 DdNode *cube, *tmpDd, *result, **G; 06384 DdManager *mgr; 06385 int *yIndex = NIL(int); 06386 06387 /* CUDD needs the y variables passed as a cube. 06388 * Therefore we must build that cube from the indices of variables 06389 * in the array before calling the procedure. 06390 */ 06391 mgr = f->mgr; 06392 Cudd_Ref(cube = DD_ONE(mgr)); 06393 for (i = 0; i < array_n(unknowns); i++) { 06394 variable = array_fetch(bdd_t *,unknowns,i); 06395 06396 /* Make sure the variable belongs to the same manager. */ 06397 assert(mgr == variable->mgr); 06398 06399 tmpDd = Cudd_bddAnd(mgr,cube,variable->node); 06400 if (tmpDd == NULL) { 06401 Cudd_RecursiveDeref(mgr,cube); 06402 return(NULL); 06403 } 06404 cuddRef(tmpDd); 06405 Cudd_RecursiveDeref(mgr, cube); 06406 cube = tmpDd; 06407 } 06408 06409 /* Allocate memory for the solutions. */ 06410 G = ALLOC(DdNode *,array_n(unknowns)); 06411 for (i = 0; i < array_n(unknowns); i++) { 06412 G[i] = NIL(DdNode); 06413 } 06414 06415 /* Solve the equation */ 06416 result = Cudd_SolveEqn(mgr,f->node,cube,G,&yIndex,array_n(unknowns)); 06417 if (result == NULL) { 06418 Cudd_RecursiveDeref(mgr, cube); 06419 return(NULL); 06420 } 06421 cuddRef(result); 06422 /* Get rid of temporary results. */ 06423 Cudd_RecursiveDeref(mgr, cube); 06424 06425 /* Build the bdd_t structure for the solutions. */ 06426 for (i = 0; i < array_n(unknowns); i++) { 06427 bdd_t *tmp = bdd_construct_bdd_t(mgr,G[i]); 06428 array_insert_last(bdd_t *, g, tmp); 06429 } 06430 06431 return(bdd_construct_bdd_t(mgr,result)); 06432 06433 } /* end of bdd_slve_eqn */
| bdd_node* bdd_split_set | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | x, | |||
| int | n, | |||
| double | m | |||
| ) |
Function********************************************************************
Synopsis [Returns m minterms from a BDD.]
Description [Returns m minterms from a BDD whose support has n variables at most. The procedure tries to create as few extra nodes as possible. The function represented by f depends on at most n of the variables in x. Returns a BDD with m minterms of the on-set of f if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Function********************************************************************
Synopsis [Computes a bdd between l and u.]
SideEffects []
Definition at line 1218 of file cuPort.c.
01219 { 01220 DdNode *result; 01221 01222 /* Make sure both operands belong to the same manager */ 01223 assert(l->mgr == u->mgr); 01224 01225 result = Cudd_bddSqueeze(l->mgr,l->node, 01226 u->node); 01227 if (result == NULL) return(NULL); 01228 cuddRef(result); 01229 return(bdd_construct_bdd_t(l->mgr,result)); 01230 01231 } /* end of bdd_squeeze */
| bdd_manager* bdd_start | ( | int | nvariables | ) |
Function********************************************************************
Synopsis [Starts the manager with nvariables variables.]
SideEffects []
Definition at line 172 of file cuPort.c.
00173 { 00174 DdManager *mgr; 00175 bdd_external_hooks *hooks; 00176 00177 mgr = Cudd_Init((unsigned int)nvariables, 0, CUDD_UNIQUE_SLOTS, 00178 CUDD_CACHE_SLOTS, getSoftDataLimit() / 10 * 9); 00179 00180 hooks = ALLOC(bdd_external_hooks,1); 00181 hooks->mdd = hooks->network = hooks->undef1 = (char *) 0; 00182 mgr->hooks = (char *) hooks; 00183 00184 return(bdd_manager *)mgr; 00185 00186 } /* end of bdd_start */
Function********************************************************************
Synopsis [Extracts a subset from a BDD with mask variables.]
Description [Extracts a subset from a BDD in the following procedure. 1. Compute the weight for each mask variable by counting the number of minterms for both positive and negative cofactors of the BDD with respect to each mask variable. (weight = positive - negative) 2. Find a representative cube of the BDD by using the weight. From the top variable of the BDD, for each variable, if the weight is greater than 0.0, choose THEN branch, othereise ELSE branch, until meeting the constant 1. 3. Quantify out the variables not in maskVars from the representative cube and if a variable in maskVars is don't care, replace the variable with a constant(1 or 0) depending on the weight. 4. Make a subset of the BDD by multiplying with the modified cube.]
SideEffects [None]
SeeAlso []
Definition at line 4791 of file cuPort.c.
04792 { 04793 int i; 04794 DdNode *subset, **vars, **maskVars; 04795 bdd_t *var; 04796 int n = array_n(varsArray); 04797 int m = array_n(maskVarsArray); 04798 04799 vars = ALLOC(DdNode *, n); 04800 if (vars == NULL) 04801 return((bdd_t *)NULL); 04802 for (i = 0; i < n; i++) { 04803 var = array_fetch(bdd_t *, varsArray, i); 04804 vars[i] = var->node; 04805 } 04806 04807 maskVars = ALLOC(DdNode *, m); 04808 if (maskVars == NULL) { 04809 FREE(vars); 04810 return((bdd_t *)NULL); 04811 } 04812 for (i = 0; i < m; i++) { 04813 var = array_fetch(bdd_t *, maskVarsArray, i); 04814 maskVars[i] = var->node; 04815 } 04816 04817 subset = (DdNode *)Cudd_SubsetWithMaskVars((DdManager *)f->mgr, 04818 (DdNode *)f->node, (DdNode **)vars, n, (DdNode **)maskVars, m); 04819 if (subset == NULL) return((bdd_t *)NULL); 04820 04821 cuddRef(subset); 04822 FREE(vars); 04823 FREE(maskVars); 04824 04825 return(bdd_construct_bdd_t(f->mgr,subset)); 04826 04827 } /* end of bdd_subset_with_mask_vars */
Function********************************************************************
Synopsis [Permutes the variables.]
SideEffects []
Definition at line 2105 of file cuPort.c.
02109 { 02110 int i,from,to; 02111 int *permut; 02112 bdd_t *variable; 02113 DdNode *result; 02114 02115 /* Make sure both arrays have the same number of elements. */ 02116 assert(array_n(old_array) == array_n(new_array)); 02117 02118 /* Allocate and fill the array with the trivial permutation. */ 02119 permut = ALLOC(int, Cudd_ReadSize((DdManager *)f->mgr)); 02120 for (i = 0; i < Cudd_ReadSize((DdManager *)f->mgr); i++) permut[i] = i; 02121 02122 /* Modify the permutation by looking at both arrays old and new. */ 02123 for (i = 0; i < array_n(old_array); i++) { 02124 variable = array_fetch(bdd_t *, old_array, i); 02125 from = Cudd_Regular(variable->node)->index; 02126 variable = array_fetch(bdd_t *, new_array, i); 02127 /* Make sure the variable belongs to this manager. */ 02128 assert(f->mgr == variable->mgr); 02129 02130 to = Cudd_Regular(variable->node)->index; 02131 permut[from] = to; 02132 } 02133 02134 result = Cudd_bddPermute(f->mgr,f->node,permut); 02135 FREE(permut); 02136 if (result == NULL) return(NULL); 02137 cuddRef(result); 02138 return(bdd_construct_bdd_t(f->mgr,result)); 02139 02140 } /* end of bdd_substitute */
Function********************************************************************
Synopsis [Permutes the variables.]
SideEffects []
Definition at line 2173 of file cuPort.c.
02177 { 02178 int i; 02179 bdd_t *f, *new_; 02180 array_t *substitute_array = array_alloc(bdd_t *, 0); 02181 02182 arrayForEachItem(bdd_t *, f_array, i, f) { 02183 new_ = bdd_substitute(f, old_array, new_array); 02184 array_insert_last(bdd_t *, substitute_array, new_); 02185 } 02186 return(substitute_array); 02187 02188 } /* end of bdd_substitute_array */
Function********************************************************************
Synopsis [Permutes the variables.]
SideEffects []
Definition at line 2199 of file cuPort.c.
02202 { 02203 int i; 02204 bdd_t *f, *new_; 02205 array_t *substitute_array = array_alloc(bdd_t *, 0); 02206 02207 arrayForEachItem(bdd_t *, f_array, i, f) { 02208 new_ = bdd_substitute_with_permut(f, permut); 02209 array_insert_last(bdd_t *, substitute_array, new_); 02210 } 02211 return(substitute_array); 02212 02213 } /* end of bdd_substitute_array_with_permut */
Function********************************************************************
Synopsis [Permutes the variables.]
SideEffects []
Definition at line 2151 of file cuPort.c.
02154 { 02155 DdNode *result; 02156 02157 result = Cudd_bddPermute(f->mgr,f->node,permut); 02158 if (result == NULL) return(NULL); 02159 cuddRef(result); 02160 return(bdd_construct_bdd_t(f->mgr,result)); 02161 02162 } /* end of bdd_substitute_with_permut */
| int bdd_test_unate | ( | bdd_t * | f, | |
| int | varId, | |||
| int | phase | |||
| ) |
Function********************************************************************
Synopsis [Tests if the varid is unate in f in the specified phase. If yes, return 1, else 0.]
SideEffects []
Definition at line 6498 of file cuPort.c.
06499 { 06500 DdNode *result; 06501 DdNode *one = DD_ONE((DdManager *)f->mgr); 06502 06503 if (phase) { 06504 result = Cudd_Increasing((DdManager *)f->mgr, (DdNode *)f->node, varId); 06505 } else { 06506 result = Cudd_Decreasing((DdManager *)f->mgr, (DdNode *)f->node, varId); 06507 } 06508 06509 if (result == one) { 06510 return 1; 06511 } else { 06512 return 0; 06513 } 06514 06515 } /* end of bdd_test_unate */
Function********************************************************************
Synopsis [Returns the Then branch of the BDD.]
SideEffects []
Definition at line 2239 of file cuPort.c.
02240 { 02241 DdNode *result; 02242 02243 result = Cudd_T(f->node); 02244 result = Cudd_NotCond(result,Cudd_IsComplement(f->node)); 02245 cuddRef(result); 02246 return(bdd_construct_bdd_t(f->mgr,result)); 02247 02248 } /* end of bdd_then */
Function********************************************************************
Synopsis [Returns the BDD of the top variable.]
Description [Returns the BDD of the top variable of the argument. If the argument is constant, it returns the constant function itself.]
SideEffects []
Definition at line 2262 of file cuPort.c.
02263 { 02264 DdNode *result; 02265 02266 if (Cudd_IsConstant(f->node)) { 02267 result = f->node; 02268 } else { 02269 result = f->mgr->vars[Cudd_Regular(f->node)->index]; 02270 } 02271 cuddRef(result); 02272 return(bdd_construct_bdd_t(f->mgr,result)); 02273 02274 } /* end of bdd_top_var */
| bdd_variableId bdd_top_var_id | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [Accesses the id of the top variable.]
SideEffects []
Definition at line 3153 of file cuPort.c.
03154 { 03155 return(Cudd_Regular(f->node)->index); 03156 03157 } /* end of bdd_top_var_id */
| long bdd_top_var_level | ( | bdd_manager * | mgr, | |
| bdd_t * | fn | |||
| ) |
Function********************************************************************
Synopsis [Gets the level of the top variable of the BDD.]
SideEffects []
Definition at line 3531 of file cuPort.c.
03532 { 03533 return((long) cuddI((DdManager *)mgr,Cudd_Regular(fn->node)->index)); 03534 03535 } /* end of bdd_top_var_level */
| int bdd_unbind_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Allows the sifting of a variable.]
Description [This function resets the flag that prevents the sifting of a variable. In successive variable reorderings, the variable will NOT be skipped, that is, sifted. Initially all variables can be sifted. It is necessary to call this function only to re-enable sifting after a call to Cudd_bddBindVar. Returns 1 if successful; 0 otherwise (i.e., invalid variable index).]
SideEffects [Changes the "bindVar" flag in DdSubtable.]
Definition at line 7366 of file cuPort.c.
07367 { 07368 return Cudd_bddUnbindVar((DdManager *) mgr, index); 07369 07370 } /* end of bdd_unbind_var */
| bdd_node* bdd_unique_inter | ( | bdd_manager * | mgr, | |
| int | v, | |||
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Returns a bdd_node whose index is v and g and h as its children.]
Description [Returns a bdd_node whose index is v and g and h as its children. Returns the bdd_node after success. The reference count of the returned BDD is not incremented. Returns NULL in case of reordering or if memory is exhausted.]
SideEffects [none]
| bdd_node* bdd_unique_inter_ivo | ( | bdd_manager * | mgr, | |
| int | v, | |||
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Returns a bdd_node whose index is v and f and g as its children.]
Description [Returns a bdd_node whose index is v and f and g as its children. Returns the bdd_node after success. The reference count of the returned BDD is not incremented. Returns NULL in case of reordering or if memory is exhausted.]
SideEffects [none]
Definition at line 5321 of file cuPort.c.
05326 { 05327 DdNode *result; 05328 DdNode *t; 05329 05330 t = cuddUniqueInter((DdManager *)mgr, v, (DdNode *)bdd_read_one(mgr), 05331 (DdNode *)bdd_not_bdd_node(bdd_read_one(mgr))); 05332 if (t == NULL) 05333 return(NULL); 05334 Cudd_Ref(t); 05335 result = cuddBddIteRecur((DdManager *)mgr, t, (DdNode *)f, (DdNode *)g); 05336 Cudd_RecursiveDeref((DdManager *)mgr,(DdNode *)t); 05337 return(result); 05338 05339 } /* end of bdd_unique_inter_ivo */
Function********************************************************************
Synopsis [Computes the cofactor of f with respect to g.]
SideEffects []
Definition at line 1160 of file cuPort.c.
01161 { 01162 DdNode *result; 01163 01164 /* Make sure both operands belong to the same manager */ 01165 assert(f->mgr == g->mgr); 01166 01167 result = Cudd_Cofactor(f->mgr,f->node, 01168 g->node); 01169 if (result == NULL) return(NULL); 01170 cuddRef(result); 01171 return(bdd_construct_bdd_t(f->mgr,result)); 01172 01173 } /* end of bdd_var_cofactor */
| int bdd_var_decomp | ( | bdd_t * | f, | |
| bdd_partition_type_t | partType, | |||
| bdd_t *** | conjArray | |||
| ) |
Function********************************************************************
Synopsis [Computes 2 partitions of a function.]
Description [Computes 2 partitions of a function. Method based on Cabodi 94. Picks a var and replaces one child in each conjunct with 1 (0). returns 2 conjuncts(disjuncts).]
SideEffects []
Definition at line 6212 of file cuPort.c.
06213 { 06214 DdNode **ddArray = NULL; 06215 int i, num = 0; 06216 bdd_t *result; 06217 06218 switch (partType) { 06219 case BDD_CONJUNCTS: 06220 num = Cudd_bddVarConjDecomp(f->mgr, f->node, &ddArray); 06221 break; 06222 case BDD_DISJUNCTS: 06223 num = Cudd_bddVarDisjDecomp(f->mgr, f->node, &ddArray); 06224 break; 06225 } 06226 if ((ddArray == NULL) || (!num)) { 06227 return 0; 06228 } 06229 06230 *conjArray = ALLOC(bdd_t *, num); 06231 if ((*conjArray) == NULL) goto outOfMem; 06232 for (i = 0; i < num; i++) { 06233 result = ALLOC(bdd_t, 1); 06234 if (result == NULL) { 06235 FREE(*conjArray); 06236 goto outOfMem; 06237 } 06238 result->mgr = f->mgr; 06239 result->node = (ddArray)[i]; 06240 result->free = FALSE; 06241 (*conjArray)[i] = result; 06242 } 06243 FREE(ddArray); 06244 return (num); 06245 06246 outOfMem: 06247 for (i = 0; i < num; i++) { 06248 Cudd_RecursiveDeref((DdManager *)f->mgr,(DdNode *)ddArray[i]); 06249 } 06250 FREE(ddArray); 06251 return(0); 06252 06253 } /* end of bdd_var_decomp */
Function********************************************************************
Synopsis [Checks whether a variable is dependent on others in a function f. Returns 1 if it is, else 0. ]
SideEffects []
| bdd_t* bdd_var_with_index | ( | bdd_manager * | manager, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Function that creates a variable of a given index.]
SideEffects []
Definition at line 3604 of file cuPort.c.
03605 { 03606 DdNode *var; 03607 03608 var = Cudd_bddIthVar((DdManager *) manager, index); 03609 cuddRef(var); 03610 return(bdd_construct_bdd_t(manager, var)); 03611 03612 } /* end of bdd_var_with_index */
Function********************************************************************
Synopsis [Composes a BDD with a vector of BDDs. Given a vector of BDDs, creates a new BDD by substituting the BDDs for the variables of the BDD f.]
SideEffects []
Definition at line 1270 of file cuPort.c.
01271 { 01272 int i, n, nVars, index; 01273 bdd_t *var, *func; 01274 DdNode *result; 01275 DdNode **vector; 01276 01277 assert(array_n(varArray) == array_n(funcArray)); 01278 n = array_n(varArray); 01279 nVars = ((DdManager *)f->mgr)->size; 01280 vector = ALLOC(DdNode *, sizeof(DdNode *) * nVars); 01281 memset(vector, 0, sizeof(DdNode *) * nVars); 01282 01283 for (i = 0; i < n; i++) { 01284 var = array_fetch(bdd_t *, varArray, i); 01285 func = array_fetch(bdd_t *, funcArray, i); 01286 index = (int)bdd_top_var_id(var); 01287 vector[index] = (DdNode *)func->node; 01288 cuddRef(vector[index]); 01289 } 01290 for (i = 0; i < nVars; i++) { 01291 if (!vector[i]) { 01292 vector[i] = Cudd_bddIthVar((DdManager *)f->mgr, i); 01293 cuddRef(vector[i]); 01294 } 01295 } 01296 01297 result = Cudd_bddVectorCompose(f->mgr, f->node, vector); 01298 01299 for (i = 0; i < nVars; i++) 01300 Cudd_RecursiveDeref((DdManager *)f->mgr, vector[i]); 01301 FREE(vector); 01302 if (result == NULL) return(NULL); 01303 cuddRef(result); 01304 return(bdd_construct_bdd_t(f->mgr,result)); 01305 01306 } /* end of bdd_vector_compose */
| bdd_node* bdd_xeqy | ( | bdd_manager * | mgr, | |
| int | N, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y | |||
| ) |
Function********************************************************************
Synopsis [Generates a BDD for the function x==y.]]
SideEffects []
| bdd_node* bdd_xgty | ( | bdd_manager * | mgr, | |
| int | N, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y | |||
| ) |
Function********************************************************************
Synopsis [Generates a BDD for the function x > y.]
Description [This function generates a BDD for the function x > y. Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. The BDD is built bottom-up. It has 3*N-1 internal nodes, if the variables are ordered as follows: x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].]
SideEffects [None]
SeeAlso [bdd_dxygtdxz]
Function********************************************************************
Synopsis [Computes the exclusive nor of two BDDs.]
SideEffects []
Definition at line 2285 of file cuPort.c.
02286 { 02287 DdNode *result; 02288 02289 /* Make sure both operands belong to the same manager. */ 02290 assert(f->mgr == g->mgr); 02291 02292 result = Cudd_bddXnor(f->mgr,f->node,g->node); 02293 if (result == NULL) return(NULL); 02294 cuddRef(result); 02295 return(bdd_construct_bdd_t(f->mgr,result)); 02296 02297 } /* end of bdd_xnor */
Function********************************************************************
Synopsis [Computes the exclusive or of two BDDs.]
SideEffects []
Definition at line 2308 of file cuPort.c.
02309 { 02310 DdNode *result; 02311 02312 /* Make sure both operands belong to the same manager. */ 02313 assert(f->mgr == g->mgr); 02314 02315 result = Cudd_bddXor(f->mgr,f->node,g->node); 02316 if (result == NULL) return(NULL); 02317 cuddRef(result); 02318 return(bdd_construct_bdd_t(f->mgr,result)); 02319 02320 } /* end of bdd_xor */
Function********************************************************************
Synopsis [Abstracts variables from the exclusive OR of two BDDs.]
SideEffects []
Definition at line 935 of file cuPort.c.
00939 { 00940 int i; 00941 bdd_t *variable; 00942 DdNode *cube,*tmpDd,*result; 00943 DdManager *mgr; 00944 00945 /* Make sure both operands belong to the same manager. */ 00946 assert(f->mgr == g->mgr); 00947 00948 /* The Boulder package needs the smothing variables passed as a cube. 00949 * Therefore we must build that cube from the indices of variables 00950 * in the array before calling the procedure. 00951 */ 00952 mgr = f->mgr; 00953 Cudd_Ref(cube = DD_ONE(mgr)); 00954 for (i = 0; i < array_n(smoothing_vars); i++) { 00955 variable = array_fetch(bdd_t *,smoothing_vars,i); 00956 00957 /* Make sure the variable belongs to the same manager. */ 00958 assert(mgr == variable->mgr); 00959 00960 tmpDd = Cudd_bddAnd(mgr,cube,variable->node); 00961 if (tmpDd == NULL) { 00962 Cudd_RecursiveDeref(mgr,cube); 00963 return(NULL); 00964 } 00965 cuddRef(tmpDd); 00966 Cudd_RecursiveDeref(mgr, cube); 00967 cube = tmpDd; 00968 } 00969 00970 /* Perform the smoothing */ 00971 result = Cudd_bddXorExistAbstract(mgr,f->node,g->node,cube); 00972 if (result == NULL) { 00973 Cudd_RecursiveDeref(mgr, cube); 00974 return(NULL); 00975 } 00976 cuddRef(result); 00977 /* Get rid of temporary results. */ 00978 Cudd_RecursiveDeref(mgr, cube); 00979 00980 /* Build the bdd_t structure for the result */ 00981 return(bdd_construct_bdd_t(mgr,result)); 00982 00983 } /* end of bdd_xor_smooth */
| bdd_node* bdd_zdd_complement | ( | bdd_manager * | mgr, | |
| bdd_node * | node | |||
| ) |
Function********************************************************************
Synopsis [Computes the complement of a ZDD cover.]
SideEffects []
Definition at line 6895 of file cuPort.c.
06896 { 06897 return((bdd_node *)Cudd_zddComplement((DdManager *)mgr, (DdNode *)node)); 06898 06899 } /* end of bdd_zdd_complement */
| int bdd_zdd_count | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
Function********************************************************************
Synopsis [Count the number of mintems of a ZDD.]
Description [Count the number of mintems of a ZDD.]
SideEffects []
Definition at line 5539 of file cuPort.c.
05540 { 05541 return(Cudd_zddCount((DdManager *)mgr, (DdNode *)f)); 05542 05543 } /* end of bdd_zdd_count */
| bdd_node* bdd_zdd_diff | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Computes the set difference of two ZDDs.]
Description [Computes the set difference of two ZDDs. Returns a pointer to the result if successful. The reference count of the result is not incremented. NULL is returned in case of re-ordering of if memory is exhausted.]
SideEffects [none]
| bdd_node* bdd_zdd_diff_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Computes the set difference of two ZDDs.]
Description [Computes the set difference of two ZDDs. Returns a pointer to the result if successful. The reference count of the result is not incremented. NULL is returned in case of re-ordering of if memory is exhausted.]
SideEffects [none]
| int bdd_zdd_get_cofactors3 | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| int | v, | |||
| bdd_node ** | f1, | |||
| bdd_node ** | f0, | |||
| bdd_node ** | fd | |||
| ) |
Function********************************************************************
Synopsis [Computes the three-way decomposition of f w.r.t. v.]
Description [Computes the three-way decomposition of function f (represented by a ZDD) w.r.t respect to variable v. Returns 1 on failure, 0 on success. Reference counts of f1, f0 and fd are not incremented. ]
SideEffects [The results are returned in f1, f0, and fd. They are NULL in case of failure.]
| bdd_node* bdd_zdd_get_node | ( | bdd_manager * | mgr, | |
| int | id, | |||
| bdd_node * | g, | |||
| bdd_node * | h | |||
| ) |
Function********************************************************************
Synopsis [Returns a zdd node with index i and g and h as its children.]
SideEffects []
| bdd_node* bdd_zdd_isop | ( | bdd_manager * | mgr, | |
| bdd_node * | L, | |||
| bdd_node * | U, | |||
| bdd_node ** | zdd_I | |||
| ) |
Function********************************************************************
Synopsis [Computes an irredundant sum of products (ISOP) in ZDD form from BDDs. This is an interface to an external function.]
SideEffects [zdd_I holds the pointer to the ZDD for the ISOP on successful return.]
SeeAlso [bdd_zdd_isop_recur]
| bdd_node* bdd_zdd_isop_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | L, | |||
| bdd_node * | U, | |||
| bdd_node ** | zdd_I | |||
| ) |
Function********************************************************************
Synopsis [Computes an irredundant sum of products (ISOP) in ZDD form from BDDs. This is a recursive procedure. Returns the pointer to the ZDD on success. Reference count of the result is not incremented. NULL in the case of re-ordering or if memory is exhausted.]
SideEffects [zdd_I holds the pointer to the ZDD for the ISOP on successful return.]
| bdd_node* bdd_zdd_product | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Computes the product of two cover represented by ZDDs. The covers on which bdd_zdd_product operates use two ZDD variables for each function variable (one ZDD variable for each literal of the variable). Those two ZDD variables should be adjacent in the order.]
SideEffects []
| bdd_node* bdd_zdd_product_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Computes the product of two cover represented by ZDDs. The covers on which bdd_zdd_product_recur operates use two ZDD variables for each function variable (one ZDD variable for each literal of the variable). Those two ZDD variables should be adjacent in the order. This is a recursive procedure. It returns the ZDD of the product if successful. Reference count of the result is not incremented. NULL is returned if re-ordering takes place or if memory is exhausted.]
SideEffects []
| void bdd_zdd_realign_disable | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Disables the alignment of ZDD vars with that of corresponding BDD vars.]
Description [Disables the alignment of ZDD vars with that of corresponding BDD vars.]
SideEffects []
Definition at line 5621 of file cuPort.c.
05622 { 05623 Cudd_zddRealignDisable((DdManager *)mgr); 05624 05625 } /* end of bdd_zdd_realign_disable */
| void bdd_zdd_realign_enable | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Enables the alignment of ZDD vars with that of corresponding BDD vars.]
Description [Enables the alignment of ZDD vars with that of corresponding BDD vars.]
SideEffects []
Definition at line 5602 of file cuPort.c.
05603 { 05604 Cudd_zddRealignEnable((DdManager *)mgr); 05605 05606 } /* end of bdd_zdd_realign_enable */
| int bdd_zdd_realignment_enabled | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns the value of the variable for the alignment of ZDD vars with that of corresponding BDD vars.]
Description [Returns the value of the variable for the alignment of ZDD vars with that of corresponding BDD vars.]
SideEffects []
Definition at line 5640 of file cuPort.c.
05641 { 05642 return(Cudd_zddRealignmentEnabled((DdManager *)mgr)); 05643 05644 } /* end of bdd_zdd_realignment_enabled */
| bdd_node* bdd_zdd_union | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Computes the union of two ZDDs.]
Description [Computes the union of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects []
| bdd_node* bdd_zdd_union_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Computes the union of two ZDDs.]
Description [Computes the union of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects []
| int bdd_zdd_vars_from_bdd_vars | ( | bdd_manager * | mgr, | |
| int | multiplicity | |||
| ) |
Function********************************************************************
Synopsis [Creates multiplicity number of ZDD vars for each BDD var.]
Description [Creates one or more ZDD variables for each BDD variable. If some ZDD variables already exist, only the missing variables are created. Parameter multiplicity allows the caller to control how many variables are created for each BDD variable in existence. For instance, if ZDDs are used to represent covers, two ZDD variables are required for each BDD variable. The order of the BDD variables is transferred to the ZDD variables. If a variable group tree exists for the BDD variables, a corresponding ZDD variable group tree is created by expanding the BDD variable tree. In any case, the ZDD variables derived from the same BDD variable are merged in a ZDD variable group. If a ZDD variable group tree exists, it is freed. Returns 1 if successful; 0 otherwise.]
SideEffects []
Definition at line 5583 of file cuPort.c.
05584 { 05585 return(Cudd_zddVarsFromBddVars((DdManager *)mgr, multiplicity)); 05586 05587 } /* end of bdd_zdd_vars_from_bdd_vars */
| bdd_node* bdd_zdd_weak_div | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Applies weak division to two ZDDs representing two covers. The result of weak division depends on the variable order. The covers on which bdd_zdd_weak_div operates use two ZDD variables for each function variable (one ZDD variable for each literal of the variable). Those two ZDD variables should be adjacent in the order.]
SideEffects []
| bdd_node* bdd_zdd_weak_div_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [Applies weak division to two ZDDs representing two covers. The result of weak division depends on the variable order. The covers on which bdd_zdd_weak_div_recur operates use two ZDD variables for each function variable (one ZDD variable for each literal of the variable). Those two ZDD variables should be adjacent in the order. This is a recursive procedure. It returns a pointer to the result if successful; Reference count of the result is not incremented. NULL is returned if re-ordering takes place or if memory is exhausted.]
SideEffects []
| bdd_t* bdd_zero | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [Returns the constant logical zero BDD.]
SideEffects [bdd_read_zero]
| static void InvalidType | ( | FILE * | file, | |
| const char * | field, | |||
| const char * | expected | |||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Function to print a warning that an illegal value was read.]
SideEffects []
SeeAlso [bdd_set_parameters]
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuPort.c,v 1.132 2009/04/11 23:44:57 fabio Exp $" [static] |
CFile***********************************************************************
FileName [cuPort.c]
PackageName [cudd]
Synopsis [SIS/VIS interface to the Decision Diagram Package of the University of Colorado.]
Description [This file implements an interface between the functions in the Berkeley BDD package and the functions provided by the CUDD (decision diagram) package from the University of Colorado. The CUDD package is a generic implementation of a decision diagram data structure. For the time being, only Boole expansion is implemented and the leaves in the in the nodes can be the constants zero, one or any arbitrary value.]
Author [Abelardo Pardo, Kavita Ravi]
Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
