source: icGREP/icgrep-devel/cudd-2.5.1/nanotrav/ntrBddTest.c

Last change on this file was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

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