Major restructuring of the code.

14 files changed, 334 insertions, 332 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 693c25bd..0bef042c 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -26,8 +26,8 @@
 
 ***********************************************************************/
 
-#ifndef __EXTRA_H__
-#define __EXTRA_H__
+#ifndef ABC__misc__extra__extra_h
+#define ABC__misc__extra__extra_h
 
 
 #ifdef _WIN32
@@ -44,10 +44,7 @@
 #include <assert.h>
 #include <time.h>
 
-#include "st.h"
-#include "cuddInt.h"
-
-
+#include "src/misc/st/st.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -76,239 +73,10 @@ typedef unsigned char      uint8;
 typedef unsigned short     uint16;
 typedef unsigned int       uint32;
 
-/* constants of the manager */
-#define     b0     Cudd_Not((dd)->one)
-#define     b1              (dd)->one
-#define     z0              (dd)->zero
-#define     z1              (dd)->one
-#define     a0              (dd)->zero
-#define     a1              (dd)->one
-
-// hash key macros
-#define hashKey1(a,TSIZE) \
-((ABC_PTRUINT_T)(a) % TSIZE)
-
-#define hashKey2(a,b,TSIZE) \
-(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE)
-
-#define hashKey3(a,b,c,TSIZE) \
-(((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)
-
-#define hashKey4(a,b,c,d,TSIZE) \
-((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
-   (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE)
-
-#define hashKey5(a,b,c,d,e,TSIZE) \
-(((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
-   (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE)
-
 /*===========================================================================*/
 /*     Various Utilities                                                     */
 /*===========================================================================*/
 
-/*=== extraBddAuto.c ========================================================*/
-
-extern DdNode *     Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc );
-extern DdNode *     Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
-extern DdNode *      extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
-extern DdNode *     Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
-extern DdNode *      extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
-extern DdNode *     Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
-extern DdNode *      extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
-
-extern DdNode *     Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
-extern DdNode *      extraBddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
-
-extern DdNode *     Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace );
-extern DdNode *     Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
-extern DdNode *      extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
-extern DdNode *     Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
-extern DdNode *      extraBddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
-
-extern DdNode *     Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
-extern DdNode *      extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
-extern DdNode *     Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
-extern DdNode *      extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
-
-extern DdNode *     Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars );
-extern DdNode **    Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations );
-
-/*=== extraBddCas.c =============================================================*/
-
-/* performs the binary encoding of the set of function using the given vars */
-extern DdNode *     Extra_bddEncodingBinary( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars );
-/* solves the column encoding problem using a sophisticated method */
-extern DdNode *     Extra_bddEncodingNonStrict( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple );
-/* collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root */
-extern st_table *   Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel );
-/* collects the nodes under the cut starting from the given set of ADD nodes */
-extern int          Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel );
-/* find the profile of a DD (the number of edges crossing each level) */
-extern int          Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel );
-
-/*=== extraBddImage.c ================================================================*/
-
-typedef struct Extra_ImageTree_t_  Extra_ImageTree_t;
-extern Extra_ImageTree_t * Extra_bddImageStart( 
-    DdManager * dd, DdNode * bCare,
-    int nParts, DdNode ** pbParts,
-    int nVars, DdNode ** pbVars, int fVerbose );
-extern DdNode *    Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare );
-extern void        Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree );
-extern DdNode *    Extra_bddImageRead( Extra_ImageTree_t * pTree );
-
-typedef struct Extra_ImageTree2_t_  Extra_ImageTree2_t;
-extern Extra_ImageTree2_t * Extra_bddImageStart2( 
-    DdManager * dd, DdNode * bCare,
-    int nParts, DdNode ** pbParts,
-    int nVars, DdNode ** pbVars, int fVerbose );
-extern DdNode *    Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare );
-extern void        Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree );
-extern DdNode *    Extra_bddImageRead2( Extra_ImageTree2_t * pTree );
-
-/*=== extraBddMisc.c ========================================================*/
-
-extern DdNode *     Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
-extern DdNode *     Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
-extern DdNode *     Extra_bddRemapUp( DdManager * dd, DdNode * bF );
-extern DdNode *     Extra_bddMove( DdManager * dd, DdNode * bF, int nVars );
-extern DdNode *     extraBddMove( DdManager * dd, DdNode * bF, DdNode * bFlag );
-extern void         Extra_StopManager( DdManager * dd );
-extern void         Extra_bddPrint( DdManager * dd, DdNode * F );
-extern void         Extra_bddPrintSupport( DdManager * dd, DdNode * F );
-extern void         extraDecomposeCover( DdManager* dd, DdNode*  zC, DdNode** zC0, DdNode** zC1, DdNode** zC2 );
-extern int          Extra_bddSuppSize( DdManager * dd, DdNode * bSupp );
-extern int          Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar );
-extern int          Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 );
-extern int          Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax );
-extern int          Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall );
-extern int *        Extra_SupportArray( DdManager * dd, DdNode * F, int * support );
-extern int *        Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support );
-extern DdNode *     Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
-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 );
-extern DdNode *     Extra_bddCreateAnd( DdManager * dd, int nVars );
-extern DdNode *     Extra_bddCreateOr( DdManager * dd, int nVars );
-extern DdNode *     Extra_bddCreateExor( DdManager * dd, int nVars );
-extern DdNode *     Extra_zddPrimes( DdManager * dd, DdNode * F );
-extern void         Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
-extern DdNode *     Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
-extern DdNode *     Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
-extern DdNode *     extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
-extern int          Extra_bddVarIsInCube( DdNode * bCube, int iVar );
-extern DdNode *     Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
-
-#ifndef ABC_PRB
-#define ABC_PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
-#endif
-
-/*=== extraBddKmap.c ================================================================*/
-
-/* displays the Karnaugh Map of a function */
-extern void        Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames );
-/* displays the Karnaugh Map of a relation */
-extern void        Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars );
-
-/*=== extraBddSymm.c =================================================================*/
-
-typedef struct Extra_SymmInfo_t_  Extra_SymmInfo_t;
-struct Extra_SymmInfo_t_ {
-    int nVars;      // the number of variables in the support
-    int nVarsMax;   // the number of variables in the DD manager
-    int nSymms;     // the number of pair-wise symmetries
-    int nNodes;     // the number of nodes in a ZDD (if applicable)
-    int * pVars;    // the list of all variables present in the support
-    char ** pSymms; // the symmetry information
-};
-
-/* computes the classical symmetry information for the function - recursive */
-extern Extra_SymmInfo_t *  Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc );
-/* computes the classical symmetry information for the function - using naive approach */
-extern Extra_SymmInfo_t *  Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc );
-extern int         Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
-
-/* allocates the data structure */
-extern Extra_SymmInfo_t *  Extra_SymmPairsAllocate( int nVars );
-/* deallocates the data structure */
-extern void        Extra_SymmPairsDissolve( Extra_SymmInfo_t * );
-/* print the contents the data structure */
-extern void        Extra_SymmPairsPrint( Extra_SymmInfo_t * );
-/* converts the ZDD into the Extra_SymmInfo_t structure */
-extern Extra_SymmInfo_t *  Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars );
-
-/* computes the classical symmetry information as a ZDD */
-extern DdNode *    Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
-extern DdNode *     extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
-/* returns a singleton-set ZDD containing all variables that are symmetric with the given one */
-extern DdNode *    Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
-extern DdNode *     extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
-/* converts a set of variables into a set of singleton subsets */
-extern DdNode *    Extra_zddGetSingletons( DdManager * dd, DdNode * bVars );
-extern DdNode *     extraZddGetSingletons( DdManager * dd, DdNode * bVars );
-/* filters the set of variables using the support of the function */
-extern DdNode *    Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
-extern DdNode *     extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
-
-/* checks the possibility that the two vars are symmetric */
-extern int         Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
-extern DdNode *     extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars );
-
-/* build the set of all tuples of K variables out of N from the BDD cube */
-extern DdNode *    Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN );
-extern DdNode *     extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN );
-/* selects one subset from a ZDD representing the set of subsets */
-extern DdNode *    Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS );
-extern DdNode *     extraZddSelectOneSubset( DdManager * dd, DdNode * zS );
-
-/*=== extraBddUnate.c =================================================================*/
-
-extern DdNode *    Extra_bddAndTime( DdManager * dd, DdNode * f, DdNode * g, int TimeOut );
-extern DdNode *    Extra_bddAndAbstractTime( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int TimeOut );
-extern DdNode *    Extra_TransferPermuteTime( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut );
-
-/*=== extraBddUnate.c =================================================================*/
-
-typedef struct Extra_UnateVar_t_  Extra_UnateVar_t;
-struct Extra_UnateVar_t_ {
-    unsigned    iVar : 30;  // index of the variable
-    unsigned    Pos  :  1;  // 1 if positive unate
-    unsigned    Neg  :  1;  // 1 if negative unate
-};
-
-typedef struct Extra_UnateInfo_t_  Extra_UnateInfo_t;
-struct Extra_UnateInfo_t_ {
-    int nVars;      // the number of variables in the support
-    int nVarsMax;   // the number of variables in the DD manager
-    int nUnate;     // the number of unate variables
-    Extra_UnateVar_t * pVars;    // the array of variables present in the support
-};
-
-/* allocates the data structure */
-extern Extra_UnateInfo_t *  Extra_UnateInfoAllocate( int nVars );
-/* deallocates the data structure */
-extern void        Extra_UnateInfoDissolve( Extra_UnateInfo_t * );
-/* print the contents the data structure */
-extern void        Extra_UnateInfoPrint( Extra_UnateInfo_t * );
-/* converts the ZDD into the Extra_SymmInfo_t structure */
-extern Extra_UnateInfo_t *  Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zUnate, DdNode * bVars );
-/* naive check of unateness of one variable */
-extern int         Extra_bddCheckUnateNaive( DdManager * dd, DdNode * bF, int iVar );
-
-/* computes the unateness information for the function */
-extern Extra_UnateInfo_t *  Extra_UnateComputeFast( DdManager * dd, DdNode * bFunc );
-extern Extra_UnateInfo_t *  Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc );
-
-/* computes the classical symmetry information as a ZDD */
-extern DdNode *    Extra_zddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
-extern DdNode *     extraZddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
-
-/* converts a set of variables into a set of singleton subsets */
-extern DdNode *    Extra_zddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
-extern DdNode *     extraZddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
-
 /*=== extraUtilBitMatrix.c ================================================================*/
 
 typedef struct Extra_BitMat_t_ Extra_BitMat_t;
@@ -391,9 +159,7 @@ extern int         Extra_MmStepReadMemUsage( Extra_MmStep_t * p );
 /*=== extraUtilMisc.c ========================================================*/
 
 /* finds the smallest integer larger or equal than the logarithm */
-extern int         Extra_Base2Log( unsigned Num );
 extern int         Extra_Base2LogDouble( double Num );
-extern int         Extra_Base10Log( unsigned Num );
 /* returns the power of two as a double */
 extern double      Extra_Power2( int Num );
 extern int         Extra_Power3( int Num );
@@ -430,8 +196,6 @@ extern unsigned ** Extra_TruthPerm53();
 extern unsigned ** Extra_TruthPerm54();
 /* bubble sort for small number of entries */
 extern void        Extra_BubbleSort( int Order[], int Costs[], int nSize, int fIncreasing );
-/* for independence from CUDD */
-extern unsigned int Cudd_PrimeCopy( unsigned int  p );
 
 /*=== extraUtilCanon.c ========================================================*/
 
@@ -451,10 +215,6 @@ static inline void Extra_ProgressBarUpdate( ProgressBar * p, int nItemsCur, char
 
 /*=== extraUtilTruth.c ================================================================*/
 
-//static inline int   Extra_Float2Int( float Val )     { return *((int *)&Val);               }
-//static inline float Extra_Int2Float( int Num )       { return *((float *)&Num);             }
-static inline int   Extra_Float2Int( float Val )     { union { int x; float y; } v; v.y = Val; return v.x;     }
-static inline float Extra_Int2Float( int Num )       { union { int x; float y; } v; v.x = Num; return v.y;     }
 static inline int   Extra_BitWordNum( int nBits )    { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0);  }
 static inline int   Extra_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
 
diff --git a/src/misc/extra/extraBdd.h b/src/misc/extra/extraBdd.h
new file mode 100644
index 00000000..25df14bb
--- /dev/null
+++ b/src/misc/extra/extraBdd.h
@@ -0,0 +1,316 @@
+/**CFile****************************************************************
+
+  FileName    [extraBdd.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [extra]
+
+  Synopsis    [Various reusable software utilities.]
+
+  Description [This library contains a number of operators and 
+  traversal routines developed to extend the functionality of 
+  CUDD v.2.3.x, by Fabio Somenzi (http://vlsi.colorado.edu/~fabio/)
+  To compile your code with the library, #include "extra.h" 
+  in your source files and link your project to CUDD and this 
+  library. Use the library at your own risk and with caution. 
+  Note that debugging of some operators still continues.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: extraBdd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__misc__extra__extra_bdd_h
+#define ABC__misc__extra__extra_bdd_h
+
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Nested includes                                                           */
+/*---------------------------------------------------------------------------*/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "src/misc/st/st.h"
+#include "src/bdd/cudd/cuddInt.h"
+#include "src/misc/extra/extra.h"
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/* constants of the manager */
+#define     b0     Cudd_Not((dd)->one)
+#define     b1              (dd)->one
+#define     z0              (dd)->zero
+#define     z1              (dd)->one
+#define     a0              (dd)->zero
+#define     a1              (dd)->one
+
+// hash key macros
+#define hashKey1(a,TSIZE) \
+((ABC_PTRUINT_T)(a) % TSIZE)
+
+#define hashKey2(a,b,TSIZE) \
+(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE)
+
+#define hashKey3(a,b,c,TSIZE) \
+(((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)
+
+#define hashKey4(a,b,c,d,TSIZE) \
+((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
+   (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE)
+
+#define hashKey5(a,b,c,d,e,TSIZE) \
+(((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
+   (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE)
+
+/*===========================================================================*/
+/*     Various Utilities                                                     */
+/*===========================================================================*/
+
+/*=== extraBddAuto.c ========================================================*/
+
+extern DdNode *     Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc );
+extern DdNode *     Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
+extern DdNode *      extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
+extern DdNode *     Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
+extern DdNode *      extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
+extern DdNode *     Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
+extern DdNode *      extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
+
+extern DdNode *     Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
+extern DdNode *      extraBddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
+
+extern DdNode *     Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace );
+extern DdNode *     Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
+extern DdNode *      extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
+extern DdNode *     Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
+extern DdNode *      extraBddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
+
+extern DdNode *     Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
+extern DdNode *      extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
+extern DdNode *     Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
+extern DdNode *      extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
+
+extern DdNode *     Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars );
+extern DdNode **    Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations );
+
+/*=== extraBddCas.c =============================================================*/
+
+/* performs the binary encoding of the set of function using the given vars */
+extern DdNode *     Extra_bddEncodingBinary( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars );
+/* solves the column encoding problem using a sophisticated method */
+extern DdNode *     Extra_bddEncodingNonStrict( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple );
+/* collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root */
+extern st_table *   Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel );
+/* collects the nodes under the cut starting from the given set of ADD nodes */
+extern int          Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel );
+/* find the profile of a DD (the number of edges crossing each level) */
+extern int          Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel );
+
+/*=== extraBddImage.c ================================================================*/
+
+typedef struct Extra_ImageTree_t_  Extra_ImageTree_t;
+extern Extra_ImageTree_t * Extra_bddImageStart( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode *    Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare );
+extern void        Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree );
+extern DdNode *    Extra_bddImageRead( Extra_ImageTree_t * pTree );
+
+typedef struct Extra_ImageTree2_t_  Extra_ImageTree2_t;
+extern Extra_ImageTree2_t * Extra_bddImageStart2( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode *    Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare );
+extern void        Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree );
+extern DdNode *    Extra_bddImageRead2( Extra_ImageTree2_t * pTree );
+
+/*=== extraBddMisc.c ========================================================*/
+
+extern DdNode *     Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
+extern DdNode *     Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
+extern DdNode *     Extra_bddRemapUp( DdManager * dd, DdNode * bF );
+extern DdNode *     Extra_bddMove( DdManager * dd, DdNode * bF, int nVars );
+extern DdNode *     extraBddMove( DdManager * dd, DdNode * bF, DdNode * bFlag );
+extern void         Extra_StopManager( DdManager * dd );
+extern void         Extra_bddPrint( DdManager * dd, DdNode * F );
+extern void         Extra_bddPrintSupport( DdManager * dd, DdNode * F );
+extern void         extraDecomposeCover( DdManager* dd, DdNode*  zC, DdNode** zC0, DdNode** zC1, DdNode** zC2 );
+extern int          Extra_bddSuppSize( DdManager * dd, DdNode * bSupp );
+extern int          Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar );
+extern int          Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 );
+extern int          Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax );
+extern int          Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall );
+extern int *        Extra_SupportArray( DdManager * dd, DdNode * F, int * support );
+extern int *        Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support );
+extern DdNode *     Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
+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 );
+extern DdNode *     Extra_bddCreateAnd( DdManager * dd, int nVars );
+extern DdNode *     Extra_bddCreateOr( DdManager * dd, int nVars );
+extern DdNode *     Extra_bddCreateExor( DdManager * dd, int nVars );
+extern DdNode *     Extra_zddPrimes( DdManager * dd, DdNode * F );
+extern void         Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
+extern DdNode *     Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
+extern DdNode *     Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
+extern DdNode *     extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
+extern int          Extra_bddVarIsInCube( DdNode * bCube, int iVar );
+extern DdNode *     Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
+
+#ifndef ABC_PRB
+#define ABC_PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
+#endif
+
+/*=== extraBddKmap.c ================================================================*/
+
+/* displays the Karnaugh Map of a function */
+extern void        Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames );
+/* displays the Karnaugh Map of a relation */
+extern void        Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars );
+
+/*=== extraBddSymm.c =================================================================*/
+
+typedef struct Extra_SymmInfo_t_  Extra_SymmInfo_t;
+struct Extra_SymmInfo_t_ {
+    int nVars;      // the number of variables in the support
+    int nVarsMax;   // the number of variables in the DD manager
+    int nSymms;     // the number of pair-wise symmetries
+    int nNodes;     // the number of nodes in a ZDD (if applicable)
+    int * pVars;    // the list of all variables present in the support
+    char ** pSymms; // the symmetry information
+};
+
+/* computes the classical symmetry information for the function - recursive */
+extern Extra_SymmInfo_t *  Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc );
+/* computes the classical symmetry information for the function - using naive approach */
+extern Extra_SymmInfo_t *  Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc );
+extern int         Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
+
+/* allocates the data structure */
+extern Extra_SymmInfo_t *  Extra_SymmPairsAllocate( int nVars );
+/* deallocates the data structure */
+extern void        Extra_SymmPairsDissolve( Extra_SymmInfo_t * );
+/* print the contents the data structure */
+extern void        Extra_SymmPairsPrint( Extra_SymmInfo_t * );
+/* converts the ZDD into the Extra_SymmInfo_t structure */
+extern Extra_SymmInfo_t *  Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars );
+
+/* computes the classical symmetry information as a ZDD */
+extern DdNode *    Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
+extern DdNode *     extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
+/* returns a singleton-set ZDD containing all variables that are symmetric with the given one */
+extern DdNode *    Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
+extern DdNode *     extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
+/* converts a set of variables into a set of singleton subsets */
+extern DdNode *    Extra_zddGetSingletons( DdManager * dd, DdNode * bVars );
+extern DdNode *     extraZddGetSingletons( DdManager * dd, DdNode * bVars );
+/* filters the set of variables using the support of the function */
+extern DdNode *    Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
+extern DdNode *     extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
+
+/* checks the possibility that the two vars are symmetric */
+extern int         Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
+extern DdNode *     extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars );
+
+/* build the set of all tuples of K variables out of N from the BDD cube */
+extern DdNode *    Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN );
+extern DdNode *     extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN );
+/* selects one subset from a ZDD representing the set of subsets */
+extern DdNode *    Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS );
+extern DdNode *     extraZddSelectOneSubset( DdManager * dd, DdNode * zS );
+
+/*=== extraBddUnate.c =================================================================*/
+
+extern DdNode *    Extra_bddAndTime( DdManager * dd, DdNode * f, DdNode * g, int TimeOut );
+extern DdNode *    Extra_bddAndAbstractTime( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int TimeOut );
+extern DdNode *    Extra_TransferPermuteTime( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut );
+
+/*=== extraBddUnate.c =================================================================*/
+
+typedef struct Extra_UnateVar_t_  Extra_UnateVar_t;
+struct Extra_UnateVar_t_ {
+    unsigned    iVar : 30;  // index of the variable
+    unsigned    Pos  :  1;  // 1 if positive unate
+    unsigned    Neg  :  1;  // 1 if negative unate
+};
+
+typedef struct Extra_UnateInfo_t_  Extra_UnateInfo_t;
+struct Extra_UnateInfo_t_ {
+    int nVars;      // the number of variables in the support
+    int nVarsMax;   // the number of variables in the DD manager
+    int nUnate;     // the number of unate variables
+    Extra_UnateVar_t * pVars;    // the array of variables present in the support
+};
+
+/* allocates the data structure */
+extern Extra_UnateInfo_t *  Extra_UnateInfoAllocate( int nVars );
+/* deallocates the data structure */
+extern void        Extra_UnateInfoDissolve( Extra_UnateInfo_t * );
+/* print the contents the data structure */
+extern void        Extra_UnateInfoPrint( Extra_UnateInfo_t * );
+/* converts the ZDD into the Extra_SymmInfo_t structure */
+extern Extra_UnateInfo_t *  Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zUnate, DdNode * bVars );
+/* naive check of unateness of one variable */
+extern int         Extra_bddCheckUnateNaive( DdManager * dd, DdNode * bF, int iVar );
+
+/* computes the unateness information for the function */
+extern Extra_UnateInfo_t *  Extra_UnateComputeFast( DdManager * dd, DdNode * bFunc );
+extern Extra_UnateInfo_t *  Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc );
+
+/* computes the classical symmetry information as a ZDD */
+extern DdNode *    Extra_zddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
+extern DdNode *     extraZddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
+
+/* converts a set of variables into a set of singleton subsets */
+extern DdNode *    Extra_zddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
+extern DdNode *     extraZddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
+
+/**AutomaticEnd***************************************************************/
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif /* __EXTRA_H__ */
diff --git a/src/misc/extra/extraBddAuto.c b/src/misc/extra/extraBddAuto.c
index 3b0e2aa0..5fb38aec 100644
--- a/src/misc/extra/extraBddAuto.c
+++ b/src/misc/extra/extraBddAuto.c
@@ -16,7 +16,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraBddCas.c b/src/misc/extra/extraBddCas.c
index 14de2d2b..0416a0d2 100644
--- a/src/misc/extra/extraBddCas.c
+++ b/src/misc/extra/extraBddCas.c
@@ -16,7 +16,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -146,7 +146,7 @@ Extra_bddEncodingBinary(
     DdNode * bResult;
     DdNode * bCube, * bTemp, * bProd;
 
-    assert( nVars >= Extra_Base2Log(nFuncs) );
+    assert( nVars >= Abc_Base2Log(nFuncs) );
 
     bResult = b0;   Cudd_Ref( bResult );
     for ( i = 0; i < nFuncs; i++ )
diff --git a/src/misc/extra/extraBddImage.c b/src/misc/extra/extraBddImage.c
index 38c18f63..46afb4f2 100644
--- a/src/misc/extra/extraBddImage.c
+++ b/src/misc/extra/extraBddImage.c
@@ -16,7 +16,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraBddKmap.c b/src/misc/extra/extraBddKmap.c
index aa8e3764..23bf2224 100644
--- a/src/misc/extra/extraBddKmap.c
+++ b/src/misc/extra/extraBddKmap.c
@@ -20,7 +20,7 @@
 ///       Version 1.0. Started - August 20, 2000        ///
 ///     Version 2.0. Added to EXTRA - July 17, 2001     ///
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 3af9c81e..4512572d 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1917,7 +1917,7 @@ DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF,
     // find the topmost variable in F and G using var order of F
     LevF = cuddI( ddF, Cudd_Regular(bF)->index );
     LevG = cuddI( ddF, pPermute ? pPermute[Cudd_Regular(bG)->index] : Cudd_Regular(bG)->index );
-    Lev  = ABC_MIN( LevF, LevG );
+    Lev  = Abc_MinInt( LevF, LevG );
     assert( Lev < ddF->size );
     bVar = ddF->vars[ddF->invperm[Lev]];
 
diff --git a/src/misc/extra/extraBddSymm.c b/src/misc/extra/extraBddSymm.c
index 0adcbd2a..9dd2c8e5 100644
--- a/src/misc/extra/extraBddSymm.c
+++ b/src/misc/extra/extraBddSymm.c
@@ -19,7 +19,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraBddTime.c b/src/misc/extra/extraBddTime.c
index b861d51a..853f8a64 100644
--- a/src/misc/extra/extraBddTime.c
+++ b/src/misc/extra/extraBddTime.c
@@ -16,7 +16,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraBddUnate.c b/src/misc/extra/extraBddUnate.c
index 3aa18e51..9ebdd4e5 100644
--- a/src/misc/extra/extraBddUnate.c
+++ b/src/misc/extra/extraBddUnate.c
@@ -20,7 +20,7 @@
 
 ***********************************************************************/
 
-#include "extra.h"
+#include "extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index a8542da4..b38befd6 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -580,7 +580,7 @@ void Extra_FileSort( char * pFileName, char * pFileNameOut )
             Begin = i + 1;
         }
     // sort the lines
-    qsort( pLines, nLines, sizeof(char *), Extra_StringCompare );
+    qsort( pLines, nLines, sizeof(char *), (int(*)(const void *,const void *))Extra_StringCompare );
     // write a new file
     pFile = fopen( pFileNameOut, "wb" );
     for ( i = 0; i < nLines; i++ )
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index e4c5acd5..b910f209 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -18,6 +18,8 @@
 
 ***********************************************************************/
 
+#include <math.h>
+
 #include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -58,27 +60,6 @@ static void Extra_Permutations_rec( char ** pRes, int nFact, int n, char Array[]
 /* Definition of exported functions                                          */
 /*---------------------------------------------------------------------------*/
 
-
-/**Function********************************************************************
-
-  Synopsis    [Finds the smallest integer larger of equal than the logarithm.]
-
-  Description [Returns [Log2(Num)].]
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-int Extra_Base2Log( unsigned Num )
-{
-    int Res;
-    if ( Num == 0 ) return 0;
-    if ( Num == 1 ) return 1;
-    for ( Res = 0, Num--; Num; Num >>= 1, Res++ );
-    return Res;
-} /* end of Extra_Base2Log */
-
 /**Function********************************************************************
 
   Synopsis    [Finds the smallest integer larger of equal than the logarithm.]
@@ -105,26 +86,6 @@ int Extra_Base2LogDouble( double Num )
 
 /**Function********************************************************************
 
-  Synopsis    [Finds the smallest integer larger of equal than the logarithm.]
-
-  Description [Returns [Log10(Num)].]
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-int Extra_Base10Log( unsigned Num )
-{
-    int Res;
-    if ( Num == 0 ) return 0;
-    if ( Num == 1 ) return 1;
-    for ( Res = 0, Num--;  Num;  Num /= 10,  Res++ );
-    return Res;
-} /* end of Extra_Base2Log */
-
-/**Function********************************************************************
-
   Synopsis    [Returns the power of two as a double.]
 
   Description []
@@ -2118,41 +2079,6 @@ void Extra_BubbleSort( int Order[], int Costs[], int nSize, int fIncreasing )
     }
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Returns the smallest prime larger than the number.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned int Cudd_PrimeCopy( unsigned int  p)
-{
-    int i,pn;
-
-    p--;
-    do {
-        p++;
-        if (p&1) {
-        pn = 1;
-        i = 3;
-        while ((unsigned) (i * i) <= p) {
-        if (p % i == 0) {
-            pn = 0;
-            break;
-        }
-        i += 2;
-        }
-    } else {
-        pn = 0;
-    }
-    } while (!pn);
-    return(p);
-
-} /* end of Cudd_Prime */
 
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
diff --git a/src/misc/extra/extraUtilProgress.c b/src/misc/extra/extraUtilProgress.c
index e7add47f..ab0f5849 100644
--- a/src/misc/extra/extraUtilProgress.c
+++ b/src/misc/extra/extraUtilProgress.c
@@ -20,7 +20,7 @@
 
 #include <stdio.h>
 #include "extra.h"
-#include "main.h"
+#include "src/base/main/main.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraUtilReader.c b/src/misc/extra/extraUtilReader.c
index bcf3da37..41e02a27 100644
--- a/src/misc/extra/extraUtilReader.c
+++ b/src/misc/extra/extraUtilReader.c
@@ -20,7 +20,7 @@
 
 #include <stdio.h>
 #include "extra.h"
-#include "vec.h"
+#include "src/misc/vec/vec.h"
 
 ABC_NAMESPACE_IMPL_START