Version abc60220

6 files changed, 441 insertions, 6 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 0d0c93a8..666d7388 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -37,9 +37,11 @@
 /* Nested includes                                                           */
 /*---------------------------------------------------------------------------*/
 
+#include <stdio.h>
+#include <stdlib.h>
 #include <string.h>
+#include <assert.h>
 #include <time.h>
-#include "util.h"
 #include "st.h"
 #include "cuddInt.h"
 
@@ -155,6 +157,7 @@ extern DdNode *     Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
 extern DdNode *     Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
 extern DdNode *     Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst );
 extern DdNode *     Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f );
+extern int          Extra_bddIsVar( DdNode * bFunc );
 
 /*=== extraBddKmap.c ================================================================*/
 
@@ -408,6 +411,27 @@ extern void        Extra_IntVecPush( Extra_IntVec_t * p, int Entry );
 extern int         Extra_IntVecPop( Extra_IntVec_t * p );
 extern void        Extra_IntVecSort( Extra_IntVec_t * p );
 
+/*=== extraUtilUtil.c ================================================================*/
+
+#define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
+#define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+#define REALLOC(type, obj, num)    \
+        (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
+        ((type *) malloc(sizeof(type) * (num)))
+
+extern long        Extra_CpuTime();
+extern int         Extra_GetSoftDataLimit();
+extern void        Extra_UtilGetoptReset();
+extern int         Extra_UtilGetopt( int argc, char *argv[], char *optstring );
+extern char *      Extra_UtilPrintTime( long t );
+extern char *      Extra_UtilStrsav( char *s );
+extern char *      Extra_UtilTildeExpand( char *fname );
+extern char *      Extra_UtilFileSearch( char *file, char *path, char *mode );
+extern void        (*Extra_UtilMMoutOfMemory)();
+
+extern char *      globalUtilOptarg;
+extern int         globalUtilOptind;
+
 /**AutomaticEnd***************************************************************/
 
 #endif /* __EXTRA_H__ */
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 7d806ec7..00e2ac94 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -52,8 +52,8 @@ static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdN
 static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute );
 
 // file "cuddUtils.c"
-static void ddSupportStep ARGS((DdNode *f, int *support));
-static void ddClearFlag ARGS((DdNode *f));
+static void ddSupportStep(DdNode *f, int *support);
+static void ddClearFlag(DdNode *f);
 
 /**AutomaticEnd***************************************************************/
 
@@ -796,6 +796,25 @@ DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f )
 
 }                                /* end of Extra_SupportNeg */
 
+/**Function********************************************************************
+
+  Synopsis    [Returns 1 if the BDD is the BDD of elementary variable.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_VectorSupport Cudd_Support]
+
+******************************************************************************/
+int Extra_bddIsVar( DdNode * bFunc )
+{
+    bFunc = Cudd_Regular( bFunc );
+    if ( cuddIsConstant(bFunc) )
+        return 0;
+    return cuddIsConstant( cuddT(bFunc) ) && cuddIsConstant( Cudd_Regular(cuddE(bFunc)) );
+}
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/
diff --git a/src/misc/extra/extraUtil.h b/src/misc/extra/extraUtil.h
new file mode 100644
index 00000000..d3f432c2
--- /dev/null
+++ b/src/misc/extra/extraUtil.h
@@ -0,0 +1,60 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtil.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [Various reusable software utilities.]
+
+  Description []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: extraUtil.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __EXTRA_UTIL_H__
+#define __EXTRA_UTIL_H__
+
+/*---------------------------------------------------------------------------*/
+/* Nested includes                                                           */
+/*---------------------------------------------------------------------------*/
+
+#include <string.h>
+#include <time.h>
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/*===========================================================================*/
+/*     Various Utilities                                                     */
+/*===========================================================================*/
+
+
+/**AutomaticEnd***************************************************************/
+
+#endif /* __EXTRA_UTIL_H__ */
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index 03b31fea..b00125d1 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -172,7 +172,7 @@ char * Extra_FileNameGeneric( char * FileName )
     char * pRes;
     
     // find the generic name of the file
-    pRes = util_strsav( FileName );
+    pRes = Extra_UtilStrsav( FileName );
     // find the pointer to the "." symbol in the file name
 //  pUnd = strstr( FileName, "_" );
     pUnd = NULL;
@@ -391,7 +391,7 @@ char * Extra_StringAppend( char * pStrGiven, char * pStrAdd )
         free( pStrGiven );
     }
     else
-        pTemp = util_strsav( pStrAdd );
+        pTemp = Extra_UtilStrsav( pStrAdd );
     return pTemp;
 }
 
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
new file mode 100644
index 00000000..71d3f652
--- /dev/null
+++ b/src/misc/extra/extraUtilUtil.c
@@ -0,0 +1,330 @@
+/**CFile****************************************************************
+
+  FileName    [extraUtilUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [Old SIS utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: extraUtilUtil.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "stdio.h"
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define EXTRA_RLIMIT_DATA_DEFAULT 67108864  // assume 64MB by default 
+
+/*  File   : getopt.c
+ *  Author : Henry Spencer, University of Toronto
+ *  Updated: 28 April 1984
+ *
+ *  Changes: (R Rudell)
+ *  changed index() to strchr();
+ *  added getopt_reset() to reset the getopt argument parsing
+ *
+ *  Purpose: get option letter from argv.
+ */
+
+char * globalUtilOptarg;        // Global argument pointer (util_optarg)
+int    globalUtilOptind = 0;    // Global argv index (util_optind)
+
+static char *pScanStr;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [util_cpu_time()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+long Extra_CpuTime()
+{
+    return clock();
+}
+
+/**Function*************************************************************
+
+  Synopsis    [getSoftDataLimit()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_GetSoftDataLimit()
+{
+    return EXTRA_RLIMIT_DATA_DEFAULT;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [util_getopt_reset()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_UtilGetoptReset()
+{
+    globalUtilOptarg = 0;
+    globalUtilOptind = 0;
+    pScanStr = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [util_getopt()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_UtilGetopt( int argc, char *argv[], char *optstring )
+{
+    register int c;
+    register char *place;
+
+    globalUtilOptarg = NULL;
+
+    if (pScanStr == NULL || *pScanStr == '\0') {
+    if (globalUtilOptind == 0) globalUtilOptind++;
+    if (globalUtilOptind >= argc) return EOF;
+    place = argv[globalUtilOptind];
+    if (place[0] != '-' || place[1] == '\0') return EOF;
+    globalUtilOptind++;
+    if (place[1] == '-' && place[2] == '\0') return EOF;
+    pScanStr = place+1;
+    }
+
+    c = *pScanStr++;
+    place = strchr(optstring, c);
+    if (place == NULL || c == ':') {
+    (void) fprintf(stderr, "%s: unknown option %c\n", argv[0], c);
+    return '?';
+    }
+    if (*++place == ':') {
+    if (*pScanStr != '\0') {
+        globalUtilOptarg = pScanStr;
+        pScanStr = NULL;
+    } else {
+        if (globalUtilOptind >= argc) {
+        (void) fprintf(stderr, "%s: %c requires an argument\n", 
+            argv[0], c);
+        return '?';
+        }
+        globalUtilOptarg = argv[globalUtilOptind];
+        globalUtilOptind++;
+    }
+    }
+    return c;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [util_print_time()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_UtilPrintTime( long t )
+{
+    static char s[40];
+
+    (void) sprintf(s, "%ld.%02ld sec", t/1000, (t%1000)/10);
+    return s;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Extra_UtilStrsav()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_UtilStrsav( char *s )
+{
+    if(s == NULL) {  /* added 7/95, for robustness */
+       return s;
+    }
+    else {
+       return strcpy(ALLOC(char, strlen(s)+1), s);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [util_tilde_expand()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_UtilTildeExpand( char *fname )
+{
+    return Extra_UtilStrsav( fname );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [check_file()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_UtilCheckFile(char *filename, char *mode)
+{
+    FILE *fp;
+    int got_file;
+
+    if (strcmp(mode, "x") == 0) {
+    mode = "r";
+    }
+    fp = fopen(filename, mode);
+    got_file = (fp != 0);
+    if (fp != 0) {
+    (void) fclose(fp);
+    }
+    return got_file;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [util_file_search()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Extra_UtilFileSearch(char *file, char *path, char *mode)
+//char *file;            // file we're looking for 
+//char *path;            // search path, colon separated 
+//char *mode;            // "r", "w", or "x" 
+{
+    int quit;
+    char *buffer, *filename, *save_path, *cp;
+
+    if (path == 0 || strcmp(path, "") == 0) {
+    path = ".";        /* just look in the current directory */
+    }
+
+    save_path = path = Extra_UtilStrsav(path);
+    quit = 0;
+    do {
+    cp = strchr(path, ':');
+    if (cp != 0) {
+        *cp = '\0';
+    } else {
+        quit = 1;
+    }
+
+    /* cons up the filename out of the path and file name */
+    if (strcmp(path, ".") == 0) {
+        buffer = Extra_UtilStrsav(file);
+    } else {
+        buffer = ALLOC(char, strlen(path) + strlen(file) + 4);
+        (void) sprintf(buffer, "%s/%s", path, file);
+    }
+    filename = Extra_UtilTildeExpand(buffer);
+    FREE(buffer);
+
+    /* see if we can access it */
+    if (Extra_UtilCheckFile(filename, mode)) {
+        FREE(save_path);
+        return filename;
+    }
+    FREE(filename);
+    path = ++cp;
+    } while (! quit); 
+
+    FREE(save_path);
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [MMout_of_memory()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/* MMout_of_memory -- out of memory for lazy people, flush and exit */
+void Extra_UtilMMout_Of_Memory( long size )
+{
+    (void) fflush(stdout);
+    (void) fprintf(stderr, "\nout of memory allocating %u bytes\n",
+           (unsigned) size);
+    assert( 0 );
+    exit(1);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [MMoutOfMemory()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void (*Extra_UtilMMoutOfMemory)() = Extra_UtilMMout_Of_Memory;
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index 8e7b1772..c4da05e4 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -2,10 +2,12 @@ SRC +=    src/misc/extra/extraBddAuto.c \
     src/misc/extra/extraBddKmap.c \
     src/misc/extra/extraBddMisc.c \
     src/misc/extra/extraBddSymm.c \
+    src/misc/extra/extraBddUnate.c \
     src/misc/extra/extraUtilBitMatrix.c \
     src/misc/extra/extraUtilCanon.c \
     src/misc/extra/extraUtilFile.c \
     src/misc/extra/extraUtilMemory.c \
     src/misc/extra/extraUtilMisc.c \
     src/misc/extra/extraUtilProgress.c \
-    src/misc/extra/extraUtilReader.c
+    src/misc/extra/extraUtilReader.c \
+    src/misc/extra/extraUtilUtil.c