| blob | ed2567e997466df2d04dd329e5974eb6c38521e1 |
1 <HTML>
3 <BODY>
5 <DL>
6 <dt><pre>
8 int <I></I>
13 )
14 </pre>
15 <dd> Adds a function to a hook. A hook is a list of
16 application-provided functions called on certain occasions by the
18 function was already in the list; 0 otherwise.
19 <p>
22 <p>
25 </code>
27 <dt><pre>
29 DdApaDigit <I></I>
35 )
36 </pre>
37 <dd> Adds two arbitrary precision integers. Returns the
38 carry out of the most significant digit.
39 <p>
42 <p>
44 <dt><pre>
46 int <I></I>
54 )
55 </pre>
56 <dd> Compares the ratios of two arbitrary precision integers
58 they are equal; -1 if the second number is larger.
59 <p>
62 <p>
64 <dt><pre>
66 int <I></I>
72 )
73 </pre>
76 number is larger.
77 <p>
80 <p>
82 <dt><pre>
84 void <I></I>
89 )
90 </pre>
91 <dd> Makes a copy of an arbitrary precision integer.
92 <p>
95 <p>
97 <dt><pre>
99 DdApaNumber <I></I>
105 )
106 </pre>
107 <dd> Counts the number of minterms of a DD. The function is
108 assumed to depend on nvars variables. The minterm count is
109 represented as an arbitrary precision unsigned integer, to allow for
110 any number of variables CUDD supports. Returns a pointer to the
111 array representing the number of minterms of the function rooted at
112 node if successful; NULL otherwise.
113 <p>
117 <p>
120 </code>
122 <dt><pre>
124 unsigned int <I></I>
130 )
131 </pre>
133 unsigned integer. Returns the remainder of the division. This
134 procedure relies on the assumption that the number of bits of a
135 DdApaDigit plus the number of bits of an unsigned int is less the
136 number of bits of the mantissa of a double. This guarantees that the
137 product of a DdApaDigit and an unsigned int can be represented
138 without loss of precision by a double. On machines where this
139 assumption is not satisfied, this procedure will malfunction.
140 <p>
143 <p>
146 </code>
148 <dt><pre>
150 int <I></I>
153 )
154 </pre>
155 <dd> Finds the number of digits for an arbitrary precision
156 integer given the maximum number of binary digits. The number of
157 binary digits should be positive. Returns the number of digits if
158 successful; 0 otherwise.
159 <p>
162 <p>
164 <dt><pre>
166 void <I></I>
171 )
172 </pre>
173 <dd> Sets an arbitrary precision integer to a power of
174 two. If the power of two is too large to be represented, the number
175 is set to 0.
176 <p>
179 <p>
181 <dt><pre>
183 int <I></I>
188 )
189 </pre>
190 <dd> Prints an arbitrary precision integer in decimal format.
192 <p>
195 <p>
199 </code>
201 <dt><pre>
203 int <I></I>
209 )
210 </pre>
211 <dd> Prints the density of a BDD or ADD using
213 <p>
216 <p>
218 <dt><pre>
220 int <I></I>
226 )
227 </pre>
228 <dd> Prints an arbitrary precision integer in exponential format.
230 <p>
233 <p>
237 </code>
239 <dt><pre>
241 int <I></I>
246 )
247 </pre>
248 <dd> Prints an arbitrary precision integer in hexadecimal format.
250 <p>
253 <p>
257 </code>
259 <dt><pre>
261 int <I></I>
268 )
269 </pre>
270 <dd> Prints the number of minterms of a BDD or ADD in
271 exponential format using arbitrary precision arithmetic. Parameter
272 precision controls the number of signficant digits printed. Returns
274 <p>
277 <p>
280 </code>
282 <dt><pre>
284 int <I></I>
290 )
291 </pre>
292 <dd> Prints the number of minterms of a BDD or ADD using
294 <p>
297 <p>
300 </code>
302 <dt><pre>
304 void <I></I>
309 )
310 </pre>
311 <dd> Sets an arbitrary precision integer to a one-digit literal.
312 <p>
315 <p>
317 <dt><pre>
319 void <I></I>
325 )
326 </pre>
327 <dd> Shifts right an arbitrary precision integer by one
328 binary place. The most significant binary digit of the result is
330 <p>
333 <p>
335 <dt><pre>
337 DdApaDigit <I></I>
343 )
344 </pre>
345 <dd> Divides an arbitrary precision integer by a digit.
346 <p>
349 <p>
351 <dt><pre>
353 DdApaDigit <I></I>
359 )
360 </pre>
361 <dd> Subtracts two arbitrary precision integers. Returns the
362 borrow out of the most significant digit.
363 <p>
367 <p>
369 <dt><pre>
371 void <I></I>
374 )
375 </pre>
376 <dd> Disables automatic dynamic reordering of ZDDs.
377 <p>
380 <p>
385 </code>
387 <dt><pre>
389 void <I></I>
392 )
393 </pre>
394 <dd> Disables automatic dynamic reordering.
395 <p>
398 <p>
403 </code>
405 <dt><pre>
407 void <I></I>
411 )
412 </pre>
413 <dd> Enables automatic dynamic reordering of ZDDs. Parameter
414 method is used to determine the method used for reordering ZDDs. If
415 CUDD_REORDER_SAME is passed, the method is unchanged.
416 <p>
419 <p>
424 </code>
426 <dt><pre>
428 void <I></I>
432 )
433 </pre>
434 <dd> Enables automatic dynamic reordering of BDDs and
435 ADDs. Parameter method is used to determine the method used for
436 reordering. If CUDD_REORDER_SAME is passed, the method is
437 unchanged.
438 <p>
441 <p>
446 </code>
448 <dt><pre>
450 double <I></I>
453 )
454 </pre>
455 <dd> Computes the average distance between adjacent nodes in
456 the manager. Adjacent nodes are node pairs such that the second node
457 is the then child, else child, or next node in the collision list.
458 <p>
461 <p>
463 <dt><pre>
465 DdNode * <I></I>
469 )
470 </pre>
472 resulting ADD if successful; NULL otherwise.
473 <p>
476 <p>
482 </code>
484 <dt><pre>
486 int <I></I>
491 )
492 </pre>
493 <dd> Builds a positional array from the BDD of a cube.
494 Array must have one entry for each BDD variable. The positional
495 array has 1 in i-th position if the variable of index i appears in
496 true form in the cube; it has 0 in i-th position if the variable of
497 index i appears in complemented form in the cube; finally, it has 2
498 in i-th position if the variable of index i does not appear in the
500 otherwise.
501 <p>
504 <p>
507 </code>
509 <dt><pre>
511 DdNode * <I></I>
520 )
521 </pre>
522 <dd> Extracts a dense superset from a BDD. The procedure is
523 identical to the underapproximation procedure except for the fact that it
524 works on the complement of the given function. Extracting the subset
525 of the complement function is equivalent to extracting the superset
526 of the function.
527 Returns a pointer to the BDD of the superset if successful. NULL if
528 intermediate result causes the procedure to run out of memory. The
529 parameter numVars is the maximum number of variables to be used in
530 minterm calculation. The optimal number
531 should be as close as possible to the size of the support of f.
532 However, it is safe to pass the value returned by Cudd_ReadSize for
533 numVars when the number of variables is under 1023. If numVars is
535 the procedure will compute a value which will avoid overflow but
536 will cause underflow with 2046 variables or more.
537 <p>
540 <p>
547 </code>
549 <dt><pre>
551 DdNode * <I></I>
560 )
561 </pre>
562 <dd> Extracts a dense subset from a BDD. This procedure uses
563 a biased remapping technique and density as the cost function. The bias
564 is a function. This procedure tries to approximate where the bias is 0
565 and preserve the given function where the bias is 1.
566 Returns a pointer to the BDD of the subset if
567 successful. NULL if the procedure runs out of memory. The parameter
568 numVars is the maximum number of variables to be used in minterm
569 calculation. The optimal number should be as close as possible to
570 the size of the support of f. However, it is safe to pass the value
571 returned by Cudd_ReadSize for numVars when the number of variables
573 overflow. If a 0 parameter is passed then the procedure will compute
574 a value which will avoid overflow but will cause underflow with 2046
575 variables or more.
576 <p>
579 <p>
586 </code>
588 <dt><pre>
590 DdNode * <I></I>
595 )
596 </pre>
597 <dd> Computes the compatible projection of relation R with
598 respect to cube Y. Returns a pointer to the c-projection if
599 successful; NULL otherwise. For a comparison between Cudd_CProjection
600 and Cudd_PrioritySelect, see the documentation of the latter.
601 <p>
604 <p>
607 </code>
609 <dt><pre>
611 int <I></I>
614 )
615 </pre>
616 <dd> Checks for the following conditions:
617 <ul>
618 <li>Wrong sizes of subtables.
619 <li>Wrong number of keys found in unique subtable.
620 <li>Wrong number of dead found in unique subtable.
621 <li>Wrong number of keys found in the constant table
622 <li>Wrong number of dead found in the constant table
623 <li>Wrong number of total slots found
624 <li>Wrong number of maximum keys found
625 <li>Wrong number of total dead found
626 </ul>
627 Reports the average length of non-empty lists. Returns the number of
628 subtables for which the number of keys is wrong.
629 <p>
632 <p>
635 </code>
637 <dt><pre>
639 int <I></I>
642 )
643 </pre>
644 <dd> Checks the unique table for nodes with non-zero
645 reference counts. It is normally called before Cudd_Quit to make sure
646 that there are no memory leaks due to missing Cudd_RecursiveDeref's.
647 Takes into account that reference counts may saturate and that the
648 basic constants and the projection functions are referenced by the
649 manager. Returns the number of nodes with non-zero reference count.
650 (Except for the cases mentioned above.)
651 <p>
654 <p>
656 <dt><pre>
658 int <I></I>
666 )
667 </pre>
668 <dd> Classifies the variables in the support of two DDs
672 <p>
675 returned as side effects.
676 <p>
680 </code>
682 <dt><pre>
684 void <I></I>
687 )
688 </pre>
689 <dd> Clear the error code of a manager.
690 <p>
693 <p>
696 </code>
698 <dt><pre>
700 double * <I></I>
704 )
705 </pre>
706 <dd> Computes the fraction of minterms in the on-set of all
707 the positive cofactors of DD. Returns the pointer to an array of
708 doubles if successful; NULL otherwise. The array has as many
709 positions as there are BDD variables in the manager plus one. The
710 last position of the array contains the fraction of the minterms in
711 the ON-set of the function represented by the BDD or ADD. The other
712 positions of the array hold the variable signatures.
713 <p>
716 <p>
718 <dt><pre>
720 DdNode * <I></I>
725 )
726 </pre>
727 <dd> Computes the cofactor of f with respect to g; g must be
728 the BDD or the ADD of a cube. Returns a pointer to the cofactor if
729 successful; NULL otherwise.
730 <p>
733 <p>
737 </code>
739 <dt><pre>
741 int <I></I>
744 )
745 </pre>
746 <dd> Counts the number of leaves in a DD. Returns the number
747 of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM
748 otherwise.
749 <p>
752 <p>
755 </code>
757 <dt><pre>
759 double <I></I>
764 )
765 </pre>
766 <dd> Counts the number of minterms of a DD. The function is
767 assumed to depend on nvars variables. The minterm count is
768 represented as a double, to allow for a larger number of variables.
769 Returns the number of minterms of the function rooted at node if
770 successful; (double) CUDD_OUT_OF_MEM otherwise.
771 <p>
774 <p>
778 </code>
780 <dt><pre>
782 double <I></I>
785 )
786 </pre>
787 <dd> Counts the number of paths to a non-zero terminal of a
788 DD. The path count is
789 represented as a double, to allow for a larger number of variables.
790 Returns the number of paths of the function rooted at node.
791 <p>
794 <p>
798 </code>
800 <dt><pre>
802 double <I></I>
805 )
806 </pre>
807 <dd> Counts the number of paths of a DD. Paths to all
808 terminal nodes are counted. The path count is represented as a
809 double, to allow for a larger number of variables. Returns the
810 number of paths of the function rooted at node if successful;
811 (double) CUDD_OUT_OF_MEM otherwise.
812 <p>
815 <p>
818 </code>
820 <dt><pre>
822 DdNode * <I></I>
826 )
827 </pre>
828 <dd> Builds a cube from a positional array. The array must
829 have one integer entry for each BDD variable. If the i-th entry is
830 1, the variable of index i appears in true form in the cube; If the
831 i-th entry is 0, the variable of index i appears complemented in the
832 cube; otherwise the variable does not appear in the cube. Returns a
833 pointer to the BDD for the cube if successful; NULL otherwise.
834 <p>
837 <p>
842 </code>
844 <dt><pre>
846 int <I></I>
849 )
850 </pre>
851 <dd> Counts the number of nodes in a DD. Returns the number
852 of nodes in the graph rooted at node.
853 <p>
856 <p>
860 </code>
862 <dt><pre>
864 int <I></I>
867 )
868 </pre>
869 <dd> Tells whether dead nodes are counted towards triggering
871 <p>
874 <p>
878 </code>
880 <dt><pre>
882 int <I></I>
885 )
886 </pre>
887 <dd> Checks for inconsistencies in the DD heap:
888 <ul>
889 <li> node has illegal index
890 <li> live node has dead children
891 <li> node has illegal Then or Else pointers
892 <li> BDD/ADD node has identical children
893 <li> ZDD node has zero then child
894 <li> wrong number of total nodes
895 <li> wrong number of dead nodes
896 <li> ref count error at node
897 </ul>
898 Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is
899 not enough memory; 1 otherwise.
900 <p>
903 <p>
906 </code>
908 <dt><pre>
910 DdNode * <I></I>
915 )
916 </pre>
917 <dd> Determines whether the function represented by BDD f is
918 negative unate (monotonic decreasing) in variable i. Returns the
919 constant one is f is unate and the (logical) constant zero if it is not.
920 This function does not generate any new nodes.
921 <p>
924 <p>
927 </code>
929 <dt><pre>
931 void <I></I>
935 )
936 </pre>
937 <dd> Enqueues node n for later dereferencing. If the queue
938 is full decreases the reference count of the oldest node N to make
939 room for n. If N dies, recursively decreases the reference counts of
940 its children. It is used to dispose of a BDD that is currently not
941 needed, but may be useful again in the near future. The dereferencing
942 proper is done as in Cudd_IterDerefBdd.
943 <p>
946 <p>
950 </code>
952 <dt><pre>
954 double <I></I>
959 )
960 </pre>
961 <dd> Computes the density of a BDD or ADD. The density is
962 the ratio of the number of minterms to the number of nodes. If 0 is
963 passed as number of variables, the number of variables existing in
964 the manager is used. Returns the density if successful; (double)
965 CUDD_OUT_OF_MEM otherwise.
966 <p>
969 <p>
973 </code>
975 <dt><pre>
977 void <I></I>
980 )
981 </pre>
982 <dd> Decreases the reference count of node. It is primarily
983 used in recursive procedures to decrease the ref count of a result
984 node before returning it. This accomplishes the goal of removing the
985 protection applied by a previous Cudd_Ref.
986 <p>
989 <p>
994 </code>
996 <dt><pre>
998 void <I></I>
1001 )
1002 </pre>
1003 <dd> Disables garbage collection. Garbage collection is
1004 initially enabled. This function may be called to disable it.
1005 However, garbage collection will still occur when a new node must be
1006 created and no memory is left, or when garbage collection is required
1007 for correctness. (E.g., before reordering.)
1008 <p>
1011 <p>
1013 <dd> <b>See Also</b> <code><a href="#Cudd_EnableGarbageCollection">Cudd_EnableGarbageCollection</a>
1015 </code>
1017 <dt><pre>
1019 int <I></I>
1022 )
1023 </pre>
1024 <dd> Disables reporting of reordering stats.
1026 <p>
1029 hooks.
1030 <p>
1032 <dd> <b>See Also</b> <code><a href="#Cudd_EnableReorderingReporting">Cudd_EnableReorderingReporting</a>
1034 </code>
1036 <dt><pre>
1038 DdNode * <I></I>
1045 )
1046 </pre>
1047 <dd> This function generates a BDD for the function x -y != c.
1050 The BDD is built bottom-up.
1051 It has a linear number of nodes if the variables are ordered as follows:
1053 <p>
1056 <p>
1059 </code>
1061 <dt><pre>
1063 int <I></I>
1072 )
1073 </pre>
1074 <dd> Writes a blif body representing the argument BDDs as a
1075 network of multiplexers. No header (.model, .inputs, and .outputs) and
1076 footer (.end) are produced by this function. One multiplexer is written
1078 out-of-memory, file system full, or an ADD with constants different
1080 caller responsibility. Cudd_DumpBlifBody uses a minimal unique subset of
1081 the hexadecimal address of a node as name for it. If the argument
1082 inames is non-null, it is assumed to hold the pointers to the names
1083 of the inputs. Similarly for onames. This function prints out only
1084 .names part.
1085 <p>
1088 <p>
1096 </code>
1098 <dt><pre>
1100 int <I></I>
1110 )
1111 </pre>
1112 <dd> Writes a blif file representing the argument BDDs as a
1113 network of multiplexers. One multiplexer is written for each BDD
1115 out-of-memory, file system full, or an ADD with constants different
1117 caller responsibility. Cudd_DumpBlif uses a minimal unique subset of
1118 the hexadecimal address of a node as name for it. If the argument
1119 inames is non-null, it is assumed to hold the pointers to the names
1120 of the inputs. Similarly for onames.
1121 <p>
1124 <p>
1132 </code>
1134 <dt><pre>
1136 int <I></I>
1144 )
1145 </pre>
1146 <dd> Writes a DDcal file representing the argument BDDs.
1148 file system full). Cudd_DumpDDcal does not close the file: This
1149 is the caller responsibility. Cudd_DumpDDcal uses a minimal unique
1150 subset of the hexadecimal address of a node as name for it. If the
1151 argument inames is non-null, it is assumed to hold the pointers to
1152 the names of the inputs. Similarly for onames.
1153 <p>
1156 <p>
1163 </code>
1165 <dt><pre>
1167 int <I></I>
1175 )
1176 </pre>
1177 <dd> Writes a daVinci file representing the argument BDDs.
1179 file system full). Cudd_DumpDaVinci does not close the file: This
1180 is the caller responsibility. Cudd_DumpDaVinci uses a minimal unique
1181 subset of the hexadecimal address of a node as name for it. If the
1182 argument inames is non-null, it is assumed to hold the pointers to
1183 the names of the inputs. Similarly for onames.
1184 <p>
1187 <p>
1194 </code>
1196 <dt><pre>
1198 int <I></I>
1206 )
1207 </pre>
1208 <dd> Writes a file representing the argument DDs in a format
1209 suitable for the graph drawing program dot.
1211 file system full).
1212 Cudd_DumpDot does not close the file: This is the caller
1213 responsibility. Cudd_DumpDot uses a minimal unique subset of the
1214 hexadecimal address of a node as name for it.
1215 If the argument inames is non-null, it is assumed to hold the pointers
1216 to the names of the inputs. Similarly for onames.
1217 Cudd_DumpDot uses the following convention to draw arcs:
1218 <ul>
1219 <li> solid line: THEN arcs;
1220 <li> dotted line: complement arcs;
1221 <li> dashed line: regular ELSE arcs.
1222 </ul>
1223 The dot options are chosen so that the drawing fits on a letter-size
1224 sheet.
1225 <p>
1228 <p>
1235 </code>
1237 <dt><pre>
1239 int <I></I>
1247 )
1248 </pre>
1249 <dd> Writes factored forms representing the argument BDDs.
1250 The format of the factored form is the one used in the genlib files
1252 otherwise (e.g., file system full). Cudd_DumpFactoredForm does not
1253 close the file: This is the caller responsibility. Caution must be
1254 exercised because a factored form may be exponentially larger than
1255 the argument BDD. If the argument inames is non-null, it is assumed
1256 to hold the pointers to the names of the inputs. Similarly for
1257 onames.
1258 <p>
1261 <p>
1268 </code>
1270 <dt><pre>
1272 DdNode * <I></I>
1279 )
1280 </pre>
1281 <dd> This function generates a BDD for the function d(x,y)
1282 > d(x,z);
1285 with 0 the most significant bit.
1286 The distance d(x,y) is defined as:
1288 The BDD is built bottom-up.
1291 <p>
1294 <p>
1300 </code>
1302 <dt><pre>
1304 DdNode * <I></I>
1311 )
1312 </pre>
1313 <dd> This function generates a BDD for the function d(x,y)
1314 > d(y,z);
1317 with 0 the most significant bit.
1318 The distance d(x,y) is defined as:
1320 The BDD is built bottom-up.
1323 <p>
1326 <p>
1332 </code>
1334 <dt><pre>
1336 void <I></I>
1339 )
1340 </pre>
1341 <dd> Enables garbage collection. Garbage collection is
1342 initially enabled. Therefore it is necessary to call this function
1343 only if garbage collection has been explicitly disabled.
1344 <p>
1347 <p>
1349 <dd> <b>See Also</b> <code><a href="#Cudd_DisableGarbageCollection">Cudd_DisableGarbageCollection</a>
1351 </code>
1353 <dt><pre>
1355 int <I></I>
1358 )
1359 </pre>
1360 <dd> Enables reporting of reordering stats.
1362 <p>
1365 hooks.
1366 <p>
1368 <dd> <b>See Also</b> <code><a href="#Cudd_DisableReorderingReporting">Cudd_DisableReorderingReporting</a>
1370 </code>
1372 <dt><pre>
1374 int <I></I>
1380 )
1381 </pre>
1382 <dd> Counts the number of minterms of a DD with extended precision.
1383 The function is assumed to depend on nvars variables. The minterm count is
1384 represented as an EpDouble, to allow any number of variables.
1385 Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.
1386 <p>
1389 <p>
1393 </code>
1395 <dt><pre>
1397 int <I></I>
1404 )
1405 </pre>
1406 <dd> Compares two ADDs for equality within tolerance. Two
1407 ADDs are reported to be equal if the maximum difference between them
1408 (the sup norm of their difference) is less than or equal to the
1409 tolerance parameter. Returns 1 if the two ADDs are equal (within
1411 the first failure is reported to the standard output.
1412 <p>
1415 <p>
1417 <dt><pre>
1419 int <I></I>
1425 )
1426 </pre>
1430 otherwise. No new nodes are created.
1431 <p>
1434 <p>
1437 </code>
1439 <dt><pre>
1441 int <I></I>
1445 )
1446 </pre>
1447 <dd> Estimates the number of nodes in a cofactor of a DD.
1448 Returns an estimate of the number of nodes in the positive cofactor of
1449 the graph rooted at node with respect to the variable whose index is i.
1450 This procedure implements with minor changes the algorithm of Cabodi et al.
1451 (ICCAD96). It does not allocate any memory, it does not change the
1452 state of the manager, and it is fast. However, it has been observed to
1453 overestimate the size of the cofactor by as much as a factor of 2.
1454 <p>
1457 <p>
1460 </code>
1462 <dt><pre>
1464 int <I></I>
1470 )
1471 </pre>
1472 <dd> Estimates the number of nodes in a cofactor of a DD.
1473 Returns an estimate of the number of nodes in a cofactor of
1474 the graph rooted at node with respect to the variable whose index is i.
1475 In case of failure, returns CUDD_OUT_OF_MEM.
1476 This function uses a refinement of the algorithm of Cabodi et al.
1477 (ICCAD96). The refinement allows the procedure to account for part
1478 of the recombination that may occur in the part of the cofactor above
1479 the cofactoring variable. This procedure does no create any new node.
1480 It does keep a small table of results; therefore it may run out of memory.
1481 If this is a concern, one should use Cudd_EstimateCofactorSimple, which
1482 is faster, does not allocate any memory, but is less accurate.
1483 <p>
1486 <p>
1490 </code>
1492 <dt><pre>
1494 DdNode * <I></I>
1499 )
1500 </pre>
1501 <dd> Finds the value of a DD for a given variable
1502 assignment. The variable assignment is passed in an array of int's,
1503 that should specify a zero or a one for each variable in the support
1504 of the function. Returns a pointer to a constant node. No new nodes
1505 are produced.
1506 <p>
1509 <p>
1513 </code>
1515 <dt><pre>
1517 double <I></I>
1520 )
1521 </pre>
1522 <dd> Computes the fraction of slots in the unique table that
1523 should be in use. This expected value is based on the assumption
1524 that the hash function distributes the keys randomly; it can be
1525 compared with the result of Cudd_ReadUsedSlots to monitor the
1526 performance of the unique table hash function.
1527 <p>
1530 <p>
1534 </code>
1536 <dt><pre>
1538 DdNode * <I></I>
1542 )
1543 </pre>
1544 <dd> Returns the cube of the essential variables. A positive
1545 literal means that the variable must be set to 1 for the function to be
1547 function to be 1. Returns a pointer to the cube BDD if successful;
1548 NULL otherwise.
1549 <p>
1552 <p>
1555 </code>
1557 <dt><pre>
1559 DdTlcInfo * <I></I>
1563 )
1564 </pre>
1565 <dd> Returns the one- and two-literal clauses of a DD.
1566 Returns a pointer to the structure holding the clauses if
1567 successful; NULL otherwise. For a constant DD, the empty set of clauses
1568 is returned. This is obviously correct for a non-zero constant. For the
1569 constant zero, it is based on the assumption that only those clauses
1570 containing variables in the support of the function are considered. Since
1571 the support of a constant function is empty, no clauses are returned.
1572 <p>
1575 <p>
1578 </code>
1580 <dt><pre>
1582 DdGen * <I></I>
1588 )
1589 </pre>
1590 <dd> Defines an iterator on the onset of a decision diagram
1591 and finds its first cube. Returns a generator that contains the
1592 information necessary to continue the enumeration if successful; NULL
1593 otherwise.<p>
1594 A cube is represented as an array of literals, which are integers in
1596 uncomplemented literal, and 2 stands for don't care. The enumeration
1597 produces a disjoint cover of the function associated with the diagram.
1598 The size of the array equals the number of variables in the manager at
1599 the time Cudd_FirstCube is called.<p>
1600 For each cube, a value is also returned. This value is always 1 for a
1601 BDD, while it may be different from 1 for an ADD.
1602 For BDDs, the offset is the set of cubes whose value is the logical zero.
1603 For ADDs, the offset is the set of cubes whose value is the
1604 background value. The cubes of the offset are not enumerated.
1605 <p>
1608 <p>
1615 </code>
1617 <dt><pre>
1619 DdGen * <I></I>
1624 )
1625 </pre>
1626 <dd> Defines an iterator on the nodes of a decision diagram
1627 and finds its first node. Returns a generator that contains the
1628 information necessary to continue the enumeration if successful;
1629 NULL otherwise. The nodes are enumerated in a reverse topological
1630 order, so that a node is always preceded in the enumeration by its
1631 descendants.
1632 <p>
1635 <p>
1642 </code>
1644 <dt><pre>
1646 DdGen * <I></I>
1652 )
1653 </pre>
1654 <dd> Defines an iterator on a pair of BDDs describing a
1655 (possibly incompletely specified) Boolean functions and finds the
1656 first cube of a cover of the function. Returns a generator
1657 that contains the information necessary to continue the enumeration
1658 if successful; NULL otherwise.<p>
1660 The two argument BDDs are the lower and upper bounds of an interval.
1661 It is a mistake to call this function with a lower bound that is not
1662 less than or equal to the upper bound.<p>
1664 A cube is represented as an array of literals, which are integers in
1666 uncomplemented literal, and 2 stands for don't care. The enumeration
1667 produces a prime and irredundant cover of the function associated
1668 with the two BDDs. The size of the array equals the number of
1669 variables in the manager at the time Cudd_FirstCube is called.<p>
1671 This iterator can only be used on BDDs.
1672 <p>
1675 <p>
1683 </code>
1685 <dt><pre>
1687 void <I></I>
1690 )
1691 </pre>
1692 <dd> Frees the variable group tree of the manager.
1693 <p>
1696 <p>
1701 </code>
1703 <dt><pre>
1705 void <I></I>
1708 )
1709 </pre>
1710 <dd> Frees the variable group tree of the manager.
1711 <p>
1714 <p>
1719 </code>
1721 <dt><pre>
1723 int <I></I>
1726 )
1727 </pre>
1729 <p>
1732 <p>
1734 <dd> <b>See Also</b> <code><a href="#Cudd_EnableGarbageCollection">Cudd_EnableGarbageCollection</a>
1736 </code>
1738 <dt><pre>
1740 int <I></I>
1743 )
1744 </pre>
1746 be used in mis-like foreach constructs.
1747 <p>
1750 <p>
1759 </code>
1761 <dt><pre>
1763 DdNode * <I></I>
1768 )
1769 </pre>
1770 <dd> Determines whether the function represented by BDD f is
1771 positive unate (monotonic increasing) in variable i. It is based on
1772 Cudd_Decreasing and the fact that f is monotonic increasing in i if
1773 and only if its complement is monotonic decreasing in i.
1774 <p>
1777 <p>
1780 </code>
1782 <dt><pre>
1784 DdNode * <I></I>
1789 )
1790 </pre>
1791 <dd> Builds a cube of BDD variables from an array of indices.
1792 Returns a pointer to the result if successful; NULL otherwise.
1793 <p>
1796 <p>
1800 </code>
1802 <dt><pre>
1804 DdNode * <I></I>
1811 )
1812 </pre>
1816 The BDD is built bottom-up.
1817 It has a linear number of nodes if the variables are ordered as follows:
1819 <p>
1822 <p>
1825 </code>
1827 <dt><pre>
1829 DdManager * <I></I>
1836 )
1837 </pre>
1838 <dd> Creates a new DD manager, initializes the table, the
1839 basic constants and the projection functions. If maxMemory is 0,
1840 Cudd_Init decides suitable values for the maximum size of the cache
1841 and for the limit for fast unique table growth based on the available
1842 memory. Returns a pointer to the manager if successful; NULL
1843 otherwise.
1844 <p>
1847 <p>
1850 </code>
1852 <dt><pre>
1854 int <I></I>
1857 )
1858 </pre>
1860 generator is empty or NULL; 0 otherswise.
1861 <p>
1864 <p>
1873 </code>
1875 <dt><pre>
1877 int <I></I>
1882 )
1883 </pre>
1884 <dd> Checks whether a function is in a hook. A hook is a list of
1885 application-provided functions called on certain occasions by the
1887 <p>
1890 <p>
1894 </code>
1896 <dt><pre>
1898 int <I></I>
1901 )
1902 </pre>
1904 useful to test the results of Cudd_bddIteConstant, Cudd_addIteConstant,
1905 Cudd_addEvalConst. These results may be a special value signifying
1906 non-constant. In the other cases the macro Cudd_IsConstant can be used.
1907 <p>
1910 <p>
1916 </code>
1918 <dt><pre>
1920 void <I></I>
1924 )
1925 </pre>
1926 <dd> Decreases the reference count of node n. If n dies,
1927 recursively decreases the reference counts of its children. It is
1928 used to dispose of a BDD that is no longer needed. It is more
1929 efficient than Cudd_RecursiveDeref, but it cannot be used on
1930 ADDs. The greater efficiency comes from being able to assume that no
1931 constant node will ever die as a result of a call to this
1932 procedure.
1933 <p>
1936 <p>
1940 </code>
1942 <dt><pre>
1944 DdNode * <I></I>
1949 )
1950 </pre>
1951 <dd> Finds a largest cube in a DD. f is the DD we want to
1952 get the largest cube for. The problem is translated into the one of
1953 finding a shortest path in f, when both THEN and ELSE arcs are assumed to
1954 have unit length. This yields a largest cube in the disjoint cover
1955 corresponding to the DD. Therefore, it is not necessarily the largest
1956 implicant of f. Returns the largest cube as a BDD.
1957 <p>
1960 <p>
1963 </code>
1965 <dt><pre>
1967 DdNode * <I></I>
1971 )
1972 </pre>
1973 <dd> Converts a ZDD cover to a BDD graph. If successful, it
1974 returns a BDD node, otherwise it returns NULL.
1975 <p>
1978 </code>
1980 <dt><pre>
1982 MtrNode * <I></I>
1988 )
1989 </pre>
1990 <dd> Creates a new variable group. The group starts at
1991 variable and contains size variables. The parameter low is the index
1992 of the first variable. If the variable already exists, its current
1993 position in the order is known to the manager. If the variable does
1994 not exist yet, the position is assumed to be the same as the index.
1995 The group tree is created if it does not exist yet.
1996 Returns a pointer to the group if successful; NULL otherwise.
1997 <p>
2000 <p>
2003 </code>
2005 <dt><pre>
2007 MtrNode * <I></I>
2013 )
2014 </pre>
2015 <dd> Creates a new ZDD variable group. The group starts at
2016 variable and contains size variables. The parameter low is the index
2017 of the first variable. If the variable already exists, its current
2018 position in the order is known to the manager. If the variable does
2019 not exist yet, the position is assumed to be the same as the index.
2020 The group tree is created if it does not exist yet.
2021 Returns a pointer to the group if successful; NULL otherwise.
2022 <p>
2025 <p>
2028 </code>
2030 <dt><pre>
2032 int <I></I>
2038 )
2039 </pre>
2040 <dd> Returns the minimum Hamming distance between the
2041 minterms of a function f and a reference minterm. The function is
2042 given as a BDD; the minterm is given as an array of integers, one
2043 for each variable in the manager. Returns the minimum distance if
2044 it is less than the upper bound; the upper bound if the minimum
2045 distance is at least as large; CUDD_OUT_OF_MEM in case of failure.
2046 <p>
2049 <p>
2053 </code>
2055 <dt><pre>
2057 DdApaNumber <I></I>
2060 )
2061 </pre>
2062 <dd> Allocates memory for an arbitrary precision
2063 integer. Returns a pointer to the allocated memory if successful;
2064 NULL otherwise.
2065 <p>
2068 <p>
2070 <dt><pre>
2072 int <I></I>
2077 )
2078 </pre>
2079 <dd> Generates the next cube of a decision diagram onset,
2081 otherwise.
2082 <p>
2085 generator is modified.
2086 <p>
2093 </code>
2095 <dt><pre>
2097 int <I></I>
2101 )
2102 </pre>
2103 <dd> Finds the node of a decision diagram, using generator
2105 <p>
2108 <p>
2115 </code>
2117 <dt><pre>
2119 int <I></I>
2123 )
2124 </pre>
2125 <dd> Generates the next cube of a Boolean function,
2127 otherwise.
2128 <p>
2131 generator is modified.
2132 <p>
2140 </code>
2142 <dt><pre>
2144 unsigned int <I></I>
2147 )
2148 </pre>
2149 <dd> Returns the index of the node. The node pointer can be
2150 either regular or complemented.
2151 <p>
2154 <p>
2157 </code>
2159 <dt><pre>
2161 void <I></I>
2164 )
2165 </pre>
2166 <dd> Warns that a memory allocation failed.
2167 This function can be used as replacement of MMout_of_memory to prevent
2168 the safe_mem functions of the util package from exiting when malloc
2169 returns NULL. One possible use is in case of discretionary allocations;
2170 for instance, the allocation of memory to enlarge the computed table.
2171 <p>
2174 <p>
2176 <dt><pre>
2178 DdNode * <I></I>
2186 )
2187 </pre>
2188 <dd> Extracts a dense superset from a BDD. The procedure is
2189 identical to the underapproximation procedure except for the fact that it
2190 works on the complement of the given function. Extracting the subset
2191 of the complement function is equivalent to extracting the superset
2192 of the function.
2193 Returns a pointer to the BDD of the superset if successful. NULL if
2194 intermediate result causes the procedure to run out of memory. The
2195 parameter numVars is the maximum number of variables to be used in
2196 minterm calculation. The optimal number
2197 should be as close as possible to the size of the support of f.
2198 However, it is safe to pass the value returned by Cudd_ReadSize for
2199 numVars when the number of variables is under 1023. If numVars is
2201 the procedure will compute a value which will avoid overflow but
2202 will cause underflow with 2046 variables or more.
2203 <p>
2206 <p>
2211 </code>
2213 <dt><pre>
2215 unsigned int <I></I>
2218 )
2219 </pre>
2221 <p>
2224 <p>
2226 <dt><pre>
2228 int <I></I>
2234 )
2235 </pre>
2236 <dd> Prints to the standard output a DD and its statistics.
2237 The statistics include the number of nodes, the number of leaves, and
2238 the number of minterms. (The number of minterms is the number of
2239 assignments to the variables that cause the function to be different
2240 from the logical zero (for BDDs) and from the background value (for
2242 <ul>
2248 </ul>
2249 For the purpose of counting the number of minterms, the function is
2251 <p>
2254 <p>
2260 </code>
2262 <dt><pre>
2264 int <I></I>
2268 )
2269 </pre>
2270 <dd> Prints out statistics and settings for a CUDD manager.
2272 <p>
2275 <p>
2277 <dt><pre>
2279 int <I></I>
2282 )
2283 </pre>
2285 success; 0 otherwise.
2286 <p>
2289 <p>
2291 <dt><pre>
2293 int <I></I>
2297 )
2298 </pre>
2299 <dd> Prints a disjoint sum of product cover for the function
2300 rooted at node. Each product corresponds to a path from node to a
2301 leaf node different from the logical zero, and different from the
2302 background value. Uses the package default output file. Returns 1
2303 if successful; 0 otherwise.
2304 <p>
2307 <p>
2311 </code>
2313 <dt><pre>
2315 int <I></I>
2321 )
2322 </pre>
2325 the variable indices are printed.
2326 <p>
2329 <p>
2331 <dd> <b>See Also</b> <code><a href="#Cudd_FindTwoLiteralClauses">Cudd_FindTwoLiteralClauses</a>
2332 </code>
2334 <dt><pre>
2336 void <I></I>
2339 )
2340 </pre>
2341 <dd> Prints the package version number.
2342 <p>
2345 <p>
2347 <dt><pre>
2349 DdNode * <I></I>
2359 )
2360 </pre>
2361 <dd> Selects pairs from a relation R(x,y) (given as a BDD)
2362 in such a way that a given x appears in one pair only. Uses a
2363 priority function to determine which y should be paired to a given x.
2364 Cudd_PrioritySelect returns a pointer to
2365 the selected function if successful; NULL otherwise.
2366 Three of the arguments--x, y, and z--are vectors of BDD variables.
2367 The first two are the variables on which R depends. The third vectore
2368 is a vector of auxiliary variables, used during the computation. This
2369 vector is optional. If a NULL value is passed instead,
2370 Cudd_PrioritySelect will create the working variables on the fly.
2371 The sizes of x and y (and z if it is not NULL) should equal n.
2372 The priority function Pi can be passed as a BDD, or can be built by
2373 Cudd_PrioritySelect. If NULL is passed instead of a DdNode *,
2374 parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the
2375 priority function. (Pifunc is a pointer to a C function.) If Pi is not
2376 NULL, then Pifunc is ignored. Pifunc should have the same interface as
2377 the standard priority functions (e.g., Cudd_Dxygtdxz).
2378 Cudd_PrioritySelect and Cudd_CProjection can sometimes be used
2379 interchangeably. Specifically, calling Cudd_PrioritySelect with
2380 Cudd_Xgty as Pifunc produces the same result as calling
2381 Cudd_CProjection with the all-zero minterm as reference minterm.
2382 However, depending on the application, one or the other may be
2383 preferable:
2384 <ul>
2385 <li> When extracting representatives from an equivalence relation,
2386 Cudd_CProjection has the advantage of nor requiring the auxiliary
2387 variables.
2388 <li> When computing matchings in general bipartite graphs,
2389 Cudd_PrioritySelect normally obtains better results because it can use
2390 more powerful matching schemes (e.g., Cudd_Dxygtdxz).
2391 </ul>
2392 <p>
2395 the manager.
2396 <p>
2403 </code>
2405 <dt><pre>
2407 void <I></I>
2410 )
2411 </pre>
2412 <dd> Deletes resources associated with a DD manager and
2413 resets the global statistical counters. (Otherwise, another manaqger
2414 subsequently created would inherit the stats of this one.)
2415 <p>
2418 <p>
2421 </code>
2423 <dt><pre>
2425 long <I></I>
2427 <b></b> <i></i>
2428 )
2429 </pre>
2432 of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly
2434 The random generator can be explicitly initialized by calling
2435 Cudd_Srandom. If no explicit initialization is performed, then the
2436 seed 1 is assumed.
2437 <p>
2440 <p>
2443 </code>
2445 <dt><pre>
2447 int <I></I>
2450 )
2451 </pre>
2452 <dd> Returns the current value of the arcviolation
2453 parameter. This parameter is used in group sifting to decide how
2455 tolerable when checking for aggregation due to extended
2457 causes fewer variables to be aggregated. The default value is 0.
2458 <p>
2461 <p>
2464 </code>
2466 <dt><pre>
2468 DdNode * <I></I>
2471 )
2472 </pre>
2473 <dd> Reads the background constant of the manager.
2474 <p>
2477 <p>
2479 <dt><pre>
2481 double <I></I>
2484 )
2485 </pre>
2486 <dd> Returns the number of cache hits.
2487 <p>
2490 <p>
2493 </code>
2495 <dt><pre>
2497 double <I></I>
2500 )
2501 </pre>
2502 <dd> Returns the number of cache look-ups.
2503 <p>
2506 <p>
2509 </code>
2511 <dt><pre>
2513 unsigned int <I></I>
2516 )
2517 </pre>
2518 <dd> Reads the number of slots in the cache.
2519 <p>
2522 <p>
2525 </code>
2527 <dt><pre>
2529 double <I></I>
2532 )
2533 </pre>
2534 <dd> Reads the fraction of used slots in the cache. The unused
2535 slots are those in which no valid data is stored. Garbage collection,
2536 variable reordering, and cache resizing may cause used slots to become
2537 unused.
2538 <p>
2541 <p>
2544 </code>
2546 <dt><pre>
2548 unsigned int <I></I>
2551 )
2552 </pre>
2553 <dd> Returns the number of dead nodes in the unique table.
2554 <p>
2557 <p>
2560 </code>
2562 <dt><pre>
2564 CUDD_VALUE_TYPE <I></I>
2567 )
2568 </pre>
2569 <dd> Reads the epsilon parameter of the manager. The epsilon
2570 parameter control the comparison between floating point numbers.
2571 <p>
2574 <p>
2577 </code>
2579 <dt><pre>
2581 Cudd_ErrorType <I></I>
2584 )
2585 </pre>
2586 <dd> Returns the code of the last error. The error codes are
2587 defined in cudd.h.
2588 <p>
2591 <p>
2594 </code>
2596 <dt><pre>
2598 long <I></I>
2601 )
2602 </pre>
2603 <dd> Returns the number of milliseconds spent doing garbage
2604 collection since the manager was initialized.
2605 <p>
2608 <p>
2610 <dd> <b>See Also</b> <code><a href="#Cudd_ReadGarbageCollections">Cudd_ReadGarbageCollections</a>
2611 </code>
2613 <dt><pre>
2615 int <I></I>
2618 )
2619 </pre>
2620 <dd> Returns the number of times garbage collection has
2621 occurred in the manager. The number includes both the calls from
2622 reordering procedures and those caused by requests to create new
2623 nodes.
2624 <p>
2627 <p>
2629 <dd> <b>See Also</b> <code><a href="#Cudd_ReadGarbageCollectionTime">Cudd_ReadGarbageCollectionTime</a>
2630 </code>
2632 <dt><pre>
2634 Cudd_AggregationType <I></I>
2637 )
2638 </pre>
2639 <dd> Reads the groupcheck parameter of the manager. The
2640 groupcheck parameter determines the aggregation criterion in group
2641 sifting.
2642 <p>
2645 <p>
2648 </code>
2650 <dt><pre>
2652 int <I></I>
2656 )
2657 </pre>
2658 <dd> Returns the index of the ZDD variable currently in the
2659 i-th position of the order. If the index is CUDD_CONST_INDEX, returns
2660 CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.
2661 <p>
2664 <p>
2668 </code>
2670 <dt><pre>
2672 int <I></I>
2676 )
2677 </pre>
2678 <dd> Returns the index of the variable currently in the i-th
2679 position of the order. If the index is CUDD_CONST_INDEX, returns
2680 CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.
2681 <p>
2684 <p>
2688 </code>
2690 <dt><pre>
2692 int <I></I>
2700 )
2701 </pre>
2702 <dd> Accesses the i-th clause of a DD given the clause set which
2704 or in case of error.
2705 <p>
2708 <p>
2710 <dd> <b>See Also</b> <code><a href="#Cudd_FindTwoLiteralClauses">Cudd_FindTwoLiteralClauses</a>
2711 </code>
2713 <dt><pre>
2715 unsigned int <I></I>
2718 )
2719 </pre>
2720 <dd> Returns the total number of nodes currently in the unique
2721 table, including the dead nodes.
2722 <p>
2725 <p>
2728 </code>
2730 <dt><pre>
2732 int <I></I>
2737 )
2738 </pre>
2739 <dd> Reads an entry of the linear transform matrix.
2740 <p>
2743 <p>
2745 <dt><pre>
2747 DdNode * <I></I>
2750 )
2751 </pre>
2752 <dd> Returns the zero constant of the manager. The logic zero
2753 constant is the complement of the one constant, and is distinct from
2754 the arithmetic zero.
2755 <p>
2758 <p>
2762 </code>
2764 <dt><pre>
2766 unsigned int <I></I>
2769 )
2770 </pre>
2771 <dd> Reads the looseUpTo parameter of the manager.
2772 <p>
2775 <p>
2780 </code>
2782 <dt><pre>
2784 unsigned int <I></I>
2787 )
2788 </pre>
2789 <dd> Reads the maxCacheHard parameter of the manager.
2790 <p>
2793 <p>
2797 </code>
2799 <dt><pre>
2801 unsigned int <I></I>
2804 )
2805 </pre>
2806 <dd> Returns the soft limit for the cache size. The soft limit
2807 <p>
2810 <p>
2813 </code>
2815 <dt><pre>
2817 double <I></I>
2820 )
2821 </pre>
2822 <dd> Reads the maxGrowthAlt parameter of the manager. This
2823 parameter is analogous to the maxGrowth paramter, and is used every
2824 given number of reorderings instead of maxGrowth. The number of
2825 reorderings is set with Cudd_SetReorderingCycle. If the number of
2826 reorderings is 0 (default) maxGrowthAlt is never used.
2827 <p>
2830 <p>
2836 </code>
2838 <dt><pre>
2840 double <I></I>
2843 )
2844 </pre>
2845 <dd> Reads the maxGrowth parameter of the manager. This
2846 parameter determines how much the number of nodes can grow during
2847 sifting of a variable. Overall, sifting never increases the size of
2848 the decision diagrams. This parameter only refers to intermediate
2849 results. A lower value will speed up sifting, possibly at the
2850 expense of quality.
2851 <p>
2854 <p>
2858 </code>
2860 <dt><pre>
2862 unsigned int <I></I>
2865 )
2866 </pre>
2867 <dd> Reads the maximum allowed number of live nodes. When this
2868 number is exceeded, the package returns NULL.
2869 <p>
2872 <p>
2875 </code>
2877 <dt><pre>
2879 unsigned long <I></I>
2882 )
2883 </pre>
2884 <dd> Reads the maximum allowed memory. When this
2885 number is exceeded, the package returns NULL.
2886 <p>
2889 <p>
2892 </code>
2894 <dt><pre>
2896 unsigned long <I></I>
2899 )
2900 </pre>
2901 <dd> Returns the memory in use by the manager measured in bytes.
2902 <p>
2905 <p>
2907 <dt><pre>
2909 unsigned int <I></I>
2912 )
2913 </pre>
2914 <dd> Reads the minDead parameter of the manager. The minDead
2915 parameter is used by the package to decide whether to collect garbage
2916 or resize a subtable of the unique table when the subtable becomes
2917 too full. The application can indirectly control the value of minDead
2918 by setting the looseUpTo parameter.
2919 <p>
2922 <p>
2927 </code>
2929 <dt><pre>
2931 unsigned int <I></I>
2934 )
2935 </pre>
2936 <dd> Reads the hit rate that causes resizinig of the computed
2937 table.
2938 <p>
2941 <p>
2944 </code>
2946 <dt><pre>
2948 DdNode * <I></I>
2951 )
2952 </pre>
2953 <dd> Reads the minus-infinity constant from the manager.
2954 <p>
2957 <p>
2959 <dt><pre>
2961 unsigned int <I></I>
2964 )
2965 </pre>
2966 <dd> Returns the threshold for the next dynamic reordering.
2967 The threshold is in terms of number of nodes and is in effect only
2968 if reordering is enabled. The count does not include the dead nodes,
2969 unless the countDead parameter of the manager has been changed from
2970 its default setting.
2971 <p>
2974 <p>
2977 </code>
2979 <dt><pre>
2981 long <I></I>
2984 )
2985 </pre>
2986 <dd> Reports the number of live nodes in BDDs and ADDs. This
2987 number does not include the isolated projection functions and the
2988 unused constants. These nodes that are not counted are not part of
2989 the DDs manipulated by the application.
2990 <p>
2993 <p>
2997 </code>
2999 <dt><pre>
3001 double <I></I>
3004 )
3005 </pre>
3006 <dd> Returns the number of nodes killed by dereferencing if the
3007 keeping of this statistic is enabled; -1 otherwise. This statistic is
3008 enabled only if the package is compiled with DD_STATS defined.
3009 <p>
3012 <p>
3015 </code>
3017 <dt><pre>
3019 double <I></I>
3022 )
3023 </pre>
3024 <dd> Returns the number of nodes returned to the free list if the
3025 keeping of this statistic is enabled; -1 otherwise. This statistic is
3026 enabled only if the package is compiled with DD_STATS defined.
3027 <p>
3030 <p>
3033 </code>
3035 <dt><pre>
3037 int <I></I>
3040 )
3041 </pre>
3042 <dd> Reads the current number of crossovers used by the
3043 genetic algorithm for variable reordering. A larger number of crossovers will
3044 cause the genetic algorithm to take more time, but will generally
3045 produce better results. The default value is 0, in which case the
3046 package uses three times the number of variables as number of crossovers,
3047 with a maximum of 60.
3048 <p>
3051 <p>
3054 </code>
3056 <dt><pre>
3058 DdNode * <I></I>
3061 )
3062 </pre>
3063 <dd> Returns the one constant of the manager. The one
3064 constant is common to ADDs and BDDs.
3065 <p>
3068 <p>
3073 </code>
3075 <dt><pre>
3077 int <I></I>
3080 )
3081 </pre>
3082 <dd> Reports the peak number of live nodes. This count is kept
3083 only if CUDD is compiled with DD_STATS defined. If DD_STATS is not
3084 defined, this function returns -1.
3085 <p>
3088 <p>
3093 </code>
3095 <dt><pre>
3097 long <I></I>
3100 )
3101 </pre>
3102 <dd> Reports the peak number of nodes. This number includes
3103 node on the free list. At the peak, the number of nodes on the free
3104 list is guaranteed to be less than DD_MEM_CHUNK.
3105 <p>
3108 <p>
3112 </code>
3114 <dt><pre>
3116 int <I></I>
3120 )
3121 </pre>
3122 <dd> Returns the current position of the i-th ZDD variable
3123 in the order. If the index is CUDD_CONST_INDEX, returns
3124 CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
3125 -1.
3126 <p>
3129 <p>
3133 </code>
3135 <dt><pre>
3137 int <I></I>
3141 )
3142 </pre>
3143 <dd> Returns the current position of the i-th variable in
3144 the order. If the index is CUDD_CONST_INDEX, returns
3145 CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
3146 -1.
3147 <p>
3150 <p>
3154 </code>
3156 <dt><pre>
3158 DdNode * <I></I>
3161 )
3162 </pre>
3163 <dd> Reads the plus-infinity constant from the manager.
3164 <p>
3167 <p>
3169 <dt><pre>
3171 int <I></I>
3174 )
3175 </pre>
3176 <dd> Reads the current size of the population used by the
3177 genetic algorithm for variable reordering. A larger population size will
3178 cause the genetic algorithm to take more time, but will generally
3179 produce better results. The default value is 0, in which case the
3180 package uses three times the number of variables as population size,
3181 with a maximum of 120.
3182 <p>
3185 <p>
3188 </code>
3190 <dt><pre>
3192 int <I></I>
3195 )
3196 </pre>
3197 <dd> Returns the current value of the recombination
3198 parameter used in group sifting. A larger (positive) value makes the
3199 aggregation of variables due to the second difference criterion more
3200 likely. A smaller (negative) value makes aggregation less likely.
3201 <p>
3204 <p>
3207 </code>
3209 <dt><pre>
3211 double <I></I>
3214 )
3215 </pre>
3216 <dd> Returns the number of recursive calls if the package is
3217 compiled with DD_COUNT defined.
3218 <p>
3221 <p>
3223 <dt><pre>
3225 int <I></I>
3228 )
3229 </pre>
3230 <dd> Reads the reordCycle parameter of the manager. This
3231 parameter determines how often the alternate threshold on maximum
3232 growth is used in reordering.
3233 <p>
3236 <p>
3238 <dd> <b>See Also</b> <code><a href="#Cudd_ReadMaxGrowthAlternate">Cudd_ReadMaxGrowthAlternate</a>
3241 </code>
3243 <dt><pre>
3245 long <I></I>
3248 )
3249 </pre>
3250 <dd> Returns the number of milliseconds spent reordering
3251 variables since the manager was initialized. The time spent in collecting
3252 garbage before reordering is included.
3253 <p>
3256 <p>
3259 </code>
3261 <dt><pre>
3263 int <I></I>
3266 )
3267 </pre>
3268 <dd> Returns the number of times reordering has occurred in the
3269 manager. The number includes both the calls to Cudd_ReduceHeap from
3270 the application program and those automatically performed by the
3271 package. However, calls that do not even initiate reordering are not
3272 counted. A call may not initiate reordering if there are fewer than
3273 minsize live nodes in the manager, or if CUDD_REORDER_NONE is specified
3274 as reordering method. The calls to Cudd_ShuffleHeap are not counted.
3275 <p>
3278 <p>
3282 </code>
3284 <dt><pre>
3286 int <I></I>
3289 )
3290 </pre>
3291 <dd> Reads the siftMaxSwap parameter of the manager. This
3292 parameter gives the maximum number of swaps that will be attempted
3293 for each invocation of sifting. The real number of swaps may exceed
3294 the set limit because the package will always complete the sifting
3295 of the variable that causes the limit to be reached.
3296 <p>
3299 <p>
3303 </code>
3305 <dt><pre>
3307 int <I></I>
3310 )
3311 </pre>
3312 <dd> Reads the siftMaxVar parameter of the manager. This
3313 parameter gives the maximum number of variables that will be sifted
3314 for each invocation of sifting.
3315 <p>
3318 <p>
3322 </code>
3324 <dt><pre>
3326 int <I></I>
3329 )
3330 </pre>
3331 <dd> Returns the number of BDD variables in existance.
3332 <p>
3335 <p>
3338 </code>
3340 <dt><pre>
3342 unsigned int <I></I>
3345 )
3346 </pre>
3347 <dd> Returns the total number of slots of the unique table.
3348 This number ismainly for diagnostic purposes.
3349 <p>
3352 <p>
3354 <dt><pre>
3356 FILE * <I></I>
3359 )
3360 </pre>
3361 <dd> Reads the stderr of a manager. This is the file pointer to
3362 which messages normally going to stderr are written. It is initialized
3363 to stderr. Cudd_SetStderr allows the application to redirect it.
3364 <p>
3367 <p>
3371 </code>
3373 <dt><pre>
3375 FILE * <I></I>
3378 )
3379 </pre>
3380 <dd> Reads the stdout of a manager. This is the file pointer to
3381 which messages normally going to stdout are written. It is initialized
3382 to stdout. Cudd_SetStdout allows the application to redirect it.
3383 <p>
3386 <p>
3390 </code>
3392 <dt><pre>
3394 double <I></I>
3397 )
3398 </pre>
3399 <dd> Reads the number of elementary reordering steps.
3400 <p>
3403 <p>
3405 <dt><pre>
3407 int <I></I>
3410 )
3411 </pre>
3412 <dd> Returns the current value of the symmviolation
3413 parameter. This parameter is used in group sifting to decide how
3417 small value causes fewer variables to be aggregated. The default
3418 value is 0.
3419 <p>
3422 <p>
3425 </code>
3427 <dt><pre>
3429 MtrNode * <I></I>
3432 )
3433 </pre>
3434 <dd> Returns the variable group tree of the manager.
3435 <p>
3438 <p>
3443 </code>
3445 <dt><pre>
3447 double <I></I>
3450 )
3451 </pre>
3452 <dd> Returns the number of links followed during look-ups in the
3453 unique table if the keeping of this statistic is enabled; -1 otherwise.
3454 If an item is found in the first position of its collision list, the
3455 number of links followed is taken to be 0. If it is in second position,
3456 the number of links is 1, and so on. This statistic is enabled only if
3457 the package is compiled with DD_UNIQUE_PROFILE defined.
3458 <p>
3461 <p>
3464 </code>
3466 <dt><pre>
3468 double <I></I>
3471 )
3472 </pre>
3473 <dd> Returns the number of look-ups in the unique table if the
3474 keeping of this statistic is enabled; -1 otherwise. This statistic is
3475 enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.
3476 <p>
3479 <p>
3482 </code>
3484 <dt><pre>
3486 double <I></I>
3489 )
3490 </pre>
3491 <dd> Reads the fraction of used slots in the unique
3492 table. The unused slots are those in which no valid data is
3493 stored. Garbage collection, variable reordering, and subtable
3494 resizing may cause used slots to become unused.
3495 <p>
3498 <p>
3501 </code>
3503 <dt><pre>
3505 DdNode * <I></I>
3509 )
3510 </pre>
3511 <dd> Returns the i-th element of the vars array if it falls
3512 within the array bounds; NULL otherwise. If i is the index of an
3513 existing variable, this function produces the same result as
3514 Cudd_bddIthVar. However, if the i-th var does not exist yet,
3515 Cudd_bddIthVar will create it, whereas Cudd_ReadVars will not.
3516 <p>
3519 <p>
3522 </code>
3524 <dt><pre>
3526 DdNode * <I></I>
3530 )
3531 </pre>
3533 The representation of the constant 1 function as a ZDD depends on
3534 how many variables it (nominally) depends on. The index of the
3536 <p>
3539 <p>
3542 </code>
3544 <dt><pre>
3546 int <I></I>
3549 )
3550 </pre>
3551 <dd> Returns the number of ZDD variables in existance.
3552 <p>
3555 <p>
3558 </code>
3560 <dt><pre>
3562 MtrNode * <I></I>
3565 )
3566 </pre>
3567 <dd> Returns the variable group tree of the manager.
3568 <p>
3571 <p>
3576 </code>
3578 <dt><pre>
3580 DdNode * <I></I>
3583 )
3584 </pre>
3585 <dd> Returns the zero constant of the manager. The zero
3586 constant is the arithmetic zero, rather than the logic zero. The
3587 latter is the complement of the one constant.
3588 <p>
3591 <p>
3595 </code>
3597 <dt><pre>
3599 void <I></I>
3603 )
3604 </pre>
3605 <dd> Decreases the reference count of ZDD node n. If n dies,
3606 recursively decreases the reference counts of its children. It is
3607 used to dispose of a ZDD that is no longer needed.
3608 <p>
3611 <p>
3616 </code>
3618 <dt><pre>
3620 void <I></I>
3624 )
3625 </pre>
3626 <dd> Decreases the reference count of node n. If n dies,
3627 recursively decreases the reference counts of its children. It is
3628 used to dispose of a DD that is no longer needed.
3629 <p>
3632 <p>
3637 </code>
3639 <dt><pre>
3641 int <I></I>
3646 )
3647 </pre>
3648 <dd> Main dynamic reordering routine.
3649 Calls one of the possible reordering procedures:
3650 <ul>
3651 <li>Swapping
3652 <li>Sifting
3653 <li>Symmetric Sifting
3654 <li>Group Sifting
3655 <li>Window Permutation
3656 <li>Simulated Annealing
3657 <li>Genetic Algorithm
3658 <li>Dynamic Programming (exact)
3659 </ul>
3661 For sifting, symmetric sifting, group sifting, and window
3662 permutation it is possible to request reordering to convergence.<p>
3664 The core of all methods is the reordering procedure
3665 cuddSwapInPlace() which swaps two adjacent variables and is based
3666 on Rudell's paper.
3668 sifting (with and without convergence) returns 1 plus the number of
3669 symmetric variables, in case of success.
3670 <p>
3673 the cache.
3674 <p>
3676 <dt><pre>
3678 void <I></I>
3681 )
3682 </pre>
3683 <dd> Increases the reference count of a node, if it is not
3684 saturated.
3685 <p>
3688 <p>
3692 </code>
3694 <dt><pre>
3696 DdNode * <I></I>
3703 )
3704 </pre>
3705 <dd> Extracts a dense superset from a BDD. The procedure is
3706 identical to the underapproximation procedure except for the fact that it
3707 works on the complement of the given function. Extracting the subset
3708 of the complement function is equivalent to extracting the superset
3709 of the function.
3710 Returns a pointer to the BDD of the superset if successful. NULL if
3711 intermediate result causes the procedure to run out of memory. The
3712 parameter numVars is the maximum number of variables to be used in
3713 minterm calculation. The optimal number
3714 should be as close as possible to the size of the support of f.
3715 However, it is safe to pass the value returned by Cudd_ReadSize for
3716 numVars when the number of variables is under 1023. If numVars is
3718 the procedure will compute a value which will avoid overflow but
3719 will cause underflow with 2046 variables or more.
3720 <p>
3723 <p>
3728 </code>
3730 <dt><pre>
3732 DdNode * <I></I>
3739 )
3740 </pre>
3741 <dd> Extracts a dense subset from a BDD. This procedure uses
3742 a remapping technique and density as the cost function.
3743 Returns a pointer to the BDD of the subset if
3744 successful. NULL if the procedure runs out of memory. The parameter
3745 numVars is the maximum number of variables to be used in minterm
3746 calculation. The optimal number should be as close as possible to
3747 the size of the support of f. However, it is safe to pass the value
3748 returned by Cudd_ReadSize for numVars when the number of variables
3750 overflow. If a 0 parameter is passed then the procedure will compute
3751 a value which will avoid overflow but will cause underflow with 2046
3752 variables or more.
3753 <p>
3756 <p>
3762 </code>
3764 <dt><pre>
3766 int <I></I>
3771 )
3772 </pre>
3773 <dd> Removes a function from a hook. A hook is a list of
3774 application-provided functions called on certain occasions by the
3776 <p>
3779 <p>
3782 </code>
3784 <dt><pre>
3786 int <I></I>
3789 )
3790 </pre>
3792 0 otherwise.
3793 <p>
3796 <p>
3798 <dd> <b>See Also</b> <code><a href="#Cudd_EnableReorderingReporting">Cudd_EnableReorderingReporting</a>
3800 </code>
3802 <dt><pre>
3804 int <I></I>
3808 )
3809 </pre>
3810 <dd> Reports the status of automatic dynamic reordering of
3811 ZDDs. Parameter method is set to the ZDD reordering method currently
3813 otherwise.
3814 <p>
3817 selected.
3818 <p>
3823 </code>
3825 <dt><pre>
3827 int <I></I>
3831 )
3832 </pre>
3833 <dd> Reports the status of automatic dynamic reordering of
3834 BDDs and ADDs. Parameter method is set to the reordering method
3836 otherwise.
3837 <p>
3840 selected.
3841 <p>
3846 </code>
3848 <dt><pre>
3850 void <I></I>
3854 )
3855 </pre>
3856 <dd> Sets the value of the arcviolation
3857 parameter. This parameter is used in group sifting to decide how
3859 tolerable when checking for aggregation due to extended
3861 causes fewer variables to be aggregated. The default value is 0.
3862 <p>
3865 <p>
3868 </code>
3870 <dt><pre>
3872 void <I></I>
3876 )
3877 </pre>
3878 <dd> Sets the background constant of the manager. It assumes
3879 that the DdNode pointer bck is already referenced.
3880 <p>
3883 <p>
3885 <dt><pre>
3887 void <I></I>
3891 )
3892 </pre>
3893 <dd> Sets the epsilon parameter of the manager to ep. The epsilon
3894 parameter control the comparison between floating point numbers.
3895 <p>
3898 <p>
3901 </code>
3903 <dt><pre>
3905 void <I></I>
3909 )
3910 </pre>
3911 <dd> Sets the parameter groupcheck of the manager to gc. The
3912 groupcheck parameter determines the aggregation criterion in group
3913 sifting.
3914 <p>
3917 <p>
3920 </code>
3922 <dt><pre>
3924 void <I></I>
3928 )
3929 </pre>
3930 <dd> Sets the looseUpTo parameter of the manager. This
3931 parameter of the manager controls the threshold beyond which no fast
3932 growth of the unique table is allowed. The threshold is given as a
3933 number of slots. If the value passed to this function is 0, the
3934 function determines a suitable value based on the available memory.
3935 <p>
3938 <p>
3942 </code>
3944 <dt><pre>
3946 void <I></I>
3950 )
3951 </pre>
3952 <dd> Sets the maxCacheHard parameter of the manager. The
3953 cache cannot grow larger than maxCacheHard entries. This parameter
3954 allows an application to control the trade-off of memory versus
3955 speed. If the value passed to this function is 0, the function
3956 determines a suitable maximum cache size based on the available memory.
3957 <p>
3960 <p>
3964 </code>
3966 <dt><pre>
3968 void <I></I>
3972 )
3973 </pre>
3974 <dd> Sets the maxGrowthAlt parameter of the manager. This
3975 parameter is analogous to the maxGrowth paramter, and is used every
3976 given number of reorderings instead of maxGrowth. The number of
3977 reorderings is set with Cudd_SetReorderingCycle. If the number of
3978 reorderings is 0 (default) maxGrowthAlt is never used.
3979 <p>
3982 <p>
3984 <dd> <b>See Also</b> <code><a href="#Cudd_ReadMaxGrowthAlternate">Cudd_ReadMaxGrowthAlternate</a>
3988 </code>
3990 <dt><pre>
3992 void <I></I>
3996 )
3997 </pre>
3998 <dd> Sets the maxGrowth parameter of the manager. This
3999 parameter determines how much the number of nodes can grow during
4000 sifting of a variable. Overall, sifting never increases the size of
4001 the decision diagrams. This parameter only refers to intermediate
4002 results. A lower value will speed up sifting, possibly at the
4003 expense of quality.
4004 <p>
4007 <p>
4011 </code>
4013 <dt><pre>
4015 void <I></I>
4019 )
4020 </pre>
4021 <dd> Sets the maximum allowed number of live nodes. When this
4022 number is exceeded, the package returns NULL.
4023 <p>
4026 <p>
4029 </code>
4031 <dt><pre>
4033 void <I></I>
4037 )
4038 </pre>
4039 <dd> Sets the maximum allowed memory. When this
4040 number is exceeded, the package returns NULL.
4041 <p>
4044 <p>
4047 </code>
4049 <dt><pre>
4051 void <I></I>
4055 )
4056 </pre>
4057 <dd> Sets the minHit parameter of the manager. This
4058 parameter controls the resizing of the computed table. If the hit
4059 rate is larger than the specified value, and the cache is not
4060 already too large, then its size is doubled.
4061 <p>
4064 <p>
4067 </code>
4069 <dt><pre>
4071 void <I></I>
4075 )
4076 </pre>
4077 <dd> Sets the threshold for the next dynamic reordering.
4078 The threshold is in terms of number of nodes and is in effect only
4079 if reordering is enabled. The count does not include the dead nodes,
4080 unless the countDead parameter of the manager has been changed from
4081 its default setting.
4082 <p>
4085 <p>
4088 </code>
4090 <dt><pre>
4092 void <I></I>
4096 )
4097 </pre>
4098 <dd> Sets the number of crossovers used by the genetic
4099 algorithm for variable reordering. A larger number of crossovers
4100 will cause the genetic algorithm to take more time, but will
4101 generally produce better results. The default value is 0, in which
4102 case the package uses three times the number of variables as number
4103 of crossovers, with a maximum of 60.
4104 <p>
4107 <p>
4110 </code>
4112 <dt><pre>
4114 void <I></I>
4118 )
4119 </pre>
4120 <dd> Sets the size of the population used by the
4121 genetic algorithm for variable reordering. A larger population size will
4122 cause the genetic algorithm to take more time, but will generally
4123 produce better results. The default value is 0, in which case the
4124 package uses three times the number of variables as population size,
4125 with a maximum of 120.
4126 <p>
4129 <p>
4132 </code>
4134 <dt><pre>
4136 void <I></I>
4140 )
4141 </pre>
4142 <dd> Sets the value of the recombination parameter used in
4143 group sifting. A larger (positive) value makes the aggregation of
4144 variables due to the second difference criterion more likely. A
4145 smaller (negative) value makes aggregation less likely. The default
4146 value is 0.
4147 <p>
4150 <p>
4153 </code>
4155 <dt><pre>
4157 void <I></I>
4161 )
4162 </pre>
4163 <dd> Sets the reordCycle parameter of the manager. This
4164 parameter determines how often the alternate threshold on maximum
4165 growth is used in reordering.
4166 <p>
4169 <p>
4171 <dd> <b>See Also</b> <code><a href="#Cudd_ReadMaxGrowthAlternate">Cudd_ReadMaxGrowthAlternate</a>
4174 </code>
4176 <dt><pre>
4178 void <I></I>
4182 )
4183 </pre>
4184 <dd> Sets the siftMaxSwap parameter of the manager. This
4185 parameter gives the maximum number of swaps that will be attempted
4186 for each invocation of sifting. The real number of swaps may exceed
4187 the set limit because the package will always complete the sifting
4188 of the variable that causes the limit to be reached.
4189 <p>
4192 <p>
4196 </code>
4198 <dt><pre>
4200 void <I></I>
4204 )
4205 </pre>
4206 <dd> Sets the siftMaxVar parameter of the manager. This
4207 parameter gives the maximum number of variables that will be sifted
4208 for each invocation of sifting.
4209 <p>
4212 <p>
4216 </code>
4218 <dt><pre>
4220 void <I></I>
4224 )
4225 </pre>
4226 <dd> Sets the stderr of a manager.
4227 <p>
4230 <p>
4234 </code>
4236 <dt><pre>
4238 void <I></I>
4242 )
4243 </pre>
4244 <dd> Sets the stdout of a manager.
4245 <p>
4248 <p>
4252 </code>
4254 <dt><pre>
4256 void <I></I>
4260 )
4261 </pre>
4262 <dd> Sets the value of the symmviolation
4263 parameter. This parameter is used in group sifting to decide how
4267 small value causes fewer variables to be aggregated. The default
4268 value is 0.
4269 <p>
4272 <p>
4275 </code>
4277 <dt><pre>
4279 void <I></I>
4283 )
4284 </pre>
4285 <dd> Sets the variable group tree of the manager.
4286 <p>
4289 <p>
4294 </code>
4296 <dt><pre>
4298 int <I></I>
4304 )
4305 </pre>
4306 <dd> Registers with the manager a variable mapping described
4307 by two sets of variables. This variable mapping is then used by
4308 functions like Cudd_bddVarMap. This function is convenient for
4309 those applications that perform the same mapping several times.
4310 However, if several different permutations are used, it may be more
4311 efficient not to rely on the registered mapping, because changing
4312 mapping causes the cache to be cleared. (The initial setting,
4313 however, does not clear the cache.) The two sets of variables (x and
4314 y) must have the same size (x and y). The size is given by n. The
4315 two sets of variables are normally disjoint, but this restriction is
4316 not imposeded by the function. When new variables are created, the
4317 map is automatically extended (each new variable maps to
4318 itself). The typical use, however, is to wait until all variables
4319 are created, and then create the map. Returns 1 if the mapping is
4320 successfully registered with the manager; 0 otherwise.
4321 <p>
4324 <p>
4329 </code>
4331 <dt><pre>
4333 void <I></I>
4337 )
4338 </pre>
4339 <dd> Sets the ZDD variable group tree of the manager.
4340 <p>
4343 <p>
4348 </code>
4350 <dt><pre>
4352 int <I></I>
4356 )
4357 </pre>
4358 <dd> Counts the number of nodes in an array of DDs. Shared
4359 nodes are counted only once. Returns the total number of nodes.
4360 <p>
4363 <p>
4366 </code>
4368 <dt><pre>
4370 int <I></I>
4375 )
4376 </pre>
4377 <dd> Find the length of the shortest path(s) in a DD. f is
4378 the DD we want to get the shortest path for; weight[i] is the
4379 weight of the THEN edge coming from the node whose index is i. All
4380 ELSE edges have 0 weight. Returns the length of the shortest
4381 path(s) if such a path is found; a large number if the function is
4382 identically 0, and CUDD_OUT_OF_MEM in case of failure.
4383 <p>
4386 <p>
4389 </code>
4391 <dt><pre>
4393 DdNode * <I></I>
4400 )
4401 </pre>
4402 <dd> Finds a shortest path in a DD. f is the DD we want to
4403 get the shortest path for; weight[i] is the weight of the THEN arc
4404 coming from the node whose index is i. If weight is NULL, then unit
4405 weights are assumed for all THEN arcs. All ELSE arcs have 0 weight.
4406 If non-NULL, both weight and support should point to arrays with at
4407 least as many entries as there are variables in the manager.
4408 Returns the shortest path as the BDD of a cube.
4409 <p>
4412 If support is NULL on entry, then Cudd_ShortestPath does not compute
4413 the true support info. length contains the length of the path.
4414 <p>
4418 </code>
4420 <dt><pre>
4422 int <I></I>
4426 )
4427 </pre>
4428 <dd> Reorders variables according to given permutation.
4429 The i-th entry of the permutation array contains the index of the variable
4430 that should be brought to the i-th level. The size of the array should be
4431 equal or greater to the number of variables currently in use.
4433 <p>
4436 the cache.
4437 <p>
4440 </code>
4442 <dt><pre>
4444 DdNode * <I></I>
4452 )
4453 </pre>
4455 value is the consistency condition. The y variables are the unknowns
4456 and the remaining variables are the parameters. Returns the
4457 consistency condition if successful; NULL otherwise. Cudd_SolveEqn
4458 allocates an array and fills it with the indices of the
4459 unknowns. This array is used by Cudd_VerifySol.
4460 <p>
4463 variables are returned in yIndex.
4464 <p>
4467 </code>
4469 <dt><pre>
4471 DdNode * <I></I>
4478 )
4479 </pre>
4482 to create as few extra nodes as possible. The function represented
4485 of the on-set of S if successful; NULL otherwise.
4486 <p>
4489 <p>
4491 <dt><pre>
4493 void <I></I>
4496 )
4497 </pre>
4498 <dd> Initializer for the portable number generator based on
4499 ran2 in "Numerical Recipes in C." The input is the seed for the
4500 generator. If it is negative, its absolute value is taken as seed.
4502 recurrences used to generate a long-period stream, and sets up the
4503 shuffle table.
4504 <p>
4507 <p>
4510 </code>
4512 <dt><pre>
4514 int <I></I>
4519 )
4520 </pre>
4521 <dd> Sample hook function to call after reordering.
4522 Prints on the manager's stdout final size and reordering time.
4524 <p>
4527 <p>
4530 </code>
4532 <dt><pre>
4534 int <I></I>
4539 )
4540 </pre>
4541 <dd> Sample hook function to call before reordering.
4542 Prints on the manager's stdout reordering method and initial size.
4544 <p>
4547 <p>
4550 </code>
4552 <dt><pre>
4554 DdNode * <I></I>
4560 )
4561 </pre>
4563 the ratio of number of minterms to number of nodes. Uses several
4564 techniques in series. It is more expensive than other subsetting
4565 procedures, but often produces better results. See
4566 Cudd_SubsetShortPaths for a description of the threshold and nvars
4567 parameters. Returns a pointer to the result if successful; NULL
4568 otherwise.
4569 <p>
4572 <p>
4578 </code>
4580 <dt><pre>
4582 DdNode * <I></I>
4588 )
4589 </pre>
4590 <dd> Extracts a dense subset from a BDD. This procedure
4591 builds a subset by throwing away one of the children of each node,
4592 starting from the root, until the result is small enough. The child
4593 that is eliminated from the result is the one that contributes the
4594 fewer minterms. Returns a pointer to the BDD of the subset if
4595 successful. NULL if the procedure runs out of memory. The parameter
4596 numVars is the maximum number of variables to be used in minterm
4597 calculation and node count calculation. The optimal number should
4598 be as close as possible to the size of the support of f. However,
4599 it is safe to pass the value returned by Cudd_ReadSize for numVars
4600 when the number of variables is under 1023. If numVars is larger
4602 procedure will compute a value which will avoid overflow but will
4603 cause underflow with 2046 variables or more.
4604 <p>
4607 <p>
4612 </code>
4614 <dt><pre>
4616 DdNode * <I></I>
4623 )
4624 </pre>
4625 <dd> Extracts a dense subset from a BDD. This procedure
4626 tries to preserve the shortest paths of the input BDD, because they
4627 give many minterms and contribute few nodes. This procedure may
4628 increase the number of nodes in trying to create the subset or
4629 reduce the number of nodes due to recombination as compared to the
4630 original BDD. Hence the threshold may not be strictly adhered to. In
4631 practice, recombination overshadows the increase in the number of
4632 nodes and results in small BDDs as compared to the threshold. The
4633 hardlimit specifies whether threshold needs to be strictly adhered
4634 to. If it is set to 1, the procedure ensures that result is never
4635 larger than the specified limit but may be considerably less than
4636 the threshold. Returns a pointer to the BDD for the subset if
4637 successful; NULL otherwise. The value for numVars should be as
4638 close as possible to the size of the support of f for better
4639 efficiency. However, it is safe to pass the value returned by
4640 Cudd_ReadSize for numVars. If 0 is passed, then the value returned
4641 by Cudd_ReadSize is used.
4642 <p>
4645 <p>
4650 </code>
4652 <dt><pre>
4654 DdNode * <I></I>
4662 )
4663 </pre>
4664 <dd> Extracts a subset from a BDD in the following procedure.
4665 1. Compute the weight for each mask variable by counting the number of
4666 minterms for both positive and negative cofactors of the BDD with
4667 respect to each mask variable. (weight = #positive - #negative)
4668 2. Find a representative cube of the BDD by using the weight. From the
4669 top variable of the BDD, for each variable, if the weight is greater
4670 than 0.0, choose THEN branch, othereise ELSE branch, until meeting
4671 the constant 1.
4672 3. Quantify out the variables not in maskVars from the representative
4673 cube and if a variable in maskVars is don't care, replace the
4675 4. Make a subset of the BDD by multiplying with the modified cube.
4676 <p>
4679 <p>
4681 <dt><pre>
4683 DdNode * <I></I>
4689 )
4690 </pre>
4692 the ratio of number of minterms to number of nodes. Uses several
4693 techniques in series. It is more expensive than other supersetting
4694 procedures, but often produces better results. See
4695 Cudd_SupersetShortPaths for a description of the threshold and nvars
4696 parameters. Returns a pointer to the result if successful; NULL
4697 otherwise.
4698 <p>
4701 <p>
4708 </code>
4710 <dt><pre>
4712 DdNode * <I></I>
4718 )
4719 </pre>
4720 <dd> Extracts a dense superset from a BDD. The procedure is
4721 identical to the subset procedure except for the fact that it
4722 receives the complement of the given function. Extracting the subset
4723 of the complement function is equivalent to extracting the superset
4724 of the function. This procedure builds a superset by throwing away
4725 one of the children of each node starting from the root of the
4726 complement function, until the result is small enough. The child
4727 that is eliminated from the result is the one that contributes the
4728 fewer minterms.
4729 Returns a pointer to the BDD of the superset if successful. NULL if
4730 intermediate result causes the procedure to run out of memory. The
4731 parameter numVars is the maximum number of variables to be used in
4732 minterm calculation and node count calculation. The optimal number
4733 should be as close as possible to the size of the support of f.
4734 However, it is safe to pass the value returned by Cudd_ReadSize for
4735 numVars when the number of variables is under 1023. If numVars is
4737 the procedure will compute a value which will avoid overflow but
4738 will cause underflow with 2046 variables or more.
4739 <p>
4742 <p>
4747 </code>
4749 <dt><pre>
4751 DdNode * <I></I>
4758 )
4759 </pre>
4760 <dd> Extracts a dense superset from a BDD. The procedure is
4761 identical to the subset procedure except for the fact that it
4762 receives the complement of the given function. Extracting the subset
4763 of the complement function is equivalent to extracting the superset
4764 of the function. This procedure tries to preserve the shortest
4765 paths of the complement BDD, because they give many minterms and
4766 contribute few nodes. This procedure may increase the number of
4767 nodes in trying to create the superset or reduce the number of nodes
4768 due to recombination as compared to the original BDD. Hence the
4769 threshold may not be strictly adhered to. In practice, recombination
4770 overshadows the increase in the number of nodes and results in small
4771 BDDs as compared to the threshold. The hardlimit specifies whether
4772 threshold needs to be strictly adhered to. If it is set to 1, the
4773 procedure ensures that result is never larger than the specified
4774 limit but may be considerably less than the threshold. Returns a
4775 pointer to the BDD for the superset if successful; NULL
4776 otherwise. The value for numVars should be as close as possible to
4777 the size of the support of f for better efficiency. However, it is
4778 safe to pass the value returned by Cudd_ReadSize for numVar. If 0
4779 is passed, then the value returned by Cudd_ReadSize is used.
4780 <p>
4783 <p>
4788 </code>
4790 <dt><pre>
4792 int * <I></I>
4796 )
4797 </pre>
4798 <dd> Finds the variables on which a DD depends. Returns an
4799 index array of the variables if successful; NULL otherwise. The
4800 size of the array equals the number of variables in the manager.
4801 Each entry of the array is 1 if the corresponding variable is in the
4802 support of the DD and 0 otherwise.
4803 <p>
4806 <p>
4811 </code>
4813 <dt><pre>
4815 int <I></I>
4819 )
4820 </pre>
4821 <dd> Counts the variables on which a DD depends.
4822 Returns the number of the variables if successful; CUDD_OUT_OF_MEM
4823 otherwise.
4824 <p>
4827 <p>
4830 </code>
4832 <dt><pre>
4834 DdNode * <I></I>
4838 )
4839 </pre>
4840 <dd> Finds the variables on which a DD depends.
4841 Returns a BDD consisting of the product of the variables if
4842 successful; NULL otherwise.
4843 <p>
4846 <p>
4850 </code>
4852 <dt><pre>
4854 void <I></I>
4859 )
4860 </pre>
4861 <dd> Prints statistics on symmetric variables.
4862 <p>
4865 <p>
4867 <dt><pre>
4869 void <I></I>
4872 )
4873 </pre>
4874 <dd> Causes the dead nodes not to be counted towards
4875 triggering reordering. This causes less frequent reorderings. By
4876 default dead nodes are not counted. Therefore there is no need to
4877 call this function unless Cudd_TurnOnCountDead has been previously
4878 called.
4879 <p>
4882 <p>
4886 </code>
4888 <dt><pre>
4890 void <I></I>
4893 )
4894 </pre>
4895 <dd> Causes the dead nodes to be counted towards triggering
4896 reordering. This causes more frequent reorderings. By default dead
4897 nodes are not counted.
4898 <p>
4901 <p>
4905 </code>
4907 <dt><pre>
4909 DdNode * <I></I>
4917 )
4918 </pre>
4919 <dd> Extracts a dense subset from a BDD. This procedure uses
4920 a variant of Tom Shiple's underapproximation method. The main
4921 difference from the original method is that density is used as cost
4922 function. Returns a pointer to the BDD of the subset if
4923 successful. NULL if the procedure runs out of memory. The parameter
4924 numVars is the maximum number of variables to be used in minterm
4925 calculation. The optimal number should be as close as possible to
4926 the size of the support of f. However, it is safe to pass the value
4927 returned by Cudd_ReadSize for numVars when the number of variables
4929 overflow. If a 0 parameter is passed then the procedure will compute
4930 a value which will avoid overflow but will cause underflow with 2046
4931 variables or more.
4932 <p>
4935 <p>
4940 </code>
4942 <dt><pre>
4944 int * <I></I>
4949 )
4950 </pre>
4951 <dd> Finds the variables on which a set of DDs depends.
4952 The set must contain either BDDs and ADDs, or ZDDs.
4953 Returns an index array of the variables if successful; NULL otherwise.
4954 <p>
4957 <p>
4962 </code>
4964 <dt><pre>
4966 int <I></I>
4971 )
4972 </pre>
4973 <dd> Counts the variables on which a set of DDs depends.
4974 The set must contain either BDDs and ADDs, or ZDDs.
4975 Returns the number of the variables if successful; CUDD_OUT_OF_MEM
4976 otherwise.
4977 <p>
4980 <p>
4984 </code>
4986 <dt><pre>
4988 DdNode * <I></I>
4993 )
4994 </pre>
4995 <dd> Finds the variables on which a set of DDs depends.
4996 The set must contain either BDDs and ADDs, or ZDDs.
4997 Returns a BDD consisting of the product of the variables if
4998 successful; NULL otherwise.
4999 <p>
5002 <p>
5006 </code>
5008 <dt><pre>
5010 DdNode * <I></I>
5017 )
5018 </pre>
5020 substitutes the solution components for the unknowns of F and returns
5021 the resulting BDD for F.
5022 <p>
5025 <p>
5028 </code>
5030 <dt><pre>
5032 DdNode * <I></I>
5038 )
5039 </pre>
5040 <dd> This function generates a BDD for the function x==y.
5043 The BDD is built bottom-up.
5046 <p>
5049 <p>
5052 </code>
5054 <dt><pre>
5056 DdNode * <I></I>
5063 )
5064 </pre>
5068 The BDD is built bottom-up.
5071 Argument z is not used by Cudd_Xgty: it is included to make it
5072 call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.
5073 <p>
5076 <p>
5081 </code>
5083 <dt><pre>
5085 DdNode * <I></I>
5090 )
5091 </pre>
5092 <dd> Returns NULL if not a terminal case; f op g otherwise,
5093 where f op g is f if f==g; background if f!=g.
5094 <p>
5097 <p>
5100 </code>
5102 <dt><pre>
5104 DdNode * <I></I>
5110 )
5111 </pre>
5112 <dd> Applies op to the corresponding discriminants of f and g.
5113 Returns a pointer to the result if succssful; NULL otherwise.
5114 <p>
5117 <p>
5136 </code>
5138 <dt><pre>
5140 DdNode * <I></I>
5146 )
5147 </pre>
5148 <dd> Converts an ADD to a BDD by replacing all
5149 discriminants greater than or equal to lower and less than or equal to
5151 the resulting BDD if successful; NULL otherwise.
5152 <p>
5155 <p>
5161 </code>
5163 <dt><pre>
5165 DdNode * <I></I>
5170 )
5171 </pre>
5172 <dd> Converts an ADD to a BDD by replacing all
5174 discriminants with 0. The i-th bit refers to the integer
5175 representation of the leaf value. If the value is has a fractional
5176 part, it is ignored. Repeated calls to this procedure allow one to
5177 transform an integer-valued ADD into an array of BDDs, one for each
5178 bit of the leaf values. Returns a pointer to the resulting BDD if
5179 successful; NULL otherwise.
5180 <p>
5183 <p>
5188 </code>
5190 <dt><pre>
5192 DdNode * <I></I>
5196 )
5197 </pre>
5198 <dd> Converts an ADD to a BDD by replacing all
5200 resulting BDD if successful; NULL otherwise.
5201 <p>
5204 <p>
5210 </code>
5212 <dt><pre>
5214 DdNode * <I></I>
5219 )
5220 </pre>
5221 <dd> Converts an ADD to a BDD by replacing all
5222 discriminants STRICTLY greater than value with 1, and all other
5223 discriminants with 0. Returns a pointer to the resulting BDD if
5224 successful; NULL otherwise.
5225 <p>
5228 <p>
5234 </code>
5236 <dt><pre>
5238 DdNode * <I></I>
5243 )
5244 </pre>
5245 <dd> Converts an ADD to a BDD by replacing all
5246 discriminants greater than or equal to value with 1, and all other
5247 discriminants with 0. Returns a pointer to the resulting BDD if
5248 successful; NULL otherwise.
5249 <p>
5252 <p>
5258 </code>
5260 <dt><pre>
5262 DdNode * <I></I>
5266 )
5267 </pre>
5268 <dd> Computes the complement of an ADD a la C language: The
5270 Returns a pointer to the resulting ADD if successful; NULL otherwise.
5271 <p>
5274 <p>
5277 </code>
5279 <dt><pre>
5281 DdNode * <I></I>
5287 )
5288 </pre>
5289 <dd> Substitutes g for x_v in the ADD for f. v is the index of the
5291 the corresponding projection function to the recursive procedure, so
5292 that the cache may be used. Returns the composed ADD if successful;
5293 NULL otherwise.
5294 <p>
5297 <p>
5300 </code>
5302 <dt><pre>
5304 DdNode * <I></I>
5310 )
5311 </pre>
5312 <dd> Computes the cube of an array of ADD variables. If
5313 non-null, the phase argument indicates which literal of each
5314 variable should appear in the cube. If phase[i] is nonzero, then the
5315 positive literal is used. If phase is NULL, the cube is positive unate.
5316 Returns a pointer to the result if successful; NULL otherwise.
5317 <p>
5320 <p>
5323 </code>
5325 <dt><pre>
5327 DdNode * <I></I>
5332 )
5333 </pre>
5335 ADD. List of special cases:
5336 <ul>
5342 </ul>
5343 Returns a pointer to the result if successful; NULL otherwise.
5344 <p>
5347 <p>
5350 </code>
5352 <dt><pre>
5354 DdNode * <I></I>
5358 )
5359 </pre>
5360 <dd> Retrieves the ADD for constant c if it already
5361 exists, or creates a new ADD. Returns a pointer to the
5362 ADD if successful; NULL otherwise.
5363 <p>
5366 <p>
5370 </code>
5372 <dt><pre>
5374 DdNode * <I></I>
5379 )
5380 </pre>
5381 <dd> Returns NULL if not a terminal case; f op g otherwise,
5382 where f op g is plusinfinity if f=g; min(f,g) if f!=g.
5383 <p>
5386 <p>
5389 </code>
5391 <dt><pre>
5393 DdNode * <I></I>
5398 )
5399 </pre>
5400 <dd> Integer and floating point division. Returns NULL if not
5401 a terminal case; f / g otherwise.
5402 <p>
5405 <p>
5408 </code>
5410 <dt><pre>
5412 DdNode * <I></I>
5417 )
5418 </pre>
5421 or may not be constant) or DD_NON_CONSTANT. If f is identically 0,
5422 the check is assumed to be successful, and the background value is
5423 returned. No new nodes are created.
5424 <p>
5427 <p>
5431 </code>
5433 <dt><pre>
5435 DdNode * <I></I>
5440 )
5441 </pre>
5442 <dd> Abstracts all the variables in cube from f by summing
5443 over all possible values taken by the variables. Returns the
5444 abstracted ADD.
5445 <p>
5448 <p>
5453 </code>
5455 <dt><pre>
5457 DdNode * <I></I>
5461 )
5462 </pre>
5463 <dd> Returns a pointer to a constant ADD.
5464 <p>
5467 <p>
5469 <dt><pre>
5471 DdNode * <I></I>
5475 )
5476 </pre>
5477 <dd> Returns a pointer to a constant ADD.
5478 <p>
5481 <p>
5483 <dt><pre>
5485 DdNode * <I></I>
5491 )
5492 </pre>
5493 <dd> Given a vector of ADDs, creates a new ADD by substituting the
5494 ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted
5495 for the x_v and vectorOff the ADDs to be substituted for x_v'. There should
5496 be an entry in vector for each variable in the manager. If no substitution
5497 is sought for a given variable, the corresponding projection function should
5498 be specified in the vector. This function implements simultaneous
5499 composition. Returns a pointer to the resulting ADD if successful; NULL
5500 otherwise.
5501 <p>
5504 <p>
5511 </code>
5513 <dt><pre>
5515 DdNode * <I></I>
5521 )
5522 </pre>
5523 <dd> Computes the Hamming distance ADD. Returns an ADD that
5524 gives the Hamming distance between its two arguments if successful;
5525 NULL otherwise. The two vectors xVars and yVars identify the variables
5526 that form the two arguments.
5527 <p>
5530 <p>
5532 <dt><pre>
5534 int <I></I>
5552 )
5553 </pre>
5554 <dd> Reads in a matrix in the format of the Harwell-Boeing
5555 benchmark suite. The variables are ordered as follows:
5556 <blockquote>
5558 </blockquote>
5559 0 is the most significant bit. On input, nx and ny hold the numbers
5560 of row and column variables already in existence. On output, they
5561 hold the numbers of row and column variables actually used by the
5562 matrix. m and n are set to the numbers of rows and columns of the
5563 matrix. Their values on input are immaterial. Returns 1 on
5564 success; 0 otherwise. The ADD for the sparse matrix is returned in
5566 <p>
5569 <p>
5573 </code>
5575 <dt><pre>
5577 DdNode * <I></I>
5583 )
5584 </pre>
5586 Returns a pointer to the resulting ADD (which may or may not be
5587 constant) or DD_NON_CONSTANT. No new nodes are created. This function
5588 can be used, for instance, to check that g has a constant value
5589 (specified by h) whenever f is 1. If the constant value is unknown,
5590 then one should use Cudd_addEvalConst.
5591 <p>
5594 <p>
5599 </code>
5601 <dt><pre>
5603 DdNode * <I></I>
5609 )
5610 </pre>
5611 <dd> Implements ITE(f,g,h). This procedure assumes that f is
5613 otherwise.
5614 <p>
5617 <p>
5622 </code>
5624 <dt><pre>
5626 DdNode * <I></I>
5631 )
5632 </pre>
5633 <dd> Produces an ADD from another ADD by replacing all
5635 discriminants with 0. The i-th bit refers to the integer
5636 representation of the leaf value. If the value is has a fractional
5637 part, it is ignored. Repeated calls to this procedure allow one to
5638 transform an integer-valued ADD into an array of ADDs, one for each
5639 bit of the leaf values. Returns a pointer to the resulting ADD if
5640 successful; NULL otherwise.
5641 <p>
5644 <p>
5647 </code>
5649 <dt><pre>
5651 DdNode * <I></I>
5655 )
5656 </pre>
5657 <dd> Retrieves the ADD variable with index i if it already
5658 exists, or creates a new ADD variable. Returns a pointer to the
5659 variable if successful; NULL otherwise. An ADD variable differs from
5660 a BDD variable because it points to the arithmetic zero, instead of
5661 having a complement pointer to 1.
5662 <p>
5665 <p>
5671 </code>
5673 <dt><pre>
5675 int <I></I>
5680 )
5681 </pre>
5683 No new nodes are created. This procedure works for arbitrary ADDs.
5685 <p>
5688 <p>
5693 </code>
5695 <dt><pre>
5697 DdNode * <I></I>
5701 )
5702 </pre>
5703 <dd> Natural logarithm of an ADDs. Returns NULL
5704 if not a terminal case; log(f) otherwise. The discriminants of f must
5705 be positive double's.
5706 <p>
5709 <p>
5712 </code>
5714 <dt><pre>
5716 DdNode * <I></I>
5723 )
5724 </pre>
5725 <dd> Calculates the product of two matrices, A and B,
5726 represented as ADDs. This procedure implements the quasiring multiplication
5727 algorithm. A is assumed to depend on variables x (rows) and z
5728 (columns). B is assumed to depend on variables z (rows) and y
5729 (columns). The product of A and B then depends on x (rows) and y
5730 (columns). Only the z variables have to be explicitly identified;
5731 they are the "summation" variables. Returns a pointer to the
5732 result if successful; NULL otherwise.
5733 <p>
5736 <p>
5741 </code>
5743 <dt><pre>
5745 DdNode * <I></I>
5750 )
5751 </pre>
5752 <dd> Integer and floating point max for Cudd_addApply.
5753 Returns NULL if not a terminal case; max(f,g) otherwise.
5754 <p>
5757 <p>
5760 </code>
5762 <dt><pre>
5764 DdNode * <I></I>
5769 )
5770 </pre>
5771 <dd> Integer and floating point min for Cudd_addApply.
5772 Returns NULL if not a terminal case; min(f,g) otherwise.
5773 <p>
5776 <p>
5779 </code>
5781 <dt><pre>
5783 DdNode * <I></I>
5788 )
5789 </pre>
5790 <dd> Integer and floating point subtraction. Returns NULL if
5791 not a terminal case; f - g otherwise.
5792 <p>
5795 <p>
5798 </code>
5800 <dt><pre>
5802 DdNode * <I></I>
5807 )
5808 </pre>
5809 <dd> Applies op to the discriminants of f.
5810 Returns a pointer to the result if succssful; NULL otherwise.
5811 <p>
5814 <p>
5818 </code>
5820 <dt><pre>
5822 DdNode * <I></I>
5827 )
5828 </pre>
5830 if not a terminal case; f NAND g otherwise.
5831 <p>
5834 <p>
5837 </code>
5839 <dt><pre>
5841 DdNode * <I></I>
5845 )
5846 </pre>
5847 <dd> Computes the additive inverse of an ADD. Returns a pointer
5848 to the result if successful; NULL otherwise.
5849 <p>
5852 <p>
5855 </code>
5857 <dt><pre>
5859 DdNode * <I></I>
5863 )
5864 </pre>
5865 <dd> Creates a new ADD variable. The new variable has an
5866 index equal to the largest previous index plus 1 and is positioned at
5867 the specified level in the order. Returns a pointer to the new
5868 variable if successful; NULL otherwise.
5869 <p>
5872 <p>
5877 </code>
5879 <dt><pre>
5881 DdNode * <I></I>
5884 )
5885 </pre>
5886 <dd> Creates a new ADD variable. The new variable has an
5887 index equal to the largest previous index plus 1. Returns a
5888 pointer to the new variable if successful; NULL otherwise.
5889 An ADD variable differs from a BDD variable because it points to the
5890 arithmetic zero, instead of having a complement pointer to 1.
5891 <p>
5894 <p>
5900 </code>
5902 <dt><pre>
5904 DdNode * <I></I>
5909 )
5910 </pre>
5913 should be an entry in vector for each variable in the manager.
5914 This function implements non-simultaneous composition. If any of the
5915 functions being composed depends on any of the variables being
5916 substituted, then the result depends on the order of composition,
5917 which in turn depends on the variable order: The variables farther from
5918 the roots in the order are substituted first.
5919 Returns a pointer to the resulting ADD if successful; NULL
5920 otherwise.
5921 <p>
5924 <p>
5929 </code>
5931 <dt><pre>
5933 DdNode * <I></I>
5938 )
5939 </pre>
5941 if not a terminal case; f NOR g otherwise.
5942 <p>
5945 <p>
5948 </code>
5950 <dt><pre>
5952 DdNode * <I></I>
5957 )
5958 </pre>
5960 conjunction with Cudd_addApply. Returns NULL if not a terminal
5961 case.
5962 <p>
5965 <p>
5968 </code>
5970 <dt><pre>
5972 DdNode * <I></I>
5977 )
5978 </pre>
5980 by taking the disjunction over all possible values taken by the
5981 variables. Returns the abstracted ADD if successful; NULL
5982 otherwise.
5983 <p>
5986 <p>
5990 </code>
5992 <dt><pre>
5994 DdNode * <I></I>
5999 )
6000 </pre>
6002 if not a terminal case; f OR g otherwise.
6003 <p>
6006 <p>
6009 </code>
6011 <dt><pre>
6013 DdNode * <I></I>
6019 )
6020 </pre>
6021 <dd> Takes the pointwise minimum of a matrix and the outer
6022 sum of two vectors. This procedure is used in the Floyd-Warshall
6023 all-pair shortest path algorithm. Returns a pointer to the result if
6024 successful; NULL otherwise.
6025 <p>
6028 <p>
6030 <dt><pre>
6032 DdNode * <I></I>
6037 )
6038 </pre>
6039 <dd> Given a permutation in array permut, creates a new ADD
6040 with permuted variables. There should be an entry in array permut
6041 for each variable in the manager. The i-th entry of permut holds the
6042 index of the variable that is to substitute the i-th
6043 variable. Returns a pointer to the resulting ADD if successful; NULL
6044 otherwise.
6045 <p>
6048 <p>
6052 </code>
6054 <dt><pre>
6056 DdNode * <I></I>
6061 )
6062 </pre>
6063 <dd> Integer and floating point addition. Returns NULL if not
6064 a terminal case; f+g otherwise.
6065 <p>
6068 <p>
6071 </code>
6073 <dt><pre>
6075 int <I></I>
6092 )
6093 </pre>
6094 <dd> Reads in a sparse matrix specified in a simple format.
6095 The first line of the input contains the numbers of rows and columns.
6096 The remaining lines contain the elements of the matrix, one per line.
6097 Given a background value
6098 (specified by the background field of the manager), only the values
6099 different from it are explicitly listed. Each foreground element is
6100 described by two integers, i.e., the row and column number, and a
6101 real number, i.e., the value.<p>
6102 Cudd_addRead produces an ADD that depends on two sets of variables: x
6106 The variables may already exist or may be created by the function.
6107 The index of x[i] is bx+i*sx, and the index of y[i] is by+i*sy.<p>
6108 On input, nx and ny hold the numbers
6109 of row and column variables already in existence. On output, they
6110 hold the numbers of row and column variables actually used by the
6111 matrix. When Cudd_addRead creates the variable arrays,
6112 the index of x[i] is bx+i*sx, and the index of y[i] is by+i*sy.
6113 When some variables already exist Cudd_addRead expects the indices
6114 of the existing x variables to be bx+i*sx, and the indices of the
6115 existing y variables to be by+i*sy.<p>
6116 m and n are set to the numbers of rows and columns of the
6117 matrix. Their values on input are immaterial.
6118 The ADD for the
6121 <p>
6124 variables. m and n are set to the numbers of rows and columns. x and y
6125 are possibly extended to represent the array of row and column
6126 variables. Similarly for xn and yn_, which hold on return from
6127 Cudd_addRead the complements of the row and column variables.
6128 <p>
6132 </code>
6134 <dt><pre>
6136 DdNode * <I></I>
6143 )
6144 </pre>
6145 <dd> Builds an ADD for the residue modulo m of an n-bit
6146 number. The modulus must be at least 2, and the number of bits at
6147 least 1. Parameter options specifies whether the MSB should be on top
6148 or the LSB; and whther the number whose residue is computed is in
6149 two's complement notation or not. The macro CUDD_RESIDUE_DEFAULT
6150 specifies LSB on top and unsigned number. The macro CUDD_RESIDUE_MSB
6151 specifies MSB on top, and the macro CUDD_RESIDUE_TC specifies two's
6152 complement residue. To request MSB on top and two's complement residue
6153 simultaneously, one can OR the two macros:
6154 CUDD_RESIDUE_MSB | CUDD_RESIDUE_TC.
6155 Cudd_addResidue returns a pointer to the resulting ADD if successful;
6156 NULL otherwise.
6157 <p>
6160 <p>
6162 <dt><pre>
6164 DdNode * <I></I>
6169 )
6170 </pre>
6171 <dd> ADD restrict according to Coudert and Madre's algorithm
6172 (ICCAD90). Returns the restricted ADD if successful; otherwise NULL.
6173 If application of restrict results in an ADD larger than the input
6174 ADD, the input ADD is returned.
6175 <p>
6178 <p>
6182 </code>
6184 <dt><pre>
6186 DdNode * <I></I>
6191 )
6192 </pre>
6193 <dd> Rounds off the discriminants of an ADD. The discriminants are
6194 rounded off to N digits after the decimal. Returns a pointer to the result
6195 ADD if successful; NULL otherwise.
6196 <p>
6199 <p>
6201 <dt><pre>
6203 DdNode * <I></I>
6208 )
6209 </pre>
6210 <dd> Computes an n ADD where the discriminants are the
6211 multiplicative inverses of the corresponding discriminants of the
6212 argument ADD. Returns a pointer to the resulting ADD in case of
6213 success. Returns NULL if any discriminants smaller than epsilon is
6214 encountered.
6215 <p>
6218 <p>
6220 <dt><pre>
6222 DdNode * <I></I>
6227 )
6228 </pre>
6230 Returns NULL if not a terminal case; f op g otherwise.
6231 <p>
6234 <p>
6237 </code>
6239 <dt><pre>
6241 DdNode * <I></I>
6248 )
6249 </pre>
6250 <dd> Swaps two sets of variables of the same size (x and y) in
6251 the ADD f. The size is given by n. The two sets of variables are
6252 assumed to be disjoint. Returns a pointer to the resulting ADD if
6253 successful; NULL otherwise.
6254 <p>
6257 <p>
6261 </code>
6263 <dt><pre>
6265 DdNode * <I></I>
6270 )
6271 </pre>
6273 Returns NULL if not a terminal case; f op g otherwise.
6274 <p>
6277 <p>
6280 </code>
6282 <dt><pre>
6284 DdNode * <I></I>
6291 )
6292 </pre>
6293 <dd> Calculates the product of two matrices, A and B,
6294 represented as ADDs, using the CMU matrix by matrix multiplication
6295 procedure by Clarke et al.. Matrix A has x's as row variables and z's
6296 as column variables, while matrix B has z's as row variables and y's
6297 as column variables. Returns the pointer to the result if successful;
6298 NULL otherwise. The resulting matrix has x's as row variables and y's
6299 as column variables.
6300 <p>
6303 <p>
6306 </code>
6308 <dt><pre>
6310 DdNode * <I></I>
6315 )
6316 </pre>
6317 <dd> Integer and floating point multiplication. Returns NULL
6318 if not a terminal case; f * g otherwise. This function can be used also
6320 <p>
6323 <p>
6326 </code>
6328 <dt><pre>
6330 DdNode * <I></I>
6337 )
6338 </pre>
6339 <dd> Implements the semiring multiplication algorithm used in
6340 the triangulation step for the shortest path computation. f
6341 is assumed to depend on variables x (rows) and z (columns). g is
6342 assumed to depend on variables z (rows) and y (columns). The product
6343 of f and g then depends on x (rows) and y (columns). Only the z
6344 variables have to be explicitly identified; they are the
6345 "abstraction" variables. Returns a pointer to the result if
6346 successful; NULL otherwise.
6347 <p>
6350 <p>
6354 </code>
6356 <dt><pre>
6358 DdNode * <I></I>
6363 )
6364 </pre>
6365 <dd> Abstracts all the variables in cube from f by taking
6366 the product over all possible values taken by the variable. Returns
6367 the abstracted ADD if successful; NULL otherwise.
6368 <p>
6371 <p>
6376 </code>
6378 <dt><pre>
6380 DdNode * <I></I>
6385 )
6386 </pre>
6389 should be an entry in vector for each variable in the manager.
6390 If no substitution is sought for a given variable, the corresponding
6391 projection function should be specified in the vector.
6392 This function implements simultaneous composition.
6393 Returns a pointer to the resulting ADD if successful; NULL
6394 otherwise.
6395 <p>
6398 <p>
6404 </code>
6406 <dt><pre>
6408 DdNode * <I></I>
6414 )
6415 </pre>
6416 <dd> Generates a Walsh matrix in ADD form. Returns a pointer
6417 to the matrixi if successful; NULL otherwise.
6418 <p>
6421 <p>
6423 <dt><pre>
6425 DdNode * <I></I>
6431 )
6432 </pre>
6433 <dd> This function generates an ADD for the function x==y.
6436 The ADD is built bottom-up.
6439 <p>
6442 <p>
6445 </code>
6447 <dt><pre>
6449 DdNode * <I></I>
6454 )
6455 </pre>
6457 if not a terminal case; f XNOR g otherwise.
6458 <p>
6461 <p>
6464 </code>
6466 <dt><pre>
6468 DdNode * <I></I>
6473 )
6474 </pre>
6476 if not a terminal case; f XOR g otherwise.
6477 <p>
6480 <p>
6483 </code>
6485 <dt><pre>
6487 DdNode * <I></I>
6493 )
6494 </pre>
6495 <dd> Rearranges a set of variables in the BDD B. The size of
6496 the set is given by n. This procedure is intended for the
6497 `randomization' of the priority functions. Returns a pointer to the
6498 BDD if successful; NULL otherwise.
6499 <p>
6502 <p>
6509 </code>
6511 <dt><pre>
6513 DdNode * <I></I>
6520 )
6521 </pre>
6522 <dd> Takes the AND of two BDDs and simultaneously abstracts
6523 the variables in cube. The variables are existentially abstracted.
6524 Returns a pointer to the result is successful; NULL otherwise.
6525 In particular, if the number of new nodes created exceeds
6527 <p>
6530 <p>
6533 </code>
6535 <dt><pre>
6537 DdNode * <I></I>
6543 )
6544 </pre>
6545 <dd> Takes the AND of two BDDs and simultaneously abstracts
6546 the variables in cube. The variables are existentially abstracted.
6547 Returns a pointer to the result is successful; NULL otherwise.
6548 Cudd_bddAndAbstract implements the semiring matrix multiplication
6549 algorithm for the boolean semiring.
6550 <p>
6553 <p>
6558 </code>
6560 <dt><pre>
6562 DdNode * <I></I>
6568 )
6569 </pre>
6570 <dd> Computes the conjunction of two BDDs f and g. Returns a
6571 pointer to the resulting BDD if successful; NULL if the intermediate
6573 required.
6574 <p>
6577 <p>
6580 </code>
6582 <dt><pre>
6584 DdNode * <I></I>
6589 )
6590 </pre>
6591 <dd> Computes the conjunction of two BDDs f and g. Returns a
6592 pointer to the resulting BDD if successful; NULL if the intermediate
6593 result blows up.
6594 <p>
6597 <p>
6608 </code>
6610 <dt><pre>
6612 int <I></I>
6617 )
6618 </pre>
6619 <dd> Performs two-way conjunctive decomposition of a
6620 BDD. This procedure owes its name to the use of supersetting to
6621 obtain an initial factor of the given function. Returns the number
6623 decomposition was found; 0 otherwise. The conjuncts produced by this
6624 procedure tend to be imbalanced.
6625 <p>
6628 The array is allocated by this function. It is the caller's responsibility
6629 to free it. On successful completion, the conjuncts are already
6630 referenced. If the function returns 0, the array for the conjuncts is
6631 not allocated. If the function returns 1, the only factor equals the
6632 function to be decomposed.
6633 <p>
6642 </code>
6644 <dt><pre>
6646 int <I></I>
6651 )
6652 </pre>
6653 <dd> Performs two-way disjunctive decomposition of a BDD.
6654 Returns the number of disjuncts produced, that is, 2 if successful;
6656 disjuncts produced by this procedure tend to be imbalanced.
6657 <p>
6660 The array is allocated by this function. It is the caller's responsibility
6661 to free it. On successful completion, the disjuncts are already
6662 referenced. If the function returns 0, the array for the disjuncts is
6663 not allocated. If the function returns 1, the only factor equals the
6664 function to be decomposed.
6665 <p>
6671 </code>
6673 <dt><pre>
6675 int <I></I>
6679 )
6680 </pre>
6681 <dd> This function sets a flag to prevent sifting of a
6683 variable index).
6684 <p>
6687 <p>
6690 </code>
6692 <dt><pre>
6694 DdNode * <I></I>
6699 )
6700 </pre>
6701 <dd> Computes the boolean difference of f with respect to the
6702 variable with index x. Returns the BDD of the boolean difference if
6703 successful; NULL otherwise.
6704 <p>
6707 <p>
6709 <dt><pre>
6711 DdNode ** <I></I>
6715 )
6716 </pre>
6717 <dd> Computes a vector of BDDs whose image equals a non-zero
6718 function.
6719 The result depends on the variable order. The i-th component of the vector
6720 depends only on the first i variables in the order. Each BDD in the vector
6721 is not larger than the BDD of the given characteristic function. This
6722 function is based on the description of char-to-vect in "Verification of
6723 Sequential Machines Using Boolean Functional Vectors" by O. Coudert, C.
6724 Berthet and J. C. Madre.
6725 Returns a pointer to an array containing the result if successful; NULL
6726 otherwise. The size of the array equals the number of variables in the
6727 manager. The components of the solution have their reference counts
6728 already incremented (unlike the results of most other functions in
6729 the package).
6730 <p>
6733 <p>
6736 </code>
6738 <dt><pre>
6740 DdNode * <I></I>
6748 )
6749 </pre>
6750 <dd> Approximates the conjunction of two BDDs f and g and
6751 simultaneously abstracts the variables in cube. The variables are
6752 existentially abstracted. Returns a pointer to the resulting BDD if
6753 successful; NULL if the intermediate result blows up.
6754 <p>
6757 <p>
6761 </code>
6763 <dt><pre>
6765 DdNode * <I></I>
6772 )
6773 </pre>
6774 <dd> Approximates the conjunction of two BDDs f and g. Returns a
6775 pointer to the resulting BDD if successful; NULL if the intermediate
6776 result blows up.
6777 <p>
6780 <p>
6783 </code>
6785 <dt><pre>
6787 DdNode * <I></I>
6793 )
6794 </pre>
6795 <dd> Finds a cube of f at minimum Hamming distance from the
6796 minterms of g. All the minterms of the cube are at the minimum
6797 distance. If the distance is 0, the cube belongs to the
6798 intersection of f and g. Returns the cube if successful; NULL
6799 otherwise.
6800 <p>
6803 <p>
6806 </code>
6808 <dt><pre>
6810 DdNode * <I></I>
6816 )
6817 </pre>
6818 <dd> Substitutes g for x_v in the BDD for f. v is the index of the
6819 variable to be substituted. Cudd_bddCompose passes the corresponding
6820 projection function to the recursive procedure, so that the cache may
6821 be used. Returns the composed BDD if successful; NULL otherwise.
6822 <p>
6825 <p>
6828 </code>
6830 <dt><pre>
6832 DdNode * <I></I>
6838 )
6839 </pre>
6840 <dd> Computes the cube of an array of BDD variables. If
6841 non-null, the phase argument indicates which literal of each
6842 variable should appear in the cube. If phase[i] is nonzero, then the
6843 positive literal is used. If phase is NULL, the cube is positive unate.
6844 Returns a pointer to the result if successful; NULL otherwise.
6845 <p>
6848 <p>
6853 </code>
6855 <dt><pre>
6857 DdNode ** <I></I>
6861 )
6862 </pre>
6863 <dd> BDD conjunctive decomposition as in McMillan's CAV96
6864 paper. The decomposition is canonical only for a given variable
6865 order. If canonicity is required, variable ordering must be disabled
6866 after the decomposition has been computed. Returns an array with one
6867 entry for each BDD variable in the manager if successful; otherwise
6868 NULL. The components of the solution have their reference counts
6869 already incremented (unlike the results of most other functions in
6870 the package.
6871 <p>
6874 <p>
6878 </code>
6880 <dt><pre>
6882 DdNode * <I></I>
6887 )
6888 </pre>
6889 <dd> Computes f constrain c (f @ c).
6890 Uses a canonical form: (f' @ c) = ( f @ c)'. (Note: this is not true
6891 for c.) List of special cases:
6892 <ul>
6899 </ul>
6900 Returns a pointer to the result if successful; NULL otherwise. Note that if
6901 F=(f1,...,fn) and reordering takes place while computing F @ c, then the
6902 image restriction property (Img(F,c) = Img(F @ c)) is lost.
6903 <p>
6906 <p>
6910 </code>
6912 <dt><pre>
6914 double <I></I>
6920 )
6921 </pre>
6922 <dd> Computes the correlation of f and g for given input
6923 probabilities. On input, prob[i] is supposed to contain the
6924 probability of the i-th input variable to be 1.
6925 If f == g, their correlation is 1. If f == g', their
6926 correlation is 0. Returns the probability that f and g have the same
6927 value. If it runs out of memory, returns (double)CUDD_OUT_OF_MEM. The
6928 correlation of f and the constant one gives the probability of f.
6929 <p>
6932 <p>
6935 </code>
6937 <dt><pre>
6939 double <I></I>
6944 )
6945 </pre>
6946 <dd> Computes the correlation of f and g. If f == g, their
6948 fraction of minterms in the ON-set of the EXNOR of f and g. If it
6949 runs out of memory, returns (double)CUDD_OUT_OF_MEM.
6950 <p>
6953 <p>
6955 <dd> <b>See Also</b> <code><a href="#Cudd_bddCorrelationWeights">Cudd_bddCorrelationWeights</a>
6956 </code>
6958 <dt><pre>
6960 DdNode * <I></I>
6965 )
6966 </pre>
6967 <dd> Existentially abstracts all the variables in cube from f.
6968 Returns the abstracted BDD if successful; NULL otherwise.
6969 <p>
6972 <p>
6976 </code>
6978 <dt><pre>
6980 int <I></I>
6985 )
6986 </pre>
6987 <dd> Performs two-way conjunctive decomposition of a
6988 BDD. This procedure owes its name to the fact tht it generalizes the
6989 decomposition based on the cofactors with respect to one
6990 variable. Returns the number of conjuncts produced, that is, 2 if
6992 otherwise. The conjuncts produced by this procedure tend to be
6993 balanced.
6994 <p>
6997 The array is allocated by this function. It is the caller's responsibility
6998 to free it. On successful completion, the conjuncts are already
6999 referenced. If the function returns 0, the array for the conjuncts is
7000 not allocated. If the function returns 1, the only factor equals the
7001 function to be decomposed.
7002 <p>
7008 </code>
7010 <dt><pre>
7012 int <I></I>
7017 )
7018 </pre>
7019 <dd> Performs two-way disjunctive decomposition of a BDD.
7020 Returns the number of disjuncts produced, that is, 2 if successful;
7022 disjuncts produced by this procedure tend to be balanced.
7023 <p>
7026 The array is allocated by this function. It is the caller's responsibility
7027 to free it. On successful completion, the disjuncts are already
7028 referenced. If the function returns 0, the array for the disjuncts is
7029 not allocated. If the function returns 1, the only factor equals the
7030 function to be decomposed.
7031 <p>
7037 </code>
7039 <dt><pre>
7041 DdNode * <I></I>
7046 )
7047 </pre>
7048 <dd> Computes a function included in the intersection of f and
7049 g. (That is, a witness that the intersection is not empty.)
7050 Cudd_bddIntersect tries to build as few new nodes as possible. If the
7051 only result of interest is whether f and g intersect,
7052 Cudd_bddLeq should be used instead.
7053 <p>
7056 <p>
7060 </code>
7062 <dt><pre>
7064 DdNode * <I></I>
7071 )
7072 </pre>
7073 <dd> This function generates a BDD for the function
7076 The number of variables N should be sufficient to represent the bounds;
7077 otherwise, the bounds are truncated to their N least significant bits.
7079 are finally conjoined.
7080 <p>
7083 <p>
7086 </code>
7088 <dt><pre>
7090 int <I></I>
7094 )
7095 </pre>
7097 the variable's type is present state; 0 if the variable exists but is
7098 not a present state; -1 if the variable does not exist.
7099 <p>
7102 <p>
7107 </code>
7109 <dt><pre>
7111 int <I></I>
7115 )
7116 </pre>
7118 the variable's type is primary input; 0 if the variable exists but is
7119 not a primary input; -1 if the variable does not exist.
7120 <p>
7123 <p>
7128 </code>
7130 <dt><pre>
7132 int <I></I>
7136 )
7137 </pre>
7139 the variable's type is present state; 0 if the variable exists but is
7140 not a present state; -1 if the variable does not exist.
7141 <p>
7144 <p>
7149 </code>
7151 <dt><pre>
7153 int <I></I>
7159 )
7160 </pre>
7161 <dd> Determines whether a given variable is essential with a
7163 and f-->x_id, or if phase == 0 and f-->x_id'.
7164 <p>
7167 <p>
7170 </code>
7172 <dt><pre>
7174 int <I></I>
7178 )
7179 </pre>
7180 <dd> Checks whether a variable is set to be in a hard group. This
7181 function is used for lazy sifting. Returns 1 if the variable is marked
7182 to be in a hard group; 0 if the variable exists, but it is not marked to be
7183 in a hard group; -1 if the variable does not exist.
7184 <p>
7187 <p>
7190 </code>
7192 <dt><pre>
7194 int <I></I>
7198 )
7199 </pre>
7200 <dd> Checks whether a variable is set to be grouped. This
7201 function is used for lazy sifting.
7202 <p>
7205 <p>
7207 <dt><pre>
7209 int <I></I>
7213 )
7214 </pre>
7215 <dd> Checks whether a variable is set to be ungrouped. This
7216 function is used for lazy sifting. Returns 1 if the variable is marked
7217 to be ungrouped; 0 if the variable exists, but it is not marked to be
7218 ungrouped; -1 if the variable does not exist.
7219 <p>
7222 <p>
7224 <dd> <b>See Also</b> <code><a href="#Cudd_bddSetVarToBeUngrouped">Cudd_bddSetVarToBeUngrouped</a>
7225 </code>
7227 <dt><pre>
7229 DdNode * <I></I>
7234 )
7235 </pre>
7236 <dd> Computes a BDD in the interval between L and U with a
7237 simple sum-of-produuct cover. This procedure is similar to
7238 Cudd_zddIsop, but it does not return the ZDD for the cover. Returns
7239 a pointer to the BDD if successful; NULL otherwise.
7240 <p>
7243 <p>
7246 </code>
7248 <dt><pre>
7250 DdNode * <I></I>
7256 )
7257 </pre>
7258 <dd> Implements ITEconstant(f,g,h). Returns a pointer to the
7259 resulting BDD (which may or may not be constant) or DD_NON_CONSTANT.
7260 No new nodes are created.
7261 <p>
7264 <p>
7270 </code>
7272 <dt><pre>
7274 int <I></I>
7279 )
7280 </pre>
7281 <dd> Performs two-way conjunctive decomposition of a
7282 BDD. This procedure owes its name to the iterated use of
7283 supersetting to obtain a factor of the given function. Returns the
7285 meaningful decomposition was found; 0 otherwise. The conjuncts
7286 produced by this procedure tend to be imbalanced.
7287 <p>
7290 The array is allocated by this function. It is the caller's responsibility
7291 to free it. On successful completion, the conjuncts are already
7292 referenced. If the function returns 0, the array for the conjuncts is
7293 not allocated. If the function returns 1, the only factor equals the
7294 function to be decomposed.
7295 <p>
7304 </code>
7306 <dt><pre>
7308 int <I></I>
7313 )
7314 </pre>
7315 <dd> Performs two-way disjunctive decomposition of a BDD.
7316 Returns the number of disjuncts produced, that is, 2 if successful;
7318 disjuncts produced by this procedure tend to be imbalanced.
7319 <p>
7322 The array is allocated by this function. It is the caller's responsibility
7323 to free it. On successful completion, the disjuncts are already
7324 referenced. If the function returns 0, the array for the disjuncts is
7325 not allocated. If the function returns 1, the only factor equals the
7326 function to be decomposed.
7327 <p>
7333 </code>
7335 <dt><pre>
7337 DdNode * <I></I>
7343 )
7344 </pre>
7345 <dd> Implements ITE(f,g,h). Returns a pointer to the
7346 resulting BDD if successful; NULL if the intermediate result blows
7347 up.
7348 <p>
7351 <p>
7356 </code>
7358 <dt><pre>
7360 DdNode * <I></I>
7364 )
7365 </pre>
7366 <dd> Retrieves the BDD variable with index i if it already
7367 exists, or creates a new BDD variable. Returns a pointer to the
7368 variable if successful; NULL otherwise.
7369 <p>
7372 <p>
7378 </code>
7380 <dt><pre>
7382 DdNode * <I></I>
7387 )
7388 </pre>
7389 <dd> Performs safe minimization of a BDD. Given the BDD
7394 of the result is guaranteed not to exceed the size of
7396 al.. Returns a pointer to the result if successful; NULL
7397 otherwise.
7398 <p>
7401 <p>
7404 </code>
7406 <dt><pre>
7408 int <I></I>
7414 )
7415 </pre>
7416 <dd> Tells whether f is less than of equal to G unless D is
7418 of equal to G, and 0 otherwise. No new nodes are created.
7419 <p>
7422 <p>
7427 </code>
7429 <dt><pre>
7431 int <I></I>
7436 )
7437 </pre>
7439 No new nodes are created.
7440 <p>
7443 <p>
7447 </code>
7449 <dt><pre>
7451 DdNode * <I></I>
7456 )
7457 </pre>
7458 <dd> Computes the intesection of two sets of literals
7459 represented as BDDs. Each set is represented as a cube of the
7460 literals in the set. The empty set is represented by the constant 1.
7461 No variable can be simultaneously present in both phases in a set.
7462 Returns a pointer to the BDD representing the intersected sets, if
7463 successful; NULL otherwise.
7464 <p>
7467 <p>
7469 <dt><pre>
7471 DdNode * <I></I>
7476 )
7477 </pre>
7478 <dd> Expands cube to a prime implicant of f. Returns the prime
7479 if successful; NULL otherwise. In particular, NULL is returned if cube
7480 is not a real cube or is not an implicant of f.
7481 <p>
7484 <p>
7486 <dt><pre>
7488 DdNode * <I></I>
7493 )
7494 </pre>
7497 otherwise.
7498 <p>
7501 <p>
7506 </code>
7508 <dt><pre>
7510 DdNode * <I></I>
7515 )
7516 </pre>
7517 <dd> Computes f non-polluting-and g. The non-polluting AND
7518 of f and g is a hybrid of AND and Restrict. From Restrict, this
7519 operation takes the idea of existentially quantifying the top
7520 variable of the second operand if it does not appear in the first.
7521 Therefore, the variables that appear in the result also appear in f.
7522 For the rest, the function behaves like AND. Since the two operands
7523 play different roles, non-polluting AND is not commutative.
7525 Returns a pointer to the result if successful; NULL otherwise.
7526 <p>
7529 <p>
7533 </code>
7535 <dt><pre>
7537 DdNode * <I></I>
7542 )
7543 </pre>
7544 <dd> Computes the NAND of two BDDs f and g. Returns a
7545 pointer to the resulting BDD if successful; NULL if the intermediate
7546 result blows up.
7547 <p>
7550 <p>
7559 </code>
7561 <dt><pre>
7563 DdNode * <I></I>
7567 )
7568 </pre>
7569 <dd> Creates a new BDD variable. The new variable has an
7570 index equal to the largest previous index plus 1 and is positioned at
7571 the specified level in the order. Returns a pointer to the new
7572 variable if successful; NULL otherwise.
7573 <p>
7576 <p>
7581 </code>
7583 <dt><pre>
7585 DdNode * <I></I>
7588 )
7589 </pre>
7590 <dd> Creates a new BDD variable. The new variable has an
7591 index equal to the largest previous index plus 1. Returns a
7592 pointer to the new variable if successful; NULL otherwise.
7593 <p>
7596 <p>
7601 </code>
7603 <dt><pre>
7605 DdNode * <I></I>
7610 )
7611 </pre>
7612 <dd> Computes the NOR of two BDDs f and g. Returns a
7613 pointer to the resulting BDD if successful; NULL if the intermediate
7614 result blows up.
7615 <p>
7618 <p>
7627 </code>
7629 <dt><pre>
7631 DdNode * <I></I>
7636 )
7637 </pre>
7638 <dd> Computes the disjunction of two BDDs f and g. Returns a
7639 pointer to the resulting BDD if successful; NULL if the intermediate
7640 result blows up.
7641 <p>
7644 <p>
7653 </code>
7655 <dt><pre>
7657 DdNode * <I></I>
7662 )
7663 </pre>
7664 <dd> Given a permutation in array permut, creates a new BDD
7665 with permuted variables. There should be an entry in array permut
7666 for each variable in the manager. The i-th entry of permut holds the
7667 index of the variable that is to substitute the i-th variable.
7668 Returns a pointer to the resulting BDD if successful; NULL
7669 otherwise.
7670 <p>
7673 <p>
7677 </code>
7679 <dt><pre>
7681 DdNode ** <I></I>
7688 )
7689 </pre>
7690 <dd> Picks k on-set minterms evenly distributed from given DD.
7694 built by this procedure may not be contained in
7696 pointer to it if successful; NULL otherwise. There are three reasons
7697 why the procedure may fail:
7698 <ul>
7699 <li> It may run out of memory;
7702 </ul>
7703 <p>
7706 <p>
7710 </code>
7712 <dt><pre>
7714 int <I></I>
7719 )
7720 </pre>
7721 <dd> Picks one on-set cube randomly from the given DD. The
7722 cube is written into an array of characters. The array must have at
7723 least as many entries as there are variables. Returns 1 if
7724 successful; 0 otherwise.
7725 <p>
7728 <p>
7731 </code>
7733 <dt><pre>
7735 DdNode * <I></I>
7741 )
7742 </pre>
7743 <dd> Picks one on-set minterm randomly from the given
7747 built by this procedure may not be contained in
7749 to it if successful; NULL otherwise. There are three reasons why the
7750 procedure may fail:
7751 <ul>
7752 <li> It may run out of memory;
7755 </ul>
7756 <p>
7759 <p>
7762 </code>
7764 <dt><pre>
7766 int <I></I>
7771 )
7772 </pre>
7773 <dd> Prints a sum of product cover for an incompletely
7774 specified function given by a lower bound and an upper bound. Each
7775 product is a prime implicant obtained by expanding the product
7776 corresponding to a path from node to the constant one. Uses the
7778 <p>
7781 <p>
7784 </code>
7786 <dt><pre>
7788 int <I></I>
7792 )
7793 </pre>
7794 <dd> Reads a corresponding pair index for a given index.
7795 These pair indices are present and next state variable. Returns the
7796 corresponding variable index if the variable exists; -1 otherwise.
7797 <p>
7800 <p>
7803 </code>
7805 <dt><pre>
7807 int <I></I>
7822 )
7823 </pre>
7824 <dd> Reads in a graph (without labels) given as an adjacency
7825 matrix. The first line of the input contains the numbers of rows and
7826 columns of the adjacency matrix. The remaining lines contain the arcs
7827 of the graph, one per line. Each arc is described by two integers,
7828 i.e., the row and column number, or the indices of the two endpoints.
7829 Cudd_bddRead produces a BDD that depends on two sets of variables: x
7833 indices.
7834 The variables may already exist or may be created by the function.
7835 The index of x[i] is bx+i*sx, and the index of y[i] is by+i*sy.<p>
7836 On input, nx and ny hold the numbers of row and column variables already
7837 in existence. On output, they hold the numbers of row and column
7838 variables actually used by the matrix. When Cudd_bddRead creates the
7839 variable arrays, the index of x[i] is bx+i*sx, and the index of
7840 y[i] is by+i*sy. When some variables already exist, Cudd_bddRead
7841 expects the indices of the existing x variables to be bx+i*sx, and the
7842 indices of the existing y variables to be by+i*sy.<p>
7843 m and n are set to the numbers of rows and columns of the
7844 matrix. Their values on input are immaterial. The BDD for the graph
7847 <p>
7850 variables. m and n are set to the numbers of rows and columns. x and y
7851 are possibly extended to represent the array of row and column
7852 variables.
7853 <p>
7857 </code>
7859 <dt><pre>
7861 void <I></I>
7864 )
7865 </pre>
7866 <dd> Disables realignment of ZDD order to BDD order.
7867 <p>
7870 <p>
7876 </code>
7878 <dt><pre>
7880 void <I></I>
7883 )
7884 </pre>
7885 <dd> Enables realignment of the BDD variable order to the
7886 ZDD variable order after the ZDDs have been reordered. The
7887 number of ZDD variables must be a multiple of the number of BDD
7888 variables for realignment to make sense. If this condition is not met,
7890 ratio of the two numbers. For the purpose of realignment, the ZDD
7893 is initially disabled.
7894 <p>
7897 <p>
7904 </code>
7906 <dt><pre>
7908 int <I></I>
7911 )
7912 </pre>
7914 enabled; 0 otherwise.
7915 <p>
7918 <p>
7924 </code>
7926 <dt><pre>
7928 int <I></I>
7932 )
7933 </pre>
7934 <dd> Resets a variable not to be grouped. This function is
7936 <p>
7939 <p>
7943 </code>
7945 <dt><pre>
7947 DdNode * <I></I>
7952 )
7953 </pre>
7954 <dd> BDD restrict according to Coudert and Madre's algorithm
7955 (ICCAD90). Returns the restricted BDD if successful; otherwise NULL.
7956 If application of restrict results in a BDD larger than the input
7957 BDD, the input BDD is returned.
7958 <p>
7961 <p>
7965 </code>
7967 <dt><pre>
7969 int <I></I>
7973 )
7974 </pre>
7975 <dd> Sets a variable type to next state. The variable type is
7977 <p>
7980 <p>
7985 </code>
7987 <dt><pre>
7989 int <I></I>
7994 )
7995 </pre>
7996 <dd> Sets a corresponding pair index for a given index.
7997 These pair indices are present and next state variable. Returns 1 if
7998 successful; 0 otherwise.
7999 <p>
8002 <p>
8005 </code>
8007 <dt><pre>
8009 int <I></I>
8013 )
8014 </pre>
8015 <dd> Sets a variable type to primary input. The variable type is
8017 <p>
8020 <p>
8025 </code>
8027 <dt><pre>
8029 int <I></I>
8033 )
8034 </pre>
8035 <dd> Sets a variable type to present state. The variable type is
8037 <p>
8040 <p>
8045 </code>
8047 <dt><pre>
8049 int <I></I>
8053 )
8054 </pre>
8055 <dd> Sets a variable to be a hard group. This function is used
8057 <p>
8060 <p>
8065 </code>
8067 <dt><pre>
8069 int <I></I>
8073 )
8074 </pre>
8075 <dd> Sets a variable to be grouped. This function is used for
8077 <p>
8080 <p>
8084 </code>
8086 <dt><pre>
8088 int <I></I>
8092 )
8093 </pre>
8094 <dd> Sets a variable to be ungrouped. This function is used
8096 <p>
8099 <p>
8101 <dd> <b>See Also</b> <code><a href="#Cudd_bddIsVarToBeUngrouped">Cudd_bddIsVarToBeUngrouped</a>
8102 </code>
8104 <dt><pre>
8106 DdNode * <I></I>
8111 )
8112 </pre>
8113 <dd> Finds a small BDD in a function interval. Given BDDs
8115 upper bound of a function interval, Cudd_bddSqueeze produces the BDD
8116 of a function within the interval with a small BDD. Returns a
8117 pointer to the result if successful; NULL otherwise.
8118 <p>
8121 <p>
8125 </code>
8127 <dt><pre>
8129 DdNode * <I></I>
8136 )
8137 </pre>
8138 <dd> Swaps two sets of variables of the same size (x and y)
8139 in the BDD f. The size is given by n. The two sets of variables are
8140 assumed to be disjoint. Returns a pointer to the resulting BDD if
8141 successful; NULL otherwise.
8142 <p>
8145 <p>
8149 </code>
8151 <dt><pre>
8153 DdNode * <I></I>
8158 )
8159 </pre>
8160 <dd> Convert a BDD from a manager to another one. The orders of the
8161 variables in the two managers may be different. Returns a
8162 pointer to the BDD in the destination manager if successful; NULL
8163 otherwise.
8164 <p>
8167 <p>
8169 <dt><pre>
8171 int <I></I>
8175 )
8176 </pre>
8177 <dd> This function resets the flag that prevents the sifting
8178 of a variable. In successive variable reorderings, the variable will
8179 NOT be skipped, that is, sifted. Initially all variables can be
8180 sifted. It is necessary to call this function only to re-enable
8182 otherwise (i.e., invalid variable index).
8183 <p>
8186 <p>
8189 </code>
8191 <dt><pre>
8193 DdNode * <I></I>
8198 )
8199 </pre>
8200 <dd> Universally abstracts all the variables in cube from f.
8201 Returns the abstracted BDD if successful; NULL otherwise.
8202 <p>
8205 <p>
8209 </code>
8211 <dt><pre>
8213 int <I></I>
8218 )
8219 </pre>
8220 <dd> Conjunctively decomposes one BDD according to a
8224 the sizes of the two conjuncts and to keep them small. Returns the
8226 meaningful decomposition was found; 0 otherwise.
8227 <p>
8230 The array is allocated by this function. It is the caller's responsibility
8231 to free it. On successful completion, the conjuncts are already
8232 referenced. If the function returns 0, the array for the conjuncts is
8233 not allocated. If the function returns 1, the only factor equals the
8234 function to be decomposed.
8235 <p>
8241 </code>
8243 <dt><pre>
8245 int <I></I>
8250 )
8251 </pre>
8252 <dd> Performs two-way disjunctive decomposition of a BDD
8256 the sizes of the two disjuncts and to keep them small. Returns the
8258 meaningful decomposition was found; 0 otherwise.
8259 <p>
8262 The array is allocated by this function. It is the caller's responsibility
8263 to free it. On successful completion, the disjuncts are already
8264 referenced. If the function returns 0, the array for the disjuncts is
8265 not allocated. If the function returns 1, the only factor equals the
8266 function to be decomposed.
8267 <p>
8273 </code>
8275 <dt><pre>
8277 int <I></I>
8281 )
8282 </pre>
8284 sifting. Initially all variables can be sifted. This function returns
8285 0 only if there has been a previous call to Cudd_bddBindVar for that
8286 variable not followed by a call to Cudd_bddUnbindVar. The function returns
8287 0 also in the case in which the index of the variable is out of bounds.
8288 <p>
8291 <p>
8295 </code>
8297 <dt><pre>
8299 int <I></I>
8304 )
8305 </pre>
8306 <dd> Checks whether a variable is dependent on others in a
8308 new nodes are created.
8309 <p>
8312 <p>
8314 <dt><pre>
8316 DdNode * <I></I>
8320 )
8321 </pre>
8322 <dd> Remaps the variables of a BDD using the default
8323 variable map. A typical use of this function is to swap two sets of
8324 variables. The variable map must be registered with Cudd_SetVarMap.
8325 Returns a pointer to the resulting BDD if successful; NULL
8326 otherwise.
8327 <p>
8330 <p>
8335 </code>
8337 <dt><pre>
8339 DdNode * <I></I>
8344 )
8345 </pre>
8346 <dd> Given a vector of BDDs, creates a new BDD by
8347 substituting the BDDs for the variables of the BDD f. There
8348 should be an entry in vector for each variable in the manager.
8349 If no substitution is sought for a given variable, the corresponding
8350 projection function should be specified in the vector.
8351 This function implements simultaneous composition.
8352 Returns a pointer to the resulting BDD if successful; NULL
8353 otherwise.
8354 <p>
8357 <p>
8362 </code>
8364 <dt><pre>
8366 DdNode * <I></I>
8371 )
8372 </pre>
8373 <dd> Computes the exclusive NOR of two BDDs f and g. Returns a
8374 pointer to the resulting BDD if successful; NULL if the intermediate
8375 result blows up.
8376 <p>
8379 <p>
8388 </code>
8390 <dt><pre>
8392 DdNode * <I></I>
8398 )
8399 </pre>
8400 <dd> Takes the exclusive OR of two BDDs and simultaneously abstracts
8401 the variables in cube. The variables are existentially abstracted. Returns a
8402 pointer to the result is successful; NULL otherwise.
8403 <p>
8406 <p>
8411 </code>
8413 <dt><pre>
8415 DdNode * <I></I>
8420 )
8421 </pre>
8422 <dd> Computes the exclusive OR of two BDDs f and g. Returns a
8423 pointer to the resulting BDD if successful; NULL if the intermediate
8424 result blows up.
8425 <p>
8428 <p>
8437 </code>
8439 <dt><pre>
8441 void <I></I>
8444 )
8445 </pre>
8446 <dd> Frees a DdTlcInfo Structure as well as the memory pointed
8447 by it.
8448 <p>
8451 <p>
8453 <dt><pre>
8455 DdNode * <I></I>
8460 )
8461 </pre>
8462 <dd> Substitutes a variable with its complement in a ZDD.
8463 returns a pointer to the result if successful; NULL otherwise.
8464 <p>
8467 <p>
8469 <dt><pre>
8471 DdNode * <I></I>
8475 )
8476 </pre>
8477 <dd> Computes a complement cover for a ZDD node. For lack of a
8478 better method, we first extract the function BDD from the ZDD cover,
8479 then make the complement of the ZDD cover from the complement of the
8480 BDD node by using ISOP. Returns a pointer to the resulting cover if
8481 successful; NULL otherwise. The result depends on current variable
8482 order.
8483 <p>
8486 <p>
8488 <dt><pre>
8490 double <I></I>
8494 )
8495 </pre>
8496 <dd> Counts the number of minterms of a ZDD. The result is
8497 returned as a double. If the procedure runs out of memory, it
8498 returns (double) CUDD_OUT_OF_MEM. This procedure is used in
8499 Cudd_zddCountMinterm.
8500 <p>
8503 <p>
8507 </code>
8509 <dt><pre>
8511 double <I></I>
8516 )
8517 </pre>
8518 <dd> Counts the number of minterms of the ZDD rooted at
8521 support of the function. If the procedure runs out of memory, it
8522 returns (double) CUDD_OUT_OF_MEM.
8523 <p>
8526 <p>
8529 </code>
8531 <dt><pre>
8533 int <I></I>
8537 )
8538 </pre>
8539 <dd> Returns an integer representing the number of minterms
8540 in a ZDD.
8541 <p>
8544 <p>
8547 </code>
8549 <dt><pre>
8551 char * <I></I>
8556 )
8557 </pre>
8558 <dd> Converts a path of a ZDD representing a cover to a
8559 string. The string represents an implicant of the cover. The path
8560 is typically produced by Cudd_zddForeachPath. Returns a pointer to
8561 the string if successful; NULL otherwise. If the str input is NULL,
8562 it allocates a new string. The string passed to this function must
8563 have enough room for all variables and for the terminator.
8564 <p>
8567 <p>
8570 </code>
8572 <dt><pre>
8574 int <I></I>
8577 )
8578 </pre>
8579 <dd> Counts the number of nodes in a ZDD. This function
8580 duplicates Cudd_DagSize and is only retained for compatibility.
8581 <p>
8584 <p>
8587 </code>
8589 <dt><pre>
8591 DdNode * <I></I>
8596 )
8597 </pre>
8598 <dd> Inclusion test for ZDDs (P implies Q). No new nodes are
8599 generated by this procedure. Returns empty if true;
8600 a valid pointer different from empty or DD_NON_CONSTANT otherwise.
8601 <p>
8604 <p>
8607 </code>
8609 <dt><pre>
8611 DdNode * <I></I>
8616 )
8617 </pre>
8618 <dd> Computes the difference of two ZDDs. Returns a pointer to the
8619 result if successful; NULL otherwise.
8620 <p>
8623 <p>
8626 </code>
8628 <dt><pre>
8630 DdNode * <I></I>
8635 )
8636 </pre>
8637 <dd> Modified version of Cudd_zddDivide. This function may
8638 disappear in future releases.
8639 <p>
8642 <p>
8644 <dt><pre>
8646 DdNode * <I></I>
8651 )
8652 </pre>
8653 <dd> Computes the quotient of two unate covers represented
8654 by ZDDs. Unate covers use one ZDD variable for each BDD
8655 variable. Returns a pointer to the resulting ZDD if successful; NULL
8656 otherwise.
8657 <p>
8660 <p>
8663 </code>
8665 <dt><pre>
8667 int <I></I>
8675 )
8676 </pre>
8677 <dd> Writes a file representing the argument ZDDs in a format
8678 suitable for the graph drawing program dot.
8680 file system full).
8681 Cudd_zddDumpDot does not close the file: This is the caller
8682 responsibility. Cudd_zddDumpDot uses a minimal unique subset of the
8683 hexadecimal address of a node as name for it.
8684 If the argument inames is non-null, it is assumed to hold the pointers
8685 to the names of the inputs. Similarly for onames.
8686 Cudd_zddDumpDot uses the following convention to draw arcs:
8687 <ul>
8688 <li> solid line: THEN arcs;
8689 <li> dashed line: ELSE arcs.
8690 </ul>
8691 The dot options are chosen so that the drawing fits on a letter-size
8692 sheet.
8693 <p>
8696 <p>
8700 </code>
8702 <dt><pre>
8704 DdGen * <I></I>
8709 )
8710 </pre>
8711 <dd> Defines an iterator on the paths of a ZDD
8712 and finds its first path. Returns a generator that contains the
8713 information necessary to continue the enumeration if successful; NULL
8714 otherwise.<p>
8715 A path is represented as an array of literals, which are integers in
8717 out of a node, and 2 stands for the absence of a node.
8718 The size of the array equals the number of variables in the manager at
8719 the time Cudd_zddFirstCube is called.<p>
8720 The paths that end in the empty terminal are not enumerated.
8721 <p>
8724 <p>
8730 </code>
8732 <dt><pre>
8734 DdNode * <I></I>
8739 )
8740 </pre>
8741 <dd> Computes the intersection of two ZDDs. Returns a pointer to
8742 the result if successful; NULL otherwise.
8743 <p>
8746 <p>
8748 <dt><pre>
8750 DdNode * <I></I>
8756 )
8757 </pre>
8758 <dd> Computes an irredundant sum of products (ISOP) in ZDD
8759 form from BDDs. The two BDDs L and U represent the lower bound and
8760 the upper bound, respectively, of the function. The ISOP uses two
8761 ZDD variables for each BDD variable: One for the positive literal,
8762 and one for the negative literal. These two variables should be
8763 adjacent in the ZDD order. The two ZDD variables corresponding to
8766 variable order. If successful, Cudd_zddIsop returns the BDD for
8767 the function chosen from the interval. The ZDD representing the
8768 irredundant cover is returned as a side effect in zdd_I. In case of
8769 failure, NULL is returned.
8770 <p>
8773 successful return.
8774 <p>
8778 </code>
8780 <dt><pre>
8782 DdNode * <I></I>
8788 )
8789 </pre>
8790 <dd> Computes the ITE of three ZDDs. Returns a pointer to the
8791 result if successful; NULL otherwise.
8792 <p>
8795 <p>
8797 <dt><pre>
8799 DdNode * <I></I>
8803 )
8804 </pre>
8805 <dd> Retrieves the ZDD variable with index i if it already
8806 exists, or creates a new ZDD variable. Returns a pointer to the
8807 variable if successful; NULL otherwise.
8808 <p>
8811 <p>
8815 </code>
8817 <dt><pre>
8819 int <I></I>
8823 )
8824 </pre>
8825 <dd> Generates the next path of a ZDD onset,
8827 otherwise.
8828 <p>
8831 generator is modified.
8832 <p>
8838 </code>
8840 <dt><pre>
8842 DdNode * <I></I>
8846 )
8847 </pre>
8848 <dd> Converts a BDD into a ZDD. This function assumes that
8849 there is a one-to-one correspondence between the BDD variables and the
8850 ZDD variables, and that the variable order is the same for both types
8851 of variables. These conditions are established if the ZDD variables
8852 are created by one call to Cudd_zddVarsFromBddVars with multiplicity =
8853 1. Returns a pointer to the resulting ZDD if successful; NULL otherwise.
8854 <p>
8857 <p>
8860 </code>
8862 <dt><pre>
8864 DdNode * <I></I>
8868 )
8869 </pre>
8870 <dd> Converts a ZDD into a BDD. Returns a pointer to the resulting
8871 ZDD if successful; NULL otherwise.
8872 <p>
8875 <p>
8878 </code>
8880 <dt><pre>
8882 int <I></I>
8886 )
8887 </pre>
8888 <dd> Prints a sum of products from a ZDD representing a cover.
8890 <p>
8893 <p>
8896 </code>
8898 <dt><pre>
8900 int <I></I>
8906 )
8907 </pre>
8908 <dd> Prints to the standard output a DD and its statistics.
8909 The statistics include the number of nodes and the number of minterms.
8910 (The number of minterms is also the number of combinations in the set.)
8912 <ul>
8918 </ul>
8920 <p>
8923 <p>
8925 <dt><pre>
8927 int <I></I>
8931 )
8932 </pre>
8934 if successful; 0 otherwise.
8935 <p>
8938 <p>
8942 </code>
8944 <dt><pre>
8946 void <I></I>
8949 )
8950 </pre>
8951 <dd> Prints the ZDD table for debugging purposes.
8952 <p>
8955 <p>
8957 <dt><pre>
8959 DdNode * <I></I>
8964 )
8965 </pre>
8966 <dd> Computes the product of two covers represented by
8967 ZDDs. The result is also a ZDD. Returns a pointer to the result if
8968 successful; NULL otherwise. The covers on which Cudd_zddProduct
8969 operates use two ZDD variables for each function variable (one ZDD
8970 variable for each literal of the variable). Those two ZDD variables
8971 should be adjacent in the order.
8972 <p>
8975 <p>
8978 </code>
8980 <dt><pre>
8982 long <I></I>
8985 )
8986 </pre>
8987 <dd> Reports the number of nodes in ZDDs. This
8989 <p>
8992 <p>
8996 </code>
8998 <dt><pre>
9000 void <I></I>
9003 )
9004 </pre>
9005 <dd> Disables realignment of ZDD order to BDD order.
9006 <p>
9009 <p>
9015 </code>
9017 <dt><pre>
9019 void <I></I>
9022 )
9023 </pre>
9024 <dd> Enables realignment of the ZDD variable order to the
9025 BDD variable order after the BDDs and ADDs have been reordered. The
9026 number of ZDD variables must be a multiple of the number of BDD
9027 variables for realignment to make sense. If this condition is not met,
9029 ratio of the two numbers. For the purpose of realignment, the ZDD
9032 is initially disabled.
9033 <p>
9036 <p>
9043 </code>
9045 <dt><pre>
9047 int <I></I>
9050 )
9051 </pre>
9053 enabled; 0 otherwise.
9054 <p>
9057 <p>
9063 </code>
9065 <dt><pre>
9067 int <I></I>
9072 )
9073 </pre>
9074 <dd> Main dynamic reordering routine for ZDDs.
9075 Calls one of the possible reordering procedures:
9076 <ul>
9077 <li>Swapping
9078 <li>Sifting
9079 <li>Symmetric Sifting
9080 </ul>
9082 For sifting and symmetric sifting it is possible to request reordering
9083 to convergence.<p>
9085 The core of all methods is the reordering procedure
9086 cuddZddSwapInPlace() which swaps two adjacent variables.
9088 sifting (with and without convergence) returns 1 plus the number of
9089 symmetric variables, in case of success.
9090 <p>
9093 the cache.
9094 <p>
9096 <dt><pre>
9098 int <I></I>
9102 )
9103 </pre>
9104 <dd> Reorders ZDD variables according to given permutation.
9105 The i-th entry of the permutation array contains the index of the variable
9106 that should be brought to the i-th level. The size of the array should be
9107 equal or greater to the number of variables currently in use.
9109 <p>
9112 the cache.
9113 <p>
9116 </code>
9118 <dt><pre>
9120 DdNode * <I></I>
9125 )
9126 </pre>
9127 <dd> Computes the negative cofactor of a ZDD w.r.t. a
9128 variable. In terms of combinations, the result is the set of all
9129 combinations in which the variable is negated. Returns a pointer to
9130 the result if successful; NULL otherwise.
9131 <p>
9134 <p>
9137 </code>
9139 <dt><pre>
9141 DdNode * <I></I>
9146 )
9147 </pre>
9148 <dd> Computes the positive cofactor of a ZDD w.r.t. a
9149 variable. In terms of combinations, the result is the set of all
9150 combinations in which the variable is asserted. Returns a pointer to
9151 the result if successful; NULL otherwise.
9152 <p>
9155 <p>
9158 </code>
9160 <dt><pre>
9162 void <I></I>
9167 )
9168 </pre>
9169 <dd> Prints statistics on symmetric ZDD variables.
9170 <p>
9173 <p>
9175 <dt><pre>
9177 DdNode * <I></I>
9182 )
9183 </pre>
9184 <dd> Computes the product of two unate covers represented as
9185 ZDDs. Unate covers use one ZDD variable for each BDD
9186 variable. Returns a pointer to the result if successful; NULL
9187 otherwise.
9188 <p>
9191 <p>
9194 </code>
9196 <dt><pre>
9198 DdNode * <I></I>
9203 )
9204 </pre>
9205 <dd> Computes the union of two ZDDs. Returns a pointer to the
9206 result if successful; NULL otherwise.
9207 <p>
9210 <p>
9212 <dt><pre>
9214 int <I></I>
9218 )
9219 </pre>
9220 <dd> Creates one or more ZDD variables for each BDD
9221 variable. If some ZDD variables already exist, only the missing
9222 variables are created. Parameter multiplicity allows the caller to
9223 control how many variables are created for each BDD variable in
9224 existence. For instance, if ZDDs are used to represent covers, two
9225 ZDD variables are required for each BDD variable. The order of the
9226 BDD variables is transferred to the ZDD variables. If a variable
9227 group tree exists for the BDD variables, a corresponding ZDD
9228 variable group tree is created by expanding the BDD variable
9229 tree. In any case, the ZDD variables derived from the same BDD
9230 variable are merged in a ZDD variable group. If a ZDD variable group
9232 <p>
9235 <p>
9240 </code>
9242 <dt><pre>
9244 DdNode * <I></I>
9249 )
9250 </pre>
9251 <dd> Modified version of Cudd_zddWeakDiv. This function may
9252 disappear in future releases.
9253 <p>
9256 <p>
9259 </code>
9261 <dt><pre>
9263 DdNode * <I></I>
9268 )
9269 </pre>
9270 <dd> Applies weak division to two ZDDs representing two
9271 covers. Returns a pointer to the ZDD representing the result if
9272 successful; NULL otherwise. The result of weak division depends on
9273 the variable order. The covers on which Cudd_zddWeakDiv operates use
9274 two ZDD variables for each function variable (one ZDD variable for
9275 each literal of the variable). Those two ZDD variables should be
9276 adjacent in the order.
9277 <p>
9280 <p>
9283 </code>
9286 </DL>
9287 <HR>
9288 Last updated on 20090220 23h06
9289 </BODY></HTML>