1 /**
2 @file
3
4 @ingroup nanotrav
5
6 @brief %BDD test functions for the nanotrav program.
7
8 @author Fabio Somenzi
9
10 @copyright@parblock
11 Copyright (c) 1995-2015, Regents of the University of Colorado
12
13 All rights reserved.
14
15 Redistribution and use in source and binary forms, with or without
16 modification, are permitted provided that the following conditions
17 are met:
18
19 Redistributions of source code must retain the above copyright
20 notice, this list of conditions and the following disclaimer.
21
22 Redistributions in binary form must reproduce the above copyright
23 notice, this list of conditions and the following disclaimer in the
24 documentation and/or other materials provided with the distribution.
25
26 Neither the name of the University of Colorado nor the names of its
27 contributors may be used to endorse or promote products derived from
28 this software without specific prior written permission.
29
30 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
31 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
32 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
33 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
34 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
35 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
36 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
37 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
38 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
39 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
40 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
41 POSSIBILITY OF SUCH DAMAGE.
42 @endparblock
43
44 */
45
46 #include "ntr.h"
47 #include "cuddInt.h"
48
49 /*---------------------------------------------------------------------------*/
50 /* Constant declarations */
51 /*---------------------------------------------------------------------------*/
52
53 /*---------------------------------------------------------------------------*/
54 /* Stucture declarations */
55 /*---------------------------------------------------------------------------*/
56
57 /*---------------------------------------------------------------------------*/
58 /* Type declarations */
59 /*---------------------------------------------------------------------------*/
60
61 /*---------------------------------------------------------------------------*/
62 /* Variable declarations */
63 /*---------------------------------------------------------------------------*/
64
65
66 /*---------------------------------------------------------------------------*/
67 /* Macro declarations */
68 /*---------------------------------------------------------------------------*/
69
70 /** \cond */
71
72 /*---------------------------------------------------------------------------*/
73 /* Static function prototypes */
74 /*---------------------------------------------------------------------------*/
75
76 static int ntrTestMinimizationAux (DdManager *dd, BnetNetwork *net1, DdNode *f, char *name, DdNode *c, char *cname, NtrOptions *option);
77 static int ntrTestDensityAux (DdManager *dd, BnetNetwork *net, DdNode *f, char *name, NtrOptions *option);
78 static int ntrTestDecompAux (DdManager *dd, BnetNetwork *net, DdNode *f, char *name, NtrOptions *option);
79 static int ntrTestCofEstAux (DdManager * dd, BnetNetwork * net, DdNode * f, char * name, NtrOptions * option);
80 static int ntrTestClippingAux (DdManager *dd, BnetNetwork *net1, DdNode *f, char *name, DdNode *g, char *gname, NtrOptions *option);
81 static int ntrTestEquivAndContainAux (DdManager *dd, BnetNetwork *net1, DdNode *f, char *fname, DdNode *g, char *gname, DdNode *d, char *dname, NtrOptions *option);
82 static int ntrTestClosestCubeAux (DdManager *dd, BnetNetwork *net, DdNode *f, char *fname, DdNode *g, char *gname, DdNode **vars, NtrOptions *option);
83 static int ntrTestCharToVect(DdManager * dd, DdNode * f, NtrOptions *option);
84 #if 0
85 static DdNode * ntrCompress1 (DdManager *dd, DdNode *f, int nvars, int threshold);
86 #endif
87 static DdNode * ntrCompress2 (DdManager *dd, DdNode *f, int nvars, int threshold);
88 static BnetNode * ntrNodeIsBuffer (BnetNode *nd, st_table *hash);
89
90 /** \endcond */
91
92
93 /*---------------------------------------------------------------------------*/
94 /* Definition of exported functions */
95 /*---------------------------------------------------------------------------*/
96
97
98 /**
99 @brief Tests %BDD minimization functions.
100
101 @details Tests %BDD minimization functions, including
102 leaf-identifying compaction, squeezing, and restrict. This function
103 uses as constraint the first output of net2 and computes positive
104 and negative cofactors of all the outputs of net1. For each
105 cofactor, it checks whether compaction was safe (cofactor not larger
106 than original function) and that the expansion based on each
107 minimization function (used as a generalized cofactor) equals the
108 original function.
109
110 @return 1 if successful; 0 otherwise.
111
112 @sideeffect None
113
114 */
115 int
Ntr_TestMinimization(DdManager * dd,BnetNetwork * net1,BnetNetwork * net2,NtrOptions * option)116 Ntr_TestMinimization(
117 DdManager * dd,
118 BnetNetwork * net1,
119 BnetNetwork * net2,
120 NtrOptions * option)
121 {
122 DdNode *f;
123 DdNode *c = NULL;
124 char *cname = NULL;
125 BnetNode *node;
126 int i;
127 int result;
128 int nsize, csize;
129
130 if (option->second == FALSE) return(1);
131
132 (void) printf("Testing BDD minimization algorithms\n");
133 /* Use largest output of second network as constraint. */
134 csize = -1;
135 for (i = 0; i < net2->noutputs; i++) {
136 if (!st_lookup(net2->hash,net2->outputs[i],(void **)&node)) {
137 return(0);
138 }
139 nsize = Cudd_DagSize(node->dd);
140 if (nsize > csize) {
141 c = node->dd;
142 cname = node->name;
143 csize = nsize;
144 }
145 }
146 if (c == NULL || cname == NULL) return(0);
147 (void) printf("TEST-MINI: Constrain (%s) %d nodes\n",
148 cname, Cudd_DagSize(c));
149
150 if (option->node == NULL) {
151 for (i = 0; i < net1->noutputs; i++) {
152 if (!st_lookup(net1->hash,net1->outputs[i],(void **)&node)) {
153 return(0);
154 }
155 f = node->dd;
156 if (f == NULL) return(0);
157 result = ntrTestMinimizationAux(dd,net1,f,node->name,c,cname,
158 option);
159 if (result == 0) return(0);
160 }
161 } else {
162 if (!st_lookup(net1->hash,option->node,(void **)&node)) {
163 return(0);
164 }
165 f = node->dd;
166 if (f == NULL) return(0);
167 result = ntrTestMinimizationAux(dd,net1,f,option->node,c,cname,option);
168 if (result == 0) return(0);
169 }
170
171 return(1);
172
173 } /* end of Ntr_TestMinimization */
174
175
176 /**
177 @brief Tests %BDD density-related functions.
178
179 @return 1 if successful; 0 otherwise.
180
181 @sideeffect None
182
183 */
184 int
Ntr_TestDensity(DdManager * dd,BnetNetwork * net1,NtrOptions * option)185 Ntr_TestDensity(
186 DdManager * dd,
187 BnetNetwork * net1,
188 NtrOptions * option)
189 {
190 DdNode *f;
191 BnetNode *node;
192 int i;
193 int result;
194
195 if (option->density == FALSE) return(1);
196
197 (void) printf("Testing BDD density-related algorithms\n");
198 if (option->node == NULL) {
199 for (i = 0; i < net1->noutputs; i++) {
200 if (!st_lookup(net1->hash,net1->outputs[i],(void **)&node)) {
201 return(0);
202 }
203 f = node->dd;
204 if (f == NULL) return(0);
205 result = ntrTestDensityAux(dd,net1,f,node->name,option);
206 if (result == 0) return(0);
207 }
208 } else {
209 if (!st_lookup(net1->hash,option->node,(void **)&node)) {
210 return(0);
211 }
212 f = node->dd;
213 if (f == NULL) return(0);
214 result = ntrTestDensityAux(dd,net1,f,option->node,option);
215 if (result == 0) return(0);
216 }
217
218 return(1);
219
220 } /* end of Ntr_TestDensity */
221
222
223 /**
224 @brief Tests %BDD decomposition functions.
225
226 @return 1 if successful; 0 otherwise.
227
228 @sideeffect None
229
230 */
231 int
Ntr_TestDecomp(DdManager * dd,BnetNetwork * net1,NtrOptions * option)232 Ntr_TestDecomp(
233 DdManager * dd,
234 BnetNetwork * net1,
235 NtrOptions * option)
236 {
237 DdNode *f;
238 BnetNode *node;
239 int i;
240 int result;
241
242 if (option->decomp == FALSE) return(1);
243
244 (void) printf("Testing BDD decomposition algorithms\n");
245 if (option->node == NULL) {
246 for (i = 0; i < net1->noutputs; i++) {
247 if (!st_lookup(net1->hash,net1->outputs[i],(void **)&node)) {
248 return(0);
249 }
250 f = node->dd;
251 if (f == NULL) return(0);
252 result = ntrTestDecompAux(dd,net1,f,node->name,option);
253 if (result == 0) return(0);
254 }
255 } else {
256 if (!st_lookup(net1->hash,option->node,(void **)&node)) {
257 return(0);
258 }
259 f = node->dd;
260 if (f == NULL) return(0);
261 result = ntrTestDecompAux(dd,net1,f,option->node,option);
262 if (result == 0) return(0);
263 }
264
265 return(1);
266
267 } /* end of ntrTestDecomp */
268
269
270 /**
271 @brief Verify equivalence of combinational networks.
272
273 @details The two networks are supposed to have the same names for
274 inputs and outputs. The only exception is that the second network
275 may miss output buffers that are present in the first network. This
276 function tries to match both the output and the input of the buffer.
277
278 @return 1 if successful and if the networks are equivalent; -1 if
279 successful, but the networks are not equivalent; 0 otherwise.
280
281 @sideeffect None
282
283 */
284 int
Ntr_VerifyEquivalence(DdManager * dd,BnetNetwork * net1,BnetNetwork * net2,NtrOptions * option)285 Ntr_VerifyEquivalence(
286 DdManager * dd,
287 BnetNetwork * net1,
288 BnetNetwork * net2,
289 NtrOptions * option)
290 {
291 BnetNode *node;
292 char *oname;
293 DdNode *odd1, *odd2;
294 int i;
295 int pr;
296
297 (void) printf("Testing equivalence\n");
298 if (net2->noutputs != net1->noutputs) {
299 (void) printf("The two networks have different number of outputs\n");
300 (void) printf(" %s has %d outputs\n %s has %d outputs\n",
301 net1->name, net1->noutputs, net2->name, net2->noutputs);
302 return(-1);
303 }
304 if (net2->nlatches != net1->nlatches) {
305 (void) printf("The two networks have different number of latches\n");
306 (void) printf(" %s has %d latches\n %s has %d latches\n",
307 net1->name, net1->nlatches, net2->name, net2->nlatches);
308 return(-1);
309 }
310
311 pr = option->verb;
312 for (i = 0; i < net1->noutputs; i++) {
313 oname = net1->outputs[i];
314 if (!st_lookup(net1->hash,oname,(void **)&node)) {
315 return(0);
316 }
317 odd1 = node->dd;
318 (void) printf("%s", oname);
319 Cudd_PrintDebug(dd, node->dd, Cudd_ReadSize(dd), pr);
320 if (!st_lookup(net2->hash,oname,(void **)&node)) {
321 BnetNode *inpnd;
322 if ((inpnd = ntrNodeIsBuffer(node,net1->hash)) == NULL ||
323 !st_lookup(net2->hash,inpnd->name,(void **)&node)) {
324 (void) printf("Output %s missing from network %s\n",
325 oname, net2->name);
326 return(-1);
327 } else {
328 odd2 = inpnd->dd;
329 }
330 } else {
331 odd2 = node->dd;
332 }
333 if (odd1 != odd2) {
334 (void) printf("Output %s is not equivalent\n", oname);
335 return(-1);
336 }
337 }
338 return(1);
339
340 } /* end of Ntr_VerifyEquivalence */
341
342
343 /**
344 @brief Tests %BDD cofactor estimate functions.
345
346 @return 1 if successful; 0 otherwise.
347
348 @sideeffect None
349
350 */
351 int
Ntr_TestCofactorEstimate(DdManager * dd,BnetNetwork * net,NtrOptions * option)352 Ntr_TestCofactorEstimate(
353 DdManager * dd,
354 BnetNetwork * net,
355 NtrOptions * option)
356 {
357 DdNode *f;
358 BnetNode *node;
359 int i;
360 int result;
361
362 if (option->cofest == FALSE) return(1);
363
364 (void) printf("Testing BDD cofactor estimation algorithms\n");
365 if (option->node == NULL) {
366 for (i = 0; i < net->noutputs; i++) {
367 if (!st_lookup(net->hash,net->outputs[i],(void **)&node)) {
368 return(0);
369 }
370 f = node->dd;
371 if (f == NULL) return(0);
372 result = ntrTestCofEstAux(dd,net,f,node->name,option);
373 if (result == 0) return(0);
374 }
375 } else {
376 if (!st_lookup(net->hash,option->node,(void **)&node)) {
377 return(0);
378 }
379 f = node->dd;
380 if (f == NULL) return(0);
381 result = ntrTestCofEstAux(dd,net,f,option->node,option);
382 if (result == 0) return(0);
383 }
384
385 return(1);
386
387 } /* end of Ntr_TestCofactorEstimate */
388
389
390 /**
391 @brief Tests %BDD clipping functions.
392
393 @return 1 if successful; 0 otherwise.
394
395 @sideeffect None
396
397 */
398 int
Ntr_TestClipping(DdManager * dd,BnetNetwork * net1,BnetNetwork * net2,NtrOptions * option)399 Ntr_TestClipping(
400 DdManager * dd,
401 BnetNetwork * net1,
402 BnetNetwork * net2,
403 NtrOptions * option)
404 {
405 DdNode *f;
406 DdNode *g = NULL;
407 char *gname = NULL;
408 BnetNode *node;
409 int i;
410 int result;
411 int nsize, gsize;
412
413 if (option->clip < 0.0) return(1);
414
415 (void) printf("Testing BDD clipping algorithms\n");
416 /* Use largest output of second network as second operand. */
417 gsize = -1;
418 for (i = 0; i < net2->noutputs; i++) {
419 if (!st_lookup(net2->hash,net2->outputs[i],(void **)&node)) {
420 return(0);
421 }
422 nsize = Cudd_DagSize(node->dd);
423 if (nsize > gsize) {
424 g = node->dd;
425 gname = node->name;
426 gsize = nsize;
427 }
428 }
429 if (g == NULL || gname == NULL) return(0);
430 (void) printf("TEST-CLIP: Second operand (%s) %d nodes\n",
431 gname, Cudd_DagSize(g));
432
433 if (option->node == NULL) {
434 for (i = 0; i < net1->noutputs; i++) {
435 if (!st_lookup(net1->hash,net1->outputs[i],(void **)&node)) {
436 return(0);
437 }
438 f = node->dd;
439 if (f == NULL) return(0);
440 result = ntrTestClippingAux(dd,net1,f,node->name,g,gname,option);
441 if (result == 0) return(0);
442 }
443 } else {
444 if (!st_lookup(net1->hash,option->node,(void **)&node)) {
445 return(0);
446 }
447 f = node->dd;
448 if (f == NULL) return(0);
449 result = ntrTestClippingAux(dd,net1,f,option->node,g,gname,option);
450 if (result == 0) return(0);
451 }
452
453 return(1);
454
455 } /* end of Ntr_TestClipping */
456
457
458 /**
459 @brief Tests %BDD equivalence and containment with don't cares.
460
461 @details Tests functions for %BDD equivalence and containment
462 with don't cares, including Cudd_EquivDC and Cudd_bddLeqUnless. This
463 function uses as care set the first output of net2 and checkes
464 equivalence and containment for of all the output pairs of net1.
465
466 @return 1 if successful; 0 otherwise.
467
468 @sideeffect None
469
470 */
471 int
Ntr_TestEquivAndContain(DdManager * dd,BnetNetwork * net1,BnetNetwork * net2,NtrOptions * option)472 Ntr_TestEquivAndContain(
473 DdManager *dd,
474 BnetNetwork *net1,
475 BnetNetwork *net2,
476 NtrOptions *option)
477 {
478 DdNode *f, *g;
479 DdNode *d = NULL;
480 char *dname = NULL;
481 BnetNode *node1, *node2;
482 int i, j;
483 int result;
484 int nsize, dsize;
485
486 if (option->dontcares == FALSE) return(1);
487
488 (void) printf("Testing BDD equivalence and containment algorithms\n");
489 /* Use largest output of second network as constraint. */
490 dsize = -1;
491 for (i = 0; i < net2->noutputs; i++) {
492 if (!st_lookup(net2->hash,net2->outputs[i],(void **)&node1)) {
493 return(0);
494 }
495 nsize = Cudd_DagSize(node1->dd);
496 if (nsize > dsize) {
497 d = node1->dd;
498 dname = node1->name;
499 dsize = nsize;
500 }
501 }
502 if (d == NULL || dname == NULL) return(0);
503 (void) printf("TEST-DC: Don't care set (%s) %d nodes\n",
504 dname, Cudd_DagSize(d));
505
506 if (option->node == NULL) {
507 for (i = 0; i < net1->noutputs; i++) {
508 if (!st_lookup(net1->hash,net1->outputs[i],(void **)&node1)) {
509 return(0);
510 }
511 f = node1->dd;
512 if (f == NULL) return(0);
513 for (j = 0; j < net1->noutputs; j++) {
514 if (!st_lookup(net1->hash,net1->outputs[j],(void **)&node2)) {
515 return(0);
516 }
517 g = node2->dd;
518 if (g == NULL) return(0);
519 result = ntrTestEquivAndContainAux(dd,net1,f,node1->name,g,
520 node2->name,d,dname,option);
521 if (result == 0) return(0);
522 }
523 }
524 } else {
525 if (!st_lookup(net1->hash,option->node,(void **)&node1)) {
526 return(0);
527 }
528 f = node1->dd;
529 if (f == NULL) return(0);
530 for (j = 0; j < net1->noutputs; j++) {
531 if (!st_lookup(net1->hash,net1->outputs[j],(void **)&node2)) {
532 return(0);
533 }
534 g = node2->dd;
535 if (g == NULL) return(0);
536 result = ntrTestEquivAndContainAux(dd,net1,f,option->node,
537 g,node2->name,d,dname,option);
538 if (result == 0) return(0);
539 }
540 }
541
542 return(1);
543
544 } /* end of Ntr_TestEquivAndContain */
545
546
547 /**
548 @brief Tests the Cudd_bddClosestCube function.
549
550 @return 1 if successful; 0 otherwise.
551
552 @sideeffect None
553
554 */
555 int
Ntr_TestClosestCube(DdManager * dd,BnetNetwork * net,NtrOptions * option)556 Ntr_TestClosestCube(
557 DdManager * dd,
558 BnetNetwork * net,
559 NtrOptions * option)
560 {
561 DdNode *f, *g;
562 BnetNode *node1, *node2;
563 int i, j, nvars;
564 int result;
565 DdNode **vars;
566 double calls;
567
568 if (option->closestCube == FALSE) return(1);
569
570 (void) printf("Testing Cudd_bddClosestCube\n");
571 nvars = Cudd_ReadSize(dd);
572 vars = ALLOC(DdNode *, nvars);
573 if (vars == NULL) return(0);
574 for (i = 0; i < nvars; i++) {
575 vars[i] = Cudd_bddIthVar(dd,i);
576 }
577 calls = Cudd_ReadRecursiveCalls(dd);
578 if (option->node == NULL) {
579 for (i = 0; i < net->noutputs; i++) {
580 if (!st_lookup(net->hash,net->outputs[i],(void **)&node1)) {
581 FREE(vars);
582 return(0);
583 }
584 f = node1->dd;
585 if (f == NULL) {
586 FREE(vars);
587 return(0);
588 }
589 for (j = 0; j < net->noutputs; j++) {
590 if (!st_lookup(net->hash,net->outputs[j],(void **)&node2)) {
591 FREE(vars);
592 return(0);
593 }
594 g = node2->dd;
595 if (g == NULL) {
596 FREE(vars);
597 return(0);
598 }
599 result = ntrTestClosestCubeAux(dd,net,f,node1->name,g,
600 node2->name,vars,option);
601 if (result == 0) {
602 FREE(vars);
603 return(0);
604 }
605 }
606 }
607 } else {
608 if (!st_lookup(net->hash,option->node,(void **)&node1)) {
609 FREE(vars);
610 return(0);
611 }
612 f = node1->dd;
613 if (f == NULL) {
614 FREE(vars);
615 return(0);
616 }
617 for (j = 0; j < net->noutputs; j++) {
618 if (!st_lookup(net->hash,net->outputs[j],(void **)&node2)) {
619 FREE(vars);
620 return(0);
621 }
622 g = node2->dd;
623 if (g == NULL) {
624 FREE(vars);
625 return(0);
626 }
627 result = ntrTestClosestCubeAux(dd,net,f,option->node,g,
628 node2->name,vars,option);
629 if (result == 0) {
630 FREE(vars);
631 return(0);
632 }
633 }
634 }
635 (void) printf("End of test. Performed %.0f recursive calls.\n",
636 Cudd_ReadRecursiveCalls(dd) - calls);
637 FREE(vars);
638 return(1);
639
640 } /* end of Ntr_TestClosestCube */
641
642
643 /**
644 @brief Tests extraction of two-literal clauses.
645
646 @return 1 if successful; 0 otherwise.
647
648 @sideeffect None
649
650 */
651 int
Ntr_TestTwoLiteralClauses(DdManager * dd,BnetNetwork * net1,NtrOptions * option)652 Ntr_TestTwoLiteralClauses(
653 DdManager * dd,
654 BnetNetwork * net1,
655 NtrOptions * option)
656 {
657 DdNode *f;
658 BnetNode *node;
659 int result;
660 char **inames = NULL;
661 int i;
662
663 if (option->clauses == FALSE) return(1);
664
665 /* Initialize data structures. */
666 inames = ALLOC(char *,Cudd_ReadSize(dd));
667 if (inames == NULL) return(0);
668 for (i = 0; i < Cudd_ReadSize(dd); i++) {
669 inames[i] = NULL;
670 }
671
672 /* Find the input names. */
673 for (i = 0; i < net1->ninputs; i++) {
674 if (!st_lookup(net1->hash,net1->inputs[i],(void **)&node)) {
675 FREE(inames);
676 return(0);
677 }
678 inames[node->var] = net1->inputs[i];
679 }
680 for (i = 0; i < net1->nlatches; i++) {
681 if (!st_lookup(net1->hash,net1->latches[i][1],(void **)&node)) {
682 FREE(inames);
683 return(0);
684 }
685 inames[node->var] = net1->latches[i][1];
686 }
687
688 (void) printf("Testing extraction of two literal clauses\n");
689 if (option->node == NULL) {
690 for (i = 0; i < net1->noutputs; i++) {
691 if (!st_lookup(net1->hash,net1->outputs[i],(void **)&node)) {
692 return(0);
693 }
694 f = node->dd;
695 if (f == NULL) {
696 FREE(inames);
697 return(0);
698 }
699 (void) printf("*** %s ***\n", net1->outputs[i]);
700 result = Cudd_PrintTwoLiteralClauses(dd, f, inames, NULL);
701 if (result == 0) {
702 FREE(inames);
703 return(0);
704 }
705 }
706 } else {
707 if (!st_lookup(net1->hash,option->node,(void **)&node)) {
708 return(0);
709 }
710 f = node->dd;
711 if (f == NULL) {
712 FREE(inames);
713 return(0);
714 }
715 (void) printf("*** %s ***\n", option->node);
716 result = Cudd_PrintTwoLiteralClauses(dd, f, inames, NULL);
717 if (result == 0) {
718 FREE(inames);
719 return(0);
720 }
721 }
722
723 FREE(inames);
724 return(1);
725
726 } /* end of Ntr_TestTwoLiteralClauses */
727
728
729 /**
730 @brief Test char-to-vect conversion.
731
732 @return 1 if successful; 0 otherwise.
733
734 @sideeffect None
735
736 */
737 int
Ntr_TestCharToVect(DdManager * dd,BnetNetwork * net1,NtrOptions * option)738 Ntr_TestCharToVect(
739 DdManager * dd,
740 BnetNetwork * net1,
741 NtrOptions * option)
742 {
743 DdNode *f;
744 int result;
745 BnetNode *node;
746 int i;
747
748 if (option->char2vect == FALSE) return(1);
749
750 (void) printf("Testing char-to-vect\n");
751 if (net1->nlatches > 0) {
752 NtrPartTR *T;
753 T = Ntr_buildTR(dd,net1,option,NTR_IMAGE_MONO);
754 result = ntrTestCharToVect(dd,T->part[0],option);
755 Ntr_freeTR(dd,T);
756 } else if (option->node == NULL) {
757 result = 1;
758 for (i = 0; i < net1->noutputs; i++) {
759 if (!st_lookup(net1->hash,net1->outputs[i],(void **)&node)) {
760 return(0);
761 }
762 f = node->dd;
763 if (f == NULL) return(0);
764 (void) printf("*** %s ***\n", net1->outputs[i]);
765 result = ntrTestCharToVect(dd,f,option);
766 if (result == 0) return(0);
767 }
768 } else {
769 if (!st_lookup(net1->hash,option->node,(void **)&node)) {
770 return(0);
771 }
772 f = node->dd;
773 if (f == NULL) return(0);
774 result = ntrTestCharToVect(dd,f,option);
775 }
776 return(result);
777
778 } /* end of Ntr_TestCharToVect */
779
780
781 /*---------------------------------------------------------------------------*/
782 /* Definition of internal functions */
783 /*---------------------------------------------------------------------------*/
784
785 /*---------------------------------------------------------------------------*/
786 /* Definition of static functions */
787 /*---------------------------------------------------------------------------*/
788
789
790 /**
791 @brief Processes one %BDD for Ntr_TestMinimization.
792
793 @return 1 if successful; 0 otherwise.
794
795 @sideeffect None
796
797 @see Ntr_TestMinimization
798
799 */
800 static int
ntrTestMinimizationAux(DdManager * dd,BnetNetwork * net1,DdNode * f,char * name,DdNode * c,char * cname,NtrOptions * option)801 ntrTestMinimizationAux(
802 DdManager * dd,
803 BnetNetwork * net1,
804 DdNode * f,
805 char * name,
806 DdNode * c,
807 char * cname,
808 NtrOptions * option)
809 {
810 DdNode *com1, *com0, *min1, *min0, *sq1, *sq0;
811 DdNode *rs1, *rs0, *cs1, *cs0, *na1, *na0, *a1, *a0;
812 DdNode *g, *u1, *l1, *u0, *l0;
813 int pr, nvars;
814 int sizeF, sizeMin1, sizeMin0, sizeSq1, sizeSq0, sizeCom1, sizeCom0;
815 int sizeRs1, sizeRs0, sizeCs1, sizeCs0, sizeNa1, sizeNa0, sizeA1, sizeA0;
816 static char *onames[11];
817 DdNode *outputs[11];
818 DdNode *fc[2];
819
820 pr = option->verb;
821 fc[0] = f; fc[1] = c;
822 nvars = Cudd_VectorSupportSize(dd,fc,2);
823 if (nvars == CUDD_OUT_OF_MEM) return(0);
824 (void) printf("TEST-MINI:: %s\n", name);
825 (void) printf("T-M ");
826 Cudd_PrintDebug(dd, f, nvars, pr);
827 sizeF = Cudd_DagSize(f);
828
829 /* Compute positive generalized cofactor. */
830 com1 = Cudd_bddLICompaction(dd, f, c);
831 if (com1 == NULL) {
832 (void) printf("TEST-MINI: LI-compaction failed (1).\n");
833 return(0);
834 }
835 Cudd_Ref(com1);
836 (void) printf("T-M L1 ");
837 Cudd_PrintDebug(dd, com1, nvars, pr);
838 sizeCom1 = Cudd_DagSize(com1);
839 if (sizeCom1 > sizeF) {
840 (void) printf("TEST-MINI: LI-compaction not safe (1).\n");
841 return(0);
842 }
843 min1 = Cudd_bddMinimize(dd, f, c);
844 if (min1 == NULL) {
845 (void) printf("TEST-MINI: minimize failed (1).\n");
846 return(0);
847 }
848 Cudd_Ref(min1);
849 (void) printf("T-M M1 ");
850 Cudd_PrintDebug(dd, min1, nvars, pr);
851 sizeMin1 = Cudd_DagSize(min1);
852 if (sizeMin1 > sizeF) {
853 (void) printf("TEST-MINI: minimize not safe (1).\n");
854 return(0);
855 }
856 rs1 = Cudd_bddRestrict(dd, f, c);
857 if (rs1 == NULL) {
858 (void) printf("TEST-MINI: restrict failed (1).\n");
859 return(0);
860 }
861 Cudd_Ref(rs1);
862 (void) printf("T-M R1 ");
863 Cudd_PrintDebug(dd, rs1, nvars, pr);
864 sizeRs1 = Cudd_DagSize(rs1);
865 cs1 = Cudd_bddConstrain(dd, f, c);
866 if (cs1 == NULL) {
867 (void) printf("TEST-MINI: constrain failed (1).\n");
868 return(0);
869 }
870 Cudd_Ref(cs1);
871 (void) printf("T-M C1 ");
872 Cudd_PrintDebug(dd, cs1, nvars, pr);
873 sizeCs1 = Cudd_DagSize(cs1);
874 l1 = Cudd_bddAnd(dd, f, c);
875 if (l1 == NULL) {
876 (void) printf("TEST-MINI: lower bound failed (1).\n");
877 return(0);
878 }
879 Cudd_Ref(l1);
880 u1 = Cudd_bddOr(dd, f, Cudd_Not(c));
881 if (u1 == NULL) {
882 (void) printf("TEST-MINI: upper bound failed (1).\n");
883 return(0);
884 }
885 Cudd_Ref(u1);
886 (void) printf("TEST-MINI: (lb,ub) : (%d,%d) nodes\n",
887 Cudd_DagSize(l1), Cudd_DagSize(u1));
888 sq1 = Cudd_bddSqueeze(dd, l1, u1);
889 if (sq1 == NULL) {
890 (void) printf("TEST-MINI: squeezing failed (1).\n");
891 return(0);
892 }
893 Cudd_Ref(sq1);
894 sizeSq1 = Cudd_DagSize(sq1);
895 if (sizeSq1 > sizeF) {
896 Cudd_RecursiveDeref(dd,sq1);
897 sq1 = f;
898 Cudd_Ref(sq1);
899 sizeSq1 = sizeF;
900 }
901 (void) printf("T-M S1 ");
902 Cudd_PrintDebug(dd, sq1, nvars, pr);
903 na1 = Cudd_bddNPAnd(dd, f, c);
904 if (na1 == NULL) {
905 (void) printf("TEST-MINI: NPand failed (1).\n");
906 return(0);
907 }
908 Cudd_Ref(na1);
909 (void) printf("T-M N1 ");
910 Cudd_PrintDebug(dd, na1, nvars, pr);
911 sizeNa1 = Cudd_DagSize(na1);
912 a1 = Cudd_bddAnd(dd, f, c);
913 if (a1 == NULL) {
914 (void) printf("TEST-MINI: and failed (1).\n");
915 return(0);
916 }
917 Cudd_Ref(a1);
918 (void) printf("T-M A1 ");
919 Cudd_PrintDebug(dd, a1, nvars, pr);
920 sizeA1 = Cudd_DagSize(a1);
921 (void) printf("TEST-MINI: f %d comp %d mini %d rest %d cons %d sque %d na %d and %d\n",
922 sizeF, sizeCom1, sizeMin1, sizeRs1, sizeCs1, sizeSq1, sizeNa1, sizeA1);
923 if (option->bdddump) {
924 onames[0] = name; outputs[0] = f;
925 onames[1] = cname; outputs[1] = c;
926 onames[2] = (char *) "cons"; outputs[2] = cs1;
927 onames[3] = (char *) "rest"; outputs[3] = rs1;
928 onames[4] = (char *) "comp"; outputs[4] = com1;
929 onames[5] = (char *) "mini"; outputs[5] = min1;
930 onames[6] = (char *) "sqee"; outputs[6] = sq1;
931 onames[7] = (char *) "lb"; outputs[7] = l1;
932 onames[8] = (char *) "ub"; outputs[8] = u1;
933 onames[9] = (char *) "na"; outputs[9] = na1;
934 onames[10] = (char *) "and"; outputs[10] = a1;
935 if (!Bnet_bddArrayDump(dd, net1, option->dumpfile, outputs, onames,
936 11, option->dumpFmt))
937 return(0);
938 }
939 Cudd_RecursiveDeref(dd,l1);
940 Cudd_RecursiveDeref(dd,u1);
941
942 /* Compute negative generalized cofactor. */
943 (void) printf("TEST-MINI:: %s\n", name);
944 (void) printf("T-M ");
945 Cudd_PrintDebug(dd, f, nvars, pr);
946
947 com0 = Cudd_bddLICompaction(dd, f, Cudd_Not(c));
948 if (com0 == NULL) {
949 (void) printf("TEST-MINI: LI-compaction failed (2).\n");
950 return(0);
951 }
952 Cudd_Ref(com0);
953 (void) printf("T-M L0 ");
954 Cudd_PrintDebug(dd, com0, nvars, pr);
955 sizeCom0 = Cudd_DagSize(com0);
956 if (sizeCom0 > sizeF) {
957 (void) printf("TEST-MINI: LI-compaction not safe (2).\n");
958 return(0);
959 }
960 min0 = Cudd_bddMinimize(dd, f, Cudd_Not(c));
961 if (min0 == NULL) {
962 (void) printf("TEST-MINI: minimize failed (2).\n");
963 return(0);
964 }
965 Cudd_Ref(min0);
966 (void) printf("T-M M0 ");
967 Cudd_PrintDebug(dd, min0, nvars, pr);
968 sizeMin0 = Cudd_DagSize(min0);
969 if (sizeMin0 > sizeF) {
970 (void) printf("TEST-MINI: minimize not safe (2).\n");
971 return(0);
972 }
973 rs0 = Cudd_bddRestrict(dd, f, Cudd_Not(c));
974 if (rs0 == NULL) {
975 (void) printf("TEST-MINI: restrict failed (2).\n");
976 return(0);
977 }
978 Cudd_Ref(rs0);
979 (void) printf("T-M R0 ");
980 Cudd_PrintDebug(dd, rs0, nvars, pr);
981 sizeRs0 = Cudd_DagSize(rs0);
982 cs0 = Cudd_bddConstrain(dd, f, Cudd_Not(c));
983 if (cs0 == NULL) {
984 (void) printf("TEST-MINI: constrain failed (2).\n");
985 return(0);
986 }
987 Cudd_Ref(cs0);
988 (void) printf("T-M C0 ");
989 Cudd_PrintDebug(dd, cs0, nvars, pr);
990 sizeCs0 = Cudd_DagSize(cs0);
991
992 l0 = Cudd_bddAnd(dd, f, Cudd_Not(c));
993 if (l0 == NULL) {
994 (void) printf("TEST-MINI: lower bound failed (2).\n");
995 return(0);
996 }
997 Cudd_Ref(l0);
998 u0 = Cudd_bddOr(dd, f, c);
999 if (u0 == NULL) {
1000 (void) printf("TEST-MINI: upper bound failed (2).\n");
1001 return(0);
1002 }
1003 Cudd_Ref(u0);
1004 (void) printf("TEST-MINI: (lb,ub) : (%d,%d) nodes\n",
1005 Cudd_DagSize(l0), Cudd_DagSize(u0));
1006 sq0 = Cudd_bddSqueeze(dd, l0, u0);
1007 if (sq0 == NULL) {
1008 (void) printf("TEST-MINI: squeezing failed (2).\n");
1009 return(0);
1010 }
1011 Cudd_Ref(sq0);
1012 Cudd_RecursiveDeref(dd,l0);
1013 Cudd_RecursiveDeref(dd,u0);
1014 sizeSq0 = Cudd_DagSize(sq0);
1015 if (sizeSq0 > sizeF) {
1016 Cudd_RecursiveDeref(dd,sq0);
1017 sq0 = f;
1018 Cudd_Ref(sq0);
1019 sizeSq0 = sizeF;
1020 }
1021 (void) printf("T-M S0 ");
1022 Cudd_PrintDebug(dd, sq0, nvars, pr);
1023 na0 = Cudd_bddNPAnd(dd, f, Cudd_Not(c));
1024 if (na0 == NULL) {
1025 (void) printf("TEST-MINI: NPand failed (2).\n");
1026 return(0);
1027 }
1028 Cudd_Ref(na0);
1029 (void) printf("T-M N0 ");
1030 Cudd_PrintDebug(dd, na0, nvars, pr);
1031 sizeNa0 = Cudd_DagSize(na0);
1032 a0 = Cudd_bddAnd(dd, f, Cudd_Not(c));
1033 if (a0 == NULL) {
1034 (void) printf("TEST-MINI: and failed (2).\n");
1035 return(0);
1036 }
1037 Cudd_Ref(a0);
1038 (void) printf("T-M A0 ");
1039 Cudd_PrintDebug(dd, a0, nvars, pr);
1040 sizeA0 = Cudd_DagSize(a0);
1041 (void) printf("TEST-MINI: f %d comp %d mini %d rest %d cons %d sque %d na %d, and %d\n",
1042 sizeF, sizeCom0, sizeMin0, sizeRs0, sizeCs0, sizeSq0, sizeNa0, sizeA0);
1043
1044 /* Check fundamental identity. */
1045 g = Cudd_bddIte(dd,c,com1,com0);
1046 if (g == NULL) {
1047 (void) printf("TEST-MINI: LI-compaction failed (3).\n");
1048 return(0);
1049 }
1050 Cudd_Ref(g);
1051 if (g != f) {
1052 (void) printf("TEST-MINI: LI-compaction failed (4).\n");
1053 return(0);
1054 }
1055 Cudd_RecursiveDeref(dd,com1);
1056 Cudd_RecursiveDeref(dd,com0);
1057 Cudd_RecursiveDeref(dd,g);
1058 g = Cudd_bddIte(dd,c,min1,min0);
1059 if (g == NULL) {
1060 (void) printf("TEST-MINI: minimize failed (3).\n");
1061 return(0);
1062 }
1063 Cudd_Ref(g);
1064 if (g != f) {
1065 (void) printf("TEST-MINI: minimize failed (4).\n");
1066 return(0);
1067 }
1068 Cudd_RecursiveDeref(dd,min1);
1069 Cudd_RecursiveDeref(dd,min0);
1070 Cudd_RecursiveDeref(dd,g);
1071 g = Cudd_bddIte(dd,c,sq1,sq0);
1072 if (g == NULL) {
1073 (void) printf("TEST-MINI: squeezing failed (3).\n");
1074 return(0);
1075 }
1076 Cudd_Ref(g);
1077 if (g != f) {
1078 (void) printf("TEST-MINI: squeezing failed (4).\n");
1079 return(0);
1080 }
1081 Cudd_RecursiveDeref(dd,sq1);
1082 Cudd_RecursiveDeref(dd,sq0);
1083 Cudd_RecursiveDeref(dd,g);
1084 g = Cudd_bddIte(dd,c,rs1,rs0);
1085 if (g == NULL) {
1086 (void) printf("TEST-MINI: restrict failed (3).\n");
1087 return(0);
1088 }
1089 Cudd_Ref(g);
1090 if (g != f) {
1091 (void) printf("TEST-MINI: restrict failed (4).\n");
1092 return(0);
1093 }
1094 Cudd_RecursiveDeref(dd,rs1);
1095 Cudd_RecursiveDeref(dd,rs0);
1096 Cudd_RecursiveDeref(dd,g);
1097 g = Cudd_bddIte(dd,c,cs1,cs0);
1098 if (g == NULL) {
1099 (void) printf("TEST-MINI: constrain failed (3).\n");
1100 return(0);
1101 }
1102 Cudd_Ref(g);
1103 if (g != f) {
1104 (void) printf("TEST-MINI: constrain failed (4).\n");
1105 return(0);
1106 }
1107 Cudd_RecursiveDeref(dd,cs1);
1108 Cudd_RecursiveDeref(dd,cs0);
1109 Cudd_RecursiveDeref(dd,g);
1110 g = Cudd_bddIte(dd,c,na1,na0);
1111 if (g == NULL) {
1112 (void) printf("TEST-MINI: NPand failed (3).\n");
1113 return(0);
1114 }
1115 Cudd_Ref(g);
1116 if (g != f) {
1117 (void) printf("TEST-MINI: NPand failed (4).\n");
1118 return(0);
1119 }
1120 Cudd_RecursiveDeref(dd,na1);
1121 Cudd_RecursiveDeref(dd,na0);
1122 Cudd_RecursiveDeref(dd,g);
1123 g = Cudd_bddIte(dd,c,a1,a0);
1124 if (g == NULL) {
1125 (void) printf("TEST-MINI: and failed (3).\n");
1126 return(0);
1127 }
1128 Cudd_Ref(g);
1129 if (g != f) {
1130 (void) printf("TEST-MINI: and failed (4).\n");
1131 return(0);
1132 }
1133 Cudd_RecursiveDeref(dd,a1);
1134 Cudd_RecursiveDeref(dd,a0);
1135 Cudd_RecursiveDeref(dd,g);
1136
1137 return(1);
1138
1139 } /* end of ntrTestMinimizationAux */
1140
1141
1142 /**
1143 @brief Processes one %BDD for Ntr_TestDensity.
1144
1145 @return 1 if successful; 0 otherwise.
1146
1147 @sideeffect None
1148
1149 @see Ntr_TestDensity ntrCompress1
1150
1151 */
1152 static int
ntrTestDensityAux(DdManager * dd,BnetNetwork * net,DdNode * f,char * name,NtrOptions * option)1153 ntrTestDensityAux(
1154 DdManager * dd,
1155 BnetNetwork * net,
1156 DdNode * f,
1157 char * name,
1158 NtrOptions * option)
1159 {
1160 DdNode *s, *b, *hb, *sp, *ua, *c1, *c2;
1161 int pr;
1162 int result;
1163 int nvars;
1164 int size, sizeS;
1165 double densityF, densityB, densityS, densityHB, densitySP, densityUA;
1166 double densityC1, densityC2;
1167 char *onames[8];
1168 DdNode *outputs[8];
1169
1170 result = 1;
1171 pr = option->verb;
1172 nvars = Cudd_SupportSize(dd,f);
1173 if (nvars == CUDD_OUT_OF_MEM) return(0);
1174 densityF = Cudd_Density(dd,f,nvars);
1175 (void) printf("TEST-DENSITY:: %s (%d variables)\n", name, nvars);
1176 if (pr > 0) {
1177 (void) printf("T-D (%g)", densityF);
1178 Cudd_PrintDebug(dd, f, nvars, pr);
1179 (void) printf("T-D APA ");
1180 if (!Cudd_ApaPrintMinterm(stdout, dd, f, nvars))
1181 result = 0;
1182 }
1183 /* Test remapping underapproximation. */
1184 /* s = Cudd_SubsetRemap(dd,f); */
1185 s = Cudd_RemapUnderApprox(dd,f,nvars,0,option->quality);
1186 if (s == NULL) {
1187 (void) printf("TEST-DENSITY: computation failed\n");
1188 return(0);
1189 }
1190 Cudd_Ref(s);
1191 sizeS = Cudd_DagSize(s);
1192 densityS = Cudd_Density(dd,s,nvars);
1193 if (pr > 0) {
1194 (void) printf("T-D ID (%g)", densityS);
1195 Cudd_PrintDebug(dd, s, nvars, pr);
1196 }
1197 if (!Cudd_bddLeq(dd,s,f)) {
1198 (void) printf("TEST-DENSITY: result not a subset\n");
1199 result = 0;
1200 }
1201 if (densityF > densityS) {
1202 (void) printf("TEST-DENSITY: result less dense\n");
1203 /* result = 0; */
1204 }
1205 size = sizeS;
1206 /* Test biased underapproximation. */
1207 b = Cudd_BiasedUnderApprox(dd,f,Cudd_Not(s),nvars,0,
1208 option->quality*1.1,option->quality*0.5);
1209 if (b == NULL) {
1210 (void) printf("TEST-DENSITY: computation failed\n");
1211 return(0);
1212 }
1213 Cudd_Ref(b);
1214 densityB = Cudd_Density(dd,b,nvars);
1215 if (pr > 0) {
1216 (void) printf("T-D BU (%g)", densityB);
1217 Cudd_PrintDebug(dd, b, nvars, pr);
1218 }
1219 if (!Cudd_bddLeq(dd,b,f)) {
1220 (void) printf("TEST-DENSITY: result not a subset\n");
1221 result = 0;
1222 }
1223 if (densityF > densityB) {
1224 (void) printf("TEST-DENSITY: result less dense\n");
1225 /* result = 0; */
1226 }
1227 /* Test heavy-branch subsetting. */
1228 hb = Cudd_SubsetHeavyBranch(dd, f, nvars, size);
1229 if (hb == NULL) {
1230 (void) printf("TEST-DENSITY: HB computation failed\n");
1231 Cudd_RecursiveDeref(dd,s);
1232 return(0);
1233 }
1234 Cudd_Ref(hb);
1235 densityHB = Cudd_Density(dd,hb,nvars);
1236 if (pr > 0) {
1237 (void) printf("T-D HB (%g)", densityHB);
1238 Cudd_PrintDebug(dd, hb, nvars, pr);
1239 }
1240 if (!Cudd_bddLeq(dd,hb,f)) {
1241 (void) printf("TEST-DENSITY: HB not a subset\n");
1242 result = 0;
1243 }
1244 /* Test short paths subsetting. */
1245 sp = Cudd_SubsetShortPaths(dd, f, nvars, size, 0);
1246 if (sp == NULL) {
1247 (void) printf("TEST-DENSITY: SP computation failed\n");
1248 Cudd_RecursiveDeref(dd,s);
1249 Cudd_RecursiveDeref(dd,hb);
1250 return(0);
1251 }
1252 Cudd_Ref(sp);
1253 densitySP = Cudd_Density(dd,sp,nvars);
1254 if (pr > 0) {
1255 (void) printf("T-D SP (%g)", densitySP);
1256 Cudd_PrintDebug(dd, sp, nvars, pr);
1257 }
1258 if (!Cudd_bddLeq(dd,sp,f)) {
1259 (void) printf("TEST-DENSITY: SP not a subset\n");
1260 result = 0;
1261 }
1262 /* Test underapproximation. */
1263 ua = Cudd_UnderApprox(dd,f,nvars,0,FALSE,option->quality);
1264 if (ua == NULL) {
1265 (void) printf("TEST-DENSITY: computation failed\n");
1266 Cudd_RecursiveDeref(dd,s);
1267 Cudd_RecursiveDeref(dd,hb);
1268 Cudd_RecursiveDeref(dd,sp);
1269 return(0);
1270 }
1271 Cudd_Ref(ua);
1272 densityUA = Cudd_Density(dd,ua,nvars);
1273 if (pr > 0) {
1274 (void) printf("T-D UA (%g)", densityUA);
1275 Cudd_PrintDebug(dd, ua, nvars, pr);
1276 }
1277 if (!Cudd_bddLeq(dd,ua,f)) {
1278 (void) printf("TEST-DENSITY: result not a subset\n");
1279 result = 0;
1280 }
1281 if (densityF > densityUA) {
1282 (void) printf("TEST-DENSITY: result less dense\n");
1283 }
1284 /* Test compress 2 method. */
1285 c1 = ntrCompress2(dd, f, nvars, size);
1286 if (c1 == NULL) {
1287 (void) printf("TEST-DENSITY: C1 computation failed\n");
1288 Cudd_RecursiveDeref(dd,s);
1289 Cudd_RecursiveDeref(dd,hb);
1290 Cudd_RecursiveDeref(dd,sp);
1291 Cudd_RecursiveDeref(dd,ua);
1292 return(0);
1293 }
1294 densityC1 = Cudd_Density(dd,c1,nvars);
1295 if (pr > 0) {
1296 (void) printf("T-D C1 (%g)", densityC1);
1297 Cudd_PrintDebug(dd, c1, nvars, pr);
1298 }
1299 if (!Cudd_bddLeq(dd,c1,f)) {
1300 (void) printf("TEST-DENSITY: C1 not a subset\n");
1301 result = 0;
1302 }
1303 /* Test compress subsetting. */
1304 c2 = Cudd_SubsetCompress(dd, f, nvars, size);
1305 if (c2 == NULL) {
1306 (void) printf("TEST-DENSITY: C2 computation failed\n");
1307 Cudd_RecursiveDeref(dd,s);
1308 Cudd_RecursiveDeref(dd,hb);
1309 Cudd_RecursiveDeref(dd,sp);
1310 Cudd_RecursiveDeref(dd,ua);
1311 Cudd_RecursiveDeref(dd,c1);
1312 return(0);
1313 }
1314 Cudd_Ref(c2);
1315 densityC2 = Cudd_Density(dd,c2,nvars);
1316 if (pr > 0) {
1317 (void) printf("T-D C2 (%g)", densityC2);
1318 Cudd_PrintDebug(dd, c2, nvars, pr);
1319 }
1320 if (!Cudd_bddLeq(dd,c2,f)) {
1321 (void) printf("TEST-DENSITY: C2 not a subset\n");
1322 result = 0;
1323 }
1324 /* Dump results if so requested. */
1325 if (option->bdddump) {
1326 onames[0] = name; outputs[0] = f;
1327 onames[1] = (char *) "id"; outputs[1] = s;
1328 onames[2] = (char *) "bu"; outputs[2] = b;
1329 onames[3] = (char *) "hb"; outputs[3] = hb;
1330 onames[4] = (char *) "sp"; outputs[4] = sp;
1331 onames[5] = (char *) "ua"; outputs[5] = ua;
1332 onames[6] = (char *) "c1"; outputs[6] = c1;
1333 onames[7] = (char *) "c2"; outputs[7] = c2;
1334 result &= Bnet_bddArrayDump(dd, net, option->dumpfile, outputs,
1335 onames, 8, option->dumpFmt);
1336 }
1337
1338 Cudd_RecursiveDeref(dd,s);
1339 Cudd_RecursiveDeref(dd,b);
1340 Cudd_RecursiveDeref(dd,hb);
1341 Cudd_RecursiveDeref(dd,sp);
1342 Cudd_RecursiveDeref(dd,ua);
1343 Cudd_RecursiveDeref(dd,c1);
1344 Cudd_RecursiveDeref(dd,c2);
1345
1346 return(result);
1347
1348 } /* end of ntrTestDensityAux */
1349
1350
1351 /**
1352 @brief Processes one %BDD for Ntr_TestDecomp.
1353
1354 @return 1 if successful; 0 otherwise.
1355
1356 @sideeffect None
1357
1358 @see Ntr_TestDecomp
1359
1360 */
1361 static int
ntrTestDecompAux(DdManager * dd,BnetNetwork * net,DdNode * f,char * name,NtrOptions * option)1362 ntrTestDecompAux(
1363 DdManager * dd,
1364 BnetNetwork * net,
1365 DdNode * f,
1366 char * name,
1367 NtrOptions * option)
1368 {
1369 DdNode *one, *g, *h, *product;
1370 DdNode **A, **I, **G, **V;
1371 int pr;
1372 int i, result;
1373 int nA, nI, nG, nV;
1374 int nvars;
1375 int sizeSa;
1376 int sizeSi, sizeSg, sizeSv;
1377 char *onames[9];
1378 DdNode *outputs[9];
1379
1380 result = 1;
1381 pr = option->verb;
1382 nvars = Cudd_SupportSize(dd,f);
1383 if (nvars == CUDD_OUT_OF_MEM) return(0);
1384 (void) printf("TEST-DECOMP:: %s (%d variables)\n", name, nvars);
1385 if (pr > 0) {
1386 (void) printf("T-d ");
1387 Cudd_PrintDebug(dd, f, nvars, pr);
1388 }
1389 one = Cudd_ReadOne(dd);
1390
1391 /* Test Cudd_bddApproxConjDecomp */
1392 nA = Cudd_bddApproxConjDecomp(dd,f,&A);
1393 if (nA == 0) {
1394 (void) printf("TEST-DECOMP: computation failed\n");
1395 return(0);
1396 }
1397 g = A[0];
1398 h = (nA == 2) ? A[1] : one;
1399 sizeSa = Cudd_SharingSize(A,nA);
1400 if (pr > 0) {
1401 (void) printf("T-d SS : %d nodes\n", sizeSa);
1402 (void) printf("T-d GS ");
1403 Cudd_PrintDebug(dd, g, nvars, pr);
1404 (void) printf("T-d HS ");
1405 Cudd_PrintDebug(dd, h, nvars, pr);
1406 }
1407 product = Cudd_bddAnd(dd,g,h);
1408 if (product == NULL) {
1409 (void) printf("TEST-DECOMP: computation failed\n");
1410 return(0);
1411 }
1412 Cudd_Ref(product);
1413 if (product != f) {
1414 (void) printf("TEST-DECOMP: result not a decomposition\n");
1415 result = 0;
1416 }
1417 Cudd_RecursiveDeref(dd,product);
1418
1419 /* Test Cudd_bddIterConjDecomp */
1420 nI = Cudd_bddIterConjDecomp(dd,f,&I);
1421 if (nI == 0) {
1422 (void) printf("TEST-DECOMP: computation failed\n");
1423 return(0);
1424 }
1425 g = I[0];
1426 h = (nI == 2) ? I[1] : one;
1427 sizeSi = Cudd_SharingSize(I,nI);
1428 if (pr > 0) {
1429 (void) printf("T-d SI : %d nodes\n", sizeSi);
1430 (void) printf("T-d GI ");
1431 Cudd_PrintDebug(dd, g, nvars, pr);
1432 (void) printf("T-d HI ");
1433 Cudd_PrintDebug(dd, h, nvars, pr);
1434 }
1435 product = Cudd_bddAnd(dd,g,h);
1436 if (product == NULL) {
1437 (void) printf("TEST-DECOMP: computation failed\n");
1438 return(0);
1439 }
1440 Cudd_Ref(product);
1441 if (product != f) {
1442 (void) printf("TEST-DECOMP: result not a decomposition\n");
1443 result = 0;
1444 }
1445 Cudd_RecursiveDeref(dd,product);
1446
1447 /* Test Cudd_bddGenConjDecomp */
1448 nG = Cudd_bddGenConjDecomp(dd,f,&G);
1449 if (nG == 0) {
1450 (void) printf("TEST-DECOMP: computation failed\n");
1451 return(0);
1452 }
1453 g = G[0];
1454 h = (nG == 2) ? G[1] : one;
1455 sizeSg = Cudd_SharingSize(G,nG);
1456 if (pr > 0) {
1457 (void) printf("T-d SD : %d nodes\n", sizeSg);
1458 (void) printf("T-d GD ");
1459 Cudd_PrintDebug(dd, g, nvars, pr);
1460 (void) printf("T-d HD ");
1461 Cudd_PrintDebug(dd, h, nvars, pr);
1462 }
1463 product = Cudd_bddAnd(dd,g,h);
1464 if (product == NULL) {
1465 (void) printf("TEST-DECOMP: computation failed\n");
1466 return(0);
1467 }
1468 Cudd_Ref(product);
1469 if (product != f) {
1470 (void) printf("TEST-DECOMP: result not a decomposition\n");
1471 result = 0;
1472 }
1473 Cudd_RecursiveDeref(dd,product);
1474
1475 /* Test Cudd_bddVarConjDecomp */
1476 nV = Cudd_bddVarConjDecomp(dd,f,&V);
1477 if (nV == 0) {
1478 (void) printf("TEST-DECOMP: computation failed\n");
1479 return(0);
1480 }
1481 g = V[0];
1482 h = (nV == 2) ? V[1] : one;
1483 sizeSv = Cudd_SharingSize(V,nV);
1484 if (pr > 0) {
1485 (void) printf("T-d SQ : %d nodes\n", sizeSv);
1486 (void) printf("T-d GQ ");
1487 Cudd_PrintDebug(dd, g, nvars, pr);
1488 (void) printf("T-d HQ ");
1489 Cudd_PrintDebug(dd, h, nvars, pr);
1490 }
1491 product = Cudd_bddAnd(dd,g,h);
1492 if (product == NULL) {
1493 (void) printf("TEST-DECOMP: computation failed\n");
1494 return(0);
1495 }
1496 Cudd_Ref(product);
1497 if (product != f) {
1498 (void) printf("TEST-DECOMP: result not a decomposition\n");
1499 result = 0;
1500 }
1501 Cudd_RecursiveDeref(dd,product);
1502
1503 /* Dump to file if requested. */
1504 if (option->bdddump) {
1505 onames[0] = name; outputs[0] = f;
1506 onames[1] = (char *) "ga"; outputs[1] = A[0];
1507 onames[2] = (char *) "ha"; outputs[2] = (nA == 2) ? A[1] : one;
1508 onames[3] = (char *) "gi"; outputs[3] = I[0];
1509 onames[4] = (char *) "hi"; outputs[4] = (nI == 2) ? I[1] : one;
1510 onames[5] = (char *) "gg"; outputs[5] = G[0];
1511 onames[6] = (char *) "hg"; outputs[6] = (nG == 2) ? G[1] : one;
1512 onames[7] = (char *) "gv"; outputs[7] = V[0];
1513 onames[8] = (char *) "hv"; outputs[8] = (nV == 2) ? V[1] : one;
1514 result &= Bnet_bddArrayDump(dd, net, option->dumpfile, outputs,
1515 onames, 9, option->dumpFmt);
1516 }
1517
1518 /* Clean up. */
1519 for (i = 0; i < nA; i++) {
1520 Cudd_RecursiveDeref(dd,A[i]);
1521 }
1522 for (i = 0; i < nI; i++) {
1523 Cudd_RecursiveDeref(dd,I[i]);
1524 }
1525 for (i = 0; i < nG; i++) {
1526 Cudd_RecursiveDeref(dd,G[i]);
1527 }
1528 for (i = 0; i < nV; i++) {
1529 Cudd_RecursiveDeref(dd,V[i]);
1530 }
1531 FREE(A);
1532 FREE(I);
1533 FREE(G);
1534 FREE(V);
1535
1536 return(result);
1537
1538 } /* end of ntrTestDecompAux */
1539
1540
1541 /**
1542 @brief Processes one %BDD for Ntr_TestCofactorEstimate.
1543
1544 @return 1 if successful; 0 otherwise.
1545
1546 @sideeffect None
1547
1548 */
1549 static int
ntrTestCofEstAux(DdManager * dd,BnetNetwork * net,DdNode * f,char * name,NtrOptions * option)1550 ntrTestCofEstAux(
1551 DdManager * dd,
1552 BnetNetwork * net,
1553 DdNode * f,
1554 char * name,
1555 NtrOptions * option)
1556 {
1557 DdNode *support, *scan, *cof;
1558 int pr;
1559 int nvars;
1560 int exactSize, estimate, estimateS;
1561 int totalExactSize = 0;
1562 int totalEstimate = 0;
1563 int totalEstimateS = 0;
1564 int largestError = -1;
1565 int largestErrorS = -1;
1566 DdNode *errorVar = NULL;
1567
1568 pr = option->verb;
1569 support = Cudd_Support(dd,f);
1570 if (support == NULL) return(0);
1571 Cudd_Ref(support);
1572 nvars = Cudd_DagSize(support) - 1;
1573 scan = support;
1574 while (!Cudd_IsConstant(scan)) {
1575 DdNode *var = Cudd_bddIthVar(dd,scan->index);
1576 cof = Cudd_Cofactor(dd,f,var);
1577 if (cof == NULL) return(0);
1578 Cudd_Ref(cof);
1579 exactSize = Cudd_DagSize(cof);
1580 totalExactSize += exactSize;
1581 estimate = Cudd_EstimateCofactor(dd,f,scan->index,1);
1582 totalEstimate += estimate;
1583 if (estimate < exactSize)
1584 (void) printf("Optimistic estimate!\n");
1585 if (estimate - exactSize > largestError) {
1586 largestError = estimate - exactSize;
1587 errorVar = var;
1588 }
1589 estimateS = Cudd_EstimateCofactorSimple(f,scan->index);
1590 totalEstimateS += estimateS;
1591 if (estimateS < exactSize)
1592 (void) printf("Optimistic estimateS!\n");
1593 if (estimateS - exactSize > largestErrorS)
1594 largestErrorS = estimateS - exactSize;
1595 Cudd_RecursiveDeref(dd,cof);
1596 scan = cuddT(scan);
1597 }
1598 Cudd_RecursiveDeref(dd,support);
1599 (void) printf("TEST-COF:: %s (%d vars)", name, nvars);
1600 Cudd_PrintDebug(dd, f, nvars, pr);
1601 (void) printf("T-c : %d\n", totalExactSize);
1602 (void) printf("T-c E : %d %d\n", totalEstimate, largestError);
1603 (void) printf("T-c S : %d %d\n", totalEstimateS, largestErrorS);
1604
1605 /* Dump to file if requested. */
1606 if (option->bdddump) {
1607 char *onames[3];
1608 DdNode *outputs[3];
1609 int result;
1610 cof = Cudd_Cofactor(dd,f,errorVar);
1611 if (cof == NULL) return(0);
1612 Cudd_Ref(cof);
1613 onames[0] = name; outputs[0] = f;
1614 onames[1] = (char *) "var"; outputs[1] = errorVar;
1615 onames[2] = (char *) "cof"; outputs[2] = cof;
1616 result = Bnet_bddArrayDump(dd, net, option->dumpfile, outputs,
1617 onames, 3, option->dumpFmt);
1618 Cudd_RecursiveDeref(dd,cof);
1619 if (result == 0) return(0);
1620 }
1621
1622 return(1);
1623
1624 } /* end of ntrTestCofEstAux */
1625
1626
1627 /**
1628 @brief Processes one %BDD for Ntr_TestClipping.
1629
1630 @details It checks whether clipping was correct.
1631
1632 @return 1 if successful; 0 otherwise.
1633
1634 @sideeffect None
1635
1636 @see Ntr_TestClipping
1637
1638 */
1639 static int
ntrTestClippingAux(DdManager * dd,BnetNetwork * net1,DdNode * f,char * name,DdNode * g,char * gname,NtrOptions * option)1640 ntrTestClippingAux(
1641 DdManager * dd,
1642 BnetNetwork * net1,
1643 DdNode * f,
1644 char * name,
1645 DdNode * g,
1646 char * gname,
1647 NtrOptions * option)
1648 {
1649 DdNode *prod, *sub, *sup;
1650 DdNode *subF, *subG, *psub;
1651 DdNode *supF, *supG, *psup;
1652 int pr, nvars, depth;
1653 int sizeProd, sizeSub, sizeSup;
1654 static char *onames[7];
1655 DdNode *outputs[7];
1656 DdNode *operands[2];
1657 int retval = 1;
1658 int threshold = (option->threshold < 0) ? 0 : option->threshold;
1659
1660 pr = option->verb;
1661 operands[0] = f; operands[1] = g;
1662 nvars = Cudd_VectorSupportSize(dd,operands,2);
1663 if (nvars == CUDD_OUT_OF_MEM) return(0);
1664 depth = (int) ((double) nvars * option->clip);
1665 (void) printf("TEST-CLIP:: %s depth = %d\n", name, depth);
1666 (void) printf("T-C ");
1667 Cudd_PrintDebug(dd, f, nvars, pr);
1668
1669 /* Compute product. */
1670 prod = Cudd_bddAnd(dd, f, g);
1671 if (prod == NULL) {
1672 (void) printf("TEST-CLIP: product failed.\n");
1673 return(0);
1674 }
1675 Cudd_Ref(prod);
1676 (void) printf("T-C P= ");
1677 Cudd_PrintDebug(dd, prod, nvars, pr);
1678 sizeProd = Cudd_DagSize(prod);
1679
1680 /* Compute subset of product. */
1681 sub = Cudd_bddClippingAnd(dd, f, g, depth, 0);
1682 if (sub == NULL) {
1683 (void) printf("TEST-CLIP: subsetting product failed.\n");
1684 return(0);
1685 }
1686 Cudd_Ref(sub);
1687 (void) printf("T-C P- ");
1688 Cudd_PrintDebug(dd, sub, nvars, pr);
1689 sizeSub = Cudd_DagSize(sub);
1690 if (sizeSub > sizeProd) {
1691 (void) printf("TEST-CLIP: subsetting product not safe.\n");
1692 }
1693
1694 /* Compute product of subsets. */
1695 subF = Cudd_RemapUnderApprox(dd,f,nvars,threshold,option->quality);
1696 if (subF == NULL) {
1697 (void) printf("TEST-CLIP: subsetting of f failed.\n");
1698 return(0);
1699 }
1700 Cudd_Ref(subF);
1701 subG = Cudd_RemapUnderApprox(dd,g,nvars,threshold,option->quality);
1702 if (subF == NULL) {
1703 (void) printf("TEST-CLIP: subsetting of g failed.\n");
1704 return(0);
1705 }
1706 Cudd_Ref(subG);
1707 psub = Cudd_bddAnd(dd,subF,subG);
1708 if (psub == NULL) {
1709 (void) printf("TEST-CLIP: product of subsets failed.\n");
1710 return(0);
1711 }
1712 Cudd_Ref(psub);
1713 Cudd_RecursiveDeref(dd,subF);
1714 Cudd_RecursiveDeref(dd,subG);
1715 (void) printf("T-C P< ");
1716 Cudd_PrintDebug(dd, psub, nvars, pr);
1717
1718 /* Compute superset of product. */
1719 sup = Cudd_bddClippingAnd(dd, f, g, depth, 1);
1720 if (sup == NULL) {
1721 (void) printf("TEST-CLIP: supersetting product failed.\n");
1722 return(0);
1723 }
1724 Cudd_Ref(sup);
1725 (void) printf("T-C P+ ");
1726 Cudd_PrintDebug(dd, sup, nvars, pr);
1727 sizeSup = Cudd_DagSize(sup);
1728 if (sizeSup > sizeProd) {
1729 (void) printf("TEST-CLIP: supersetting product not safe.\n");
1730 }
1731
1732 /* Compute product of supersets. */
1733 supF = Cudd_RemapOverApprox(dd,f,nvars,threshold,option->quality);
1734 if (supF == NULL) {
1735 (void) printf("TEST-CLIP: supersetting of f failed.\n");
1736 return(0);
1737 }
1738 Cudd_Ref(supF);
1739 supG = Cudd_RemapOverApprox(dd,g,nvars,threshold,option->quality);
1740 if (supF == NULL) {
1741 (void) printf("TEST-CLIP: supersetting of g failed.\n");
1742 return(0);
1743 }
1744 Cudd_Ref(supG);
1745 psup = Cudd_bddAnd(dd,supF,supG);
1746 if (psup == NULL) {
1747 (void) printf("TEST-CLIP: product of supersets failed.\n");
1748 return(0);
1749 }
1750 Cudd_Ref(psup);
1751 Cudd_RecursiveDeref(dd,supF);
1752 Cudd_RecursiveDeref(dd,supG);
1753 (void) printf("T-C P> ");
1754 Cudd_PrintDebug(dd, psup, nvars, pr);
1755
1756 if (option->bdddump) {
1757 onames[0] = name; outputs[0] = f;
1758 onames[1] = gname; outputs[1] = g;
1759 onames[2] = (char *) "prod"; outputs[2] = prod;
1760 onames[3] = (char *) "sub"; outputs[3] = sub;
1761 onames[4] = (char *) "sup"; outputs[4] = sup;
1762 onames[5] = (char *) "psub"; outputs[5] = psub;
1763 onames[6] = (char *) "psup"; outputs[6] = psup;
1764 retval &= Bnet_bddArrayDump(dd, net1, option->dumpfile, outputs,
1765 onames, 7, option->dumpFmt);
1766 }
1767
1768 /* Check correctness. */
1769 if (!Cudd_bddLeq(dd,sub,prod)) {
1770 (void) printf("TEST-CLIP: subsetting product not a subset.\n");
1771 return(0);
1772 }
1773 if (!Cudd_bddLeq(dd,prod,sup)) {
1774 (void) printf("TEST-CLIP: supersetting product not a superset.\n");
1775 return(0);
1776 }
1777 if (!Cudd_bddLeq(dd,psub,prod)) {
1778 (void) printf("TEST-CLIP: product of subsets not a subset.\n");
1779 return(0);
1780 }
1781 if (!Cudd_bddLeq(dd,prod,psup)) {
1782 (void) printf("TEST-CLIP: product of supersets not a superset.\n");
1783 return(0);
1784 }
1785
1786 Cudd_RecursiveDeref(dd,prod);
1787 Cudd_RecursiveDeref(dd,sub);
1788 Cudd_RecursiveDeref(dd,sup);
1789 Cudd_RecursiveDeref(dd,psub);
1790 Cudd_RecursiveDeref(dd,psup);
1791
1792 return(retval);
1793
1794 } /* end of ntrTestClippingAux */
1795
1796
1797
1798 /**
1799 @brief Processes one triplet of BDDs for Ntr_TestEquivAndContain.
1800
1801 @return 1 if successful; 0 otherwise.
1802
1803 @sideeffect None
1804
1805 @see Ntr_TestEquivAndContain
1806
1807 */
1808 static int
ntrTestEquivAndContainAux(DdManager * dd,BnetNetwork * net1,DdNode * f,char * fname,DdNode * g,char * gname,DdNode * d,char * dname,NtrOptions * option)1809 ntrTestEquivAndContainAux(
1810 DdManager *dd,
1811 BnetNetwork *net1,
1812 DdNode *f,
1813 char *fname,
1814 DdNode *g,
1815 char *gname,
1816 DdNode *d,
1817 char *dname,
1818 NtrOptions *option)
1819 {
1820 DdNode *xor_, *diff, *ndiff;
1821 int pr, nvars;
1822 int equiv, implies;
1823 static char *onames[6];
1824 DdNode *outputs[6];
1825 DdNode *fgd[3];
1826
1827 pr = option->verb;
1828 fgd[0] = f; fgd[1] = g; fgd[2] = d;
1829 nvars = Cudd_VectorSupportSize(dd,fgd,3);
1830 if (nvars == CUDD_OUT_OF_MEM) return(0);
1831 (void) printf("TEST-DC:: %s [=<]= %s unless %s\n", fname, gname, dname);
1832 (void) printf("T-F ");
1833 Cudd_PrintDebug(dd, f, nvars, pr);
1834 (void) printf("T-G ");
1835 Cudd_PrintDebug(dd, g, nvars, pr);
1836 (void) printf("T-D ");
1837 Cudd_PrintDebug(dd, d, nvars, pr);
1838
1839 /* Check equivalence unless don't cares. */
1840 xor_ = Cudd_bddXor(dd, f, g);
1841 if (xor_ == NULL) {
1842 (void) printf("TEST-DC: XOR computation failed (1).\n");
1843 return(0);
1844 }
1845 Cudd_Ref(xor_);
1846 equiv = Cudd_EquivDC(dd, f, g, d);
1847 if (equiv != Cudd_bddLeq(dd,xor_,d)) {
1848 (void) printf("TEST-DC: EquivDC computation incorrect (1).\n");
1849 (void) printf(" EquivDC states that %s and %s are %s\n",
1850 fname, gname, equiv ? "equivalent" : "not equivalent");
1851 (void) printf("T-X ");
1852 Cudd_PrintDebug(dd, xor_, nvars, pr);
1853 return(0);
1854 }
1855 equiv = Cudd_EquivDC(dd, f, g, Cudd_Not(d));
1856 if (equiv != Cudd_bddLeq(dd,xor_,Cudd_Not(d))) {
1857 (void) printf("TEST-DC: EquivDC computation incorrect (2).\n");
1858 (void) printf(" EquivDC states that %s and %s are %s\n",
1859 fname, gname, equiv ? "equivalent" : "not equivalent");
1860 (void) printf("T-X ");
1861 Cudd_PrintDebug(dd, xor_, nvars, pr);
1862 return(0);
1863 }
1864 equiv = Cudd_EquivDC(dd, f, Cudd_Not(g), d);
1865 if (equiv != Cudd_bddLeq(dd,Cudd_Not(xor_),d)) {
1866 (void) printf("TEST-DC: EquivDC computation incorrect (3).\n");
1867 (void) printf(" EquivDC states that %s and not %s are %s\n",
1868 fname, gname, equiv ? "equivalent" : "not equivalent");
1869 (void) printf("T-X ");
1870 Cudd_PrintDebug(dd, Cudd_Not(xor_), nvars, pr);
1871 return(0);
1872 }
1873 equiv = Cudd_EquivDC(dd, f, Cudd_Not(g), Cudd_Not(d));
1874 if (equiv != Cudd_bddLeq(dd,d,xor_)) {
1875 (void) printf("TEST-DC: EquivDC computation incorrect (4).\n");
1876 (void) printf(" EquivDC states that %s and not %s are %s\n",
1877 fname, gname, equiv ? "equivalent" : "not equivalent");
1878 (void) printf("T-X ");
1879 Cudd_PrintDebug(dd, Cudd_Not(xor_), nvars, pr);
1880 return(0);
1881 }
1882
1883 /* Check containment unless don't cares. */
1884 diff = Cudd_bddAnd(dd, f, Cudd_Not(g));
1885 if (diff == NULL) {
1886 (void) printf("TEST-DC: AND/NOT computation failed (1).\n");
1887 return(0);
1888 }
1889 Cudd_Ref(diff);
1890 implies = Cudd_bddLeqUnless(dd, f, g, d);
1891 if (implies != Cudd_bddLeq(dd,diff,d)) {
1892 (void) printf("TEST-DC: LeqUnless computation incorrect (1).\n");
1893 (void) printf(" LeqUnless states that %s %s %s\n",
1894 fname, implies ? "implies" : "does not imply", gname);
1895 (void) printf("T-I ");
1896 Cudd_PrintDebug(dd, diff, nvars, pr);
1897 return(0);
1898 }
1899 implies = Cudd_bddLeqUnless(dd, f, g, Cudd_Not(d));
1900 if (implies != Cudd_bddLeq(dd,diff,Cudd_Not(d))) {
1901 (void) printf("TEST-DC: LeqUnless computation incorrect (2).\n");
1902 (void) printf(" LeqUnless states that %s %s %s\n",
1903 fname, implies ? "implies" : "does not imply", gname);
1904 (void) printf("T-I ");
1905 Cudd_PrintDebug(dd, diff, nvars, pr);
1906 return(0);
1907 }
1908 ndiff = Cudd_bddAnd(dd, f, g);
1909 if (ndiff == NULL) {
1910 (void) printf("TEST-DC: AND computation failed (3).\n");
1911 return(0);
1912 }
1913 Cudd_Ref(ndiff);
1914 implies = Cudd_bddLeqUnless(dd, f, Cudd_Not(g), d);
1915 if (implies != Cudd_bddLeq(dd,ndiff,d)) {
1916 (void) printf("TEST-DC: LeqUnless computation incorrect (3).\n");
1917 (void) printf(" LeqUnless states that %s %s not(%s)\n",
1918 fname, implies ? "implies" : "does not imply", gname);
1919 (void) printf("T-I ");
1920 Cudd_PrintDebug(dd, ndiff, nvars, pr);
1921 return(0);
1922 }
1923 implies = Cudd_bddLeqUnless(dd, f, Cudd_Not(g), Cudd_Not(d));
1924 if (implies != Cudd_bddLeq(dd,ndiff,Cudd_Not(d))) {
1925 (void) printf("TEST-DC: LeqUnless computation incorrect (3).\n");
1926 (void) printf(" LeqUnless states that %s %s not(%s)\n",
1927 fname, implies ? "implies" : "does not imply", gname);
1928 (void) printf("T-I ");
1929 Cudd_PrintDebug(dd, ndiff, nvars, pr);
1930 return(0);
1931 }
1932 if (option->bdddump) {
1933 onames[0] = fname; outputs[0] = f;
1934 onames[1] = gname; outputs[1] = g;
1935 onames[2] = dname; outputs[2] = d;
1936 onames[3] = (char *) "xor"; outputs[3] = xor_;
1937 onames[4] = (char *) "diff"; outputs[4] = diff;
1938 onames[5] = (char *) "ndiff"; outputs[5] = ndiff;
1939 if (!Bnet_bddArrayDump(dd, net1, option->dumpfile, outputs, onames,
1940 6, option->dumpFmt))
1941 return(0);
1942 }
1943 Cudd_RecursiveDeref(dd,xor_);
1944 Cudd_RecursiveDeref(dd,diff);
1945 Cudd_RecursiveDeref(dd,ndiff);
1946
1947 return(1);
1948
1949 } /* end of ntrTestEquivAndContainAux */
1950
1951
1952 /**
1953 @brief Processes one pair of BDDs for Ntr_TestClosestCube.
1954
1955 @return 1 if successful; 0 otherwise.
1956
1957 @sideeffect None
1958
1959 @see Ntr_TestClosestCube
1960
1961 */
1962 static int
ntrTestClosestCubeAux(DdManager * dd,BnetNetwork * net,DdNode * f,char * fname,DdNode * g,char * gname,DdNode ** vars,NtrOptions * option)1963 ntrTestClosestCubeAux(
1964 DdManager *dd,
1965 BnetNetwork *net,
1966 DdNode *f,
1967 char *fname,
1968 DdNode *g,
1969 char *gname,
1970 DdNode **vars,
1971 NtrOptions *option)
1972 {
1973 DdNode *cube, *cubeN;
1974 int distance, pr, nvars;
1975 DdNode *fg[2];
1976 static char *onames[4];
1977 DdNode *outputs[4];
1978
1979 pr = option->verb;
1980 fg[0] = f; fg[1] = g;
1981 nvars = Cudd_VectorSupportSize(dd,fg,2);
1982 if (nvars == CUDD_OUT_OF_MEM) return(0);
1983 (void) printf("TEST-CC:: H(%s, %s)\n", fname, gname);
1984 (void) printf("T-F ");
1985 Cudd_PrintDebug(dd, f, nvars, pr);
1986 (void) printf("T-G ");
1987 Cudd_PrintDebug(dd, g, nvars, pr);
1988
1989 cube = Cudd_bddClosestCube(dd, f, g, &distance);
1990 if (cube == NULL) {
1991 (void) printf("TEST-CC: computation failed (1).\n");
1992 return(0);
1993 }
1994 Cudd_Ref(cube);
1995 (void) printf("T-C (%d) ", distance);
1996 Cudd_PrintDebug(dd, cube, nvars, pr);
1997 if (distance == 0) {
1998 if (!Cudd_bddLeq(dd,cube,g)) {
1999 (void) printf("TEST-CC: distance-0 cube not in g (2).\n");
2000 return(0);
2001 }
2002 }
2003
2004 (void) printf("T-GN ");
2005 Cudd_PrintDebug(dd, Cudd_Not(g), nvars, pr);
2006 cubeN = Cudd_bddClosestCube(dd, f, Cudd_Not(g), &distance);
2007 if (cubeN == NULL) {
2008 (void) printf("TEST-CC: computation failed (3).\n");
2009 return(0);
2010 }
2011 Cudd_Ref(cubeN);
2012 (void) printf("T-N (%d) ", distance);
2013 Cudd_PrintDebug(dd, cubeN, nvars, pr);
2014 if (distance == 0) {
2015 if (!Cudd_bddLeq(dd,cubeN,Cudd_Not(g))) {
2016 (void) printf("TEST-CC: distance-0 cube not in not(g) (4).\n");
2017 return(0);
2018 }
2019 } else {
2020 int d, *minterm;
2021 int numvars = Cudd_ReadSize(dd);
2022 DdNode *scan, *zero;
2023 DdNode *minBdd = Cudd_bddPickOneMinterm(dd,cubeN,vars,numvars);
2024 if (minBdd == NULL) {
2025 (void) printf("TEST-CC: minterm selection failed (5).\n");
2026 return(0);
2027 }
2028 Cudd_Ref(minBdd);
2029 minterm = ALLOC(int,numvars);
2030 if (minterm == NULL) {
2031 (void) printf("TEST-CC: allocation failed (6).\n");
2032 Cudd_RecursiveDeref(dd,minBdd);
2033 return(0);
2034 }
2035 scan = minBdd;
2036 zero = Cudd_Not(DD_ONE(dd));
2037 while (!Cudd_IsConstant(scan)) {
2038 DdNode *R = Cudd_Regular(scan);
2039 DdNode *T = Cudd_T(R);
2040 DdNode *E = Cudd_E(R);
2041 if (R != scan) {
2042 T = Cudd_Not(T);
2043 E = Cudd_Not(E);
2044 }
2045 if (T == zero) {
2046 minterm[Cudd_NodeReadIndex(R)] = 0;
2047 scan = E;
2048 } else {
2049 minterm[Cudd_NodeReadIndex(R)] = 1;
2050 scan = T;
2051 }
2052 }
2053 Cudd_RecursiveDeref(dd,minBdd);
2054 d = Cudd_MinHammingDist(dd,Cudd_Not(g),minterm,numvars);
2055 FREE(minterm);
2056 if (d != distance) {
2057 (void) printf("TEST-CC: distance disagreement (7).\n");
2058 return(0);
2059 }
2060 }
2061
2062 if (option->bdddump) {
2063 onames[0] = fname; outputs[0] = f;
2064 onames[1] = gname; outputs[1] = g;
2065 onames[2] = (char *) "cube"; outputs[2] = cube;
2066 onames[3] = (char *) "cubeN"; outputs[3] = cubeN;
2067 if (!Bnet_bddArrayDump(dd, net, option->dumpfile, outputs, onames,
2068 4, option->dumpFmt))
2069 return(0);
2070 }
2071 Cudd_RecursiveDeref(dd,cube);
2072 Cudd_RecursiveDeref(dd,cubeN);
2073
2074 return(1);
2075
2076 } /* end of ntrTestClosestCubeAux */
2077
2078
2079 /**
2080 @brief Processes one BDDs for Ntr_TestCharToVect.
2081
2082 @return 1 if successful; 0 otherwise.
2083
2084 @sideeffect None
2085
2086 @see Ntr_TestCharToVect
2087
2088 */
2089 static int
ntrTestCharToVect(DdManager * dd,DdNode * f,NtrOptions * option)2090 ntrTestCharToVect(
2091 DdManager * dd,
2092 DdNode * f,
2093 NtrOptions *option)
2094 {
2095 DdNode **vector;
2096 int sharingSize;
2097 DdNode *verify;
2098 int pr = option->verb;
2099 int i;
2100
2101 (void) fprintf(stdout,"f");
2102 Cudd_PrintDebug(dd, f, Cudd_ReadSize(dd), 1);
2103 if (pr > 1) {
2104 Cudd_bddPrintCover(dd, f, f);
2105 }
2106 vector = Cudd_bddCharToVect(dd,f);
2107 if (vector == NULL) return(0);
2108 sharingSize = Cudd_SharingSize(vector, Cudd_ReadSize(dd));
2109 (void) fprintf(stdout, "Vector Size: %d components %d nodes\n",
2110 Cudd_ReadSize(dd), sharingSize);
2111 for (i = 0; i < Cudd_ReadSize(dd); i++) {
2112 (void) fprintf(stdout,"v[%d]",i);
2113 Cudd_PrintDebug(dd, vector[i], Cudd_ReadSize(dd), 1);
2114 if (pr > 1) {
2115 Cudd_bddPrintCover(dd, vector[i], vector[i]);
2116 }
2117 }
2118 verify = Cudd_bddVectorCompose(dd,f,vector);
2119 if (verify != Cudd_ReadOne(dd)) {
2120 (void) fprintf(stdout, "Verification failed!\n");
2121 return(0);
2122 }
2123 Cudd_Ref(verify);
2124 Cudd_IterDerefBdd(dd, verify);
2125 for (i = 0; i < Cudd_ReadSize(dd); i++) {
2126 Cudd_IterDerefBdd(dd, vector[i]);
2127 }
2128 FREE(vector);
2129 return(1);
2130
2131 } /* end of ntrTestCharToVect */
2132
2133
2134 #if 0
2135 /**
2136 @brief Try hard to squeeze a %BDD.
2137
2138 @return a pointer to the squeezed %BDD if successful; NULL otherwise.
2139
2140 @sideeffect None
2141
2142 @see ntrTestDensityAux Cudd_SubsetCompress
2143
2144 */
2145 static DdNode *
2146 ntrCompress1(
2147 DdManager * dd,
2148 DdNode * f,
2149 int nvars,
2150 int threshold)
2151 {
2152 DdNode *res, *tmp1, *tmp2;
2153 int sizeI, size;
2154
2155 tmp1 = Cudd_RemapUnderApprox(dd,f,nvars,0,1.0);
2156 if (tmp1 == NULL) return(NULL);
2157 Cudd_Ref(tmp1);
2158 sizeI = Cudd_DagSize(tmp1);
2159 size = (sizeI < threshold) ? sizeI : threshold;
2160 tmp2 = Cudd_SubsetShortPaths(dd, tmp1, nvars, size, 0);
2161 if (tmp2 == NULL) {
2162 Cudd_RecursiveDeref(dd,tmp1);
2163 return(NULL);
2164 }
2165 Cudd_Ref(tmp2);
2166 Cudd_RecursiveDeref(dd,tmp1);
2167 res = Cudd_bddSqueeze(dd,tmp2,f);
2168 if (res == NULL) {
2169 Cudd_RecursiveDeref(dd,tmp2);
2170 return(NULL);
2171 }
2172 Cudd_Ref(res);
2173 Cudd_RecursiveDeref(dd,tmp2);
2174 return(res);
2175
2176 } /* end of ntrCompress1 */
2177 #endif
2178
2179
2180 /**
2181 @brief Try hard to squeeze a %BDD.
2182
2183 @return a pointer to the squeezed %BDD if successful; NULL otherwise.
2184
2185 @sideeffect None
2186
2187 @see ntrTestDensityAux Cudd_SubsetCompress
2188
2189 */
2190 static DdNode *
ntrCompress2(DdManager * dd,DdNode * f,int nvars,int threshold)2191 ntrCompress2(
2192 DdManager * dd,
2193 DdNode * f,
2194 int nvars,
2195 int threshold)
2196 {
2197 DdNode *res, *tmp1, *tmp2;
2198 int sizeI;
2199
2200 tmp1 = Cudd_RemapUnderApprox(dd,f,nvars,0,1.0);
2201 if (tmp1 == NULL) return(NULL);
2202 Cudd_Ref(tmp1);
2203 sizeI = Cudd_DagSize(tmp1);
2204 if (sizeI > threshold) {
2205 tmp2 = Cudd_SubsetShortPaths(dd, tmp1, nvars, threshold, 0);
2206 if (tmp2 == NULL) {
2207 Cudd_RecursiveDeref(dd,tmp1);
2208 return(NULL);
2209 }
2210 Cudd_Ref(tmp2);
2211 Cudd_RecursiveDeref(dd,tmp1);
2212 } else {
2213 tmp2 = tmp1;
2214 }
2215 res = Cudd_bddSqueeze(dd,tmp2,f);
2216 if (res == NULL) {
2217 Cudd_RecursiveDeref(dd,tmp2);
2218 return(NULL);
2219 }
2220 Cudd_Ref(res);
2221 if (Cudd_Density(dd,res,nvars) < Cudd_Density(dd,tmp2,nvars)) {
2222 Cudd_RecursiveDeref(dd,res);
2223 return(tmp2);
2224 } else {
2225 Cudd_RecursiveDeref(dd,tmp2);
2226 return(res);
2227 }
2228
2229 } /* end of ntrCompress2 */
2230
2231
2232 /**
2233 @brief Checks whether node is a buffer.
2234
2235 @return a pointer to the input node if nd is a buffer; NULL
2236 otherwise.
2237
2238 @sideeffect None
2239
2240 */
2241 static BnetNode *
ntrNodeIsBuffer(BnetNode * nd,st_table * hash)2242 ntrNodeIsBuffer(
2243 BnetNode *nd,
2244 st_table *hash)
2245 {
2246 BnetNode *inpnd;
2247
2248 if (nd->ninp != 1) return(0);
2249 if (!st_lookup(hash, nd->inputs[0], (void **) &inpnd)) return(0);
2250
2251 return(nd->dd == inpnd->dd ? inpnd : NULL);
2252
2253 } /* end of ntrNodeIsBuffer */
2254