Made gate library package Mio independent of CUDD.

22 files changed, 1552 insertions, 154 deletions

diff --git a/.hgignore b/.hgignore
index ae20be3d..2c467f92 100644
--- a/.hgignore
+++ b/.hgignore
@@ -14,6 +14,7 @@ docs/
 
 src/ext/
 src/xxx/
+src/aig/au/
 
 *~
 *.orig
diff --git a/abc.rc b/abc.rc
index de9a743a..895d92a6 100644
--- a/abc.rc
+++ b/abc.rc
@@ -74,6 +74,7 @@ alias rvl read_verlib
 alias rsup read_super mcnc5_old.super
 alias rlib read_library
 alias rlibc read_library cadence.genlib
+alias rty read_liberty
 alias rlut read_lut
 alias rw rewrite
 alias rwz rewrite -z
diff --git a/abclib.dsp b/abclib.dsp
index f4d8fb96..326bb6c1 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1943,6 +1943,10 @@ SOURCE=.\src\map\mapper\mapperVec.c
 # PROP Default_Filter ""
 # Begin Source File
 
+SOURCE=.\src\map\mio\exp.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\map\mio\mio.c
 # End Source File
 # Begin Source File
@@ -1963,10 +1967,18 @@ SOURCE=.\src\map\mio\mioInt.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\map\mio\mioParse.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\map\mio\mioRead.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\map\mio\mioSop.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\map\mio\mioUtils.c
 # End Source File
 # End Group
@@ -4199,35 +4211,35 @@ SOURCE=.\src\aig\au\auDiv.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auDsd.c
+SOURCE=.\src\aig\au\auDsdData.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auFanout.c
+SOURCE=.\src\aig\au\auDsdForm.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auFour.c
+SOURCE=.\src\aig\au\auDsdTab.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auHash.c
+SOURCE=.\src\aig\au\auFanout.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auInt.h
+SOURCE=.\src\aig\au\auFour.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auMffc.c
+SOURCE=.\src\aig\au\auHash.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auNpn6.c
+SOURCE=.\src\aig\au\auInt.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\au\auNpnTab.c
+SOURCE=.\src\aig\au\auMffc.c
 # End Source File
 # Begin Source File
 
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 1c5b05fe..745b19ba 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -503,7 +503,8 @@ static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gi
     Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
     Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
     assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
-    s_Counter++;
+//    s_Counter++;
+//    s_Counter = Abc_MaxInt( s_Counter, Vec_IntSize(p->vLevReas)/3 );
 }
 
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c0c0d71e..415e2797 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8687,8 +8687,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Aig_ManStop( pAig );
     }
 */
-/*
 
+/*
     if ( Abc_NtkIsStrash(pNtk) )
     {
         extern Abc_Ntk_t * Au_ManTransformTest( Abc_Ntk_t * pAig );
@@ -8708,6 +8708,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 */
 
+/*
+{
+    extern int Au_DsdVecTest( int nVars );
+    Au_DsdVecTest( 6 );
+}
+*/
 
 {
 //    extern void Au_Sat3DeriveImpls();
diff --git a/src/map/amap/amapLib.c b/src/map/amap/amapLib.c
index 474b444d..74017dde 100644
--- a/src/map/amap/amapLib.c
+++ b/src/map/amap/amapLib.c
@@ -306,10 +306,11 @@ void Amap_LibPrintSelectedGates( Amap_Lib_t * p, int fAllGates )
     vArray = fAllGates? p->vGates : p->vSelect;
     Vec_PtrForEachEntry( Amap_Gat_t *, vArray, pGate, i )
     {
-        printf( "Gate %4d : %15s   Area = %9.2f\n", pGate->Id, pGate->pName, pGate->dArea );
-        printf( "    Formula: %s=%s\n", pGate->pOutName, pGate->pForm );
-        printf( "    DSD:     " );
+        printf( "%3d :%12s %d %9.2f  ", i, pGate->pName, pGate->nPins, pGate->dArea );
+        printf( "%4s=%40s  ", pGate->pOutName, pGate->pForm );
+        printf( "DSD: " );
         Kit_DsdPrintFromTruth( pGate->pFunc, pGate->nPins );
+        printf( "\n" );
     }
 }
 
@@ -345,6 +346,7 @@ Amap_Lib_t * Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryVe
         printf( "Selected %d functionally unique gates. ",
             Vec_PtrSize(p->vSelect), Vec_PtrSize(p->vSorted) );
         ABC_PRT( "Time", clock() - clk );
+//       Amap_LibPrintSelectedGates( p, 0 );
     }
     clk = clock();
     Amap_LibCreateRules( p, fVeryVerbose );
diff --git a/src/map/mapper/mapperSuper.c b/src/map/mapper/mapperSuper.c
index 58deddb7..7ade52fe 100644
--- a/src/map/mapper/mapperSuper.c
+++ b/src/map/mapper/mapperSuper.c
@@ -114,7 +114,7 @@ int Map_LibraryReadFile( Map_SuperLib_t * pLib, FILE * pFile )
     fclose( pFileGen );
 
     // read the genlib library
-    pLib->pGenlib = Mio_LibraryRead( Abc_FrameGetGlobalFrame(), pLibName, 0, 0 );
+    pLib->pGenlib = Mio_LibraryRead( pLibName, 0, 0 );
     if ( pLib->pGenlib == NULL )
     {
         printf( "Cannot read GENLIB file \"%s\".\n", pLibName );
diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c
index f6a0d2d3..bfca980b 100644
--- a/src/map/mapper/mapperTree.c
+++ b/src/map/mapper/mapperTree.c
@@ -76,7 +76,7 @@ int Map_LibraryReadTree( Map_SuperLib_t * pLib, char * pFileName, char * pExclud
         pAbc = Abc_FrameGetGlobalFrame();
         
         tExcludeGate = st_init_table(strcmp, st_strhash);
-        if ( (num = Mio_LibraryReadExclude( pAbc, pExcludeFile, tExcludeGate )) == -1 )
+        if ( (num = Mio_LibraryReadExclude( pExcludeFile, tExcludeGate )) == -1 )
         {
             st_free_table( tExcludeGate );
             tExcludeGate = 0;
@@ -169,7 +169,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
     fclose( pFileGen );
 
     // read the genlib library
-    pLib->pGenlib = Mio_LibraryRead( Abc_FrameGetGlobalFrame(), pLibFile, 0, 0 );
+    pLib->pGenlib = Mio_LibraryRead( pLibFile, 0, 0 );
     if ( pLib->pGenlib == NULL )
     {
         printf( "Cannot read GENLIB file \"%s\".\n", pLibFile );
diff --git a/src/map/mapper/mapperTree_old.c b/src/map/mapper/mapperTree_old.c
index d0acff12..1a76b267 100644
--- a/src/map/mapper/mapperTree_old.c
+++ b/src/map/mapper/mapperTree_old.c
@@ -167,7 +167,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
     fclose( pFileGen );
 
     // read the genlib library
-    pLib->pGenlib = Mio_LibraryRead( Abc_FrameGetGlobalFrame(), pLibFile, 0, 0 );
+    pLib->pGenlib = Mio_LibraryRead( pLibFile, 0, 0 );
     if ( pLib->pGenlib == NULL )
     {
         printf( "Cannot read GENLIB file \"%s\".\n", pLibFile );
diff --git a/src/map/mio/exp.h b/src/map/mio/exp.h
new file mode 100644
index 00000000..fa643325
--- /dev/null
+++ b/src/map/mio/exp.h
@@ -0,0 +1,218 @@
+/**CFile****************************************************************
+
+  FileName    [exp.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Boolean expression.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: exp.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __EXP_H__
+#define __EXP_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define EXP_CONST0 -1
+#define EXP_CONST1 -2
+
+static inline Vec_Int_t * Exp_Const0()
+{
+    Vec_Int_t * vExp;
+    vExp = Vec_IntAlloc( 1 );
+    Vec_IntPush( vExp, EXP_CONST0 );
+    return vExp;
+}
+static inline Vec_Int_t * Exp_Const1()
+{
+    Vec_Int_t * vExp;
+    vExp = Vec_IntAlloc( 1 );
+    Vec_IntPush( vExp, EXP_CONST1 );
+    return vExp;
+}
+static inline int Exp_IsConst( Vec_Int_t * p )
+{
+    return Vec_IntEntry(p,0) == EXP_CONST0 || Vec_IntEntry(p,0) == EXP_CONST1;
+}
+static inline int Exp_IsConst0( Vec_Int_t * p )
+{
+    return Vec_IntEntry(p,0) == EXP_CONST0;
+}
+static inline int Exp_IsConst1( Vec_Int_t * p )
+{
+    return Vec_IntEntry(p,0) == EXP_CONST1;
+}
+static inline Vec_Int_t * Exp_Var( int iVar )
+{
+    Vec_Int_t * vExp;
+    vExp = Vec_IntAlloc( 1 );
+    Vec_IntPush( vExp, 2 * iVar );
+    return vExp;
+}
+static inline int Exp_LitShift( int nVars, int Lit, int Shift )
+{
+    if ( Lit < 2 * nVars )
+        return Lit;
+    return Lit + 2 * Shift;
+}
+static inline int Exp_IsLit( Vec_Int_t * p )
+{
+    return Vec_IntSize(p) == 1 && !Exp_IsConst(p);
+}
+static inline int Exp_NodeNum( Vec_Int_t * p )
+{
+    return Vec_IntSize(p)/2;
+}
+static inline Vec_Int_t * Exp_Not( Vec_Int_t * p )
+{
+    Vec_IntWriteEntry( p, 0, Vec_IntEntry(p,0) ^ 1 );
+    return p;
+}
+static inline void Exp_PrintLit( int nVars, int Lit )
+{
+    if ( Lit == EXP_CONST0 )
+        Abc_Print( 1, "Const0" );
+    else if ( Lit == EXP_CONST1 )
+        Abc_Print( 1, "Const1" );
+    else if ( Lit < 2 * nVars )
+        Abc_Print( 1, "%s%c", (Lit&1) ? "!" : " ", 'a' + Lit/2 );
+    else
+        Abc_Print( 1, "%s%d", (Lit&1) ? "!" : " ", Lit/2 );
+}
+static inline void Exp_Print( int nVars, Vec_Int_t * p )
+{
+    int i;
+    for ( i = 0; i < Exp_NodeNum(p); i++ )
+    {
+        Abc_Print( 1, "%2d = ", nVars + i );
+        Exp_PrintLit( nVars, Vec_IntEntry(p, 2*i+0) );
+        Abc_Print( 1, " & " );
+        Exp_PrintLit( nVars, Vec_IntEntry(p, 2*i+1) );
+        Abc_Print( 1, "\n" );
+    }
+    Abc_Print( 1, " F = " );
+    Exp_PrintLit( nVars, Vec_IntEntryLast(p) );
+    Abc_Print( 1, "\n" );
+}
+static inline Vec_Int_t * Exp_Reverse( Vec_Int_t * p )
+{
+    Vec_IntReverseOrder( p );
+    return p;
+}
+static inline void Exp_PrintReverse( int nVars, Vec_Int_t * p )
+{
+    Exp_Reverse( p );
+    Exp_Print( nVars, p );
+    Exp_Reverse( p );
+}
+static inline Vec_Int_t * Exp_And( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1, int fCompl0, int fCompl1 )
+{
+    int i, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
+    Vec_Int_t * r = Vec_IntAlloc( Len0 + Len1 + 1 );
+    assert( (Len0 & 1) && (Len1 & 1) );
+    Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2) );
+    Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0) ^ fCompl0, Len1/2 ) );
+    Vec_IntPush( r, Vec_IntEntry(p1, 0) ^ fCompl1 );
+    for ( i = 1; i < Len0; i++ )
+        Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, i), Len1/2 ) );
+    for ( i = 1; i < Len1; i++ )
+        Vec_IntPush( r, Vec_IntEntry(p1, i) );
+    assert( Vec_IntSize(r) == Len0 + Len1 + 1 );
+    return r;
+}
+static inline Vec_Int_t * Exp_Or( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1 )
+{
+    return Exp_Not( Exp_And(pMan, nVars, p0, p1, 1, 1) );
+}
+static inline Vec_Int_t * Exp_Xor( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1 )
+{
+    int i, v = 0, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
+    Vec_Int_t * r = Vec_IntAlloc( Len0 + Len1 + 5 );
+    assert( (Len0 & 1) && (Len1 & 1) );
+    Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 2)     );
+    Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 1) + 1 );
+    Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 0) + 1 );
+    Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0) ^ 1, Len1/2 ) );
+    Vec_IntPush( r, Vec_IntEntry(p1, 0) );
+    Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0), Len1/2 ) );
+    Vec_IntPush( r, Vec_IntEntry(p1, 0) ^ 1 );
+    for ( i = 1; i < Len0; i++ )
+        Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, i), Len1/2 ) );
+    for ( i = 1; i < Len1; i++ )
+        Vec_IntPush( r, Vec_IntEntry(p1, i) );
+    assert( Vec_IntSize(r) == Len0 + Len1 + 5 );
+    return Exp_Not( r );
+}
+static inline word Exp_Truth6Lit( int nVars, int Lit, word * puFanins, word * puNodes )
+{
+    if ( Lit == EXP_CONST0 )
+        return 0;
+    if ( Lit == EXP_CONST1 )
+        return ~0;
+    if ( Lit < 2 * nVars )
+        return (Lit&1) ? ~puFanins[Lit/2] : puFanins[Lit/2];
+    return (Lit&1) ? ~puNodes[Lit/2-nVars] : puNodes[Lit/2-nVars];
+}
+static inline word Exp_Truth6( int nVars, Vec_Int_t * p, word * puFanins )
+{
+    static word Truth6[6] = {
+        0xAAAAAAAAAAAAAAAA,
+        0xCCCCCCCCCCCCCCCC,
+        0xF0F0F0F0F0F0F0F0,
+        0xFF00FF00FF00FF00,
+        0xFFFF0000FFFF0000,
+        0xFFFFFFFF00000000
+    };
+    word * puNodes, Res;
+    int i;
+    if ( puFanins == NULL )
+        puFanins = (word *)Truth6;
+    puNodes = ABC_CALLOC( word, Exp_NodeNum(p) );
+    for ( i = 0; i < Exp_NodeNum(p); i++ )
+        puNodes[i] = Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+0), puFanins, puNodes ) & 
+                  Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+1), puFanins, puNodes );
+    Res = Exp_Truth6Lit( nVars, Vec_IntEntryLast(p), puFanins, puNodes );
+    ABC_FREE( puNodes );
+    return Res;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_END
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c
index 2121b7b9..a034e549 100644
--- a/src/map/mio/mio.c
+++ b/src/map/mio/mio.c
@@ -22,10 +22,8 @@
 #include <unistd.h>
 #endif
 
-#include "abc.h"
-#include "mvc.h"
-#include "mainInt.h"
-#include "mioInt.h"
+#include "main.h"
+#include "mio.h"
 #include "mapper.h"
 #include "amap.h"
 
@@ -276,7 +274,7 @@ int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
     fclose( pFile );
 
     // set the new network
-    pLib = Mio_LibraryRead( pAbc, FileName, 0, fVerbose );  
+    pLib = Mio_LibraryRead( FileName, 0, fVerbose );  
     if ( pLib == NULL )
     {
         fprintf( pErr, "Reading GENLIB library has failed.\n" );
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index 0e993520..de35b637 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -43,6 +43,8 @@ typedef struct  Mio_LibraryStruct_t_      Mio_Library_t;
 typedef struct  Mio_GateStruct_t_         Mio_Gate_t;
 typedef struct  Mio_PinStruct_t_          Mio_Pin_t;
 
+static inline char *    Mio_UtilStrsav( char * s )     { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL;   }
+
 ////////////////////////////////////////////////////////////////////////
 ///                       GLOBAL VARIABLES                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -82,7 +84,7 @@ extern char *            Mio_LibraryReadName       ( Mio_Library_t * pLib );
 extern int               Mio_LibraryReadGateNum    ( Mio_Library_t * pLib );
 extern Mio_Gate_t *      Mio_LibraryReadGates      ( Mio_Library_t * pLib );
 extern Mio_Gate_t **     Mio_LibraryReadGatesByName( Mio_Library_t * pLib );
-extern DdManager *       Mio_LibraryReadDd         ( Mio_Library_t * pLib );
+//extern DdManager *       Mio_LibraryReadDd         ( Mio_Library_t * pLib );
 extern Mio_Gate_t *      Mio_LibraryReadGateByName ( Mio_Library_t * pLib, char * pName );
 extern char *            Mio_LibraryReadSopByName  ( Mio_Library_t * pLib, char * pName );    
 extern Mio_Gate_t *      Mio_LibraryReadConst0     ( Mio_Library_t * pLib );
@@ -112,7 +114,8 @@ extern Mio_Gate_t *      Mio_GateReadNext          ( Mio_Gate_t * pGate );
 extern int               Mio_GateReadInputs        ( Mio_Gate_t * pGate );      
 extern double            Mio_GateReadDelayMax      ( Mio_Gate_t * pGate );      
 extern char *            Mio_GateReadSop           ( Mio_Gate_t * pGate );      
-extern DdNode *          Mio_GateReadFunc          ( Mio_Gate_t * pGate );
+//extern DdNode *          Mio_GateReadFunc          ( Mio_Gate_t * pGate );
+extern word              Mio_GateReadTruth         ( Mio_Gate_t * pGate );
 extern int               Mio_GateReadValue         ( Mio_Gate_t * pGate );
 extern void              Mio_GateSetValue          ( Mio_Gate_t * pGate, int Value );
 extern char *            Mio_PinReadName           ( Mio_Pin_t * pPin );  
@@ -126,10 +129,14 @@ extern double            Mio_PinReadDelayFanoutFall( Mio_Pin_t * pPin );
 extern double            Mio_PinReadDelayBlockMax  ( Mio_Pin_t * pPin );  
 extern Mio_Pin_t *       Mio_PinReadNext           ( Mio_Pin_t * pPin );  
 /*=== mioRead.c =============================================================*/
-extern Mio_Library_t *   Mio_LibraryRead( void * pAbc, char * FileName, char * ExcludeFile, int fVerbose );
-extern int               Mio_LibraryReadExclude( void * pAbc, char * ExcludeFile, st_table * tExcludeGate );
+extern Mio_Library_t *   Mio_LibraryRead( char * FileName, char * ExcludeFile, int fVerbose );
+extern int               Mio_LibraryReadExclude( char * ExcludeFile, st_table * tExcludeGate );
 /*=== mioFunc.c =============================================================*/
 extern int               Mio_LibraryParseFormulas( Mio_Library_t * pLib );
+/*=== mioParse.c =============================================================*/
+extern Vec_Int_t *       Mio_ParseFormula( char * pFormInit, char ** ppVarNames, int nVars );
+/*=== mioSop.c =============================================================*/
+extern char *            Mio_LibDeriveSop( int nVars, Vec_Int_t * vExpr, Vec_Str_t * vStr );
 /*=== mioUtils.c =============================================================*/
 extern void              Mio_LibraryDelete( Mio_Library_t * pLib );
 extern void              Mio_GateDelete( Mio_Gate_t * pGate );
@@ -137,6 +144,7 @@ extern void              Mio_PinDelete( Mio_Pin_t * pPin );
 extern Mio_Pin_t *       Mio_PinDup( Mio_Pin_t * pPin );
 extern void              Mio_WriteLibrary( FILE * pFile, Mio_Library_t * pLib, int fPrintSops );
 extern Mio_Gate_t **     Mio_CollectRoots( Mio_Library_t * pLib, int nInputs, float tDelay, int fSkipInv, int * pnGates );
+extern word              Mio_DeriveTruthTable6( Mio_Gate_t * pGate );
 extern void              Mio_DeriveTruthTable( Mio_Gate_t * pGate, unsigned uTruthsIn[][2], int nSigns, int nInputs, unsigned uTruthRes[] );
 extern void              Mio_DeriveGateDelays( Mio_Gate_t * pGate, 
                             float ** ptPinDelays, int nPins, int nInputs, float tDelayZero, 
diff --git a/src/map/mio/mioApi.c b/src/map/mio/mioApi.c
index 9b267c30..927a01ea 100644
--- a/src/map/mio/mioApi.c
+++ b/src/map/mio/mioApi.c
@@ -44,7 +44,7 @@ char *            Mio_LibraryReadName          ( Mio_Library_t * pLib )  { retur
 int               Mio_LibraryReadGateNum       ( Mio_Library_t * pLib )  { return pLib->nGates;   }
 Mio_Gate_t *      Mio_LibraryReadGates         ( Mio_Library_t * pLib )  { return pLib->pGates;   }
 Mio_Gate_t **     Mio_LibraryReadGatesByName   ( Mio_Library_t * pLib )  { return pLib->ppGatesName;}
-DdManager *       Mio_LibraryReadDd            ( Mio_Library_t * pLib )  { return pLib->dd;       }
+//DdManager *       Mio_LibraryReadDd            ( Mio_Library_t * pLib )  { return pLib->dd;       }
 Mio_Gate_t *      Mio_LibraryReadBuf           ( Mio_Library_t * pLib )  { return pLib->pGateBuf; }
 Mio_Gate_t *      Mio_LibraryReadInv           ( Mio_Library_t * pLib )  { return pLib->pGateInv; }
 Mio_Gate_t *      Mio_LibraryReadConst0        ( Mio_Library_t * pLib )  { return pLib->pGate0;     }
@@ -145,7 +145,9 @@ Mio_Gate_t *      Mio_GateReadNext    ( Mio_Gate_t * pGate )            { return
 int               Mio_GateReadInputs  ( Mio_Gate_t * pGate )            { return pGate->nInputs;   }
 double            Mio_GateReadDelayMax( Mio_Gate_t * pGate )            { return pGate->dDelayMax; }
 char *            Mio_GateReadSop     ( Mio_Gate_t * pGate )            { return pGate->pSop;      }
-DdNode *          Mio_GateReadFunc    ( Mio_Gate_t * pGate )            { return pGate->bFunc;     }
+//DdNode *          Mio_GateReadFunc    ( Mio_Gate_t * pGate )            { return pGate->bFunc;     }
+word              Mio_GateReadTruth   ( Mio_Gate_t * pGate )            { return pGate->nInputs <= 6 ? pGate->uTruth : 0;   }
+word *            Mio_GateReadTruthP  ( Mio_Gate_t * pGate )            { return pGate->nInputs <= 6 ? NULL: pGate->pTruth; }
 int               Mio_GateReadValue   ( Mio_Gate_t * pGate )            { return pGate->Value;     }
 void              Mio_GateSetValue    ( Mio_Gate_t * pGate, int Value ) { pGate->Value = Value;    }
 
diff --git a/src/map/mio/mioForm.c b/src/map/mio/mioForm.c
new file mode 100644
index 00000000..5c7a48e6
--- /dev/null
+++ b/src/map/mio/mioForm.c
@@ -0,0 +1,307 @@
+/**CFile****************************************************************
+
+  FileName    [mioForm.c]
+
+  PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
+
+  Synopsis    [Parsing equestion formula.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 8, 2003.]
+
+  Revision    [$Id: mioForm.c,v 1.4 2004/06/28 14:20:25 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mioInt.h"
+#include "parse.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// these symbols (and no other) can appear in the formulas
+#define MIO_SYMB_AND    '*'
+#define MIO_SYMB_AND2   '&'
+#define MIO_SYMB_OR     '+'
+#define MIO_SYMB_OR2    '|'
+#define MIO_SYMB_XOR    '^'
+#define MIO_SYMB_NOT    '!'
+#define MIO_SYMB_AFTNOT '\''
+#define MIO_SYMB_OPEN   '('
+#define MIO_SYMB_CLOSE  ')'
+
+static int Mio_GateParseFormula( Mio_Gate_t * pGate );
+static int Mio_GateCollectNames( char * pFormula, char * pPinNames[] );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Deriving the functionality of the gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mio_LibraryParseFormulas( Mio_Library_t * pLib )
+{
+    Mio_Gate_t * pGate;
+
+    // count the gates
+    pLib->nGates = 0;
+    Mio_LibraryForEachGate( pLib, pGate )
+        pLib->nGates++;        
+
+    // start a temporary BDD manager
+    pLib->dd = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    // introduce ZDD variables
+    Cudd_zddVarsFromBddVars( pLib->dd, 2 );
+
+    // for each gate, derive its function
+    Mio_LibraryForEachGate( pLib, pGate )
+        if ( Mio_GateParseFormula( pGate ) )
+            return 1;
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Registers the cube string with the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Mio_SopRegister( Mem_Flex_t * pMan, char * pName )
+{
+    char * pRegName;
+    if ( pName == NULL ) return NULL;
+    pRegName = Mem_FlexEntryFetch( pMan, strlen(pName) + 1 );
+    strcpy( pRegName, pName );
+    return pRegName;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deriving the functionality of the gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mio_GateParseFormula( Mio_Gate_t * pGate )
+{
+    extern char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
+    DdManager * dd = pGate->pLib->dd;
+    char * pPinNames[100];
+    char * pPinNamesCopy[100];
+    Mio_Pin_t * pPin, ** ppPin;
+    int nPins, iPin, i;
+
+    // set the maximum delay of the gate; count pins
+    pGate->dDelayMax = 0.0;
+    nPins = 0;
+    Mio_GateForEachPin( pGate, pPin )
+    {
+        // set the maximum delay of the gate
+        if ( pGate->dDelayMax < pPin->dDelayBlockMax )
+            pGate->dDelayMax = pPin->dDelayBlockMax;
+        // count the pin
+        nPins++;
+    }
+
+    // check for the gate with const function
+    if ( nPins == 0 )
+    {
+        if ( strcmp( pGate->pForm, MIO_STRING_CONST0 ) == 0 )
+        {
+            pGate->bFunc = b0;
+            pGate->pSop = Mio_SopRegister( (Mem_Flex_t *)pGate->pLib->pMmFlex, " 0\n" );
+            pGate->pLib->pGate0 = pGate;
+        }
+        else if ( strcmp( pGate->pForm, MIO_STRING_CONST1 ) == 0 )
+        {
+            pGate->bFunc = b1;
+            pGate->pSop = Mio_SopRegister( (Mem_Flex_t *)pGate->pLib->pMmFlex, " 1\n" );
+            pGate->pLib->pGate1 = pGate;
+        }
+        else
+        {
+            printf( "Cannot parse formula \"%s\" of gate \"%s\".\n", pGate->pForm, pGate->pName );
+            return 1;
+        }
+        Cudd_Ref( pGate->bFunc );
+        return 0;
+    }
+
+    // collect the names as they appear in the formula
+    nPins = Mio_GateCollectNames( pGate->pForm, pPinNames );
+    if ( nPins == 0 )
+    {
+        printf( "Cannot read formula \"%s\" of gate \"%s\".\n", pGate->pForm, pGate->pName );
+        return 1;
+    }
+
+    // set the number of inputs
+    pGate->nInputs = nPins;
+
+    // consider the case when all the pins have identical pin info
+    if ( strcmp( pGate->pPins->pName, "*" ) == 0 )
+    {
+        // get the topmost (generic) pin
+        pPin = pGate->pPins;
+        ABC_FREE( pPin->pName );
+
+        // create individual pins from the generic pin
+        ppPin = &pPin->pNext;
+        for ( i = 1; i < nPins; i++ )
+        {
+            // get the new pin
+            *ppPin = Mio_PinDup( pPin );
+            // set its name
+            (*ppPin)->pName = pPinNames[i];
+            // prepare the next place in the list
+            ppPin = &((*ppPin)->pNext);
+        }
+        *ppPin = NULL;
+
+        // set the name of the topmost pin
+        pPin->pName = pPinNames[0];
+    }
+    else
+    {
+        // reorder the variable names to appear the save way as the pins
+        iPin = 0;
+        Mio_GateForEachPin( pGate, pPin )
+        {
+            // find the pin with the name pPin->pName
+            for ( i = 0; i < nPins; i++ )
+            {
+                if ( pPinNames[i] && strcmp( pPinNames[i], pPin->pName ) == 0 )
+                {
+                    // free pPinNames[i] because it is already available as pPin->pName
+                    // setting pPinNames[i] to NULL is useful to make sure that
+                    // this name is not assigned to two pins in the list
+                    ABC_FREE( pPinNames[i] );
+                    pPinNamesCopy[iPin++] = pPin->pName;
+                    break;
+                }
+                if ( i == nPins )
+                {
+                    printf( "Cannot find pin name \"%s\" in the formula \"%s\" of gate \"%s\".\n", 
+                        pPin->pName, pGate->pForm, pGate->pName );
+                    return 1;
+                }
+            }
+        }
+
+        // check for the remaining names
+        for ( i = 0; i < nPins; i++ )
+            if ( pPinNames[i] )
+            {
+                printf( "Name \"%s\" appears in the formula \"%s\" of gate \"%s\" but there is no such pin.\n", 
+                    pPinNames[i], pGate->pForm, pGate->pName );
+                return 1;
+            }
+
+        // copy the names back
+        memcpy( pPinNames, pPinNamesCopy, nPins * sizeof(char *) );
+    }
+
+    // expand the manager if necessary
+    if ( dd->size < nPins )
+    {
+        Cudd_Quit( dd );
+        dd = Cudd_Init( nPins + 10, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+        Cudd_zddVarsFromBddVars( dd, 2 );
+    }
+
+    // derive the formula as the BDD
+    pGate->bFunc = Parse_FormulaParser( stdout, pGate->pForm, nPins, 0, pPinNames, dd, dd->vars );
+    if ( pGate->bFunc == NULL )
+        return 1;
+    Cudd_Ref( pGate->bFunc );
+
+    // derive the cover (SOP)
+    pGate->pSop = Abc_ConvertBddToSop( pGate->pLib->pMmFlex, dd, pGate->bFunc, pGate->bFunc, nPins, 0, pGate->pLib->vCube, -1 );
+
+    // derive the truth table
+    if ( pGate->nInputs <= 6 )
+        pGate->uTruth = Mio_DeriveTruthTable6( pGate );
+
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect the pin names in the formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mio_GateCollectNames( char * pFormula, char * pPinNames[] )
+{
+    char Buffer[1000];
+    char * pTemp;
+    int nPins, i;
+
+    // save the formula as it was
+    strcpy( Buffer, pFormula );
+
+    // remove the non-name symbols
+    for ( pTemp = Buffer; *pTemp; pTemp++ )
+        if ( *pTemp == MIO_SYMB_AND  || *pTemp == MIO_SYMB_AND2   || 
+             *pTemp == MIO_SYMB_OR   || *pTemp == MIO_SYMB_OR2    || 
+             *pTemp == MIO_SYMB_XOR  || 
+             *pTemp == MIO_SYMB_NOT  || *pTemp == MIO_SYMB_AFTNOT ||
+             *pTemp == MIO_SYMB_OPEN || *pTemp == MIO_SYMB_CLOSE )
+             *pTemp = ' ';
+
+    // save the names
+    nPins = 0;
+    pTemp = strtok( Buffer, " " );
+    while ( pTemp )
+    {
+        for ( i = 0; i < nPins; i++ )
+            if ( strcmp( pTemp, pPinNames[i] ) == 0 )
+                break;
+        if ( i == nPins )
+        { // cannot find this name; save it
+            pPinNames[nPins++] = Mio_UtilStrsav(pTemp);
+        }
+        // get the next name
+        pTemp = strtok( NULL, " " );
+    }
+    return nPins;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/map/mio/mioFunc.c b/src/map/mio/mioFunc.c
index c14944c4..c63a3794 100644
--- a/src/map/mio/mioFunc.c
+++ b/src/map/mio/mioFunc.c
@@ -17,7 +17,8 @@
 ***********************************************************************/
 
 #include "mioInt.h"
-#include "parse.h"
+//#include "parse.h"
+#include "exp.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -37,16 +38,13 @@ ABC_NAMESPACE_IMPL_START
 #define MIO_SYMB_OPEN   '('
 #define MIO_SYMB_CLOSE  ')'
 
-static int Mio_GateParseFormula( Mio_Gate_t * pGate );
-static int Mio_GateCollectNames( char * pFormula, char * pPinNames[] );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Deriving the functionality of the gates.]
+  Synopsis    [Registers the cube string with the network.]
 
   Description []
                
@@ -55,27 +53,61 @@ static int Mio_GateCollectNames( char * pFormula, char * pPinNames[] );
   SeeAlso     []
 
 ***********************************************************************/
-int Mio_LibraryParseFormulas( Mio_Library_t * pLib )
+char * Mio_SopRegister( Mem_Flex_t * pMan, char * pName )
 {
-    Mio_Gate_t * pGate;
+    char * pRegName;
+    if ( pName == NULL ) return NULL;
+    pRegName = Mem_FlexEntryFetch( pMan, strlen(pName) + 1 );
+    strcpy( pRegName, pName );
+    return pRegName;
+}
 
-    // count the gates
-    pLib->nGates = 0;
-    Mio_LibraryForEachGate( pLib, pGate )
-        pLib->nGates++;        
+/**Function*************************************************************
 
-    // start a temporary BDD manager
-    pLib->dd = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    // introduce ZDD variables
-    Cudd_zddVarsFromBddVars( pLib->dd, 2 );
+  Synopsis    [Collect the pin names in the formula.]
 
-    // for each gate, derive its function
-    Mio_LibraryForEachGate( pLib, pGate )
-        if ( Mio_GateParseFormula( pGate ) )
-            return 1;
-    return 0;
-}
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mio_GateCollectNames( char * pFormula, char * pPinNames[] )
+{
+    char Buffer[1000];
+    char * pTemp;
+    int nPins, i;
 
+    // save the formula as it was
+    strcpy( Buffer, pFormula );
+
+    // remove the non-name symbols
+    for ( pTemp = Buffer; *pTemp; pTemp++ )
+        if ( *pTemp == MIO_SYMB_AND  || *pTemp == MIO_SYMB_AND2   || 
+             *pTemp == MIO_SYMB_OR   || *pTemp == MIO_SYMB_OR2    || 
+             *pTemp == MIO_SYMB_XOR  || 
+             *pTemp == MIO_SYMB_NOT  || *pTemp == MIO_SYMB_AFTNOT ||
+             *pTemp == MIO_SYMB_OPEN || *pTemp == MIO_SYMB_CLOSE )
+             *pTemp = ' ';
+
+    // save the names
+    nPins = 0;
+    pTemp = strtok( Buffer, " " );
+    while ( pTemp )
+    {
+        for ( i = 0; i < nPins; i++ )
+            if ( strcmp( pTemp, pPinNames[i] ) == 0 )
+                break;
+        if ( i == nPins )
+        { // cannot find this name; save it
+            pPinNames[nPins++] = Mio_UtilStrsav(pTemp);
+        }
+        // get the next name
+        pTemp = strtok( NULL, " " );
+    }
+    return nPins;
+}
 
 /**Function*************************************************************
 
@@ -90,8 +122,6 @@ int Mio_LibraryParseFormulas( Mio_Library_t * pLib )
 ***********************************************************************/
 int Mio_GateParseFormula( Mio_Gate_t * pGate )
 {
-    extern char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
-    DdManager * dd = pGate->pLib->dd;
     char * pPinNames[100];
     char * pPinNamesCopy[100];
     Mio_Pin_t * pPin, ** ppPin;
@@ -114,14 +144,16 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
     {
         if ( strcmp( pGate->pForm, MIO_STRING_CONST0 ) == 0 )
         {
-            pGate->bFunc = b0;
-            pGate->pSop = Abc_SopRegister( (Mem_Flex_t *)pGate->pLib->pMmFlex, " 0\n" );
+//            pGate->bFunc = b0;
+            pGate->vExpr = Exp_Const0();
+            pGate->pSop = Mio_SopRegister( (Mem_Flex_t *)pGate->pLib->pMmFlex, " 0\n" );
             pGate->pLib->pGate0 = pGate;
         }
         else if ( strcmp( pGate->pForm, MIO_STRING_CONST1 ) == 0 )
         {
-            pGate->bFunc = b1;
-            pGate->pSop = Abc_SopRegister( (Mem_Flex_t *)pGate->pLib->pMmFlex, " 1\n" );
+//            pGate->bFunc = b1;
+            pGate->vExpr = Exp_Const1();
+            pGate->pSop = Mio_SopRegister( (Mem_Flex_t *)pGate->pLib->pMmFlex, " 1\n" );
             pGate->pLib->pGate1 = pGate;
         }
         else
@@ -129,7 +161,7 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
             printf( "Cannot parse formula \"%s\" of gate \"%s\".\n", pGate->pForm, pGate->pName );
             return 1;
         }
-        Cudd_Ref( pGate->bFunc );
+//        Cudd_Ref( pGate->bFunc );
         return 0;
     }
 
@@ -206,7 +238,7 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
         // copy the names back
         memcpy( pPinNames, pPinNamesCopy, nPins * sizeof(char *) );
     }
-
+/*
     // expand the manager if necessary
     if ( dd->size < nPins )
     {
@@ -214,21 +246,43 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
         dd = Cudd_Init( nPins + 10, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
         Cudd_zddVarsFromBddVars( dd, 2 );
     }
-
-    // derive the formula as the BDD
+    // derive formula as the BDD
     pGate->bFunc = Parse_FormulaParser( stdout, pGate->pForm, nPins, 0, pPinNames, dd, dd->vars );
     if ( pGate->bFunc == NULL )
         return 1;
     Cudd_Ref( pGate->bFunc );
-
-    // derive the cover (SOP)
+    // derive cover
     pGate->pSop = Abc_ConvertBddToSop( pGate->pLib->pMmFlex, dd, pGate->bFunc, pGate->bFunc, nPins, 0, pGate->pLib->vCube, -1 );
+*/
+
+    // derive expression 
+    pGate->vExpr = Mio_ParseFormula( pGate->pForm, (char **)pPinNames, nPins );
+    // derive cover
+    pGate->pSop = Mio_LibDeriveSop( nPins, pGate->vExpr, pGate->pLib->vCube );
+    pGate->pSop = Mio_SopRegister( (Mem_Flex_t *)pGate->pLib->pMmFlex, pGate->pSop );
+    // derive truth table
+    if ( nPins <= 6 )
+        pGate->uTruth = Exp_Truth6( nPins, pGate->vExpr, NULL );
+/*
+    // verify
+    if ( pGate->nInputs <= 6 )
+    {
+        extern word Abc_SopToTruth( char * pSop, int nInputs );
+        word t2 = Abc_SopToTruth( pGate->pSop, nPins );
+        if ( pGate->uTruth != t2 )
+        {
+            printf( "%s\n", pGate->pForm );
+            Exp_Print( nPins, pGate->vExpr );
+            printf( "Verification failed!\n" );
+        }
+    }
+*/
     return 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collect the pin names in the formula.]
+  Synopsis    [Deriving the functionality of the gates.]
 
   Description []
                
@@ -237,40 +291,20 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
   SeeAlso     []
 
 ***********************************************************************/
-int Mio_GateCollectNames( char * pFormula, char * pPinNames[] )
+int Mio_LibraryParseFormulas( Mio_Library_t * pLib )
 {
-    char Buffer[1000];
-    char * pTemp;
-    int nPins, i;
-
-    // save the formula as it was
-    strcpy( Buffer, pFormula );
+    Mio_Gate_t * pGate;
 
-    // remove the non-name symbols
-    for ( pTemp = Buffer; *pTemp; pTemp++ )
-        if ( *pTemp == MIO_SYMB_AND  || *pTemp == MIO_SYMB_AND2   || 
-             *pTemp == MIO_SYMB_OR   || *pTemp == MIO_SYMB_OR2    || 
-             *pTemp == MIO_SYMB_XOR  || 
-             *pTemp == MIO_SYMB_NOT  || *pTemp == MIO_SYMB_AFTNOT ||
-             *pTemp == MIO_SYMB_OPEN || *pTemp == MIO_SYMB_CLOSE )
-             *pTemp = ' ';
+    // count the gates
+    pLib->nGates = 0;
+    Mio_LibraryForEachGate( pLib, pGate )
+        pLib->nGates++;        
 
-    // save the names
-    nPins = 0;
-    pTemp = strtok( Buffer, " " );
-    while ( pTemp )
-    {
-        for ( i = 0; i < nPins; i++ )
-            if ( strcmp( pTemp, pPinNames[i] ) == 0 )
-                break;
-        if ( i == nPins )
-        { // cannot find this name; save it
-            pPinNames[nPins++] = Extra_UtilStrsav(pTemp);
-        }
-        // get the next name
-        pTemp = strtok( NULL, " " );
-    }
-    return nPins;
+    // for each gate, derive its function
+    Mio_LibraryForEachGate( pLib, pGate )
+        if ( Mio_GateParseFormula( pGate ) )
+            return 1;
+    return 0;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mio/mioInt.h b/src/map/mio/mioInt.h
index 87bd7d4e..0752e29a 100644
--- a/src/map/mio/mioInt.h
+++ b/src/map/mio/mioInt.h
@@ -24,13 +24,15 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#include "abc.h"
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include "vec.h"
 #include "mem.h"
-#include "mvc.h"
-#include "main.h"
+#include "st.h"
 #include "mio.h"
-#include "extra.h"
-
+ 
 ABC_NAMESPACE_HEADER_START
 
 
@@ -69,7 +71,7 @@ struct  Mio_LibraryStruct_t_
     Mio_Gate_t *       pGateNand2;  // the NAND2 gate
     Mio_Gate_t *       pGateAnd2;   // the AND2 gate
     st_table *         tName2Gate;  // the mapping of gate names into their pointer
-    DdManager *        dd;          // the nanager storing functions of gates
+//    DdManager *        dd;          // the nanager storing functions of gates
     Mem_Flex_t *       pMmFlex;     // the memory manaqer for SOPs
     Vec_Str_t *        vCube;       // temporary cube
 }; 
@@ -90,8 +92,11 @@ struct  Mio_GateStruct_t_
     // the derived information
     int                nInputs;     // the number of inputs
     double             dDelayMax;   // the maximum delay
-    DdNode *           bFunc;       // the functionality
+//    DdNode *           bFunc;       // the functionality
     char *             pSop;        // sum-of-products
+    Vec_Int_t *        vExpr;       // boolean expression
+    union { word       uTruth;      // truth table
+    word *             pTruth; };   // pointer to the truth table
     int                Value;       // user's information
 };
 
@@ -127,7 +132,6 @@ struct  Mio_PinStruct_t_
 /*=== mioUtils.c =============================================================*/
 
 
-
 ABC_NAMESPACE_HEADER_END
 
 #endif
diff --git a/src/map/mio/mioParse.c b/src/map/mio/mioParse.c
new file mode 100644
index 00000000..c68b7dea
--- /dev/null
+++ b/src/map/mio/mioParse.c
@@ -0,0 +1,391 @@
+/**CFile****************************************************************
+
+  FileName    [mioParse.c]
+
+  PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
+
+  Synopsis    [Parsing Boolean expressions.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 8, 2003.]
+
+  Revision    [$Id: mioParse.c,v 1.4 2004/06/28 14:20:25 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mioInt.h"
+#include "exp.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the list of operation symbols to be used in expressions
+#define MIO_EQN_SYM_OPEN    '('   // opening paranthesis
+#define MIO_EQN_SYM_CLOSE   ')'   // closing paranthesis
+#define MIO_EQN_SYM_CONST0  '0'   // constant 0
+#define MIO_EQN_SYM_CONST1  '1'   // constant 1
+#define MIO_EQN_SYM_NEG     '!'   // negation before the variable
+#define MIO_EQN_SYM_NEGAFT  '\''  // negation after the variable
+#define MIO_EQN_SYM_AND     '*'   // logic AND
+#define MIO_EQN_SYM_AND2    '&'   // logic AND
+#define MIO_EQN_SYM_XOR     '^'   // logic XOR
+#define MIO_EQN_SYM_OR      '+'   // logic OR
+#define MIO_EQN_SYM_OR2     '|'   // logic OR
+
+// the list of opcodes (also specifying operation precedence)
+#define MIO_EQN_OPER_NEG    10    // negation
+#define MIO_EQN_OPER_AND     9    // logic AND
+#define MIO_EQN_OPER_XOR     8    // logic XOR
+#define MIO_EQN_OPER_OR      7    // logic OR
+#define MIO_EQN_OPER_MARK    1    // OpStack token standing for an opening paranthesis
+
+// these are values of the internal Flag
+#define MIO_EQN_FLAG_START   1    // after the opening parenthesis 
+#define MIO_EQN_FLAG_VAR     2    // after operation is received
+#define MIO_EQN_FLAG_OPER    3    // after operation symbol is received
+#define MIO_EQN_FLAG_ERROR   4    // when error is detected
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs the operation on the top entries in the stack.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Mio_ParseFormulaOper( int * pMan, int nVars, Vec_Ptr_t * pStackFn, int Oper )
+{
+    Vec_Int_t * gArg1, * gArg2, * gFunc;
+    // perform the given operation
+    gArg2 = (Vec_Int_t *)Vec_PtrPop( pStackFn );
+    gArg1 = (Vec_Int_t *)Vec_PtrPop( pStackFn );
+    if ( Oper == MIO_EQN_OPER_AND )
+        gFunc = Exp_And( pMan, nVars, gArg1, gArg2, 0, 0 );
+    else if ( Oper == MIO_EQN_OPER_OR )
+        gFunc = Exp_Or( pMan, nVars, gArg1, gArg2 );
+    else if ( Oper == MIO_EQN_OPER_XOR )
+        gFunc = Exp_Xor( pMan, nVars, gArg1, gArg2 );
+    else
+        return NULL;
+//    Cudd_Ref( gFunc );
+//    Cudd_RecursiveDeref( dd, gArg1 );
+//    Cudd_RecursiveDeref( dd, gArg2 );
+    Vec_IntFree( gArg1 );
+    Vec_IntFree( gArg2 );
+    Vec_PtrPush( pStackFn,  gFunc );
+    return gFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG corresponding to the equation.]
+
+  Description [Takes the stream to output messages, the formula, the vector
+  of variable names and the AIG manager.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Mio_ParseFormula( char * pFormInit, char ** ppVarNames, int nVars )
+{
+    char * pFormula;
+    int Man = nVars, * pMan = &Man;
+    Vec_Ptr_t * pStackFn;
+    Vec_Int_t * pStackOp;
+    Vec_Int_t * gFunc;
+    char * pTemp, * pName;
+    int nParans, fFound, Flag;
+    int Oper, Oper1, Oper2;
+    int i, v;
+
+    // make sure that the number of opening and closing parantheses is the same
+    nParans = 0;
+    for ( pTemp = pFormInit; *pTemp; pTemp++ )
+        if ( *pTemp == '(' )
+            nParans++;
+        else if ( *pTemp == ')' )
+            nParans--;
+    if ( nParans != 0 )
+    {
+        fprintf( stdout, "Mio_ParseFormula(): Different number of opening and closing parantheses ().\n" );
+        return NULL;
+    }
+
+    // copy the formula
+    pFormula = ABC_ALLOC( char, strlen(pFormInit) + 3 );
+    sprintf( pFormula, "(%s)", pFormInit );
+
+    // start the stacks
+    pStackFn = Vec_PtrAlloc( 100 );
+    pStackOp = Vec_IntAlloc( 100 );
+
+    Flag = MIO_EQN_FLAG_START;
+    for ( pTemp = pFormula; *pTemp; pTemp++ )
+    {
+        switch ( *pTemp )
+        {
+        // skip all spaces, tabs, and end-of-lines
+        case ' ':
+        case '\t':
+        case '\r':
+        case '\n':
+            continue;
+        case MIO_EQN_SYM_CONST0:
+            Vec_PtrPush( pStackFn, Exp_Const0() );  // Cudd_Ref( b0 );
+            if ( Flag == MIO_EQN_FLAG_VAR )
+            {
+                fprintf( stdout, "Mio_ParseFormula(): No operation symbol before constant 0.\n" );
+                Flag = MIO_EQN_FLAG_ERROR; 
+                break;
+            }
+            Flag = MIO_EQN_FLAG_VAR; 
+            break;
+        case MIO_EQN_SYM_CONST1:
+            Vec_PtrPush( pStackFn, Exp_Const1() );  //  Cudd_Ref( b1 );
+            if ( Flag == MIO_EQN_FLAG_VAR )
+            {
+                fprintf( stdout, "Mio_ParseFormula(): No operation symbol before constant 1.\n" );
+                Flag = MIO_EQN_FLAG_ERROR; 
+                break;
+            }
+            Flag = MIO_EQN_FLAG_VAR; 
+            break;
+        case MIO_EQN_SYM_NEG:
+            if ( Flag == MIO_EQN_FLAG_VAR )
+            {// if NEGBEF follows a variable, AND is assumed
+                Vec_IntPush( pStackOp, MIO_EQN_OPER_AND );
+                Flag = MIO_EQN_FLAG_OPER;
+            }
+            Vec_IntPush( pStackOp, MIO_EQN_OPER_NEG );
+            break;
+        case MIO_EQN_SYM_NEGAFT:
+            if ( Flag != MIO_EQN_FLAG_VAR )
+            {// if there is no variable before NEGAFT, it is an error
+                fprintf( stdout, "Mio_ParseFormula(): No variable is specified before the negation suffix.\n" );
+                Flag = MIO_EQN_FLAG_ERROR; 
+                break;
+            }
+            else // if ( Flag == PARSE_FLAG_VAR )
+                Vec_PtrPush( pStackFn, Exp_Not( (Vec_Int_t *)Vec_PtrPop(pStackFn) ) );
+            break;
+        case MIO_EQN_SYM_AND:
+        case MIO_EQN_SYM_AND2:
+        case MIO_EQN_SYM_OR:
+        case MIO_EQN_SYM_OR2:
+        case MIO_EQN_SYM_XOR:
+            if ( Flag != MIO_EQN_FLAG_VAR )
+            {
+                fprintf( stdout, "Mio_ParseFormula(): There is no variable before AND, EXOR, or OR.\n" );
+                Flag = MIO_EQN_FLAG_ERROR; 
+                break;
+            }
+            if ( *pTemp == MIO_EQN_SYM_AND || *pTemp == MIO_EQN_SYM_AND2 )
+                Vec_IntPush( pStackOp, MIO_EQN_OPER_AND );
+            else if ( *pTemp == MIO_EQN_SYM_OR || *pTemp == MIO_EQN_SYM_OR2 )
+                Vec_IntPush( pStackOp, MIO_EQN_OPER_OR );
+            else //if ( *pTemp == MIO_EQN_SYM_XOR )
+                Vec_IntPush( pStackOp, MIO_EQN_OPER_XOR );
+            Flag = MIO_EQN_FLAG_OPER; 
+            break;
+        case MIO_EQN_SYM_OPEN:
+            if ( Flag == MIO_EQN_FLAG_VAR )
+            {
+                Vec_IntPush( pStackOp, MIO_EQN_OPER_AND );
+//                fprintf( stdout, "Mio_ParseFormula(): An opening paranthesis follows a var without operation sign.\n" ); 
+//                Flag = MIO_EQN_FLAG_ERROR; 
+//              break; 
+            }
+            Vec_IntPush( pStackOp, MIO_EQN_OPER_MARK );
+            // after an opening bracket, it feels like starting over again
+            Flag = MIO_EQN_FLAG_START; 
+            break;
+        case MIO_EQN_SYM_CLOSE:
+            if ( Vec_IntSize( pStackOp ) != 0 )
+            {
+                while ( 1 )
+                {
+                    if ( Vec_IntSize( pStackOp ) == 0 )
+                    {
+                        fprintf( stdout, "Mio_ParseFormula(): There is no opening paranthesis\n" );
+                        Flag = MIO_EQN_FLAG_ERROR; 
+                        break;
+                    }
+                    Oper = Vec_IntPop( pStackOp );
+                    if ( Oper == MIO_EQN_OPER_MARK )
+                        break;
+
+                    // perform the given operation
+                    if ( Mio_ParseFormulaOper( pMan, nVars, pStackFn, Oper ) == NULL )
+                    {
+                        fprintf( stdout, "Mio_ParseFormula(): Unknown operation\n" );
+                        ABC_FREE( pFormula );
+                        Vec_PtrFreeP( &pStackFn );
+                        Vec_IntFreeP( &pStackOp );
+                        return NULL;
+                    }
+                }
+            }
+            else
+            {
+                fprintf( stdout, "Mio_ParseFormula(): There is no opening paranthesis\n" );
+                Flag = MIO_EQN_FLAG_ERROR; 
+                break;
+            }
+            if ( Flag != MIO_EQN_FLAG_ERROR )
+                Flag = MIO_EQN_FLAG_VAR; 
+            break;
+
+
+        default:
+            // scan the next name
+            for ( i = 0; pTemp[i] && 
+                         pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' &&
+                         pTemp[i] != MIO_EQN_SYM_AND && pTemp[i] != MIO_EQN_SYM_AND2 && pTemp[i] != MIO_EQN_SYM_OR && pTemp[i] != MIO_EQN_SYM_OR2 && 
+                         pTemp[i] != MIO_EQN_SYM_XOR && pTemp[i] != MIO_EQN_SYM_NEGAFT && pTemp[i] != MIO_EQN_SYM_CLOSE; 
+                  i++ )
+              {
+                    if ( pTemp[i] == MIO_EQN_SYM_NEG || pTemp[i] == MIO_EQN_SYM_OPEN )
+                    {
+                        fprintf( stdout, "Mio_ParseFormula(): The negation sign or an opening paranthesis inside the variable name.\n" );
+                        Flag = MIO_EQN_FLAG_ERROR; 
+                        break;
+                    }
+              }
+            // variable name is found
+            fFound = 0;
+//            Vec_PtrForEachEntry( char *, vVarNames, pName, v )
+            for ( v = 0; v < nVars; v++ )
+            {
+                pName = ppVarNames[v];
+                if ( strncmp(pTemp, pName, i) == 0 && strlen(pName) == (unsigned)i )
+                {
+                    pTemp += i-1;
+                    fFound = 1;
+                    break;
+                }
+            }
+            if ( !fFound )
+            { 
+                fprintf( stdout, "Mio_ParseFormula(): The parser cannot find var \"%s\" in the input var list.\n", pTemp ); 
+                Flag = MIO_EQN_FLAG_ERROR; 
+                break; 
+            }
+/*
+            if ( Flag == MIO_EQN_FLAG_VAR )
+            {
+                fprintf( stdout, "Mio_ParseFormula(): The variable name \"%s\" follows another var without operation sign.\n", pTemp ); 
+                Flag = MIO_EQN_FLAG_ERROR; 
+                break; 
+            }
+*/
+            if ( Flag == MIO_EQN_FLAG_VAR )
+                Vec_IntPush( pStackOp, MIO_EQN_OPER_AND );
+
+            Vec_PtrPush( pStackFn, Exp_Var(v) ); // Cudd_Ref( pbVars[v] );
+            Flag = MIO_EQN_FLAG_VAR; 
+            break;
+        }
+
+        if ( Flag == MIO_EQN_FLAG_ERROR )
+            break;      // error exit
+        else if ( Flag == MIO_EQN_FLAG_START )
+            continue;  //  go on parsing
+        else if ( Flag == MIO_EQN_FLAG_VAR )
+            while ( 1 )
+            {  // check if there are negations in the OpStack     
+                if ( Vec_IntSize( pStackOp ) == 0 )
+                    break;
+                Oper = Vec_IntPop( pStackOp );
+                if ( Oper != MIO_EQN_OPER_NEG )
+                {
+                    Vec_IntPush( pStackOp, Oper );
+                    break;
+                }
+                else
+                {
+                      Vec_PtrPush( pStackFn, Exp_Not((Vec_Int_t *)Vec_PtrPop(pStackFn)) );
+                }
+            }
+        else // if ( Flag == MIO_EQN_FLAG_OPER )
+            while ( 1 )
+            {  // execute all the operations in the OpStack
+               // with precedence higher or equal than the last one
+                Oper1 = Vec_IntPop( pStackOp ); // the last operation
+                if ( Vec_IntSize( pStackOp ) == 0 ) 
+                {  // if it is the only operation, push it back
+                    Vec_IntPush( pStackOp, Oper1 );
+                    break;
+                }
+                Oper2 = Vec_IntPop( pStackOp ); // the operation before the last one
+                if ( Oper2 >= Oper1 )  
+                {  // if Oper2 precedence is higher or equal, execute it
+                    if ( Mio_ParseFormulaOper( pMan, nVars, pStackFn, Oper2 ) == NULL )
+                    {
+                        fprintf( stdout, "Mio_ParseFormula(): Unknown operation\n" );
+                        ABC_FREE( pFormula );
+                        Vec_PtrFreeP( &pStackFn );
+                        Vec_IntFreeP( &pStackOp );
+                        return NULL;
+                    }
+                    Vec_IntPush( pStackOp,  Oper1 );     // push the last operation back
+                }
+                else
+                {  // if Oper2 precedence is lower, push them back and done
+                    Vec_IntPush( pStackOp, Oper2 );
+                    Vec_IntPush( pStackOp, Oper1 );
+                    break;
+                }
+            }
+    }
+
+    if ( Flag != MIO_EQN_FLAG_ERROR )
+    {
+        if ( Vec_PtrSize(pStackFn) != 0 )
+        {    
+            gFunc = (Vec_Int_t *)Vec_PtrPop(pStackFn);
+            if ( Vec_PtrSize(pStackFn) == 0 )
+                if ( Vec_IntSize( pStackOp ) == 0 )
+                {
+//                    Cudd_Deref( gFunc );
+                    ABC_FREE( pFormula );
+                    Vec_PtrFreeP( &pStackFn );
+                    Vec_IntFreeP( &pStackOp );
+                    return Exp_Reverse(gFunc);
+                }
+                else
+                    fprintf( stdout, "Mio_ParseFormula(): Something is left in the operation stack\n" );
+            else
+                fprintf( stdout, "Mio_ParseFormula(): Something is left in the function stack\n" );
+        }
+        else
+            fprintf( stdout, "Mio_ParseFormula(): The input string is empty\n" );
+    }
+    ABC_FREE( pFormula );
+    Vec_PtrFreeP( &pStackFn );
+    Vec_IntFreeP( &pStackOp );
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/map/mio/mioRead.c b/src/map/mio/mioRead.c
index 3b93856c..dd57d766 100644
--- a/src/map/mio/mioRead.c
+++ b/src/map/mio/mioRead.c
@@ -18,6 +18,7 @@
 
 #include <ctype.h>
 #include "mioInt.h"
+#include "ioAbc.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -30,13 +31,13 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-static Mio_Library_t * Mio_LibraryReadOne( Abc_Frame_t * pAbc, char * FileName, int fExtendedFormat, st_table * tExcludeGate, int fVerbose );
-static int          Mio_LibraryReadInternal( Mio_Library_t * pLib, char * pBuffer, int fExtendedFormat, st_table * tExcludeGate, int fVerbose );
-static Mio_Gate_t * Mio_LibraryReadGate( char ** ppToken, int fExtendedFormat );
-static Mio_Pin_t *  Mio_LibraryReadPin( char ** ppToken, int fExtendedFormat );
-static char *       chomp( char *s );
-static void         Mio_LibraryDetectSpecialGates( Mio_Library_t * pLib );
-static void         Io_ReadFileRemoveComments( char * pBuffer, int * pnDots, int * pnLines );
+static Mio_Library_t * Mio_LibraryReadOne( char * FileName, int fExtendedFormat, st_table * tExcludeGate, int fVerbose );
+static int             Mio_LibraryReadInternal( Mio_Library_t * pLib, char * pBuffer, int fExtendedFormat, st_table * tExcludeGate, int fVerbose );
+static Mio_Gate_t *    Mio_LibraryReadGate( char ** ppToken, int fExtendedFormat );
+static Mio_Pin_t *     Mio_LibraryReadPin( char ** ppToken, int fExtendedFormat );
+static char *          chomp( char *s );
+static void            Mio_LibraryDetectSpecialGates( Mio_Library_t * pLib );
+static void            Io_ReadFileRemoveComments( char * pBuffer, int * pnDots, int * pnLines );
 
 /**Function*************************************************************
 
@@ -49,7 +50,7 @@ static void         Io_ReadFileRemoveComments( char * pBuffer, int * pnDots, int
   SeeAlso     []
 
 ***********************************************************************/
-Mio_Library_t * Mio_LibraryRead( void * pAbc, char * FileName, char * ExcludeFile, int fVerbose )
+Mio_Library_t * Mio_LibraryRead( char * FileName, char * ExcludeFile, int fVerbose )
 {
     Mio_Library_t * pLib;
     int num;
@@ -59,19 +60,19 @@ Mio_Library_t * Mio_LibraryRead( void * pAbc, char * FileName, char * ExcludeFil
     if ( ExcludeFile )
     {
         tExcludeGate = st_init_table(strcmp, st_strhash);
-        if ( (num = Mio_LibraryReadExclude( pAbc, ExcludeFile, tExcludeGate )) == -1 )
+        if ( (num = Mio_LibraryReadExclude( ExcludeFile, tExcludeGate )) == -1 )
         {
             st_free_table( tExcludeGate );
             tExcludeGate = 0;
             return 0;
         }
-        fprintf ( Abc_FrameReadOut( (Abc_Frame_t *)pAbc ), "Read %d gates from exclude file\n", num );
+        fprintf ( stdout, "Read %d gates from exclude file\n", num );
     }
 
-    pLib = Mio_LibraryReadOne( (Abc_Frame_t *)pAbc, FileName, 0, tExcludeGate, fVerbose );       // try normal format first ..
+    pLib = Mio_LibraryReadOne( FileName, 0, tExcludeGate, fVerbose );       // try normal format first ..
     if ( pLib == NULL )
     {
-        pLib = Mio_LibraryReadOne( (Abc_Frame_t *)pAbc, FileName, 1, tExcludeGate, fVerbose );   // .. otherwise try extended format 
+        pLib = Mio_LibraryReadOne( FileName, 1, tExcludeGate, fVerbose );   // .. otherwise try extended format 
         if ( pLib != NULL )
             printf ( "Warning: Read extended GENLIB format but ignoring extensions\n" );
     }
@@ -92,7 +93,7 @@ Mio_Library_t * Mio_LibraryRead( void * pAbc, char * FileName, char * ExcludeFil
   SeeAlso     []
 
 ***********************************************************************/
-Mio_Library_t * Mio_LibraryReadOne( Abc_Frame_t * pAbc, char * FileName, int fExtendedFormat, st_table * tExcludeGate, int fVerbose )
+Mio_Library_t * Mio_LibraryReadOne( char * FileName, int fExtendedFormat, st_table * tExcludeGate, int fVerbose )
 {
     Mio_Library_t * pLib;
     char * pBuffer = 0;
@@ -100,7 +101,7 @@ Mio_Library_t * Mio_LibraryReadOne( Abc_Frame_t * pAbc, char * FileName, int fEx
     // allocate the genlib structure
     pLib = ABC_ALLOC( Mio_Library_t, 1 );
     memset( pLib, 0, sizeof(Mio_Library_t) );
-    pLib->pName = Extra_UtilStrsav( FileName );
+    pLib->pName = Mio_UtilStrsav( FileName );
     pLib->tName2Gate = st_init_table(strcmp, st_strhash);
     pLib->pMmFlex = Mem_FlexStart();
     pLib->vCube = Vec_StrAlloc( 100 );
@@ -252,7 +253,7 @@ Mio_Gate_t * Mio_LibraryReadGate( char ** ppToken, int fExtendedFormat )
 
     // read the name
     pToken = strtok( NULL, " \t\r\n" );
-    pGate->pName = Extra_UtilStrsav( pToken );
+    pGate->pName = Mio_UtilStrsav( pToken );
 
     // read the area
     pToken = strtok( NULL, " \t\r\n" );
@@ -320,7 +321,7 @@ Mio_Pin_t * Mio_LibraryReadPin( char ** ppToken, int fExtendedFormat )
 
     // read the name
     pToken = strtok( NULL, " \t\r\n" );
-    pPin->pName = Extra_UtilStrsav( pToken );
+    pPin->pName = Mio_UtilStrsav( pToken );
 
     // read the pin phase
     pToken = strtok( NULL, " \t\r\n" );
@@ -504,18 +505,18 @@ void Mio_LibrarySortGates( Mio_Library_t * pLib )
 void Mio_LibraryDetectSpecialGates( Mio_Library_t * pLib )
 {
     Mio_Gate_t * pGate;
-    DdNode * bFuncBuf, * bFuncInv, * bFuncNand2, * bFuncAnd2;
+    word uFuncBuf, uFuncInv, uFuncNand2, uFuncAnd2;
 
     Mio_LibrarySortGates( pLib );
 
-    bFuncBuf   = pLib->dd->vars[0];                                              Cudd_Ref( bFuncBuf );
-    bFuncInv   = Cudd_Not( pLib->dd->vars[0] );                                  Cudd_Ref( bFuncInv );
-    bFuncNand2 = Cudd_bddNand( pLib->dd, pLib->dd->vars[0], pLib->dd->vars[1] ); Cudd_Ref( bFuncNand2 );
-    bFuncAnd2  = Cudd_bddAnd( pLib->dd, pLib->dd->vars[0], pLib->dd->vars[1] );  Cudd_Ref( bFuncAnd2 );
+    uFuncBuf   = 0xAAAAAAAAAAAAAAAA;
+    uFuncAnd2  = 0xAAAAAAAAAAAAAAAA & 0xCCCCCCCCCCCCCCCC;
+    uFuncInv   = ~uFuncBuf;
+    uFuncNand2 = ~uFuncAnd2;
 
     // get buffer
     Mio_LibraryForEachGate( pLib, pGate )
-        if ( pLib->pGateBuf == NULL && pGate->bFunc == bFuncBuf )
+        if ( pLib->pGateBuf == NULL && pGate->uTruth == uFuncBuf )
         {
             pLib->pGateBuf = pGate;
             break;
@@ -528,7 +529,7 @@ void Mio_LibraryDetectSpecialGates( Mio_Library_t * pLib )
  
     // get inverter
     Mio_LibraryForEachGate( pLib, pGate )
-        if ( pLib->pGateInv == NULL && pGate->bFunc == bFuncInv )
+        if ( pLib->pGateInv == NULL && pGate->uTruth == uFuncInv )
         {
             pLib->pGateInv = pGate;
             break;
@@ -541,13 +542,13 @@ void Mio_LibraryDetectSpecialGates( Mio_Library_t * pLib )
 
     // get the NAND2 and AND2 gates
     Mio_LibraryForEachGate( pLib, pGate )
-        if ( pLib->pGateNand2 == NULL && pGate->bFunc == bFuncNand2 )
+        if ( pLib->pGateNand2 == NULL && pGate->uTruth == uFuncNand2 )
         {
             pLib->pGateNand2 = pGate;
             break;
         }
     Mio_LibraryForEachGate( pLib, pGate )
-        if ( pLib->pGateAnd2 == NULL && pGate->bFunc == bFuncAnd2 )
+        if ( pLib->pGateAnd2 == NULL && pGate->uTruth == uFuncAnd2 )
         {
             pLib->pGateAnd2 = pGate;
             break;
@@ -557,10 +558,6 @@ void Mio_LibraryDetectSpecialGates( Mio_Library_t * pLib )
         printf( "Warnings: GENLIB library reader cannot detect the AND2 or NAND2 gate.\n" );
         printf( "Some parts of the supergate-based technology mapper may not work correctly.\n" );
     }
-
-    Cudd_RecursiveDeref( pLib->dd, bFuncInv );
-    Cudd_RecursiveDeref( pLib->dd, bFuncNand2 );
-    Cudd_RecursiveDeref( pLib->dd, bFuncAnd2 );
 }
 
 /**Function*************************************************************
@@ -574,7 +571,7 @@ void Mio_LibraryDetectSpecialGates( Mio_Library_t * pLib )
   SeeAlso     []
 
 ***********************************************************************/
-int Mio_LibraryReadExclude( void * pAbc, char * ExcludeFile, st_table * tExcludeGate )
+int Mio_LibraryReadExclude( char * ExcludeFile, st_table * tExcludeGate )
 {
     int nDel = 0;
     FILE *pEx;
@@ -588,14 +585,14 @@ int Mio_LibraryReadExclude( void * pAbc, char * ExcludeFile, st_table * tExclude
 
         if ( pEx == NULL )
         {
-            fprintf ( Abc_FrameReadErr( (Abc_Frame_t *)pAbc ), "Error: Could not open exclude file %s. Stop.\n", ExcludeFile );
+            fprintf ( stdout, "Error: Could not open exclude file %s. Stop.\n", ExcludeFile );
             return -1;
         }
 
         while (1 == fscanf( pEx, "%127s", buffer ))
         {
             //printf ("Read: '%s'\n", buffer );
-            st_insert( tExcludeGate, Extra_UtilStrsav( buffer ), (char *)0 );
+            st_insert( tExcludeGate, Mio_UtilStrsav( buffer ), (char *)0 );
             nDel++;
         }
 
diff --git a/src/map/mio/mioSop.c b/src/map/mio/mioSop.c
new file mode 100644
index 00000000..46122121
--- /dev/null
+++ b/src/map/mio/mioSop.c
@@ -0,0 +1,333 @@
+/**CFile****************************************************************
+
+  FileName    [mioSop.c]
+
+  PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
+
+  Synopsis    [Derives SOP from Boolean expression.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 8, 2003.]
+
+  Revision    [$Id: mioSop.c,v 1.4 2004/06/28 14:20:25 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mioInt.h"
+#include "exp.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline unsigned Mio_CubeVar0( int v )                       { return (1<< (v<<1)   );                   }
+static inline unsigned Mio_CubeVar1( int v )                       { return (1<<((v<<1)+1));                   }
+static inline int      Mio_CubeHasVar0( unsigned x, int v )        { return (x & Mio_CubeVar0(v)) > 0;         }
+static inline int      Mio_CubeHasVar1( unsigned x, int v )        { return (x & Mio_CubeVar1(v)) > 0;         }
+static inline int      Mio_CubeEmpty( unsigned x )                 { return (x & (x>>1) & 0x55555555) != 0;    }
+static inline unsigned Mio_CubeAnd( unsigned x, unsigned y )       { return x | y;                             }
+static inline int      Mio_CubeContains( unsigned x, unsigned y )  { return (x | y) == y;                      } // x contains y
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Push while performing SCC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mio_SopPushSCC( Vec_Int_t * p, unsigned c )
+{
+    unsigned Entry;
+    int i, k = 0;
+    Vec_IntForEachEntry( p, Entry, i )
+    {
+        if ( Mio_CubeContains( Entry, c ) ) // Entry contains c
+        {
+            assert( i == k );
+            return;
+        }
+        if ( Mio_CubeContains( c, Entry ) ) // c contains Entry
+            continue;
+        Vec_IntWriteEntry( p, k++, Entry );
+    }
+    Vec_IntShrink( p, k );
+    Vec_IntPush( p, c );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Make the OR of two covers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Mio_SopCoverOr( Vec_Int_t * p, Vec_Int_t * q )
+{
+    Vec_Int_t * r;
+    unsigned Entry;
+    int i;
+    r = Vec_IntAlloc( Vec_IntSize(p) + Vec_IntSize(q) );
+    Vec_IntForEachEntry( p, Entry, i )
+        Vec_IntPush( r, Entry );
+    Vec_IntForEachEntry( q, Entry, i )
+        Mio_SopPushSCC( r, Entry );
+    return r;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Make the AND of two covers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Mio_SopCoverAnd( Vec_Int_t * p, Vec_Int_t * q )
+{
+    Vec_Int_t * r;
+    unsigned EntryP, EntryQ;
+    int i, k;
+    r = Vec_IntAlloc( Vec_IntSize(p) * Vec_IntSize(q) );
+    Vec_IntForEachEntry( p, EntryP, i )
+        Vec_IntForEachEntry( q, EntryQ, k )
+            if ( !Mio_CubeEmpty( Mio_CubeAnd(EntryP, EntryQ) ) )
+                Mio_SopPushSCC( r, Mio_CubeAnd(EntryP, EntryQ) );
+    return r;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create negative literal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Mio_SopVar0( int i )
+{
+    Vec_Int_t * vSop;
+    vSop = Vec_IntAlloc( 1 );
+    Vec_IntPush( vSop, Mio_CubeVar0(i) );
+    return vSop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create positive literal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Mio_SopVar1( int i )
+{
+    Vec_Int_t * vSop;
+    vSop = Vec_IntAlloc( 1 );
+    Vec_IntPush( vSop, Mio_CubeVar1(i) );
+    return vSop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create constant 0 literal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Mio_SopConst0()
+{
+    Vec_Int_t * vSop;
+    vSop = Vec_IntAlloc( 1 );
+    return vSop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create constant 1 literal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Mio_SopConst1()
+{
+    Vec_Int_t * vSop;
+    vSop = Vec_IntAlloc( 1 );
+    Vec_IntPush( vSop, 0 );
+    return vSop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives SOP representation as the char string.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Mio_SopDeriveFromArray( Vec_Int_t * vSop, int nVars, Vec_Str_t * vStr, int fPolarity )
+{
+    unsigned Entry;
+    int i, k;
+    Vec_StrClear( vStr );
+    if ( Vec_IntSize(vSop) == 0 )
+    {
+        Vec_StrPush( vStr, ' ' );
+        Vec_StrPush( vStr, (char)('1'-fPolarity) );
+        Vec_StrPush( vStr, '\n' );
+        Vec_StrPush( vStr, '\0' );
+        return Vec_StrArray( vStr );
+    }
+    if ( Vec_IntSize(vSop) == 1 && Vec_IntEntry(vSop, 0) == 0 )
+    {
+        Vec_StrPush( vStr, ' ' );
+        Vec_StrPush( vStr, (char)('0'+fPolarity) );
+        Vec_StrPush( vStr, '\n' );
+        Vec_StrPush( vStr, '\0' );
+        return Vec_StrArray( vStr );
+    }
+    // create cubes
+    Vec_IntForEachEntry( vSop, Entry, i )
+    {
+        for ( k = 0; k < nVars; k++ )
+        {
+            if ( Mio_CubeHasVar0( Entry, k ) )
+                Vec_StrPush( vStr, '0' );
+            else if ( Mio_CubeHasVar1( Entry, k ) )
+                Vec_StrPush( vStr, '1' );
+            else 
+                Vec_StrPush( vStr, '-' );
+        }
+        Vec_StrPush( vStr, ' ' );
+        Vec_StrPush( vStr, (char)('0'+fPolarity) );
+        Vec_StrPush( vStr, '\n' );
+    }
+    Vec_StrPush( vStr, '\0' );
+    return Vec_StrArray( vStr );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives SOP representation.]
+
+  Description [The SOP is guaranteed to be SCC-free but not minimal.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Mio_LibDeriveSop( int nVars, Vec_Int_t * vExpr, Vec_Str_t * vStr )
+{
+    Vec_Int_t * vSop;
+    Vec_Ptr_t * vSops0, * vSops1, * vTemp;
+    int i, Index0, Index1, fCompl0, fCompl1;
+    Vec_StrClear( vStr );
+    if ( Exp_IsConst0(vExpr) )
+    {
+        Vec_StrPrintStr( vStr, " 0\n" );
+        Vec_StrPush( vStr, '\0' );
+        return Vec_StrArray( vStr );
+    }
+    if ( Exp_IsConst1(vExpr) )
+    {
+        Vec_StrPrintStr( vStr, " 1\n" );
+        Vec_StrPush( vStr, '\0' );
+        return Vec_StrArray( vStr );
+    }
+    if ( Exp_IsLit(vExpr) )
+    {
+        for ( i = 0; i < nVars; i++ )
+            Vec_StrPush( vStr, '-' );
+        Vec_StrPrintStr( vStr, " 1\n" );
+        Vec_StrPush( vStr, '\0' );
+        assert( (Vec_IntEntry(vExpr,0) >> 1) < nVars );
+        Vec_StrWriteEntry( vStr, Vec_IntEntry(vExpr,0) >> 1, (char)('1' - (Vec_IntEntry(vExpr,0) & 1)) );
+        return Vec_StrArray( vStr );
+    }
+    vSops0 = Vec_PtrAlloc( nVars + Exp_NodeNum(vExpr) );
+    vSops1 = Vec_PtrAlloc( nVars + Exp_NodeNum(vExpr) );
+    for ( i = 0; i < nVars; i++ )
+    {
+        Vec_PtrPush( vSops0, Mio_SopVar0(i) );
+        Vec_PtrPush( vSops1, Mio_SopVar1(i) );
+    }
+    for ( i = 0; i < Exp_NodeNum(vExpr); i++ )
+    {
+        Index0  = Vec_IntEntry( vExpr, 2*i+0 ) >> 1;
+        Index1  = Vec_IntEntry( vExpr, 2*i+1 ) >> 1;
+        fCompl0 = Vec_IntEntry( vExpr, 2*i+0 ) & 1;
+        fCompl1 = Vec_IntEntry( vExpr, 2*i+1 ) & 1;
+        // positive polarity
+        vSop = Mio_SopCoverAnd( fCompl0 ? (Vec_Int_t *)Vec_PtrEntry(vSops0, Index0) : (Vec_Int_t *)Vec_PtrEntry(vSops1, Index0),
+                                fCompl1 ? (Vec_Int_t *)Vec_PtrEntry(vSops0, Index1) : (Vec_Int_t *)Vec_PtrEntry(vSops1, Index1) );
+        Vec_PtrPush( vSops1, vSop );
+        // negative polarity
+        vSop = Mio_SopCoverOr( fCompl0 ? (Vec_Int_t *)Vec_PtrEntry(vSops1, Index0) : (Vec_Int_t *)Vec_PtrEntry(vSops0, Index0),
+                               fCompl1 ? (Vec_Int_t *)Vec_PtrEntry(vSops1, Index1) : (Vec_Int_t *)Vec_PtrEntry(vSops0, Index1) );
+        Vec_PtrPush( vSops0, vSop );
+    }
+    // complement
+    if ( Vec_IntEntryLast(vExpr) & 1 )
+    {
+        vTemp  = vSops0;
+        vSops0 = vSops1;
+        vSops1 = vTemp;
+    }
+    // select the best polarity
+    if ( Vec_IntSize( (Vec_Int_t *)Vec_PtrEntryLast(vSops0) ) < Vec_IntSize( (Vec_Int_t *)Vec_PtrEntryLast(vSops1) ) )
+        vSop = (Vec_Int_t *)Vec_PtrEntryLast(vSops0);
+    else
+        vSop = (Vec_Int_t *)Vec_PtrEntryLast(vSops1);
+    // convert positive polarity into SOP
+    Mio_SopDeriveFromArray( vSop, nVars, vStr, (vSop == Vec_PtrEntryLast(vSops1)) );
+    Vec_VecFree( (Vec_Vec_t *)vSops0 );
+    Vec_VecFree( (Vec_Vec_t *)vSops1 );
+    return Vec_StrArray( vStr );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c
index d0d47060..09f1ec96 100644
--- a/src/map/mio/mioUtils.c
+++ b/src/map/mio/mioUtils.c
@@ -17,6 +17,8 @@
 ***********************************************************************/
 
 #include "mioInt.h"
+#include "main.h"
+#include "exp.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,7 +30,6 @@ ABC_NAMESPACE_IMPL_START
 static void Mio_WriteGate( FILE * pFile, Mio_Gate_t * pGate, int fPrintSops );
 static void Mio_WritePin( FILE * pFile, Mio_Pin_t * pPin );
 static int  Mio_DelayCompare( Mio_Gate_t ** ppG1, Mio_Gate_t ** ppG2 );
-static void Mio_DeriveTruthTable_rec( DdNode * bFunc, unsigned uTruthsIn[][2], unsigned uTruthRes[] );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -60,8 +61,8 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
     Vec_StrFree( pLib->vCube );
     if ( pLib->tName2Gate )
         st_free_table( pLib->tName2Gate );
-    if ( pLib->dd )
-        Cudd_Quit( pLib->dd );
+//    if ( pLib->dd )
+//        Cudd_Quit( pLib->dd );
     ABC_FREE( pLib->ppGates0 );
     ABC_FREE( pLib->ppGatesName );
     ABC_FREE( pLib );
@@ -81,11 +82,14 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
 void Mio_GateDelete( Mio_Gate_t * pGate )
 {
     Mio_Pin_t * pPin, * pPin2;
+    if ( pGate->nInputs > 6 )
+        ABC_FREE( pGate->pTruth );
+    Vec_IntFreeP( &pGate->vExpr );
     ABC_FREE( pGate->pOutName );
     ABC_FREE( pGate->pName );
     ABC_FREE( pGate->pForm );
-    if ( pGate->bFunc )
-        Cudd_RecursiveDeref( pGate->pLib->dd, pGate->bFunc );
+//    if ( pGate->bFunc )
+//        Cudd_RecursiveDeref( pGate->pLib->dd, pGate->bFunc );
     Mio_GateForEachPinSafe( pGate, pPin, pPin2 )
         Mio_PinDelete( pPin );   
     ABC_FREE( pGate );
@@ -125,7 +129,7 @@ Mio_Pin_t * Mio_PinDup( Mio_Pin_t * pPin )
 
     pPinNew = ABC_ALLOC( Mio_Pin_t, 1 );
     *pPinNew = *pPin;
-    pPinNew->pName = (pPinNew->pName ? Extra_UtilStrsav(pPinNew->pName) : NULL);
+    pPinNew->pName = (pPinNew->pName ? Mio_UtilStrsav(pPinNew->pName) : NULL);
     pPinNew->pNext = NULL;
 
     return pPinNew;
@@ -229,11 +233,11 @@ Mio_Gate_t ** Mio_CollectRoots( Mio_Library_t * pLib, int nInputs, float tDelay,
     Mio_Gate_t ** ppGates;
     /* st_table * tFuncs; */
     /* st_generator * gen; */
-    DdNode * bFunc;
-    DdManager * dd;
+//    DdNode * bFunc;
+//    DdManager * dd;
     int nGates, iGate;
 
-    dd     = Mio_LibraryReadDd( pLib );
+//    dd     = Mio_LibraryReadDd( pLib );
     nGates = Mio_LibraryReadGateNum( pLib );
 
     /*
@@ -272,16 +276,19 @@ Mio_Gate_t ** Mio_CollectRoots( Mio_Library_t * pLib, int nInputs, float tDelay,
     iGate = 0;
     Mio_LibraryForEachGate( pLib, pGate )
     {
-        bFunc = Mio_GateReadFunc(pGate);
+//        bFunc = Mio_GateReadFunc(pGate);
         if ( pGate->nInputs > nInputs )
             continue;
         if ( pGate->dDelayMax > (double)tDelay )
             continue;
-        if ( bFunc == b0 || bFunc == b1 )
+//        if ( bFunc == b0 || bFunc == b1 )
+        if ( pGate->uTruth == 0 || pGate->uTruth == ~0 )
             continue;
-        if ( bFunc == dd->vars[0] )
+//        if ( bFunc == dd->vars[0] )
+        if ( pGate->uTruth == 0xAAAAAAAAAAAAAAAA )
             continue;
-        if ( bFunc == Cudd_Not(dd->vars[0]) && fSkipInv )
+//        if ( bFunc == Cudd_Not(dd->vars[0]) && fSkipInv )
+        if ( pGate->uTruth == ~0xAAAAAAAAAAAAAAAA && fSkipInv )
             continue;
 
         assert( iGate < nGates );
@@ -332,11 +339,24 @@ int Mio_DelayCompare( Mio_Gate_t ** ppG1, Mio_Gate_t ** ppG2 )
   SeeAlso     []
 
 ***********************************************************************/
-void Mio_DeriveTruthTable( Mio_Gate_t * pGate, unsigned uTruthsIn[][2], int nSigns, int nInputs, unsigned uTruthRes[] )
+word Mio_DeriveTruthTable6( Mio_Gate_t * pGate )
 {
-    Mio_DeriveTruthTable_rec( pGate->bFunc, uTruthsIn, uTruthRes );
+    static unsigned uTruths6[6][2] = {
+        { 0xAAAAAAAA, 0xAAAAAAAA },
+        { 0xCCCCCCCC, 0xCCCCCCCC },
+        { 0xF0F0F0F0, 0xF0F0F0F0 },
+        { 0xFF00FF00, 0xFF00FF00 },
+        { 0xFFFF0000, 0xFFFF0000 },
+        { 0x00000000, 0xFFFFFFFF }
+    };
+    unsigned uTruthRes[2];
+    assert( pGate->nInputs <= 6 );
+    Mio_DeriveTruthTable( pGate, uTruths6, pGate->nInputs, 6, uTruthRes );
+    return *((word *)uTruthRes);
 }
 
+#if 0
+
 /**Function*************************************************************
 
   Synopsis    [Recursively derives the truth table of the gate.]
@@ -383,6 +403,67 @@ void Mio_DeriveTruthTable_rec( DdNode * bFunc, unsigned uTruthsIn[][2], unsigned
 
 /**Function*************************************************************
 
+  Synopsis    [Derives the truth table of the gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mio_DeriveTruthTable( Mio_Gate_t * pGate, unsigned uTruthsIn[][2], int nSigns, int nInputs, unsigned uTruthRes[] )
+{
+    Mio_DeriveTruthTable_rec( pGate->bFunc, uTruthsIn, uTruthRes );
+}
+
+#endif
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table of the gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mio_DeriveTruthTable( Mio_Gate_t * pGate, unsigned uTruthsIn[][2], int nSigns, int nInputs, unsigned uTruthRes[] )
+{
+    word uRes, uFanins[6];
+    int i;
+    assert( pGate->nInputs == nSigns );
+    for ( i = 0; i < nSigns; i++ )
+        uFanins[i] = (((word)uTruthsIn[i][1]) << 32) | (word)uTruthsIn[i][0];
+    uRes = Exp_Truth6( nSigns, pGate->vExpr, (word *)uFanins );
+    uTruthRes[0] = uRes & 0xFFFFFFFF;
+    uTruthRes[1] = uRes >> 32;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the number of variables in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mio_SopGetVarNum( char * pSop )
+{
+    char * pCur;
+    for ( pCur = pSop; *pCur != '\n'; pCur++ )
+        if ( *pCur == 0 )
+            return -1;
+    return pCur - pSop - 2;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives the truth table of the root of the gate.]
 
   Description [Given the truth tables of the leaves of the gate,
@@ -403,7 +484,7 @@ void Mio_DeriveTruthTable2( Mio_Gate_t * pGate, unsigned uTruthsIn[][2], int nTr
     assert( pGate->nInputs == nTruths );
     assert( nInputs < 7 );
 
-    nFanins = Abc_SopGetVarNum( pGate->pSop );
+    nFanins = Mio_SopGetVarNum( pGate->pSop );
     assert( nFanins == nInputs );
 
     // clean the resulting truth table
@@ -411,8 +492,8 @@ void Mio_DeriveTruthTable2( Mio_Gate_t * pGate, unsigned uTruthsIn[][2], int nTr
     uTruthRes[1] = 0;
     if ( nInputs < 6 )
     {
-//        for ( c = 0; *(pCube = pGate->pSop + c * (nFanins + 3)); c++ )
-        Abc_SopForEachCube( pGate->pSop, nFanins, pCube )
+//        Abc_SopForEachCube( pGate->pSop, nFanins, pCube )
+        for ( pCube = pGate->pSop; *pCube; pCube += (nFanins) + 3 )
         {
             // add the clause
             uSignCube[0] = MIO_FULL;
@@ -430,8 +511,8 @@ void Mio_DeriveTruthTable2( Mio_Gate_t * pGate, unsigned uTruthsIn[][2], int nTr
     else
     {
         // consider the case when two unsigneds should be used
-//        for ( c = 0; *(pCube = pGate->pSop + c * (nFanins + 3)); c++ )
-        Abc_SopForEachCube( pGate->pSop, nFanins, pCube )
+//        Abc_SopForEachCube( pGate->pSop, nFanins, pCube )
+        for ( pCube = pGate->pSop; *pCube; pCube += (nFanins) + 3 )
         {
             uSignCube[0] = MIO_FULL;
             uSignCube[1] = MIO_FULL;
diff --git a/src/map/mio/module.make b/src/map/mio/module.make
index 26a4561c..30870576 100644
--- a/src/map/mio/module.make
+++ b/src/map/mio/module.make
@@ -1,5 +1,7 @@
 SRC +=  src/map/mio/mio.c \
     src/map/mio/mioApi.c \
     src/map/mio/mioFunc.c \
+    src/map/mio/mioParse.c \
     src/map/mio/mioRead.c \
+    src/map/mio/mioSop.c \
     src/map/mio/mioUtils.c
diff --git a/src/map/super/super.c b/src/map/super/super.c
index 6483547e..2cc52a44 100644
--- a/src/map/super/super.c
+++ b/src/map/super/super.c
@@ -260,7 +260,7 @@ int Super_CommandSupergates( Abc_Frame_t * pAbc, int argc, char **argv )
     fclose( pFile );
 
     // set the new network
-    pLib = Mio_LibraryRead( pAbc, FileName, ExcludeFile, fVerbose );
+    pLib = Mio_LibraryRead( FileName, ExcludeFile, fVerbose );
     if ( pLib == NULL )
     {
         fprintf( pErr, "Reading library has failed.\n" );