You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

4233 lines
101 KiB

  1. /**
  2. @file
  3. @ingroup cudd
  4. @brief Utility functions.
  5. @author Fabio Somenzi
  6. @copyright@parblock
  7. Copyright (c) 1995-2015, Regents of the University of Colorado
  8. All rights reserved.
  9. Redistribution and use in source and binary forms, with or without
  10. modification, are permitted provided that the following conditions
  11. are met:
  12. Redistributions of source code must retain the above copyright
  13. notice, this list of conditions and the following disclaimer.
  14. Redistributions in binary form must reproduce the above copyright
  15. notice, this list of conditions and the following disclaimer in the
  16. documentation and/or other materials provided with the distribution.
  17. Neither the name of the University of Colorado nor the names of its
  18. contributors may be used to endorse or promote products derived from
  19. this software without specific prior written permission.
  20. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  21. "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  22. LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  23. FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  24. COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  25. INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  26. BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  27. LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  28. CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  29. LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  30. ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  31. POSSIBILITY OF SUCH DAMAGE.
  32. @endparblock
  33. */
  34. #include <stddef.h>
  35. #include <float.h>
  36. #include "util.h"
  37. #include "epdInt.h"
  38. #include "cuddInt.h"
  39. /*---------------------------------------------------------------------------*/
  40. /* Constant declarations */
  41. /*---------------------------------------------------------------------------*/
  42. /* Random generator constants. */
  43. #define MODULUS1 2147483563
  44. #define LEQA1 40014
  45. #define LEQQ1 53668
  46. #define LEQR1 12211
  47. #define MODULUS2 2147483399
  48. #define LEQA2 40692
  49. #define LEQQ2 52774
  50. #define LEQR2 3791
  51. #define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)
  52. /*---------------------------------------------------------------------------*/
  53. /* Stucture declarations */
  54. /*---------------------------------------------------------------------------*/
  55. /*---------------------------------------------------------------------------*/
  56. /* Type declarations */
  57. /*---------------------------------------------------------------------------*/
  58. /*---------------------------------------------------------------------------*/
  59. /* Variable declarations */
  60. /*---------------------------------------------------------------------------*/
  61. /*---------------------------------------------------------------------------*/
  62. /* Macro declarations */
  63. /*---------------------------------------------------------------------------*/
  64. #define bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ')
  65. /** \cond */
  66. /*---------------------------------------------------------------------------*/
  67. /* Static function prototypes */
  68. /*---------------------------------------------------------------------------*/
  69. static int dp2 (DdManager *dd, DdNode *f, st_table *t);
  70. static void ddPrintMintermAux (DdManager *dd, DdNode *node, int *list);
  71. static int ddDagInt (DdNode *n);
  72. static int cuddNodeArrayRecur (DdNode *f, DdNodePtr *table, int index);
  73. static int cuddEstimateCofactor (DdManager *dd, st_table *table, DdNode * node, int i, int phase, DdNode ** ptr);
  74. static DdNode * cuddUniqueLookup (DdManager * unique, int index, DdNode * T, DdNode * E);
  75. static int cuddEstimateCofactorSimple (DdNode * node, int i);
  76. static double ddCountMintermAux (DdManager *dd, DdNode *node, double max, DdHashTable *table);
  77. static int ddEpdCountMintermAux (DdManager const *dd, DdNode *node, EpDouble *max, EpDouble *epd, st_table *table);
  78. static long double ddLdblCountMintermAux(DdManager const *manager, DdNode *node, long double max, st_table *table);
  79. static double ddCountPathAux (DdNode *node, st_table *table);
  80. static double ddCountPathsToNonZero (DdNode * N, st_table * table);
  81. static void ddSupportStep (DdNode *f, int *support);
  82. static void ddClearFlag (DdNode *f);
  83. static int ddLeavesInt (DdNode *n);
  84. static int ddPickArbitraryMinterms (DdManager *dd, DdNode *node, int nvars, int nminterms, char **string);
  85. static int ddPickRepresentativeCube (DdManager *dd, DdNode *node, double *weight, char *string);
  86. static enum st_retval ddEpdFree (void * key, void * value, void * arg);
  87. static void ddFindSupport(DdManager *dd, DdNode *f, int *SP);
  88. static void ddClearVars(DdManager *dd, int SP);
  89. static int indexCompare(const void *a, const void *b);
  90. static enum st_retval ddLdblFree(void * key, void * value, void * arg);
  91. #if HAVE_POWL != 1
  92. static long double powl(long double base, long double exponent);
  93. #endif
  94. /** \endcond */
  95. /*---------------------------------------------------------------------------*/
  96. /* Definition of exported functions */
  97. /*---------------------------------------------------------------------------*/
  98. /**
  99. @brief Prints a disjoint sum of products.
  100. @details Prints a disjoint sum of product cover for the function
  101. rooted at node. Each product corresponds to a path from node to a
  102. leaf node different from the logical zero, and different from the
  103. background value. Uses the package default output file.
  104. @return 1 if successful; 0 otherwise.
  105. @sideeffect None
  106. @see Cudd_PrintDebug Cudd_bddPrintCover
  107. */
  108. int
  109. Cudd_PrintMinterm(
  110. DdManager * manager,
  111. DdNode * node)
  112. {
  113. int i, *list;
  114. list = ALLOC(int,manager->size);
  115. if (list == NULL) {
  116. manager->errorCode = CUDD_MEMORY_OUT;
  117. return(0);
  118. }
  119. for (i = 0; i < manager->size; i++) list[i] = 2;
  120. ddPrintMintermAux(manager,node,list);
  121. FREE(list);
  122. return(1);
  123. } /* end of Cudd_PrintMinterm */
  124. /**
  125. @brief Prints a sum of prime implicants of a %BDD.
  126. @details Prints a sum of product cover for an incompletely
  127. specified function given by a lower bound and an upper bound. Each
  128. product is a prime implicant obtained by expanding the product
  129. corresponding to a path from node to the constant one. Uses the
  130. package default output file.
  131. @return 1 if successful; 0 otherwise.
  132. @sideeffect None
  133. @see Cudd_PrintMinterm
  134. */
  135. int
  136. Cudd_bddPrintCover(
  137. DdManager *dd,
  138. DdNode *l,
  139. DdNode *u)
  140. {
  141. int *array;
  142. int q, result;
  143. DdNode *lb;
  144. #ifdef DD_DEBUG
  145. DdNode *cover;
  146. #endif
  147. array = ALLOC(int, Cudd_ReadSize(dd));
  148. if (array == NULL) return(0);
  149. lb = l;
  150. cuddRef(lb);
  151. #ifdef DD_DEBUG
  152. cover = Cudd_ReadLogicZero(dd);
  153. cuddRef(cover);
  154. #endif
  155. while (lb != Cudd_ReadLogicZero(dd)) {
  156. DdNode *implicant, *prime, *tmp;
  157. int length;
  158. implicant = Cudd_LargestCube(dd,lb,&length);
  159. if (implicant == NULL) {
  160. Cudd_RecursiveDeref(dd,lb);
  161. FREE(array);
  162. return(0);
  163. }
  164. cuddRef(implicant);
  165. prime = Cudd_bddMakePrime(dd,implicant,u);
  166. if (prime == NULL) {
  167. Cudd_RecursiveDeref(dd,lb);
  168. Cudd_RecursiveDeref(dd,implicant);
  169. FREE(array);
  170. return(0);
  171. }
  172. cuddRef(prime);
  173. Cudd_RecursiveDeref(dd,implicant);
  174. tmp = Cudd_bddAnd(dd,lb,Cudd_Not(prime));
  175. if (tmp == NULL) {
  176. Cudd_RecursiveDeref(dd,lb);
  177. Cudd_RecursiveDeref(dd,prime);
  178. FREE(array);
  179. return(0);
  180. }
  181. cuddRef(tmp);
  182. Cudd_RecursiveDeref(dd,lb);
  183. lb = tmp;
  184. result = Cudd_BddToCubeArray(dd,prime,array);
  185. if (result == 0) {
  186. Cudd_RecursiveDeref(dd,lb);
  187. Cudd_RecursiveDeref(dd,prime);
  188. FREE(array);
  189. return(0);
  190. }
  191. for (q = 0; q < dd->size; q++) {
  192. switch (array[q]) {
  193. case 0:
  194. (void) fprintf(dd->out, "0");
  195. break;
  196. case 1:
  197. (void) fprintf(dd->out, "1");
  198. break;
  199. case 2:
  200. (void) fprintf(dd->out, "-");
  201. break;
  202. default:
  203. (void) fprintf(dd->out, "?");
  204. }
  205. }
  206. (void) fprintf(dd->out, " 1\n");
  207. #ifdef DD_DEBUG
  208. tmp = Cudd_bddOr(dd,prime,cover);
  209. if (tmp == NULL) {
  210. Cudd_RecursiveDeref(dd,cover);
  211. Cudd_RecursiveDeref(dd,lb);
  212. Cudd_RecursiveDeref(dd,prime);
  213. FREE(array);
  214. return(0);
  215. }
  216. cuddRef(tmp);
  217. Cudd_RecursiveDeref(dd,cover);
  218. cover = tmp;
  219. #endif
  220. Cudd_RecursiveDeref(dd,prime);
  221. }
  222. (void) fprintf(dd->out, "\n");
  223. Cudd_RecursiveDeref(dd,lb);
  224. FREE(array);
  225. #ifdef DD_DEBUG
  226. if (!Cudd_bddLeq(dd,cover,u) || !Cudd_bddLeq(dd,l,cover)) {
  227. Cudd_RecursiveDeref(dd,cover);
  228. return(0);
  229. }
  230. Cudd_RecursiveDeref(dd,cover);
  231. #endif
  232. return(1);
  233. } /* end of Cudd_bddPrintCover */
  234. /**
  235. @brief Prints to the manager standard output a %DD and its statistics.
  236. @details The statistics include the number of nodes, the number of leaves,
  237. and the number of minterms. (The number of minterms is the number of
  238. assignments to the variables that cause the function to be different
  239. from the logical zero (for BDDs) and from the background value (for
  240. ADDs.) The statistics are printed if pr &gt; 0. Specifically:
  241. <ul>
  242. <li> pr = 0 : prints nothing
  243. <li> pr = 1 : prints counts of nodes and minterms
  244. <li> pr = 2 : prints counts + disjoint sum of product
  245. <li> pr = 3 : prints counts + list of nodes
  246. <li> pr &gt; 3 : prints counts + disjoint sum of product + list of nodes
  247. </ul>
  248. For the purpose of counting the number of minterms, the function is
  249. supposed to depend on n variables.
  250. @return 1 if successful; 0 otherwise.
  251. @sideeffect None
  252. @see Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm
  253. Cudd_PrintMinterm
  254. */
  255. int
  256. Cudd_PrintDebug(
  257. DdManager * dd,
  258. DdNode * f,
  259. int n,
  260. int pr)
  261. {
  262. DdNode *azero, *bzero;
  263. int nodes;
  264. int leaves;
  265. double minterms;
  266. int retval = 1;
  267. if (dd == NULL) {
  268. return(0);
  269. }
  270. if (f == NULL) {
  271. (void) fprintf(dd->out,": is the NULL DD\n");
  272. (void) fflush(dd->out);
  273. dd->errorCode = CUDD_INVALID_ARG;
  274. return(0);
  275. }
  276. azero = DD_ZERO(dd);
  277. bzero = Cudd_Not(DD_ONE(dd));
  278. if ((f == azero || f == bzero) && pr > 0){
  279. (void) fprintf(dd->out,": is the zero DD\n");
  280. (void) fflush(dd->out);
  281. return(1);
  282. }
  283. if (pr > 0) {
  284. nodes = Cudd_DagSize(f);
  285. if (nodes == CUDD_OUT_OF_MEM) retval = 0;
  286. leaves = Cudd_CountLeaves(f);
  287. if (leaves == CUDD_OUT_OF_MEM) retval = 0;
  288. minterms = Cudd_CountMinterm(dd, f, n);
  289. if (minterms == (double)CUDD_OUT_OF_MEM) {
  290. retval = 0;
  291. (void) fprintf(dd->out,": %d nodes %d leaves unknown minterms\n",
  292. nodes, leaves);
  293. } else {
  294. (void) fprintf(dd->out,": %d nodes %d leaves %g minterms\n",
  295. nodes, leaves, minterms);
  296. }
  297. if (pr > 2) {
  298. if (!cuddP(dd, f)) retval = 0;
  299. }
  300. if (pr == 2 || pr > 3) {
  301. if (!Cudd_PrintMinterm(dd,f)) retval = 0;
  302. (void) fprintf(dd->out,"\n");
  303. }
  304. (void) fflush(dd->out);
  305. }
  306. return(retval);
  307. } /* end of Cudd_PrintDebug */
  308. /**
  309. @brief Prints a one-line summary of an %ADD or %BDD to the manager stdout.
  310. @details The summary includes the number of nodes, the number of leaves,
  311. and the number of minterms. The number of minterms is computed with
  312. arbitrary precision unlike Cudd_PrintDebug(). For the purpose of counting
  313. minterms, the function `f` is supposed to depend on `n` variables.
  314. @return 1 if successful; 0 otherwise.
  315. @see Cudd_PrintDebug Cudd_ApaPrintMinterm Cudd_ApaPrintMintermExp
  316. */
  317. int
  318. Cudd_PrintSummary(
  319. DdManager * dd /**< manager */,
  320. DdNode * f /**< %DD to be summarized */,
  321. int n /**< number of variables for minterm computation */,
  322. int mode /**< integer (0) or exponential (1) format */)
  323. {
  324. DdNode *azero, *bzero;
  325. int nodes, leaves, digits;
  326. int retval = 1;
  327. DdApaNumber count;
  328. if (dd == NULL) {
  329. return(0);
  330. }
  331. if (f == NULL) {
  332. (void) fprintf(dd->out,": is the NULL DD\n");
  333. (void) fflush(dd->out);
  334. dd->errorCode = CUDD_INVALID_ARG;
  335. return(0);
  336. }
  337. azero = DD_ZERO(dd);
  338. bzero = Cudd_Not(DD_ONE(dd));
  339. if (f == azero || f == bzero){
  340. (void) fprintf(dd->out,": is the zero DD\n");
  341. (void) fflush(dd->out);
  342. return(1);
  343. }
  344. nodes = Cudd_DagSize(f);
  345. if (nodes == CUDD_OUT_OF_MEM) retval = 0;
  346. leaves = Cudd_CountLeaves(f);
  347. if (leaves == CUDD_OUT_OF_MEM) retval = 0;
  348. (void) fprintf(dd->out,": %d nodes %d leaves ", nodes, leaves);
  349. count = Cudd_ApaCountMinterm(dd, f, n, &digits);
  350. if (count == NULL) {
  351. retval = 0;
  352. } else if (mode) {
  353. if (!Cudd_ApaPrintExponential(dd->out, digits, count, 6))
  354. retval = 0;
  355. } else {
  356. if (!Cudd_ApaPrintDecimal(dd->out, digits, count))
  357. retval = 0;
  358. }
  359. FREE(count);
  360. (void) fprintf(dd->out, " minterms\n");
  361. (void) fflush(dd->out);
  362. return(retval);
  363. } /* end of Cudd_PrintSummary */
  364. /**
  365. @brief Counts the number of nodes in a %DD.
  366. @return the number of nodes in the graph rooted at node.
  367. @sideeffect None
  368. @see Cudd_SharingSize Cudd_PrintDebug
  369. */
  370. int
  371. Cudd_DagSize(
  372. DdNode * node)
  373. {
  374. int i;
  375. i = ddDagInt(Cudd_Regular(node));
  376. ddClearFlag(Cudd_Regular(node));
  377. return(i);
  378. } /* end of Cudd_DagSize */
  379. /**
  380. @brief Estimates the number of nodes in a cofactor of a %DD.
  381. @details This function uses a refinement of the algorithm of Cabodi
  382. et al. (ICCAD96). The refinement allows the procedure to account
  383. for part of the recombination that may occur in the part of the
  384. cofactor above the cofactoring variable. This procedure does not
  385. create any new node. It does keep a small table of results;
  386. therefore it may run out of memory. If this is a concern, one
  387. should use Cudd_EstimateCofactorSimple, which is faster, does not
  388. allocate any memory, but is less accurate.
  389. @return an estimate of the number of nodes in a cofactor of the
  390. graph rooted at node with respect to the variable whose index is i.
  391. In case of failure, returns CUDD_OUT_OF_MEM.
  392. @sideeffect None
  393. @see Cudd_DagSize Cudd_EstimateCofactorSimple
  394. */
  395. int
  396. Cudd_EstimateCofactor(
  397. DdManager *dd /**< manager */,
  398. DdNode * f /**< function */,
  399. int i /**< index of variable */,
  400. int phase /**< 1: positive; 0: negative */
  401. )
  402. {
  403. int val;
  404. DdNode *ptr;
  405. st_table *table;
  406. table = st_init_table(st_ptrcmp,st_ptrhash);
  407. if (table == NULL) {
  408. dd->errorCode = CUDD_MEMORY_OUT;
  409. return(CUDD_OUT_OF_MEM);
  410. }
  411. val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr);
  412. ddClearFlag(Cudd_Regular(f));
  413. st_free_table(table);
  414. if (val == CUDD_OUT_OF_MEM)
  415. dd->errorCode = CUDD_MEMORY_OUT;
  416. return(val);
  417. } /* end of Cudd_EstimateCofactor */
  418. /**
  419. @brief Estimates the number of nodes in a cofactor of a %DD.
  420. @details Returns an estimate of the number of nodes in the positive
  421. cofactor of the graph rooted at node with respect to the variable
  422. whose index is i. This procedure implements with minor changes the
  423. algorithm of Cabodi et al. (ICCAD96). It does not allocate any
  424. memory, it does not change the state of the manager, and it is
  425. fast. However, it has been observed to overestimate the size of the
  426. cofactor by as much as a factor of 2.
  427. @sideeffect None
  428. @see Cudd_DagSize
  429. */
  430. int
  431. Cudd_EstimateCofactorSimple(
  432. DdNode * node,
  433. int i)
  434. {
  435. int val;
  436. val = cuddEstimateCofactorSimple(Cudd_Regular(node),i);
  437. ddClearFlag(Cudd_Regular(node));
  438. return(val);
  439. } /* end of Cudd_EstimateCofactorSimple */
  440. /**
  441. @brief Counts the number of nodes in an array of DDs.
  442. @details Shared nodes are counted only once.
  443. @return the total number of nodes.
  444. @sideeffect None
  445. @see Cudd_DagSize
  446. */
  447. int
  448. Cudd_SharingSize(
  449. DdNode ** nodeArray,
  450. int n)
  451. {
  452. int i,j;
  453. i = 0;
  454. for (j = 0; j < n; j++) {
  455. i += ddDagInt(Cudd_Regular(nodeArray[j]));
  456. }
  457. for (j = 0; j < n; j++) {
  458. ddClearFlag(Cudd_Regular(nodeArray[j]));
  459. }
  460. return(i);
  461. } /* end of Cudd_SharingSize */
  462. /**
  463. @brief Counts the minterms of an %ADD or %BDD.
  464. @details The function is assumed to depend on `nvars` variables. The
  465. minterm count is represented as a double; hence overflow is
  466. possible. For functions with many variables (more than 1023 if
  467. floating point conforms to IEEE 754), one should consider
  468. Cudd_ApaCountMinterm() or Cudd_EpdCountMinterm().
  469. @return the number of minterms of the function rooted at node if
  470. successful; +infinity if the number of minterms is known to be larger
  471. than the maximum value representable as a double; `(double) CUDD_OUT_OF_MEM`
  472. otherwise.
  473. @sideeffect None
  474. @see Cudd_ApaCountMinterm Cudd_EpdCountMinterm Cudd_LdblCountMinterm
  475. Cudd_PrintDebug Cudd_CountPath
  476. */
  477. //double
  478. //Cudd_CountMinterm(
  479. // DdManager * manager,
  480. // DdNode * node,
  481. // int nvars)
  482. //{
  483. // double max;
  484. // DdHashTable *table;
  485. // double res;
  486. // CUDD_VALUE_TYPE epsilon;
  487. //
  488. // /* Scale the maximum number of minterm. This is done in an attempt
  489. // * to deal with functions that depend on more than 1023, but less
  490. // * than 2044 variables and don't have too many minterms.
  491. // */
  492. // printf("vars: %i, min_exp: %.400f, %i\n", nvars, DBL_MIN_EXP, DBL_MIN_EXP);
  493. // printf("1: %f, 2: %i \n", (double)(nvars + DBL_MIN_EXP), (nvars + DBL_MIN_EXP));
  494. // max = pow(2.0,(double)(nvars + DBL_MIN_EXP));
  495. // printf("max: %f, DD_PLUS_INF_VAL: %.50f\n", max, DD_PLUS_INF_VAL);
  496. // if (max >= DD_PLUS_INF_VAL) {
  497. // return((double)CUDD_OUT_OF_MEM);
  498. // }
  499. // table = cuddHashTableInit(manager,1,2);
  500. // if (table == NULL) {
  501. // return((double)CUDD_OUT_OF_MEM);
  502. // }
  503. // /* Temporarily set epsilon to 0 to avoid rounding errors. */
  504. // epsilon = Cudd_ReadEpsilon(manager);
  505. // Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0);
  506. // res = ddCountMintermAux(manager,node,max,table);
  507. // cuddHashTableQuit(table);
  508. // Cudd_SetEpsilon(manager,epsilon);
  509. // if (res == (double)CUDD_OUT_OF_MEM) {
  510. // return((double)CUDD_OUT_OF_MEM);
  511. // } else if (res >= pow(2.0,(double)(DBL_MAX_EXP + DBL_MIN_EXP))) {
  512. // /* Minterm count is too large to be scaled back. */
  513. // return(DD_PLUS_INF_VAL);
  514. // } else {
  515. // printf("in third case: %.400f\n", res);
  516. // /* Undo the scaling. */
  517. // res *= pow(2.0,(double)-DBL_MIN_EXP);
  518. // printf("after rescaling: %f\n", res);
  519. // return(res);
  520. // }
  521. //
  522. //} /* end of Cudd_CountMinterm */
  523. /**Function********************************************************************
  524. Synopsis [Counts the number of minterms of a DD.]
  525. Description [Counts the number of minterms of a DD. The function is
  526. assumed to depend on nvars variables. The minterm count is
  527. represented as a double, to allow for a larger number of variables.
  528. Returns the number of minterms of the function rooted at node if
  529. successful; (double) CUDD_OUT_OF_MEM otherwise.]
  530. SideEffects [None]
  531. SeeAlso [Cudd_PrintDebug Cudd_CountPath]
  532. ******************************************************************************/
  533. double
  534. Cudd_CountMinterm(
  535. DdManager * manager,
  536. DdNode * node,
  537. int nvars)
  538. {
  539. double max;
  540. DdHashTable *table;
  541. double res;
  542. CUDD_VALUE_TYPE epsilon;
  543. max = pow(2.0,(double)nvars);
  544. table = cuddHashTableInit(manager,1,2);
  545. if (table == NULL) {
  546. return((double)CUDD_OUT_OF_MEM);
  547. }
  548. epsilon = Cudd_ReadEpsilon(manager);
  549. Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0);
  550. res = ddCountMintermAux(manager,node,max,table);
  551. cuddHashTableQuit(table);
  552. Cudd_SetEpsilon(manager,epsilon);
  553. return(res);
  554. } /* end of Cudd_CountMinterm */
  555. /**
  556. @brief Counts the paths of a %DD.
  557. @details Paths to all terminal nodes are counted. The path count is
  558. represented as a double; hence overflow is possible.
  559. @return the number of paths of the function rooted at node if
  560. successful; `(double) CUDD_OUT_OF_MEM` otherwise.
  561. @sideeffect None
  562. @see Cudd_CountMinterm
  563. */
  564. double
  565. Cudd_CountPath(
  566. DdNode * node)
  567. {
  568. st_table *table;
  569. double i;
  570. table = st_init_table(st_ptrcmp,st_ptrhash);
  571. if (table == NULL) {
  572. return((double)CUDD_OUT_OF_MEM);
  573. }
  574. i = ddCountPathAux(Cudd_Regular(node),table);
  575. st_foreach(table, cuddStCountfree, NULL);
  576. st_free_table(table);
  577. return(i);
  578. } /* end of Cudd_CountPath */
  579. /**
  580. @brief Counts the minterms of an %ADD or %BDD with extended range.
  581. @details The function is assumed to depend on `nvars` variables. The
  582. minterm count is represented as an `EpDouble`, to allow for any
  583. number of variables.
  584. @return 0 if successful; `CUDD_OUT_OF_MEM` otherwise.
  585. @sideeffect None
  586. @see Cudd_CountMinterm Cudd_LdblCountMinterm Cudd_ApaCountMinterm
  587. Cudd_PrintDebug Cudd_CountPath
  588. */
  589. int
  590. Cudd_EpdCountMinterm(
  591. DdManager const * manager,
  592. DdNode * node,
  593. int nvars,
  594. EpDouble * epd)
  595. {
  596. EpDouble max, tmp;
  597. st_table *table;
  598. int status;
  599. EpdPow2(nvars, &max);
  600. table = st_init_table(st_ptrcmp, st_ptrhash);
  601. if (table == NULL) {
  602. EpdMakeZero(epd, 0);
  603. return(CUDD_OUT_OF_MEM);
  604. }
  605. status = ddEpdCountMintermAux(manager,Cudd_Regular(node),&max,epd,table);
  606. st_foreach(table, ddEpdFree, NULL);
  607. st_free_table(table);
  608. if (status == CUDD_OUT_OF_MEM) {
  609. EpdMakeZero(epd, 0);
  610. return(CUDD_OUT_OF_MEM);
  611. }
  612. if (Cudd_IsComplement(node)) {
  613. EpdSubtract3(&max, epd, &tmp);
  614. EpdCopy(&tmp, epd);
  615. }
  616. return(0);
  617. } /* end of Cudd_EpdCountMinterm */
  618. /**
  619. @brief Returns the number of minterms of aa %ADD or %BDD as a long double.
  620. @details On systems where double and long double are the same type,
  621. Cudd_CountMinterm() is preferable. On systems where long double values
  622. have 15-bit exponents, this function avoids overflow for up to 16383
  623. variables. It applies scaling to try to avoid overflow when the number of
  624. variables is larger than 16383, but smaller than 32764.
  625. @return The nimterm count if successful; +infinity if the number is known to
  626. be too large for representation as a long double;
  627. `(long double)CUDD_OUT_OF_MEM` otherwise.
  628. @see Cudd_CountMinterm Cudd_EpdCountMinterm Cudd_ApaCountMinterm
  629. */
  630. long double
  631. Cudd_LdblCountMinterm(
  632. DdManager const *manager,
  633. DdNode *node,
  634. int nvars)
  635. {
  636. long double max, count;
  637. st_table *table;
  638. max = powl(2.0L, (long double) (nvars+LDBL_MIN_EXP));
  639. if (max == HUGE_VALL) {
  640. return((long double)CUDD_OUT_OF_MEM);
  641. }
  642. table = st_init_table(st_ptrcmp, st_ptrhash);
  643. if (table == NULL) {
  644. return((long double)CUDD_OUT_OF_MEM);
  645. }
  646. count = ddLdblCountMintermAux(manager, Cudd_Regular(node), max, table);
  647. st_foreach(table, ddLdblFree, NULL);
  648. st_free_table(table);
  649. if (count == (long double)CUDD_OUT_OF_MEM) {
  650. return((long double)CUDD_OUT_OF_MEM);
  651. }
  652. if (Cudd_IsComplement(node)) {
  653. count = max - count;
  654. }
  655. if (count >= powl(2.0L, (long double)(LDBL_MAX_EXP + LDBL_MIN_EXP))) {
  656. /* Minterm count is too large to be scaled back. */
  657. return(HUGE_VALL);
  658. } else {
  659. /* Undo the scaling. */
  660. count *= powl(2.0L,(long double)-LDBL_MIN_EXP);
  661. return(count);
  662. }
  663. } /* end of Cudd_LdlbCountMinterm */
  664. /**
  665. @brief Prints the number of minterms of an %ADD or %BDD with extended range.
  666. @return 1 if successful; 0 otherwise.
  667. @sideeffect None
  668. @see Cudd_EpdCountMinterm Cudd_ApaPrintMintermExp
  669. */
  670. int
  671. Cudd_EpdPrintMinterm(
  672. DdManager const * dd,
  673. DdNode * node,
  674. int nvars)
  675. {
  676. EpDouble epd;
  677. int ret;
  678. char pstring[128];
  679. ret = Cudd_EpdCountMinterm(dd, node, nvars, &epd);
  680. if (ret !=0) return(0);
  681. EpdGetString(&epd, pstring);
  682. fprintf(dd->out, "%s", pstring);
  683. return(1);
  684. } /* end of Cudd_EpdPrintMinterm */
  685. /**
  686. @brief Counts the paths to a non-zero terminal of a %DD.
  687. @details The path count is represented as a double; hence overflow is
  688. possible.
  689. @return the number of paths of the function rooted at node.
  690. @sideeffect None
  691. @see Cudd_CountMinterm Cudd_CountPath
  692. */
  693. double
  694. Cudd_CountPathsToNonZero(
  695. DdNode * node)
  696. {
  697. st_table *table;
  698. double i;
  699. table = st_init_table(st_ptrcmp,st_ptrhash);
  700. if (table == NULL) {
  701. return((double)CUDD_OUT_OF_MEM);
  702. }
  703. i = ddCountPathsToNonZero(node,table);
  704. st_foreach(table, cuddStCountfree, NULL);
  705. st_free_table(table);
  706. return(i);
  707. } /* end of Cudd_CountPathsToNonZero */
  708. /**
  709. @brief Finds the variables on which a %DD depends.
  710. @return the number of variables if successful; CUDD_OUT_OF_MEM
  711. otherwise.
  712. @sideeffect The indices of the support variables are returned as
  713. side effects. If the function is constant, no array is allocated.
  714. @see Cudd_Support Cudd_SupportIndex Cudd_VectorSupportIndices
  715. */
  716. int
  717. Cudd_SupportIndices(
  718. DdManager * dd /**< manager */,
  719. DdNode * f /**< %DD whose support is sought */,
  720. int **indices /**< array containing (on return) the indices */)
  721. {
  722. int SP = 0;
  723. ddFindSupport(dd, Cudd_Regular(f), &SP);
  724. ddClearFlag(Cudd_Regular(f));
  725. ddClearVars(dd, SP);
  726. if (SP > 0) {
  727. int i;
  728. *indices = ALLOC(int, SP);
  729. if (*indices == NULL) {
  730. dd->errorCode = CUDD_MEMORY_OUT;
  731. return(CUDD_OUT_OF_MEM);
  732. }
  733. for (i = 0; i < SP; i++)
  734. (*indices)[i] = (int) (ptrint) dd->stack[i];
  735. util_qsort(*indices, SP, sizeof(int), indexCompare);
  736. } else {
  737. *indices = NULL;
  738. }
  739. return(SP);
  740. } /* end of Cudd_SupportIndices */
  741. /**
  742. @brief Finds the variables on which a %DD depends.
  743. @return a %BDD consisting of the product of the variables if
  744. successful; NULL otherwise.
  745. @sideeffect None
  746. @see Cudd_VectorSupport Cudd_ClassifySupport
  747. */
  748. DdNode *
  749. Cudd_Support(
  750. DdManager * dd /**< manager */,
  751. DdNode * f /**< %DD whose support is sought */)
  752. {
  753. int *support;
  754. DdNode *res;
  755. int j;
  756. int size = Cudd_SupportIndices(dd, f, &support);
  757. if (size == CUDD_OUT_OF_MEM)
  758. return(NULL);
  759. /* Transform support from array of indices to cube. */
  760. res = DD_ONE(dd);
  761. cuddRef(res);
  762. for (j = size - 1; j >= 0; j--) { /* for each index bottom-up (almost) */
  763. int index = support[j];
  764. DdNode *var = dd->vars[index];
  765. DdNode *tmp = Cudd_bddAnd(dd,res,var);
  766. if (tmp == NULL) {
  767. Cudd_RecursiveDeref(dd,res);
  768. FREE(support);
  769. return(NULL);
  770. }
  771. cuddRef(tmp);
  772. Cudd_RecursiveDeref(dd,res);
  773. res = tmp;
  774. }
  775. FREE(support);
  776. cuddDeref(res);
  777. return(res);
  778. } /* end of Cudd_Support */
  779. /**
  780. @brief Finds the variables on which a %DD depends.
  781. @return an index array of the variables if successful; NULL
  782. otherwise. The size of the array equals the number of variables in
  783. the manager. Each entry of the array is 1 if the corresponding
  784. variable is in the support of the %DD and 0 otherwise.
  785. @sideeffect None
  786. @see Cudd_Support Cudd_SupportIndices Cudd_ClassifySupport
  787. */
  788. int *
  789. Cudd_SupportIndex(
  790. DdManager * dd /**< manager */,
  791. DdNode * f /**< %DD whose support is sought */)
  792. {
  793. int *support;
  794. int i;
  795. int size;
  796. /* Allocate and initialize support array for ddSupportStep. */
  797. size = ddMax(dd->size, dd->sizeZ);
  798. support = ALLOC(int,size);
  799. if (support == NULL) {
  800. dd->errorCode = CUDD_MEMORY_OUT;
  801. return(NULL);
  802. }
  803. for (i = 0; i < size; i++) {
  804. support[i] = 0;
  805. }
  806. /* Compute support and clean up markers. */
  807. ddSupportStep(Cudd_Regular(f),support);
  808. ddClearFlag(Cudd_Regular(f));
  809. return(support);
  810. } /* end of Cudd_SupportIndex */
  811. /**
  812. @brief Counts the variables on which a %DD depends.
  813. @return the variables on which a %DD depends.
  814. @sideeffect None
  815. @see Cudd_Support Cudd_SupportIndices
  816. */
  817. int
  818. Cudd_SupportSize(
  819. DdManager * dd /**< manager */,
  820. DdNode * f /**< %DD whose support size is sought */)
  821. {
  822. int SP = 0;
  823. ddFindSupport(dd, Cudd_Regular(f), &SP);
  824. ddClearFlag(Cudd_Regular(f));
  825. ddClearVars(dd, SP);
  826. return(SP);
  827. } /* end of Cudd_SupportSize */
  828. /**
  829. @brief Finds the variables on which a set of DDs depends.
  830. @details The set must contain either BDDs and ADDs, or ZDDs.
  831. @return the number of variables if successful; CUDD_OUT_OF_MEM
  832. otherwise.
  833. @sideeffect The indices of the support variables are returned as
  834. side effects. If the function is constant, no array is allocated.
  835. @see Cudd_Support Cudd_SupportIndex Cudd_VectorSupportIndices
  836. */
  837. int
  838. Cudd_VectorSupportIndices(
  839. DdManager * dd /**< manager */,
  840. DdNode ** F /**< %DD whose support is sought */,
  841. int n /**< size of the array */,
  842. int **indices /**< array containing (on return) the indices */)
  843. {
  844. int i;
  845. int SP = 0;
  846. /* Compute support and clean up markers. */
  847. for (i = 0; i < n; i++) {
  848. ddFindSupport(dd, Cudd_Regular(F[i]), &SP);
  849. }
  850. for (i = 0; i < n; i++) {
  851. ddClearFlag(Cudd_Regular(F[i]));
  852. }
  853. ddClearVars(dd, SP);
  854. if (SP > 0) {
  855. *indices = ALLOC(int, SP);
  856. if (*indices == NULL) {
  857. dd->errorCode = CUDD_MEMORY_OUT;
  858. return(CUDD_OUT_OF_MEM);
  859. }
  860. for (i = 0; i < SP; i++)
  861. (*indices)[i] = (int) (ptrint) dd->stack[i];
  862. util_qsort(*indices, SP, sizeof(int), indexCompare);
  863. } else {
  864. *indices = NULL;
  865. }
  866. return(SP);
  867. } /* end of Cudd_VectorSupportIndices */
  868. /**
  869. @brief Finds the variables on which a set of DDs depends.
  870. @details The set must contain either BDDs and ADDs, or ZDDs.
  871. @return a %BDD consisting of the product of the variables if
  872. successful; NULL otherwise.
  873. @sideeffect None
  874. @see Cudd_Support Cudd_ClassifySupport
  875. */
  876. DdNode *
  877. Cudd_VectorSupport(
  878. DdManager * dd /**< manager */,
  879. DdNode ** F /**< array of DDs whose support is sought */,
  880. int n /**< size of the array */)
  881. {
  882. int *support;
  883. DdNode *res;
  884. int j;
  885. int size = Cudd_VectorSupportIndices(dd, F, n, &support);
  886. if (size == CUDD_OUT_OF_MEM)
  887. return(NULL);
  888. /* Transform support from array of indices to cube. */
  889. res = DD_ONE(dd);
  890. cuddRef(res);
  891. for (j = size - 1; j >= 0; j--) { /* for each index bottom-up (almost) */
  892. int index = support[j];
  893. DdNode *var = dd->vars[index];
  894. DdNode *tmp = Cudd_bddAnd(dd,res,var);
  895. if (tmp == NULL) {
  896. Cudd_RecursiveDeref(dd,res);
  897. FREE(support);
  898. return(NULL);
  899. }
  900. cuddRef(tmp);
  901. Cudd_RecursiveDeref(dd,res);
  902. res = tmp;
  903. }
  904. FREE(support);
  905. cuddDeref(res);
  906. return(res);
  907. } /* end of Cudd_VectorSupport */
  908. /**
  909. @brief Finds the variables on which a set of DDs depends.
  910. @details The set must contain either BDDs and ADDs, or ZDDs.
  911. @return an index array of the variables if successful; NULL
  912. otherwise.
  913. @sideeffect None
  914. @see Cudd_SupportIndex Cudd_VectorSupport Cudd_VectorSupportIndices
  915. */
  916. int *
  917. Cudd_VectorSupportIndex(
  918. DdManager * dd /**< manager */,
  919. DdNode ** F /**< array of DDs whose support is sought */,
  920. int n /**< size of the array */)
  921. {
  922. int *support;
  923. int i;
  924. int size;
  925. /* Allocate and initialize support array for ddSupportStep. */
  926. size = ddMax(dd->size, dd->sizeZ);
  927. support = ALLOC(int,size);
  928. if (support == NULL) {
  929. dd->errorCode = CUDD_MEMORY_OUT;
  930. return(NULL);
  931. }
  932. for (i = 0; i < size; i++) {
  933. support[i] = 0;
  934. }
  935. /* Compute support and clean up markers. */
  936. for (i = 0; i < n; i++) {
  937. ddSupportStep(Cudd_Regular(F[i]),support);
  938. }
  939. for (i = 0; i < n; i++) {
  940. ddClearFlag(Cudd_Regular(F[i]));
  941. }
  942. return(support);
  943. } /* end of Cudd_VectorSupportIndex */
  944. /**
  945. @brief Counts the variables on which a set of DDs depends.
  946. @details The set must contain either BDDs and ADDs, or ZDDs.
  947. @return the number of variables on which a set of DDs depends.
  948. @sideeffect None
  949. @see Cudd_VectorSupport Cudd_SupportSize
  950. */
  951. int
  952. Cudd_VectorSupportSize(
  953. DdManager * dd /**< manager */,
  954. DdNode ** F /**< array of DDs whose support is sought */,
  955. int n /**< size of the array */)
  956. {
  957. int i;
  958. int SP = 0;
  959. /* Compute support and clean up markers. */
  960. for (i = 0; i < n; i++) {
  961. ddFindSupport(dd, Cudd_Regular(F[i]), &SP);
  962. }
  963. for (i = 0; i < n; i++) {
  964. ddClearFlag(Cudd_Regular(F[i]));
  965. }
  966. ddClearVars(dd, SP);
  967. return(SP);
  968. } /* end of Cudd_VectorSupportSize */
  969. /**
  970. @brief Classifies the variables in the support of two DDs.
  971. @details Classifies the variables in the support of two DDs
  972. <code>f</code> and <code>g</code>, depending on whether they appear
  973. in both DDs, only in <code>f</code>, or only in <code>g</code>.
  974. @return 1 if successful; 0 otherwise.
  975. @sideeffect The cubes of the three classes of variables are
  976. returned as side effects.
  977. @see Cudd_Support Cudd_VectorSupport
  978. */
  979. int
  980. Cudd_ClassifySupport(
  981. DdManager * dd /**< manager */,
  982. DdNode * f /**< first %DD */,
  983. DdNode * g /**< second %DD */,
  984. DdNode ** common /**< cube of shared variables */,
  985. DdNode ** onlyF /**< cube of variables only in f */,
  986. DdNode ** onlyG /**< cube of variables only in g */)
  987. {
  988. int *supportF, *supportG;
  989. int fi, gi;
  990. int sizeF, sizeG;
  991. sizeF = Cudd_SupportIndices(dd, f, &supportF);
  992. if (sizeF == CUDD_OUT_OF_MEM)
  993. return(0);
  994. sizeG = Cudd_SupportIndices(dd, g, &supportG);
  995. if (sizeG == CUDD_OUT_OF_MEM) {
  996. FREE(supportF);
  997. return(0);
  998. }
  999. /* Classify variables and create cubes. This part of the procedure
  1000. ** relies on the sorting of the indices in the two support arrays.
  1001. */
  1002. *common = *onlyF = *onlyG = DD_ONE(dd);
  1003. cuddRef(*common); cuddRef(*onlyF); cuddRef(*onlyG);
  1004. fi = sizeF - 1;
  1005. gi = sizeG - 1;
  1006. while (fi >= 0 || gi >= 0) {
  1007. int indexF = fi >= 0 ? supportF[fi] : -1;
  1008. int indexG = gi >= 0 ? supportG[gi] : -1;
  1009. int index = ddMax(indexF, indexG);
  1010. DdNode *var = dd->vars[index];
  1011. #ifdef DD_DEBUG
  1012. assert(index >= 0);
  1013. #endif
  1014. if (indexF == indexG) {
  1015. DdNode *tmp = Cudd_bddAnd(dd,*common,var);
  1016. if (tmp == NULL) {
  1017. Cudd_RecursiveDeref(dd,*common);
  1018. Cudd_RecursiveDeref(dd,*onlyF);
  1019. Cudd_RecursiveDeref(dd,*onlyG);
  1020. FREE(supportF); FREE(supportG);
  1021. return(0);
  1022. }
  1023. cuddRef(tmp);
  1024. Cudd_RecursiveDeref(dd,*common);
  1025. *common = tmp;
  1026. fi--;
  1027. gi--;
  1028. } else if (index == indexF) {
  1029. DdNode *tmp = Cudd_bddAnd(dd,*onlyF,var);
  1030. if (tmp == NULL) {
  1031. Cudd_RecursiveDeref(dd,*common);
  1032. Cudd_RecursiveDeref(dd,*onlyF);
  1033. Cudd_RecursiveDeref(dd,*onlyG);
  1034. FREE(supportF); FREE(supportG);
  1035. return(0);
  1036. }
  1037. cuddRef(tmp);
  1038. Cudd_RecursiveDeref(dd,*onlyF);
  1039. *onlyF = tmp;
  1040. fi--;
  1041. } else { /* index == indexG */
  1042. DdNode *tmp = Cudd_bddAnd(dd,*onlyG,var);
  1043. if (tmp == NULL) {
  1044. Cudd_RecursiveDeref(dd,*common);
  1045. Cudd_RecursiveDeref(dd,*onlyF);
  1046. Cudd_RecursiveDeref(dd,*onlyG);
  1047. FREE(supportF); FREE(supportG);
  1048. return(0);
  1049. }
  1050. cuddRef(tmp);
  1051. Cudd_RecursiveDeref(dd,*onlyG);
  1052. *onlyG = tmp;
  1053. gi--;
  1054. }
  1055. }
  1056. FREE(supportF); FREE(supportG);
  1057. cuddDeref(*common); cuddDeref(*onlyF); cuddDeref(*onlyG);
  1058. return(1);
  1059. } /* end of Cudd_ClassifySupport */
  1060. /**
  1061. @brief Counts the number of leaves in a %DD.
  1062. @return the number of leaves in the %DD rooted at node if successful;
  1063. CUDD_OUT_OF_MEM otherwise.
  1064. @sideeffect None
  1065. @see Cudd_PrintDebug
  1066. */
  1067. int
  1068. Cudd_CountLeaves(
  1069. DdNode * node)
  1070. {
  1071. int i;
  1072. i = ddLeavesInt(Cudd_Regular(node));
  1073. ddClearFlag(Cudd_Regular(node));
  1074. return(i);
  1075. } /* end of Cudd_CountLeaves */
  1076. /**
  1077. @brief Picks one on-set cube randomly from the given %DD.
  1078. @details The cube is written into an array of characters. The array
  1079. must have at least as many entries as there are variables.
  1080. @return 1 if successful; 0 otherwise.
  1081. @sideeffect None
  1082. @see Cudd_bddPickOneMinterm
  1083. */
  1084. int
  1085. Cudd_bddPickOneCube(
  1086. DdManager * ddm,
  1087. DdNode * node,
  1088. char * string)
  1089. {
  1090. DdNode *N, *T, *E;
  1091. DdNode *one, *bzero;
  1092. char dir;
  1093. int i;
  1094. if (string == NULL || node == NULL) return(0);
  1095. /* The constant 0 function has no on-set cubes. */
  1096. one = DD_ONE(ddm);
  1097. bzero = Cudd_Not(one);
  1098. if (node == bzero) {
  1099. ddm->errorCode = CUDD_INVALID_ARG;
  1100. return(0);
  1101. }
  1102. for (i = 0; i < ddm->size; i++) string[i] = 2;
  1103. for (;;) {
  1104. if (node == one) break;
  1105. N = Cudd_Regular(node);
  1106. T = cuddT(N); E = cuddE(N);
  1107. if (Cudd_IsComplement(node)) {
  1108. T = Cudd_Not(T); E = Cudd_Not(E);
  1109. }
  1110. if (T == bzero) {
  1111. string[N->index] = 0;
  1112. node = E;
  1113. } else if (E == bzero) {
  1114. string[N->index] = 1;
  1115. node = T;
  1116. } else {
  1117. dir = (char) ((Cudd_Random(ddm) & 0x2000) >> 13);
  1118. string[N->index] = dir;
  1119. node = dir ? T : E;
  1120. }
  1121. }
  1122. return(1);
  1123. } /* end of Cudd_bddPickOneCube */
  1124. /**
  1125. @brief Picks one on-set minterm randomly from the given %DD.
  1126. @details The minterm is in terms of <code>vars</code>. The array
  1127. <code>vars</code> should contain at least all variables in the
  1128. support of <code>f</code>; if this condition is not met the minterm
  1129. built by this procedure may not be contained in <code>f</code>.
  1130. @return a pointer to the %BDD for the minterm if successful; NULL otherwise.
  1131. There are three reasons why the procedure may fail:
  1132. <ul>
  1133. <li> It may run out of memory;
  1134. <li> the function <code>f</code> may be the constant 0;
  1135. <li> the minterm may not be contained in <code>f</code>.
  1136. </ul>
  1137. @sideeffect None
  1138. @see Cudd_bddPickOneCube
  1139. */
  1140. DdNode *
  1141. Cudd_bddPickOneMinterm(
  1142. DdManager * dd /**< manager */,
  1143. DdNode * f /**< function from which to pick one minterm */,
  1144. DdNode ** vars /**< array of variables */,
  1145. int n /**< size of <code>vars</code> */)
  1146. {
  1147. char *string;
  1148. int i, size;
  1149. int *indices;
  1150. int result;
  1151. DdNode *old, *neW;
  1152. size = dd->size;
  1153. string = ALLOC(char, size);
  1154. if (string == NULL) {
  1155. dd->errorCode = CUDD_MEMORY_OUT;
  1156. return(NULL);
  1157. }
  1158. indices = ALLOC(int,n);
  1159. if (indices == NULL) {
  1160. dd->errorCode = CUDD_MEMORY_OUT;
  1161. FREE(string);
  1162. return(NULL);
  1163. }
  1164. for (i = 0; i < n; i++) {
  1165. indices[i] = vars[i]->index;
  1166. }
  1167. result = Cudd_bddPickOneCube(dd,f,string);
  1168. if (result == 0) {
  1169. FREE(string);
  1170. FREE(indices);
  1171. return(NULL);
  1172. }
  1173. /* Randomize choice for don't cares. */
  1174. for (i = 0; i < n; i++) {
  1175. if (string[indices[i]] == 2)
  1176. string[indices[i]] = (char) ((Cudd_Random(dd) & 0x20) >> 5);
  1177. }
  1178. /* Build result BDD. */
  1179. old = Cudd_ReadOne(dd);
  1180. cuddRef(old);
  1181. for (i = n-1; i >= 0; i--) {
  1182. neW = Cudd_bddAnd(dd,old,Cudd_NotCond(vars[i],string[indices[i]]==0));
  1183. if (neW == NULL) {
  1184. FREE(string);
  1185. FREE(indices);
  1186. Cudd_RecursiveDeref(dd,old);
  1187. return(NULL);
  1188. }
  1189. cuddRef(neW);
  1190. Cudd_RecursiveDeref(dd,old);
  1191. old = neW;
  1192. }
  1193. #ifdef DD_DEBUG
  1194. /* Test. */
  1195. if (Cudd_bddLeq(dd,old,f)) {
  1196. cuddDeref(old);
  1197. } else {
  1198. Cudd_RecursiveDeref(dd,old);
  1199. old = NULL;
  1200. }
  1201. #else
  1202. cuddDeref(old);
  1203. #endif
  1204. FREE(string);
  1205. FREE(indices);
  1206. return(old);
  1207. } /* end of Cudd_bddPickOneMinterm */
  1208. /**
  1209. @brief Picks k on-set minterms evenly distributed from given %DD.
  1210. @details The minterms are in terms of <code>vars</code>. The array
  1211. <code>vars</code> should contain at least all variables in the
  1212. support of <code>f</code>; if this condition is not met the minterms
  1213. built by this procedure may not be contained in <code>f</code>.
  1214. @return an array of BDDs for the minterms if successful; NULL otherwise.
  1215. There are three reasons why the procedure may fail:
  1216. <ul>
  1217. <li> It may run out of memory;
  1218. <li> the function <code>f</code> may be the constant 0;
  1219. <li> the minterms may not be contained in <code>f</code>.
  1220. </ul>
  1221. @sideeffect None
  1222. @see Cudd_bddPickOneMinterm Cudd_bddPickOneCube
  1223. */
  1224. DdNode **
  1225. Cudd_bddPickArbitraryMinterms(
  1226. DdManager * dd /**< manager */,
  1227. DdNode * f /**< function from which to pick k minterms */,
  1228. DdNode ** vars /**< array of variables */,
  1229. int n /**< size of <code>vars</code> */,
  1230. int k /**< number of minterms to find */)
  1231. {
  1232. char **string;
  1233. int i, j, l, size;
  1234. int *indices;
  1235. int result;
  1236. DdNode **old, *neW;
  1237. double minterms;
  1238. char *saveString;
  1239. int saveFlag, savePoint = 0, isSame;
  1240. minterms = Cudd_CountMinterm(dd,f,n);
  1241. if ((double)k > minterms) {
  1242. return(NULL);
  1243. }
  1244. size = dd->size;
  1245. string = ALLOC(char *, k);
  1246. if (string == NULL) {
  1247. dd->errorCode = CUDD_MEMORY_OUT;
  1248. return(NULL);
  1249. }
  1250. for (i = 0; i < k; i++) {
  1251. string[i] = ALLOC(char, size + 1);
  1252. if (string[i] == NULL) {
  1253. for (j = 0; j < i; j++)
  1254. FREE(string[i]);
  1255. FREE(string);
  1256. dd->errorCode = CUDD_MEMORY_OUT;
  1257. return(NULL);
  1258. }
  1259. for (j = 0; j < size; j++) string[i][j] = '2';
  1260. string[i][size] = '\0';
  1261. }
  1262. indices = ALLOC(int,n);
  1263. if (indices == NULL) {
  1264. dd->errorCode = CUDD_MEMORY_OUT;
  1265. for (i = 0; i < k; i++)
  1266. FREE(string[i]);
  1267. FREE(string);
  1268. return(NULL);
  1269. }
  1270. for (i = 0; i < n; i++) {
  1271. indices[i] = vars[i]->index;
  1272. }
  1273. result = ddPickArbitraryMinterms(dd,f,n,k,string);
  1274. if (result == 0) {
  1275. for (i = 0; i < k; i++)
  1276. FREE(string[i]);
  1277. FREE(string);
  1278. FREE(indices);
  1279. return(NULL);
  1280. }
  1281. old = ALLOC(DdNode *, k);
  1282. if (old == NULL) {
  1283. dd->errorCode = CUDD_MEMORY_OUT;
  1284. for (i = 0; i < k; i++)
  1285. FREE(string[i]);
  1286. FREE(string);
  1287. FREE(indices);
  1288. return(NULL);
  1289. }
  1290. saveString = ALLOC(char, size + 1);
  1291. if (saveString == NULL) {
  1292. dd->errorCode = CUDD_MEMORY_OUT;
  1293. for (i = 0; i < k; i++)
  1294. FREE(string[i]);
  1295. FREE(string);
  1296. FREE(indices);
  1297. FREE(old);
  1298. return(NULL);
  1299. }
  1300. saveFlag = 0;
  1301. /* Build result BDD array. */
  1302. for (i = 0; i < k; i++) {
  1303. isSame = 0;
  1304. if (!saveFlag) {
  1305. for (j = i + 1; j < k; j++) {
  1306. if (strcmp(string[i], string[j]) == 0) {
  1307. savePoint = i;
  1308. strcpy(saveString, string[i]);
  1309. saveFlag = 1;
  1310. break;
  1311. }
  1312. }
  1313. } else {
  1314. if (strcmp(string[i], saveString) == 0) {
  1315. isSame = 1;
  1316. } else {
  1317. saveFlag = 0;
  1318. for (j = i + 1; j < k; j++) {
  1319. if (strcmp(string[i], string[j]) == 0) {
  1320. savePoint = i;
  1321. strcpy(saveString, string[i]);
  1322. saveFlag = 1;
  1323. break;
  1324. }
  1325. }
  1326. }
  1327. }
  1328. /* Randomize choice for don't cares. */
  1329. for (j = 0; j < n; j++) {
  1330. if (string[i][indices[j]] == '2')
  1331. string[i][indices[j]] =
  1332. (char) ((Cudd_Random(dd) & 0x20) ? '1' : '0');
  1333. }
  1334. while (isSame) {
  1335. isSame = 0;
  1336. for (j = savePoint; j < i; j++) {
  1337. if (strcmp(string[i], string[j]) == 0) {
  1338. isSame = 1;
  1339. break;
  1340. }
  1341. }
  1342. if (isSame) {
  1343. strcpy(string[i], saveString);
  1344. /* Randomize choice for don't cares. */
  1345. for (j = 0; j < n; j++) {
  1346. if (string[i][indices[j]] == '2')
  1347. string[i][indices[j]] =
  1348. (char) ((Cudd_Random(dd) & 0x20) ? '1' : '0');
  1349. }
  1350. }
  1351. }
  1352. old[i] = Cudd_ReadOne(dd);
  1353. cuddRef(old[i]);
  1354. for (j = 0; j < n; j++) {
  1355. if (string[i][indices[j]] == '0') {
  1356. neW = Cudd_bddAnd(dd,old[i],Cudd_Not(vars[j]));
  1357. } else {
  1358. neW = Cudd_bddAnd(dd,old[i],vars[j]);
  1359. }
  1360. if (neW == NULL) {
  1361. FREE(saveString);
  1362. for (l = 0; l < k; l++)
  1363. FREE(string[l]);
  1364. FREE(string);
  1365. FREE(indices);
  1366. for (l = 0; l <= i; l++)
  1367. Cudd_RecursiveDeref(dd,old[l]);
  1368. FREE(old);
  1369. return(NULL);
  1370. }
  1371. cuddRef(neW);
  1372. Cudd_RecursiveDeref(dd,old[i]);
  1373. old[i] = neW;
  1374. }
  1375. /* Test. */
  1376. if (!Cudd_bddLeq(dd,old[i],f)) {
  1377. FREE(saveString);
  1378. for (l = 0; l < k; l++)
  1379. FREE(string[l]);
  1380. FREE(string);
  1381. FREE(indices);
  1382. for (l = 0; l <= i; l++)
  1383. Cudd_RecursiveDeref(dd,old[l]);
  1384. FREE(old);
  1385. return(NULL);
  1386. }
  1387. }
  1388. FREE(saveString);
  1389. for (i = 0; i < k; i++) {
  1390. cuddDeref(old[i]);
  1391. FREE(string[i]);
  1392. }
  1393. FREE(string);
  1394. FREE(indices);
  1395. return(old);
  1396. } /* end of Cudd_bddPickArbitraryMinterms */
  1397. /**
  1398. @brief Extracts a subset from a %BDD.
  1399. @details Extracts a subset from a %BDD in the following procedure.
  1400. 1. Compute the weight for each mask variable by counting the number of
  1401. minterms for both positive and negative cofactors of the %BDD with
  1402. respect to each mask variable. (weight = # positive - # negative)
  1403. 2. Find a representative cube of the %BDD by using the weight. From the
  1404. top variable of the %BDD, for each variable, if the weight is greater
  1405. than 0.0, choose THEN branch, othereise ELSE branch, until meeting
  1406. the constant 1.
  1407. 3. Quantify out the variables not in maskVars from the representative
  1408. cube and if a variable in maskVars is don't care, replace the
  1409. variable with a constant(1 or 0) depending on the weight.
  1410. 4. Make a subset of the %BDD by multiplying with the modified cube.
  1411. @sideeffect None
  1412. */
  1413. DdNode *
  1414. Cudd_SubsetWithMaskVars(
  1415. DdManager * dd /**< manager */,
  1416. DdNode * f /**< function from which to pick a cube */,
  1417. DdNode ** vars /**< array of variables */,
  1418. int nvars /**< size of <code>vars</code> */,
  1419. DdNode ** maskVars /**< array of variables */,
  1420. int mvars /**< size of <code>maskVars</code> */)
  1421. {
  1422. double *weight;
  1423. char *string;
  1424. int i, size;
  1425. int *indices, *mask;
  1426. int result;
  1427. DdNode *cube, *newCube, *subset;
  1428. DdNode *cof;
  1429. DdNode *support;
  1430. DdNode *zero;
  1431. support = Cudd_Support(dd,f);
  1432. cuddRef(support);
  1433. Cudd_RecursiveDeref(dd,support);
  1434. size = dd->size;
  1435. weight = ALLOC(double,size);
  1436. if (weight == NULL) {
  1437. dd->errorCode = CUDD_MEMORY_OUT;
  1438. return(NULL);
  1439. }
  1440. for (i = 0; i < size; i++) {
  1441. weight[i] = 0.0;
  1442. }
  1443. for (i = 0; i < mvars; i++) {
  1444. cof = Cudd_Cofactor(dd, f, maskVars[i]);
  1445. cuddRef(cof);
  1446. weight[i] = Cudd_CountMinterm(dd, cof, nvars);
  1447. Cudd_RecursiveDeref(dd,cof);
  1448. cof = Cudd_Cofactor(dd, f, Cudd_Not(maskVars[i]));
  1449. cuddRef(cof);
  1450. weight[i] -= Cudd_CountMinterm(dd, cof, nvars);
  1451. Cudd_RecursiveDeref(dd,cof);
  1452. }
  1453. string = ALLOC(char, size + 1);
  1454. if (string == NULL) {
  1455. dd->errorCode = CUDD_MEMORY_OUT;
  1456. FREE(weight);
  1457. return(NULL);
  1458. }
  1459. mask = ALLOC(int, size);
  1460. if (mask == NULL) {
  1461. dd->errorCode = CUDD_MEMORY_OUT;
  1462. FREE(weight);
  1463. FREE(string);
  1464. return(NULL);
  1465. }
  1466. for (i = 0; i < size; i++) {
  1467. string[i] = '2';
  1468. mask[i] = 0;
  1469. }
  1470. string[size] = '\0';
  1471. indices = ALLOC(int,nvars);
  1472. if (indices == NULL) {
  1473. dd->errorCode = CUDD_MEMORY_OUT;
  1474. FREE(weight);
  1475. FREE(string);
  1476. FREE(mask);
  1477. return(NULL);
  1478. }
  1479. for (i = 0; i < nvars; i++) {
  1480. indices[i] = vars[i]->index;
  1481. }
  1482. result = ddPickRepresentativeCube(dd,f,weight,string);
  1483. if (result == 0) {
  1484. FREE(weight);
  1485. FREE(string);
  1486. FREE(mask);
  1487. FREE(indices);
  1488. return(NULL);
  1489. }
  1490. cube = Cudd_ReadOne(dd);
  1491. cuddRef(cube);
  1492. zero = Cudd_Not(Cudd_ReadOne(dd));
  1493. for (i = 0; i < nvars; i++) {
  1494. if (string[indices[i]] == '0') {
  1495. newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
  1496. } else if (string[indices[i]] == '1') {
  1497. newCube = Cudd_bddIte(dd,cube,vars[i],zero);
  1498. } else
  1499. continue;
  1500. if (newCube == NULL) {
  1501. FREE(weight);
  1502. FREE(string);
  1503. FREE(mask);
  1504. FREE(indices);
  1505. Cudd_RecursiveDeref(dd,cube);
  1506. return(NULL);
  1507. }
  1508. cuddRef(newCube);
  1509. Cudd_RecursiveDeref(dd,cube);
  1510. cube = newCube;
  1511. }
  1512. Cudd_RecursiveDeref(dd,cube);
  1513. for (i = 0; i < mvars; i++) {
  1514. mask[maskVars[i]->index] = 1;
  1515. }
  1516. for (i = 0; i < nvars; i++) {
  1517. if (mask[indices[i]]) {
  1518. if (string[indices[i]] == '2') {
  1519. if (weight[indices[i]] >= 0.0)
  1520. string[indices[i]] = '1';
  1521. else
  1522. string[indices[i]] = '0';
  1523. }
  1524. } else {
  1525. string[indices[i]] = '2';
  1526. }
  1527. }
  1528. cube = Cudd_ReadOne(dd);
  1529. cuddRef(cube);
  1530. zero = Cudd_Not(Cudd_ReadOne(dd));
  1531. /* Build result BDD. */
  1532. for (i = 0; i < nvars; i++) {
  1533. if (string[indices[i]] == '0') {
  1534. newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
  1535. } else if (string[indices[i]] == '1') {
  1536. newCube = Cudd_bddIte(dd,cube,vars[i],zero);
  1537. } else
  1538. continue;
  1539. if (newCube == NULL) {
  1540. FREE(weight);
  1541. FREE(string);
  1542. FREE(mask);
  1543. FREE(indices);
  1544. Cudd_RecursiveDeref(dd,cube);
  1545. return(NULL);
  1546. }
  1547. cuddRef(newCube);
  1548. Cudd_RecursiveDeref(dd,cube);
  1549. cube = newCube;
  1550. }
  1551. subset = Cudd_bddAnd(dd,f,cube);
  1552. cuddRef(subset);
  1553. Cudd_RecursiveDeref(dd,cube);
  1554. /* Test. */
  1555. if (Cudd_bddLeq(dd,subset,f)) {
  1556. cuddDeref(subset);
  1557. } else {
  1558. Cudd_RecursiveDeref(dd,subset);
  1559. subset = NULL;
  1560. }
  1561. FREE(weight);
  1562. FREE(string);
  1563. FREE(mask);
  1564. FREE(indices);
  1565. return(subset);
  1566. } /* end of Cudd_SubsetWithMaskVars */
  1567. /**
  1568. @brief Finds the first cube of a decision diagram.
  1569. @details Defines an iterator on the onset of a decision diagram
  1570. and finds its first cube.<p>
  1571. A cube is represented as an array of literals, which are integers in
  1572. {0, 1, 2}; 0 represents a complemented literal, 1 represents an
  1573. uncomplemented literal, and 2 stands for don't care. The enumeration
  1574. produces a disjoint cover of the function associated with the diagram.
  1575. The size of the array equals the number of variables in the manager at
  1576. the time Cudd_FirstCube is called.<p>
  1577. For each cube, a value is also returned. This value is always 1 for a
  1578. %BDD, while it may be different from 1 for an %ADD.
  1579. For BDDs, the offset is the set of cubes whose value is the logical zero.
  1580. For ADDs, the offset is the set of cubes whose value is the
  1581. background value. The cubes of the offset are not enumerated.
  1582. @return a generator that contains the information necessary to
  1583. continue the enumeration if successful; NULL otherwise.
  1584. @sideeffect The first cube and its value are returned as side effects.
  1585. @see Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty
  1586. Cudd_FirstNode
  1587. */
  1588. DdGen *
  1589. Cudd_FirstCube(
  1590. DdManager * dd,
  1591. DdNode * f,
  1592. int ** cube,
  1593. CUDD_VALUE_TYPE * value)
  1594. {
  1595. DdGen *gen;
  1596. DdNode *top, *treg, *next, *nreg, *prev, *preg;
  1597. int i;
  1598. int nvars;
  1599. /* Sanity Check. */
  1600. if (dd == NULL || f == NULL) return(NULL);
  1601. /* Allocate generator an initialize it. */
  1602. gen = ALLOC(DdGen,1);
  1603. if (gen == NULL) {
  1604. dd->errorCode = CUDD_MEMORY_OUT;
  1605. return(NULL);
  1606. }
  1607. gen->manager = dd;
  1608. gen->type = CUDD_GEN_CUBES;
  1609. gen->status = CUDD_GEN_EMPTY;
  1610. gen->gen.cubes.cube = NULL;
  1611. gen->gen.cubes.value = DD_ZERO_VAL;
  1612. gen->stack.sp = 0;
  1613. gen->stack.stack = NULL;
  1614. gen->node = NULL;
  1615. nvars = dd->size;
  1616. gen->gen.cubes.cube = ALLOC(int,nvars);
  1617. if (gen->gen.cubes.cube == NULL) {
  1618. dd->errorCode = CUDD_MEMORY_OUT;
  1619. FREE(gen);
  1620. return(NULL);
  1621. }
  1622. for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
  1623. /* The maximum stack depth is one plus the number of variables.
  1624. ** because a path may have nodes at all levels, including the
  1625. ** constant level.
  1626. */
  1627. gen->stack.stack = ALLOC(DdNodePtr, nvars+1);
  1628. if (gen->stack.stack == NULL) {
  1629. dd->errorCode = CUDD_MEMORY_OUT;
  1630. FREE(gen->gen.cubes.cube);
  1631. FREE(gen);
  1632. return(NULL);
  1633. }
  1634. for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
  1635. /* Find the first cube of the onset. */
  1636. gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
  1637. while (1) {
  1638. top = gen->stack.stack[gen->stack.sp-1];
  1639. treg = Cudd_Regular(top);
  1640. if (!cuddIsConstant(treg)) {
  1641. /* Take the else branch first. */
  1642. gen->gen.cubes.cube[treg->index] = 0;
  1643. next = cuddE(treg);
  1644. if (top != treg) next = Cudd_Not(next);
  1645. gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
  1646. } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
  1647. /* Backtrack */
  1648. while (1) {
  1649. if (gen->stack.sp == 1) {
  1650. /* The current node has no predecessor. */
  1651. gen->status = CUDD_GEN_EMPTY;
  1652. gen->stack.sp--;
  1653. goto done;
  1654. }
  1655. prev = gen->stack.stack[gen->stack.sp-2];
  1656. preg = Cudd_Regular(prev);
  1657. nreg = cuddT(preg);
  1658. if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
  1659. if (next != top) { /* follow the then branch next */
  1660. gen->gen.cubes.cube[preg->index] = 1;
  1661. gen->stack.stack[gen->stack.sp-1] = next;
  1662. break;
  1663. }
  1664. /* Pop the stack and try again. */
  1665. gen->gen.cubes.cube[preg->index] = 2;
  1666. gen->stack.sp--;
  1667. top = gen->stack.stack[gen->stack.sp-1];
  1668. }
  1669. } else {
  1670. gen->status = CUDD_GEN_NONEMPTY;
  1671. gen->gen.cubes.value = cuddV(top);
  1672. goto done;
  1673. }
  1674. }
  1675. done:
  1676. *cube = gen->gen.cubes.cube;
  1677. *value = gen->gen.cubes.value;
  1678. return(gen);
  1679. } /* end of Cudd_FirstCube */
  1680. /**
  1681. @brief Generates the next cube of a decision diagram onset.
  1682. @return 0 if the enumeration is completed; 1 otherwise.
  1683. @sideeffect The cube and its value are returned as side effects. The
  1684. generator is modified.
  1685. @see Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty
  1686. Cudd_NextNode
  1687. */
  1688. int
  1689. Cudd_NextCube(
  1690. DdGen * gen,
  1691. int ** cube,
  1692. CUDD_VALUE_TYPE * value)
  1693. {
  1694. DdNode *top, *treg, *next, *nreg, *prev, *preg;
  1695. DdManager *dd = gen->manager;
  1696. /* Backtrack from previously reached terminal node. */
  1697. while (1) {
  1698. if (gen->stack.sp == 1) {
  1699. /* The current node has no predecessor. */
  1700. gen->status = CUDD_GEN_EMPTY;
  1701. gen->stack.sp--;
  1702. goto done;
  1703. }
  1704. top = gen->stack.stack[gen->stack.sp-1];
  1705. prev = gen->stack.stack[gen->stack.sp-2];
  1706. preg = Cudd_Regular(prev);
  1707. nreg = cuddT(preg);
  1708. if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
  1709. if (next != top) { /* follow the then branch next */
  1710. gen->gen.cubes.cube[preg->index] = 1;
  1711. gen->stack.stack[gen->stack.sp-1] = next;
  1712. break;
  1713. }
  1714. /* Pop the stack and try again. */
  1715. gen->gen.cubes.cube[preg->index] = 2;
  1716. gen->stack.sp--;
  1717. }
  1718. while (1) {
  1719. top = gen->stack.stack[gen->stack.sp-1];
  1720. treg = Cudd_Regular(top);
  1721. if (!cuddIsConstant(treg)) {
  1722. /* Take the else branch first. */
  1723. gen->gen.cubes.cube[treg->index] = 0;
  1724. next = cuddE(treg);
  1725. if (top != treg) next = Cudd_Not(next);
  1726. gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
  1727. } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
  1728. /* Backtrack */
  1729. while (1) {
  1730. if (gen->stack.sp == 1) {
  1731. /* The current node has no predecessor. */
  1732. gen->status = CUDD_GEN_EMPTY;
  1733. gen->stack.sp--;
  1734. goto done;
  1735. }
  1736. prev = gen->stack.stack[gen->stack.sp-2];
  1737. preg = Cudd_Regular(prev);
  1738. nreg = cuddT(preg);
  1739. if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
  1740. if (next != top) { /* follow the then branch next */
  1741. gen->gen.cubes.cube[preg->index] = 1;
  1742. gen->stack.stack[gen->stack.sp-1] = next;
  1743. break;
  1744. }
  1745. /* Pop the stack and try again. */
  1746. gen->gen.cubes.cube[preg->index] = 2;
  1747. gen->stack.sp--;
  1748. top = gen->stack.stack[gen->stack.sp-1];
  1749. }
  1750. } else {
  1751. gen->status = CUDD_GEN_NONEMPTY;
  1752. gen->gen.cubes.value = cuddV(top);
  1753. goto done;
  1754. }
  1755. }
  1756. done:
  1757. if (gen->status == CUDD_GEN_EMPTY) return(0);
  1758. *cube = gen->gen.cubes.cube;
  1759. *value = gen->gen.cubes.value;
  1760. return(1);
  1761. } /* end of Cudd_NextCube */
  1762. /**
  1763. @brief Finds the first prime of a Boolean function.
  1764. @details@parblock
  1765. Defines an iterator on a pair of BDDs describing a
  1766. (possibly incompletely specified) Boolean functions and finds the
  1767. first cube of a cover of the function.
  1768. The two argument BDDs are the lower and upper bounds of an interval.
  1769. It is a mistake to call this function with a lower bound that is not
  1770. less than or equal to the upper bound.
  1771. A cube is represented as an array of literals, which are integers in
  1772. {0, 1, 2}; 0 represents a complemented literal, 1 represents an
  1773. uncomplemented literal, and 2 stands for don't care. The enumeration
  1774. produces a prime and irredundant cover of the function associated
  1775. with the two BDDs. The size of the array equals the number of
  1776. variables in the manager at the time Cudd_FirstCube is called.
  1777. This iterator can only be used on BDDs.
  1778. @endparblock
  1779. @return a generator that contains the information necessary to
  1780. continue the enumeration if successful; NULL otherwise.
  1781. @sideeffect The first cube is returned as side effect.
  1782. @see Cudd_ForeachPrime Cudd_NextPrime Cudd_GenFree Cudd_IsGenEmpty
  1783. Cudd_FirstCube Cudd_FirstNode
  1784. */
  1785. DdGen *
  1786. Cudd_FirstPrime(
  1787. DdManager *dd,
  1788. DdNode *l,
  1789. DdNode *u,
  1790. int **cube)
  1791. {
  1792. DdGen *gen;
  1793. DdNode *implicant, *prime, *tmp;
  1794. int length, result;
  1795. /* Sanity Check. */
  1796. if (dd == NULL || l == NULL || u == NULL) return(NULL);
  1797. /* Allocate generator an initialize it. */
  1798. gen = ALLOC(DdGen,1);
  1799. if (gen == NULL) {
  1800. dd->errorCode = CUDD_MEMORY_OUT;
  1801. return(NULL);
  1802. }
  1803. gen->manager = dd;
  1804. gen->type = CUDD_GEN_PRIMES;
  1805. gen->status = CUDD_GEN_EMPTY;
  1806. gen->gen.primes.cube = NULL;
  1807. gen->gen.primes.ub = u;
  1808. gen->stack.sp = 0;
  1809. gen->stack.stack = NULL;
  1810. gen->node = l;
  1811. cuddRef(l);
  1812. gen->gen.primes.cube = ALLOC(int,dd->size);
  1813. if (gen->gen.primes.cube == NULL) {
  1814. dd->errorCode = CUDD_MEMORY_OUT;
  1815. FREE(gen);
  1816. return(NULL);
  1817. }
  1818. if (gen->node == Cudd_ReadLogicZero(dd)) {
  1819. gen->status = CUDD_GEN_EMPTY;
  1820. } else {
  1821. implicant = Cudd_LargestCube(dd,gen->node,&length);
  1822. if (implicant == NULL) {
  1823. Cudd_RecursiveDeref(dd,gen->node);
  1824. FREE(gen->gen.primes.cube);
  1825. FREE(gen);
  1826. return(NULL);
  1827. }
  1828. cuddRef(implicant);
  1829. prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
  1830. if (prime == NULL) {
  1831. Cudd_RecursiveDeref(dd,gen->node);
  1832. Cudd_RecursiveDeref(dd,implicant);
  1833. FREE(gen->gen.primes.cube);
  1834. FREE(gen);
  1835. return(NULL);
  1836. }
  1837. cuddRef(prime);
  1838. Cudd_RecursiveDeref(dd,implicant);
  1839. tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
  1840. if (tmp == NULL) {
  1841. Cudd_RecursiveDeref(dd,gen->node);
  1842. Cudd_RecursiveDeref(dd,prime);
  1843. FREE(gen->gen.primes.cube);
  1844. FREE(gen);
  1845. return(NULL);
  1846. }
  1847. cuddRef(tmp);
  1848. Cudd_RecursiveDeref(dd,gen->node);
  1849. gen->node = tmp;
  1850. result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
  1851. if (result == 0) {
  1852. Cudd_RecursiveDeref(dd,gen->node);
  1853. Cudd_RecursiveDeref(dd,prime);
  1854. FREE(gen->gen.primes.cube);
  1855. FREE(gen);
  1856. return(NULL);
  1857. }
  1858. Cudd_RecursiveDeref(dd,prime);
  1859. gen->status = CUDD_GEN_NONEMPTY;
  1860. }
  1861. *cube = gen->gen.primes.cube;
  1862. return(gen);
  1863. } /* end of Cudd_FirstPrime */
  1864. /**
  1865. @brief Generates the next prime of a Boolean function.
  1866. @return 0 if the enumeration is completed; 1 otherwise.
  1867. @sideeffect The cube and is returned as side effects. The
  1868. generator is modified.
  1869. @see Cudd_ForeachPrime Cudd_FirstPrime Cudd_GenFree Cudd_IsGenEmpty
  1870. Cudd_NextCube Cudd_NextNode
  1871. */
  1872. int
  1873. Cudd_NextPrime(
  1874. DdGen *gen,
  1875. int **cube)
  1876. {
  1877. DdNode *implicant, *prime, *tmp;
  1878. DdManager *dd = gen->manager;
  1879. int length, result;
  1880. if (gen->node == Cudd_ReadLogicZero(dd)) {
  1881. gen->status = CUDD_GEN_EMPTY;
  1882. } else {
  1883. implicant = Cudd_LargestCube(dd,gen->node,&length);
  1884. if (implicant == NULL) {
  1885. gen->status = CUDD_GEN_EMPTY;
  1886. return(0);
  1887. }
  1888. cuddRef(implicant);
  1889. prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
  1890. if (prime == NULL) {
  1891. Cudd_RecursiveDeref(dd,implicant);
  1892. gen->status = CUDD_GEN_EMPTY;
  1893. return(0);
  1894. }
  1895. cuddRef(prime);
  1896. Cudd_RecursiveDeref(dd,implicant);
  1897. tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
  1898. if (tmp == NULL) {
  1899. Cudd_RecursiveDeref(dd,prime);
  1900. gen->status = CUDD_GEN_EMPTY;
  1901. return(0);
  1902. }
  1903. cuddRef(tmp);
  1904. Cudd_RecursiveDeref(dd,gen->node);
  1905. gen->node = tmp;
  1906. result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
  1907. if (result == 0) {
  1908. Cudd_RecursiveDeref(dd,prime);
  1909. gen->status = CUDD_GEN_EMPTY;
  1910. return(0);
  1911. }
  1912. Cudd_RecursiveDeref(dd,prime);
  1913. gen->status = CUDD_GEN_NONEMPTY;
  1914. }
  1915. if (gen->status == CUDD_GEN_EMPTY) return(0);
  1916. *cube = gen->gen.primes.cube;
  1917. return(1);
  1918. } /* end of Cudd_NextPrime */
  1919. /**
  1920. @brief Computes the cube of an array of %BDD variables.
  1921. @details If non-null, the phase argument indicates which literal of
  1922. each variable should appear in the cube. If phase\[i\] is nonzero,
  1923. then the positive literal is used. If phase is NULL, the cube is
  1924. positive unate.
  1925. @return a pointer to the result if successful; NULL otherwise.
  1926. @sideeffect None
  1927. @see Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd
  1928. */
  1929. DdNode *
  1930. Cudd_bddComputeCube(
  1931. DdManager * dd,
  1932. DdNode ** vars,
  1933. int * phase,
  1934. int n)
  1935. {
  1936. DdNode *cube;
  1937. DdNode *fn;
  1938. int i;
  1939. cube = DD_ONE(dd);
  1940. cuddRef(cube);
  1941. for (i = n - 1; i >= 0; i--) {
  1942. if (phase == NULL || phase[i] != 0) {
  1943. fn = Cudd_bddAnd(dd,vars[i],cube);
  1944. } else {
  1945. fn = Cudd_bddAnd(dd,Cudd_Not(vars[i]),cube);
  1946. }
  1947. if (fn == NULL) {
  1948. Cudd_RecursiveDeref(dd,cube);
  1949. return(NULL);
  1950. }
  1951. cuddRef(fn);
  1952. Cudd_RecursiveDeref(dd,cube);
  1953. cube = fn;
  1954. }
  1955. cuddDeref(cube);
  1956. return(cube);
  1957. } /* end of Cudd_bddComputeCube */
  1958. /**
  1959. @brief Computes the cube of an array of %ADD variables.
  1960. @details If non-null, the phase argument indicates which literal of
  1961. each variable should appear in the cube. If phase\[i\] is nonzero,
  1962. then the positive literal is used. If phase is NULL, the cube is
  1963. positive unate.
  1964. @return a pointer to the result if successful; NULL otherwise.
  1965. @sideeffect none
  1966. @see Cudd_bddComputeCube
  1967. */
  1968. DdNode *
  1969. Cudd_addComputeCube(
  1970. DdManager * dd,
  1971. DdNode ** vars,
  1972. int * phase,
  1973. int n)
  1974. {
  1975. DdNode *cube, *azero;
  1976. DdNode *fn;
  1977. int i;
  1978. cube = DD_ONE(dd);
  1979. cuddRef(cube);
  1980. azero = DD_ZERO(dd);
  1981. for (i = n - 1; i >= 0; i--) {
  1982. if (phase == NULL || phase[i] != 0) {
  1983. fn = Cudd_addIte(dd,vars[i],cube,azero);
  1984. } else {
  1985. fn = Cudd_addIte(dd,vars[i],azero,cube);
  1986. }
  1987. if (fn == NULL) {
  1988. Cudd_RecursiveDeref(dd,cube);
  1989. return(NULL);
  1990. }
  1991. cuddRef(fn);
  1992. Cudd_RecursiveDeref(dd,cube);
  1993. cube = fn;
  1994. }
  1995. cuddDeref(cube);
  1996. return(cube);
  1997. } /* end of Cudd_addComputeCube */
  1998. /**
  1999. @brief Builds the %BDD of a cube from a positional array.
  2000. @details The array must have one integer entry for each %BDD
  2001. variable. If the i-th entry is 1, the variable of index i appears
  2002. in true form in the cube; If the i-th entry is 0, the variable of
  2003. index i appears complemented in the cube; otherwise the variable
  2004. does not appear in the cube.
  2005. @return a pointer to the %BDD for the cube if successful; NULL
  2006. otherwise.
  2007. @sideeffect None
  2008. @see Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray
  2009. */
  2010. DdNode *
  2011. Cudd_CubeArrayToBdd(
  2012. DdManager *dd,
  2013. int *array)
  2014. {
  2015. DdNode *cube, *var, *tmp;
  2016. int i;
  2017. int size = Cudd_ReadSize(dd);
  2018. cube = DD_ONE(dd);
  2019. cuddRef(cube);
  2020. for (i = size - 1; i >= 0; i--) {
  2021. if ((array[i] & ~1) == 0) {
  2022. var = Cudd_bddIthVar(dd,i);
  2023. tmp = Cudd_bddAnd(dd,cube,Cudd_NotCond(var,array[i]==0));
  2024. if (tmp == NULL) {
  2025. Cudd_RecursiveDeref(dd,cube);
  2026. return(NULL);
  2027. }
  2028. cuddRef(tmp);
  2029. Cudd_RecursiveDeref(dd,cube);
  2030. cube = tmp;
  2031. }
  2032. }
  2033. cuddDeref(cube);
  2034. return(cube);
  2035. } /* end of Cudd_CubeArrayToBdd */
  2036. /**
  2037. @brief Builds a positional array from the %BDD of a cube.
  2038. @details Array must have one entry for each %BDD variable. The
  2039. positional array has 1 in i-th position if the variable of index i
  2040. appears in true form in the cube; it has 0 in i-th position if the
  2041. variable of index i appears in complemented form in the cube;
  2042. finally, it has 2 in i-th position if the variable of index i does
  2043. not appear in the cube.
  2044. @return 1 if successful (the %BDD is indeed a cube); 0 otherwise.
  2045. @sideeffect The result is in the array passed by reference.
  2046. @see Cudd_CubeArrayToBdd
  2047. */
  2048. int
  2049. Cudd_BddToCubeArray(
  2050. DdManager *dd,
  2051. DdNode *cube,
  2052. int *array)
  2053. {
  2054. DdNode *scan, *t, *e;
  2055. int i;
  2056. int size = Cudd_ReadSize(dd);
  2057. DdNode *lzero = Cudd_Not(DD_ONE(dd));
  2058. for (i = size-1; i >= 0; i--) {
  2059. array[i] = 2;
  2060. }
  2061. scan = cube;
  2062. while (!Cudd_IsConstantInt(scan)) {
  2063. unsigned int index = Cudd_Regular(scan)->index;
  2064. cuddGetBranches(scan,&t,&e);
  2065. if (t == lzero) {
  2066. array[index] = 0;
  2067. scan = e;
  2068. } else if (e == lzero) {
  2069. array[index] = 1;
  2070. scan = t;
  2071. } else {
  2072. return(0); /* cube is not a cube */
  2073. }
  2074. }
  2075. if (scan == lzero) {
  2076. return(0);
  2077. } else {
  2078. return(1);
  2079. }
  2080. } /* end of Cudd_BddToCubeArray */
  2081. /**
  2082. @brief Finds the first node of a decision diagram.
  2083. @details Defines an iterator on the nodes of a decision diagram and
  2084. finds its first node. The nodes are enumerated in a reverse
  2085. topological order, so that a node is always preceded in the
  2086. enumeration by its descendants.
  2087. @return a generator that contains the information necessary to
  2088. continue the enumeration if successful; NULL otherwise.
  2089. @sideeffect The first node is returned as a side effect.
  2090. @see Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty
  2091. Cudd_FirstCube
  2092. */
  2093. DdGen *
  2094. Cudd_FirstNode(
  2095. DdManager * dd,
  2096. DdNode * f,
  2097. DdNode ** node)
  2098. {
  2099. DdGen *gen;
  2100. int size;
  2101. /* Sanity Check. */
  2102. if (dd == NULL || f == NULL) return(NULL);
  2103. /* Allocate generator an initialize it. */
  2104. gen = ALLOC(DdGen,1);
  2105. if (gen == NULL) {
  2106. dd->errorCode = CUDD_MEMORY_OUT;
  2107. return(NULL);
  2108. }
  2109. gen->manager = dd;
  2110. gen->type = CUDD_GEN_NODES;
  2111. gen->status = CUDD_GEN_EMPTY;
  2112. gen->stack.sp = 0;
  2113. gen->node = NULL;
  2114. /* Collect all the nodes on the generator stack for later perusal. */
  2115. gen->stack.stack = cuddNodeArray(Cudd_Regular(f), &size);
  2116. if (gen->stack.stack == NULL) {
  2117. FREE(gen);
  2118. dd->errorCode = CUDD_MEMORY_OUT;
  2119. return(NULL);
  2120. }
  2121. gen->gen.nodes.size = size;
  2122. /* Find the first node. */
  2123. if (gen->stack.sp < gen->gen.nodes.size) {
  2124. gen->status = CUDD_GEN_NONEMPTY;
  2125. gen->node = gen->stack.stack[gen->stack.sp];
  2126. *node = gen->node;
  2127. }
  2128. return(gen);
  2129. } /* end of Cudd_FirstNode */
  2130. /**
  2131. @brief Finds the next node of a decision diagram.
  2132. @return 0 if the enumeration is completed; 1 otherwise.
  2133. @sideeffect The next node is returned as a side effect.
  2134. @see Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty
  2135. Cudd_NextCube
  2136. */
  2137. int
  2138. Cudd_NextNode(
  2139. DdGen * gen,
  2140. DdNode ** node)
  2141. {
  2142. /* Find the next node. */
  2143. gen->stack.sp++;
  2144. if (gen->stack.sp < gen->gen.nodes.size) {
  2145. gen->node = gen->stack.stack[gen->stack.sp];
  2146. *node = gen->node;
  2147. return(1);
  2148. } else {
  2149. gen->status = CUDD_GEN_EMPTY;
  2150. return(0);
  2151. }
  2152. } /* end of Cudd_NextNode */
  2153. /**
  2154. @brief Frees a CUDD generator.
  2155. @return always 0.
  2156. @sideeffect None
  2157. @see Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
  2158. Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty
  2159. */
  2160. int
  2161. Cudd_GenFree(
  2162. DdGen * gen)
  2163. {
  2164. if (gen == NULL) return(0);
  2165. switch (gen->type) {
  2166. case CUDD_GEN_CUBES:
  2167. case CUDD_GEN_ZDD_PATHS:
  2168. FREE(gen->gen.cubes.cube);
  2169. FREE(gen->stack.stack);
  2170. break;
  2171. case CUDD_GEN_PRIMES:
  2172. FREE(gen->gen.primes.cube);
  2173. Cudd_RecursiveDeref(gen->manager,gen->node);
  2174. break;
  2175. case CUDD_GEN_NODES:
  2176. FREE(gen->stack.stack);
  2177. break;
  2178. default:
  2179. return(0);
  2180. }
  2181. FREE(gen);
  2182. return(0);
  2183. } /* end of Cudd_GenFree */
  2184. /**
  2185. @brief Queries the status of a generator.
  2186. @return 1 if the generator is empty or NULL; 0 otherswise.
  2187. @sideeffect None
  2188. @see Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
  2189. Cudd_FirstNode Cudd_NextNode Cudd_GenFree
  2190. */
  2191. int
  2192. Cudd_IsGenEmpty(
  2193. DdGen * gen)
  2194. {
  2195. if (gen == NULL) return(1);
  2196. return(gen->status == CUDD_GEN_EMPTY);
  2197. } /* end of Cudd_IsGenEmpty */
  2198. /**
  2199. @brief Builds a cube of %BDD variables from an array of indices.
  2200. @return a pointer to the result if successful; NULL otherwise.
  2201. @sideeffect None
  2202. @see Cudd_bddComputeCube Cudd_CubeArrayToBdd
  2203. */
  2204. DdNode *
  2205. Cudd_IndicesToCube(
  2206. DdManager * dd,
  2207. int * array,
  2208. int n)
  2209. {
  2210. DdNode *cube, *tmp;
  2211. int i;
  2212. cube = DD_ONE(dd);
  2213. cuddRef(cube);
  2214. for (i = n - 1; i >= 0; i--) {
  2215. tmp = Cudd_bddAnd(dd,Cudd_bddIthVar(dd,array[i]),cube);
  2216. if (tmp == NULL) {
  2217. Cudd_RecursiveDeref(dd,cube);
  2218. return(NULL);
  2219. }
  2220. cuddRef(tmp);
  2221. Cudd_RecursiveDeref(dd,cube);
  2222. cube = tmp;
  2223. }
  2224. cuddDeref(cube);
  2225. return(cube);
  2226. } /* end of Cudd_IndicesToCube */
  2227. /**
  2228. @brief Prints the package version number.
  2229. @sideeffect None
  2230. */
  2231. void
  2232. Cudd_PrintVersion(
  2233. FILE * fp)
  2234. {
  2235. (void) fprintf(fp, "%s\n", CUDD_VERSION);
  2236. } /* end of Cudd_PrintVersion */
  2237. /**
  2238. @brief Computes the average distance between adjacent nodes in the manager.
  2239. @details Adjacent nodes are node pairs such that the second node
  2240. is the then child, else child, or next node in the collision list.
  2241. @sideeffect None
  2242. */
  2243. double
  2244. Cudd_AverageDistance(
  2245. DdManager * dd)
  2246. {
  2247. double tetotal, nexttotal;
  2248. double tesubtotal, nextsubtotal;
  2249. double temeasured, nextmeasured;
  2250. int i, j;
  2251. int slots, nvars;
  2252. ptrdiff_t diff;
  2253. DdNode *scan;
  2254. DdNodePtr *nodelist;
  2255. DdNode *sentinel = &(dd->sentinel);
  2256. nvars = dd->size;
  2257. if (nvars == 0) return(0.0);
  2258. /* Initialize totals. */
  2259. tetotal = 0.0;
  2260. nexttotal = 0.0;
  2261. temeasured = 0.0;
  2262. nextmeasured = 0.0;
  2263. /* Scan the variable subtables. */
  2264. for (i = 0; i < nvars; i++) {
  2265. nodelist = dd->subtables[i].nodelist;
  2266. tesubtotal = 0.0;
  2267. nextsubtotal = 0.0;
  2268. slots = dd->subtables[i].slots;
  2269. for (j = 0; j < slots; j++) {
  2270. scan = nodelist[j];
  2271. while (scan != sentinel) {
  2272. diff = (ptrint) scan - (ptrint) cuddT(scan);
  2273. tesubtotal += (double) ddAbs(diff);
  2274. diff = (ptrint) scan - (ptrint) Cudd_Regular(cuddE(scan));
  2275. tesubtotal += (double) ddAbs(diff);
  2276. temeasured += 2.0;
  2277. if (scan->next != sentinel) {
  2278. diff = (ptrint) scan - (ptrint) scan->next;
  2279. nextsubtotal += (double) ddAbs(diff);
  2280. nextmeasured += 1.0;
  2281. }
  2282. scan = scan->next;
  2283. }
  2284. }
  2285. tetotal += tesubtotal;
  2286. nexttotal += nextsubtotal;
  2287. }
  2288. /* Scan the constant table. */
  2289. nodelist = dd->constants.nodelist;
  2290. nextsubtotal = 0.0;
  2291. slots = dd->constants.slots;
  2292. for (j = 0; j < slots; j++) {
  2293. scan = nodelist[j];
  2294. while (scan != NULL) {
  2295. if (scan->next != NULL) {
  2296. diff = (ptrint) scan - (ptrint) scan->next;
  2297. nextsubtotal += (double) ddAbs(diff);
  2298. nextmeasured += 1.0;
  2299. }
  2300. scan = scan->next;
  2301. }
  2302. }
  2303. nexttotal += nextsubtotal;
  2304. return((tetotal + nexttotal) / (temeasured + nextmeasured));
  2305. } /* end of Cudd_AverageDistance */
  2306. /**
  2307. @brief Portable random number generator.
  2308. @details Based on ran2 from "Numerical Recipes in C." It is a long
  2309. period (> 2 * 10^18) random number generator of L'Ecuyer with
  2310. Bays-Durham shuffle. The random generator can be explicitly
  2311. initialized by calling Cudd_Srandom. If no explicit initialization
  2312. is performed, then the seed 1 is assumed.
  2313. @return a long integer uniformly distributed between 0 and
  2314. 2147483561 (inclusive of the endpoint values).
  2315. @sideeffect None
  2316. @see Cudd_Srandom
  2317. */
  2318. int32_t
  2319. Cudd_Random(DdManager *dd)
  2320. {
  2321. int i; /* index in the shuffle table */
  2322. int32_t w; /* work variable */
  2323. /* dd->cuddRand == 0 if the geneartor has not been initialized yet. */
  2324. if (dd->cuddRand == 0) Cudd_Srandom(dd,1);
  2325. /* Compute cuddRand = (cuddRand * LEQA1) % MODULUS1 avoiding
  2326. ** overflows by Schrage's method.
  2327. */
  2328. w = dd->cuddRand / LEQQ1;
  2329. dd->cuddRand = LEQA1 * (dd->cuddRand - w * LEQQ1) - w * LEQR1;
  2330. dd->cuddRand += (dd->cuddRand < 0) * MODULUS1;
  2331. /* Compute dd->cuddRand2 = (dd->cuddRand2 * LEQA2) % MODULUS2 avoiding
  2332. ** overflows by Schrage's method.
  2333. */
  2334. w = dd->cuddRand2 / LEQQ2;
  2335. dd->cuddRand2 = LEQA2 * (dd->cuddRand2 - w * LEQQ2) - w * LEQR2;
  2336. dd->cuddRand2 += (dd->cuddRand2 < 0) * MODULUS2;
  2337. /* dd->cuddRand is shuffled with the Bays-Durham algorithm.
  2338. ** dd->shuffleSelect and cuddRand2 are combined to generate the output.
  2339. */
  2340. /* Pick one element from the shuffle table; "i" will be in the range
  2341. ** from 0 to STAB_SIZE-1.
  2342. */
  2343. i = (int) (dd->shuffleSelect / STAB_DIV);
  2344. /* Mix the element of the shuffle table with the current iterate of
  2345. ** the second sub-generator, and replace the chosen element of the
  2346. ** shuffle table with the current iterate of the first sub-generator.
  2347. */
  2348. dd->shuffleSelect = dd->shuffleTable[i] - dd->cuddRand2;
  2349. dd->shuffleTable[i] = dd->cuddRand;
  2350. dd->shuffleSelect += (dd->shuffleSelect < 1) * (MODULUS1 - 1);
  2351. /* Since dd->shuffleSelect != 0, and we want to be able to return 0,
  2352. ** here we subtract 1 before returning.
  2353. */
  2354. return(dd->shuffleSelect - 1);
  2355. } /* end of Cudd_Random */
  2356. /**
  2357. @brief Initializer for the portable random number generator.
  2358. @details Based on ran2 in "Numerical Recipes in C." The input is the
  2359. seed for the generator. If it is negative, its absolute value is
  2360. taken as seed. If it is 0, then 1 is taken as seed. The initialized
  2361. sets up the two recurrences used to generate a long-period stream,
  2362. and sets up the shuffle table.
  2363. @sideeffect None
  2364. @see Cudd_Random
  2365. */
  2366. void
  2367. Cudd_Srandom(
  2368. DdManager *dd,
  2369. int32_t seed)
  2370. {
  2371. int32_t i;
  2372. if (seed < 0) dd->cuddRand = -seed;
  2373. else if (seed == 0) dd->cuddRand = 1;
  2374. else dd->cuddRand = seed;
  2375. dd->cuddRand2 = dd->cuddRand;
  2376. /* Load the shuffle table (after 11 warm-ups). */
  2377. for (i = 0; i < STAB_SIZE + 11; i++) {
  2378. int32_t w;
  2379. w = dd->cuddRand / LEQQ1;
  2380. dd->cuddRand = LEQA1 * (dd->cuddRand - w * LEQQ1) - w * LEQR1;
  2381. dd->cuddRand += (dd->cuddRand < 0) * MODULUS1;
  2382. dd->shuffleTable[i % STAB_SIZE] = dd->cuddRand;
  2383. }
  2384. dd->shuffleSelect = dd->shuffleTable[1 % STAB_SIZE];
  2385. } /* end of Cudd_Srandom */
  2386. /**
  2387. @brief Computes the density of a %BDD or %ADD.
  2388. @details The density is the ratio of the number of minterms to the
  2389. number of nodes. If 0 is passed as number of variables, the number
  2390. of variables existing in the manager is used.
  2391. @return the density if successful; (double) CUDD_OUT_OF_MEM
  2392. otherwise.
  2393. @sideeffect None
  2394. @see Cudd_CountMinterm Cudd_DagSize
  2395. */
  2396. double
  2397. Cudd_Density(
  2398. DdManager * dd /**< manager */,
  2399. DdNode * f /**< function whose density is sought */,
  2400. int nvars /**< size of the support of f */)
  2401. {
  2402. double minterms;
  2403. int nodes;
  2404. double density;
  2405. if (nvars == 0) nvars = dd->size;
  2406. minterms = Cudd_CountMinterm(dd,f,nvars);
  2407. if (minterms == (double) CUDD_OUT_OF_MEM) return(minterms);
  2408. nodes = Cudd_DagSize(f);
  2409. density = minterms / (double) nodes;
  2410. return(density);
  2411. } /* end of Cudd_Density */
  2412. /**
  2413. @brief Warns that a memory allocation failed.
  2414. @details This function can be used as replacement of MMout_of_memory
  2415. to prevent the safe_mem functions of the util package from exiting
  2416. when malloc returns NULL. One possible use is in case of
  2417. discretionary allocations; for instance, an allocation of memory to
  2418. enlarge the computed table.
  2419. @sideeffect None
  2420. @see Cudd_OutOfMemSilent Cudd_RegisterOutOfMemoryCallback
  2421. */
  2422. void
  2423. Cudd_OutOfMem(
  2424. size_t size /**< size of the allocation that failed */)
  2425. {
  2426. (void) fflush(stdout);
  2427. (void) fprintf(stderr, "\nCUDD: unable to allocate %" PRIszt " bytes\n",
  2428. size);
  2429. } /* end of Cudd_OutOfMem */
  2430. /**
  2431. @brief Doesn not warn that a memory allocation failed.
  2432. @details This function can be used as replacement of MMout_of_memory
  2433. to prevent the safe_mem functions of the util package from exiting
  2434. when malloc returns NULL. One possible use is in case of
  2435. discretionary allocations; for instance, an allocation of memory to
  2436. enlarge the computed table.
  2437. @sideeffect None
  2438. @see Cudd_OutOfMem Cudd_RegisterOutOfMemoryCallback
  2439. */
  2440. void
  2441. Cudd_OutOfMemSilent(
  2442. size_t size /**< size of the allocation that failed */)
  2443. {
  2444. (void) size; /* suppress warning */
  2445. } /* end of Cudd_OutOfMem */
  2446. /*---------------------------------------------------------------------------*/
  2447. /* Definition of internal functions */
  2448. /*---------------------------------------------------------------------------*/
  2449. /**
  2450. @brief Prints a %DD to the standard output. One line per node is
  2451. printed.
  2452. @return 1 if successful; 0 otherwise.
  2453. @sideeffect None
  2454. @see Cudd_PrintDebug
  2455. */
  2456. int
  2457. cuddP(
  2458. DdManager * dd,
  2459. DdNode * f)
  2460. {
  2461. int retval;
  2462. st_table *table = st_init_table(st_ptrcmp,st_ptrhash);
  2463. if (table == NULL) return(0);
  2464. retval = dp2(dd,f,table);
  2465. st_free_table(table);
  2466. (void) fputc('\n',dd->out);
  2467. return(retval);
  2468. } /* end of cuddP */
  2469. /**
  2470. @brief Frees the memory used to store the minterm counts recorded
  2471. in the visited table.
  2472. @return ST_CONTINUE.
  2473. @sideeffect None
  2474. */
  2475. enum st_retval
  2476. cuddStCountfree(
  2477. void * key,
  2478. void * value,
  2479. void * arg)
  2480. {
  2481. double *d = (double *)value;
  2482. (void) key; /* avoid warning */
  2483. (void) arg; /* avoid warning */
  2484. FREE(d);
  2485. return(ST_CONTINUE);
  2486. } /* end of cuddStCountfree */
  2487. /**
  2488. @brief Recursively collects all the nodes of a %DD in a symbol
  2489. table.
  2490. @details Traverses the %DD f and collects all its nodes in a
  2491. symbol table. f is assumed to be a regular pointer and
  2492. cuddCollectNodes guarantees this assumption in the recursive calls.
  2493. @return 1 in case of success; 0 otherwise.
  2494. @sideeffect None
  2495. */
  2496. int
  2497. cuddCollectNodes(
  2498. DdNode * f,
  2499. st_table * visited)
  2500. {
  2501. DdNode *T, *E;
  2502. int retval;
  2503. #ifdef DD_DEBUG
  2504. assert(!Cudd_IsComplement(f));
  2505. #endif
  2506. /* If already visited, nothing to do. */
  2507. if (st_is_member(visited, f) == 1)
  2508. return(1);
  2509. /* Check for abnormal condition that should never happen. */
  2510. if (f == NULL)
  2511. return(0);
  2512. /* Mark node as visited. */
  2513. if (st_add_direct(visited, f, NULL) == ST_OUT_OF_MEM)
  2514. return(0);
  2515. /* Check terminal case. */
  2516. if (cuddIsConstant(f))
  2517. return(1);
  2518. /* Recursive calls. */
  2519. T = cuddT(f);
  2520. retval = cuddCollectNodes(T,visited);
  2521. if (retval != 1) return(retval);
  2522. E = Cudd_Regular(cuddE(f));
  2523. retval = cuddCollectNodes(E,visited);
  2524. return(retval);
  2525. } /* end of cuddCollectNodes */
  2526. /**
  2527. @brief Recursively collects all the nodes of a %DD in an array.
  2528. @details Traverses the %DD f and collects all its nodes in an array.
  2529. The caller should free the array returned by cuddNodeArray. The
  2530. nodes are collected in reverse topological order, so that a node is
  2531. always preceded in the array by all its descendants.
  2532. @return a pointer to the array of nodes in case of success; NULL
  2533. otherwise.
  2534. @sideeffect The number of nodes is returned as a side effect.
  2535. @see Cudd_FirstNode
  2536. */
  2537. DdNodePtr *
  2538. cuddNodeArray(
  2539. DdNode *f,
  2540. int *n)
  2541. {
  2542. DdNodePtr *table;
  2543. int size, retval;
  2544. size = ddDagInt(Cudd_Regular(f));
  2545. table = ALLOC(DdNodePtr, size);
  2546. if (table == NULL) {
  2547. ddClearFlag(Cudd_Regular(f));
  2548. return(NULL);
  2549. }
  2550. retval = cuddNodeArrayRecur(f, table, 0);
  2551. assert(retval == size);
  2552. *n = size;
  2553. return(table);
  2554. } /* cuddNodeArray */
  2555. /*---------------------------------------------------------------------------*/
  2556. /* Definition of static functions */
  2557. /*---------------------------------------------------------------------------*/
  2558. /**
  2559. @brief Performs the recursive step of cuddP.
  2560. @return 1 in case of success; 0 otherwise.
  2561. @sideeffect None
  2562. */
  2563. static int
  2564. dp2(
  2565. DdManager *dd,
  2566. DdNode * f,
  2567. st_table * t)
  2568. {
  2569. DdNode *g, *n, *N;
  2570. int T,E;
  2571. if (f == NULL) {
  2572. return(0);
  2573. }
  2574. g = Cudd_Regular(f);
  2575. if (cuddIsConstant(g)) {
  2576. (void) fprintf(dd->out,"ID = %c0x%" PRIxPTR "\tvalue = %-9g\n", bang(f),
  2577. (ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
  2578. return(1);
  2579. }
  2580. if (st_is_member(t,g) == 1) {
  2581. return(1);
  2582. }
  2583. if (st_add_direct(t,g,NULL) == ST_OUT_OF_MEM)
  2584. return(0);
  2585. #ifdef DD_STATS
  2586. (void) fprintf(dd->out,"ID = %c0x%"PRIxPTR"\tindex = %d\tr = %d\t", bang(f),
  2587. (ptruint) g / (ptruint) sizeof(DdNode), g->index, g->ref);
  2588. #else
  2589. (void) fprintf(dd->out,"ID = %c0x%" PRIxPTR "\tindex = %u\t", bang(f),
  2590. (ptruint) g / (ptruint) sizeof(DdNode),g->index);
  2591. #endif
  2592. n = cuddT(g);
  2593. if (cuddIsConstant(n)) {
  2594. (void) fprintf(dd->out,"T = %-9g\t",cuddV(n));
  2595. T = 1;
  2596. } else {
  2597. (void) fprintf(dd->out,"T = 0x%" PRIxPTR "\t",
  2598. (ptruint) n / (ptruint) sizeof(DdNode));
  2599. T = 0;
  2600. }
  2601. n = cuddE(g);
  2602. N = Cudd_Regular(n);
  2603. if (cuddIsConstant(N)) {
  2604. (void) fprintf(dd->out,"E = %c%-9g\n",bang(n),cuddV(N));
  2605. E = 1;
  2606. } else {
  2607. (void) fprintf(dd->out,"E = %c0x%" PRIxPTR "\n",
  2608. bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
  2609. E = 0;
  2610. }
  2611. if (E == 0) {
  2612. if (dp2(dd,N,t) == 0)
  2613. return(0);
  2614. }
  2615. if (T == 0) {
  2616. if (dp2(dd,cuddT(g),t) == 0)
  2617. return(0);
  2618. }
  2619. return(1);
  2620. } /* end of dp2 */
  2621. /**
  2622. @brief Performs the recursive step of Cudd_PrintMinterm.
  2623. @sideeffect None
  2624. */
  2625. static void
  2626. ddPrintMintermAux(
  2627. DdManager * dd /**< manager */,
  2628. DdNode * node /**< current node */,
  2629. int * list /**< current recursion path */)
  2630. {
  2631. DdNode *N,*Nv,*Nnv;
  2632. int i,v;
  2633. unsigned int index;
  2634. N = Cudd_Regular(node);
  2635. if (cuddIsConstant(N)) {
  2636. /* Terminal case: Print one cube based on the current recursion
  2637. ** path, unless we have reached the background value (ADDs) or
  2638. ** the logical zero (BDDs).
  2639. */
  2640. if (node != dd->background && node != Cudd_Not(dd->one)) {
  2641. for (i = 0; i < dd->size; i++) {
  2642. v = list[i];
  2643. if (v == 0) (void) fprintf(dd->out,"0");
  2644. else if (v == 1) (void) fprintf(dd->out,"1");
  2645. else (void) fprintf(dd->out,"-");
  2646. }
  2647. (void) fprintf(dd->out," % g\n", cuddV(node));
  2648. }
  2649. } else {
  2650. Nv = cuddT(N);
  2651. Nnv = cuddE(N);
  2652. if (Cudd_IsComplement(node)) {
  2653. Nv = Cudd_Not(Nv);
  2654. Nnv = Cudd_Not(Nnv);
  2655. }
  2656. index = N->index;
  2657. list[index] = 0;
  2658. ddPrintMintermAux(dd,Nnv,list);
  2659. list[index] = 1;
  2660. ddPrintMintermAux(dd,Nv,list);
  2661. list[index] = 2;
  2662. }
  2663. return;
  2664. } /* end of ddPrintMintermAux */
  2665. /**
  2666. @brief Performs the recursive step of Cudd_DagSize.
  2667. @return the number of nodes in the graph rooted at n.
  2668. @sideeffect None
  2669. */
  2670. static int
  2671. ddDagInt(
  2672. DdNode * n)
  2673. {
  2674. int tval, eval;
  2675. if (Cudd_IsComplement(n->next)) {
  2676. return(0);
  2677. }
  2678. n->next = Cudd_Not(n->next);
  2679. if (cuddIsConstant(n)) {
  2680. return(1);
  2681. }
  2682. tval = ddDagInt(cuddT(n));
  2683. eval = ddDagInt(Cudd_Regular(cuddE(n)));
  2684. return(1 + tval + eval);
  2685. } /* end of ddDagInt */
  2686. /**
  2687. @brief Performs the recursive step of cuddNodeArray.
  2688. @details node is supposed to be regular; the invariant is maintained
  2689. by this procedure.
  2690. @return an the number of nodes in the %DD.
  2691. @sideeffect Clears the least significant bit of the next field that
  2692. was used as visited flag by cuddNodeArrayRecur when counting the
  2693. nodes.
  2694. */
  2695. static int
  2696. cuddNodeArrayRecur(
  2697. DdNode *f,
  2698. DdNodePtr *table,
  2699. int index)
  2700. {
  2701. int tindex, eindex;
  2702. if (!Cudd_IsComplement(f->next)) {
  2703. return(index);
  2704. }
  2705. /* Clear visited flag. */
  2706. f->next = Cudd_Regular(f->next);
  2707. if (cuddIsConstant(f)) {
  2708. table[index] = f;
  2709. return(index + 1);
  2710. }
  2711. tindex = cuddNodeArrayRecur(cuddT(f), table, index);
  2712. eindex = cuddNodeArrayRecur(Cudd_Regular(cuddE(f)), table, tindex);
  2713. table[eindex] = f;
  2714. return(eindex + 1);
  2715. } /* end of cuddNodeArrayRecur */
  2716. /**
  2717. @brief Performs the recursive step of Cudd_CofactorEstimate.
  2718. @details Uses the least significant bit of the next field as visited
  2719. flag. node is supposed to be regular; the invariant is maintained by
  2720. this procedure.
  2721. @return an estimate of the number of nodes in the %DD of a cofactor
  2722. of node.
  2723. @sideeffect None
  2724. */
  2725. static int
  2726. cuddEstimateCofactor(
  2727. DdManager *dd,
  2728. st_table *table,
  2729. DdNode * node,
  2730. int i,
  2731. int phase,
  2732. DdNode ** ptr)
  2733. {
  2734. int tval, eval, val;
  2735. DdNode *ptrT, *ptrE;
  2736. #ifdef DD_DEBUG
  2737. assert(!Cudd_IsComplement(node));
  2738. #endif
  2739. if (Cudd_IsComplement(node->next)) {
  2740. if (!st_lookup(table, node, (void **)ptr)) {
  2741. if (st_add_direct(table, node, node) == ST_OUT_OF_MEM)
  2742. return(CUDD_OUT_OF_MEM);
  2743. *ptr = node;
  2744. }
  2745. return(0);
  2746. }
  2747. node->next = Cudd_Not(node->next);
  2748. if (cuddIsConstant(node)) {
  2749. *ptr = node;
  2750. if (st_add_direct(table, node, node) == ST_OUT_OF_MEM)
  2751. return(CUDD_OUT_OF_MEM);
  2752. return(1);
  2753. }
  2754. if ((int) node->index == i) {
  2755. if (phase == 1) {
  2756. *ptr = cuddT(node);
  2757. val = ddDagInt(cuddT(node));
  2758. } else {
  2759. *ptr = cuddE(node);
  2760. val = ddDagInt(Cudd_Regular(cuddE(node)));
  2761. }
  2762. if (node->ref > 1) {
  2763. if (st_add_direct(table,node,*ptr) == ST_OUT_OF_MEM)
  2764. return(CUDD_OUT_OF_MEM);
  2765. }
  2766. return(val);
  2767. }
  2768. if (dd->perm[node->index] > dd->perm[i]) {
  2769. *ptr = node;
  2770. if (node->ref > 1) {
  2771. if (st_add_direct(table,node,node) == ST_OUT_OF_MEM)
  2772. return(CUDD_OUT_OF_MEM);
  2773. }
  2774. val = 1 + ddDagInt(cuddT(node)) + ddDagInt(Cudd_Regular(cuddE(node)));
  2775. return(val);
  2776. }
  2777. tval = cuddEstimateCofactor(dd,table,cuddT(node),i,phase,&ptrT);
  2778. if (tval == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
  2779. eval = cuddEstimateCofactor(dd,table,Cudd_Regular(cuddE(node)),i,
  2780. phase,&ptrE);
  2781. if (eval == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
  2782. ptrE = Cudd_NotCond(ptrE,Cudd_IsComplement(cuddE(node)));
  2783. if (ptrT == ptrE) { /* recombination */
  2784. *ptr = ptrT;
  2785. val = tval;
  2786. if (node->ref > 1) {
  2787. if (st_add_direct(table,node,*ptr) == ST_OUT_OF_MEM)
  2788. return(CUDD_OUT_OF_MEM);
  2789. }
  2790. } else {
  2791. int complement = Cudd_IsComplement(ptrT);
  2792. if (complement) {
  2793. ptrT = Cudd_Regular(ptrT);
  2794. ptrE = Cudd_Complement(ptrE);
  2795. }
  2796. if ((ptrT != cuddT(node) || ptrE != cuddE(node)) &&
  2797. (*ptr = cuddUniqueLookup(dd,node->index,ptrT,ptrE)) != NULL) {
  2798. if (Cudd_IsComplement((*ptr)->next)) {
  2799. val = 0;
  2800. } else {
  2801. val = 1 + tval + eval;
  2802. }
  2803. if (node->ref > 1) {
  2804. if (st_add_direct(table,node,*ptr) == ST_OUT_OF_MEM)
  2805. return(CUDD_OUT_OF_MEM);
  2806. }
  2807. if (complement) {
  2808. *ptr = Cudd_Complement(*ptr);
  2809. }
  2810. } else {
  2811. *ptr = node;
  2812. val = 1 + tval + eval;
  2813. }
  2814. }
  2815. return(val);
  2816. } /* end of cuddEstimateCofactor */
  2817. /**
  2818. @brief Checks the unique table for the existence of an internal node.
  2819. @return a pointer to the node if it is in the table; NULL otherwise.
  2820. @sideeffect None
  2821. @see cuddUniqueInter
  2822. */
  2823. static DdNode *
  2824. cuddUniqueLookup(
  2825. DdManager * unique,
  2826. int index,
  2827. DdNode * T,
  2828. DdNode * E)
  2829. {
  2830. unsigned int posn;
  2831. int level;
  2832. DdNodePtr *nodelist;
  2833. DdNode *looking;
  2834. DdSubtable *subtable;
  2835. if (index >= unique->size) {
  2836. return(NULL);
  2837. }
  2838. level = unique->perm[index];
  2839. subtable = &(unique->subtables[level]);
  2840. #ifdef DD_DEBUG
  2841. assert(level < cuddI(unique,T->index));
  2842. assert(level < cuddI(unique,Cudd_Regular(E)->index));
  2843. #endif
  2844. posn = ddHash(T, E, subtable->shift);
  2845. nodelist = subtable->nodelist;
  2846. looking = nodelist[posn];
  2847. while (T < cuddT(looking)) {
  2848. looking = Cudd_Regular(looking->next);
  2849. }
  2850. while (T == cuddT(looking) && E < cuddE(looking)) {
  2851. looking = Cudd_Regular(looking->next);
  2852. }
  2853. if (cuddT(looking) == T && cuddE(looking) == E) {
  2854. return(looking);
  2855. }
  2856. return(NULL);
  2857. } /* end of cuddUniqueLookup */
  2858. /**
  2859. @brief Performs the recursive step of Cudd_CofactorEstimateSimple.
  2860. @details Uses the least significant bit of the next field as visited
  2861. flag. node is supposed to be regular; the invariant is maintained by
  2862. this procedure.
  2863. @return an estimate of the number of nodes in the %DD of the positive
  2864. cofactor of node.
  2865. @sideeffect None
  2866. */
  2867. static int
  2868. cuddEstimateCofactorSimple(
  2869. DdNode * node,
  2870. int i)
  2871. {
  2872. int tval, eval;
  2873. if (Cudd_IsComplement(node->next)) {
  2874. return(0);
  2875. }
  2876. node->next = Cudd_Not(node->next);
  2877. if (cuddIsConstant(node)) {
  2878. return(1);
  2879. }
  2880. tval = cuddEstimateCofactorSimple(cuddT(node),i);
  2881. if ((int) node->index == i) return(tval);
  2882. eval = cuddEstimateCofactorSimple(Cudd_Regular(cuddE(node)),i);
  2883. return(1 + tval + eval);
  2884. } /* end of cuddEstimateCofactorSimple */
  2885. /**
  2886. @brief Performs the recursive step of Cudd_CountMinterm.
  2887. @details It is based on the following identity. Let |f| be the
  2888. number of minterms of f. Then:
  2889. |f| = (|f0|+|f1|)/2
  2890. where f0 and f1 are the two cofactors of f. Does not use the
  2891. identity |f'| = max - |f|, to minimize loss of accuracy due to
  2892. roundoff.
  2893. @return the number of minterms of the function rooted at node.
  2894. @sideeffect None
  2895. */
  2896. static double
  2897. ddCountMintermAux(
  2898. DdManager * dd,
  2899. DdNode * node,
  2900. double max,
  2901. DdHashTable * table)
  2902. {
  2903. DdNode *N, *Nt, *Ne;
  2904. double min, minT, minE;
  2905. DdNode *res;
  2906. N = Cudd_Regular(node);
  2907. if (cuddIsConstant(N)) {
  2908. if (node == dd->background || node == Cudd_Not(dd->one)) {
  2909. return(0.0);
  2910. } else {
  2911. return(max);
  2912. }
  2913. }
  2914. if (N->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
  2915. min = cuddV(res);
  2916. if (res->ref == 0) {
  2917. table->manager->dead++;
  2918. table->manager->constants.dead++;
  2919. }
  2920. return(min);
  2921. }
  2922. Nt = cuddT(N); Ne = cuddE(N);
  2923. if (Cudd_IsComplement(node)) {
  2924. Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
  2925. }
  2926. minT = ddCountMintermAux(dd,Nt,max,table);
  2927. if (minT == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
  2928. minT *= 0.5;
  2929. minE = ddCountMintermAux(dd,Ne,max,table);
  2930. if (minE == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
  2931. minE *= 0.5;
  2932. min = minT + minE;
  2933. if (N->ref != 1) {
  2934. ptrint fanout = (ptrint) N->ref;
  2935. cuddSatDec(fanout);
  2936. res = cuddUniqueConst(table->manager,min);
  2937. if (!res) {
  2938. return((double)CUDD_OUT_OF_MEM);
  2939. }
  2940. if (!cuddHashTableInsert1(table,node,res,fanout)) {
  2941. cuddRef(res); Cudd_RecursiveDeref(table->manager, res);
  2942. return((double)CUDD_OUT_OF_MEM);
  2943. }
  2944. }
  2945. return(min);
  2946. } /* end of ddCountMintermAux */
  2947. /**
  2948. @brief Performs the recursive step of Cudd_CountPath.
  2949. @details It is based on the following identity. Let |f| be the
  2950. number of paths of f. Then:
  2951. |f| = |f0|+|f1|
  2952. where f0 and f1 are the two cofactors of f. Uses the
  2953. identity |f'| = |f|, to improve the utilization of the (local) cache.
  2954. @return the number of paths of the function rooted at node.
  2955. @sideeffect None
  2956. */
  2957. static double
  2958. ddCountPathAux(
  2959. DdNode * node,
  2960. st_table * table)
  2961. {
  2962. DdNode *Nv, *Nnv;
  2963. double paths, *ppaths, paths1, paths2;
  2964. void *dummy;
  2965. if (cuddIsConstant(node)) {
  2966. return(1.0);
  2967. }
  2968. if (st_lookup(table, node, &dummy)) {
  2969. paths = *(double *) dummy;
  2970. return(paths);
  2971. }
  2972. Nv = cuddT(node); Nnv = cuddE(node);
  2973. paths1 = ddCountPathAux(Nv,table);
  2974. if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
  2975. paths2 = ddCountPathAux(Cudd_Regular(Nnv),table);
  2976. if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
  2977. paths = paths1 + paths2;
  2978. ppaths = ALLOC(double,1);
  2979. if (ppaths == NULL) {
  2980. return((double)CUDD_OUT_OF_MEM);
  2981. }
  2982. *ppaths = paths;
  2983. if (st_add_direct(table, node, ppaths) == ST_OUT_OF_MEM) {
  2984. FREE(ppaths);
  2985. return((double)CUDD_OUT_OF_MEM);
  2986. }
  2987. return(paths);
  2988. } /* end of ddCountPathAux */
  2989. /**
  2990. @brief Performs the recursive step of Cudd_EpdCountMinterm.
  2991. @details It is based on the following identity. Let |f| be the
  2992. number of minterms of f. Then:
  2993. |f| = (|f0|+|f1|)/2
  2994. where f0 and f1 are the two cofactors of f. Does not use the
  2995. identity |f'| = max - |f|, to minimize loss of accuracy due to
  2996. roundoff.
  2997. @return the number of minterms of the function rooted at node.
  2998. @sideeffect None
  2999. */
  3000. static int
  3001. ddEpdCountMintermAux(
  3002. DdManager const * dd,
  3003. DdNode * node,
  3004. EpDouble * max,
  3005. EpDouble * epd,
  3006. st_table * table)
  3007. {
  3008. DdNode *Nt, *Ne;
  3009. EpDouble *min, minT, minE;
  3010. EpDouble *res;
  3011. int status;
  3012. /* node is assumed to be regular */
  3013. if (cuddIsConstant(node)) {
  3014. if (node == dd->background) {
  3015. EpdMakeZero(epd, 0);
  3016. } else {
  3017. EpdCopy(max, epd);
  3018. }
  3019. return(0);
  3020. }
  3021. if (node->ref != 1 && st_lookup(table, node, (void **) &res)) {
  3022. EpdCopy(res, epd);
  3023. return(0);
  3024. }
  3025. Nt = cuddT(node); Ne = cuddE(node);
  3026. status = ddEpdCountMintermAux(dd,Nt,max,&minT,table);
  3027. if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
  3028. EpdMultiply(&minT, (double)0.5);
  3029. status = ddEpdCountMintermAux(dd,Cudd_Regular(Ne),max,&minE,table);
  3030. if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
  3031. if (Cudd_IsComplement(Ne)) {
  3032. EpdSubtract3(max, &minE, epd);
  3033. EpdCopy(epd, &minE);
  3034. }
  3035. EpdMultiply(&minE, (double)0.5);
  3036. EpdAdd3(&minT, &minE, epd);
  3037. if (node->ref > 1) {
  3038. min = EpdAlloc();
  3039. if (!min)
  3040. return(CUDD_OUT_OF_MEM);
  3041. EpdCopy(epd, min);
  3042. if (st_insert(table, node, min) == ST_OUT_OF_MEM) {
  3043. EpdFree(min);
  3044. return(CUDD_OUT_OF_MEM);
  3045. }
  3046. }
  3047. return(0);
  3048. } /* end of ddEpdCountMintermAux */
  3049. /**
  3050. @brief Performs the recursive step of Cudd_LdblCountMinterm.
  3051. @details It is based on the following identity. Let |f| be the
  3052. number of minterms of f. Then:
  3053. |f| = (|f0|+|f1|)/2
  3054. where f0 and f1 are the two cofactors of f. Does not use the
  3055. identity |f'| = max - |f|, to minimize loss of accuracy due to
  3056. roundoff.
  3057. @return the number of minterms of the function rooted at node.
  3058. @sideeffect None
  3059. */
  3060. static long double
  3061. ddLdblCountMintermAux(
  3062. DdManager const *manager,
  3063. DdNode *node,
  3064. long double max,
  3065. st_table *table)
  3066. {
  3067. DdNode *t, *e;
  3068. long double min, minT, minE;
  3069. long double *res;
  3070. if (cuddIsConstant(node)) {
  3071. if (node == manager->background) {
  3072. return 0.0L;
  3073. } else {
  3074. return max;
  3075. }
  3076. }
  3077. if (node->ref != 1 && st_lookup(table, node, (void **) &res)) {
  3078. return *res;
  3079. }
  3080. t = cuddT(node); e = cuddE(node);
  3081. minT = ddLdblCountMintermAux(manager, t, max, table);
  3082. if (minT == (long double) CUDD_OUT_OF_MEM)
  3083. return((long double) CUDD_OUT_OF_MEM);
  3084. minT *= 0.5L;
  3085. minE = ddLdblCountMintermAux(manager, Cudd_Regular(e), max, table);
  3086. if (minE == (long double) CUDD_OUT_OF_MEM)
  3087. return((long double) CUDD_OUT_OF_MEM);
  3088. if (Cudd_IsComplement(e)) {
  3089. minE = max - minE;
  3090. }
  3091. minE *= 0.5L;
  3092. min = minT + minE;
  3093. if (node->ref != 1) {
  3094. res = ALLOC(long double, 1);
  3095. if (res == NULL)
  3096. return((long double) CUDD_OUT_OF_MEM);
  3097. *res = min;
  3098. if (st_insert(table, node, res) == ST_OUT_OF_MEM) {
  3099. FREE(res);
  3100. return((long double) CUDD_OUT_OF_MEM);
  3101. }
  3102. }
  3103. return(min);
  3104. } /* end of ddLdblCountMintermAux */
  3105. /**
  3106. @brief Performs the recursive step of Cudd_CountPathsToNonZero.
  3107. @details It is based on the following identity. Let |f| be the
  3108. number of paths of f. Then:
  3109. |f| = |f0|+|f1|
  3110. where f0 and f1 are the two cofactors of f.
  3111. @return the number of paths of the function rooted at node.
  3112. @sideeffect None
  3113. */
  3114. static double
  3115. ddCountPathsToNonZero(
  3116. DdNode * N,
  3117. st_table * table)
  3118. {
  3119. DdNode *node, *Nt, *Ne;
  3120. double paths, *ppaths, paths1, paths2;
  3121. void *dummy;
  3122. node = Cudd_Regular(N);
  3123. if (cuddIsConstant(node)) {
  3124. return((double) !(Cudd_IsComplement(N) || cuddV(node)==DD_ZERO_VAL));
  3125. }
  3126. if (st_lookup(table, N, &dummy)) {
  3127. paths = *(double *) dummy;
  3128. return(paths);
  3129. }
  3130. Nt = cuddT(node); Ne = cuddE(node);
  3131. if (node != N) {
  3132. Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
  3133. }
  3134. paths1 = ddCountPathsToNonZero(Nt,table);
  3135. if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
  3136. paths2 = ddCountPathsToNonZero(Ne,table);
  3137. if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
  3138. paths = paths1 + paths2;
  3139. ppaths = ALLOC(double,1);
  3140. if (ppaths == NULL) {
  3141. return((double)CUDD_OUT_OF_MEM);
  3142. }
  3143. *ppaths = paths;
  3144. if (st_add_direct(table, N, ppaths) == ST_OUT_OF_MEM) {
  3145. FREE(ppaths);
  3146. return((double)CUDD_OUT_OF_MEM);
  3147. }
  3148. return(paths);
  3149. } /* end of ddCountPathsToNonZero */
  3150. /**
  3151. @brief Performs the recursive step of Cudd_Support.
  3152. @details Performs a DFS from f. The support is accumulated in supp
  3153. as a side effect. Uses the LSB of the then pointer as visited flag.
  3154. @sideeffect None
  3155. @see ddClearFlag
  3156. */
  3157. static void
  3158. ddSupportStep(
  3159. DdNode * f,
  3160. int * support)
  3161. {
  3162. if (cuddIsConstant(f) || Cudd_IsComplement(f->next))
  3163. return;
  3164. support[f->index] = 1;
  3165. ddSupportStep(cuddT(f),support);
  3166. ddSupportStep(Cudd_Regular(cuddE(f)),support);
  3167. /* Mark as visited. */
  3168. f->next = Cudd_Complement(f->next);
  3169. } /* end of ddSupportStep */
  3170. /**
  3171. @brief Performs a DFS from f, clearing the LSB of the next pointers.
  3172. @sideeffect None
  3173. @see ddSupportStep ddFindSupport ddLeavesInt ddDagInt
  3174. */
  3175. static void
  3176. ddClearFlag(
  3177. DdNode * f)
  3178. {
  3179. if (!Cudd_IsComplement(f->next)) {
  3180. return;
  3181. }
  3182. /* Clear visited flag. */
  3183. f->next = Cudd_Regular(f->next);
  3184. if (cuddIsConstant(f)) {
  3185. return;
  3186. }
  3187. ddClearFlag(cuddT(f));
  3188. ddClearFlag(Cudd_Regular(cuddE(f)));
  3189. return;
  3190. } /* end of ddClearFlag */
  3191. /**
  3192. @brief Performs the recursive step of Cudd_CountLeaves.
  3193. @return the number of leaves in the %DD rooted at n.
  3194. @sideeffect None
  3195. @see Cudd_CountLeaves
  3196. */
  3197. static int
  3198. ddLeavesInt(
  3199. DdNode * n)
  3200. {
  3201. int tval, eval;
  3202. if (Cudd_IsComplement(n->next)) {
  3203. return(0);
  3204. }
  3205. n->next = Cudd_Not(n->next);
  3206. if (cuddIsConstant(n)) {
  3207. return(1);
  3208. }
  3209. tval = ddLeavesInt(cuddT(n));
  3210. eval = ddLeavesInt(Cudd_Regular(cuddE(n)));
  3211. return(tval + eval);
  3212. } /* end of ddLeavesInt */
  3213. /**
  3214. @brief Performs the recursive step of Cudd_bddPickArbitraryMinterms.
  3215. @return 1 if successful; 0 otherwise.
  3216. @sideeffect none
  3217. @see Cudd_bddPickArbitraryMinterms
  3218. */
  3219. static int
  3220. ddPickArbitraryMinterms(
  3221. DdManager *dd,
  3222. DdNode *node,
  3223. int nvars,
  3224. int nminterms,
  3225. char **string)
  3226. {
  3227. DdNode *N, *T, *E;
  3228. DdNode *one, *bzero;
  3229. int i, t, result;
  3230. double min1, min2;
  3231. if (string == NULL || node == NULL) return(0);
  3232. /* The constant 0 function has no on-set cubes. */
  3233. one = DD_ONE(dd);
  3234. bzero = Cudd_Not(one);
  3235. if (nminterms == 0 || node == bzero) return(1);
  3236. if (node == one) {
  3237. return(1);
  3238. }
  3239. N = Cudd_Regular(node);
  3240. T = cuddT(N); E = cuddE(N);
  3241. if (Cudd_IsComplement(node)) {
  3242. T = Cudd_Not(T); E = Cudd_Not(E);
  3243. }
  3244. min1 = Cudd_CountMinterm(dd, T, nvars) / 2.0;
  3245. if (min1 == (double)CUDD_OUT_OF_MEM) return(0);
  3246. min2 = Cudd_CountMinterm(dd, E, nvars) / 2.0;
  3247. if (min2 == (double)CUDD_OUT_OF_MEM) return(0);
  3248. t = (int)((double)nminterms * min1 / (min1 + min2) + 0.5);
  3249. for (i = 0; i < t; i++)
  3250. string[i][N->index] = '1';
  3251. for (i = t; i < nminterms; i++)
  3252. string[i][N->index] = '0';
  3253. result = ddPickArbitraryMinterms(dd,T,nvars,t,&string[0]);
  3254. if (result == 0)
  3255. return(0);
  3256. result = ddPickArbitraryMinterms(dd,E,nvars,nminterms-t,&string[t]);
  3257. return(result);
  3258. } /* end of ddPickArbitraryMinterms */
  3259. /**
  3260. @brief Finds a representative cube of a %BDD.
  3261. @details Finds a representative cube of a %BDD with the weight of
  3262. each variable. From the top variable, if the weight is greater than or
  3263. equal to 0.0, choose THEN branch unless the child is the constant 0.
  3264. Otherwise, choose ELSE branch unless the child is the constant 0.
  3265. @sideeffect Cudd_SubsetWithMaskVars Cudd_bddPickOneCube
  3266. */
  3267. static int
  3268. ddPickRepresentativeCube(
  3269. DdManager *dd,
  3270. DdNode *node,
  3271. double *weight,
  3272. char *string)
  3273. {
  3274. DdNode *N, *T, *E;
  3275. DdNode *one, *bzero;
  3276. if (string == NULL || node == NULL) return(0);
  3277. /* The constant 0 function has no on-set cubes. */
  3278. one = DD_ONE(dd);
  3279. bzero = Cudd_Not(one);
  3280. if (node == bzero) return(0);
  3281. if (node == DD_ONE(dd)) return(1);
  3282. for (;;) {
  3283. N = Cudd_Regular(node);
  3284. if (N == one)
  3285. break;
  3286. T = cuddT(N);
  3287. E = cuddE(N);
  3288. if (Cudd_IsComplement(node)) {
  3289. T = Cudd_Not(T);
  3290. E = Cudd_Not(E);
  3291. }
  3292. if (weight[N->index] >= 0.0) {
  3293. if (T == bzero) {
  3294. node = E;
  3295. string[N->index] = '0';
  3296. } else {
  3297. node = T;
  3298. string[N->index] = '1';
  3299. }
  3300. } else {
  3301. if (E == bzero) {
  3302. node = T;
  3303. string[N->index] = '1';
  3304. } else {
  3305. node = E;
  3306. string[N->index] = '0';
  3307. }
  3308. }
  3309. }
  3310. return(1);
  3311. } /* end of ddPickRepresentativeCube */
  3312. /**
  3313. @brief Frees the memory used to store the minterm counts recorded
  3314. in the visited table.
  3315. @return ST_CONTINUE.
  3316. @sideeffect None
  3317. */
  3318. static enum st_retval
  3319. ddEpdFree(
  3320. void * key,
  3321. void * value,
  3322. void * arg)
  3323. {
  3324. EpDouble *epd = (EpDouble *) value;
  3325. (void) key; /* avoid warning */
  3326. (void) arg; /* avoid warning */
  3327. EpdFree(epd);
  3328. return(ST_CONTINUE);
  3329. } /* end of ddEpdFree */
  3330. /**
  3331. @brief Recursively find the support of f.
  3332. @details This function uses the LSB of the next field of the nodes
  3333. of f as visited flag. It also uses the LSB of the next field of the
  3334. variables as flag to remember whether a certain index has already
  3335. been seen. Finally, it uses the manager stack to record all seen
  3336. indices.
  3337. @sideeffect The stack pointer SP is modified by side-effect. The next
  3338. fields are changed and need to be reset.
  3339. */
  3340. static void
  3341. ddFindSupport(
  3342. DdManager *dd,
  3343. DdNode *f,
  3344. int *SP)
  3345. {
  3346. unsigned int index;
  3347. DdNode *var;
  3348. if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) {
  3349. return;
  3350. }
  3351. index = f->index;
  3352. var = dd->vars[index];
  3353. /* It is possible that var is embedded in f. That causes no problem,
  3354. ** though, because if we see it after encountering another node with
  3355. ** the same index, nothing is supposed to happen.
  3356. */
  3357. if (!Cudd_IsComplement(var->next)) {
  3358. var->next = Cudd_Complement(var->next);
  3359. dd->stack[*SP] = (DdNode *)(ptruint) index;
  3360. (*SP)++;
  3361. }
  3362. ddFindSupport(dd, cuddT(f), SP);
  3363. ddFindSupport(dd, Cudd_Regular(cuddE(f)), SP);
  3364. /* Mark as visited. */
  3365. f->next = Cudd_Complement(f->next);
  3366. } /* end of ddFindSupport */
  3367. /**
  3368. @brief Clears visited flags for variables.
  3369. @sideeffect None
  3370. */
  3371. static void
  3372. ddClearVars(
  3373. DdManager *dd,
  3374. int SP)
  3375. {
  3376. int i;
  3377. for (i = 0; i < SP; i++) {
  3378. int index = (int) (ptrint) dd->stack[i];
  3379. DdNode *var = dd->vars[index];
  3380. var->next = Cudd_Regular(var->next);
  3381. }
  3382. } /* end of ddClearVars */
  3383. /**
  3384. @brief Compares indices for qsort.
  3385. @details Subtracting these integers cannot produce overflow, because
  3386. they are non-negative.
  3387. @sideeffect None
  3388. */
  3389. static int
  3390. indexCompare(
  3391. const void *a,
  3392. const void *b)
  3393. {
  3394. int ia = *(int const *) a;
  3395. int ib = *(int const *) b;
  3396. return(ia - ib);
  3397. } /* end of indexCompare */
  3398. /**
  3399. @brief Frees the memory used to store the minterm counts recorded in the
  3400. visited table by Cudd_LdblCountMinterm.
  3401. @returns ST_CONTINUE.
  3402. @sideeffect None
  3403. */
  3404. static enum st_retval
  3405. ddLdblFree(
  3406. void * key,
  3407. void * value,
  3408. void * arg)
  3409. {
  3410. long double * ld = (long double *) value;
  3411. (void) key; /* avoid warning */
  3412. (void) arg; /* avoid warning */
  3413. FREE(ld);
  3414. return(ST_CONTINUE);
  3415. } /* end of ddLdblFree */
  3416. #if HAVE_POWL != 1
  3417. /**
  3418. @brief Replacement for standard library powl.
  3419. @details Some systems' C libraries, notably Cygwin as of 2015,
  3420. lack an implementation of powl. This simple-minded replacement
  3421. works for integral powers. It is based on iterative squaring.
  3422. @return base raised to the exponent.
  3423. */
  3424. static long double
  3425. powl(
  3426. long double base,
  3427. long double exponent)
  3428. {
  3429. long exp;
  3430. long double power = 1.0L, square = base;
  3431. if (exponent < 0.0L) {
  3432. exp = (long) -exponent;
  3433. } else {
  3434. exp = (long) exponent;
  3435. }
  3436. /* Compute base^exponent by iterative squaring.
  3437. * The loop invariant is power * square^exp = base^exponent.
  3438. */
  3439. while (exp > 0) {
  3440. if (exp & 1L)
  3441. power *= square;
  3442. square *= square;
  3443. exp >>= 1L;
  3444. }
  3445. if (exponent < 0.0L) {
  3446. power = 1.0L / power;
  3447. }
  3448. return(power);
  3449. } /* end of powl */
  3450. #endif