From e7b544f11151f09a4a3fbe39b4a176795a82f677 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 13 Feb 2011 13:42:25 -0800 Subject: Upgrade to the latest CUDD 2.4.2. --- src/bdd/cudd/testcudd.c | 178 +++++++++++++++++++++++++++++++++++------------- 1 file changed, 129 insertions(+), 49 deletions(-) (limited to 'src/bdd/cudd/testcudd.c') diff --git a/src/bdd/cudd/testcudd.c b/src/bdd/cudd/testcudd.c index 1b6de5aa..f21f7816 100644 --- a/src/bdd/cudd/testcudd.c +++ b/src/bdd/cudd/testcudd.c @@ -16,19 +16,43 @@ Author [Fabio Somenzi] - Copyright [ This file was created at the University of Colorado at - Boulder. The University of Colorado at Boulder makes no warranty - about the suitability of this software for any purpose. It is - presented on an AS IS basis.] + Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado + + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + Neither the name of the University of Colorado nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS + FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; + LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN + ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + POSSIBILITY OF SUCH DAMAGE.] ******************************************************************************/ -#include "util_hack.h" +#include "util.h" #include "cuddInt.h" -ABC_NAMESPACE_IMPL_START - - /*---------------------------------------------------------------------------*/ /* Constant declarations */ @@ -41,10 +65,10 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: testcudd.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: testcudd.c,v 1.20 2009/03/08 02:49:02 fabio Exp $"; #endif -static char *onames[] = { "C", "M" }; /* names of functions to be dumped */ +static const char *onames[] = { "C", "M" }; /* names of functions to be dumped */ /**AutomaticStart*************************************************************/ @@ -52,12 +76,12 @@ static char *onames[] = { "C", "M" }; /* names of functions to be dumped */ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static void usage ARGS((char * prog)); -static FILE *open_file ARGS((char *filename, char *mode)); -static int testIterators ARGS((DdManager *dd, DdNode *M, DdNode *C, int pr)); -static int testXor ARGS((DdManager *dd, DdNode *f, int pr, int nvars)); -static int testHamming ARGS((DdManager *dd, DdNode *f, int pr, int nvars)); -static int testWalsh ARGS((DdManager *dd, int N, int cmu, int approach, int pr)); +static void usage (char * prog); +static FILE *open_file (char *filename, const char *mode); +static int testIterators (DdManager *dd, DdNode *M, DdNode *C, int pr); +static int testXor (DdManager *dd, DdNode *f, int pr, int nvars); +static int testHamming (DdManager *dd, DdNode *f, int pr); +static int testWalsh (DdManager *dd, int N, int cmu, int approach, int pr); /**AutomaticEnd***************************************************************/ @@ -77,17 +101,17 @@ int main(int argc, char **argv) { FILE *fp; /* pointer to input file */ - char *file = ""; /* input file name */ + char *file = (char *) ""; /* input file name */ FILE *dfp = NULL; /* pointer to dump file */ char *dfile; /* file for DD dump */ DdNode *dfunc[2]; /* addresses of the functions to be dumped */ DdManager *dd; /* pointer to DD manager */ - DdNode *one, *zero; /* fast access to constant functions */ + DdNode *one; /* fast access to constant function */ DdNode *M; DdNode **x; /* pointers to variables */ DdNode **y; /* pointers to variables */ - DdNode **xn; /* complements of row variables */ - DdNode **yn_; /* complements of column variables */ + DdNode **xn; /* complements of row variables */ + DdNode **yn_; /* complements of column variables */ DdNode **xvars; DdNode **yvars; DdNode *C; /* result of converting from ADD to BDD */ @@ -149,7 +173,7 @@ main(int argc, char **argv) blifOrDot = 0; /* dot format */ /* Parse command line. */ - while ((c = util_getopt(argc, argv, "CDHMPS:a:bcd:g:hkmn:p:v:x:X:")) + while ((c = util_getopt(argc, argv, (char *) "CDHMPS:a:bcd:g:hkmn:p:v:x:X:")) != EOF) { switch(c) { case 'C': @@ -216,7 +240,7 @@ main(int argc, char **argv) } if (argc - util_optind == 0) { - file = "-"; + file = (char *) "-"; } else if (argc - util_optind == 1) { file = argv[util_optind]; } else { @@ -241,7 +265,6 @@ main(int argc, char **argv) /* Initialize manager and provide easy reference to terminals. */ dd = Cudd_Init(nvars,0,nslots,cacheSize,maxMemory); one = DD_ONE(dd); - zero = DD_ZERO(dd); dd->groupcheck = (Cudd_AggregationType) groupcheck; if (autodyn) Cudd_AutodynEnable(dd,CUDD_REORDER_SAME); @@ -335,7 +358,7 @@ main(int argc, char **argv) if (retval == 0) exit(2); /* Test Hamming distance functions. */ - retval = testHamming(dd,C,pr,nx+ny); + retval = testHamming(dd,C,pr); if (retval == 0) exit(2); /* Test selection functions. */ @@ -356,6 +379,43 @@ main(int argc, char **argv) } Cudd_RecursiveDeref(dd, CPr); } + + /* Test inequality generator. */ + { + int Nmin = ddMin(nx,ny); + int q; + DdGen *gen; + int *cube; + DdNode *f = Cudd_Inequality(dd,Nmin,2,xvars,yvars); + if (f == NULL) exit(2); + Cudd_Ref(f); + if (pr>0) { + (void) printf(":4: ineq"); + Cudd_PrintDebug(dd,f,nx+ny,pr); + if (pr>1) { + Cudd_ForeachPrime(dd,Cudd_Not(f),Cudd_Not(f),gen,cube) { + for (q = 0; q < dd->size; q++) { + switch (cube[q]) { + case 0: + (void) printf("1"); + break; + case 1: + (void) printf("0"); + break; + case 2: + (void) printf("-"); + break; + default: + (void) printf("?"); + } + } + (void) printf(" 1\n"); + } + (void) printf("\n"); + } + } + Cudd_IterDerefBdd(dd, f); + } FREE(xvars); FREE(yvars); Cudd_RecursiveDeref(dd, CP); @@ -419,7 +479,7 @@ main(int argc, char **argv) } /* Reorder if so requested. */ - if (approach != CUDD_REORDER_NONE) { + if (approach != CUDD_REORDER_NONE) { #ifndef DD_STATS retval = Cudd_EnableReorderingReporting(dd); if (retval == 0) { @@ -502,9 +562,10 @@ main(int argc, char **argv) dfunc[1] = M; if (blifOrDot == 1) { /* Only dump C because blif cannot handle ADDs */ - retval = Cudd_DumpBlif(dd,1,dfunc,NULL,onames,NULL,dfp); + retval = Cudd_DumpBlif(dd,1,dfunc,NULL,(char **)onames, + NULL,dfp,0); } else { - retval = Cudd_DumpDot(dd,2,dfunc,NULL,onames,dfp); + retval = Cudd_DumpDot(dd,2,dfunc,NULL,(char **)onames,dfp); } if (retval != 1) { (void) fprintf(stderr,"abnormal termination\n"); @@ -524,9 +585,9 @@ main(int argc, char **argv) } if (pr>0) { (void) printf("Number of variables = %6d\t",dd->size); - (void) printf("Number of slots = %6d\n",dd->slots); - (void) printf("Number of keys = %6d\t",dd->keys); - (void) printf("Number of min dead = %6d\n",dd->minDead); + (void) printf("Number of slots = %6u\n",dd->slots); + (void) printf("Number of keys = %6u\t",dd->keys); + (void) printf("Number of min dead = %6u\n",dd->minDead); } } while (multiple && !feof(fp)); @@ -643,15 +704,15 @@ usage(char *prog) ******************************************************************************/ static FILE * -open_file(char *filename, char *mode) +open_file(char *filename, const char *mode) { FILE *fp; if (strcmp(filename, "-") == 0) { - return mode[0] == 'r' ? stdin : stdout; + return mode[0] == 'r' ? stdin : stdout; } else if ((fp = fopen(filename, mode)) == NULL) { - perror(filename); - exit(1); + perror(filename); + exit(1); } return fp; @@ -798,34 +859,56 @@ testIterators( if (!Cudd_bddPrintCover(dd,C,C)) return(0); } + if (pr>1) { + (void) printf("Testing iterator on primes (CNF):\n"); + Cudd_ForeachPrime(dd,Cudd_Not(C),Cudd_Not(C),gen,cube) { + for (q = 0; q < dd->size; q++) { + switch (cube[q]) { + case 0: + (void) printf("1"); + break; + case 1: + (void) printf("0"); + break; + case 2: + (void) printf("-"); + break; + default: + (void) printf("?"); + } + } + (void) printf(" 1\n"); + } + (void) printf("\n"); + } + /* Test iterator on nodes. */ if (pr>2) { - DdGen *gen; DdNode *node; (void) printf("Testing iterator on nodes:\n"); Cudd_ForeachNode(dd,M,gen,node) { if (Cudd_IsConstant(node)) { #if SIZEOF_VOID_P == 8 (void) printf("ID = 0x%lx\tvalue = %-9g\n", - (unsigned long) node / - (unsigned long) sizeof(DdNode), + (ptruint) node / + (ptruint) sizeof(DdNode), Cudd_V(node)); #else (void) printf("ID = 0x%x\tvalue = %-9g\n", - (unsigned int) node / - (unsigned int) sizeof(DdNode), + (ptruint) node / + (ptruint) sizeof(DdNode), Cudd_V(node)); #endif } else { #if SIZEOF_VOID_P == 8 - (void) printf("ID = 0x%lx\tindex = %d\tr = %d\n", - (unsigned long) node / - (unsigned long) sizeof(DdNode), + (void) printf("ID = 0x%lx\tindex = %u\tr = %u\n", + (ptruint) node / + (ptruint) sizeof(DdNode), node->index, node->ref); #else - (void) printf("ID = 0x%x\tindex = %d\tr = %d\n", - (unsigned int) node / - (unsigned int) sizeof(DdNode), + (void) printf("ID = 0x%x\tindex = %u\tr = %u\n", + (ptruint) node / + (ptruint) sizeof(DdNode), node->index, node->ref); #endif } @@ -932,8 +1015,7 @@ static int testHamming( DdManager *dd, DdNode *f, - int pr, - int nvars) + int pr) { DdNode **vars, *minBdd, *zero, *scan; int i; @@ -989,5 +1071,3 @@ testHamming( return(1); } /* end of testHamming */ -ABC_NAMESPACE_IMPL_END - -- cgit v1.2.3