1 /**CFile***********************************************************************
2
3 FileName [cuddSubsetHB.c]
4
5 PackageName [cudd]
6
7 Synopsis [Procedure to subset the given BDD by choosing the heavier
8 branches.]
9
10
11 Description [External procedures provided by this module:
12 <ul>
13 <li> Cudd_SubsetHeavyBranch()
14 <li> Cudd_SupersetHeavyBranch()
15 </ul>
16 Internal procedures included in this module:
17 <ul>
18 <li> cuddSubsetHeavyBranch()
19 </ul>
20 Static procedures included in this module:
21 <ul>
22 <li> ResizeCountMintermPages();
23 <li> ResizeNodeDataPages()
24 <li> ResizeCountNodePages()
25 <li> SubsetCountMintermAux()
26 <li> SubsetCountMinterm()
27 <li> SubsetCountNodesAux()
28 <li> SubsetCountNodes()
29 <li> BuildSubsetBdd()
30 </ul>
31 ]
32
33 SeeAlso [cuddSubsetSP.c]
34
35 Author [Kavita Ravi]
36
37 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
38
39 All rights reserved.
40
41 Redistribution and use in source and binary forms, with or without
42 modification, are permitted provided that the following conditions
43 are met:
44
45 Redistributions of source code must retain the above copyright
46 notice, this list of conditions and the following disclaimer.
47
48 Redistributions in binary form must reproduce the above copyright
49 notice, this list of conditions and the following disclaimer in the
50 documentation and/or other materials provided with the distribution.
51
52 Neither the name of the University of Colorado nor the names of its
53 contributors may be used to endorse or promote products derived from
54 this software without specific prior written permission.
55
56 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
57 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
58 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
59 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
60 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
61 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
62 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
63 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
64 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
65 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
66 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
67 POSSIBILITY OF SUCH DAMAGE.]
68
69 ******************************************************************************/
70
71 #ifdef __STDC__
72 #include <float.h>
73 #else
74 #define DBL_MAX_EXP 1024
75 #endif
76 #include "misc/util/util_hack.h"
77 #include "cuddInt.h"
78
79 ABC_NAMESPACE_IMPL_START
80
81
82
83 /*---------------------------------------------------------------------------*/
84 /* Constant declarations */
85 /*---------------------------------------------------------------------------*/
86
87 #define DEFAULT_PAGE_SIZE 2048
88 #define DEFAULT_NODE_DATA_PAGE_SIZE 1024
89 #define INITIAL_PAGES 128
90
91
92 /*---------------------------------------------------------------------------*/
93 /* Stucture declarations */
94 /*---------------------------------------------------------------------------*/
95
96 /* data structure to store the information on each node. It keeps
97 * the number of minterms represented by the DAG rooted at this node
98 * in terms of the number of variables specified by the user, number
99 * of nodes in this DAG and the number of nodes of its child with
100 * lesser number of minterms that are not shared by the child with
101 * more minterms
102 */
103 struct NodeData {
104 double *mintermPointer;
105 int *nodesPointer;
106 int *lightChildNodesPointer;
107 };
108
109 /*---------------------------------------------------------------------------*/
110 /* Type declarations */
111 /*---------------------------------------------------------------------------*/
112
113 typedef struct NodeData NodeData_t;
114
115 /*---------------------------------------------------------------------------*/
116 /* Variable declarations */
117 /*---------------------------------------------------------------------------*/
118
119 #ifndef lint
120 static char rcsid[] DD_UNUSED = "$Id: cuddSubsetHB.c,v 1.37 2009/02/20 02:14:58 fabio Exp $";
121 #endif
122
123 static int memOut;
124 #ifdef DEBUG
125 static int num_calls;
126 #endif
127
128 static DdNode *zero, *one; /* constant functions */
129 static double **mintermPages; /* pointers to the pages */
130 static int **nodePages; /* pointers to the pages */
131 static int **lightNodePages; /* pointers to the pages */
132 static double *currentMintermPage; /* pointer to the current
133 page */
134 static double max; /* to store the 2^n value of the number
135 * of variables */
136
137 static int *currentNodePage; /* pointer to the current
138 page */
139 static int *currentLightNodePage; /* pointer to the
140 * current page */
141 static int pageIndex; /* index to next element */
142 static int page; /* index to current page */
143 static int pageSize = DEFAULT_PAGE_SIZE; /* page size */
144 static int maxPages; /* number of page pointers */
145
146 static NodeData_t *currentNodeDataPage; /* pointer to the current
147 page */
148 static int nodeDataPage; /* index to next element */
149 static int nodeDataPageIndex; /* index to next element */
150 static NodeData_t **nodeDataPages; /* index to current page */
151 static int nodeDataPageSize = DEFAULT_NODE_DATA_PAGE_SIZE;
152 /* page size */
153 static int maxNodeDataPages; /* number of page pointers */
154
155
156 /*---------------------------------------------------------------------------*/
157 /* Macro declarations */
158 /*---------------------------------------------------------------------------*/
159
160 /**AutomaticStart*************************************************************/
161
162 /*---------------------------------------------------------------------------*/
163 /* Static function prototypes */
164 /*---------------------------------------------------------------------------*/
165
166 static void ResizeNodeDataPages (void);
167 static void ResizeCountMintermPages (void);
168 static void ResizeCountNodePages (void);
169 static double SubsetCountMintermAux (DdNode *node, double max, st__table *table);
170 static st__table * SubsetCountMinterm (DdNode *node, int nvars);
171 static int SubsetCountNodesAux (DdNode *node, st__table *table, double max);
172 static int SubsetCountNodes (DdNode *node, st__table *table, int nvars);
173 static void StoreNodes ( st__table *storeTable, DdManager *dd, DdNode *node);
174 static DdNode * BuildSubsetBdd (DdManager *dd, DdNode *node, int *size, st__table *visitedTable, int threshold, st__table *storeTable, st__table *approxTable);
175
176 /**AutomaticEnd***************************************************************/
177
178
179 /*---------------------------------------------------------------------------*/
180 /* Definition of exported functions */
181 /*---------------------------------------------------------------------------*/
182
183 /**Function********************************************************************
184
185 Synopsis [Extracts a dense subset from a BDD with the heavy branch
186 heuristic.]
187
188 Description [Extracts a dense subset from a BDD. This procedure
189 builds a subset by throwing away one of the children of each node,
190 starting from the root, until the result is small enough. The child
191 that is eliminated from the result is the one that contributes the
192 fewer minterms. Returns a pointer to the BDD of the subset if
193 successful. NULL if the procedure runs out of memory. The parameter
194 numVars is the maximum number of variables to be used in minterm
195 calculation and node count calculation. The optimal number should
196 be as close as possible to the size of the support of f. However,
197 it is safe to pass the value returned by Cudd_ReadSize for numVars
198 when the number of variables is under 1023. If numVars is larger
199 than 1023, it will overflow. If a 0 parameter is passed then the
200 procedure will compute a value which will avoid overflow but will
201 cause underflow with 2046 variables or more.]
202
203 SideEffects [None]
204
205 SeeAlso [Cudd_SubsetShortPaths Cudd_SupersetHeavyBranch Cudd_ReadSize]
206
207 ******************************************************************************/
208 DdNode *
Cudd_SubsetHeavyBranch(DdManager * dd,DdNode * f,int numVars,int threshold)209 Cudd_SubsetHeavyBranch(
210 DdManager * dd /* manager */,
211 DdNode * f /* function to be subset */,
212 int numVars /* number of variables in the support of f */,
213 int threshold /* maximum number of nodes in the subset */)
214 {
215 DdNode *subset;
216
217 memOut = 0;
218 do {
219 dd->reordered = 0;
220 subset = cuddSubsetHeavyBranch(dd, f, numVars, threshold);
221 } while ((dd->reordered == 1) && (!memOut));
222
223 return(subset);
224
225 } /* end of Cudd_SubsetHeavyBranch */
226
227
228 /**Function********************************************************************
229
230 Synopsis [Extracts a dense superset from a BDD with the heavy branch
231 heuristic.]
232
233 Description [Extracts a dense superset from a BDD. The procedure is
234 identical to the subset procedure except for the fact that it
235 receives the complement of the given function. Extracting the subset
236 of the complement function is equivalent to extracting the superset
237 of the function. This procedure builds a superset by throwing away
238 one of the children of each node starting from the root of the
239 complement function, until the result is small enough. The child
240 that is eliminated from the result is the one that contributes the
241 fewer minterms.
242 Returns a pointer to the BDD of the superset if successful. NULL if
243 intermediate result causes the procedure to run out of memory. The
244 parameter numVars is the maximum number of variables to be used in
245 minterm calculation and node count calculation. The optimal number
246 should be as close as possible to the size of the support of f.
247 However, it is safe to pass the value returned by Cudd_ReadSize for
248 numVars when the number of variables is under 1023. If numVars is
249 larger than 1023, it will overflow. If a 0 parameter is passed then
250 the procedure will compute a value which will avoid overflow but
251 will cause underflow with 2046 variables or more.]
252
253 SideEffects [None]
254
255 SeeAlso [Cudd_SubsetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]
256
257 ******************************************************************************/
258 DdNode *
Cudd_SupersetHeavyBranch(DdManager * dd,DdNode * f,int numVars,int threshold)259 Cudd_SupersetHeavyBranch(
260 DdManager * dd /* manager */,
261 DdNode * f /* function to be superset */,
262 int numVars /* number of variables in the support of f */,
263 int threshold /* maximum number of nodes in the superset */)
264 {
265 DdNode *subset, *g;
266
267 g = Cudd_Not(f);
268 memOut = 0;
269 do {
270 dd->reordered = 0;
271 subset = cuddSubsetHeavyBranch(dd, g, numVars, threshold);
272 } while ((dd->reordered == 1) && (!memOut));
273
274 return(Cudd_NotCond(subset, (subset != NULL)));
275
276 } /* end of Cudd_SupersetHeavyBranch */
277
278
279 /*---------------------------------------------------------------------------*/
280 /* Definition of internal functions */
281 /*---------------------------------------------------------------------------*/
282
283
284 /**Function********************************************************************
285
286 Synopsis [The main procedure that returns a subset by choosing the heavier
287 branch in the BDD.]
288
289 Description [Here a subset BDD is built by throwing away one of the
290 children. Starting at root, annotate each node with the number of
291 minterms (in terms of the total number of variables specified -
292 numVars), number of nodes taken by the DAG rooted at this node and
293 number of additional nodes taken by the child that has the lesser
294 minterms. The child with the lower number of minterms is thrown away
295 and a dyanmic count of the nodes of the subset is kept. Once the
296 threshold is reached the subset is returned to the calling
297 procedure.]
298
299 SideEffects [None]
300
301 SeeAlso [Cudd_SubsetHeavyBranch]
302
303 ******************************************************************************/
304 DdNode *
cuddSubsetHeavyBranch(DdManager * dd,DdNode * f,int numVars,int threshold)305 cuddSubsetHeavyBranch(
306 DdManager * dd /* DD manager */,
307 DdNode * f /* current DD */,
308 int numVars /* maximum number of variables */,
309 int threshold /* threshold size for the subset */)
310 {
311
312 int i, *size;
313 st__table *visitedTable;
314 int numNodes;
315 NodeData_t *currNodeQual;
316 DdNode *subset;
317 st__table *storeTable, *approxTable;
318 char *key, *value;
319 st__generator *stGen;
320
321 if (f == NULL) {
322 fprintf(dd->err, "Cannot subset, nil object\n");
323 dd->errorCode = CUDD_INVALID_ARG;
324 return(NULL);
325 }
326
327 one = Cudd_ReadOne(dd);
328 zero = Cudd_Not(one);
329
330 /* If user does not know numVars value, set it to the maximum
331 * exponent that the pow function can take. The -1 is due to the
332 * discrepancy in the value that pow takes and the value that
333 * log gives.
334 */
335 if (numVars == 0) {
336 /* set default value */
337 numVars = DBL_MAX_EXP - 1;
338 }
339
340 if (Cudd_IsConstant(f)) {
341 return(f);
342 }
343
344 max = pow(2.0, (double)numVars);
345
346 /* Create visited table where structures for node data are allocated and
347 stored in a st__table */
348 visitedTable = SubsetCountMinterm(f, numVars);
349 if ((visitedTable == NULL) || memOut) {
350 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
351 dd->errorCode = CUDD_MEMORY_OUT;
352 return(0);
353 }
354 numNodes = SubsetCountNodes(f, visitedTable, numVars);
355 if (memOut) {
356 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
357 dd->errorCode = CUDD_MEMORY_OUT;
358 return(0);
359 }
360
361 if ( st__lookup(visitedTable, (const char *)f, (char **)&currNodeQual) == 0) {
362 fprintf(dd->err,
363 "Something is wrong, ought to be node quality table\n");
364 dd->errorCode = CUDD_INTERNAL_ERROR;
365 }
366
367 size = ABC_ALLOC(int, 1);
368 if (size == NULL) {
369 dd->errorCode = CUDD_MEMORY_OUT;
370 return(NULL);
371 }
372 *size = numNodes;
373
374 #ifdef DEBUG
375 num_calls = 0;
376 #endif
377 /* table to store nodes being created. */
378 storeTable = st__init_table( st__ptrcmp, st__ptrhash);
379 /* insert the constant */
380 cuddRef(one);
381 if ( st__insert(storeTable, (char *)Cudd_ReadOne(dd), NIL(char)) ==
382 st__OUT_OF_MEM) {
383 fprintf(dd->out, "Something wrong, st__table insert failed\n");
384 }
385 /* table to store approximations of nodes */
386 approxTable = st__init_table( st__ptrcmp, st__ptrhash);
387 subset = (DdNode *)BuildSubsetBdd(dd, f, size, visitedTable, threshold,
388 storeTable, approxTable);
389 if (subset != NULL) {
390 cuddRef(subset);
391 }
392
393 stGen = st__init_gen(approxTable);
394 if (stGen == NULL) {
395 st__free_table(approxTable);
396 return(NULL);
397 }
398 while( st__gen(stGen, (const char **)&key, (char **)&value)) {
399 Cudd_RecursiveDeref(dd, (DdNode *)value);
400 }
401 st__free_gen(stGen); stGen = NULL;
402 st__free_table(approxTable);
403
404 stGen = st__init_gen(storeTable);
405 if (stGen == NULL) {
406 st__free_table(storeTable);
407 return(NULL);
408 }
409 while( st__gen(stGen, (const char **)&key, (char **)&value)) {
410 Cudd_RecursiveDeref(dd, (DdNode *)key);
411 }
412 st__free_gen(stGen); stGen = NULL;
413 st__free_table(storeTable);
414
415 for (i = 0; i <= page; i++) {
416 ABC_FREE(mintermPages[i]);
417 }
418 ABC_FREE(mintermPages);
419 for (i = 0; i <= page; i++) {
420 ABC_FREE(nodePages[i]);
421 }
422 ABC_FREE(nodePages);
423 for (i = 0; i <= page; i++) {
424 ABC_FREE(lightNodePages[i]);
425 }
426 ABC_FREE(lightNodePages);
427 for (i = 0; i <= nodeDataPage; i++) {
428 ABC_FREE(nodeDataPages[i]);
429 }
430 ABC_FREE(nodeDataPages);
431 st__free_table(visitedTable);
432 ABC_FREE(size);
433 #if 0
434 (void) Cudd_DebugCheck(dd);
435 (void) Cudd_CheckKeys(dd);
436 #endif
437
438 if (subset != NULL) {
439 #ifdef DD_DEBUG
440 if (!Cudd_bddLeq(dd, subset, f)) {
441 fprintf(dd->err, "Wrong subset\n");
442 dd->errorCode = CUDD_INTERNAL_ERROR;
443 return(NULL);
444 }
445 #endif
446 cuddDeref(subset);
447 return(subset);
448 } else {
449 return(NULL);
450 }
451 } /* end of cuddSubsetHeavyBranch */
452
453
454 /*---------------------------------------------------------------------------*/
455 /* Definition of static functions */
456 /*---------------------------------------------------------------------------*/
457
458
459 /**Function********************************************************************
460
461 Synopsis [Resize the number of pages allocated to store the node data.]
462
463 Description [Resize the number of pages allocated to store the node data
464 The procedure moves the counter to the next page when the end of
465 the page is reached and allocates new pages when necessary.]
466
467 SideEffects [Changes the size of pages, page, page index, maximum
468 number of pages freeing stuff in case of memory out. ]
469
470 SeeAlso []
471
472 ******************************************************************************/
473 static void
ResizeNodeDataPages(void)474 ResizeNodeDataPages(void)
475 {
476 int i;
477 NodeData_t **newNodeDataPages;
478
479 nodeDataPage++;
480 /* If the current page index is larger than the number of pages
481 * allocated, allocate a new page array. Page numbers are incremented by
482 * INITIAL_PAGES
483 */
484 if (nodeDataPage == maxNodeDataPages) {
485 newNodeDataPages = ABC_ALLOC(NodeData_t *,maxNodeDataPages + INITIAL_PAGES);
486 if (newNodeDataPages == NULL) {
487 for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
488 ABC_FREE(nodeDataPages);
489 memOut = 1;
490 return;
491 } else {
492 for (i = 0; i < maxNodeDataPages; i++) {
493 newNodeDataPages[i] = nodeDataPages[i];
494 }
495 /* Increase total page count */
496 maxNodeDataPages += INITIAL_PAGES;
497 ABC_FREE(nodeDataPages);
498 nodeDataPages = newNodeDataPages;
499 }
500 }
501 /* Allocate a new page */
502 currentNodeDataPage = nodeDataPages[nodeDataPage] =
503 ABC_ALLOC(NodeData_t ,nodeDataPageSize);
504 if (currentNodeDataPage == NULL) {
505 for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
506 ABC_FREE(nodeDataPages);
507 memOut = 1;
508 return;
509 }
510 /* reset page index */
511 nodeDataPageIndex = 0;
512 return;
513
514 } /* end of ResizeNodeDataPages */
515
516
517 /**Function********************************************************************
518
519 Synopsis [Resize the number of pages allocated to store the minterm
520 counts. ]
521
522 Description [Resize the number of pages allocated to store the minterm
523 counts. The procedure moves the counter to the next page when the
524 end of the page is reached and allocates new pages when necessary.]
525
526 SideEffects [Changes the size of minterm pages, page, page index, maximum
527 number of pages freeing stuff in case of memory out. ]
528
529 SeeAlso []
530
531 ******************************************************************************/
532 static void
ResizeCountMintermPages(void)533 ResizeCountMintermPages(void)
534 {
535 int i;
536 double **newMintermPages;
537
538 page++;
539 /* If the current page index is larger than the number of pages
540 * allocated, allocate a new page array. Page numbers are incremented by
541 * INITIAL_PAGES
542 */
543 if (page == maxPages) {
544 newMintermPages = ABC_ALLOC(double *,maxPages + INITIAL_PAGES);
545 if (newMintermPages == NULL) {
546 for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
547 ABC_FREE(mintermPages);
548 memOut = 1;
549 return;
550 } else {
551 for (i = 0; i < maxPages; i++) {
552 newMintermPages[i] = mintermPages[i];
553 }
554 /* Increase total page count */
555 maxPages += INITIAL_PAGES;
556 ABC_FREE(mintermPages);
557 mintermPages = newMintermPages;
558 }
559 }
560 /* Allocate a new page */
561 currentMintermPage = mintermPages[page] = ABC_ALLOC(double,pageSize);
562 if (currentMintermPage == NULL) {
563 for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
564 ABC_FREE(mintermPages);
565 memOut = 1;
566 return;
567 }
568 /* reset page index */
569 pageIndex = 0;
570 return;
571
572 } /* end of ResizeCountMintermPages */
573
574
575 /**Function********************************************************************
576
577 Synopsis [Resize the number of pages allocated to store the node counts.]
578
579 Description [Resize the number of pages allocated to store the node counts.
580 The procedure moves the counter to the next page when the end of
581 the page is reached and allocates new pages when necessary.]
582
583 SideEffects [Changes the size of pages, page, page index, maximum
584 number of pages freeing stuff in case of memory out.]
585
586 SeeAlso []
587
588 ******************************************************************************/
589 static void
ResizeCountNodePages(void)590 ResizeCountNodePages(void)
591 {
592 int i;
593 int **newNodePages;
594
595 page++;
596
597 /* If the current page index is larger than the number of pages
598 * allocated, allocate a new page array. The number of pages is incremented
599 * by INITIAL_PAGES.
600 */
601 if (page == maxPages) {
602 newNodePages = ABC_ALLOC(int *,maxPages + INITIAL_PAGES);
603 if (newNodePages == NULL) {
604 for (i = 0; i < page; i++) ABC_FREE(nodePages[i]);
605 ABC_FREE(nodePages);
606 for (i = 0; i < page; i++) ABC_FREE(lightNodePages[i]);
607 ABC_FREE(lightNodePages);
608 memOut = 1;
609 return;
610 } else {
611 for (i = 0; i < maxPages; i++) {
612 newNodePages[i] = nodePages[i];
613 }
614 ABC_FREE(nodePages);
615 nodePages = newNodePages;
616 }
617
618 newNodePages = ABC_ALLOC(int *,maxPages + INITIAL_PAGES);
619 if (newNodePages == NULL) {
620 for (i = 0; i < page; i++) ABC_FREE(nodePages[i]);
621 ABC_FREE(nodePages);
622 for (i = 0; i < page; i++) ABC_FREE(lightNodePages[i]);
623 ABC_FREE(lightNodePages);
624 memOut = 1;
625 return;
626 } else {
627 for (i = 0; i < maxPages; i++) {
628 newNodePages[i] = lightNodePages[i];
629 }
630 ABC_FREE(lightNodePages);
631 lightNodePages = newNodePages;
632 }
633 /* Increase total page count */
634 maxPages += INITIAL_PAGES;
635 }
636 /* Allocate a new page */
637 currentNodePage = nodePages[page] = ABC_ALLOC(int,pageSize);
638 if (currentNodePage == NULL) {
639 for (i = 0; i < page; i++) ABC_FREE(nodePages[i]);
640 ABC_FREE(nodePages);
641 for (i = 0; i < page; i++) ABC_FREE(lightNodePages[i]);
642 ABC_FREE(lightNodePages);
643 memOut = 1;
644 return;
645 }
646 /* Allocate a new page */
647 currentLightNodePage = lightNodePages[page] = ABC_ALLOC(int,pageSize);
648 if (currentLightNodePage == NULL) {
649 for (i = 0; i <= page; i++) ABC_FREE(nodePages[i]);
650 ABC_FREE(nodePages);
651 for (i = 0; i < page; i++) ABC_FREE(lightNodePages[i]);
652 ABC_FREE(lightNodePages);
653 memOut = 1;
654 return;
655 }
656 /* reset page index */
657 pageIndex = 0;
658 return;
659
660 } /* end of ResizeCountNodePages */
661
662
663 /**Function********************************************************************
664
665 Synopsis [Recursively counts minterms of each node in the DAG.]
666
667 Description [Recursively counts minterms of each node in the DAG.
668 Similar to the cuddCountMintermAux which recursively counts the
669 number of minterms for the dag rooted at each node in terms of the
670 total number of variables (max). This procedure creates the node
671 data structure and stores the minterm count as part of the node
672 data structure. ]
673
674 SideEffects [Creates structures of type node quality and fills the st__table]
675
676 SeeAlso [SubsetCountMinterm]
677
678 ******************************************************************************/
679 static double
SubsetCountMintermAux(DdNode * node,double max,st__table * table)680 SubsetCountMintermAux(
681 DdNode * node /* function to analyze */,
682 double max /* number of minterms of constant 1 */,
683 st__table * table /* visitedTable table */)
684 {
685
686 DdNode *N,*Nv,*Nnv; /* nodes to store cofactors */
687 double min,*pmin; /* minterm count */
688 double min1, min2; /* minterm count */
689 NodeData_t *dummy;
690 NodeData_t *newEntry;
691 int i;
692
693 #ifdef DEBUG
694 num_calls++;
695 #endif
696
697 /* Constant case */
698 if (Cudd_IsConstant(node)) {
699 if (node == zero) {
700 return(0.0);
701 } else {
702 return(max);
703 }
704 } else {
705
706 /* check if entry for this node exists */
707 if ( st__lookup(table, (const char *)node, (char **)&dummy)) {
708 min = *(dummy->mintermPointer);
709 return(min);
710 }
711
712 /* Make the node regular to extract cofactors */
713 N = Cudd_Regular(node);
714
715 /* store the cofactors */
716 Nv = Cudd_T(N);
717 Nnv = Cudd_E(N);
718
719 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
720 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
721
722 min1 = SubsetCountMintermAux(Nv, max,table)/2.0;
723 if (memOut) return(0.0);
724 min2 = SubsetCountMintermAux(Nnv,max,table)/2.0;
725 if (memOut) return(0.0);
726 min = (min1+min2);
727
728 /* if page index is at the bottom, then create a new page */
729 if (pageIndex == pageSize) ResizeCountMintermPages();
730 if (memOut) {
731 for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
732 ABC_FREE(nodeDataPages);
733 st__free_table(table);
734 return(0.0);
735 }
736
737 /* point to the correct location in the page */
738 pmin = currentMintermPage+pageIndex;
739 pageIndex++;
740
741 /* store the minterm count of this node in the page */
742 *pmin = min;
743
744 /* Note I allocate the struct here. Freeing taken care of later */
745 if (nodeDataPageIndex == nodeDataPageSize) ResizeNodeDataPages();
746 if (memOut) {
747 for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
748 ABC_FREE(mintermPages);
749 st__free_table(table);
750 return(0.0);
751 }
752
753 newEntry = currentNodeDataPage + nodeDataPageIndex;
754 nodeDataPageIndex++;
755
756 /* points to the correct location in the page */
757 newEntry->mintermPointer = pmin;
758 /* initialize this field of the Node Quality structure */
759 newEntry->nodesPointer = NULL;
760
761 /* insert entry for the node in the table */
762 if ( st__insert(table,(char *)node, (char *)newEntry) == st__OUT_OF_MEM) {
763 memOut = 1;
764 for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
765 ABC_FREE(mintermPages);
766 for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
767 ABC_FREE(nodeDataPages);
768 st__free_table(table);
769 return(0.0);
770 }
771 return(min);
772 }
773
774 } /* end of SubsetCountMintermAux */
775
776
777 /**Function********************************************************************
778
779 Synopsis [Counts minterms of each node in the DAG]
780
781 Description [Counts minterms of each node in the DAG. Similar to the
782 Cudd_CountMinterm procedure except this returns the minterm count for
783 all the nodes in the bdd in an st__table.]
784
785 SideEffects [none]
786
787 SeeAlso [SubsetCountMintermAux]
788
789 ******************************************************************************/
790 static st__table *
SubsetCountMinterm(DdNode * node,int nvars)791 SubsetCountMinterm(
792 DdNode * node /* function to be analyzed */,
793 int nvars /* number of variables node depends on */)
794 {
795 st__table *table;
796 int i;
797
798
799 #ifdef DEBUG
800 num_calls = 0;
801 #endif
802
803 max = pow(2.0,(double) nvars);
804 table = st__init_table( st__ptrcmp, st__ptrhash);
805 if (table == NULL) goto OUT_OF_MEM;
806 maxPages = INITIAL_PAGES;
807 mintermPages = ABC_ALLOC(double *,maxPages);
808 if (mintermPages == NULL) {
809 st__free_table(table);
810 goto OUT_OF_MEM;
811 }
812 page = 0;
813 currentMintermPage = ABC_ALLOC(double,pageSize);
814 mintermPages[page] = currentMintermPage;
815 if (currentMintermPage == NULL) {
816 ABC_FREE(mintermPages);
817 st__free_table(table);
818 goto OUT_OF_MEM;
819 }
820 pageIndex = 0;
821 maxNodeDataPages = INITIAL_PAGES;
822 nodeDataPages = ABC_ALLOC(NodeData_t *, maxNodeDataPages);
823 if (nodeDataPages == NULL) {
824 for (i = 0; i <= page ; i++) ABC_FREE(mintermPages[i]);
825 ABC_FREE(mintermPages);
826 st__free_table(table);
827 goto OUT_OF_MEM;
828 }
829 nodeDataPage = 0;
830 currentNodeDataPage = ABC_ALLOC(NodeData_t ,nodeDataPageSize);
831 nodeDataPages[nodeDataPage] = currentNodeDataPage;
832 if (currentNodeDataPage == NULL) {
833 for (i = 0; i <= page ; i++) ABC_FREE(mintermPages[i]);
834 ABC_FREE(mintermPages);
835 ABC_FREE(nodeDataPages);
836 st__free_table(table);
837 goto OUT_OF_MEM;
838 }
839 nodeDataPageIndex = 0;
840
841 (void) SubsetCountMintermAux(node,max,table);
842 if (memOut) goto OUT_OF_MEM;
843 return(table);
844
845 OUT_OF_MEM:
846 memOut = 1;
847 return(NULL);
848
849 } /* end of SubsetCountMinterm */
850
851
852 /**Function********************************************************************
853
854 Synopsis [Recursively counts the number of nodes under the dag.
855 Also counts the number of nodes under the lighter child of
856 this node.]
857
858 Description [Recursively counts the number of nodes under the dag.
859 Also counts the number of nodes under the lighter child of
860 this node. . Note that the same dag may be the lighter child of two
861 different nodes and have different counts. As with the minterm counts,
862 the node counts are stored in pages to be space efficient and the
863 address for these node counts are stored in an st__table associated
864 to each node. ]
865
866 SideEffects [Updates the node data table with node counts]
867
868 SeeAlso [SubsetCountNodes]
869
870 ******************************************************************************/
871 static int
SubsetCountNodesAux(DdNode * node,st__table * table,double max)872 SubsetCountNodesAux(
873 DdNode * node /* current node */,
874 st__table * table /* table to update node count, also serves as visited table. */,
875 double max /* maximum number of variables */)
876 {
877 int tval, eval, i;
878 DdNode *N, *Nv, *Nnv;
879 double minNv, minNnv;
880 NodeData_t *dummyN, *dummyNv, *dummyNnv, *dummyNBar;
881 int *pmin, *pminBar, *val;
882
883 if ((node == NULL) || Cudd_IsConstant(node))
884 return(0);
885
886 /* if this node has been processed do nothing */
887 if ( st__lookup(table, (const char *)node, (char **)&dummyN) == 1) {
888 val = dummyN->nodesPointer;
889 if (val != NULL)
890 return(0);
891 } else {
892 return(0);
893 }
894
895 N = Cudd_Regular(node);
896 Nv = Cudd_T(N);
897 Nnv = Cudd_E(N);
898
899 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
900 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
901
902 /* find the minterm counts for the THEN and ELSE branches */
903 if (Cudd_IsConstant(Nv)) {
904 if (Nv == zero) {
905 minNv = 0.0;
906 } else {
907 minNv = max;
908 }
909 } else {
910 if ( st__lookup(table, (const char *)Nv, (char **)&dummyNv) == 1)
911 minNv = *(dummyNv->mintermPointer);
912 else {
913 return(0);
914 }
915 }
916 if (Cudd_IsConstant(Nnv)) {
917 if (Nnv == zero) {
918 minNnv = 0.0;
919 } else {
920 minNnv = max;
921 }
922 } else {
923 if ( st__lookup(table, (const char *)Nnv, (char **)&dummyNnv) == 1) {
924 minNnv = *(dummyNnv->mintermPointer);
925 }
926 else {
927 return(0);
928 }
929 }
930
931
932 /* recur based on which has larger minterm, */
933 if (minNv >= minNnv) {
934 tval = SubsetCountNodesAux(Nv, table, max);
935 if (memOut) return(0);
936 eval = SubsetCountNodesAux(Nnv, table, max);
937 if (memOut) return(0);
938
939 /* store the node count of the lighter child. */
940 if (pageIndex == pageSize) ResizeCountNodePages();
941 if (memOut) {
942 for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
943 ABC_FREE(mintermPages);
944 for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
945 ABC_FREE(nodeDataPages);
946 st__free_table(table);
947 return(0);
948 }
949 pmin = currentLightNodePage + pageIndex;
950 *pmin = eval; /* Here the ELSE child is lighter */
951 dummyN->lightChildNodesPointer = pmin;
952
953 } else {
954 eval = SubsetCountNodesAux(Nnv, table, max);
955 if (memOut) return(0);
956 tval = SubsetCountNodesAux(Nv, table, max);
957 if (memOut) return(0);
958
959 /* store the node count of the lighter child. */
960 if (pageIndex == pageSize) ResizeCountNodePages();
961 if (memOut) {
962 for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
963 ABC_FREE(mintermPages);
964 for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
965 ABC_FREE(nodeDataPages);
966 st__free_table(table);
967 return(0);
968 }
969 pmin = currentLightNodePage + pageIndex;
970 *pmin = tval; /* Here the THEN child is lighter */
971 dummyN->lightChildNodesPointer = pmin;
972
973 }
974 /* updating the page index for node count storage. */
975 pmin = currentNodePage + pageIndex;
976 *pmin = tval + eval + 1;
977 dummyN->nodesPointer = pmin;
978
979 /* pageIndex is parallel page index for count_nodes and count_lightNodes */
980 pageIndex++;
981
982 /* if this node has been reached first, it belongs to a heavier
983 branch. Its complement will be reached later on a lighter branch.
984 Hence the complement has zero node count. */
985
986 if ( st__lookup(table, (const char *)Cudd_Not(node), (char **)&dummyNBar) == 1) {
987 if (pageIndex == pageSize) ResizeCountNodePages();
988 if (memOut) {
989 for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
990 ABC_FREE(mintermPages);
991 for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
992 ABC_FREE(nodeDataPages);
993 st__free_table(table);
994 return(0);
995 }
996 pminBar = currentLightNodePage + pageIndex;
997 *pminBar = 0;
998 dummyNBar->lightChildNodesPointer = pminBar;
999 /* The lighter child has less nodes than the parent.
1000 * So if parent 0 then lighter child zero
1001 */
1002 if (pageIndex == pageSize) ResizeCountNodePages();
1003 if (memOut) {
1004 for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
1005 ABC_FREE(mintermPages);
1006 for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
1007 ABC_FREE(nodeDataPages);
1008 st__free_table(table);
1009 return(0);
1010 }
1011 pminBar = currentNodePage + pageIndex;
1012 *pminBar = 0;
1013 dummyNBar->nodesPointer = pminBar ; /* maybe should point to zero */
1014
1015 pageIndex++;
1016 }
1017 return(*pmin);
1018 } /*end of SubsetCountNodesAux */
1019
1020
1021 /**Function********************************************************************
1022
1023 Synopsis [Counts the nodes under the current node and its lighter child]
1024
1025 Description [Counts the nodes under the current node and its lighter
1026 child. Calls a recursive procedure to count the number of nodes of
1027 a DAG rooted at a particular node and the number of nodes taken by its
1028 lighter child.]
1029
1030 SideEffects [None]
1031
1032 SeeAlso [SubsetCountNodesAux]
1033
1034 ******************************************************************************/
1035 static int
SubsetCountNodes(DdNode * node,st__table * table,int nvars)1036 SubsetCountNodes(
1037 DdNode * node /* function to be analyzed */,
1038 st__table * table /* node quality table */,
1039 int nvars /* number of variables node depends on */)
1040 {
1041 int num;
1042 int i;
1043
1044 #ifdef DEBUG
1045 num_calls = 0;
1046 #endif
1047
1048 max = pow(2.0,(double) nvars);
1049 maxPages = INITIAL_PAGES;
1050 nodePages = ABC_ALLOC(int *,maxPages);
1051 if (nodePages == NULL) {
1052 goto OUT_OF_MEM;
1053 }
1054
1055 lightNodePages = ABC_ALLOC(int *,maxPages);
1056 if (lightNodePages == NULL) {
1057 for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
1058 ABC_FREE(mintermPages);
1059 for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
1060 ABC_FREE(nodeDataPages);
1061 ABC_FREE(nodePages);
1062 goto OUT_OF_MEM;
1063 }
1064
1065 page = 0;
1066 currentNodePage = nodePages[page] = ABC_ALLOC(int,pageSize);
1067 if (currentNodePage == NULL) {
1068 for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
1069 ABC_FREE(mintermPages);
1070 for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
1071 ABC_FREE(nodeDataPages);
1072 ABC_FREE(lightNodePages);
1073 ABC_FREE(nodePages);
1074 goto OUT_OF_MEM;
1075 }
1076
1077 currentLightNodePage = lightNodePages[page] = ABC_ALLOC(int,pageSize);
1078 if (currentLightNodePage == NULL) {
1079 for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
1080 ABC_FREE(mintermPages);
1081 for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
1082 ABC_FREE(nodeDataPages);
1083 ABC_FREE(currentNodePage);
1084 ABC_FREE(lightNodePages);
1085 ABC_FREE(nodePages);
1086 goto OUT_OF_MEM;
1087 }
1088
1089 pageIndex = 0;
1090 num = SubsetCountNodesAux(node,table,max);
1091 if (memOut) goto OUT_OF_MEM;
1092 return(num);
1093
1094 OUT_OF_MEM:
1095 memOut = 1;
1096 return(0);
1097
1098 } /* end of SubsetCountNodes */
1099
1100
1101 /**Function********************************************************************
1102
1103 Synopsis [Procedure to recursively store nodes that are retained in the subset.]
1104
1105 Description [rocedure to recursively store nodes that are retained in the subset.]
1106
1107 SideEffects [None]
1108
1109 SeeAlso [StoreNodes]
1110
1111 ******************************************************************************/
1112 static void
StoreNodes(st__table * storeTable,DdManager * dd,DdNode * node)1113 StoreNodes(
1114 st__table * storeTable,
1115 DdManager * dd,
1116 DdNode * node)
1117 {
1118 DdNode *N, *Nt, *Ne;
1119 if (Cudd_IsConstant(dd)) {
1120 return;
1121 }
1122 N = Cudd_Regular(node);
1123 if ( st__lookup(storeTable, (char *)N, NIL(char *))) {
1124 return;
1125 }
1126 cuddRef(N);
1127 if ( st__insert(storeTable, (char *)N, NIL(char)) == st__OUT_OF_MEM) {
1128 fprintf(dd->err,"Something wrong, st__table insert failed\n");
1129 }
1130
1131 Nt = Cudd_T(N);
1132 Ne = Cudd_E(N);
1133
1134 StoreNodes(storeTable, dd, Nt);
1135 StoreNodes(storeTable, dd, Ne);
1136 return;
1137
1138 }
1139
1140
1141 /**Function********************************************************************
1142
1143 Synopsis [Builds the subset BDD using the heavy branch method.]
1144
1145 Description [The procedure carries out the building of the subset BDD
1146 starting at the root. Using the three different counts labelling each node,
1147 the procedure chooses the heavier branch starting from the root and keeps
1148 track of the number of nodes it discards at each step, thus keeping count
1149 of the size of the subset BDD dynamically. Once the threshold is satisfied,
1150 the procedure then calls ITE to build the BDD.]
1151
1152 SideEffects [None]
1153
1154 SeeAlso []
1155
1156 ******************************************************************************/
1157 static DdNode *
BuildSubsetBdd(DdManager * dd,DdNode * node,int * size,st__table * visitedTable,int threshold,st__table * storeTable,st__table * approxTable)1158 BuildSubsetBdd(
1159 DdManager * dd /* DD manager */,
1160 DdNode * node /* current node */,
1161 int * size /* current size of the subset */,
1162 st__table * visitedTable /* visited table storing all node data */,
1163 int threshold,
1164 st__table * storeTable,
1165 st__table * approxTable)
1166 {
1167
1168 DdNode *Nv, *Nnv, *N, *topv, *neW;
1169 double minNv, minNnv;
1170 NodeData_t *currNodeQual;
1171 NodeData_t *currNodeQualT;
1172 NodeData_t *currNodeQualE;
1173 DdNode *ThenBranch, *ElseBranch;
1174 unsigned int topid;
1175 char *dummy;
1176
1177 #ifdef DEBUG
1178 num_calls++;
1179 #endif
1180 /*If the size of the subset is below the threshold, dont do
1181 anything. */
1182 if ((*size) <= threshold) {
1183 /* store nodes below this, so we can recombine if possible */
1184 StoreNodes(storeTable, dd, node);
1185 return(node);
1186 }
1187
1188 if (Cudd_IsConstant(node))
1189 return(node);
1190
1191 /* Look up minterm count for this node. */
1192 if (! st__lookup(visitedTable, (const char *)node, (char **)&currNodeQual)) {
1193 fprintf(dd->err,
1194 "Something is wrong, ought to be in node quality table\n");
1195 }
1196
1197 /* Get children. */
1198 N = Cudd_Regular(node);
1199 Nv = Cudd_T(N);
1200 Nnv = Cudd_E(N);
1201
1202 /* complement if necessary */
1203 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
1204 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
1205
1206 if (!Cudd_IsConstant(Nv)) {
1207 /* find out minterms and nodes contributed by then child */
1208 if (! st__lookup(visitedTable, (const char *)Nv, (char **)&currNodeQualT)) {
1209 fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
1210 dd->errorCode = CUDD_INTERNAL_ERROR;
1211 return(NULL);
1212 }
1213 else {
1214 minNv = *(((NodeData_t *)currNodeQualT)->mintermPointer);
1215 }
1216 } else {
1217 if (Nv == zero) {
1218 minNv = 0;
1219 } else {
1220 minNv = max;
1221 }
1222 }
1223 if (!Cudd_IsConstant(Nnv)) {
1224 /* find out minterms and nodes contributed by else child */
1225 if (! st__lookup(visitedTable, (const char *)Nnv, (char **)&currNodeQualE)) {
1226 fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
1227 dd->errorCode = CUDD_INTERNAL_ERROR;
1228 return(NULL);
1229 } else {
1230 minNnv = *(((NodeData_t *)currNodeQualE)->mintermPointer);
1231 }
1232 } else {
1233 if (Nnv == zero) {
1234 minNnv = 0;
1235 } else {
1236 minNnv = max;
1237 }
1238 }
1239
1240 /* keep track of size of subset by subtracting the number of
1241 * differential nodes contributed by lighter child
1242 */
1243 *size = (*(size)) - (int)*(currNodeQual->lightChildNodesPointer);
1244 if (minNv >= minNnv) { /*SubsetCountNodesAux procedure takes
1245 the Then branch in case of a tie */
1246
1247 /* recur with the Then branch */
1248 ThenBranch = (DdNode *)BuildSubsetBdd(dd, Nv, size,
1249 visitedTable, threshold, storeTable, approxTable);
1250 if (ThenBranch == NULL) {
1251 return(NULL);
1252 }
1253 cuddRef(ThenBranch);
1254 /* The Else branch is either a node that already exists in the
1255 * subset, or one whose approximation has been computed, or
1256 * Zero.
1257 */
1258 if ( st__lookup(storeTable, (char *)Cudd_Regular(Nnv), &dummy)) {
1259 ElseBranch = Nnv;
1260 cuddRef(ElseBranch);
1261 } else {
1262 if ( st__lookup(approxTable, (char *)Nnv, &dummy)) {
1263 ElseBranch = (DdNode *)dummy;
1264 cuddRef(ElseBranch);
1265 } else {
1266 ElseBranch = zero;
1267 cuddRef(ElseBranch);
1268 }
1269 }
1270
1271 }
1272 else {
1273 /* recur with the Else branch */
1274 ElseBranch = (DdNode *)BuildSubsetBdd(dd, Nnv, size,
1275 visitedTable, threshold, storeTable, approxTable);
1276 if (ElseBranch == NULL) {
1277 return(NULL);
1278 }
1279 cuddRef(ElseBranch);
1280 /* The Then branch is either a node that already exists in the
1281 * subset, or one whose approximation has been computed, or
1282 * Zero.
1283 */
1284 if ( st__lookup(storeTable, (char *)Cudd_Regular(Nv), &dummy)) {
1285 ThenBranch = Nv;
1286 cuddRef(ThenBranch);
1287 } else {
1288 if ( st__lookup(approxTable, (char *)Nv, &dummy)) {
1289 ThenBranch = (DdNode *)dummy;
1290 cuddRef(ThenBranch);
1291 } else {
1292 ThenBranch = zero;
1293 cuddRef(ThenBranch);
1294 }
1295 }
1296 }
1297
1298 /* construct the Bdd with the top variable and the two children */
1299 topid = Cudd_NodeReadIndex(N);
1300 topv = Cudd_ReadVars(dd, topid);
1301 cuddRef(topv);
1302 neW = cuddBddIteRecur(dd, topv, ThenBranch, ElseBranch);
1303 if (neW != NULL) {
1304 cuddRef(neW);
1305 }
1306 Cudd_RecursiveDeref(dd, topv);
1307 Cudd_RecursiveDeref(dd, ThenBranch);
1308 Cudd_RecursiveDeref(dd, ElseBranch);
1309
1310
1311 if (neW == NULL)
1312 return(NULL);
1313 else {
1314 /* store this node in the store table */
1315 if (! st__lookup(storeTable, (char *)Cudd_Regular(neW), &dummy)) {
1316 cuddRef(neW);
1317 if (! st__insert(storeTable, (char *)Cudd_Regular(neW), NIL(char)))
1318 return (NULL);
1319 }
1320 /* store the approximation for this node */
1321 if (N != Cudd_Regular(neW)) {
1322 if ( st__lookup(approxTable, (char *)node, &dummy)) {
1323 fprintf(dd->err, "This node should not be in the approximated table\n");
1324 } else {
1325 cuddRef(neW);
1326 if (! st__insert(approxTable, (char *)node, (char *)neW))
1327 return(NULL);
1328 }
1329 }
1330 cuddDeref(neW);
1331 return(neW);
1332 }
1333 } /* end of BuildSubsetBdd */
1334
1335
1336 ABC_NAMESPACE_IMPL_END
1337
1338