src/calPort/calPort.c File Reference
#include "calPortInt.h"#include "epd.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 | |||
| ) |
| bdd_node* bdd_add_apply_recur | ( | bdd_manager * | mgr, | |
| bdd_node *(*)(bdd_manager *, bdd_node **, bdd_node **) | operation, | |||
| bdd_node * | fn1, | |||
| bdd_node * | fn2 | |||
| ) |
| bdd_node* bdd_add_bdd_strict_threshold | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| BDD_VALUE_TYPE | value | |||
| ) |
| bdd_node* bdd_add_bdd_threshold | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| BDD_VALUE_TYPE | value | |||
| ) |
| bdd_node* bdd_add_cmpl | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
| bdd_node* bdd_add_compose | ( | bdd_manager * | mgr, | |
| bdd_node * | fn1, | |||
| bdd_node * | fn2, | |||
| int | var | |||
| ) |
| bdd_node* bdd_add_compute_cube | ( | bdd_manager * | mgr, | |
| bdd_node ** | vars, | |||
| int * | phase, | |||
| int | n | |||
| ) |
| bdd_node* bdd_add_const | ( | bdd_manager * | mgr, | |
| BDD_VALUE_TYPE | c | |||
| ) |
| bdd_node* bdd_add_divide | ( | bdd_manager * | mgr, | |
| bdd_node ** | fn1, | |||
| bdd_node ** | fn2 | |||
| ) |
| bdd_node* bdd_add_exist_abstract | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node * | vars | |||
| ) |
| bdd_node* bdd_add_find_max | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
| bdd_node* bdd_add_general_vector_compose | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | vectorOn, | |||
| bdd_node ** | vectorOff | |||
| ) |
| bdd_node* bdd_add_hamming | ( | bdd_manager * | mgr, | |
| bdd_node ** | xVars, | |||
| bdd_node ** | yVars, | |||
| int | nVars | |||
| ) |
| int bdd_add_hook | ( | bdd_manager * | mgr, | |
| int(*)(bdd_manager *, char *, void *) | procedure, | |||
| bdd_hook_type_t | whichHook | |||
| ) |
| bdd_node* bdd_add_ite | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g, | |||
| bdd_node * | h | |||
| ) |
| bdd_node* bdd_add_ith_var | ( | bdd_manager * | mgr, | |
| int | i | |||
| ) |
| bdd_node* bdd_add_matrix_multiply | ( | bdd_manager * | mgr, | |
| bdd_node * | A, | |||
| bdd_node * | B, | |||
| bdd_node ** | z, | |||
| int | nz | |||
| ) |
| bdd_node* bdd_add_minus | ( | bdd_manager * | mgr, | |
| bdd_node ** | fn1, | |||
| bdd_node ** | fn2 | |||
| ) |
| bdd_node* bdd_add_nonsim_compose | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node ** | vector | |||
| ) |
| bdd_node* bdd_add_permute | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| int * | permut | |||
| ) |
| bdd_node* bdd_add_plus | ( | bdd_manager * | mgr, | |
| bdd_node ** | fn1, | |||
| bdd_node ** | fn2 | |||
| ) |
| bdd_node* bdd_add_residue | ( | bdd_manager * | mgr, | |
| int | n, | |||
| int | m, | |||
| int | options, | |||
| int | top | |||
| ) |
| bdd_node* bdd_add_roundoff | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| int | N | |||
| ) |
| bdd_node* bdd_add_swap_variables | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y, | |||
| int | n | |||
| ) |
| bdd_node* bdd_add_times | ( | bdd_manager * | mgr, | |
| bdd_node ** | fn1, | |||
| bdd_node ** | fn2 | |||
| ) |
| BDD_VALUE_TYPE bdd_add_value | ( | bdd_node * | f | ) |
| bdd_node* bdd_add_vector_compose | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node ** | vector | |||
| ) |
| bdd_node* bdd_add_xnor | ( | bdd_manager * | mgr, | |
| bdd_node ** | fn1, | |||
| bdd_node ** | fn2 | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 311 of file calPort.c.
00312 { 00313 Cal_Bdd temp1, temp2; 00314 bdd_t *result; 00315 Cal_BddManager mgr; 00316 00317 mgr = f->bddManager; 00318 temp1 = ((f_phase == TRUE) ? Cal_BddIdentity(mgr, f->calBdd) : 00319 Cal_BddNot(mgr, f->calBdd)); 00320 temp2 = ((g_phase == TRUE) ? Cal_BddIdentity(mgr, g->calBdd) : 00321 Cal_BddNot(mgr, g->calBdd)); 00322 result = bdd_construct_bdd_t(mgr, Cal_BddAnd(mgr, temp1, temp2)); 00323 Cal_BddFree(mgr, temp1); 00324 Cal_BddFree(mgr, temp2); 00325 return result; 00326 }
Definition at line 346 of file calPort.c.
00347 { 00348 Cal_Bdd temp1, temp2, result; 00349 bdd_t *g; 00350 Cal_BddManager mgr; 00351 int i; 00352 00353 mgr = f->bddManager; 00354 result = ((f_phase == TRUE) ? Cal_BddIdentity(mgr, f->calBdd) : 00355 Cal_BddNot(mgr, f->calBdd)); 00356 00357 for (i = 0; i < array_n(g_array); i++) { 00358 g = array_fetch(bdd_t *, g_array, i); 00359 temp1 = result; 00360 temp2 = ((g_phase == TRUE) ? Cal_BddIdentity(mgr, g->calBdd) : 00361 Cal_BddNot(mgr, g->calBdd)); 00362 result = Cal_BddAnd(mgr, temp1, temp2); 00363 Cal_BddFree(mgr, temp1); 00364 Cal_BddFree(mgr, temp2); 00365 if (result == NULL) 00366 return(NULL); 00367 } 00368 00369 return(bdd_construct_bdd_t(mgr, result)); 00370 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 603 of file calPort.c.
00604 { 00605 int num_vars, i; 00606 bdd_t *fn, *result; 00607 Cal_Bdd *assoc; 00608 Cal_BddManager mgr; 00609 int assocId; 00610 00611 num_vars = array_n(smoothingVars); 00612 if (num_vars == 0) { 00613 fprintf(stderr,"bdd_and_smooth: no smoothing variables"); 00614 return bdd_and(f, g, 1, 1); 00615 } 00616 mgr = f->bddManager; 00617 assoc = Cal_MemAlloc(Cal_Bdd, num_vars+1); 00618 for (i = 0; i < num_vars; i++) { 00619 fn = array_fetch(bdd_t *, smoothingVars, i); 00620 assoc[i] = fn->calBdd; 00621 } 00622 assoc[num_vars] = 0; 00623 assocId = Cal_AssociationInit(mgr, assoc, 0); 00624 Cal_AssociationSetCurrent(mgr, assocId); 00625 result = bdd_construct_bdd_t(mgr, Cal_BddRelProd(mgr, f->calBdd, g->calBdd)); 00626 Cal_MemFree(assoc); 00627 return result; 00628 }
| bdd_t* bdd_and_smooth_with_limit | ( | bdd_t * | f, | |
| bdd_t * | g, | |||
| array_t * | smoothingVars, | |||
| unsigned int | limit | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [Unsupported: Fall back to standard and_smooth]
SideEffects [required]
SeeAlso [bdd_and_smooth]
Definition at line 642 of file calPort.c.
00643 { 00644 return bdd_and_smooth(f, g, smoothingVars); 00645 }
| 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 BDDs with limit on nodes created]
Description [AND of BDDs with limit on nodes created. This function is not supported by the CAL package. We fall back to the standard AND.]
SideEffects [required]
SeeAlso [bdd_and]
Definition at line 340 of file calPort.c.
00341 { 00342 return bdd_and(f, g, f_phase, g_phase); 00343 }
| bdd_t* bdd_approx_biased_rua | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| bdd_t * | bias, | |||
| int | numVars, | |||
| int | threshold, | |||
| double | quality, | |||
| double | quality1 | |||
| ) |
| bdd_t* bdd_approx_compress | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| int | numVars, | |||
| int | threshold | |||
| ) |
| int bdd_approx_decomp | ( | bdd_t * | f, | |
| bdd_partition_type_t | partType, | |||
| bdd_t *** | conjArray | |||
| ) |
| bdd_t* bdd_approx_hb | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| int | numVars, | |||
| int | threshold | |||
| ) |
| bdd_t* bdd_approx_remap_ua | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| int | numVars, | |||
| int | threshold, | |||
| double | quality | |||
| ) |
| bdd_t* bdd_approx_sp | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| int | numVars, | |||
| int | threshold, | |||
| int | hardlimit | |||
| ) |
| bdd_t* bdd_approx_ua | ( | bdd_t * | f, | |
| bdd_approx_dir_t | approxDir, | |||
| int | numVars, | |||
| int | threshold, | |||
| int | safe, | |||
| double | quality | |||
| ) |
| bdd_node* bdd_bdd_and | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_bdd_and_abstract | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g, | |||
| bdd_node * | cube | |||
| ) |
| bdd_node* bdd_bdd_and_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_bdd_boolean_diff | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| int | x | |||
| ) |
| bdd_node* bdd_bdd_cofactor | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_bdd_compute_cube | ( | bdd_manager * | mgr, | |
| bdd_node ** | vars, | |||
| int * | phase, | |||
| int | n | |||
| ) |
| bdd_node* bdd_bdd_constrain | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | c | |||
| ) |
| bdd_node* bdd_bdd_cprojection | ( | bdd_manager * | mgr, | |
| bdd_node * | R, | |||
| bdd_node * | Y | |||
| ) |
| bdd_node* bdd_bdd_exist_abstract | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node * | cube | |||
| ) |
| bdd_node* bdd_bdd_ite | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g, | |||
| bdd_node * | h | |||
| ) |
| bdd_node* bdd_bdd_ith_var | ( | bdd_manager * | mgr, | |
| int | i | |||
| ) |
| int bdd_bdd_leq | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_bdd_new_var | ( | bdd_manager * | mgr | ) |
| bdd_node* bdd_bdd_or | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_bdd_permute | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| int * | permut | |||
| ) |
| int bdd_bdd_pick_one_cube | ( | bdd_manager * | mgr, | |
| bdd_node * | node, | |||
| char * | string | |||
| ) |
| bdd_node* bdd_bdd_pick_one_minterm | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | vars, | |||
| int | n | |||
| ) |
| bdd_node* bdd_bdd_restrict | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | c | |||
| ) |
| bdd_node* bdd_bdd_support | ( | bdd_manager * | mgr, | |
| bdd_node * | F | |||
| ) |
| int bdd_bdd_support_size | ( | bdd_manager * | mgr, | |
| bdd_node * | F | |||
| ) |
| bdd_node* bdd_bdd_swap_variables | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y, | |||
| int | n | |||
| ) |
| bdd_node* bdd_bdd_to_add | ( | bdd_manager * | mgr, | |
| bdd_node * | fn | |||
| ) |
| bdd_node* bdd_bdd_univ_abstract | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node * | vars | |||
| ) |
| bdd_node* bdd_bdd_vector_compose | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | vector | |||
| ) |
| bdd_node* bdd_bdd_vector_support | ( | bdd_manager * | mgr, | |
| bdd_node ** | F, | |||
| int | n | |||
| ) |
| int bdd_bdd_vector_support_size | ( | bdd_manager * | mgr, | |
| bdd_node ** | F, | |||
| int | n | |||
| ) |
| bdd_node* bdd_bdd_xnor | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_bdd_xor | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 658 of file calPort.c.
00659 { 00660 return bdd_construct_bdd_t(fMin->bddManager, 00661 Cal_BddBetween(fMin->bddManager, 00662 fMin->calBdd, 00663 fMax->calBdd)); 00664 }
| int bdd_bind_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_check_zero_ref | ( | bdd_manager * | mgr | ) |
| double* bdd_cof_minterm | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 676 of file calPort.c.
00677 { 00678 return bdd_construct_bdd_t(f->bddManager, 00679 Cal_BddCofactor(f->bddManager, 00680 f->calBdd, 00681 g->calBdd)); 00682 }
Definition at line 685 of file calPort.c.
00686 { 00687 bdd_t *operand; 00688 Cal_Bdd result, temp; 00689 int i; 00690 00691 result = Cal_BddIdentity(f->bddManager, f->calBdd); 00692 00693 for (i = 0; i < array_n(bddArray); i++) { 00694 operand = array_fetch(bdd_t *, bddArray, i); 00695 temp = Cal_BddCofactor(f->bddManager, result, operand->calBdd); 00696 if (temp == NULL) { 00697 Cal_BddFree(f->bddManager, result); 00698 return(NULL); 00699 } 00700 Cal_BddFree(f->bddManager, result); 00701 result = temp; 00702 } 00703 00704 return(bdd_construct_bdd_t(f->bddManager, result)); 00705 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 718 of file calPort.c.
00719 { 00720 return bdd_construct_bdd_t(f->bddManager, 00721 Cal_BddCompose(f->bddManager, 00722 f->calBdd, 00723 v->calBdd, 00724 g->calBdd)); 00725 }
| bdd_t* bdd_compute_cube | ( | bdd_manager * | mgr, | |
| array_t * | vars | |||
| ) |
| bdd_t* bdd_compute_cube_with_phase | ( | bdd_manager * | mgr, | |
| array_t * | vars, | |||
| array_t * | phase | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 738 of file calPort.c.
00739 { 00740 int num_vars, i; 00741 bdd_t *fn, *result; 00742 Cal_Bdd *assoc; 00743 Cal_BddManager mgr; 00744 00745 num_vars = array_n(quantifyingVars); 00746 if (num_vars == 0) { 00747 fprintf(stderr, "bdd_consensus: no smoothing variables"); 00748 return f; 00749 } 00750 mgr = f->bddManager; 00751 assoc = Cal_MemAlloc(Cal_Bdd, num_vars+1); 00752 for (i = 0; i < num_vars; i++) { 00753 fn = array_fetch(bdd_t *, quantifyingVars, i); 00754 assoc[i] = fn->calBdd; 00755 } 00756 assoc[num_vars] = 0; 00757 Cal_TempAssociationInit(mgr, assoc, 0); 00758 Cal_AssociationSetCurrent(mgr, -1); 00759 result = bdd_construct_bdd_t(mgr, Cal_BddForAll(mgr, f->calBdd)); 00760 Cal_MemFree(assoc); 00761 Cal_TempAssociationQuit(mgr); 00762 return result; 00763 }
| bdd_t* bdd_construct_bdd_t | ( | bdd_manager * | mgr, | |
| bdd_node * | fn | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Function to construct a bdd_t.]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 92 of file calPort.c.
00093 { 00094 bdd_t *result; 00095 if (!fn){ 00096 fail("bdd_construct_bdd_t: possible memory overflow"); 00097 } 00098 result = Cal_MemAlloc(bdd_t, 1); 00099 result->bddManager = (Cal_BddManager_t *) mgr; 00100 result->calBdd = (Cal_Bdd) fn; 00101 result->free = 0; 00102 return result; 00103 }
| double bdd_count_minterm | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1355 of file calPort.c.
01356 { 01357 int numVars; 01358 double fraction; 01359 numVars = array_n(var_array); 01360 fraction = Cal_BddSatisfyingFraction(f->bddManager, f->calBdd); 01361 return (fraction * pow((double) 2, (double) numVars)); 01362 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 776 of file calPort.c.
00777 { 00778 return NIL(bdd_t); 00779 00780 /* 00781 int num_vars, i; 00782 bdd_t *fn, *result; 00783 Cal_Bdd_t*assoc; 00784 Cal_BddManager mgr; 00785 00786 if (f == NIL(bdd_t)) 00787 fail ("bdd_cproject: invalid BDD"); 00788 00789 num_vars = array_n(quantifying_vars); 00790 if (num_vars <= 0) { 00791 printf("Warning: bdd_cproject: no projection variables\n"); 00792 result = bdd_dup(f); 00793 } 00794 else { 00795 assoc = Cal_MemAlloc(Cal_Bdd_t, num_vars+1); 00796 for (i = 0; i < num_vars; i++) { 00797 fn = array_fetch(bdd_t *, quantifying_vars, i); 00798 assoc[i] = fn->calBdd; 00799 } 00800 assoc[num_vars] = (struct bdd_ *) 0; 00801 mgr = f->bddManager; 00802 cmu_bdd_temp_assoc(mgr, assoc, 0); 00803 (void) cmu_bdd_assoc(mgr, -1); 00804 result = bdd_construct_bdd_t(mgr, cmu_bdd_project(mgr, f->calBdd)); 00805 Cal_MemFree(assoc); 00806 } 00807 return result; 00808 */ 00809 }
| bdd_t* bdd_create_variable | ( | bdd_manager * | manager | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 180 of file calPort.c.
00181 { 00182 Cal_BddManager mgr = (Cal_BddManager) manager; 00183 return bdd_construct_bdd_t(mgr, Cal_BddManagerCreateNewVarLast(mgr)); 00184 }
| bdd_t* bdd_create_variable_after | ( | bdd_manager * | manager, | |
| bdd_variableId | afterId | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 197 of file calPort.c.
00198 { 00199 Cal_Bdd afterVar; 00200 bdd_t *result; 00201 Cal_BddManager mgr = (Cal_BddManager) manager; 00202 afterVar = Cal_BddManagerGetVarWithId(mgr, afterId + 1); 00203 result = bdd_construct_bdd_t(mgr, 00204 Cal_BddManagerCreateNewVarAfter(mgr, 00205 afterVar)); 00206 00207 /* No need to free after_var, since single variable BDDs are never garbage collected */ 00208 00209 return result; 00210 }
| int bdd_debug_check | ( | bdd_manager * | mgr | ) |
| void bdd_deref | ( | bdd_node * | f | ) |
| int bdd_disable_reordering_reporting | ( | bdd_manager * | mgr | ) |
| void bdd_discard_all_var_groups | ( | bdd_manager * | mgr | ) |
| void bdd_dump_blif | ( | bdd_manager * | mgr, | |
| int | nBdds, | |||
| bdd_node ** | bdds, | |||
| char ** | inames, | |||
| char ** | onames, | |||
| char * | model, | |||
| FILE * | fp | |||
| ) |
| void bdd_dump_blif_body | ( | bdd_manager * | mgr, | |
| int | nBdds, | |||
| bdd_node ** | bdds, | |||
| char ** | inames, | |||
| char ** | onames, | |||
| FILE * | fp | |||
| ) |
| void bdd_dump_dot | ( | bdd_manager * | mgr, | |
| int | nBdds, | |||
| bdd_node ** | bdds, | |||
| char ** | inames, | |||
| char ** | onames, | |||
| FILE * | fp | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 252 of file calPort.c.
00253 { 00254 return bdd_construct_bdd_t(f->bddManager, Cal_BddIdentity(f->bddManager, f->calBdd)); 00255 }
| bdd_node* bdd_dxygtdxz | ( | bdd_manager * | mgr, | |
| int | N, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y, | |||
| bdd_node ** | z | |||
| ) |
| void bdd_dynamic_reordering | ( | bdd_manager * | manager, | |
| bdd_reorder_type_t | algorithm_type, | |||
| bdd_reorder_verbosity_t | verbosity | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1716 of file calPort.c.
01718 { 01719 Cal_BddManager mgr = (Cal_BddManager) manager; 01720 switch(algorithm_type) { 01721 case BDD_REORDER_SIFT: 01722 Cal_BddDynamicReordering(mgr, CAL_REORDER_SIFT); 01723 break; 01724 case BDD_REORDER_WINDOW: 01725 Cal_BddDynamicReordering(mgr, CAL_REORDER_WINDOW); 01726 break; 01727 case BDD_REORDER_NONE: 01728 Cal_BddDynamicReordering(mgr, CAL_REORDER_NONE); 01729 break; 01730 default: 01731 fprintf(stderr,"CAL: bdd_dynamic_reordering: unknown algorithm type\n"); 01732 fprintf(stderr,"Using SIFT method instead\n"); 01733 Cal_BddDynamicReordering(mgr, CAL_REORDER_SIFT); 01734 } 01735 01736 }
| void bdd_dynamic_reordering_disable | ( | bdd_manager * | mgr | ) |
| void bdd_dynamic_reordering_zdd | ( | bdd_manager * | manager, | |
| bdd_reorder_type_t | algorithm_type, | |||
| bdd_reorder_verbosity_t | verbosity | |||
| ) |
| void bdd_dynamic_reordering_zdd_disable | ( | bdd_manager * | mgr | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 822 of file calPort.c.
00823 { 00824 return bdd_construct_bdd_t(f->bddManager, Cal_BddElse(f->bddManager, f->calBdd)); 00825 }
| int bdd_enable_reordering_reporting | ( | bdd_manager * | mgr | ) |
| void bdd_end | ( | void * | manager | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 132 of file calPort.c.
00133 { 00134 Cal_BddManager mgr = (Cal_BddManager) manager; 00135 void *hooks; 00136 hooks = Cal_BddManagerGetHooks(mgr); 00137 Cal_MemFree(hooks); 00138 Cal_BddManagerQuit(mgr); 00139 }
Function********************************************************************
Synopsis [Counts the number of minterms in the on set.]
SideEffects []
Definition at line 1371 of file calPort.c.
01375 { 01376 double nMinterms; 01377 01378 nMinterms = bdd_count_onset(f, var_array); 01379 EpdConvert(nMinterms, epd); 01380 return 0; 01381 } /* end of bdd_epd_count_onset */
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1165 of file calPort.c.
01166 { 01167 return Cal_BddIsEqual(f->bddManager, f->calBdd, g->calBdd); 01168 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
| int bdd_equal_sup_norm | ( | bdd_manager * | mgr, | |
| bdd_node * | fn, | |||
| bdd_node * | gn, | |||
| BDD_VALUE_TYPE | tolerance, | |||
| int | pr | |||
| ) |
| void bdd_free | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 268 of file calPort.c.
00269 { 00270 if (f == NIL(bdd_t)) { 00271 fail("bdd_free: trying to free a NIL bdd_t"); 00272 } 00273 if (f->free){ 00274 fail("bdd_free: Trying to free a freed bdd_t"); 00275 } 00276 Cal_BddFree(f->bddManager, f->calBdd); 00277 f->calBdd = (Cal_Bdd) 0; 00278 f->bddManager = NIL(Cal_BddManager_t); 00279 f->free = 1; 00280 Cal_MemFree(f); 00281 }
| int bdd_gen_decomp | ( | bdd_t * | f, | |
| bdd_partition_type_t | partType, | |||
| bdd_t *** | conjArray | |||
| ) |
| bdd_external_hooks* bdd_get_external_hooks | ( | bdd_manager * | manager | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1682 of file calPort.c.
01683 { 01684 Cal_BddManager mgr = (Cal_BddManager) manager; 01685 return (bdd_external_hooks *) Cal_BddManagerGetHooks(mgr); 01686 }
| int bdd_get_free | ( | bdd_t * | f | ) |
| bdd_variableId bdd_get_id_from_level | ( | bdd_manager * | manager, | |
| long | level | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1773 of file calPort.c.
01774 { 01775 Cal_Bdd fn; 01776 Cal_BddManager mgr = (Cal_BddManager) manager; 01777 fn = Cal_BddManagerGetVarWithIndex(mgr, level); 01778 if (!fn){ 01779 /* variable should always be found, since they are created at bdd_start */ 01780 fprintf(stderr, "bdd_get_id_from_level: assumption violated"); 01781 exit(-1); 01782 } 01783 return ((bdd_variableId)(Cal_BddGetIfId(mgr, fn) - 1 )); 01784 }
| int bdd_get_level_from_id | ( | bdd_manager * | mgr, | |
| int | id | |||
| ) |
| bdd_manager* bdd_get_manager | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1410 of file calPort.c.
01411 { 01412 return (bdd_manager *) (f->bddManager); 01413 }
| bdd_package_type_t bdd_get_package_name | ( | void | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1427 of file calPort.c.
01428 { 01429 Cal_Bdd *support, var; 01430 Cal_BddManager mgr; 01431 long num_vars; 01432 var_set_t *result; 01433 int id, i; 01434 01435 mgr = f->bddManager; 01436 num_vars = Cal_BddVars(mgr); 01437 result = var_set_new((int) num_vars); 01438 support = Cal_MemAlloc(Cal_Bdd, (num_vars+1) * sizeof(Cal_Bdd)); 01439 for (i = 0; i <= num_vars; ++i) { 01440 support[i] = 0; 01441 } 01442 01443 (void) Cal_BddSupport(mgr, f->calBdd, support); 01444 for (i = 0; i < num_vars; ++i) { 01445 var = support[i]; 01446 if (var) { 01447 id = (int) (Cal_BddGetIfId(mgr, var) - 1); 01448 var_set_set_elt(result, id); 01449 } 01450 } 01451 01452 Cal_MemFree(support); 01453 return result; 01454 }
| bdd_t* bdd_get_variable | ( | bdd_manager * | manager, | |
| bdd_variableId | varId | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 225 of file calPort.c.
00226 { 00227 Cal_Bdd varBdd; 00228 Cal_BddManager mgr = (Cal_BddManager) manager; 00229 unsigned int numVars = Cal_BddVars(mgr); 00230 if (varId + 1 < numVars) { 00231 varBdd = Cal_BddManagerGetVarWithId(mgr, varId + 1); 00232 } else { 00233 int i; 00234 for (i=numVars, varBdd = NULL; i <= varId + 1; i++) { 00235 varBdd = Cal_BddManagerCreateNewVarLast(mgr); 00236 } 00237 } 00238 return bdd_construct_bdd_t(mgr, varBdd); 00239 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1521 of file calPort.c.
01522 { 01523 int i; 01524 bdd_t *var; 01525 array_t *result; 01526 bdd_variableId varId; 01527 01528 result = array_alloc(bdd_variableId, 0); 01529 for (i = 0; i < array_n(var_array); i++) { 01530 var = array_fetch(bdd_t *, var_array, i); 01531 varId = (int) bdd_top_var_id(var); 01532 array_insert_last(bdd_variableId, result, varId); 01533 } 01534 return result; 01535 }
| bdd_node* bdd_indices_to_cube | ( | bdd_manager * | mgr, | |
| int * | idArray, | |||
| int | n | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1208 of file calPort.c.
01209 { 01210 return bdd_construct_bdd_t(f->bddManager, Cal_BddIntersects(f->bddManager, 01211 f->calBdd, 01212 g->calBdd)); 01213 }
| int bdd_is_complement | ( | bdd_node * | f | ) |
| int bdd_is_constant | ( | bdd_node * | f | ) |
Function********************************************************************
Synopsis [Return TRUE if f is a cube, else return FALSE.]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1816 of file calPort.c.
01817 { 01818 Cal_BddManager mgr; 01819 if (f == NIL(bdd_t)) { 01820 fail("bdd_is_cube: invalid BDD"); 01821 } 01822 if(f->free) fail ("Freed Bdd passed to bdd_is_cube"); 01823 mgr = f->bddManager; 01824 return ((boolean)Cal_BddIsCube(mgr, f->calBdd)); 01825 }
| int bdd_is_lazy_sift | ( | bdd_manager * | mgr | ) |
| int bdd_is_ns_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_is_pi_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_is_ps_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Checks whether a BDD is a support of f.]
SideEffects []
Definition at line 1465 of file calPort.c.
01466 { 01467 return(bdd_is_support_var_id(f, bdd_top_var_id(var))); 01468 }
| 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 1479 of file calPort.c.
01480 { 01481 Cal_Bdd *support, var; 01482 Cal_BddManager mgr; 01483 long num_vars; 01484 int id, i; 01485 01486 mgr = f->bddManager; 01487 num_vars = Cal_BddVars(mgr); 01488 support = Cal_MemAlloc(Cal_Bdd, (num_vars+1) * sizeof(Cal_Bdd)); 01489 for (i = 0; i <= num_vars; ++i) { 01490 support[i] = 0; 01491 } 01492 01493 (void) Cal_BddSupport(mgr, f->calBdd, support); 01494 for (i = 0; i < num_vars; ++i) { 01495 var = support[i]; 01496 if (var) { 01497 id = (int) (Cal_BddGetIfId(mgr, var) - 1); 01498 if (id == index) { 01499 Cal_MemFree(support); 01500 return 1; 01501 } 01502 } 01503 } 01504 01505 Cal_MemFree(support); 01506 return 0; 01507 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1242 of file calPort.c.
01243 { 01244 return ((phase == TRUE) ? Cal_BddIsBddOne(f->bddManager, f->calBdd): 01245 Cal_BddIsBddZero(f->bddManager, f->calBdd)); 01246 01247 }
| int bdd_is_var_hard_group | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_is_var_to_be_grouped | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_is_var_to_be_ungrouped | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| bdd_t* bdd_ite | ( | bdd_t * | i, | |
| bdd_t * | t, | |||
| bdd_t * | e, | |||
| boolean | i_phase, | |||
| boolean | t_phase, | |||
| boolean | e_phase | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 838 of file calPort.c.
00840 { 00841 Cal_Bdd temp1, temp2, temp3; 00842 bdd_t *result; 00843 Cal_BddManager mgr; 00844 00845 mgr = i->bddManager; 00846 temp1 = (i_phase ? Cal_BddIdentity(mgr, i->calBdd) : Cal_BddNot(mgr, i->calBdd)); 00847 temp2 = (t_phase ? Cal_BddIdentity(mgr, t->calBdd) : Cal_BddNot(mgr, t->calBdd)); 00848 temp3 = (e_phase ? Cal_BddIdentity(mgr, e->calBdd) : Cal_BddNot(mgr, e->calBdd)); 00849 result = bdd_construct_bdd_t(mgr, Cal_BddITE(mgr, temp1, temp2, temp3)); 00850 Cal_BddFree(mgr, temp1); 00851 Cal_BddFree(mgr, temp2); 00852 Cal_BddFree(mgr, temp3); 00853 return result; 00854 }
| int bdd_iter_decomp | ( | bdd_t * | f, | |
| bdd_partition_type_t | partType, | |||
| bdd_t *** | conjArray | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1260 of file calPort.c.
01261 { 01262 Cal_Bdd temp1, temp2, impliesFn; 01263 Cal_BddManager mgr; 01264 boolean resultValue; 01265 01266 mgr = f->bddManager; 01267 temp1 = (f_phase ? Cal_BddIdentity(mgr, f->calBdd) : Cal_BddNot(mgr, f->calBdd)); 01268 temp2 = (g_phase ? Cal_BddIdentity(mgr, g->calBdd) : Cal_BddNot(mgr, g->calBdd)); 01269 impliesFn = Cal_BddImplies(mgr, temp1, temp2); /* returns a minterm 01270 of temp1*!temp2 01271 */ 01272 resultValue = Cal_BddIsBddZero(mgr, impliesFn); 01273 Cal_BddFree(mgr, temp1); 01274 Cal_BddFree(mgr, temp2); 01275 Cal_BddFree(mgr, impliesFn); 01276 return resultValue; 01277 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1322 of file calPort.c.
01323 { 01324 int i; 01325 bdd_t *g; 01326 boolean result; 01327 01328 arrayForEachItem(bdd_t *, g_array, i, g) { 01329 result = bdd_leq(f, g, f_phase, g_phase); 01330 if (g_phase) { 01331 if (!result) 01332 return(0); 01333 } else { 01334 if (result) 01335 return(1); 01336 } 01337 } 01338 if (g_phase) 01339 return(1); 01340 else 01341 return(0); 01342 }
| boolean bdd_lequal_mod_care_set | ( | bdd_t * | f, | |
| bdd_t * | g, | |||
| boolean | f_phase, | |||
| boolean | g_phase, | |||
| bdd_t * | careSet | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
| bdd_node* bdd_make_bdd_from_zdd_cover | ( | bdd_manager * | mgr, | |
| bdd_node * | node | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 867 of file calPort.c.
00868 { 00869 return bdd_construct_bdd_t(f->bddManager, 00870 Cal_BddReduce(f->bddManager, 00871 f->calBdd, c->calBdd)); 00872 }
Definition at line 875 of file calPort.c.
00876 { 00877 bdd_t *operand; 00878 Cal_Bdd result, temp; 00879 int i; 00880 00881 result = Cal_BddIdentity(f->bddManager, f->calBdd); 00882 for (i = 0; i < array_n(bddArray); i++) { 00883 operand = array_fetch(bdd_t *, bddArray, i); 00884 temp = Cal_BddReduce(f->bddManager, result, operand->calBdd); 00885 if (temp == NULL) { 00886 Cal_BddFree(f->bddManager, result); 00887 return(NULL); 00888 } 00889 Cal_BddFree(f->bddManager, result); 00890 result = temp; 00891 } 00892 00893 return(bdd_construct_bdd_t(f->bddManager, result)); 00894 }
| bdd_t* bdd_multiway_and | ( | bdd_manager * | manager, | |
| array_t * | bddArray | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 383 of file calPort.c.
00384 { 00385 int i; 00386 Cal_Bdd *calBddArray; 00387 bdd_t *operand, *result; 00388 Cal_BddManager mgr = (Cal_BddManager) manager; 00389 00390 calBddArray = Cal_MemAlloc(Cal_Bdd, array_n(bddArray)+1); 00391 for (i=0; i<array_n(bddArray); i++){ 00392 operand = array_fetch(bdd_t*, bddArray, i); 00393 calBddArray[i] = operand->calBdd; 00394 } 00395 calBddArray[i] = (Cal_Bdd)0; 00396 result = bdd_construct_bdd_t(mgr, 00397 Cal_BddMultiwayAnd(mgr, calBddArray)); 00398 Cal_MemFree(calBddArray); 00399 return result; 00400 }
| bdd_t* bdd_multiway_or | ( | bdd_manager * | manager, | |
| array_t * | bddArray | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 413 of file calPort.c.
00414 { 00415 int i; 00416 Cal_Bdd *calBddArray; 00417 bdd_t *operand, *result; 00418 Cal_BddManager mgr = (Cal_BddManager) manager; 00419 00420 calBddArray = Cal_MemAlloc(Cal_Bdd, array_n(bddArray)+1); 00421 for (i=0; i<array_n(bddArray); i++){ 00422 operand = array_fetch(bdd_t*, bddArray, i); 00423 calBddArray[i] = operand->calBdd; 00424 } 00425 calBddArray[i] = (Cal_Bdd)0; 00426 result = bdd_construct_bdd_t(mgr, 00427 Cal_BddMultiwayOr(mgr, calBddArray)); 00428 Cal_MemFree(calBddArray); 00429 return result; 00430 }
| bdd_t* bdd_multiway_xor | ( | bdd_manager * | manager, | |
| array_t * | bddArray | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 443 of file calPort.c.
00444 { 00445 int i; 00446 Cal_Bdd *calBddArray; 00447 bdd_t *operand, *result; 00448 Cal_BddManager mgr = (Cal_BddManager) manager; 00449 00450 calBddArray = Cal_MemAlloc(Cal_Bdd, array_n(bddArray)+1); 00451 for (i=0; i<array_n(bddArray); i++){ 00452 operand = array_fetch(bdd_t*, bddArray, i); 00453 calBddArray[i] = operand->calBdd; 00454 } 00455 calBddArray[i] = (Cal_Bdd)0; 00456 result = bdd_construct_bdd_t(mgr, 00457 Cal_BddMultiwayXor(mgr, calBddArray)); 00458 Cal_MemFree(calBddArray); 00459 return result; 00460 }
Function********************************************************************
Synopsis []
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1838 of file calPort.c.
01839 { 01840 return (bdd_block *) Cal_BddNewVarBlock(f->bddManager, f->calBdd, length); 01841 }
| int bdd_node_read_index | ( | bdd_node * | f | ) |
| int bdd_node_size | ( | bdd_node * | f | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 907 of file calPort.c.
00908 { 00909 return bdd_construct_bdd_t(f->bddManager, Cal_BddNot(f->bddManager, f->calBdd)); 00910 }
| unsigned int bdd_num_vars | ( | bdd_manager * | manager | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1548 of file calPort.c.
01549 { 01550 Cal_BddManager mgr = (Cal_BddManager) manager; 01551 return (Cal_BddVars(mgr)); 01552 }
| int bdd_num_zdd_vars | ( | bdd_manager * | mgr | ) |
| bdd_t* bdd_one | ( | bdd_manager * | manager | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 923 of file calPort.c.
00924 { 00925 Cal_BddManager mgr = (Cal_BddManager) manager; 00926 return bdd_construct_bdd_t(mgr, Cal_BddOne(mgr)); 00927 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 940 of file calPort.c.
00941 { 00942 Cal_Bdd temp1, temp2; 00943 bdd_t *result; 00944 Cal_BddManager mgr; 00945 00946 mgr = f->bddManager; 00947 temp1 = (f_phase ? Cal_BddIdentity(mgr, f->calBdd) : Cal_BddNot(mgr, f->calBdd)); 00948 temp2 = (g_phase ? Cal_BddIdentity(mgr, g->calBdd) : Cal_BddNot(mgr, g->calBdd)); 00949 result = bdd_construct_bdd_t(mgr, Cal_BddOr(mgr, temp1, temp2)); 00950 Cal_BddFree(mgr, temp1); 00951 Cal_BddFree(mgr, temp2); 00952 return result; 00953 }
| array_t* bdd_pairwise_and | ( | bdd_manager * | manager, | |
| array_t * | bddArray1, | |||
| array_t * | bddArray2 | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 473 of file calPort.c.
00475 { 00476 int i; 00477 array_t *resultArray; 00478 Cal_Bdd *calBddArray, *calBddResultArray; 00479 bdd_t *operand; 00480 Cal_BddManager mgr = (Cal_BddManager) manager; 00481 00482 if (array_n(bddArray1) != array_n(bddArray2)){ 00483 fprintf(stderr, "bdd_pairwise_and: Arrays of different lengths.\n"); 00484 return NIL(array_t); 00485 } 00486 calBddArray = Cal_MemAlloc(Cal_Bdd, 2*array_n(bddArray1)+1); 00487 for (i=0; i<array_n(bddArray1); i++){ 00488 operand = array_fetch(bdd_t*, bddArray1, i); 00489 calBddArray[i<<1] = operand->calBdd; 00490 operand = array_fetch(bdd_t*, bddArray2, i); 00491 calBddArray[(i<<1)+1] = operand->calBdd; 00492 } 00493 calBddArray[i<<1] = (Cal_Bdd)0; 00494 calBddResultArray = Cal_BddPairwiseAnd(mgr, calBddArray); 00495 resultArray = array_alloc(bdd_t*, 0); 00496 for (i=0; i<array_n(bddArray1); i++){ 00497 array_insert_last(bdd_t *, resultArray, 00498 bdd_construct_bdd_t(mgr, calBddResultArray[i])); 00499 } 00500 Cal_MemFree(calBddArray); 00501 Cal_MemFree(calBddResultArray); 00502 return resultArray; 00503 }
| array_t* bdd_pairwise_or | ( | bdd_manager * | manager, | |
| array_t * | bddArray1, | |||
| array_t * | bddArray2 | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 516 of file calPort.c.
00518 { 00519 int i; 00520 array_t *resultArray; 00521 Cal_Bdd *calBddArray, *calBddResultArray; 00522 bdd_t *operand; 00523 Cal_BddManager mgr = (Cal_BddManager) manager; 00524 00525 if (array_n(bddArray1) != array_n(bddArray2)){ 00526 fprintf(stderr, "bdd_pairwise_or: Arrays of different lengths.\n"); 00527 return NIL(array_t); 00528 } 00529 calBddArray = Cal_MemAlloc(Cal_Bdd, 2*array_n(bddArray1)+1); 00530 for (i=0; i<array_n(bddArray1); i++){ 00531 operand = array_fetch(bdd_t*, bddArray1, i); 00532 calBddArray[i<<1] = operand->calBdd; 00533 operand = array_fetch(bdd_t*, bddArray2, i); 00534 calBddArray[(i<<1)+1] = operand->calBdd; 00535 } 00536 calBddArray[i<<1] = (Cal_Bdd)0; 00537 calBddResultArray = Cal_BddPairwiseOr(mgr, calBddArray); 00538 resultArray = array_alloc(bdd_t*, 0); 00539 for (i=0; i<array_n(bddArray1); i++){ 00540 array_insert_last(bdd_t *, resultArray, 00541 bdd_construct_bdd_t(mgr, calBddResultArray[i])); 00542 } 00543 Cal_MemFree(calBddArray); 00544 Cal_MemFree(calBddResultArray); 00545 return resultArray; 00546 }
| array_t* bdd_pairwise_xor | ( | bdd_manager * | manager, | |
| array_t * | bddArray1, | |||
| array_t * | bddArray2 | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 560 of file calPort.c.
00562 { 00563 int i; 00564 array_t *resultArray; 00565 Cal_Bdd *calBddArray, *calBddResultArray; 00566 bdd_t *operand; 00567 Cal_BddManager mgr = (Cal_BddManager) manager; 00568 00569 if (array_n(bddArray1) != array_n(bddArray2)){ 00570 fprintf(stderr, "bdd_pairwise_xor: Arrays of different lengths.\n"); 00571 return NIL(array_t); 00572 } 00573 calBddArray = Cal_MemAlloc(Cal_Bdd, 2*array_n(bddArray1)+1); 00574 for (i=0; i<array_n(bddArray1); i++){ 00575 operand = array_fetch(bdd_t*, bddArray1, i); 00576 calBddArray[i<<1] = operand->calBdd; 00577 operand = array_fetch(bdd_t*, bddArray2, i); 00578 calBddArray[(i<<1)+1] = operand->calBdd; 00579 } 00580 calBddArray[i<<1] = (Cal_Bdd)0; 00581 calBddResultArray = Cal_BddPairwiseXor(mgr, calBddArray); 00582 resultArray = array_alloc(bdd_t*, 0); 00583 for (i=0; i<array_n(bddArray1); i++){ 00584 array_insert_last(bdd_t *, resultArray, 00585 bdd_construct_bdd_t(mgr, calBddResultArray[i])); 00586 } 00587 Cal_MemFree(calBddArray); 00588 Cal_MemFree(calBddResultArray); 00589 return resultArray; 00590 }
| void* bdd_pointer | ( | bdd_t * | f | ) |
| void bdd_print | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1565 of file calPort.c.
01566 { 01567 Cal_BddPrintBdd(f->bddManager, f->calBdd, Cal_BddNamingFnNone, 01568 Cal_BddTerminalIdFnNone, (Cal_Pointer_t) 0, (FILE *)stdout); 01569 }
| int bdd_print_apa_minterm | ( | FILE * | fp, | |
| bdd_t * | f, | |||
| int | nvars, | |||
| int | precision | |||
| ) |
| int bdd_print_cover | ( | bdd_t * | f | ) |
| int bdd_print_minterm | ( | bdd_t * | f | ) |
| void bdd_print_stats | ( | bdd_manager * | manager, | |
| FILE * | file | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1582 of file calPort.c.
01583 { 01584 Cal_BddManager mgr = (Cal_BddManager) manager; 01585 Cal_BddManagerGC(mgr); 01586 Cal_BddStats(mgr, file); 01587 }
| int bdd_ptrhash | ( | bdd_t * | f, | |
| int | size | |||
| ) |
| bdd_node* bdd_read_background | ( | bdd_manager * | mgr | ) |
| BDD_VALUE_TYPE bdd_read_epsilon | ( | bdd_manager * | mgr | ) |
| bdd_node* bdd_read_logic_zero | ( | bdd_manager * | mgr | ) |
| int bdd_read_next_reordering | ( | bdd_manager * | mgr | ) |
| int bdd_read_node_count | ( | bdd_manager * | mgr | ) |
| bdd_node* bdd_read_one | ( | bdd_manager * | mgr | ) |
| int bdd_read_pair_index | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_read_peak_live_node | ( | bdd_manager * | mgr | ) |
| long bdd_read_peak_memory | ( | bdd_manager * | mgr | ) |
| bdd_node* bdd_read_plus_infinity | ( | bdd_manager * | mgr | ) |
| int bdd_read_reordered_field | ( | bdd_manager * | mgr | ) |
| int bdd_read_reorderings | ( | bdd_manager * | mgr | ) |
| int bdd_read_zdd_level | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| bdd_node* bdd_read_zero | ( | bdd_manager * | mgr | ) |
| void bdd_realign_disable | ( | bdd_manager * | mgr | ) |
| void bdd_realign_enable | ( | bdd_manager * | mgr | ) |
| int bdd_realignment_enabled | ( | bdd_manager * | mgr | ) |
| void bdd_recursive_deref | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
| void bdd_recursive_deref_zdd | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
| void bdd_ref | ( | bdd_node * | fn | ) |
| int bdd_remove_hook | ( | bdd_manager * | mgr, | |
| int(*)(bdd_manager *, char *, void *) | procedure, | |||
| bdd_hook_type_t | whichHook | |||
| ) |
| void bdd_reorder | ( | bdd_manager * | manager | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1756 of file calPort.c.
01757 { 01758 Cal_BddManager mgr = (Cal_BddManager) manager; 01759 Cal_BddReorder(mgr); 01760 }
| bdd_reorder_verbosity_t bdd_reordering_reporting | ( | bdd_manager * | mgr | ) |
Definition at line 2184 of file calPort.c.
02185 { 02186 return BDD_REORDER_VERBOSITY_DEFAULT; 02187 }
| int bdd_reordering_status | ( | bdd_manager * | mgr, | |
| bdd_reorder_type_t * | method | |||
| ) |
| int bdd_reordering_zdd_status | ( | bdd_manager * | mgr, | |
| bdd_reorder_type_t * | method | |||
| ) |
| int bdd_reset_var_to_be_grouped | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| void bdd_set_background | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
| void bdd_set_gc_mode | ( | bdd_manager * | manager, | |
| boolean | no_gc | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1699 of file calPort.c.
01700 { 01701 Cal_BddManager mgr = (Cal_BddManager) manager; 01702 Cal_BddSetGCMode(mgr, (int) no_gc); 01703 }
| void bdd_set_next_reordering | ( | bdd_manager * | mgr, | |
| int | next | |||
| ) |
| int bdd_set_ns_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_set_pair_index | ( | bdd_manager * | mgr, | |
| int | index, | |||
| int | pairIndex | |||
| ) |
| 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 CAL 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 1877 of file calPort.c.
01881 { 01882 /* int reorderMethod; */ 01883 st_table *newValueTable; 01884 st_generator *stgen; 01885 avl_generator *avlgen; 01886 char *paramName; 01887 char *paramValue; 01888 Cal_BddManager bddManager = (Cal_BddManager)mgr; 01889 01890 01891 /* Build a new table with the parameter names but with 01892 ** the prefix removed. */ 01893 newValueTable = st_init_table(st_ptrcmp, st_ptrhash); 01894 avl_foreach_item(valueTable, avlgen, AVL_FORWARD, (char **)¶mName, 01895 (char **)¶mValue) { 01896 if (strncmp(paramName, "BDD.", 4) == 0) { 01897 st_insert(newValueTable, (char *)¶mName[4], 01898 (char *)paramValue); 01899 } 01900 } 01901 01902 st_foreach_item(newValueTable, stgen, ¶mName, ¶mValue) { 01903 unsigned int uvalue; 01904 double value; 01905 char *invalidChar; 01906 01907 invalidChar = NIL(char); 01908 01909 if (strcmp(paramName, "Node limit") == 0) { 01910 uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10); 01911 /* RB an unsigned will never be < 0 */ 01912 if (*invalidChar /*|| uvalue < 0*/) { 01913 InvalidType(file, "Node limit", "unsigned integer"); 01914 } 01915 else { 01916 bddManager->nodeLimit = uvalue; 01917 } 01918 } 01919 else if (strcmp(paramName, "Garbage collection enabled") == 0) { 01920 if (strcmp(paramValue, "yes") == 0) { 01921 bddManager->gcMode = 1; 01922 } 01923 else if (strcmp(paramValue, "no") == 0) { 01924 bddManager->gcMode = 0; 01925 } 01926 else { 01927 InvalidType(file, "Garbage collection enabled", "(yes,no)"); 01928 } 01929 } 01930 else if (strcmp(paramName, 01931 "Maximum number of variables sifted per reordering") == 0) { 01932 uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10); 01933 if (*invalidChar /*|| uvalue < 0*/) { 01934 InvalidType(file, "Maximum number of variables sifted per reordering", 01935 "unsigned integer"); 01936 } 01937 else { 01938 bddManager->maxNumVarsSiftedPerReordering = uvalue; 01939 } 01940 } 01941 else if (strcmp(paramName, 01942 "Maximum number of variable swaps per reordering") == 0) { 01943 uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10); 01944 if (*invalidChar /*|| uvalue < 0*/) { 01945 InvalidType(file, "Maximum number of variable swaps per reordering", 01946 "unsigned integer"); 01947 } 01948 else { 01949 bddManager->maxNumSwapsPerReordering = uvalue; 01950 } 01951 } 01952 else if (strcmp(paramName, 01953 "Maximum growth while sifting a variable") == 0) { 01954 value = strtod(paramValue, &invalidChar); 01955 if (*invalidChar) { 01956 InvalidType(file, "Maximum growth while sifting a variable", 01957 "real"); 01958 } 01959 else { 01960 bddManager->maxSiftingGrowth = value; 01961 } 01962 } 01963 else if (strcmp(paramName, "Dynamic reordering of BDDs enabled") == 0) { 01964 if (strcmp(paramValue, "yes") == 0) { 01965 bddManager->dynamicReorderingEnableFlag = 1; 01966 } 01967 else if (strcmp(paramValue, "no") == 0) { 01968 bddManager->dynamicReorderingEnableFlag = 0; 01969 } 01970 else { 01971 InvalidType(file, "Dynamic reordering of BDDs enabled", 01972 "(yes,no)"); 01973 } 01974 } 01975 else if (strcmp(paramName, "Use old reordering") 01976 == 0) { 01977 if (strcmp(paramValue, "yes") == 0) { 01978 bddManager->reorderMethod = CAL_REORDER_METHOD_BF; 01979 } 01980 else if (strcmp(paramValue, "no") == 0) { 01981 bddManager->reorderMethod = CAL_REORDER_METHOD_DF; 01982 } 01983 else { 01984 InvalidType(file, "Dynamic reordering of BDDs enabled", 01985 "(yes,no)"); 01986 } 01987 } 01988 else if (strcmp(paramName, "Dynamic reordering threshold") == 0) { 01989 uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10); 01990 if (*invalidChar /*|| uvalue < 0*/) { 01991 InvalidType(file, "Dynamic reordering threshold", "unsigned integer"); 01992 } 01993 else { 01994 bddManager->reorderingThreshold = uvalue; 01995 } 01996 } 01997 else if (strcmp(paramName, "Repacking after GC threshold") 01998 == 0) { 01999 value = strtod(paramValue, &invalidChar); 02000 if (*invalidChar || value < 0) { 02001 InvalidType(file, "Repacking after GC threshold", "unsigned real"); 02002 } 02003 else { 02004 bddManager->repackAfterGCThreshold = value; 02005 } 02006 } 02007 else if (strcmp(paramName, "Table repacking threshold") 02008 == 0) { 02009 value = strtod(paramValue, &invalidChar); 02010 if (*invalidChar || value < 0) { 02011 InvalidType(file, "Table repacking threshold", "unsigned real"); 02012 } 02013 else { 02014 bddManager->tableRepackThreshold = value; 02015 } 02016 } 02017 else { 02018 (void) fprintf(file, "Warning: Parameter %s not recognized.", 02019 paramName); 02020 (void) fprintf(file, " Ignored.\n"); 02021 } 02022 } /* end of st_foreach_item */ 02023 02024 /* Clean up. */ 02025 st_free_table(newValueTable); 02026 02027 return(1); 02028 02029 } /* end of bdd_set_parameters */
| int bdd_set_pi_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_set_ps_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| void bdd_set_reordered_field | ( | bdd_manager * | mgr, | |
| int | n | |||
| ) |
| int bdd_set_var_hard_group | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_set_var_to_be_grouped | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_set_var_to_be_ungrouped | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| int bdd_shuffle_heap | ( | bdd_manager * | mgr, | |
| int * | permut | |||
| ) |
| int bdd_size | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1600 of file calPort.c.
01601 { 01602 return ((int) Cal_BddSize(f->bddManager, f->calBdd, 1)); 01603 }
| long bdd_size_multiple | ( | array_t * | bdd_array | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1631 of file calPort.c.
01632 { 01633 long result; 01634 Cal_Bdd *vector_bdd; 01635 bdd_t *f; 01636 int i; 01637 Cal_BddManager mgr; 01638 01639 if ((bdd_array == NIL(array_t)) || (array_n(bdd_array) == 0)) 01640 return 0; 01641 01642 f = array_fetch(bdd_t*, bdd_array, 0); 01643 mgr = f->bddManager; 01644 vector_bdd = Cal_MemAlloc(Cal_Bdd, array_n(bdd_array)+1); 01645 for(i=0; i<array_n(bdd_array);i++){ 01646 f = array_fetch(bdd_t*, bdd_array, i); 01647 vector_bdd[i] = f->calBdd; 01648 } 01649 vector_bdd[array_n(bdd_array)] = 0; 01650 result = Cal_BddSizeMultiple(mgr, vector_bdd,1); 01651 Cal_MemFree(vector_bdd); 01652 return result; 01653 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 966 of file calPort.c.
00967 { 00968 int numVars, i; 00969 bdd_t *fn, *result; 00970 Cal_Bdd *assoc; 00971 Cal_BddManager mgr; 00972 int assocId; 00973 00974 numVars = array_n(smoothingVars); 00975 if (numVars == 0) { 00976 fprintf(stderr,"bdd_smooth: no smoothing variables"); 00977 return f; 00978 } 00979 mgr = f->bddManager; 00980 assoc = Cal_MemAlloc(Cal_Bdd, numVars+1); 00981 for (i = 0; i < numVars; i++) { 00982 fn = array_fetch(bdd_t *, smoothingVars, i); 00983 assoc[i] = fn->calBdd; 00984 } 00985 assoc[numVars] = 0; 00986 assocId = Cal_AssociationInit(mgr, assoc, 0); 00987 (void) Cal_AssociationSetCurrent(mgr, assocId); /* set the temp 00988 association as the 00989 current association 00990 */ 00991 result = bdd_construct_bdd_t(mgr, Cal_BddExists(mgr, f->calBdd)); 00992 Cal_MemFree(assoc); 00993 return result; 00994 }
Definition at line 3465 of file calPort.c.
03466 { 03467 int i; 03468 bdd_t *var, *res; 03469 array_t *smoothingVars; 03470 var_set_t *supportVarSet; 03471 03472 smoothingVars = array_alloc(bdd_t *, 0); 03473 supportVarSet = bdd_get_support(f); 03474 for (i = 0; i < supportVarSet->n_elts; i++) { 03475 if (var_set_get_elt(supportVarSet, i) == 1) { 03476 var = bdd_var_with_index(f->bddManager, i); 03477 array_insert_last(bdd_t *, smoothingVars, var); 03478 } 03479 } 03480 var_set_free(supportVarSet); 03481 03482 res = bdd_smooth(f, smoothingVars); 03483 03484 for (i = 0; i < array_n(smoothingVars); i++) { 03485 var = array_fetch(bdd_t *, smoothingVars, i); 03486 bdd_free(var); 03487 } 03488 array_free(smoothingVars); 03489 return res; 03490 }
| bdd_node* bdd_split_set | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node ** | x, | |||
| int | n, | |||
| double | m | |||
| ) |
| bdd_manager* bdd_start | ( | int | nvariables | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 152 of file calPort.c.
00153 { 00154 Cal_BddManager mgr; 00155 int i; 00156 bdd_external_hooks *hooks; 00157 00158 mgr = Cal_BddManagerInit(); 00159 for (i = 0; i < nvariables; i++) { 00160 (void) Cal_BddManagerCreateNewVarLast(mgr); 00161 } 00162 hooks = Cal_MemAlloc(bdd_external_hooks, 1); 00163 hooks->mdd = hooks->network = hooks->undef1 = (char *) 0; 00164 Cal_BddManagerSetHooks(mgr, (void *)hooks); 00165 return (bdd_manager *)mgr; 00166 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1007 of file calPort.c.
01008 { 01009 int num_old_vars, num_new_vars, i; 01010 bdd_t *fn_old, *fn_new, *result; 01011 Cal_Bdd *assoc; 01012 Cal_BddManager mgr; 01013 int assocId; 01014 01015 num_old_vars = array_n(old_array); 01016 num_new_vars = array_n(new_array); 01017 if (num_old_vars != num_new_vars) { 01018 fprintf(stderr,"bdd_substitute: mismatch of number of new and old variables"); 01019 exit(-1); 01020 } 01021 mgr = f->bddManager; 01022 assoc = Cal_MemAlloc(Cal_Bdd, 2*num_old_vars+1); 01023 for (i = 0; i < num_old_vars; i++) { 01024 fn_old = array_fetch(bdd_t *, old_array, i); 01025 fn_new = array_fetch(bdd_t *, new_array, i); 01026 assoc[2*i] = fn_old->calBdd; 01027 assoc[2*i+1] = fn_new->calBdd; 01028 } 01029 assoc[2*num_old_vars] = 0; 01030 assocId = Cal_AssociationInit(mgr, assoc, 1); 01031 (void) Cal_AssociationSetCurrent(mgr, assocId); 01032 result = bdd_construct_bdd_t(mgr, Cal_BddSubstitute(mgr, f->calBdd)); 01033 Cal_MemFree(assoc); 01034 Cal_TempAssociationQuit(mgr); 01035 return result; 01036 }
Definition at line 1039 of file calPort.c.
01040 { 01041 int i; 01042 bdd_t *f, *new_; 01043 array_t *substitute_array = array_alloc(bdd_t *, 0); 01044 01045 arrayForEachItem(bdd_t *, f_array, i, f) { 01046 new_ = bdd_substitute(f, old_array, new_array); 01047 array_insert_last(bdd_t *, substitute_array, new_); 01048 } 01049 return(substitute_array); 01050 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1080 of file calPort.c.
01081 { 01082 return bdd_construct_bdd_t(f->bddManager, Cal_BddThen(f->bddManager, f->calBdd)); 01083 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1096 of file calPort.c.
01097 { 01098 return bdd_construct_bdd_t(f->bddManager, Cal_BddIf(f->bddManager, f->calBdd)); 01099 }
| bdd_variableId bdd_top_var_id | ( | bdd_t * | f | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1666 of file calPort.c.
01667 { 01668 return ((bdd_variableId) (Cal_BddGetIfId(f->bddManager, f->calBdd) - 1)); 01669 }
| long bdd_top_var_level | ( | bdd_manager * | manager, | |
| bdd_t * | fn | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1797 of file calPort.c.
01798 { 01799 Cal_BddManager mgr = (Cal_BddManager) manager; 01800 return (long)Cal_BddGetIfIndex(mgr, fn->calBdd); 01801 }
| int bdd_unbind_var | ( | bdd_manager * | mgr, | |
| int | index | |||
| ) |
| bdd_node* bdd_unique_inter | ( | bdd_manager * | mgr, | |
| int | v, | |||
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_unique_inter_ivo | ( | bdd_manager * | mgr, | |
| int | v, | |||
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| int bdd_var_decomp | ( | bdd_t * | f, | |
| bdd_partition_type_t | partType, | |||
| bdd_t *** | conjArray | |||
| ) |
| bdd_t* bdd_var_with_index | ( | bdd_manager * | manager, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Return TRUE if f is a cube, else return FALSE.]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1854 of file calPort.c.
01855 { 01856 Cal_BddManager mgr = (Cal_BddManager) manager; 01857 return bdd_construct_bdd_t(mgr, 01858 Cal_BddManagerGetVarWithIndex(mgr, 01859 index)); 01860 }
| bdd_node* bdd_xeqy | ( | bdd_manager * | mgr, | |
| int | N, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y | |||
| ) |
| bdd_node* bdd_xgty | ( | bdd_manager * | mgr, | |
| int | N, | |||
| bdd_node ** | x, | |||
| bdd_node ** | y | |||
| ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1112 of file calPort.c.
01113 { 01114 return bdd_construct_bdd_t(f->bddManager, Cal_BddXnor(f->bddManager, f->calBdd, g->calBdd)); 01115 }
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1128 of file calPort.c.
01129 { 01130 return bdd_construct_bdd_t(f->bddManager, Cal_BddXor(f->bddManager, f->calBdd, g->calBdd)); 01131 }
| bdd_node* bdd_zdd_complement | ( | bdd_manager * | mgr, | |
| bdd_node * | node | |||
| ) |
| int bdd_zdd_count | ( | bdd_manager * | mgr, | |
| bdd_node * | f | |||
| ) |
| bdd_node* bdd_zdd_diff | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_zdd_diff_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| int bdd_zdd_get_cofactors3 | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| int | v, | |||
| bdd_node ** | f1, | |||
| bdd_node ** | f0, | |||
| bdd_node ** | fd | |||
| ) |
| bdd_node* bdd_zdd_get_node | ( | bdd_manager * | mgr, | |
| int | id, | |||
| bdd_node * | g, | |||
| bdd_node * | h | |||
| ) |
| bdd_node* bdd_zdd_isop | ( | bdd_manager * | mgr, | |
| bdd_node * | L, | |||
| bdd_node * | U, | |||
| bdd_node ** | zdd_I | |||
| ) |
| bdd_node* bdd_zdd_isop_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | L, | |||
| bdd_node * | U, | |||
| bdd_node ** | zdd_I | |||
| ) |
| bdd_node* bdd_zdd_product | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_zdd_product_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| void bdd_zdd_realign_disable | ( | bdd_manager * | mgr | ) |
| void bdd_zdd_realign_enable | ( | bdd_manager * | mgr | ) |
| int bdd_zdd_realignment_enabled | ( | bdd_manager * | mgr | ) |
| bdd_node* bdd_zdd_union | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| int bdd_zdd_vars_from_bdd_vars | ( | bdd_manager * | mgr, | |
| int | multiplicity | |||
| ) |
| bdd_node* bdd_zdd_weak_div | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_node* bdd_zdd_weak_div_recur | ( | bdd_manager * | mgr, | |
| bdd_node * | f, | |||
| bdd_node * | g | |||
| ) |
| bdd_t* bdd_zero | ( | bdd_manager * | manager | ) |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 1144 of file calPort.c.
01145 { 01146 Cal_BddManager mgr = (Cal_BddManager) manager; 01147 return bdd_construct_bdd_t(mgr, Cal_BddZero(mgr)); 01148 }
| static void InvalidType | ( | FILE * | file, | |
| char * | field, | |||
| char * | expected | |||
| ) | [static] |
CFile***********************************************************************
FileName [calPort.c]
PackageName [cal_port]
Synopsis [required]
Description [optional]
SeeAlso [optional]
Author [Rajeev K. Ranjan]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]AutomaticStart
Function********************************************************************
Synopsis [Function to print a warning that an illegal value was read.]
SideEffects []
SeeAlso [bdd_set_parameters]
