- Generated on Wed Oct 12 2011 00:34:51 for VIS by
1.7.3
|
VIS
|
00001 00019 #include "synthInt.h" 00020 00021 static char rcsid[] UNUSED = "$Id: synthGen.c,v 1.36 2005/05/11 20:17:21 hhhan Exp $"; 00022 00023 /*---------------------------------------------------------------------------*/ 00024 /* Constant declarations */ 00025 /*---------------------------------------------------------------------------*/ 00026 00027 00028 /*---------------------------------------------------------------------------*/ 00029 /* Type declarations */ 00030 /*---------------------------------------------------------------------------*/ 00031 00032 00033 /*---------------------------------------------------------------------------*/ 00034 /* Structure declarations */ 00035 /*---------------------------------------------------------------------------*/ 00036 00037 00038 /*---------------------------------------------------------------------------*/ 00039 /* Variable declarations */ 00040 /*---------------------------------------------------------------------------*/ 00041 00042 extern int UseMtree; 00043 extern int UseCommonDivisor; 00044 extern int TryNodeSharing; 00045 extern int Resubstitution; 00046 extern int RemainderComplement; 00047 extern int noMemoryFlag; 00048 extern int VerifyTreeMode; 00049 00052 /*---------------------------------------------------------------------------*/ 00053 /* Static function prototypes */ 00054 /*---------------------------------------------------------------------------*/ 00055 00056 static MlTree * LiteralFactoringTree(bdd_manager *dd, st_table *table, bdd_node *f, bdd_node *c, int level, int *ref, MlTree *bring, int verbosity); 00057 static bdd_node * BestLiteral(bdd_manager *dd, bdd_node *f, bdd_node *c); 00058 static int IsCubeFree(bdd_manager *dd, bdd_node *f); 00059 static bdd_node * CommonCube(bdd_manager *dd, bdd_node *f); 00060 00064 /*---------------------------------------------------------------------------*/ 00065 /* Definition of exported functions */ 00066 /*---------------------------------------------------------------------------*/ 00067 00068 00069 00070 /*---------------------------------------------------------------------------*/ 00071 /* Definition of internal functions */ 00072 /*---------------------------------------------------------------------------*/ 00073 00097 MlTree * 00098 SynthGenericFactorTree(bdd_manager *dd, 00099 st_table *table, 00100 bdd_node *f, 00101 int level, 00102 int *ref, 00103 MlTree *comp_d_tree, 00104 int comp_d_flag, 00105 MlTree *bring, 00106 int verbosity) 00107 { 00108 bdd_node *one = bdd_read_one(dd); 00109 bdd_node *zero = bdd_read_zero(dd); 00110 bdd_node *d, *q, *r, *m, *c; 00111 MlTree *tree, *q_tree, *d_tree, *r_tree; 00112 int q_ref, d_ref, r_ref; 00113 int ncubes; 00114 bdd_node *tmp; 00115 char message[80]; 00116 char space[80]; 00117 MlTree *comp_q_tree = (MlTree *)NULL; 00118 MlTree *comp_r_tree = (MlTree *)NULL; 00119 int found; 00120 MlTree *tmp_tree; 00121 int comp_flag; 00122 00123 if (verbosity > 1) { 00124 SynthGetSpaceString(space, level * 2, 80); 00125 sprintf(message, "%s[%d] in : ", space, level); 00126 SynthPrintZddTreeMessage(dd, f, message); 00127 sprintf(message, "%s[%d]out : ", space, level); 00128 } 00129 00130 if (bring) 00131 tree = (MlTree *)NULL; 00132 else { 00133 tree = SynthLookupMlTable(table, dd, f, 1, verbosity); 00134 /* tree could be NULL because of reordering, or a failure to 00135 * allocate memory or just that f was not in the cache. 00136 * So, we would like return NULL ONLY in the case of 00137 * reordering or failure to allocate memory. 00138 */ 00139 if (bdd_read_reordered_field(dd) || noMemoryFlag == 1) 00140 return(NULL); 00141 } 00142 if (tree) { 00143 if (verbosity > 1) 00144 SynthPrintMlTreeMessage(dd, tree, message); 00145 *ref = 1; 00146 return(tree); 00147 } 00148 00149 if (f == one || f == zero) { 00150 tree = SynthFindOrCreateMlTree(table, dd, f, 1, 0, ref, verbosity); 00151 if (!tree) 00152 return(NULL); 00153 tmp_tree = tree; 00154 tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity); 00155 if (!tree) { 00156 if (*ref == 0) 00157 SynthFreeMlTree(MlTree_Regular(tmp_tree), 1); 00158 return(NULL); 00159 } else if (tree != tmp_tree) { 00160 *ref = 1; 00161 if (comp_flag) 00162 tree = MlTree_Not(tree); 00163 } 00164 if (verbosity > 1) 00165 SynthPrintMlTreeMessage(dd, tree, message); 00166 return(tree); 00167 } 00168 00169 d_tree = (MlTree *)NULL; 00170 if (comp_d_tree) { 00171 if (comp_d_flag) 00172 d = comp_d_tree->complement; 00173 else 00174 d = comp_d_tree->node; 00175 if (!d) 00176 return((MlTree *)NULL); 00177 bdd_ref(d); 00178 } else { 00179 found = 0; 00180 d = (* SynthGetZddDivisorFunc())(dd, f); 00181 if (!d) 00182 return(NULL); 00183 bdd_ref(d); 00184 if (TryNodeSharing) { 00185 /* Here, we don't need to call bdd_ref. */ 00186 d = SynthFindBiggerDivisorInList(dd, table, f, d, &found, 00187 &comp_d_flag, &comp_d_tree, verbosity); 00188 if (!d) 00189 return(NULL); 00190 } 00191 if (UseCommonDivisor && found == 0) { 00192 tree = SynthGetFactorTreeWithCommonDivisor(dd, table, 00193 SynthGenericFactorTree, f, d, level, ref, verbosity); 00194 if (tree) 00195 return(tree); 00196 if (bdd_read_reordered_field(dd) || noMemoryFlag == 1) { 00197 bdd_recursive_deref_zdd(dd, d); 00198 return(NULL); 00199 } 00200 } 00201 } 00202 if (d == f) { 00203 tree = SynthFindOrCreateMlTree(table, dd, f, 1, 0, ref, verbosity); 00204 if (!tree) { 00205 bdd_recursive_deref_zdd(dd, d); 00206 return(NULL); 00207 } 00208 if (verbosity > 1) 00209 SynthPrintMlTreeMessage(dd, tree, message); 00210 tmp_tree = tree; 00211 tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity); 00212 if (!tree) { 00213 bdd_recursive_deref_zdd(dd, d); 00214 return(NULL); 00215 } else if (tree == tmp_tree) { 00216 if (*ref == 0) 00217 SynthPutMlTreeInList(dd, tree, 0); 00218 } else { 00219 *ref = 1; 00220 if (comp_flag) 00221 tree = MlTree_Not(tree); 00222 } 00223 bdd_recursive_deref_zdd(dd, d); 00224 return(tree); 00225 } 00226 if (!comp_d_tree) { 00227 if (st_lookup(table, (char *)d, &d_tree)) { 00228 SynthSetSharedFlag(dd, d_tree); 00229 if (MlTree_Regular(d_tree)->candidate) { 00230 if (!SynthUseCandidate(table, dd, d_tree, verbosity)) { 00231 bdd_recursive_deref_zdd(dd, d); 00232 return(NULL); 00233 } 00234 } 00235 if (MlTree_IsComplement(d_tree)) { 00236 d_tree = MlTree_Regular(d_tree); 00237 comp_d_tree = d_tree; 00238 comp_d_flag = 1; 00239 d_tree = (MlTree *)NULL; 00240 } 00241 else 00242 comp_d_flag = 0; 00243 } 00244 } else { 00245 if (!comp_d_flag) 00246 d_tree = comp_d_tree; 00247 } 00248 00249 q = (* SynthGetZddDivideFunc())(dd, f, d); 00250 if (!q) { 00251 bdd_recursive_deref_zdd(dd, d); 00252 return(NULL); 00253 } 00254 bdd_ref(q); 00255 if (comp_d_tree && q == zero) { 00256 bdd_recursive_deref_zdd(dd, d); 00257 bdd_recursive_deref_zdd(dd, q); 00258 return((MlTree *)NULL); 00259 } 00260 if (q == one) { 00261 bdd_recursive_deref_zdd(dd, q); 00262 tree = SynthPostFactorTree(dd, table, f, q, d, bring, 00263 comp_d_tree, comp_d_flag, message, ref, verbosity); 00264 bdd_recursive_deref_zdd(dd, d); 00265 return(tree); 00266 } 00267 00268 ncubes = bdd_zdd_count(dd, q); 00269 if (ncubes == 1) { 00270 if (d_tree || comp_d_tree) { 00271 m = (* SynthGetZddProductFunc())(dd, q, d); 00272 if (!m) { 00273 bdd_recursive_deref_zdd(dd, d); 00274 bdd_recursive_deref_zdd(dd, q); 00275 return(NULL); 00276 } 00277 bdd_ref(m); 00278 bdd_recursive_deref_zdd(dd, d); 00279 r = bdd_zdd_diff(dd, f, m); 00280 bdd_recursive_deref_zdd(dd, m); 00281 if (!r) { 00282 bdd_recursive_deref_zdd(dd, q); 00283 return(NULL); 00284 } 00285 bdd_ref(r); 00286 bdd_recursive_deref_zdd(dd,r); 00287 if (r == zero) { 00288 if (!d_tree) 00289 d_tree = comp_d_tree; 00290 d_ref = 1; 00291 q_tree = (MlTree *)NULL; 00292 if (st_lookup(table, (char *)q, &q_tree)) { 00293 SynthSetSharedFlag(dd, q_tree); 00294 if (MlTree_Regular(q_tree)->candidate) { 00295 if (!SynthUseCandidate(table, dd, q_tree, verbosity)) { 00296 bdd_recursive_deref_zdd(dd, q); 00297 return(NULL); 00298 } 00299 } 00300 if (MlTree_IsComplement(q_tree)) { 00301 q_tree = MlTree_Regular(q_tree); 00302 comp_q_tree = q_tree; 00303 } 00304 q_ref = 1; 00305 } else { 00306 q_tree = SynthFindOrCreateMlTree(table, dd, q, 1, 00307 0, &q_ref, verbosity); 00308 if (!q_tree) { 00309 bdd_recursive_deref_zdd(dd, q); 00310 return(NULL); 00311 } 00312 if (MlTree_IsComplement(q_tree)) { 00313 comp_q_tree = MlTree_Regular(q_tree); 00314 q_tree = comp_q_tree; 00315 } 00316 tmp_tree = q_tree; 00317 q_tree = SynthCheckAndMakeComplement(dd, table, q_tree, &comp_flag, 00318 verbosity); 00319 if (!q_tree) { 00320 bdd_recursive_deref_zdd(dd, q); 00321 return(NULL); 00322 } else if (q_tree == tmp_tree) { 00323 if (q_ref == 0) 00324 SynthPutMlTreeInList(dd, q_tree, 0); 00325 } else { 00326 if (comp_flag) 00327 comp_q_tree = q_tree; 00328 q_ref = 1; 00329 } 00330 } 00331 bdd_recursive_deref_zdd(dd, q); 00332 00333 if (bring) { 00334 tree = bring; 00335 tree->leaf = 0; 00336 tree->q = q_tree; 00337 tree->d = d_tree; 00338 tree->r = SynthFindOrCreateMlTree(table, dd, zero, 00339 1, 0, &r_ref, verbosity); 00340 if (!tree->r) 00341 return(NULL); 00342 if (MlTree_IsComplement(tree->r)) { 00343 tree->r = MlTree_Regular(tree->r); 00344 tree->r_comp = 1; 00345 } 00346 if (comp_q_tree) 00347 tree->q_comp = 1; 00348 if (comp_d_flag) 00349 tree->d_comp = 1; 00350 tree->q_ref = q_ref; 00351 tree->d_ref = d_ref; 00352 tree->r_ref = r_ref; 00353 if (verbosity > 1) 00354 SynthPrintMlTreeMessage(dd, tree, message); 00355 if (VerifyTreeMode) { 00356 SynthVerifyTree(dd, tree, 0); 00357 SynthVerifyMlTable(dd, table); 00358 } 00359 return(tree); 00360 } 00361 00362 tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity); 00363 if (!tree) 00364 return(NULL); 00365 if (*ref) 00366 (void) fprintf(vis_stdout, 00367 "** synth warning: May be duplicate.\n"); 00368 tree->q = q_tree; 00369 tree->d = d_tree; 00370 tree->r = SynthFindOrCreateMlTree(table, dd, zero, 1, 00371 0, &r_ref, verbosity); 00372 if (!tree->r) 00373 return(NULL); 00374 if (MlTree_IsComplement(tree->r)) { 00375 tree->r = MlTree_Regular(tree->r); 00376 tree->r_comp = 1; 00377 } 00378 if (comp_q_tree) 00379 tree->q_comp = 1; 00380 if (comp_d_flag) 00381 tree->d_comp = 1; 00382 tree->q_ref = q_ref; 00383 tree->d_ref = d_ref; 00384 tree->r_ref = r_ref; 00385 if (verbosity > 1) 00386 SynthPrintMlTreeMessage(dd, tree, message); 00387 SynthPutMlTreeInList(dd, tree, 0); 00388 if (VerifyTreeMode) { 00389 SynthVerifyTree(dd, tree, 0); 00390 SynthVerifyMlTable(dd, table); 00391 } 00392 return(tree); 00393 } 00394 } else 00395 bdd_recursive_deref_zdd(dd, d); 00396 00397 tree = LiteralFactoringTree(dd, table, f, q, level + 1, ref, 00398 bring, verbosity); 00399 if (!tree) { 00400 bdd_recursive_deref_zdd(dd, q); 00401 return(NULL); 00402 } 00403 tmp_tree = tree; 00404 tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity); 00405 if (!tree) { 00406 bdd_recursive_deref_zdd(dd, q); 00407 return(NULL); 00408 } else if (tree != tmp_tree) { 00409 *ref = 1; 00410 if (comp_flag) 00411 tree = MlTree_Not(tree); 00412 } 00413 bdd_recursive_deref_zdd(dd, q); 00414 00415 if (verbosity > 1) 00416 SynthPrintMlTreeMessage(dd, tree, message); 00417 return(tree); 00418 } 00419 bdd_recursive_deref_zdd(dd, d); 00420 00421 d_tree = comp_d_tree = (MlTree *)NULL; 00422 00423 tmp = q; 00424 q = SynthMakeCubeFree(dd, q); 00425 if (!q) { 00426 bdd_recursive_deref_zdd(dd,tmp); 00427 return(NULL); 00428 } 00429 bdd_ref(q); 00430 bdd_recursive_deref_zdd(dd,tmp); 00431 00432 q_tree = (MlTree *)NULL; 00433 if (st_lookup(table, (char *)q, &q_tree)) { 00434 SynthSetSharedFlag(dd, q_tree); 00435 if (MlTree_Regular(q_tree)->candidate) { 00436 if (!SynthUseCandidate(table, dd, q_tree, verbosity)) { 00437 bdd_recursive_deref_zdd(dd, q); 00438 return(NULL); 00439 } 00440 } 00441 if (MlTree_IsComplement(q_tree)) { 00442 q_tree = MlTree_Regular(q_tree); 00443 comp_q_tree = q_tree; 00444 q_tree = (MlTree *)NULL; 00445 } 00446 } 00447 00448 d = (* SynthGetZddDivideFunc())(dd, f, q); 00449 if (!d) { 00450 bdd_recursive_deref_zdd(dd, q); 00451 return(NULL); 00452 } 00453 bdd_ref(d); 00454 d_tree = (MlTree *)NULL; 00455 if (st_lookup(table, (char *)d, &d_tree)) { 00456 SynthSetSharedFlag(dd, d_tree); 00457 if (MlTree_Regular(d_tree)->candidate) { 00458 if (!SynthUseCandidate(table, dd, d_tree, verbosity)) { 00459 bdd_recursive_deref_zdd(dd, d); 00460 bdd_recursive_deref_zdd(dd, q); 00461 return(NULL); 00462 } 00463 } 00464 if (MlTree_IsComplement(d_tree)) { 00465 d_tree = MlTree_Regular(d_tree); 00466 comp_d_tree = d_tree; 00467 d_tree = (MlTree *)NULL; 00468 } 00469 } 00470 00471 m = (* SynthGetZddProductFunc())(dd, d, q); 00472 if (!m) { 00473 bdd_recursive_deref_zdd(dd, d); 00474 bdd_recursive_deref_zdd(dd, q); 00475 return(NULL); 00476 } 00477 bdd_ref(m); 00478 r = bdd_zdd_diff(dd, f, m); 00479 if (!r) { 00480 bdd_recursive_deref_zdd(dd, d); 00481 bdd_recursive_deref_zdd(dd, q); 00482 bdd_recursive_deref_zdd(dd, m); 00483 return(NULL); 00484 } 00485 bdd_ref(r); 00486 00487 r_tree = (MlTree *)NULL; 00488 if (st_lookup(table, (char *)r, &r_tree)) { 00489 SynthSetSharedFlag(dd, r_tree); 00490 if (MlTree_Regular(r_tree)->candidate) { 00491 if (!SynthUseCandidate(table, dd, r_tree, verbosity)) { 00492 bdd_recursive_deref_zdd(dd, d); 00493 bdd_recursive_deref_zdd(dd, q); 00494 bdd_recursive_deref_zdd(dd, m); 00495 bdd_recursive_deref_zdd(dd, r); 00496 return(NULL); 00497 } 00498 } 00499 if (MlTree_IsComplement(r_tree)) { 00500 r_tree = MlTree_Regular(r_tree); 00501 comp_r_tree = r_tree; 00502 r_tree = (MlTree *)NULL; 00503 } 00504 } 00505 00506 if (IsCubeFree(dd, d)) { 00507 tree = SynthFactorTreeRecur(dd, table, SynthGenericFactorTree, 00508 f, q, d, r, m, q_tree, d_tree, r_tree, 00509 comp_q_tree, comp_d_tree, comp_r_tree, 00510 bring, level, space, message, ref, verbosity); 00511 bdd_recursive_deref_zdd(dd, d); 00512 bdd_recursive_deref_zdd(dd, q); 00513 bdd_recursive_deref_zdd(dd, m); 00514 bdd_recursive_deref_zdd(dd, r); 00515 return(tree); 00516 } 00517 00518 bdd_recursive_deref_zdd(dd, q); 00519 bdd_recursive_deref_zdd(dd, r); 00520 00521 c = CommonCube(dd, d); 00522 if (!c) { 00523 bdd_recursive_deref_zdd(dd, d); 00524 return(NULL); 00525 } 00526 bdd_ref(c); 00527 bdd_recursive_deref_zdd(dd, d); 00528 tree = LiteralFactoringTree(dd, table, f, c, level + 1, 00529 ref, bring, verbosity); 00530 if (!tree) { 00531 bdd_recursive_deref_zdd(dd, c); 00532 return(NULL); 00533 } 00534 tmp_tree = tree; 00535 tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity); 00536 if (!tree) { 00537 bdd_recursive_deref_zdd(dd, c); 00538 if (*ref == 0) 00539 SynthFreeMlTree(MlTree_Regular(tree), 1); 00540 return(NULL); 00541 } else if (tree != tmp_tree) { 00542 *ref = 1; 00543 if (comp_flag) 00544 tree = MlTree_Not(tree); 00545 } 00546 bdd_recursive_deref_zdd(dd, c); 00547 00548 if (verbosity > 1) 00549 SynthPrintMlTreeMessage(dd, tree, message); 00550 if (VerifyTreeMode) { 00551 SynthVerifyTree(dd, tree, 0); 00552 SynthVerifyMlTable(dd, table); 00553 } 00554 return(tree); 00555 } 00556 00557 00570 bdd_node * 00571 SynthMakeCubeFree(bdd_manager *dd, 00572 bdd_node *f) 00573 { 00574 int i, v; 00575 int nvars, max_count, max_pos = 0; 00576 int *count; 00577 bdd_node *one = bdd_read_one(dd); 00578 bdd_node *zero = bdd_read_zero(dd); 00579 bdd_node *divisor, *node; 00580 bdd_node *tmp1, *tmp2; 00581 int ncubes; 00582 00583 if (f == one || f == zero) 00584 return(f); 00585 00586 /* Compare the number of occurrences of each literal to the number of 00587 * cubes in the cover. If no literal appears more than once, or if no 00588 * literal appears in all cubes, f is already cube-free. 00589 */ 00590 ncubes = bdd_zdd_count(dd, f); 00591 v = -1; 00592 max_count = 1; 00593 nvars = bdd_num_zdd_vars(dd); 00594 count = ALLOC(int, nvars); 00595 (void)memset((void *)count, 0, sizeof(int) * nvars); 00596 SynthCountLiteralOccurrence(dd, f, count); 00597 for (i = 0; i < nvars; i++) { 00598 if (count[i] > max_count) { 00599 v = i; 00600 max_count = count[i]; 00601 max_pos = i; 00602 } 00603 } 00604 if (v == -1 || max_count < ncubes) { 00605 FREE(count); 00606 return(f); 00607 } 00608 00609 /* Divide the cover by the first literal appearing in all cubes. */ 00610 node = bdd_zdd_get_node(dd, v, one, zero); 00611 if (!node) { 00612 FREE(count); 00613 return(NULL); 00614 } 00615 bdd_ref(node); 00616 divisor = (* SynthGetZddDivideFunc())(dd, f, node); 00617 if (!divisor) { 00618 bdd_recursive_deref_zdd(dd, node); 00619 FREE(count); 00620 return(NULL); 00621 } 00622 bdd_ref(divisor); 00623 bdd_recursive_deref_zdd(dd, node); 00624 00625 /* Divide the cover by the remaining literals appearing in all cubes. */ 00626 for (i = max_pos + 1; i < nvars; i++) { 00627 if (count[i] == max_count) { 00628 tmp1 = divisor; 00629 tmp2 = bdd_zdd_get_node(dd, i, one, zero); 00630 if (!tmp2) { 00631 FREE(count); 00632 bdd_recursive_deref_zdd(dd, tmp1); 00633 return(NULL); 00634 } 00635 bdd_ref(tmp2); 00636 divisor = (* SynthGetZddDivideFunc())(dd, divisor, tmp2); 00637 if (!divisor) { 00638 FREE(count); 00639 bdd_recursive_deref_zdd(dd, tmp1); 00640 bdd_recursive_deref_zdd(dd, tmp2); 00641 return(NULL); 00642 } 00643 bdd_ref(divisor); 00644 bdd_recursive_deref_zdd(dd, tmp1); 00645 bdd_recursive_deref_zdd(dd, tmp2); 00646 } 00647 } 00648 FREE(count); 00649 bdd_deref(divisor); 00650 return(divisor); 00651 } 00652 00653 00654 /*---------------------------------------------------------------------------*/ 00655 /* Definition of static functions */ 00656 /*---------------------------------------------------------------------------*/ 00657 00669 static MlTree * 00670 LiteralFactoringTree(bdd_manager *dd, 00671 st_table *table, 00672 bdd_node *f, 00673 bdd_node *c, 00674 int level, 00675 int *ref, 00676 MlTree *bring, 00677 int verbosity) 00678 { 00679 bdd_node *one = bdd_read_one(dd); 00680 bdd_node *zero = bdd_read_zero(dd); 00681 bdd_node *l, *q, *r; 00682 bdd_node *m; 00683 char message[80]; 00684 char space[80]; 00685 MlTree *tree, *q_tree, *d_tree, *r_tree; 00686 int q_ref, d_ref, r_ref, m_ref; 00687 char comp_mess[120]; 00688 MlTree *comp_q_tree = (MlTree *)NULL; 00689 MlTree *comp_d_tree = (MlTree *)NULL; 00690 MlTree *comp_r_tree = (MlTree *)NULL; 00691 MlTree *m_tree; 00692 int q_tree_exist, r_tree_exist; 00693 MlTree *tmp_tree; 00694 int comp_flag; 00695 00696 if (verbosity > 1) { 00697 SynthGetSpaceString(space, level * 2, 80); 00698 sprintf(message, "%s[%d] in : ", space, level); 00699 SynthPrintZddTreeMessage(dd, f, message); 00700 sprintf(message, "%s[%d]out : ", space, level); 00701 } 00702 00703 l = BestLiteral(dd, f, c); 00704 if (!l) 00705 return(NULL); 00706 bdd_ref(l); 00707 d_tree = (MlTree *)NULL; 00708 if (st_lookup(table, (char *)l, &d_tree)) { 00709 SynthSetSharedFlag(dd, d_tree); 00710 if (MlTree_Regular(d_tree)->candidate) { 00711 if (!SynthUseCandidate(table, dd, d_tree, verbosity)) { 00712 bdd_recursive_deref_zdd(dd, l); 00713 return(NULL); 00714 } 00715 } 00716 if (MlTree_IsComplement(d_tree)) { 00717 d_tree = MlTree_Regular(d_tree); 00718 comp_d_tree = d_tree; 00719 d_tree = (MlTree *)NULL; 00720 } 00721 } 00722 q = (* SynthGetZddDivideFunc())(dd, f, l); 00723 if (!q) { 00724 bdd_recursive_deref_zdd(dd, l); 00725 return(NULL); 00726 } 00727 bdd_ref(q); 00728 q_tree = (MlTree *)NULL; 00729 if (st_lookup(table, (char *)q, &q_tree)) { 00730 SynthSetSharedFlag(dd, q_tree); 00731 if (MlTree_Regular(q_tree)->candidate) { 00732 if (!SynthUseCandidate(table, dd, q_tree, verbosity)) { 00733 bdd_recursive_deref_zdd(dd, l); 00734 bdd_recursive_deref_zdd(dd, q); 00735 return(NULL); 00736 } 00737 } 00738 if (MlTree_IsComplement(q_tree)) { 00739 q_tree = MlTree_Regular(q_tree); 00740 comp_q_tree = q_tree; 00741 q_tree = (MlTree *)NULL; 00742 } 00743 } 00744 00745 m = (* SynthGetZddProductFunc())(dd, l, q); 00746 if (!m) { 00747 bdd_recursive_deref_zdd(dd, l); 00748 bdd_recursive_deref_zdd(dd, q); 00749 return(NULL); 00750 } 00751 bdd_ref(m); 00752 r = bdd_zdd_diff(dd, f, m); 00753 if (!r) { 00754 bdd_recursive_deref_zdd(dd, l); 00755 bdd_recursive_deref_zdd(dd, q); 00756 bdd_recursive_deref_zdd(dd, m); 00757 return(NULL); 00758 } 00759 bdd_ref(r); 00760 00761 r_tree = (MlTree *)NULL; 00762 if (st_lookup(table, (char *)r, &r_tree)) { 00763 SynthSetSharedFlag(dd, r_tree); 00764 if (MlTree_Regular(r_tree)->candidate) { 00765 if (!SynthUseCandidate(table, dd, r_tree, verbosity)) { 00766 bdd_recursive_deref_zdd(dd, l); 00767 bdd_recursive_deref_zdd(dd, q); 00768 bdd_recursive_deref_zdd(dd, m); 00769 bdd_recursive_deref_zdd(dd, r); 00770 return(NULL); 00771 } 00772 } 00773 if (MlTree_IsComplement(r_tree)) { 00774 r_tree = MlTree_Regular(r_tree); 00775 comp_r_tree = r_tree; 00776 r_tree = (MlTree *)NULL; 00777 } 00778 } 00779 00780 if (verbosity > 1) 00781 (void) fprintf(vis_stdout,"%s[%d] quotient\n", 00782 space, level); 00783 q_tree_exist = 0; 00784 if (q_tree) { 00785 q_ref = 1; 00786 q_tree_exist = 1; 00787 } else if (comp_q_tree) { 00788 q_tree = comp_q_tree; 00789 q_ref = 1; 00790 if (verbosity > 1) { 00791 sprintf(comp_mess, "%s\t(C) : ", space); 00792 SynthPrintZddTreeMessage(dd, q, comp_mess); 00793 } 00794 } else { 00795 q_tree = SynthGenericFactorTree(dd, table, q, level + 1, &q_ref, 00796 NULL, 0, NULL, verbosity); 00797 if (!q_tree) { 00798 bdd_recursive_deref_zdd(dd, l); 00799 bdd_recursive_deref_zdd(dd, q); 00800 bdd_recursive_deref_zdd(dd, m); 00801 bdd_recursive_deref_zdd(dd, r); 00802 return(NULL); 00803 } 00804 if (MlTree_IsComplement(q_tree)) { 00805 q_tree = MlTree_Regular(q_tree); 00806 comp_q_tree = q_tree; 00807 } else 00808 bdd_ref(q_tree->node); 00809 } 00810 tmp_tree = q_tree; 00811 q_tree = SynthCheckAndMakeComplement(dd, table, q_tree, &comp_flag, 00812 verbosity); 00813 if (!q_tree) { 00814 bdd_recursive_deref_zdd(dd, l); 00815 bdd_recursive_deref_zdd(dd, q); 00816 bdd_recursive_deref_zdd(dd, m); 00817 bdd_recursive_deref_zdd(dd, r); 00818 if (comp_q_tree != q_tree) 00819 bdd_recursive_deref_zdd(dd, tmp_tree->node); 00820 if (q_ref == 0) 00821 SynthFreeMlTree(MlTree_Regular(tmp_tree), 1); 00822 return(NULL); 00823 } 00824 if (q_tree != tmp_tree) { 00825 if (comp_flag) 00826 comp_q_tree = q_tree; 00827 q_ref = 1; 00828 } 00829 00830 if (verbosity > 1) 00831 (void) fprintf(vis_stdout,"%s[%d] literal\n", space, level); 00832 if (d_tree) { 00833 d_ref = 1; 00834 if (verbosity > 1) { 00835 sprintf(comp_mess, "%s\t(R) : ", space); 00836 SynthPrintZddTreeMessage(dd, l, comp_mess); 00837 } 00838 } else if (comp_d_tree) { 00839 d_tree = comp_d_tree; 00840 d_ref = 1; 00841 if (verbosity > 1) { 00842 sprintf(comp_mess, "%s\t(C) : ", space); 00843 SynthPrintZddTreeMessage(dd, l, comp_mess); 00844 } 00845 } else { 00846 d_tree = SynthFindOrCreateMlTree(table, dd, l, 1, 0, &d_ref, verbosity); 00847 if (!d_tree) { 00848 bdd_recursive_deref_zdd(dd, l); 00849 bdd_recursive_deref_zdd(dd, q); 00850 bdd_recursive_deref_zdd(dd, m); 00851 bdd_recursive_deref_zdd(dd, r); 00852 if (comp_q_tree != q_tree) 00853 bdd_recursive_deref_zdd(dd, q_tree->node); 00854 if (q_ref == 0) 00855 SynthFreeMlTree(MlTree_Regular(q_tree), 1); 00856 return(NULL); 00857 } 00858 if (MlTree_IsComplement(d_tree)) { 00859 comp_d_tree = MlTree_Regular(d_tree); 00860 d_tree = comp_d_tree; 00861 } 00862 if (verbosity > 1) { 00863 sprintf(comp_mess, "%s\t : ", space); 00864 SynthPrintZddTreeMessage(dd, l, comp_mess); 00865 } 00866 tmp_tree = d_tree; 00867 d_tree = SynthCheckAndMakeComplement(dd, table, d_tree, &comp_flag, 00868 verbosity); 00869 if (!d_tree) { 00870 bdd_recursive_deref_zdd(dd, l); 00871 bdd_recursive_deref_zdd(dd, q); 00872 bdd_recursive_deref_zdd(dd, m); 00873 bdd_recursive_deref_zdd(dd, r); 00874 if (comp_q_tree != q_tree) 00875 bdd_recursive_deref_zdd(dd, q_tree->node); 00876 if (q_ref == 0) 00877 SynthFreeMlTree(MlTree_Regular(q_tree), 1); 00878 if (d_ref == 0) 00879 SynthFreeMlTree(MlTree_Regular(d_tree), 1); 00880 return(NULL); 00881 } else if (d_tree == tmp_tree) { 00882 if (d_ref == 0) 00883 SynthPutMlTreeInList(dd, d_tree, 0); 00884 } else { 00885 if (comp_flag) 00886 comp_d_tree = d_tree; 00887 d_ref = 1; 00888 } 00889 } 00890 00891 m_tree = (MlTree *)NULL; 00892 m_ref = 0; 00893 if (UseMtree && m != f) { 00894 m_tree = SynthFindOrCreateMlTree(table, dd, m, 0, 1, &m_ref, verbosity); 00895 if (!m_tree) { 00896 bdd_recursive_deref_zdd(dd, l); 00897 bdd_recursive_deref_zdd(dd, q); 00898 bdd_recursive_deref_zdd(dd, m); 00899 bdd_recursive_deref_zdd(dd, r); 00900 if (comp_q_tree != q_tree) 00901 bdd_recursive_deref_zdd(dd, q_tree->node); 00902 if (q_ref == 0) 00903 SynthFreeMlTree(MlTree_Regular(q_tree), 1); 00904 if (d_ref == 0) 00905 SynthFreeMlTree(MlTree_Regular(d_tree), 1); 00906 return(NULL); 00907 } 00908 if (m_ref == 0) { 00909 m_tree->q = q_tree; 00910 m_tree->d = d_tree; 00911 m_tree->r = (MlTree *)NULL; 00912 if (comp_q_tree) 00913 m_tree->q_comp = 1; 00914 if (comp_d_tree) 00915 m_tree->d_comp = 1; 00916 m_tree->q_ref = q_ref; 00917 m_tree->d_ref = d_ref; 00918 m_tree->r_ref = 0; 00919 00920 tmp_tree = m_tree; 00921 m_tree = SynthCheckAndMakeComplement(dd, table, m_tree, &comp_flag, 00922 verbosity); 00923 if (!m_tree) { 00924 bdd_recursive_deref_zdd(dd, l); 00925 bdd_recursive_deref_zdd(dd, q); 00926 bdd_recursive_deref_zdd(dd, m); 00927 bdd_recursive_deref_zdd(dd, r); 00928 if (comp_q_tree != q_tree) 00929 bdd_recursive_deref_zdd(dd, q_tree->node); 00930 if (q_ref == 0) 00931 SynthFreeMlTree(MlTree_Regular(q_tree), 1); 00932 if (d_ref == 0) 00933 SynthFreeMlTree(MlTree_Regular(d_tree), 1); 00934 return(NULL); 00935 } else if (m_tree == tmp_tree) 00936 SynthPutMlTreeInList(dd, m_tree, 1); 00937 else { 00938 if (m_tree->candidate) 00939 SynthPutMlTreeInList(dd, m_tree, 1); 00940 else 00941 m_tree = NIL(MlTree); 00942 } 00943 if (m_tree && VerifyTreeMode) { 00944 SynthVerifyTree(dd, m_tree, 0); 00945 SynthVerifyMlTable(dd, table); 00946 } 00947 } 00948 } 00949 bdd_recursive_deref_zdd(dd, m); 00950 00951 if (verbosity > 1) 00952 (void) fprintf(vis_stdout, "%s[%d] remainder\n", space, level); 00953 r_tree_exist = 0; 00954 if (r_tree) { 00955 r_ref = 1; 00956 r_tree_exist = 1; 00957 } else if (comp_r_tree) { 00958 r_tree = comp_r_tree; 00959 r_ref = 1; 00960 if (verbosity > 1) { 00961 sprintf(comp_mess, "%s\t(C) : ", space); 00962 SynthPrintZddTreeMessage(dd, r, comp_mess); 00963 } 00964 } else if (comp_d_tree) { 00965 r_tree = SynthGenericFactorTree(dd, table, r, level + 1, &r_ref, 00966 NULL, 0, NULL, verbosity); 00967 if (!r_tree) { 00968 bdd_recursive_deref_zdd(dd, l); 00969 bdd_recursive_deref_zdd(dd, q); 00970 bdd_recursive_deref_zdd(dd, r); 00971 if (comp_q_tree != q_tree) 00972 bdd_recursive_deref_zdd(dd, q_tree->node); 00973 if (q_ref == 0) 00974 SynthFreeMlTree(MlTree_Regular(q_tree), 1); 00975 if (d_ref == 0) 00976 SynthFreeMlTree(MlTree_Regular(d_tree), 1); 00977 if (m_tree && m_ref == 0) 00978 SynthFreeMlTree(MlTree_Regular(m_tree), 1); 00979 return(NULL); 00980 } 00981 if (MlTree_IsComplement(r_tree)) { 00982 r_tree = MlTree_Regular(r_tree); 00983 comp_r_tree = r_tree; 00984 } else 00985 bdd_ref(r_tree->node); 00986 } else { 00987 if (Resubstitution) { 00988 r_tree = SynthGenericFactorTree(dd, table, r, level + 1, 00989 &r_ref, d_tree, 1, NULL, verbosity); 00990 if (!r_tree && (bdd_read_reordered_field(dd) || noMemoryFlag)) { 00991 bdd_recursive_deref_zdd(dd, l); 00992 bdd_recursive_deref_zdd(dd, q); 00993 bdd_recursive_deref_zdd(dd, r); 00994 if (comp_q_tree != q_tree) 00995 bdd_recursive_deref_zdd(dd, q_tree->node); 00996 if (q_ref == 0) 00997 SynthFreeMlTree(MlTree_Regular(q_tree), 1); 00998 if (d_ref == 0) 00999 SynthFreeMlTree(MlTree_Regular(d_tree), 1); 01000 if (m_tree && m_ref == 0) 01001 SynthFreeMlTree(MlTree_Regular(m_tree), 1); 01002 return(NULL); 01003 } 01004 } 01005 if (!r_tree) { 01006 r_tree = SynthGenericFactorTree(dd, table, r, level + 1, 01007 &r_ref, NULL, 0, NULL, verbosity); 01008 if (!r_tree) { 01009 bdd_recursive_deref_zdd(dd, l); 01010 bdd_recursive_deref_zdd(dd, q); 01011 bdd_recursive_deref_zdd(dd, r); 01012 if (comp_q_tree != q_tree) 01013 bdd_recursive_deref_zdd(dd, q_tree->node); 01014 if (q_ref == 0) 01015 SynthFreeMlTree(MlTree_Regular(q_tree), 1); 01016 if (d_ref == 0) 01017 SynthFreeMlTree(MlTree_Regular(d_tree), 1); 01018 if (m_tree && m_ref == 0) 01019 SynthFreeMlTree(MlTree_Regular(m_tree), 1); 01020 return(NULL); 01021 } 01022 } else { 01023 if (r != one && r != zero) 01024 SynthSetSharedFlag(dd, d_tree); 01025 } 01026 if (MlTree_IsComplement(r_tree)) { 01027 r_tree = MlTree_Regular(r_tree); 01028 comp_r_tree = r_tree; 01029 } else 01030 bdd_ref(r_tree->node); 01031 } 01032 if (RemainderComplement) { 01033 tmp_tree = r_tree; 01034 r_tree = SynthCheckAndMakeComplement(dd, table, r_tree, &comp_flag, 01035 verbosity); 01036 if (!r_tree) { 01037 bdd_recursive_deref_zdd(dd, l); 01038 bdd_recursive_deref_zdd(dd, q); 01039 bdd_recursive_deref_zdd(dd, r); 01040 if (comp_q_tree != q_tree) 01041 bdd_recursive_deref_zdd(dd, q_tree->node); 01042 if (comp_r_tree != r_tree) 01043 bdd_recursive_deref_zdd(dd, r_tree->node); 01044 if (q_ref == 0) 01045 SynthFreeMlTree(MlTree_Regular(q_tree), 1); 01046 if (d_ref == 0) 01047 SynthFreeMlTree(MlTree_Regular(d_tree), 1); 01048 if (r_ref == 0) 01049 SynthFreeMlTree(MlTree_Regular(r_tree), 1); 01050 if (m_tree && m_ref == 0) 01051 SynthFreeMlTree(MlTree_Regular(m_tree), 1); 01052 return(NULL); 01053 } 01054 if (r_tree != tmp_tree) { 01055 if (comp_flag) 01056 comp_r_tree = r_tree; 01057 r_ref = 1; 01058 } 01059 } 01060 01061 bdd_recursive_deref_zdd(dd, l); 01062 bdd_recursive_deref_zdd(dd, q); 01063 bdd_recursive_deref_zdd(dd, r); 01064 if ((!q_tree_exist) && (!comp_q_tree)) 01065 bdd_recursive_deref_zdd(dd, q_tree->node); 01066 if ((!r_tree_exist) && (!comp_r_tree)) 01067 bdd_recursive_deref_zdd(dd, r_tree->node); 01068 01069 if (bring) { 01070 tree = bring; 01071 tree->leaf = 0; 01072 tree->q = q_tree; 01073 tree->d = d_tree; 01074 tree->r = r_tree; 01075 if (comp_q_tree) 01076 tree->q_comp = 1; 01077 if (comp_d_tree) 01078 tree->d_comp = 1; 01079 if (comp_r_tree) 01080 tree->r_comp = 1; 01081 tree->q_ref = q_ref; 01082 tree->d_ref = d_ref; 01083 tree->r_ref = r_ref; 01084 if (UseMtree && m_tree && m_ref == 0) { 01085 MlTree_Regular(m_tree)->r = tree; 01086 if (m_tree->r->id == 0) { 01087 assert(0); 01088 /* 01089 if (!SynthUseCandidate(table, dd, m_tree, verbosity)) { 01090 SynthFreeMlTree(MlTree_Regular(m_tree), 1); 01091 return(NULL); 01092 } 01093 */ 01094 } 01095 } 01096 if (verbosity > 1) 01097 SynthPrintMlTreeMessage(dd, tree, message); 01098 if (VerifyTreeMode) { 01099 SynthVerifyTree(dd, tree, 0); 01100 SynthVerifyMlTable(dd, table); 01101 } 01102 return(tree); 01103 } 01104 01105 tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity); 01106 if (!tree) { 01107 if (q_ref == 0) 01108 SynthFreeMlTree(MlTree_Regular(q_tree), 1); 01109 if (d_ref == 0) 01110 SynthFreeMlTree(MlTree_Regular(d_tree), 1); 01111 if (r_ref == 0) 01112 SynthFreeMlTree(MlTree_Regular(r_tree), 1); 01113 if (m_tree && m_ref == 0) 01114 SynthFreeMlTree(MlTree_Regular(m_tree), 1); 01115 return(NULL); 01116 } 01117 if (*ref == 1) 01118 (void) fprintf(vis_stdout, "** synth warning: May be duplicate.\n"); 01119 tree->q = q_tree; 01120 tree->d = d_tree; 01121 tree->r = r_tree; 01122 if (comp_q_tree) 01123 tree->q_comp = 1; 01124 if (comp_d_tree) 01125 tree->d_comp = 1; 01126 if (comp_r_tree) 01127 tree->r_comp = 1; 01128 tree->q_ref = q_ref; 01129 tree->d_ref = d_ref; 01130 tree->r_ref = r_ref; 01131 if (UseMtree && m_tree && m_ref == 0) { 01132 MlTree_Regular(m_tree)->r = tree; 01133 if (m_tree->r->id == 0) { 01134 assert(0); 01135 /* 01136 if (!SynthUseCandidate(table, dd, m_tree, verbosity)) { 01137 SynthFreeMlTree(MlTree_Regular(tree), 1); 01138 SynthFreeMlTree(MlTree_Regular(m_tree), 1); 01139 return(NULL); 01140 } 01141 */ 01142 } 01143 } 01144 if (verbosity > 1) 01145 SynthPrintMlTreeMessage(dd, tree, message); 01146 SynthPutMlTreeInList(dd, tree, 0); 01147 if (VerifyTreeMode) { 01148 SynthVerifyTree(dd, tree, 0); 01149 SynthVerifyMlTable(dd, table); 01150 } 01151 return(tree); 01152 } 01153 01167 static bdd_node * 01168 BestLiteral(bdd_manager *dd, 01169 bdd_node *f, 01170 bdd_node *c) 01171 { 01172 int i, v; 01173 int nvars, max_count; 01174 int *count_f, *count_c; 01175 bdd_node *one = bdd_read_one(dd); 01176 bdd_node *zero = bdd_read_zero(dd); 01177 bdd_node *node; 01178 01179 v = -1; 01180 max_count = 0; 01181 nvars = bdd_num_zdd_vars(dd); 01182 count_f = ALLOC(int, nvars); 01183 (void)memset((void *)count_f, 0, sizeof(int) * nvars); 01184 SynthCountLiteralOccurrence(dd, f, count_f); 01185 count_c = ALLOC(int, nvars); 01186 (void)memset((void *)count_c, 0, sizeof(int) * nvars); 01187 SynthCountLiteralOccurrence(dd, c, count_c); 01188 01189 for (i = 0; i < nvars; i++) { 01190 if (count_c[i]) { 01191 if (count_f[i] > max_count) { 01192 v = i; 01193 max_count = count_f[i]; 01194 } 01195 } 01196 } 01197 01198 if (v == -1) { 01199 FREE(count_f); 01200 FREE(count_c); 01201 return(zero); 01202 } 01203 01204 node = bdd_zdd_get_node(dd, v, one, zero); 01205 if (!node) { 01206 FREE(count_f); 01207 FREE(count_c); 01208 return(NULL); 01209 } 01210 FREE(count_f); 01211 FREE(count_c); 01212 return(node); 01213 } 01214 01215 01227 static int 01228 IsCubeFree(bdd_manager *dd, 01229 bdd_node *f) 01230 { 01231 int i, v; 01232 int nvars, max_count; 01233 int *count; 01234 bdd_node *one = bdd_read_one(dd); 01235 bdd_node *zero = bdd_read_zero(dd); 01236 int ncubes; 01237 01238 if (f == one || f == zero) 01239 return(1); 01240 01241 ncubes = bdd_zdd_count(dd, f); 01242 v = -1; 01243 max_count = 1; 01244 nvars = bdd_num_zdd_vars(dd); 01245 count = ALLOC(int, nvars); 01246 (void)memset((void *)count, 0, sizeof(int) * nvars); 01247 SynthCountLiteralOccurrence(dd, f, count); 01248 for (i = 0; i < nvars; i++) { 01249 if (count[i] > max_count) { 01250 v = i; 01251 max_count = count[i]; 01252 } 01253 } 01254 FREE(count); 01255 01256 if (v == -1 || max_count < ncubes) 01257 return(1); 01258 01259 return(0); 01260 } 01261 01273 static bdd_node * 01274 CommonCube(bdd_manager *dd, 01275 bdd_node *f) 01276 { 01277 int i, v; 01278 int nvars, max_count, max_pos = 0; 01279 int *count; 01280 bdd_node *one = bdd_read_one(dd); 01281 bdd_node *zero = bdd_read_zero(dd); 01282 bdd_node *node; 01283 bdd_node *tmp1, *tmp2; 01284 int ncubes; 01285 01286 if (f == one || f == zero) { 01287 return(f); 01288 } 01289 01290 ncubes = bdd_zdd_count(dd, f); 01291 v = -1; 01292 max_count = 1; 01293 nvars = bdd_num_zdd_vars(dd); 01294 count = ALLOC(int, nvars); 01295 (void)memset((void *)count, 0, sizeof(int) * nvars); 01296 SynthCountLiteralOccurrence(dd, f, count); 01297 for (i = 0; i < nvars; i++) { 01298 if (count[i] > max_count) { 01299 v = i; 01300 max_count = count[i]; 01301 max_pos = i; 01302 } 01303 } 01304 if (v == -1 || max_count < ncubes) { 01305 FREE(count); 01306 return(zero); 01307 } 01308 01309 node = bdd_zdd_get_node(dd, v, one, zero); 01310 if (!node) { 01311 FREE(count); 01312 return(NULL); 01313 } 01314 bdd_ref(node); 01315 for (i = max_pos + 1; i < nvars; i++) { 01316 if (count[i] == max_count) { 01317 tmp1 = node; 01318 tmp2 = bdd_zdd_get_node(dd, i, one, zero); 01319 if (!tmp2) { 01320 FREE(count); 01321 bdd_recursive_deref_zdd(dd, tmp1); 01322 return(NULL); 01323 } 01324 bdd_ref(tmp2); 01325 node = (* SynthGetZddProductFunc())(dd, node, tmp2); 01326 if (!node) { 01327 FREE(count); 01328 bdd_recursive_deref_zdd(dd, tmp1); 01329 bdd_recursive_deref_zdd(dd, tmp2); 01330 return(NULL); 01331 } 01332 bdd_ref(node); 01333 bdd_recursive_deref_zdd(dd, tmp1); 01334 bdd_recursive_deref_zdd(dd, tmp2); 01335 } 01336 } 01337 FREE(count); 01338 bdd_deref(node); 01339 return(node); 01340 }
1.7.3