Renaming Cba into Bac.

12 files changed, 695 insertions, 2069 deletions

diff --git a/src/base/cba/cba.c b/src/base/cba/cba.c
index d4369533..87a5b5cd 100644
--- a/src/base/cba/cba.c
+++ b/src/base/cba/cba.c
@@ -12,7 +12,7 @@
   
   Affiliation [UC Berkeley]
 
-  Date        [Ver. 1.0. Started - November 29, 2014.]
+  Date        [Ver. 1.0. Started - July 21, 2015.]
 
   Revision    [$Id: cba.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
 
diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index 6d4262fc..20b4a7b1 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -12,7 +12,7 @@
   
   Affiliation [UC Berkeley]
 
-  Date        [Ver. 1.0. Started - November 29, 2014.]
+  Date        [Ver. 1.0. Started - July 21, 2015.]
 
   Revision    [$Id: cba.h,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
 
@@ -44,14 +44,16 @@ typedef enum {
     CBA_OBJ_NONE = 0,  // 0:  unused
     CBA_OBJ_PI,        // 1:  input
     CBA_OBJ_PO,        // 2:  output
-    CBA_OBJ_BI,        // 3:  box input
-    CBA_OBJ_BO,        // 4:  box output
-    CBA_OBJ_BOX,       // 5:  box
-
-    CBA_BOX_CF,   
-    CBA_BOX_CT,   
-    CBA_BOX_CX,   
-    CBA_BOX_CZ,   
+    CBA_OBJ_BOX,       // 3:  box
+
+    CBA_BOX_SLICE,  
+    CBA_BOX_CONCAT,  
+
+    CBA_BOX_CF,  
+    CBA_BOX_CT,  
+    CBA_BOX_CX,  
+    CBA_BOX_CZ,  
+
     CBA_BOX_BUF,  
     CBA_BOX_INV,  
     CBA_BOX_AND,  
@@ -93,7 +95,7 @@ typedef enum {
     CBA_BOX_DIV,
     CBA_BOX_MOD,
     CBA_BOX_REM,
-    CBA_BOX_POW,
+    CBA_OBJ_POW,
     CBA_BOX_MIN,
     CBA_BOX_ABS,
 
@@ -125,18 +127,10 @@ typedef enum {
     CBA_BOX_DFF,
     CBA_BOX_DFFRS,
 
-    CBA_BOX_UNKNOWN   // 67
+    CBA_BOX_LAST   // 67
 } Cba_ObjType_t; 
 
 
-// name types
-typedef enum { 
-    CBA_NAME_BIN = 0,        // 0:  binary variable
-    CBA_NAME_WORD,           // 1:  first bit of word-level variable
-    CBA_NAME_INFO,           // 2:  first bit of special variable
-    CBA_NAME_INDEX,          // 3:  index of word-level variable
-} Cba_NameType_t; 
-
 
 typedef struct Cba_Ntk_t_ Cba_Ntk_t;
 typedef struct Cba_Man_t_ Cba_Man_t;
@@ -145,26 +139,40 @@ typedef struct Cba_Man_t_ Cba_Man_t;
 struct Cba_Ntk_t_
 {
     Cba_Man_t *  pDesign;  // design
-    int          NameId;   // name ID
+    int          Id;       // network ID
+    int          NameId;   // name ID 
     int          iCopy;    // copy module
-    int          iBoxNtk;  // instance network ID
-    int          iBoxObj;  // instance object ID
-    int          Count;    // object counter
     int          Mark;     // visit mark 
     // interface
     Vec_Int_t    vInputs;  // inputs 
     Vec_Int_t    vOutputs; // outputs
-    Vec_Int_t    vInfo;    // input/output/wire info
-    // object attributes
-    Vec_Str_t    vType;    // types     
-    Vec_Int_t    vFanin;   // fanin
-    Vec_Int_t    vIndex;   // index
-    Vec_Int_t    vName;    // original NameId or InstId
-    Vec_Int_t    vFanout;  // fanout
-    Vec_Int_t    vCopy;    // copy
+    Vec_Int_t    vOrder;   // order
+    // stucture
+    Vec_Str_t    vObjType; // type     
+    Vec_Int_t    vObjFin0; // fanins
+    Vec_Int_t    vObjFon0; // outputs
+    Vec_Int_t    vFinFon;  // fons
+    Vec_Int_t    vFonObj;  // object
+    // optional
+    Vec_Int_t    vObjCopy; // copy
+    Vec_Int_t    vObjFunc; // function
+    Vec_Int_t    vObjName; // name
+    Vec_Int_t    vObjAttr; // attribute offset
+    Vec_Int_t    vAttrSto; // attribute storage
+    Vec_Int_t    vFonCopy; // copy
+    Vec_Int_t    vFonName; // name
+    Vec_Int_t    vFonRange;// range
+    Vec_Int_t    vFonLeft; // left
+    Vec_Int_t    vFonRight;// right
+    Vec_Int_t    vFonPrev; // fanout: prev fon
+    Vec_Int_t    vFonNext; // fanout: next fon
+    Vec_Int_t    vFinFon0; // fanout: first fon
+    Vec_Int_t    vFinObj;  // object
+    Vec_Int_t    vNtkObjs; // instances
     // other
-    Vec_Int_t    vArray;
-    Vec_Int_t    vArray2;
+    Vec_Ptr_t *  vOther;   // various data
+    Vec_Int_t    vArray0;
+    Vec_Int_t    vArray1;
 };
 
 // design
@@ -177,158 +185,169 @@ struct Cba_Man_t_
     Abc_Nam_t *  pMods;    // module name manager
     // internal data
     int          iRoot;    // root network
-    int          nNtks;    // number of current networks
-    Cba_Ntk_t *  pNtks;    // networks
+    Vec_Ptr_t    vNtks;    // networks
     // user data
     Vec_Str_t *  vOut;     
     Vec_Str_t *  vOut2;     
-    Vec_Int_t    vBuf2RootNtk;
-    Vec_Int_t    vBuf2RootObj;
-    Vec_Int_t    vBuf2LeafNtk;
-    Vec_Int_t    vBuf2LeafObj;
-    void *       pMioLib;
-    void **      ppGraphs;
-    int          ElemGates[4];
-    char *       pPrimNames[CBA_BOX_UNKNOWN];
-    char *       pPrimSymbs[CBA_BOX_UNKNOWN];
 };
 
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
 static inline char *         Cba_ManName( Cba_Man_t * p )                    { return p->pName;                                                                            }
 static inline char *         Cba_ManSpec( Cba_Man_t * p )                    { return p->pSpec;                                                                            }
-static inline int            Cba_ManNtkNum( Cba_Man_t * p )                  { return p->nNtks;                                                                            }
-static inline int            Cba_ManPrimNum( Cba_Man_t * p )                 { return Abc_NamObjNumMax(p->pMods) - Cba_ManNtkNum(p);                                       }
+static inline int            Cba_ManNtkNum( Cba_Man_t * p )                  { return Vec_PtrSize(&p->vNtks)-1;                                                            }
 static inline int            Cba_ManNtkIsOk( Cba_Man_t * p, int i )          { return i > 0 && i <= Cba_ManNtkNum(p);                                                      }
-static inline Cba_Ntk_t *    Cba_ManNtk( Cba_Man_t * p, int i )              { return Cba_ManNtkIsOk(p, i) ? p->pNtks + i : NULL;                                          }
+static inline Cba_Ntk_t *    Cba_ManNtk( Cba_Man_t * p, int i )              { return Cba_ManNtkIsOk(p, i) ? (Cba_Ntk_t *)Vec_PtrEntry(&p->vNtks, i) : NULL;               }
 static inline int            Cba_ManNtkFindId( Cba_Man_t * p, char * pName ) { return Abc_NamStrFind(p->pMods, pName);                                                     }
 static inline Cba_Ntk_t *    Cba_ManNtkFind( Cba_Man_t * p, char * pName )   { return Cba_ManNtk( p, Cba_ManNtkFindId(p, pName) );                                         }
 static inline Cba_Ntk_t *    Cba_ManRoot( Cba_Man_t * p )                    { return Cba_ManNtk(p, p->iRoot);                                                             }
 static inline char *         Cba_ManStr( Cba_Man_t * p, int i )              { return Abc_NamStr(p->pStrs, i);                                                             }
 static inline int            Cba_ManStrId( Cba_Man_t * p, char * pStr )      { return Abc_NamStrFind(p->pStrs, pStr);                                                      }
-static inline char *         Cba_ManPrimName( Cba_Man_t * p, Cba_ObjType_t Type ) { return p->pPrimNames[Type];                                                            }
-static inline char *         Cba_ManPrimSymb( Cba_Man_t * p, Cba_ObjType_t Type ) { return p->pPrimSymbs[Type];                                                            }
+static inline int            Cba_ManNewStrId( Cba_Man_t * p, char * pPref, int n, char * pSuff ) { char pStr[100]; sprintf(pStr, "%s%d%s", pPref?pPref:"", n, pSuff?pSuff:""); return Abc_NamStrFindOrAdd(p->pStrs, pStr, NULL); }
+static inline int            Cba_ManNameIdMax( Cba_Man_t * p )               { return Abc_NamObjNumMax(p->pStrs) + 1;                                                      }
 
-static inline int            Cba_NtkId( Cba_Ntk_t * p )                      { int i = p - p->pDesign->pNtks; assert(Cba_ManNtkIsOk(p->pDesign, i)); return i;             }
 static inline Cba_Man_t *    Cba_NtkMan( Cba_Ntk_t * p )                     { return p->pDesign;                                                                          }
-static inline int            Cba_NtkNameId( Cba_Ntk_t * p )                  { return p->NameId;                                                                           }
-static inline char *         Cba_NtkName( Cba_Ntk_t * p )                    { return Cba_ManStr(p->pDesign, Cba_NtkNameId(p));                                            }
+static inline Cba_Ntk_t *    Cba_NtkNtk( Cba_Ntk_t * p, int i )              { return Cba_ManNtk(p->pDesign, i);                                                           }
+static inline int            Cba_NtkId( Cba_Ntk_t * p )                      { return p->Id;                                                                               }
+static inline int            Cba_NtkPi( Cba_Ntk_t * p, int i )               { return Vec_IntEntry(&p->vInputs, i);                                                        }
+static inline int            Cba_NtkPo( Cba_Ntk_t * p, int i )               { return Vec_IntEntry(&p->vOutputs, i);                                                       }
+static inline char *         Cba_NtkStr( Cba_Ntk_t * p, int i )              { return Cba_ManStr(p->pDesign, i);                                                           }
+static inline char *         Cba_NtkName( Cba_Ntk_t * p )                    { return Cba_NtkStr(p, p->NameId);                                                            }
 static inline int            Cba_NtkCopy( Cba_Ntk_t * p )                    { return p->iCopy;                                                                            }
 static inline Cba_Ntk_t *    Cba_NtkCopyNtk(Cba_Man_t * pNew, Cba_Ntk_t * p) { return Cba_ManNtk(pNew, Cba_NtkCopy(p));                                                    }
-static inline void           Cba_NtkSetCopy( Cba_Ntk_t * p, int i )          { assert(p->iCopy == -1); p->iCopy = i;                                                       }
+static inline void           Cba_NtkSetCopy( Cba_Ntk_t * p, int i )          { assert(p->iCopy == 0); p->iCopy = i;                                                        }
 
-static inline int            Cba_NtkObjNum( Cba_Ntk_t * p )                  { return Vec_StrSize(&p->vType);                                                              }
-static inline int            Cba_NtkObjNumAlloc( Cba_Ntk_t * p )             { return Vec_StrCap(&p->vType);                                                               }
 static inline int            Cba_NtkPiNum( Cba_Ntk_t * p )                   { return Vec_IntSize(&p->vInputs);                                                            }
 static inline int            Cba_NtkPoNum( Cba_Ntk_t * p )                   { return Vec_IntSize(&p->vOutputs);                                                           }
 static inline int            Cba_NtkPioNum( Cba_Ntk_t * p )                  { return Cba_NtkPiNum(p) + Cba_NtkPoNum(p);                                                   }
 static inline int            Cba_NtkPiNumAlloc( Cba_Ntk_t * p )              { return Vec_IntCap(&p->vInputs);                                                             }
 static inline int            Cba_NtkPoNumAlloc( Cba_Ntk_t * p )              { return Vec_IntCap(&p->vOutputs);                                                            }
-static inline int            Cba_NtkBiNum( Cba_Ntk_t * p )                   { return Vec_StrCountEntryLit(&p->vType, (char)CBA_OBJ_BI);                                   }
-static inline int            Cba_NtkBoNum( Cba_Ntk_t * p )                   { return Vec_StrCountEntryLit(&p->vType, (char)CBA_OBJ_BO);                                   }
-static inline int            Cba_NtkCiNum( Cba_Ntk_t * p )                   { return Cba_NtkPiNum(p) + Cba_NtkBoNum(p);                                                   }
-static inline int            Cba_NtkCoNum( Cba_Ntk_t * p )                   { return Cba_NtkPoNum(p) + Cba_NtkBiNum(p);                                                   }
-static inline int            Cba_NtkBoxNum( Cba_Ntk_t * p )                  { return Cba_NtkObjNum(p) - Vec_StrCountSmallerLit(&p->vType, (char)CBA_OBJ_BOX);             }
-static inline int            Cba_NtkPrimNum( Cba_Ntk_t * p )                 { return Vec_StrCountLargerLit(&p->vType, (char)CBA_OBJ_BOX);                                 }
-static inline int            Cba_NtkUserNum( Cba_Ntk_t * p )                 { return Vec_StrCountEntryLit(&p->vType, (char)CBA_OBJ_BOX);                                  }
- 
-static inline int            Cba_NtkPi( Cba_Ntk_t * p, int i )               { return Vec_IntEntry(&p->vInputs, i);                                                        }
-static inline int            Cba_NtkPo( Cba_Ntk_t * p, int i )               { return Vec_IntEntry(&p->vOutputs, i);                                                       }
-static inline char *         Cba_NtkStr( Cba_Ntk_t * p, int i )              { return Cba_ManStr(p->pDesign, i);                                                           }
-static inline Cba_Ntk_t *    Cba_NtkHostNtk( Cba_Ntk_t * p )                 { return p->iBoxNtk > 0 ? Cba_ManNtk(p->pDesign, p->iBoxNtk) : NULL;                          }
-static inline int            Cba_NtkHostObj( Cba_Ntk_t * p )                 { return p->iBoxObj;                                                                          }
-static inline void           Cba_NtkSetHost( Cba_Ntk_t * p, int n, int i )   { assert(p->iBoxNtk == -1); p->iBoxNtk = n; p->iBoxObj = i;                                   }
-
-static inline int            Cba_InfoRange( int Beg, int End )               { return End > Beg ? End - Beg + 1 : Beg - End + 1;                                           }
-static inline int            Cba_NtkInfoNum( Cba_Ntk_t * p )                 { return Vec_IntSize(&p->vInfo)/3;                                                            }
-static inline int            Cba_NtkInfoNumAlloc( Cba_Ntk_t * p )            { return Vec_IntCap(&p->vInfo)/3;                                                             }
-static inline int            Cba_NtkInfoType( Cba_Ntk_t * p, int i )         { return Abc_Lit2Att2(Vec_IntEntry(&p->vInfo, 3*i));                                          }
-static inline int            Cba_NtkInfoName( Cba_Ntk_t * p, int i )         { return Abc_Lit2Var2(Vec_IntEntry(&p->vInfo, 3*i));                                          }
-static inline int            Cba_NtkInfoBeg( Cba_Ntk_t * p, int i )          { return Vec_IntEntry(&p->vInfo, 3*i+1);                                                      }
-static inline int            Cba_NtkInfoEnd( Cba_Ntk_t * p, int i )          { return Vec_IntEntry(&p->vInfo, 3*i+2);                                                      }
-static inline int            Cba_NtkInfoRange( Cba_Ntk_t * p, int i )        { int* a = Vec_IntEntryP(&p->vInfo, 3*i); return a[1]>=0 ? Cba_InfoRange( a[1], a[2] ) : 1;   }
-static inline int            Cba_NtkInfoIndex( Cba_Ntk_t * p, int i, int j ) { int* a = Vec_IntEntryP(&p->vInfo, 3*i); assert(a[1]>=0); return a[1]<a[2] ? a[1]+j : a[1]-j;}
-static inline void           Cba_NtkAddInfo( Cba_Ntk_t * p,int i,int b,int e){ Vec_IntPush(&p->vInfo, i); Vec_IntPushTwo(&p->vInfo, b, e);                                 }
-static inline void           Cba_NtkSetInfoName( Cba_Ntk_t * p, int i, int n){ Vec_IntWriteEntry( &p->vInfo, 3*i, n );                                                     }
-
-static inline void           Cba_NtkStartNames( Cba_Ntk_t * p )              { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vName,   Cba_NtkObjNumAlloc(p),  0);         }
-static inline void           Cba_NtkStartFanouts( Cba_Ntk_t * p )            { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vFanout, Cba_NtkObjNumAlloc(p),  0);         }
-static inline void           Cba_NtkStartCopies( Cba_Ntk_t * p )             { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vCopy,   Cba_NtkObjNumAlloc(p), -1);         }
-static inline void           Cba_NtkFreeNames( Cba_Ntk_t * p )               { Vec_IntErase(&p->vName);                                                                    }
-static inline void           Cba_NtkFreeFanouts( Cba_Ntk_t * p )             { Vec_IntErase(&p->vFanout);                                                                  }
-static inline void           Cba_NtkFreeCopies( Cba_Ntk_t * p )              { Vec_IntErase(&p->vCopy);                                                                    }
-static inline int            Cba_NtkHasNames( Cba_Ntk_t * p )                { return p->vName.pArray != NULL;                                                             }
-static inline int            Cba_NtkHasFanouts( Cba_Ntk_t * p )              { return p->vFanout.pArray != NULL;                                                           }
-static inline int            Cba_NtkHasCopies( Cba_Ntk_t * p )               { return p->vCopy.pArray != NULL;                                                             }
-
-static inline int            Cba_TypeIsBox( Cba_ObjType_t Type )             { return Type >= CBA_OBJ_BOX && Type < CBA_BOX_UNKNOWN;                                       }
-static inline Cba_NameType_t Cba_NameType( int n )                           { assert( n ); return (Cba_NameType_t)Abc_Lit2Att2( n );                                      }
-static inline int            Cba_CharIsDigit( char c )                       { return c >= '0' && c <= '9'; }
-
-static inline Cba_ObjType_t  Cba_ObjType( Cba_Ntk_t * p, int i )             { return (Cba_ObjType_t)Abc_Lit2Var((int)(unsigned char)Vec_StrEntry(&p->vType, i));          }
+static inline int            Cba_NtkObjNum( Cba_Ntk_t * p )                  { return Vec_StrSize(&p->vObjType)-1;                                                       }
+static inline int            Cba_NtkObjNumAlloc( Cba_Ntk_t * p )             { return Vec_StrCap(&p->vObjType)-1;                                                        }
+static inline int            Cba_NtkFinNum( Cba_Ntk_t * p )                  { return Vec_IntSize(&p->vFinFon)-1;                                                          }
+static inline int            Cba_NtkFinNumAlloc( Cba_Ntk_t * p )             { return Vec_IntCap(&p->vFinFon)-1;                                                           }
+static inline int            Cba_NtkFonNum( Cba_Ntk_t * p )                  { return Vec_IntSize(&p->vFonObj)-1;                                                          }
+static inline int            Cba_NtkFonNumAlloc( Cba_Ntk_t * p )             { return Vec_IntCap(&p->vFonObj)-1;                                                           }
+static inline int            Cba_NtkTypeNum( Cba_Ntk_t * p, int Type )       { return Vec_StrCountEntry(&p->vObjType, (char)Type);                                         }
+static inline int            Cba_NtkBoxNum( Cba_Ntk_t * p )                  { return Cba_NtkObjNum(p) - Cba_NtkPioNum(p);                                                 }
+static inline int            Cba_NtkBoxUserNum( Cba_Ntk_t * p )              { return Cba_NtkTypeNum(p, CBA_OBJ_BOX);                                                      }
+static inline int            Cba_NtkBoxPrimNum( Cba_Ntk_t * p )              { return Vec_StrCountLarger(&p->vObjType, (char)CBA_OBJ_BOX);                                 }
+
+static inline void           Cba_NtkStartObjCopies( Cba_Ntk_t * p )          { Vec_IntFill(&p->vObjCopy, Vec_StrCap(&p->vObjType), -1);        }
+static inline void           Cba_NtkStartObjFuncs( Cba_Ntk_t * p )           { Vec_IntFill(&p->vObjFunc, Vec_StrCap(&p->vObjType),  0);        }
+static inline void           Cba_NtkStartObjNames( Cba_Ntk_t * p )           { Vec_IntFill(&p->vObjName, Vec_StrCap(&p->vObjType),  0);        }
+static inline void           Cba_NtkStartObjAttrs( Cba_Ntk_t * p )           { Vec_IntFill(&p->vObjAttr, Vec_StrCap(&p->vObjType),  0);        }
+static inline void           Cba_NtkStartFonCopies( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonCopy, Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkStartFonNames( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonName, Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkStartFonRanges( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonRange,Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkStartFonLefts( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonLeft, Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkStartFonRights( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonRight,Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkStartFonPrevs( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonPrev, Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkStartFonNexts( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonNext, Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkStartFinFon0( Cba_Ntk_t * p )            { Vec_IntFill(&p->vFinFon0, Vec_IntCap(&p->vFinFon),   0);        }
+static inline void           Cba_NtkStartFinObjs( Cba_Ntk_t * p )            { Vec_IntFill(&p->vFinObj,  Vec_IntCap(&p->vFinFon),   0);        }
+
+static inline void           Cba_NtkFreeObjCopies( Cba_Ntk_t * p )           { Vec_IntErase(&p->vObjCopy);   }
+static inline void           Cba_NtkFreeObjFuncs( Cba_Ntk_t * p )            { Vec_IntErase(&p->vObjFunc);   }
+static inline void           Cba_NtkFreeObjNames( Cba_Ntk_t * p )            { Vec_IntErase(&p->vObjName);   }
+static inline void           Cba_NtkFreeObjAttrs( Cba_Ntk_t * p )            { Vec_IntErase(&p->vObjAttr);   }
+static inline void           Cba_NtkFreeFonCopies( Cba_Ntk_t * p )           { Vec_IntErase(&p->vFonCopy);   }
+static inline void           Cba_NtkFreeFonNames( Cba_Ntk_t * p )            { Vec_IntErase(&p->vFonName);   }
+static inline void           Cba_NtkFreeFonRanges( Cba_Ntk_t * p )           { Vec_IntErase(&p->vFonRange);  }
+static inline void           Cba_NtkFreeFonLefts( Cba_Ntk_t * p )            { Vec_IntErase(&p->vFonLeft);   }
+static inline void           Cba_NtkFreeFonRights( Cba_Ntk_t * p )           { Vec_IntErase(&p->vFonRight);  }
+static inline void           Cba_NtkFreeFonPrevs( Cba_Ntk_t * p )            { Vec_IntErase(&p->vFonPrev);   }
+static inline void           Cba_NtkFreeFonNexts( Cba_Ntk_t * p )            { Vec_IntErase(&p->vFonNext);   }
+static inline void           Cba_NtkFreeFinFon0( Cba_Ntk_t * p )             { Vec_IntErase(&p->vFinFon0);   }
+static inline void           Cba_NtkFreeFinObjs( Cba_Ntk_t * p )             { Vec_IntErase(&p->vFinObj);    }
+
+static inline int            Cba_NtkHasObjCopies( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vObjCopy) > 0; }
+static inline int            Cba_NtkHasObjFuncs( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vObjFunc) > 0; }
+static inline int            Cba_NtkHasObjNames( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vObjName) > 0; }
+static inline int            Cba_NtkHasObjAttrs( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vObjAttr) > 0; }
+static inline int            Cba_NtkHasFonCopies( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vFonCopy) > 0; }
+static inline int            Cba_NtkHasFonNames( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonName) > 0; }
+static inline int            Cba_NtkHasFonRanges( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vFonRange)> 0; }
+static inline int            Cba_NtkHasFonLefts( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonLeft) > 0; }
+static inline int            Cba_NtkHasFonRights( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vFonRight)> 0; }
+static inline int            Cba_NtkHasFonPrevs( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonPrev) > 0; }
+static inline int            Cba_NtkHasFonNexts( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonNext) > 0; }
+static inline int            Cba_NtkHasFinFon0( Cba_Ntk_t * p )              { return Vec_IntSize(&p->vFinFon0) > 0; }
+static inline int            Cba_NtkHasFinObjs( Cba_Ntk_t * p )              { return Vec_IntSize(&p->vFinObj)  > 0; }
+
+static inline void           Cba_NtkCleanObjCopies( Cba_Ntk_t * p )          { Vec_IntFill(&p->vObjCopy, Vec_StrSize(&p->vObjType), -1);                                   }
+static inline void           Cba_NtkCleanFonCopies( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonCopy, Vec_IntSize(&p->vFonObj),  -1);                                   }
+static inline void           Cba_NtkCleanFonNames( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonName, Vec_IntSize(&p->vFonObj),   0);                                   }
+
+static inline Cba_ObjType_t  Cba_ObjType( Cba_Ntk_t * p, int i )             { assert(i>0); return (Cba_ObjType_t)(int)(unsigned char)Vec_StrEntry(&p->vObjType, i);       }
+static inline void           Cba_ObjCleanType( Cba_Ntk_t * p, int i )        { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)CBA_OBJ_NONE );                      }
+static inline int            Cba_TypeIsBox( Cba_ObjType_t Type )             { return Type >= CBA_OBJ_BOX && Type < CBA_BOX_LAST;                                          }
+
 static inline int            Cba_ObjIsPi( Cba_Ntk_t * p, int i )             { return Cba_ObjType(p, i) == CBA_OBJ_PI;                                                     }
 static inline int            Cba_ObjIsPo( Cba_Ntk_t * p, int i )             { return Cba_ObjType(p, i) == CBA_OBJ_PO;                                                     }
 static inline int            Cba_ObjIsPio( Cba_Ntk_t * p, int i )            { return Cba_ObjIsPi(p, i) || Cba_ObjIsPo(p, i);                                              }
-static inline int            Cba_ObjIsBi( Cba_Ntk_t * p, int i )             { return Cba_ObjType(p, i) == CBA_OBJ_BI;                                                     }
-static inline int            Cba_ObjIsBo( Cba_Ntk_t * p, int i )             { return Cba_ObjType(p, i) == CBA_OBJ_BO;                                                     }
-static inline int            Cba_ObjIsBio( Cba_Ntk_t * p, int i )            { return Cba_ObjIsBi(p, i) || Cba_ObjIsBo(p, i);                                              }
 static inline int            Cba_ObjIsBox( Cba_Ntk_t * p, int i )            { return Cba_TypeIsBox(Cba_ObjType(p, i));                                                    }
 static inline int            Cba_ObjIsBoxUser( Cba_Ntk_t * p, int i )        { return Cba_ObjType(p, i) == CBA_OBJ_BOX;                                                    }
-static inline int            Cba_ObjIsBoxPrim( Cba_Ntk_t * p, int i )        { return Cba_ObjIsBox(p, i) && !Cba_ObjIsBoxUser(p, i);                                       }
+static inline int            Cba_ObjIsBoxPrim( Cba_Ntk_t * p, int i )        { return Cba_ObjType(p, i) >  CBA_OBJ_BOX && Cba_ObjType(p, i) < CBA_BOX_LAST;                }
 static inline int            Cba_ObjIsGate( Cba_Ntk_t * p, int i )           { return Cba_ObjType(p, i) == CBA_BOX_GATE;                                                   }
-static inline int            Cba_ObjIsCi( Cba_Ntk_t * p, int i )             { return Cba_ObjIsPi(p, i) || Cba_ObjIsBo(p, i);                                              }
-static inline int            Cba_ObjIsCo( Cba_Ntk_t * p, int i )             { return Cba_ObjIsPo(p, i) || Cba_ObjIsBi(p, i);                                              }
-static inline int            Cba_ObjIsCio( Cba_Ntk_t * p, int i )            { return Cba_ObjType(p, i) < CBA_OBJ_BOX;                                                     }
-static inline int            Cba_ObjIsConst( Cba_Ntk_t * p, int i )          { return Cba_ObjType(p, i) >= CBA_BOX_CF && Cba_ObjType(p, i) <= CBA_BOX_CZ;                  }
-static inline int            Cba_ObjIsConstBin( Cba_Ntk_t * p, int i )       { return Cba_ObjType(p, i) == CBA_BOX_CF || Cba_ObjType(p, i) == CBA_BOX_CT;                  }
-
-static inline int            Cba_ObjBit( Cba_Ntk_t * p, int i )              { assert(!Cba_ObjIsBox(p, i)); return Abc_LitIsCompl((int)Vec_StrEntry(&p->vType, i));        }
-static inline void           Cba_ObjSetBit( Cba_Ntk_t * p, int i )           { char *q = Vec_StrArray(&p->vType); assert(!Cba_ObjIsBox(p, i)); q[i] = (char)Abc_LitNot((int)q[i]); }
-static inline int            Cba_ObjFanin( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsCo(p, i)); return Vec_IntEntry(&p->vFanin, i);                              }
-static inline int            Cba_ObjIndex( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsCio(p, i)); return Vec_IntEntry(&p->vIndex, i);                             }
-static inline int            Cba_ObjNameInt( Cba_Ntk_t * p, int i )          { assert(!Cba_ObjIsCo(p, i)); return Vec_IntEntry(&p->vName, i);                              }
-static inline int            Cba_ObjName( Cba_Ntk_t * p, int i )             { return Cba_ObjIsCo(p, i) ? Cba_ObjNameInt(p, Cba_ObjFanin(p,i)) : Cba_ObjNameInt(p, i);     }
-static inline Cba_NameType_t Cba_ObjNameType( Cba_Ntk_t * p, int i )         { return Cba_NameType( Cba_ObjName(p, i) );                                                   }
-static inline int            Cba_ObjNameId( Cba_Ntk_t * p, int i )           { return Abc_Lit2Var2( Cba_ObjName(p, i) );                                                   }
-static inline char *         Cba_ObjNameStr( Cba_Ntk_t * p, int i )          { assert(Cba_ObjNameType(p, i) <= CBA_NAME_WORD); return Cba_NtkStr(p, Cba_ObjNameId(p, i));  }
-static inline int            Cba_ObjCopy( Cba_Ntk_t * p, int i )             { return Vec_IntEntry(&p->vCopy, i);                                                          }
-static inline int            Cba_ObjFanout( Cba_Ntk_t * p, int i )           { assert(Cba_ObjIsCi(p, i)); return Vec_IntEntry(&p->vFanout, i);                             }
-static inline int            Cba_ObjNextFanout( Cba_Ntk_t * p, int i )       { assert(Cba_ObjIsCo(p, i)); return Vec_IntEntry(&p->vFanout, i);                             }
-static inline void           Cba_ObjSetFanout( Cba_Ntk_t * p, int i, int x ) { assert(Cba_ObjIsCi(p, i)); Vec_IntSetEntry(&p->vFanout, i, x);                              }
-static inline void           Cba_ObjSetNextFanout( Cba_Ntk_t * p,int i,int x){ assert(Cba_ObjIsCo(p, i)); Vec_IntSetEntry(&p->vFanout, i, x);                              }
-static inline void           Cba_ObjCleanFanin( Cba_Ntk_t * p, int i )       { assert(Cba_ObjFanin(p, i) >= 0 && Cba_ObjIsCo(p, i)); Vec_IntSetEntry( &p->vFanin, i, -1);  }
-static inline void           Cba_ObjSetFanin( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjFanin(p, i) == -1 && Cba_ObjIsCo(p, i)); Vec_IntSetEntry( &p->vFanin, i, x);  }
-static inline void           Cba_ObjSetIndex( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjIndex(p, i) == -1); Vec_IntSetEntry( &p->vIndex, i, x );                      }
-static inline void           Cba_ObjSetName( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjName(p, i) == 0 && !Cba_ObjIsCo(p, i)); Vec_IntSetEntry( &p->vName, i, x );   }
-static inline void           Cba_ObjSetCopy( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjCopy(p, i) == -1);  Vec_IntSetEntry( &p->vCopy,  i, x );                      }
-static inline int            Cba_ObjGetConst( Cba_Ntk_t * p, int i )         { assert(Cba_ObjIsCi(p, i)); return Cba_ObjIsBo(p, i) && Cba_ObjIsConst(p, i-1) ? Cba_ObjType(p, i-1) : 0;              }
-
-static inline int            Cba_BoxBiNum( Cba_Ntk_t * p, int i )            { int s = i-1; assert(Cba_ObjIsBox(p, i)); while (--i >= 0               && Cba_ObjIsBi(p, i)) {} return s - i;  }
-static inline int            Cba_BoxBoNum( Cba_Ntk_t * p, int i )            { int s = i+1; assert(Cba_ObjIsBox(p, i)); while (++i < Cba_NtkObjNum(p) && Cba_ObjIsBo(p, i)) {} return i - s;  }
-static inline int            Cba_BoxSize( Cba_Ntk_t * p, int i )             { return 1 + Cba_BoxBiNum(p, i) + Cba_BoxBoNum(p, i);                                         }
-static inline int            Cba_BoxBi( Cba_Ntk_t * p, int b, int i )        { assert(Cba_ObjIsBox(p, b)); return b - 1 - i;                                               }
-static inline int            Cba_BoxBo( Cba_Ntk_t * p, int b, int i )        { assert(Cba_ObjIsBox(p, b)); return b + 1 + i;                                               }
-//static inline int            Cba_BoxBiBox( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsBi(p, i)); return i + 1 + Cba_ObjIndex(p, i);                               }
-static inline int            Cba_BoxBoBox( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsBo(p, i)); return i - 1 - Cba_ObjIndex(p, i);                               }
-static inline int            Cba_BoxFanin( Cba_Ntk_t * p, int b, int i )     { return Cba_ObjFanin(p, Cba_BoxBi(p, b, i));                                                 }
-static inline int            Cba_BoxFaninBox( Cba_Ntk_t * p, int b, int i )  { return Cba_BoxBoBox(p, Cba_BoxFanin(p, b, i));                                              }
-static inline int            Cba_BoxBiRange( Cba_Ntk_t * p, int i )          { int s = i; assert(Cba_ObjIsBi(p, i) && !Cba_ObjBit(p, i)); while (--i >= 0               && Cba_ObjIsBi(p, i) && Cba_ObjBit(p, i)) {} return s - i;  }
-static inline int            Cba_BoxBoRange( Cba_Ntk_t * p, int i )          { int s = i; assert(Cba_ObjIsBo(p, i) && !Cba_ObjBit(p, i)); while (++i < Cba_NtkObjNum(p) && Cba_ObjIsBo(p, i) && Cba_ObjBit(p, i)) {} return i - s;  }
-static inline int            Cba_ObjPiRange( Cba_Ntk_t * p, int i )          { int s = i; assert(Cba_ObjIsPi(p, i) && !Cba_ObjBit(p, i)); while (++i < Cba_NtkObjNum(p) && Cba_ObjIsPi(p, i) && Cba_ObjBit(p, i)) {} return i - s;  }
-
-static inline int            Cba_BoxNtkId( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsBox(p, i)); return Vec_IntEntry(&p->vFanin, i);                             }
-static inline void           Cba_BoxSetNtkId( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjIsBox(p, i)&&Cba_ManNtkIsOk(p->pDesign, x));Vec_IntSetEntry(&p->vFanin, i, x);}
-//static inline int            Cba_BoxBiNtkId( Cba_Ntk_t * p, int i )          { assert(Cba_ObjIsBi(p, i)); return Cba_BoxNtkId(p, Cba_BoxBiBox(p, i));                      }
-static inline int            Cba_BoxBoNtkId( Cba_Ntk_t * p, int i )          { assert(Cba_ObjIsBo(p, i)); return Cba_BoxNtkId(p, Cba_BoxBoBox(p, i));                      }
-static inline Cba_Ntk_t *    Cba_BoxNtk( Cba_Ntk_t * p, int i )              { return Cba_ManNtk( p->pDesign, Cba_BoxNtkId(p, i) );                                        }
-//static inline Cba_Ntk_t *    Cba_BoxBiNtk( Cba_Ntk_t * p, int i )            { return Cba_ManNtk( p->pDesign, Cba_BoxBiNtkId(p, i) );                                      }
-static inline Cba_Ntk_t *    Cba_BoxBoNtk( Cba_Ntk_t * p, int i )            { return Cba_ManNtk( p->pDesign, Cba_BoxBoNtkId(p, i) );                                      }
-static inline char *         Cba_BoxNtkName( Cba_Ntk_t * p, int i )          { return Abc_NamStr( p->pDesign->pMods, Cba_BoxNtkId(p, i) );                                 }
 
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
+static inline int            Cba_ObjFin0( Cba_Ntk_t * p, int i )             { assert(i>0); return Vec_IntEntry(&p->vObjFin0, i);                                          }
+static inline int            Cba_ObjFon0( Cba_Ntk_t * p, int i )             { assert(i>0); return Vec_IntEntry(&p->vObjFon0, i);                                          }
+static inline int            Cba_ObjFin( Cba_Ntk_t * p, int i, int k )       { assert(i>0); return Cba_ObjFin0(p, i) + k;                                                  }
+static inline int            Cba_ObjFon( Cba_Ntk_t * p, int i, int k )       { assert(i>0); return Cba_ObjFon0(p, i) + k;                                                  }
+static inline int            Cba_ObjFinNum( Cba_Ntk_t * p, int i )           { assert(i>0); return Cba_ObjFin0(p, i+1) - Cba_ObjFin0(p, i);                                }
+static inline int            Cba_ObjFonNum( Cba_Ntk_t * p, int i )           { assert(i>0); return Cba_ObjFon0(p, i+1) - Cba_ObjFon0(p, i);                                }
+
+static inline int            Cba_ObjCopy( Cba_Ntk_t * p, int i )             { assert(i>0); return Vec_IntGetEntryFull(&p->vObjCopy, i);                                   }
+static inline int            Cba_ObjFunc( Cba_Ntk_t * p, int i )             { assert(i>0); return Vec_IntGetEntry(&p->vObjFunc, i);                                       }
+static inline int            Cba_ObjName( Cba_Ntk_t * p, int i )             { assert(i>0); return Vec_IntGetEntry(&p->vObjName, i);                                       }
+static inline char *         Cba_ObjNameStr( Cba_Ntk_t * p, int i )          { assert(i>0); return Cba_NtkStr(p, Cba_ObjName(p, i));                                       }
+static inline int            Cba_ObjAttr( Cba_Ntk_t * p, int i )             { assert(i>0); return Vec_IntGetEntry(&p->vObjAttr, i);                                       }
+
+static inline int *          Cba_ObjAttrs( Cba_Ntk_t * p, int i )            { assert(i>0); return Vec_IntGetEntryP(&p->vObjAttr, i);                                      }
+static inline int            Cba_ObjAttrSize( Cba_Ntk_t * p, int i )         { assert(i>0); return Vec_IntEntry(&p->vAttrSto, Vec_IntGetEntry(&p->vObjAttr, i));           }
+static inline int *          Cba_ObjAttrArray( Cba_Ntk_t * p, int i )        { assert(i>0); return Vec_IntEntryP(&p->vAttrSto, Vec_IntGetEntry(&p->vObjAttr, i)+1);        }
+
+static inline void           Cba_ObjSetCopy( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjCopy(p, i) == -1); Vec_IntSetEntry( &p->vObjCopy, i, x );                     }
+static inline void           Cba_ObjSetFunc( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjFunc(p, i) ==  0); Vec_IntSetEntry( &p->vObjFunc, i, x );                     }
+static inline void           Cba_ObjSetName( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjName(p, i) ==  0); Vec_IntSetEntry( &p->vObjName, i, x );                     }
+static inline void           Cba_ObjSetAttrs( Cba_Ntk_t * p, int i, int * a, int s )  { assert(Cba_ObjAttr(p, i) == 0); Vec_IntSetEntry(&p->vObjAttr, i, Vec_IntSize(&p->vAttrSto)); if (a) Vec_IntPushArray(&p->vAttrSto, a, s);  }
+
+static inline int            Cba_FinFon( Cba_Ntk_t * p, int f )              { assert(f>0); return Vec_IntEntry(&p->vFinFon, f);                                           }
+static inline int            Cba_ObjFinFon( Cba_Ntk_t * p, int i, int k )    { assert(i>0); return Cba_FinFon(p, Cba_ObjFin(p, i, k));                                     }
+static inline int *          Cba_ObjFinFons( Cba_Ntk_t * p, int i )          { assert(i>0); return Vec_IntEntryP(&p->vFinFon, Cba_ObjFin0(p, i));                          }
+
+static inline void           Cba_ObjSetFinFon( Cba_Ntk_t * p, int i, int k, int x ) { assert(i>0); assert(Cba_ObjFinFon(p, i, k)== 0); Vec_IntWriteEntry(&p->vFinFon, Cba_ObjFin(p, i, k), x); }
+static inline void           Cba_ObjCleanFinFon( Cba_Ntk_t * p, int i, int k)       { assert(i>0); assert(Cba_ObjFinFon(p, i, k) > 0); Vec_IntWriteEntry(&p->vFinFon, Cba_ObjFin(p, i, k), 0); }
+static inline void           Cba_ObjPatchFinFon( Cba_Ntk_t * p, int i, int k, int x){ assert(i>0); Cba_ObjCleanFinFon(p, i, k); Cba_ObjSetFinFon(p, i, k, x);                                  }
+
+static inline int            Cba_ObjNtkId( Cba_Ntk_t * p, int i )            { assert(i>0 && Cba_NtkHasObjFuncs(p)); return Cba_ObjIsBoxUser(p, i) ? Cba_ObjFunc(p, i) : 0;}
+static inline Cba_Ntk_t *    Cba_ObjNtk( Cba_Ntk_t * p, int i )              { assert(i>0); return Cba_NtkNtk(p, Cba_ObjNtkId(p, i));                                      }
+static inline int            Cba_ObjSetNtkId( Cba_Ntk_t * p, int i, int x )  { assert(i>0); assert(Cba_ObjIsBoxUser(p, i)); Cba_ObjSetFunc( p, i, x );                     }
+
+static inline int            Cba_FonIsReal( int f )                          { return f > 0;                             }
+static inline int            Cba_FonIsConst( int f )                         { return f < 0;                             }
+static inline int            Cba_FonConst( int f )                           { assert(Cba_FonIsConst(f)); return -f-1;   }
+static inline int            Cba_FonFromConst( int c )                       { assert(c >= 0); return -c-1;              }
+
+static inline int            Cba_FonObj( Cba_Ntk_t * p, int f )              { return Cba_FonIsReal(f) ? Vec_IntEntry(&p->vFonObj, f) : 0;                                 }
+static inline int            Cba_FonCopy( Cba_Ntk_t * p, int f )             { return Cba_FonIsReal(f) ? Vec_IntEntry( &p->vFonCopy, f ) : f;                              }
+static inline void           Cba_FonSetCopy( Cba_Ntk_t * p, int f, int x )   { assert(Cba_FonIsReal(f)); assert(Cba_FonCopy(p, f) == 0); Vec_IntWriteEntry(&p->vFonCopy, f, x); }
+static inline int            Cba_FonName( Cba_Ntk_t * p, int f )             { assert(Cba_FonIsReal(f)); return Vec_IntGetEntry( &p->vFonName, f );                        }
+static inline char *         Cba_FonNameStr( Cba_Ntk_t * p, int f )          { assert(Cba_FonIsReal(f)); return Cba_NtkStr(p, Cba_FonName(p, f));                          }
+static inline void           Cba_FonSetName( Cba_Ntk_t * p, int f, int x )   { assert(Cba_FonIsReal(f)); assert(Cba_FonName(p, f) == 0); Vec_IntSetEntry(&p->vFonName, f, x);   }
+static inline void           Cba_FonCleanName( Cba_Ntk_t * p, int f )        { assert(Cba_FonIsReal(f)); assert(Cba_FonName(p, f) != 0); Vec_IntSetEntry(&p->vFonName, f, 0);   }
+static inline void           Cba_FonPatchName( Cba_Ntk_t * p, int f, int x)  { assert(Cba_FonIsReal(f)); Cba_FonCleanName(p, f); Cba_FonSetName(p, f, x);                  }
+static inline int            Cba_FonIndex( Cba_Ntk_t * p, int f )            { assert(Cba_FonIsReal(f)); return f - Cba_ObjFon0( p, Cba_FonObj(p, f) );                    }
+static inline int            Cba_FonNtkId( Cba_Ntk_t * p, int f )            { assert(Cba_FonIsReal(f)); return Cba_ObjNtkId( p, Cba_FonObj(p, f) );                       }
+static inline Cba_Ntk_t *    Cba_FonNtk( Cba_Ntk_t * p, int f )              { assert(Cba_FonIsReal(f)); return Cba_ObjNtk( p, Cba_FonObj(p, f) );                         }
+
+static inline int            Cba_ObjFanin( Cba_Ntk_t * p, int i, int k )     { assert(i>0); return Cba_FonObj( p, Cba_ObjFinFon(p, i, k) );                                }
 
 ////////////////////////////////////////////////////////////////////////
-///                             ITERATORS                            ///
+///                          ITERATORS                               ///
 ////////////////////////////////////////////////////////////////////////
 
 #define Cba_ManForEachNtk( p, pNtk, i )                                   \
@@ -338,61 +357,41 @@ static inline char *         Cba_BoxNtkName( Cba_Ntk_t * p, int i )          { r
     for ( i = 0; (i < Cba_NtkPiNum(p))  && (((iObj) = Cba_NtkPi(p, i)), 1); i++ ) 
 #define Cba_NtkForEachPo( p, iObj, i )                                    \
     for ( i = 0; (i < Cba_NtkPoNum(p))  && (((iObj) = Cba_NtkPo(p, i)), 1); i++ ) 
-#define Cba_NtkForEachPoDriver( p, iObj, i )                              \
-    for ( i = 0; (i < Cba_NtkPoNum(p))  && (((iObj) = Cba_ObjFanin(p, Cba_NtkPo(p, i))), 1); i++ ) 
 
-#define Cba_NtkForEachPiMain( p, iObj, i )                                \
-    for ( i = 0; (i < Cba_NtkPiNum(p))  && (((iObj) = Cba_NtkPi(p, i)), 1); i++ )  if ( Cba_ObjBit(p, iObj) ) {} else
-#define Cba_NtkForEachPoMain( p, iObj, i )                                \
-    for ( i = 0; (i < Cba_NtkPoNum(p))  && (((iObj) = Cba_NtkPo(p, i)), 1); i++ )  if ( Cba_ObjBit(p, iObj) ) {} else
+#define Cba_NtkForEachPiFon( p, iObj, iFon, i )                           \
+    for ( i = 0; (i < Cba_NtkPiNum(p))  && (((iObj) = Cba_NtkPi(p, i)), 1)  && (((iFon) = Cba_ObjFon0(p, iObj)), 1); i++ ) 
+#define Cba_NtkForEachPoDriverFon( p, iObj, iFon, i )                     \
+    for ( i = 0; (i < Cba_NtkPoNum(p))  && (((iObj) = Cba_NtkPo(p, i)), 1)  && (((iFon) = Cba_ObjFinFon(p, iObj, 0)), 1); i++ ) 
+#define Cba_NtkForEachPoDriver( p, iObj, i )                              \
+    for ( i = 0; (i < Cba_NtkPoNum(p))  && (((iObj) = Cba_ObjFanin(p, Cba_NtkPo(p, i), 0)), 1); i++ ) 
 
-#define Cba_NtkForEachObj( p, i )  if ( !Cba_ObjType(p, i) ) {} else      \
-    for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) 
+#define Cba_NtkForEachObj( p, i )                                         \
+    for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Cba_ObjType(p, i) ) {} else   
 #define Cba_NtkForEachObjType( p, Type, i )                               \
-    for ( i = 0; (i < Cba_NtkObjNum(p))  && (((Type) = Cba_ObjType(p, i)), 1); i++ ) if ( !Type ) {} else
-
+    for ( i = 1; i < Vec_StrSize(&p->vObjType)  && (((Type) = Cba_ObjType(p, i)), 1); i++ ) if ( !Type ) {} else
 #define Cba_NtkForEachBox( p, i )                                         \
-    for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) if ( !Cba_ObjIsBox(p, i) ) {} else
+    for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Cba_ObjIsBox(p, i) ) {} else
 #define Cba_NtkForEachBoxUser( p, i )                                     \
-    for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) if ( !Cba_ObjIsBoxUser(p, i) ) {} else
+    for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Cba_ObjIsBoxUser(p, i) ) {} else
 #define Cba_NtkForEachBoxPrim( p, i )                                     \
-    for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) if ( !Cba_ObjIsBoxPrim(p, i) ) {} else
-
-#define Cba_NtkForEachCi( p, i )                                          \
-    for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) if ( !Cba_ObjIsCi(p, i) ) {} else
-#define Cba_NtkForEachCo( p, i )                                          \
-    for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) if ( !Cba_ObjIsCo(p, i) ) {} else
-#define Cba_NtkForEachCio( p, i )                                         \
-    for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) if ( !Cba_ObjIsCio(p, i) ){} else
-
-#define Cba_NtkForEachBi( p, i )                                          \
-    for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) if ( !Cba_ObjIsBi(p, i) ){} else
-#define Cba_NtkForEachBo( p, i )                                          \
-    for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) if ( !Cba_ObjIsBo(p, i) ){} else
-#define Cba_NtkForEachBio( p, i )                                         \
-    for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) if ( !Cba_ObjIsBio(p, i) ){} else
-
-#define Cba_BoxForEachBi( p, iBox, iTerm, i )                             \
-    for ( iTerm = iBox - 1, i = 0; iTerm >= 0 && Cba_ObjIsBi(p, iTerm); iTerm--, i++ )
-#define Cba_BoxForEachBo( p, iBox, iTerm, i )                             \
-    for ( iTerm = iBox + 1, i = 0; iTerm < Cba_NtkObjNum(p) && Cba_ObjIsBo(p, iTerm); iTerm++, i++ )
-#define Cba_BoxForEachBiReverse( p, iBox, iTerm, i )                      \
-    for ( i = Cba_BoxBiNum(p, iBox), iTerm = iBox - i--; Cba_ObjIsBi(p, iTerm); iTerm++, i-- )
-
-#define Cba_BoxForEachBiMain( p, iBox, iTerm, i )                         \
-    for ( iTerm = iBox - 1, i = 0; iTerm >= 0 && Cba_ObjIsBi(p, iTerm); iTerm--, i++ )                if ( Cba_ObjBit(p, iTerm) ) {} else
-#define Cba_BoxForEachBoMain( p, iBox, iTerm, i )                         \
-    for ( iTerm = iBox + 1, i = 0; iTerm < Cba_NtkObjNum(p) && Cba_ObjIsBo(p, iTerm); iTerm++, i++ )  if ( Cba_ObjBit(p, iTerm) ) {} else
-
-#define Cba_BoxForEachFanin( p, iBox, iFanin, i )                         \
-    for ( i = 0; iBox - 1 - i >= 0 && Cba_ObjIsBi(p, iBox - 1 - i) && (((iFanin) = Cba_BoxFanin(p, iBox, i)), 1); i++ )
-#define Cba_BoxForEachFaninBox( p, iBox, iFanin, i )                      \
-    for ( i = 0; iBox - 1 - i >= 0 && Cba_ObjIsBi(p, iBox - 1 - i) && (((iFanin) = Cba_BoxFaninBox(p, iBox, i)), 1); i++ )
-
-#define Cba_ObjForEachFanout( p, iCi, iCo )                               \
-    for ( iCo = Cba_ObjFanout(p, iCi); iCo; iCo = Cba_ObjNextFanout(p, iCo) )
-#define Cba_BoxForEachFanoutBox( p, iBox, iCo, iFanBox )                  \
-    for ( assert(Cba_BoxBoNum(p, iBox) == 1), iCo = Cba_ObjFanout(p, Cba_BoxBo(p, iBox, 0)); iCo && ((iFanBox = Cba_BoxBiBox(p, iCo)), 1); iCo = Cba_ObjNextFanout(p, iCo) )
+    for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Cba_ObjIsBoxPrim(p, i) ) {} else
+
+#define Cba_NtkForEachFinFon( p, iFon, i )                                \
+    for ( i = 0; i < Vec_IntSize(&p->vFinFon) && (((iFon) = Vec_IntEntry(&p->vFinFon, i)), 1); i++ ) if ( !iFon ) {} else   
+#define Cba_NtkForEachFonName( p, Name, i )                               \
+    for ( i = 0; i < Vec_IntSize(&p->vFonName) && (((Name) = Vec_IntEntry(&p->vFonName, i)), 1); i++ ) if ( !Name ) {} else   
+
+#define Cba_ObjForEachFin( p, iObj, iFin, k )                             \
+    for ( k = 0, iFin = Cba_ObjFin0(p, iObj); iFin < Cba_ObjFin0(p, iObj+1); iFin++, k++ )
+#define Cba_ObjForEachFon( p, iObj, iFon, k )                             \
+    for ( k = 0, iFon = Cba_ObjFon0(p, iObj); iFon < Cba_ObjFon0(p, iObj+1); iFon++, k++ )
+#define Cba_ObjForEachFinFon( p, iObj, iFin, iFon, k )                    \
+    for ( k = 0, iFin = Cba_ObjFin0(p, iObj); iFin < Cba_ObjFin0(p, iObj+1) && ((iFon = Cba_FinFon(p, iFin)), 1); iFin++, k++ )
+#define Cba_ObjForEachFinFanin( p, iObj, iFin, iFanin, k )                \
+    for ( k = 0, iFin = Cba_ObjFin0(p, iObj); iFin < Cba_ObjFin0(p, iObj+1) && ((iFanin = Cba_FonObj(p, Cba_FinFon(p, iFin))), 1); iFin++, k++ )
+#define Cba_ObjForEachFinFaninReal( p, iObj, iFin, iFanin, k )            \
+    for ( k = 0, iFin = Cba_ObjFin0(p, iObj); iFin < Cba_ObjFin0(p, iObj+1) && ((iFanin = Cba_FonObj(p, Cba_FinFon(p, iFin))), 1); iFin++, k++ ) if ( !iFanin ) {} else
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -409,114 +408,40 @@ static inline char *         Cba_BoxNtkName( Cba_Ntk_t * p, int i )          { r
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Cba_ObjAlloc( Cba_Ntk_t * p, Cba_ObjType_t Type, int Fanin )
+static inline int Cba_ObjAlloc( Cba_Ntk_t * p, Cba_ObjType_t Type, int nFins, int nFons )
 {
-    int iObj = Cba_NtkObjNum(p);
-    assert( iObj == Vec_IntSize(&p->vFanin) );
+    int i, iObj = Vec_StrSize(&p->vObjType);
     if ( Type == CBA_OBJ_PI )
         Vec_IntPush( &p->vInputs, iObj );
     else if ( Type == CBA_OBJ_PO )
         Vec_IntPush( &p->vOutputs, iObj );
-    Vec_StrPush( &p->vType, (char)Abc_Var2Lit(Type, 0) );
-    Vec_IntPush( &p->vFanin, Fanin );
+    Vec_StrPush( &p->vObjType, (char)Type );
+    // add fins
+    for ( i = 0; i < nFins; i++ )
+        Vec_IntPush( &p->vFinFon, 0 );
+    if ( Vec_IntSize(&p->vObjFin0) )
+        Vec_IntPush( &p->vObjFin0, Vec_IntSize(&p->vFinFon) );
+    // add fons
+    for ( i = 0; i < nFons; i++ )
+        Vec_IntPush( &p->vFonObj, iObj );
+    if ( Vec_IntSize(&p->vObjFon0) )
+        Vec_IntPush( &p->vObjFon0, Vec_IntSize(&p->vFonObj) );
     return iObj;
 }
 static inline int Cba_ObjDup( Cba_Ntk_t * pNew, Cba_Ntk_t * p, int i )
 {
-    int iObj = Cba_ObjAlloc( pNew, Cba_ObjType(p, i), Cba_ObjIsBox(p, i) ? Cba_BoxNtkId(p, i) : -1 );
-    if ( Cba_NtkHasNames(p) && Cba_NtkHasNames(pNew) && !Cba_ObjIsCo(p, i) ) 
-        Cba_ObjSetName( pNew, iObj, Cba_ObjName(p, i) );
+    int iObj = Cba_ObjAlloc( pNew, Cba_ObjType(p, i), Cba_ObjFinNum(p, i), Cba_ObjFonNum(p, i) );
     Cba_ObjSetCopy( p, i, iObj );
     return iObj;
 }
-static inline int Cba_BoxAlloc( Cba_Ntk_t * p, Cba_ObjType_t Type, int nIns, int nOuts, int iNtk )
-{
-    int i, iObj;
-    for ( i = nIns - 1; i >= 0; i-- )
-        Cba_ObjAlloc( p, CBA_OBJ_BI, -1 );
-    iObj = Cba_ObjAlloc( p, Type, iNtk );
-    for ( i = 0; i < nOuts; i++ )
-        Cba_ObjAlloc( p, CBA_OBJ_BO, -1 );
-    return iObj;
-}
-static inline int Cba_BoxDup( Cba_Ntk_t * pNew, Cba_Ntk_t * p, int iBox )
-{
-    int i, iTerm, iBoxNew;
-    Cba_BoxForEachBiReverse( p, iBox, iTerm, i )
-        Cba_ObjDup( pNew, p, iTerm );
-    iBoxNew = Cba_ObjDup( pNew, p, iBox );
-    if ( Cba_NtkHasNames(p) && Cba_NtkHasNames(pNew) && Cba_ObjName(p, iBox) ) 
-        Cba_ObjSetName( pNew, iBoxNew, Cba_ObjName(p, iBox) );
-    if ( Cba_BoxNtk(p, iBox) )
-        Cba_BoxSetNtkId( pNew, iBoxNew, Cba_NtkCopy(Cba_BoxNtk(p, iBox)) );
-    Cba_BoxForEachBo( p, iBox, iTerm, i )
-        Cba_ObjDup( pNew, p, iTerm );
-    return iBoxNew;
-}
-static inline void Cba_BoxDelete( Cba_Ntk_t * p, int iBox )
-{
-    int iStart = iBox - Cba_BoxBiNum(p, iBox);
-    int i, iStop = iBox + Cba_BoxBoNum(p, iBox);
-    for ( i = iStart; i <= iStop; i++ )
-    {
-        Vec_StrWriteEntry( &p->vType,  i, (char)0 );
-        Vec_IntWriteEntry( &p->vFanin, i, -1 );
-        if ( Cba_NtkHasNames(p) )
-            Vec_IntWriteEntry( &p->vName, i, 0 );
-        if ( Cba_NtkHasFanouts(p) )
-            Vec_IntWriteEntry( &p->vFanout, i, 0 );
-    }
-}
-static inline void Cba_BoxReplace( Cba_Ntk_t * p, int iBox, int * pArray, int nSize )
-{
-    extern void Cba_NtkUpdateFanout( Cba_Ntk_t * p, int iOld, int iNew );
-    int i, Limit = Cba_BoxBoNum(p, iBox);
-    assert( Limit == nSize );
-    for ( i = 0; i < Limit; i++ )
-        Cba_NtkUpdateFanout( p, Cba_BoxBo(p, iBox, i), pArray[i] );
-}
-
-
-static inline Vec_Int_t * Cba_BoxCollectRanges( Cba_Ntk_t * p, int iBox )
-{
-    static Vec_Int_t Bits, * vBits = &Bits;
-    static int pArray[10]; int i, iTerm;
-    assert( !Cba_ObjIsBoxUser(p, iBox) );
-    // initialize array
-    vBits->pArray = pArray;
-    vBits->nSize = 0;
-    vBits->nCap = 10;
-    // iterate through inputs
-    Cba_BoxForEachBiMain( p, iBox, iTerm, i )
-        Vec_IntPush( vBits, Cba_BoxBiRange(p, iTerm) );
-    // iterate through outputs
-    Cba_BoxForEachBoMain( p, iBox, iTerm, i )
-        Vec_IntPush( vBits, Cba_BoxBoRange(p, iTerm) );
-    assert( Vec_IntSize(vBits) < 10 );
-    //Vec_IntPrint( vBits );
-    return vBits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrPrint( Vec_Str_t * p, int fInt )
+static inline void Cba_ObjDelete( Cba_Ntk_t * p, int i )
 {
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( fInt )
-            printf( "%d ", (int)p->pArray[i] );
-        else
-            printf( "%c ", p->pArray[i] );
-    printf( "\n" );
+    int k, iFin, iFon;
+    Cba_ObjCleanType( p, i );
+    Cba_ObjForEachFin( p, i, iFin, k )
+        Vec_IntWriteEntry( &p->vFinFon, iFin, 0 );
+    Cba_ObjForEachFon( p, i, iFon, k )
+        Vec_IntWriteEntry( &p->vFonObj, iFon, 0 );
 }
 
 /**Function*************************************************************
@@ -530,181 +455,287 @@ static inline void Vec_StrPrint( Vec_Str_t * p, int fInt )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Cba_NtkAlloc( Cba_Ntk_t * pNew, int NameId, int nIns, int nOuts, int nObjs )
-{
-    int NtkId, fFound;
-    assert( pNew->pDesign != NULL );
-    assert( Cba_NtkPiNum(pNew) == 0 );
-    assert( Cba_NtkPoNum(pNew) == 0 );
+static inline Cba_Ntk_t *  Cba_NtkAlloc( Cba_Man_t * p, int NameId, int nIns, int nOuts, int nObjs, int nFins, int nFons )
+{    
+    Cba_Ntk_t * pNew = ABC_CALLOC( Cba_Ntk_t, 1 );
+    assert( nIns >= 0 && nOuts >= 0 && nObjs >= 0 && nFins >= 0 && nFons >= 0 );
+    pNew->Id      = Vec_PtrSize(&p->vNtks);   Vec_PtrPush( &p->vNtks, pNew );
     pNew->NameId  = NameId;
-    pNew->iCopy   = -1;
-    pNew->iBoxNtk = -1;
-    pNew->iBoxObj = -1;
+    pNew->pDesign = p;
     Vec_IntGrow( &pNew->vInputs,  nIns );
     Vec_IntGrow( &pNew->vOutputs, nOuts );
-    Vec_StrGrow( &pNew->vType,    nObjs );
-    Vec_IntGrow( &pNew->vFanin,   nObjs );
-    // check if the network is unique
-    NtkId = Abc_NamStrFindOrAdd( pNew->pDesign->pMods, Cba_NtkStr(pNew, NameId), &fFound );
+    Vec_StrGrow( &pNew->vObjType, nObjs+1 );  Vec_StrPush( &pNew->vObjType,  (char)CBA_OBJ_NONE );
+    Vec_IntGrow( &pNew->vObjFin0, nObjs+2 );  Vec_IntPush( &pNew->vObjFin0,  0 ); Vec_IntPush( &pNew->vObjFin0, 1 );
+    Vec_IntGrow( &pNew->vObjFon0, nObjs+2 );  Vec_IntPush( &pNew->vObjFon0,  0 ); Vec_IntPush( &pNew->vObjFon0, 1 );
+    Vec_IntGrow( &pNew->vFinFon,  nFins+1 );  Vec_IntPush( &pNew->vFinFon,   0 );
+    Vec_IntGrow( &pNew->vFonObj,  nFons+1 );  Vec_IntPush( &pNew->vFonObj,   0 );
+    return pNew;
+}
+static inline void Cba_NtkAdd( Cba_Man_t * p, Cba_Ntk_t * pNtk )
+{    
+    int fFound, NtkId = Abc_NamStrFindOrAdd( p->pMods, Cba_NtkStr(pNtk, pNtk->NameId), &fFound );
     if ( fFound )
-        printf( "Network with name %s already exists.\n", Cba_NtkStr(pNew, NameId) );
+        printf( "Network with name \"%s\" already exists.\n", Cba_NtkStr(pNtk, pNtk->NameId) );
     else
-        assert( NtkId == Cba_NtkId(pNew) );
+        assert( NtkId == pNtk->Id );
 }
-static inline void Cba_NtkDup( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
+static inline Vec_Int_t * Cba_NtkCollect( Cba_Ntk_t * p )
 {
-    int i, iObj;
-    assert( pNew != p );
-    Cba_NtkAlloc( pNew, Cba_NtkNameId(p), Cba_NtkPiNum(p), Cba_NtkPoNum(p), Cba_NtkObjNum(p) );
-    if ( Vec_IntSize(&p->vInfo) )
-        Vec_IntAppend( &pNew->vInfo, &p->vInfo );
-    Cba_NtkStartCopies( p );
-    if ( Cba_NtkHasNames(p) )
-        Cba_NtkStartNames( pNew );
+    int iObj;
+    Vec_Int_t * vObjs = Vec_IntAlloc( Cba_NtkObjNum(p) );
+    Cba_NtkForEachObj( p, iObj )
+        Vec_IntPush( vObjs, iObj );
+    return vObjs;
+}
+static inline void Cba_NtkCollectDfs_rec( Cba_Ntk_t * p, int iObj, Vec_Int_t * vObjs )
+{
+    int iFin, iFanin, k;
+    if ( !Cba_ObjCopy(p, iObj) )
+        return;
+    Cba_ObjSetCopy( p, iObj, 0 );
+    Cba_ObjForEachFinFaninReal( p, iObj, iFin, iFanin, k )
+        Cba_NtkCollectDfs_rec( p, iFanin, vObjs );
+    Vec_IntPush( vObjs, iObj );
+}
+static inline Vec_Int_t * Cba_NtkCollectDfs( Cba_Ntk_t * p )
+{
+    int i, k, iObj, iFin, iFanin;
+    Vec_Int_t * vObjs = Vec_IntAlloc( Cba_NtkObjNum(p) );
+    // collect PIs
     Cba_NtkForEachPi( p, iObj, i )
-        Cba_ObjDup( pNew, p, iObj );
-    Cba_NtkForEachBox( p, iObj )
-        Cba_BoxDup( pNew, p, iObj );
+        Vec_IntPush( vObjs, iObj );
+    // prepare leaves
+    Cba_NtkCleanObjCopies( p );
+    Vec_IntForEachEntry( vObjs, iObj, i )
+        Cba_ObjSetCopy( p, iObj, 0 );
+    // collect internal
     Cba_NtkForEachPo( p, iObj, i )
-        Cba_ObjDup( pNew, p, iObj );
-    Cba_NtkForEachCo( p, iObj )
-        Cba_ObjSetFanin( pNew, Cba_ObjCopy(p, iObj), Cba_ObjCopy(p, Cba_ObjFanin(p, iObj)) );
-    //Cba_NtkFreeCopies( p ); // needed for name transfer and host ntk
-    assert( Cba_NtkObjNum(pNew) == Cba_NtkObjNumAlloc(pNew) );
+        Cba_ObjForEachFinFaninReal( p, iObj, iFin, iFanin, k )
+            Cba_NtkCollectDfs_rec( p, iFanin, vObjs );
+    // additionally collect user modules without outputs
+    Cba_NtkForEachBoxUser( p, iObj )
+        if ( Cba_ObjFonNum(p, iObj) == 0 )
+            Cba_ObjForEachFinFaninReal( p, iObj, iFin, iFanin, k )
+                Cba_NtkCollectDfs_rec( p, iFanin, vObjs );
+    // collect POs
+    Cba_NtkForEachPo( p, iObj, i )
+        Vec_IntPush( vObjs, iObj );
+    // collect user boxes without fanouts
+    Cba_NtkForEachBoxUser( p, iObj )
+        if ( Cba_ObjFonNum(p, iObj) == 0 )
+            Vec_IntPush( vObjs, iObj );
+    assert( Vec_IntSize(vObjs) <= Cba_NtkObjNum(p) );
+    if ( Vec_IntSize(vObjs) != Cba_NtkObjNum(p) )
+        printf( "Warning: DSF ordering collected %d out of %d objects.\n", Vec_IntSize(vObjs), Cba_NtkObjNum(p) );
+    return vObjs;
 }
-static inline void Cba_NtkDupUserBoxes( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
+static inline void Cba_NtkCreateFonNames( Cba_Ntk_t * p, char * pPref )
 {
-    int i, iObj;
-    assert( pNew != p );
-    Cba_NtkAlloc( pNew, Cba_NtkNameId(p), Cba_NtkPiNum(p), Cba_NtkPoNum(p), Cba_NtkObjNum(p) + 3*Cba_NtkCoNum(p) );
-    if ( Vec_IntSize(&p->vInfo) )
-        Vec_IntAppend( &pNew->vInfo, &p->vInfo );
-    Cba_NtkStartCopies( p );
+    int i, iObj, NameId;
+    Cba_NtkCleanFonNames( p );
     Cba_NtkForEachPi( p, iObj, i )
-        Cba_ObjDup( pNew, p, iObj );
+        Cba_FonSetName( p, Cba_ObjFon0(p, iObj), Cba_ObjName(p, iObj) );
     Cba_NtkForEachPo( p, iObj, i )
-        Cba_ObjDup( pNew, p, iObj );
-    Cba_NtkForEachBoxUser( p, iObj )
-        Cba_BoxDup( pNew, p, iObj );
-    // connect feed-throughs
-    Cba_NtkForEachCo( p, iObj )
-        if ( Cba_ObjCopy(p, iObj) >= 0 && Cba_ObjCopy(p, Cba_ObjFanin(p, iObj)) >= 0 )
-            Cba_ObjSetFanin( pNew, Cba_ObjCopy(p, iObj), Cba_ObjCopy(p, Cba_ObjFanin(p, iObj)) );
+        Cba_FonSetName( p, Cba_ObjFinFon(p, iObj, 0), Cba_ObjName(p, iObj) );
+    Vec_IntForEachEntryStart( &p->vFonName, NameId, i, 1 )
+        if ( NameId == 0 )
+            Vec_IntWriteEntry( &p->vFonName, i, Cba_ManNewStrId(p->pDesign, pPref, i, NULL) );
 }
-static inline void Cba_NtkMoveNames( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
+static inline void Cba_NtkMissingFonNames( Cba_Ntk_t * p, char * pPref )
 {
-    int i, iBox, iObj;
-    assert( Cba_NtkHasNames(p) );
-    assert( !Cba_NtkHasNames(pNew) );
-    Cba_NtkStartNames( pNew );
+    int i, iObj, iFon;
     Cba_NtkForEachPi( p, iObj, i )
-        Cba_ObjSetName( pNew, Cba_ObjCopy(p, iObj), Cba_ObjName(p, iObj) );
-    Cba_NtkForEachBoxUser( p, iBox )
+        if ( !Cba_FonName(p, Cba_ObjFon0(p, iObj)) )
+            Cba_FonSetName( p, Cba_ObjFon0(p, iObj), Cba_ObjName(p, iObj) );
+    Cba_NtkForEachPo( p, iObj, i )
+        if ( Cba_ObjFinFon(p, iObj, 0) > 0 && !Cba_FonName(p, Cba_ObjFinFon(p, iObj, 0)) )
+            Cba_FonSetName( p, Cba_ObjFinFon(p, iObj, 0), Cba_ObjName(p, iObj) );
+    Cba_NtkForEachObj( p, iObj )
+        Cba_ObjForEachFon( p, iObj, iFon, i )
+            if ( !Cba_FonName(p, iFon) )
+                Cba_FonSetName( p, iFon, Cba_ManNewStrId(p->pDesign, pPref, iFon, NULL) );
+}
+
+static inline void Cba_NtkCountParams( Cba_Ntk_t * p, Vec_Int_t * vObjs, int * nPis, int * nPos, int * nFins, int * nFons )
+{
+    int i, iObj;
+    *nPis = *nPos = *nFins = *nFons = 0;
+    Vec_IntForEachEntry( vObjs, iObj, i )
     {
-        Cba_ObjSetName( pNew, Cba_ObjCopy(p, iBox), Cba_ObjName(p, iBox) );
-        Cba_BoxForEachBo( p, iBox, iObj, i )
-            Cba_ObjSetName( pNew, Cba_ObjCopy(p, iObj), Cba_ObjName(p, iObj) );
+        *nPis += Cba_ObjIsPi(p, iObj);
+        *nPos += Cba_ObjIsPo(p, iObj);
+        *nFins += Cba_ObjFinNum(p, iObj);
+        *nFons += Cba_ObjFonNum(p, iObj);
     }
-    Cba_NtkForEachBoxUser( p, iBox )
-        Cba_BoxForEachBi( p, iBox, iObj, i )
-            if ( !Cba_ObjName(pNew, Cba_ObjFanin(pNew, Cba_ObjCopy(p, iObj))) )
-                Cba_ObjSetName( pNew, Cba_ObjFanin(pNew, Cba_ObjCopy(p, iObj)), Cba_ObjName(p, iObj) );
-    Cba_NtkForEachPo( p, iObj, i )
-        if ( !Cba_ObjName(pNew, Cba_ObjFanin(pNew, Cba_ObjCopy(p, iObj))) )
-            Cba_ObjSetName( pNew, Cba_ObjFanin(pNew, Cba_ObjCopy(p, iObj)), Cba_ObjName(p, iObj) );
+}
+static inline Cba_Ntk_t * Cba_NtkDup( Cba_Man_t * pMan, Cba_Ntk_t * p, Vec_Int_t * vObjs )
+{
+    Cba_Ntk_t * pNew;
+    int i, k, iObj, iObjNew, iFin, iFon;
+    int nPis, nPos, nFins, nFons;
+    Cba_NtkCountParams( p, vObjs, &nPis, &nPos, &nFins, &nFons );
+    pNew = Cba_NtkAlloc( pMan, 0, nPis, nPos, Vec_IntSize(vObjs), nFins, nFons );
+    Cba_NtkAdd( pMan, pNew );
+    Cba_NtkCleanObjCopies( p );
+    Cba_NtkCleanFonCopies( p );
+    Vec_IntForEachEntry( vObjs, iObj, i )
+    {
+        iObjNew = Cba_ObjDup( pNew, p, iObj );
+        Cba_ObjForEachFon( p, iObj, iFon, k )
+            Cba_FonSetCopy( p, iFon, Cba_ObjFon(pNew, iObjNew, k) );
+    }
+    Vec_IntForEachEntry( vObjs, iObj, i )
+    {
+        iObjNew = Cba_ObjCopy( p, iObj );
+        Cba_ObjForEachFinFon( p, iObj, iFin, iFon, k )
+            Cba_ObjSetFinFon( pNew, iObjNew, k, Cba_FonCopy(p, iFon) );
+    }
+    //Cba_NtkFreeObjCopies( p );
+    //Cba_NtkFreeFonCopies( p );
+    assert( Cba_NtkObjNum(pNew) == Cba_NtkObjNumAlloc(pNew) );
+    Cba_NtkSetCopy( p, Cba_NtkId(pNew) );
+    return pNew;
+}
+static inline Cba_Ntk_t * Cba_NtkDupOrder( Cba_Man_t * pMan, Cba_Ntk_t * p, Vec_Int_t*(* pFuncOrder)(Cba_Ntk_t*) )
+{
+    Cba_Ntk_t * pNew;
+    Vec_Int_t * vObjs = pFuncOrder ? pFuncOrder(p) : Cba_NtkCollect(p);
+    if ( vObjs == NULL )
+        return NULL;
+    pNew = Cba_NtkDup( pMan, p, vObjs );
+    Vec_IntFree( vObjs );
+    return pNew;
+}
+static inline Cba_Ntk_t * Cba_NtkDupAttrs( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
+{
+    // transfer object attributes
+    Vec_IntRemapArray( &p->vObjCopy, &p->vObjFunc,  &pNew->vObjFunc,  Cba_NtkObjNum(pNew) + 1 );
+    Vec_IntRemapArray( &p->vObjCopy, &p->vObjName,  &pNew->vObjName,  Cba_NtkObjNum(pNew) + 1 );
+    Vec_IntRemapArray( &p->vObjCopy, &p->vObjAttr,  &pNew->vObjAttr,  Cba_NtkObjNum(pNew) + 1 );
+    // transfer fon attributes
+    Vec_IntRemapArray( &p->vFonCopy, &p->vFonName,  &pNew->vFonName,  Cba_NtkFonNum(pNew) + 1 );
+    Vec_IntRemapArray( &p->vFonCopy, &p->vFonRange, &pNew->vFonRange, Cba_NtkFonNum(pNew) + 1 );
+    Vec_IntRemapArray( &p->vFonCopy, &p->vFonLeft,  &pNew->vFonLeft,  Cba_NtkFonNum(pNew) + 1 );
+    Vec_IntRemapArray( &p->vFonCopy, &p->vFonRight, &pNew->vFonRight, Cba_NtkFonNum(pNew) + 1 );
+    // duplicate attributes
+    Vec_IntAppend( &pNew->vAttrSto, &p->vAttrSto );
+    pNew->vOther = p->vOther ? (Vec_Ptr_t *)Vec_VecDup( (Vec_Vec_t *)p->vOther ) : NULL;
 }
 
 static inline void Cba_NtkFree( Cba_Ntk_t * p )
 {
+    // interface
     Vec_IntErase( &p->vInputs );
     Vec_IntErase( &p->vOutputs );
-    Vec_IntErase( &p->vInfo );
-    Vec_StrErase( &p->vType );
-    Vec_IntErase( &p->vFanin );    
-    Vec_IntErase( &p->vIndex );
-    Vec_IntErase( &p->vName );    
-    Vec_IntErase( &p->vFanout );    
-    Vec_IntErase( &p->vCopy );    
-    Vec_IntErase( &p->vArray );    
-    Vec_IntErase( &p->vArray2 );    
+    Vec_IntErase( &p->vOrder );
+    // stucture
+    Vec_StrErase( &p->vObjType );
+    Vec_IntErase( &p->vObjFin0 );    
+    Vec_IntErase( &p->vObjFon0 );
+    Vec_IntErase( &p->vFinFon );    
+    Vec_IntErase( &p->vFonObj );    
+    // optional
+    Vec_IntErase( &p->vObjCopy );    
+    Vec_IntErase( &p->vObjFunc );    
+    Vec_IntErase( &p->vObjName );    
+    Vec_IntErase( &p->vObjAttr );    
+    Vec_IntErase( &p->vAttrSto );    
+    Vec_IntErase( &p->vFonCopy );    
+    Vec_IntErase( &p->vFonName );    
+    Vec_IntErase( &p->vFonRange );    
+    Vec_IntErase( &p->vFonLeft );    
+    Vec_IntErase( &p->vFonRight );    
+    Vec_IntErase( &p->vFonPrev );    
+    Vec_IntErase( &p->vFonNext );    
+    Vec_IntErase( &p->vFinFon0 );    
+    Vec_IntErase( &p->vFinObj );    
+    Vec_IntErase( &p->vNtkObjs );    
+    // other
+    Vec_IntErase( &p->vArray0 );    
+    Vec_IntErase( &p->vArray1 );    
+    if ( p->vOther ) Vec_VecFree( (Vec_Vec_t *)p->vOther );
+    ABC_FREE( p );
 }
 static inline int Cba_NtkMemory( Cba_Ntk_t * p )
 {
     int nMem = sizeof(Cba_Ntk_t);
+    // interface
     nMem += (int)Vec_IntMemory(&p->vInputs);
     nMem += (int)Vec_IntMemory(&p->vOutputs);
-    nMem += (int)Vec_IntMemory(&p->vInfo);
-    nMem += (int)Vec_StrMemory(&p->vType);
-    nMem += (int)Vec_IntMemory(&p->vFanin);
-    nMem += (int)Vec_IntMemory(&p->vIndex);
-    nMem += (int)Vec_IntMemory(&p->vName);
-    nMem += (int)Vec_IntMemory(&p->vFanout);
-    nMem += (int)Vec_IntMemory(&p->vCopy);
+    nMem += (int)Vec_IntMemory(&p->vOrder);
+    // stucture
+    nMem += (int)Vec_StrMemory(&p->vObjType);
+    nMem += (int)Vec_IntMemory(&p->vObjFin0);
+    nMem += (int)Vec_IntMemory(&p->vObjFon0);
+    nMem += (int)Vec_IntMemory(&p->vFinFon);
+    nMem += (int)Vec_IntMemory(&p->vFonObj);
+    // optional
+    nMem += (int)Vec_IntMemory(&p->vObjCopy );  
+    nMem += (int)Vec_IntMemory(&p->vObjFunc );  
+    nMem += (int)Vec_IntMemory(&p->vObjName );  
+    nMem += (int)Vec_IntMemory(&p->vObjAttr );  
+    nMem += (int)Vec_IntMemory(&p->vAttrSto );  
+    nMem += (int)Vec_IntMemory(&p->vFonCopy );  
+    nMem += (int)Vec_IntMemory(&p->vFonName );  
+    nMem += (int)Vec_IntMemory(&p->vFonRange ); 
+    nMem += (int)Vec_IntMemory(&p->vFonLeft );  
+    nMem += (int)Vec_IntMemory(&p->vFonRight ); 
+    nMem += (int)Vec_IntMemory(&p->vFonPrev );  
+    nMem += (int)Vec_IntMemory(&p->vFonNext );  
+    nMem += (int)Vec_IntMemory(&p->vFinFon0 );  
+    nMem += (int)Vec_IntMemory(&p->vFinObj );   
+    nMem += (int)Vec_IntMemory(&p->vNtkObjs );  
+    // other
+    nMem += (int)Vec_IntMemory(&p->vArray1 );
+    nMem += (int)Vec_IntMemory(&p->vArray1 );
     return nMem;
 }
+static inline int Cba_NtkIsTopoOrder( Cba_Ntk_t * p )
+{
+    int i, iObj, iFin, iFanin, fTopo = 1;
+    Vec_Bit_t * vVisited = Vec_BitStart( Cba_NtkObjNum(p) + 1 );
+    Cba_NtkForEachObj( p, iObj )
+    {
+        Cba_ObjForEachFinFaninReal( p, iObj, iFin, iFanin, i )
+            if ( !Vec_BitEntry(vVisited, iFanin) )
+                fTopo = 0;
+        if ( !fTopo )
+            break;
+        Vec_BitWriteEntry( vVisited, iObj, 1 );
+    }
+    Vec_BitFree( vVisited );
+    return fTopo;
+}
 static inline void Cba_NtkPrintStats( Cba_Ntk_t * p )
 {
     printf( "pi =%5d  ",   Cba_NtkPiNum(p) );
-    printf( "pi =%5d  ",   Cba_NtkPoNum(p) );
-    printf( "box =%6d  ",  Cba_NtkBoxNum(p) );
-    printf( "clp =%7d  ",  p->Count );
-    printf( "obj =%7d  ",  Cba_NtkObjNum(p) );
-    printf( "%s ",         Cba_NtkName(p) );
-    if ( Cba_NtkHostNtk(p) > 0 )
-        printf( "-> %s",   Cba_NtkName(Cba_NtkHostNtk(p)) );
+    printf( "po =%5d  ",   Cba_NtkPoNum(p) );
+    printf( "user =%6d  ", Cba_NtkBoxUserNum(p) );
+    printf( "prim =%6d  ", Cba_NtkBoxPrimNum(p) );
+    printf( "topo =%4s  ", Cba_NtkIsTopoOrder(p) ? "yes" : "no" );
+    printf( "  %s ",       Cba_NtkName(p) );
+    if ( Vec_IntSize(&p->vNtkObjs) )
+        printf( "-> %s",   Cba_NtkName(Cba_NtkNtk(p, Vec_IntEntry(&p->vNtkObjs, 0))) );
     printf( "\n" );
-}
-static inline void Cba_NtkDeriveIndex( Cba_Ntk_t * p )
-{
-    int i, iObj, iTerm;
-    Vec_IntFill( &p->vIndex, Cba_NtkObjNum(p), -1 );
-    Cba_NtkForEachPi( p, iObj, i )
-        Cba_ObjSetIndex( p, iObj, i );
-    Cba_NtkForEachPo( p, iObj, i )
-        Cba_ObjSetIndex( p, iObj, i );
-    Cba_NtkForEachBox( p, iObj )
-    {
-        Cba_BoxForEachBi( p, iObj, iTerm, i )
-            Cba_ObjSetIndex( p, iTerm, i );
-        Cba_BoxForEachBo( p, iObj, iTerm, i )
-            Cba_ObjSetIndex( p, iTerm, i );
-    }
+//    Vec_StrIntPrint( &p->vObjType );
 }
 static inline void Cba_NtkPrint( Cba_Ntk_t * p )
 {
-    int i, Type, Value, Beg, End;
-    printf( "Interface (%d):\n", Cba_NtkInfoNum(p) );
-    Vec_IntForEachEntryTriple( &p->vInfo, Value, Beg, End, i )
-    {
-        printf( "%6d : ", i );
-        printf( "Type =%3d  ", Cba_NtkInfoType(p, i/3) );
-        if ( Beg >= 0 )
-            printf( "[%d:%d]   ", End, Beg );
-        else
-            printf( "        " );
-        printf( "Name =%3d   ", Cba_NtkInfoName(p, i/3) );
-        if ( Cba_NtkInfoName(p, i/3) )
-            printf( "%s", Cba_NtkStr( p, Cba_NtkInfoName(p, i/3) ) );
-        printf( "\n" );
-    }
+    int i, Type;
+    printf( "Interface (%d):\n", Cba_NtkPioNum(p) );
     printf( "Objects (%d):\n", Cba_NtkObjNum(p) );
     Cba_NtkForEachObjType( p, Type, i )
     {
         printf( "%6d : ", i );
         printf( "Type =%3d  ", Type );
-        if ( Cba_ObjIsCo(p, i) )
-            printf( "Fanin =%6d  ", Cba_ObjFanin(p, i) );
-        else if ( Cba_NtkHasNames(p) && Cba_ObjName(p, i) )
-        {
-            printf( "Name  =%6d(%d)  ", Cba_ObjNameId(p, i), Cba_ObjNameType(p, i) );
-            if ( Cba_ObjNameType(p, i) <= CBA_NAME_WORD )
-                printf( "%s", Cba_ObjNameStr(p, i) );
-        }
+        printf( "Fins = %d  ", Cba_ObjFinNum(p, i) );
+        printf( "Fons = %d  ", Cba_ObjFonNum(p, i) );
+        if ( Cba_NtkHasObjNames(p) && Cba_ObjName(p, i) )
+            printf( "%s", Cba_ObjNameStr(p, i) );
         printf( "\n" );
     }
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Manager APIs.]
@@ -716,98 +747,63 @@ static inline void Cba_NtkPrint( Cba_Ntk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline Cba_Man_t * Cba_ManAlloc( char * pFileName, int nNtks )
+static inline Cba_Man_t * Cba_ManAlloc( char * pFileName, int nNtks, Abc_Nam_t * pStrs, Abc_Nam_t * pMods )
 {
-    extern void Cba_ManSetupTypes( char ** pNames, char ** pSymbs );
-    Cba_Ntk_t * pNtk; int i;
     Cba_Man_t * pNew = ABC_CALLOC( Cba_Man_t, 1 );
     pNew->pName = Extra_FileDesignName( pFileName );
     pNew->pSpec = Abc_UtilStrsav( pFileName );
-    pNew->pStrs = Abc_NamStart( 1000, 24 );
-    pNew->pMods = Abc_NamStart( 1000, 24 );
-    pNew->iRoot = 1;
-    pNew->nNtks = nNtks;
-    pNew->pNtks = ABC_CALLOC( Cba_Ntk_t, pNew->nNtks + 1 );
-    Cba_ManForEachNtk( pNew, pNtk, i )
-        pNtk->pDesign = pNew;
-    Cba_ManSetupTypes( pNew->pPrimNames, pNew->pPrimSymbs );
-    return pNew;
-}
-static inline Cba_Man_t * Cba_ManStart( Cba_Man_t * p, int nNtks )
-{
-    Cba_Ntk_t * pNtk; int i;
-    Cba_Man_t * pNew = ABC_CALLOC( Cba_Man_t, 1 );
-    pNew->pName = Abc_UtilStrsav( Cba_ManName(p) );
-    pNew->pSpec = Abc_UtilStrsav( Cba_ManSpec(p) );
-    pNew->pStrs = Abc_NamRef( p->pStrs );  
-    pNew->pMods = Abc_NamStart( 1000, 24 );
-    pNew->iRoot = 1;
-    pNew->nNtks = nNtks;
-    pNew->pNtks = ABC_CALLOC( Cba_Ntk_t, nNtks + 1 );
-    Cba_ManForEachNtk( pNew, pNtk, i )
-        pNtk->pDesign = pNew;
+    pNew->pStrs = pStrs ? pStrs : Abc_NamStart( 1000, 24 );
+    pNew->pMods = pMods ? pMods : Abc_NamStart( 1000, 24 );
+    Vec_PtrGrow( &pNew->vNtks,  nNtks+1 ); Vec_PtrPush( &pNew->vNtks, NULL );
+    if ( nNtks == 1 ) pNew->iRoot = 1;
     return pNew;
 }
-static inline Cba_Man_t * Cba_ManDup( Cba_Man_t * p )
+static inline Cba_Man_t * Cba_ManDup( Cba_Man_t * p, Vec_Int_t*(* pFuncOrder)(Cba_Ntk_t*) )
 {
-    Cba_Ntk_t * pNtk, * pHost; int i;
-    Cba_Man_t * pNew = Cba_ManStart( p, Cba_ManNtkNum(p) );
+    Cba_Ntk_t * pNtk, * pNtkNew; int i;
+    Cba_Man_t * pNew = Cba_ManAlloc( p->pSpec, Cba_ManNtkNum(p), Abc_NamRef(p->pStrs), Abc_NamRef(p->pMods) );
     Cba_ManForEachNtk( p, pNtk, i )
-        Cba_NtkSetCopy( pNtk, i );
-    Cba_ManForEachNtk( p, pNtk, i )
-        Cba_NtkDup( Cba_NtkCopyNtk(pNew, pNtk), pNtk );
-    Cba_ManForEachNtk( p, pNtk, i )
-        if ( (pHost = Cba_NtkHostNtk(pNtk)) )
-            Cba_NtkSetHost( Cba_NtkCopyNtk(pNew, pNtk), Cba_NtkCopy(pHost), Cba_ObjCopy(pHost, Cba_NtkHostObj(pNtk)) );
-    return pNew;
-}
-static inline Cba_Man_t * Cba_ManDupUserBoxes( Cba_Man_t * p )
-{
-    Cba_Ntk_t * pNtk, * pHost; int i;
-    Cba_Man_t * pNew = Cba_ManStart( p, Cba_ManNtkNum(p) );
-    Cba_ManForEachNtk( p, pNtk, i )
-        Cba_NtkSetCopy( pNtk, i );
-    Cba_ManForEachNtk( p, pNtk, i )
-        Cba_NtkDupUserBoxes( Cba_NtkCopyNtk(pNew, pNtk), pNtk );
-    Cba_ManForEachNtk( p, pNtk, i )
-        if ( (pHost = Cba_NtkHostNtk(pNtk)) )
-            Cba_NtkSetHost( Cba_NtkCopyNtk(pNew, pNtk), Cba_NtkCopy(pHost), Cba_ObjCopy(pHost, Cba_NtkHostObj(pNtk)) );
+    {
+        pNtkNew = Cba_NtkDupOrder( pNew, pNtk, pFuncOrder );
+        Cba_NtkDupAttrs( pNtkNew, pNtk );
+    }
+//    Cba_ManForEachNtk( p, pNtk, i )
+//        if ( (pHost = Cba_NtkHostNtk(pNtk)) )
+//            Cba_NtkSetHost( Cba_NtkCopyNtk(pNew, pNtk), Cba_NtkCopy(pHost), Cba_ObjCopy(pHost, Cba_NtkHostObj(pNtk)) );
+    pNew->iRoot = Cba_ManNtkNum(pNew);
     return pNew;
 }
-static inline void Cba_ManMoveNames( Cba_Man_t * pNew, Cba_Man_t * p )
-{
-    Cba_Ntk_t * pNtk; int i;
-    Cba_ManForEachNtk( p, pNtk, i )
-        Cba_NtkMoveNames( Cba_NtkCopyNtk(pNew, pNtk), pNtk );
-}
-
-
 static inline void Cba_ManFree( Cba_Man_t * p )
 {
     Cba_Ntk_t * pNtk; int i;
     Cba_ManForEachNtk( p, pNtk, i )
         Cba_NtkFree( pNtk );
-    Vec_IntErase( &p->vBuf2LeafNtk );
-    Vec_IntErase( &p->vBuf2LeafObj );
-    Vec_IntErase( &p->vBuf2RootNtk );
-    Vec_IntErase( &p->vBuf2RootObj );
+    ABC_FREE( p->vNtks.pArray );
     Abc_NamDeref( p->pStrs );
     Abc_NamDeref( p->pMods );
+    Vec_StrFreeP( &p->vOut );
+    Vec_StrFreeP( &p->vOut2 );
     ABC_FREE( p->pName );
     ABC_FREE( p->pSpec );
-    ABC_FREE( p->pNtks );
     ABC_FREE( p );
 }
+static inline int Cba_ManIsTopOrder( Cba_Man_t * p )
+{
+    Cba_Ntk_t * pNtk; int i;
+    Cba_ManForEachNtk( p, pNtk, i )
+        if ( !Cba_NtkIsTopoOrder(pNtk) )
+            return 0;
+    return 1;
+}
 static inline int Cba_ManMemory( Cba_Man_t * p )
 {
     Cba_Ntk_t * pNtk; int i;
     int nMem = sizeof(Cba_Man_t);
-    if ( p->pName )
-    nMem += (int)strlen(p->pName);
-    if ( p->pSpec )
-    nMem += (int)strlen(p->pSpec);
+    nMem += p->pName ? (int)strlen(p->pName) : 0;
+    nMem += p->pSpec ? (int)strlen(p->pSpec) : 0;
     nMem += Abc_NamMemUsed(p->pStrs);
     nMem += Abc_NamMemUsed(p->pMods);
+    nMem += (int)Vec_PtrMemory(&p->vNtks);
     Cba_ManForEachNtk( p, pNtk, i )
         nMem += Cba_NtkMemory( pNtk );
     return nMem;
@@ -819,43 +815,56 @@ static inline int Cba_ManObjNum( Cba_Man_t * p )
         Count += Cba_NtkObjNum(pNtk);
     return Count;
 }
-static inline int Cba_ManNodeNum( Cba_Man_t * p )
+static inline int Cba_ManBoxNum( Cba_Man_t * p )
 {
     Cba_Ntk_t * pNtk; int i, Count = 0;
     Cba_ManForEachNtk( p, pNtk, i )
         Count += Cba_NtkBoxNum( pNtk );
     return Count;
 }
-static inline int Cba_ManBoxNum_rec( Cba_Ntk_t * p )
+static inline void Cba_ManBoxNumRec_rec( Cba_Ntk_t * p, int * pCountP, int * pCountU )
 {
-    int iObj, Counter = 0;
-    if ( p->Count >= 0 )
-        return p->Count;
-    Cba_NtkForEachBox( p, iObj )
-        Counter += Cba_ObjIsBoxUser(p, iObj) ? Cba_ManBoxNum_rec( Cba_BoxNtk(p, iObj) ) : 1;
-    return (p->Count = Counter);
+    int iObj, Id = Cba_NtkId(p);
+    if ( pCountP[Id] >= 0 )
+        return;
+    pCountP[Id] = pCountU[Id] = 0;
+    Cba_NtkForEachObj( p, iObj )
+    {
+        if ( Cba_ObjIsBoxUser(p, iObj) )
+        {
+            Cba_ManBoxNumRec_rec( Cba_ObjNtk(p, iObj), pCountP, pCountU );
+            pCountP[Id] += pCountP[Cba_ObjNtkId(p, iObj)];
+            pCountU[Id] += pCountU[Cba_ObjNtkId(p, iObj)] + 1;
+        }
+        else
+            pCountP[Id] += 1;
+    }
 }
-static inline int Cba_ManBoxNum( Cba_Man_t * p )
+static inline void Cba_ManBoxNumRec( Cba_Man_t * p, int * pnPrims, int * pnUsers )
 {
-    Cba_Ntk_t * pNtk; int i;
-    Cba_ManForEachNtk( p, pNtk, i )
-        pNtk->Count = -1;
-    return Cba_ManBoxNum_rec( Cba_ManRoot(p) );
+    Cba_Ntk_t * pNtk = Cba_ManRoot(p);
+    int * pCountP = ABC_FALLOC( int, Cba_ManNtkNum(p) + 1 );
+    int * pCountU = ABC_FALLOC( int, Cba_ManNtkNum(p) + 1 );
+    Cba_ManBoxNumRec_rec( pNtk, pCountP, pCountU );
+    *pnPrims = pCountP[Cba_NtkId(pNtk)];
+    *pnUsers = pCountU[Cba_NtkId(pNtk)];
+    ABC_FREE( pCountP );
+    ABC_FREE( pCountU );
 }
 static inline void Cba_ManPrintStats( Cba_Man_t * p, int nModules, int fVerbose )
 {
-    Cba_Ntk_t * pNtk; int i;
+    Cba_Ntk_t * pNtk; int i, nPrims, nUsers;
     Cba_Ntk_t * pRoot = Cba_ManRoot( p );
-    printf( "%-12s : ",   Cba_ManName(p) );
-    printf( "pi =%5d  ",  Cba_NtkPiNum(pRoot) );
-    printf( "po =%5d  ",  Cba_NtkPoNum(pRoot) );
-    printf( "pri =%4d  ", Cba_ManPrimNum(p) );
-    printf( "mod =%6d  ", Cba_ManNtkNum(p) );
-    printf( "box =%7d  ", Cba_ManNodeNum(p) );
-    printf( "obj =%7d  ", Cba_ManObjNum(p) );
+    Cba_ManBoxNumRec( p, &nPrims, &nUsers );
+    printf( "%-12s : ",     Cba_ManName(p) );
+    printf( "pi =%5d  ",    Cba_NtkPiNum(pRoot) );
+    printf( "po =%5d  ",    Cba_NtkPoNum(pRoot) );
+    printf( "mod =%6d  ",   Cba_ManNtkNum(p) );
+    printf( "box =%5d  ",   nPrims + nUsers );
+    printf( "prim =%5d  ",  nPrims );
+    printf( "user =%5d  ",  nUsers );
     printf( "mem =%6.3f MB", 1.0*Cba_ManMemory(p)/(1<<20) );
     printf( "\n" );
-    Cba_ManBoxNum( p );
     Cba_ManForEachNtk( p, pNtk, i )
     {
         if ( i == nModules+1 )
@@ -867,146 +876,20 @@ static inline void Cba_ManPrintStats( Cba_Man_t * p, int nModules, int fVerbose
 
 
 
-/**Function*************************************************************
-
-  Synopsis    [Other APIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Cba_ObjType_t Ptr_SopToType( char * pSop )
-{
-    if ( !strcmp(pSop, " 0\n") )         return CBA_BOX_CF;
-    if ( !strcmp(pSop, " 1\n") )         return CBA_BOX_CT;
-    if ( !strcmp(pSop, "1 1\n") )        return CBA_BOX_BUF;
-    if ( !strcmp(pSop, "0 1\n") )        return CBA_BOX_INV;
-    if ( !strcmp(pSop, "11 1\n") )       return CBA_BOX_AND;
-    if ( !strcmp(pSop, "00 1\n") )       return CBA_BOX_NOR;
-    if ( !strcmp(pSop, "00 0\n") )       return CBA_BOX_OR;
-    if ( !strcmp(pSop, "-1 1\n1- 1\n") ) return CBA_BOX_OR;
-    if ( !strcmp(pSop, "1- 1\n-1 1\n") ) return CBA_BOX_OR;
-    if ( !strcmp(pSop, "01 1\n10 1\n") ) return CBA_BOX_XOR;
-    if ( !strcmp(pSop, "10 1\n01 1\n") ) return CBA_BOX_XOR;
-    if ( !strcmp(pSop, "11 1\n00 1\n") ) return CBA_BOX_XNOR;
-    if ( !strcmp(pSop, "00 1\n11 1\n") ) return CBA_BOX_XNOR;
-    if ( !strcmp(pSop, "10 1\n") )       return CBA_BOX_SHARP;
-    if ( !strcmp(pSop, "01 1\n") )       return CBA_BOX_SHARPL;
-    assert( 0 );
-    return CBA_OBJ_NONE;
-}
-static inline char * Ptr_SopToTypeName( char * pSop )
-{
-    if ( !strcmp(pSop, " 0\n") )         return "CBA_BOX_C0";
-    if ( !strcmp(pSop, " 1\n") )         return "CBA_BOX_C1";
-    if ( !strcmp(pSop, "1 1\n") )        return "CBA_BOX_BUF";
-    if ( !strcmp(pSop, "0 1\n") )        return "CBA_BOX_INV";
-    if ( !strcmp(pSop, "11 1\n") )       return "CBA_BOX_AND";
-    if ( !strcmp(pSop, "00 1\n") )       return "CBA_BOX_NOR";
-    if ( !strcmp(pSop, "00 0\n") )       return "CBA_BOX_OR";
-    if ( !strcmp(pSop, "-1 1\n1- 1\n") ) return "CBA_BOX_OR";
-    if ( !strcmp(pSop, "1- 1\n-1 1\n") ) return "CBA_BOX_OR";
-    if ( !strcmp(pSop, "01 1\n10 1\n") ) return "CBA_BOX_XOR";
-    if ( !strcmp(pSop, "10 1\n01 1\n") ) return "CBA_BOX_XOR";
-    if ( !strcmp(pSop, "11 1\n00 1\n") ) return "CBA_BOX_XNOR";
-    if ( !strcmp(pSop, "00 1\n11 1\n") ) return "CBA_BOX_XNOR";
-    if ( !strcmp(pSop, "10 1\n") )       return "CBA_BOX_SHARP";
-    if ( !strcmp(pSop, "01 1\n") )       return "CBA_BOX_SHARPL";
-    assert( 0 );
-    return NULL;
-}
-static inline char * Ptr_TypeToName( Cba_ObjType_t Type )
-{
-    if ( Type == CBA_BOX_CF )    return "const0";
-    if ( Type == CBA_BOX_CT )    return "const1";
-    if ( Type == CBA_BOX_CX )    return "constX";
-    if ( Type == CBA_BOX_CZ )    return "constZ";
-    if ( Type == CBA_BOX_BUF )   return "buf";
-    if ( Type == CBA_BOX_INV )   return "not";
-    if ( Type == CBA_BOX_AND )   return "and";
-    if ( Type == CBA_BOX_NAND )  return "nand";
-    if ( Type == CBA_BOX_OR )    return "or";
-    if ( Type == CBA_BOX_NOR )   return "nor";
-    if ( Type == CBA_BOX_XOR )   return "xor";
-    if ( Type == CBA_BOX_XNOR )  return "xnor";
-    if ( Type == CBA_BOX_MUX )   return "mux";
-    if ( Type == CBA_BOX_MAJ )   return "maj";
-    if ( Type == CBA_BOX_SHARP ) return "sharp";
-    if ( Type == CBA_BOX_SHARPL) return "sharpl";
-    assert( 0 );
-    return "???";
-}
-static inline char * Ptr_TypeToSop( Cba_ObjType_t Type )
-{
-    if ( Type == CBA_BOX_CF )    return " 0\n";
-    if ( Type == CBA_BOX_CT )    return " 1\n";
-    if ( Type == CBA_BOX_CX )    return " 0\n";
-    if ( Type == CBA_BOX_CZ )    return " 0\n";
-    if ( Type == CBA_BOX_BUF )   return "1 1\n";
-    if ( Type == CBA_BOX_INV )   return "0 1\n";
-    if ( Type == CBA_BOX_AND )   return "11 1\n";
-    if ( Type == CBA_BOX_NAND )  return "11 0\n";
-    if ( Type == CBA_BOX_OR )    return "00 0\n";
-    if ( Type == CBA_BOX_NOR )   return "00 1\n";
-    if ( Type == CBA_BOX_XOR )   return "01 1\n10 1\n";
-    if ( Type == CBA_BOX_XNOR )  return "00 1\n11 1\n";
-    if ( Type == CBA_BOX_SHARP ) return "10 1\n";
-    if ( Type == CBA_BOX_SHARPL) return "01 1\n";
-    if ( Type == CBA_BOX_MUX )   return "11- 1\n0-1 1\n";
-    if ( Type == CBA_BOX_MAJ )   return "11- 1\n1-1 1\n-11 1\n";
-    assert( 0 );
-    return "???";
-}
-
-/*=== cbaCom.c ===============================================================*/
-extern void          Abc_FrameImportPtr( Vec_Ptr_t * vPtr );
-extern Vec_Ptr_t *   Abc_FrameExportPtr();
-
 /*=== cbaBlast.c =============================================================*/
-extern int           Cba_NtkBuildLibrary( Cba_Man_t * p );
-extern Gia_Man_t *   Cba_ManExtract( Cba_Man_t * p, int fBuffers, int fVerbose );
-extern Cba_Man_t *   Cba_ManInsertGia( Cba_Man_t * p, Gia_Man_t * pGia );
-extern void *        Cba_ManInsertAbc( Cba_Man_t * p, void * pAbc );
 /*=== cbaCba.c ===============================================================*/
-extern Cba_Man_t *   Cba_ManReadCba( char * pFileName );
-extern void          Cba_ManWriteCba( char * pFileName, Cba_Man_t * p );
+/*=== cbaCom.c ===============================================================*/
 /*=== cbaNtk.c ===============================================================*/
-extern char *        Cba_NtkGenerateName( Cba_Ntk_t * p, Cba_ObjType_t Type, Vec_Int_t * vBits );
-extern Cba_ObjType_t Cba_NameToType( char * pName );
-extern Vec_Int_t *   Cba_NameToRanges( char * pName );
-extern void          Cba_NtkUpdateFanout( Cba_Ntk_t * p, int iOld, int iNew );
-extern void          Cba_ManDeriveFanout( Cba_Man_t * p );
-//extern void          Cba_ManAssignInternNames( Cba_Man_t * p );
-extern void          Cba_ManAssignInternWordNames( Cba_Man_t * p );
-extern Cba_Man_t *   Cba_ManCollapse( Cba_Man_t * p );
-extern void          Cba_ManSetupTypes( char ** pNames, char ** pSymbs );
-/*=== cbaPtr.c ===============================================================*/
-extern void          Cba_PtrFree( Vec_Ptr_t * vDes );
-extern int           Cba_PtrMemory( Vec_Ptr_t * vDes );
-extern void          Cba_PtrDumpBlif( char * pFileName, Vec_Ptr_t * vDes );
-extern void          Cba_PtrDumpVerilog( char * pFileName, Vec_Ptr_t * vDes );
-extern Vec_Ptr_t *   Cba_PtrTransformTest( Vec_Ptr_t * vDes );
-/*=== cbaPtrAbc.c ============================================================*/
-extern Cba_Man_t *   Cba_PtrTransformToCba( Vec_Ptr_t * vDes );
-extern Vec_Ptr_t *   Cba_PtrDeriveFromCba( Cba_Man_t * p );
-/*=== cbaPrsBuild.c ==========================================================*/
-extern void          Prs_ManVecFree( Vec_Ptr_t * vPrs );
-extern Cba_Man_t *   Prs_ManBuildCba( char * pFileName, Vec_Ptr_t * vDes );
 /*=== cbaReadBlif.c ==========================================================*/
 extern Vec_Ptr_t *   Prs_ManReadBlif( char * pFileName );
-/*=== cbaReadSmt.c ===========================================================*/
-extern Vec_Ptr_t *   Prs_ManReadSmt( char * pFileName );
 /*=== cbaReadVer.c ===========================================================*/
 extern Vec_Ptr_t *   Prs_ManReadVerilog( char * pFileName );
 /*=== cbaWriteBlif.c =========================================================*/
-extern void          Prs_ManWriteBlif( char * pFileName, Vec_Ptr_t * p );
-extern void          Cba_ManWriteBlif( char * pFileName, Cba_Man_t * p );
+//extern void          Prs_ManWriteBlif( char * pFileName, Vec_Ptr_t * p );
+//extern void          Cba_ManWriteBlif( char * pFileName, Cba_Man_t * p );
 /*=== cbaWriteVer.c ==========================================================*/
-extern void          Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * p );
-extern void          Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p, int fUseAssign );
+//extern void          Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * p );
+//extern void          Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p, int fUseAssign );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c
index b659bf3d..87a5b5cd 100644
--- a/src/base/cba/cbaBlast.c
+++ b/src/base/cba/cbaBlast.c
@@ -1,28 +1,24 @@
 /**CFile****************************************************************
 
-  FileName    [cbaBlast.c]
+  FileName    [cba.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Hierarchical word-level netlist.]
+  PackageName [Verilog parser.]
 
-  Synopsis    [Bit-blasting of the netlist.]
+  Synopsis    [Parses several flavors of word-level Verilog.]
 
   Author      [Alan Mishchenko]
   
   Affiliation [UC Berkeley]
 
-  Date        [Ver. 1.0. Started - November 29, 2014.]
+  Date        [Ver. 1.0. Started - July 21, 2015.]
 
-  Revision    [$Id: cbaBlast.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+  Revision    [$Id: cba.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
 #include "cba.h"
-#include "base/abc/abc.h"
-#include "map/mio/mio.h"
-#include "bool/dec/dec.h"
-#include "base/main/mainInt.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -45,539 +41,8 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Cba_ManPrepareGates( Cba_Man_t * p )
-{
-    Dec_Graph_t ** ppGraphs; int i;
-    if ( p->pMioLib == NULL )
-        return;
-    ppGraphs = ABC_CALLOC( Dec_Graph_t *, Abc_NamObjNumMax(p->pMods) );
-    for ( i = 1; i < Abc_NamObjNumMax(p->pMods); i++ )
-    {
-        char * pGateName = Abc_NamStr( p->pMods, i );
-        Mio_Gate_t * pGate = Mio_LibraryReadGateByName( (Mio_Library_t *)p->pMioLib, pGateName, NULL );
-        if ( pGate != NULL )
-            ppGraphs[i] = Dec_Factor( Mio_GateReadSop(pGate) );
-    }
-    assert( p->ppGraphs == NULL );
-    p->ppGraphs = (void **)ppGraphs;
-}
-void Cba_ManUndoGates( Cba_Man_t * p )
-{
-    int i;
-    if ( p->pMioLib == NULL )
-        return;
-    for ( i = 1; i < Abc_NamObjNumMax(p->pMods); i++ )
-        if ( p->ppGraphs[i] )
-            Dec_GraphFree( (Dec_Graph_t *)p->ppGraphs[i] );
-    ABC_FREE( p->ppGraphs );
-}
 
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cba_ManAddBarbuf( Gia_Man_t * pNew, int iRes, Cba_Man_t * p, int iLNtk, int iLObj, int iRNtk, int iRObj, Vec_Int_t * vMap )
-{
-    int iBufLit, iIdLit;
-    if ( iRes == 0 || iRes == 1 )
-        return iRes;
-    assert( iRes > 0 );
-    if ( vMap && Abc_Lit2Var(iRes) < Vec_IntSize(vMap) && (iIdLit = Vec_IntEntry(vMap, Abc_Lit2Var(iRes))) >= 0 && 
-        Vec_IntEntry(&p->vBuf2LeafNtk, Abc_Lit2Var(iIdLit)) == iLNtk && Vec_IntEntry(&p->vBuf2RootNtk, Abc_Lit2Var(iIdLit)) == iRNtk )
-        return Abc_LitNotCond( Vec_IntEntry(pNew->vBarBufs, Abc_Lit2Var(iIdLit)), Abc_LitIsCompl(iRes) ^ Abc_LitIsCompl(iIdLit) );
-    assert( Cba_ManNtkIsOk(p, iLNtk) && Cba_ManNtkIsOk(p, iRNtk) );
-    Vec_IntPush( &p->vBuf2LeafNtk, iLNtk );
-    Vec_IntPush( &p->vBuf2LeafObj, iLObj );
-    Vec_IntPush( &p->vBuf2RootNtk, iRNtk );
-    Vec_IntPush( &p->vBuf2RootObj, iRObj );
-    iBufLit = Gia_ManAppendBuf( pNew, iRes );
-    if ( vMap )
-    {
-        Vec_IntSetEntryFull( vMap, Abc_Lit2Var(iRes), Abc_Var2Lit(Vec_IntSize(pNew->vBarBufs), Abc_LitIsCompl(iRes)) );
-        Vec_IntPush( pNew->vBarBufs, iBufLit );
-    }
-    return iBufLit;
-}
-int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, int fBuffers, Vec_Int_t * vMap )
-{
-    int iRes = Cba_ObjCopy( p, i );
-    if ( iRes >= 0 )
-        return iRes;
-    if ( Cba_ObjIsCo(p, i) )
-        iRes = Cba_ManExtract_rec( pNew, p, Cba_ObjFanin(p, i), fBuffers, vMap );
-    else if ( Cba_ObjIsPi(p, i) )
-    {
-        Cba_Ntk_t * pHost = Cba_NtkHostNtk( p );
-        int iObj = Cba_BoxBi( pHost, Cba_NtkHostObj(p), Cba_ObjIndex(p, i) );
-        iRes = Cba_ManExtract_rec( pNew, pHost, iObj, fBuffers, vMap );
-        if ( fBuffers )
-            iRes = Cba_ManAddBarbuf( pNew, iRes, p->pDesign, Cba_NtkId(p), i, Cba_NtkId(pHost), iObj, vMap );
-    }
-    else if ( Cba_ObjIsBo(p, i) )
-    {
-        int iBox = Cba_BoxBoBox(p, i);
-        if ( Cba_ObjIsBoxUser(p, iBox) ) // user box
-        {
-            Cba_Ntk_t * pBox = Cba_BoxBoNtk( p, i );
-            int iObj = Cba_NtkPo( pBox, Cba_ObjIndex(p, i) );
-            iRes = Cba_ManExtract_rec( pNew, pBox, iObj, fBuffers, vMap );
-            if ( fBuffers )
-                iRes = Cba_ManAddBarbuf( pNew, iRes, p->pDesign, Cba_NtkId(p), i, Cba_NtkId(pBox), iObj, vMap );
-        }
-        else // primitive
-        {
-            int iFanin, nLits, pLits[16];
-            assert( Cba_ObjIsBoxPrim(p, iBox) );
-            Cba_BoxForEachFanin( p, iBox, iFanin, nLits )
-                pLits[nLits] = Cba_ManExtract_rec( pNew, p, iFanin, fBuffers, vMap );
-            assert( nLits <= 16 );
-            if ( p->pDesign->ppGraphs ) // mapped gate
-            {
-                extern int Gia_ManFactorGraph( Gia_Man_t * p, Dec_Graph_t * pFForm, Vec_Int_t * vLeaves );
-                Dec_Graph_t * pGraph = (Dec_Graph_t *)p->pDesign->ppGraphs[Cba_BoxNtkId(p, iBox)];
-                Vec_Int_t Leaves = { nLits, nLits, pLits };
-                assert( pGraph != NULL );
-                return Gia_ManFactorGraph( pNew, pGraph, &Leaves );
-            }
-            else
-            {
-                Cba_ObjType_t Type = Cba_ObjType(p, iBox);
-                if ( nLits == 0 )
-                {
-                    if ( Type == CBA_BOX_CF )
-                        iRes = 0;
-                    else if ( Type == CBA_BOX_CT )
-                        iRes = 1;
-                    else assert( 0 );
-                }
-                else if ( nLits == 1 )
-                {
-                    if ( Type == CBA_BOX_BUF )
-                        iRes = pLits[0];
-                    else if ( Type == CBA_BOX_INV )
-                        iRes = Abc_LitNot( pLits[0] );
-                    else assert( 0 );
-                }
-                else if ( nLits == 2 )
-                {
-                    if ( Type == CBA_BOX_AND )
-                        iRes = Gia_ManHashAnd( pNew, pLits[0], pLits[1] );
-                    else if ( Type == CBA_BOX_NAND )
-                        iRes = Abc_LitNot( Gia_ManHashAnd( pNew, pLits[0], pLits[1] ) );
-                    else if ( Type == CBA_BOX_OR )
-                        iRes = Gia_ManHashOr( pNew, pLits[0], pLits[1] );
-                    else if ( Type == CBA_BOX_NOR )
-                        iRes = Abc_LitNot( Gia_ManHashOr( pNew, pLits[0], pLits[1] ) );
-                    else if ( Type == CBA_BOX_XOR )
-                        iRes = Gia_ManHashXor( pNew, pLits[0], pLits[1] );
-                    else if ( Type == CBA_BOX_XNOR )
-                        iRes = Abc_LitNot( Gia_ManHashXor( pNew, pLits[0], pLits[1] ) );
-                    else if ( Type == CBA_BOX_SHARP )
-                        iRes = Gia_ManHashAnd( pNew, pLits[0], Abc_LitNot(pLits[1]) );
-                    else if ( Type == CBA_BOX_SHARPL )
-                        iRes = Gia_ManHashAnd( pNew, Abc_LitNot(pLits[0]), pLits[1] );
-                    else assert( 0 );
-                }
-                else if ( nLits == 3 )
-                {
-                    if ( Type == CBA_BOX_MUX )
-                        iRes = Gia_ManHashMux( pNew, pLits[0], pLits[1], pLits[2] );
-                    else if ( Type == CBA_BOX_MAJ )
-                        iRes = Gia_ManHashMaj( pNew, pLits[0], pLits[1], pLits[2] );
-                    else if ( Type == CBA_BOX_ADD )
-                    {
-                        int iRes0 = Gia_ManHashAnd( pNew, pLits[1], pLits[2] );
-                        int iRes1 = Gia_ManHashOr( pNew, pLits[1], pLits[2] );
-                        assert( Cba_BoxBoNum(p, iBox) == 2 );
-                        if ( Cba_BoxBo(p, iBox, 0) == i ) // sum
-                            iRes = Gia_ManHashXor( pNew, pLits[0], Gia_ManHashAnd(pNew, Abc_LitNot(iRes0), iRes1) );
-                        else if ( Cba_BoxBo(p, iBox, 1) == i ) // cout
-                            iRes = Gia_ManHashOr( pNew, iRes0, Gia_ManHashAnd(pNew, pLits[0], iRes1) );
-                        else assert( 0 );
-                    }
-                    else assert( 0 );
-                }
-                else assert( 0 );
-            }
-        }
-    }
-    else assert( 0 );
-    Cba_ObjSetCopy( p, i, iRes );
-    return iRes;
-}
-Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fBuffers, int fVerbose )
-{
-    Cba_Ntk_t * pNtk, * pRoot = Cba_ManRoot(p);
-    Gia_Man_t * pNew, * pTemp; 
-    Vec_Int_t * vMap = NULL;
-    int i, iObj;
-
-    Vec_IntClear( &p->vBuf2LeafNtk );
-    Vec_IntClear( &p->vBuf2LeafObj );
-    Vec_IntClear( &p->vBuf2RootNtk );
-    Vec_IntClear( &p->vBuf2RootObj );
-
-    Cba_ManForEachNtk( p, pNtk, i )
-    {
-        Cba_NtkDeriveIndex( pNtk );
-        Cba_NtkStartCopies( pNtk );
-    }
-
-    // start the manager
-    pNew = Gia_ManStart( Cba_ManNodeNum(p) );
-    pNew->pName = Abc_UtilStrsav(p->pName);
-    pNew->pSpec = Abc_UtilStrsav(p->pSpec);
-
-    // primary inputs
-    Cba_NtkForEachPi( pRoot, iObj, i )
-        Cba_ObjSetCopy( pRoot, iObj, Gia_ManAppendCi(pNew) );
-
-    // internal nodes
-    Gia_ManHashAlloc( pNew );
-    pNew->vBarBufs = Vec_IntAlloc( 10000 );
-    vMap = Vec_IntStartFull( 10000 );
-    Cba_ManPrepareGates( p );
-    Cba_NtkForEachPo( pRoot, iObj, i )
-        Cba_ManExtract_rec( pNew, pRoot, iObj, fBuffers, vMap );
-    Cba_ManUndoGates( p );
-    Vec_IntFreeP( &vMap );
-    Gia_ManHashStop( pNew );
-
-    // primary outputs
-    Cba_NtkForEachPo( pRoot, iObj, i )
-        Gia_ManAppendCo( pNew, Cba_ObjCopy(pRoot, iObj) );
-    assert( Vec_IntSize(&p->vBuf2LeafNtk) == pNew->nBufs );
-
-    // cleanup
-    pNew = Gia_ManCleanup( pTemp = pNew );
-    Gia_ManStop( pTemp );
-    //Gia_ManPrintStats( pNew, NULL );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Mark each GIA node with the network it belongs to.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cba_ManMarkNodesGia( Cba_Man_t * p, Gia_Man_t * pGia )
-{
-    Gia_Obj_t * pObj; int i, Count = 0;
-    assert( Vec_IntSize(&p->vBuf2LeafNtk) == Gia_ManBufNum(pGia) );
-    Gia_ManConst0(pGia)->Value = 1;
-    Gia_ManForEachPi( pGia, pObj, i )
-        pObj->Value = 1;
-    Gia_ManForEachAnd( pGia, pObj, i )
-    {
-        if ( Gia_ObjIsBuf(pObj) )
-            pObj->Value = Vec_IntEntry( &p->vBuf2LeafNtk, Count++ );
-        else
-        {
-            pObj->Value = Gia_ObjFanin0(pObj)->Value;
-            assert( pObj->Value == Gia_ObjFanin1(pObj)->Value );
-        }
-    }
-    assert( Count == Gia_ManBufNum(pGia) );
-    Gia_ManForEachPo( pGia, pObj, i )
-    {
-        assert( Gia_ObjFanin0(pObj)->Value == 1 );
-        pObj->Value = 1;
-    }
-}
-void Cba_ManRemapBarbufs( Cba_Man_t * pNew, Cba_Man_t * p )
-{
-    Cba_Ntk_t * pNtk;  int Entry, i;
-    //assert( Vec_IntSize(&p->vBuf2RootNtk) );
-    assert( !Vec_IntSize(&pNew->vBuf2RootNtk) );
-    Vec_IntAppend( &pNew->vBuf2RootNtk, &p->vBuf2RootNtk );
-    Vec_IntAppend( &pNew->vBuf2RootObj, &p->vBuf2RootObj );
-    Vec_IntAppend( &pNew->vBuf2LeafNtk, &p->vBuf2LeafNtk );
-    Vec_IntAppend( &pNew->vBuf2LeafObj, &p->vBuf2LeafObj );
-    Vec_IntForEachEntry( &p->vBuf2LeafObj, Entry, i )
-    {
-        pNtk = Cba_ManNtk( p, Vec_IntEntry(&p->vBuf2LeafNtk, i) );
-        Vec_IntWriteEntry( &pNew->vBuf2LeafObj, i, Cba_ObjCopy(pNtk, Entry) );
-    }
-    Vec_IntForEachEntry( &p->vBuf2RootObj, Entry, i )
-    {
-        pNtk = Cba_ManNtk( p, Vec_IntEntry(&p->vBuf2RootNtk, i) );
-        Vec_IntWriteEntry( &pNew->vBuf2RootObj, i, Cba_ObjCopy(pNtk, Entry) );
-    }
-}
-void Cba_NtkCreateAndConnectBuffer( Gia_Man_t * pGia, Gia_Obj_t * pObj, Cba_Ntk_t * p, int iTerm )
-{
-    int iObj;
-    if ( pGia && Gia_ObjFaninId0p(pGia, pObj) > 0 )
-    {
-        iObj = Cba_ObjAlloc( p, CBA_OBJ_BI, Gia_ObjFanin0(pObj)->Value );
-        Cba_ObjAlloc( p, Gia_ObjFaninC0(pObj) ? CBA_BOX_INV : CBA_BOX_BUF, -1 );
-    }
-    else
-    {
-        Cba_ObjAlloc( p, pGia && Gia_ObjFaninC0(pObj) ? CBA_BOX_CT : CBA_BOX_CF, -1 );
-    }
-    iObj = Cba_ObjAlloc( p, CBA_OBJ_BO, -1 );
-    Cba_ObjSetFanin( p, iTerm, iObj );
-}
-void Cba_NtkInsertGia( Cba_Man_t * p, Gia_Man_t * pGia )
-{
-    Cba_Ntk_t * pNtk, * pRoot = Cba_ManRoot( p );
-    int i, j, k, iBox, iTerm, Count = 0;
-    Gia_Obj_t * pObj;
-
-    Gia_ManConst0(pGia)->Value = ~0;
-    Gia_ManForEachPi( pGia, pObj, i )
-        pObj->Value = Cba_NtkPi( pRoot, i );
-    Gia_ManForEachAnd( pGia, pObj, i )
-    {
-        if ( Gia_ObjIsBuf(pObj) )
-        {
-            pNtk = Cba_ManNtk( p, Vec_IntEntry(&p->vBuf2RootNtk, Count) );
-            iTerm = Vec_IntEntry( &p->vBuf2RootObj, Count );
-            assert( Cba_ObjIsCo(pNtk, iTerm) );
-            if ( Cba_ObjFanin(pNtk, iTerm) == -1 ) // not a feedthrough
-                Cba_NtkCreateAndConnectBuffer( pGia, pObj, pNtk, iTerm );
-            // prepare leaf
-            pObj->Value = Vec_IntEntry( &p->vBuf2LeafObj, Count++ );
-        }
-        else
-        {
-            int iLit0 = Gia_ObjFanin0(pObj)->Value;
-            int iLit1 = Gia_ObjFanin1(pObj)->Value;
-            Cba_ObjType_t Type;
-            pNtk = Cba_ManNtk( p, pObj->Value );
-            if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
-                Type = CBA_BOX_NOR;
-            else if ( Gia_ObjFaninC1(pObj) )
-                Type = CBA_BOX_SHARP;
-            else if ( Gia_ObjFaninC0(pObj) )
-            {
-                Type = CBA_BOX_SHARP;
-                ABC_SWAP( int, iLit0, iLit1 );
-            }
-            else 
-                Type = CBA_BOX_AND;
-            // create box
-            iTerm = Cba_ObjAlloc( pNtk, CBA_OBJ_BI, iLit1 );
-            iTerm = Cba_ObjAlloc( pNtk, CBA_OBJ_BI, iLit0 );
-            Cba_ObjAlloc( pNtk, Type, -1 );
-            pObj->Value = Cba_ObjAlloc( pNtk, CBA_OBJ_BO, -1 );
-        }
-    }
-    assert( Count == Gia_ManBufNum(pGia) );
-
-    // create constant 0 drivers for COs without barbufs
-    Cba_ManForEachNtk( p, pNtk, i )
-    {
-        Cba_NtkForEachBox( pNtk, iBox )
-            Cba_BoxForEachBi( pNtk, iBox, iTerm, j )
-                if ( Cba_ObjFanin(pNtk, iTerm) == -1 )
-                    Cba_NtkCreateAndConnectBuffer( NULL, NULL, pNtk, iTerm );
-        Cba_NtkForEachPo( pNtk, iTerm, k )
-            if ( pNtk != pRoot && Cba_ObjFanin(pNtk, iTerm) == -1 )
-                Cba_NtkCreateAndConnectBuffer( NULL, NULL, pNtk, iTerm );
-    }
-    // create node and connect POs
-    Gia_ManForEachPo( pGia, pObj, i )
-        if ( Cba_ObjFanin(pRoot, Cba_NtkPo(pRoot, i)) == -1 ) // not a feedthrough
-            Cba_NtkCreateAndConnectBuffer( pGia, pObj, pRoot, Cba_NtkPo(pRoot, i) );
-}
-Cba_Man_t * Cba_ManInsertGia( Cba_Man_t * p, Gia_Man_t * pGia )
-{
-    Cba_Man_t * pNew = Cba_ManDupUserBoxes( p );
-    Cba_ManMarkNodesGia( p, pGia );
-    Cba_ManRemapBarbufs( pNew, p );
-    Cba_NtkInsertGia( pNew, pGia );
-    Cba_ManMoveNames( pNew, p );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cba_Man_t * Cba_ManBlastTest( Cba_Man_t * p )
-{
-    Gia_Man_t * pGia = Cba_ManExtract( p, 1, 0 );
-    Cba_Man_t * pNew = Cba_ManInsertGia( p, pGia );
-    Gia_ManStop( pGia );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Mark each GIA node with the network it belongs to.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Abc_NodeIsSeriousGate( Abc_Obj_t * p )
-{
-    return Abc_ObjIsNode(p) && Abc_ObjFaninNum(p) > 0 && !Abc_ObjIsBarBuf(p);
-}
-void Cba_ManMarkNodesAbc( Cba_Man_t * p, Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj, * pFanin; int i, k, Count = 0;
-    assert( Vec_IntSize(&p->vBuf2LeafNtk) == pNtk->nBarBufs2 );
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        pObj->iTemp = 1;
-    Abc_NtkForEachNode( pNtk, pObj, i )
-    {
-        if ( Abc_ObjIsBarBuf(pObj) )
-            pObj->iTemp = Vec_IntEntry( &p->vBuf2LeafNtk, Count++ );
-        else if ( Abc_NodeIsSeriousGate(pObj) )
-        {
-            pObj->iTemp = Abc_ObjFanin0(pObj)->iTemp;
-            Abc_ObjForEachFanin( pObj, pFanin, k )
-                assert( pObj->iTemp == pFanin->iTemp );
-        }
-    }
-    Abc_NtkForEachPo( pNtk, pObj, i )
-    {
-        if ( !Abc_NodeIsSeriousGate(Abc_ObjFanin0(pObj)) )
-            continue;
-        assert( Abc_ObjFanin0(pObj)->iTemp == 1 );
-        pObj->iTemp = Abc_ObjFanin0(pObj)->iTemp;
-    }
-    assert( Count == pNtk->nBarBufs2 );
-}
-void Cba_NtkCreateOrConnectFanin( Abc_Obj_t * pFanin, Cba_Ntk_t * p, int iTerm )
-{
-    int iObj;
-    if ( pFanin && Abc_NodeIsSeriousGate(pFanin) )//&& Cba_ObjName(p, pFanin->iTemp) == -1 ) // gate without name
-    {
-        iObj = pFanin->iTemp;
-    }
-    else if ( pFanin && (Abc_ObjIsPi(pFanin) || Abc_ObjIsBarBuf(pFanin) || Abc_NodeIsSeriousGate(pFanin)) ) // PI/BO or gate with name
-    {
-        iObj = Cba_ObjAlloc( p, CBA_OBJ_BI, pFanin->iTemp );
-        Cba_ObjAlloc( p, CBA_BOX_GATE, p->pDesign->ElemGates[2] ); // buffer
-        iObj = Cba_ObjAlloc( p, CBA_OBJ_BO, -1 );
-    }
-    else
-    {
-        assert( !pFanin || Abc_NodeIsConst0(pFanin) || Abc_NodeIsConst1(pFanin) );
-        Cba_ObjAlloc( p, CBA_BOX_GATE, p->pDesign->ElemGates[(pFanin && Abc_NodeIsConst1(pFanin))] ); // const 0/1
-        iObj = Cba_ObjAlloc( p, CBA_OBJ_BO, -1 );
-    }
-    Cba_ObjSetFanin( p, iTerm, iObj );
-}
-void Cba_NtkPrepareLibrary( Cba_Man_t * p, Mio_Library_t * pLib )
-{
-    Mio_Gate_t * pGate;
-    Mio_Gate_t * pGate0 = Mio_LibraryReadConst0( pLib );
-    Mio_Gate_t * pGate1 = Mio_LibraryReadConst1( pLib );
-    Mio_Gate_t * pGate2 = Mio_LibraryReadBuf( pLib );
-    if ( !pGate0 || !pGate1 || !pGate2 )
-    {
-        printf( "The library does not have one of the elementary gates.\n" );
-        return;
-    }
-    p->ElemGates[0] = Abc_NamStrFindOrAdd( p->pMods, Mio_GateReadName(pGate0), NULL );
-    p->ElemGates[1] = Abc_NamStrFindOrAdd( p->pMods, Mio_GateReadName(pGate1), NULL );
-    p->ElemGates[2] = Abc_NamStrFindOrAdd( p->pMods, Mio_GateReadName(pGate2), NULL );
-    Mio_LibraryForEachGate( pLib, pGate )
-        if ( pGate != pGate0 && pGate != pGate1 && pGate != pGate2 )
-            Abc_NamStrFindOrAdd( p->pMods, Mio_GateReadName(pGate), NULL );
-    assert( Abc_NamObjNumMax(p->pMods) > 1 );
-}
-int Cba_NtkBuildLibrary( Cba_Man_t * p )
-{
-    int RetValue = 1;
-    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
-    if ( pLib == NULL )
-        printf( "The standard cell library is not available.\n" ), RetValue = 0;
-    else
-        Cba_NtkPrepareLibrary( p, pLib );
-    p->pMioLib = pLib;
-    return RetValue;
-}
-void Cba_NtkInsertNtk( Cba_Man_t * p, Abc_Ntk_t * pNtk )
-{
-    Cba_Ntk_t * pCbaNtk, * pRoot = Cba_ManRoot( p );
-    int i, j, k, iBox, iTerm, Count = 0;
-    Abc_Obj_t * pObj;
-    assert( Abc_NtkHasMapping(pNtk) );
-    Cba_NtkPrepareLibrary( p, (Mio_Library_t *)pNtk->pManFunc );
-    p->pMioLib = pNtk->pManFunc;
-
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        pObj->iTemp = Cba_NtkPi( pRoot, i );
-    Abc_NtkForEachNode( pNtk, pObj, i )
-    {
-        if ( Abc_ObjIsBarBuf(pObj) )
-        {
-            pCbaNtk = Cba_ManNtk( p, Vec_IntEntry(&p->vBuf2RootNtk, Count) );
-            iTerm = Vec_IntEntry( &p->vBuf2RootObj, Count );
-            assert( Cba_ObjIsCo(pCbaNtk, iTerm) );
-            if ( Cba_ObjFanin(pCbaNtk, iTerm) == -1 ) // not a feedthrough
-                Cba_NtkCreateOrConnectFanin( Abc_ObjFanin0(pObj), pCbaNtk, iTerm );
-            // prepare leaf
-            pObj->iTemp = Vec_IntEntry( &p->vBuf2LeafObj, Count++ );
-        }
-        else if ( Abc_NodeIsSeriousGate(pObj) )
-        {
-            pCbaNtk = Cba_ManNtk( p, pObj->iTemp );
-            for ( k = Abc_ObjFaninNum(pObj)-1; k >= 0; k-- )
-                iTerm = Cba_ObjAlloc( pCbaNtk, CBA_OBJ_BI, Abc_ObjFanin(pObj, k)->iTemp );
-            Cba_ObjAlloc( pCbaNtk, CBA_BOX_GATE, Abc_NamStrFind(p->pMods, Mio_GateReadName((Mio_Gate_t *)pObj->pData)) );
-            pObj->iTemp = Cba_ObjAlloc( pCbaNtk, CBA_OBJ_BO, -1 );
-        }
-    }
-    assert( Count == pNtk->nBarBufs2 );
-
-    // create constant 0 drivers for COs without barbufs
-    Cba_ManForEachNtk( p, pCbaNtk, i )
-    {
-        Cba_NtkForEachBox( pCbaNtk, iBox )
-            Cba_BoxForEachBi( pCbaNtk, iBox, iTerm, j )
-                if ( Cba_ObjFanin(pCbaNtk, iTerm) == -1 )
-                    Cba_NtkCreateOrConnectFanin( NULL, pCbaNtk, iTerm );
-        Cba_NtkForEachPo( pCbaNtk, iTerm, k )
-            if ( pCbaNtk != pRoot && Cba_ObjFanin(pCbaNtk, iTerm) == -1 )
-                Cba_NtkCreateOrConnectFanin( NULL, pCbaNtk, iTerm );
-    }
-    // create node and connect POs
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        if ( Cba_ObjFanin(pRoot, Cba_NtkPo(pRoot, i)) == -1 ) // not a feedthrough
-            Cba_NtkCreateOrConnectFanin( Abc_ObjFanin0(pObj), pRoot, Cba_NtkPo(pRoot, i) );
-}
-void * Cba_ManInsertAbc( Cba_Man_t * p, void * pAbc )
-{
-    Abc_Ntk_t * pNtk = (Abc_Ntk_t *)pAbc;
-    Cba_Man_t * pNew = Cba_ManDupUserBoxes( p );
-    Cba_ManMarkNodesAbc( p, pNtk );
-    Cba_ManRemapBarbufs( pNew, p );
-    Cba_NtkInsertNtk( pNew, pNtk );
-    Cba_ManMoveNames( pNew, p );
-    return pNew;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/cba/cbaCba.c b/src/base/cba/cbaCba.c
index 3a759ab8..87a5b5cd 100644
--- a/src/base/cba/cbaCba.c
+++ b/src/base/cba/cbaCba.c
@@ -1,20 +1,20 @@
 /**CFile****************************************************************
 
-  FileName    [cbaCba.c]
+  FileName    [cba.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Hierarchical word-level netlist.]
+  PackageName [Verilog parser.]
 
-  Synopsis    [Verilog parser.]
+  Synopsis    [Parses several flavors of word-level Verilog.]
 
   Author      [Alan Mishchenko]
   
   Affiliation [UC Berkeley]
 
-  Date        [Ver. 1.0. Started - November 29, 2014.]
+  Date        [Ver. 1.0. Started - July 21, 2015.]
 
-  Revision    [$Id: cbaCba.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+  Revision    [$Id: cba.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -30,10 +30,9 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-
 /**Function*************************************************************
 
-  Synopsis    [Read CBA.]
+  Synopsis    []
 
   Description []
                
@@ -42,252 +41,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int CbaManReadCbaLine( Vec_Str_t * vOut, int * pPos, char * pBuffer, char * pLimit )
-{
-    char c;
-    while ( (c = Vec_StrEntry(vOut, (*pPos)++)) != '\n' && pBuffer < pLimit )
-        *pBuffer++ = c;
-    *pBuffer = 0;
-    return pBuffer < pLimit;
-}
-int CbaManReadCbaNameAndNums( char * pBuffer, int * Num1, int * Num2, int * Num3, int * Num4 )
-{
-    *Num1 = *Num2 = *Num3 = *Num4 = -1;
-    // read name
-    while ( *pBuffer && *pBuffer != ' ' )
-        pBuffer++;
-    if ( !*pBuffer )
-        return 0;
-    assert( *pBuffer == ' ' );
-    *pBuffer = 0;
-    // read Num1
-    *Num1 = atoi(++pBuffer);
-    while ( *pBuffer && *pBuffer != ' ' )
-        pBuffer++;
-    if ( !*pBuffer )
-        return 0;
-    // read Num2
-    assert( *pBuffer == ' ' );
-    *Num2 = atoi(++pBuffer);
-    while ( *pBuffer && *pBuffer != ' ' )
-        pBuffer++;
-    if ( !*pBuffer )
-        return 1;
-    // read Num3
-    assert( *pBuffer == ' ' );
-    *Num3 = atoi(++pBuffer);
-    while ( *pBuffer && *pBuffer != ' ' )
-        pBuffer++;
-    if ( !*pBuffer )
-        return 1;
-    // read Num4
-    assert( *pBuffer == ' ' );
-    *Num4 = atoi(++pBuffer);
-    return 1;
-}
-void Cba_ManReadCbaVecStr( Vec_Str_t * vOut, int * pPos, Vec_Str_t * p, int nSize )
-{
-    memcpy( Vec_StrArray(p), Vec_StrArray(vOut) + *pPos, nSize );
-    *pPos += nSize;
-    p->nSize = nSize;
-    assert( Vec_StrSize(p) == Vec_StrCap(p) );
-}
-void Cba_ManReadCbaVecInt( Vec_Str_t * vOut, int * pPos, Vec_Int_t * p, int nSize )
-{
-    memcpy( Vec_IntArray(p), Vec_StrArray(vOut) + *pPos, nSize );
-    *pPos += nSize;
-    p->nSize = nSize / 4;
-    assert( Vec_IntSize(p) == Vec_IntCap(p) );
-}
-void Cba_ManReadCbaNtk( Vec_Str_t * vOut, int * pPos, Cba_Ntk_t * pNtk )
-{
-    int i, Type;
-    //char * pName; int iObj, NameId;
-    Cba_ManReadCbaVecStr( vOut, pPos, &pNtk->vType,      Cba_NtkObjNumAlloc(pNtk) );
-    Cba_ManReadCbaVecInt( vOut, pPos, &pNtk->vFanin, 4 * Cba_NtkObjNumAlloc(pNtk) );
-    Cba_ManReadCbaVecInt( vOut, pPos, &pNtk->vInfo, 12 * Cba_NtkInfoNumAlloc(pNtk) );
-    Cba_NtkForEachObjType( pNtk, Type, i )
-    {
-        if ( Type == CBA_OBJ_PI )
-            Vec_IntPush( &pNtk->vInputs, i );
-        if ( Type == CBA_OBJ_PO )
-            Vec_IntPush( &pNtk->vOutputs, i );
-    }
-    assert( Cba_NtkPiNum(pNtk)  == Cba_NtkPiNumAlloc(pNtk) );
-    assert( Cba_NtkPoNum(pNtk)  == Cba_NtkPoNumAlloc(pNtk) );
-    assert( Cba_NtkObjNum(pNtk) == Cba_NtkObjNumAlloc(pNtk) );
-    assert( Cba_NtkInfoNum(pNtk) == Cba_NtkInfoNumAlloc(pNtk) );
-/*
-    // read input/output/box names
-    Cba_NtkForEachPiMain( pNtk, iObj, i )
-    {
-        pName = Vec_StrEntryP( vOut, Pos );     
-        NameId = Abc_NamStrFindOrAdd( p->pStrs, pName, NULL );
-        Pos += strlen(pName) + 1;
-    }
-    Cba_NtkForEachPoMain( pNtk, iObj, i )
-    {
-        pName = Vec_StrEntryP( vOut, Pos );     
-        NameId = Abc_NamStrFindOrAdd( p->pStrs, pName, NULL );
-        Pos += strlen(pName) + 1;
-    }
-    Cba_NtkForEachBox( pNtk, iObj )
-    {
-        pName = Vec_StrEntryP( vOut, Pos );     
-        NameId = Abc_NamStrFindOrAdd( p->pStrs, pName, NULL );
-        Pos += strlen(pName) + 1;
-    }
-*/
-}
-Cba_Man_t * Cba_ManReadCbaInt( Vec_Str_t * vOut )
-{
-    Cba_Man_t * p;
-    Cba_Ntk_t * pNtk;
-    char Buffer[1000] = "#"; 
-    int i, NameId, Pos = 0, nNtks, Num1, Num2, Num3, Num4;
-    while ( Buffer[0] == '#' )
-        if ( !CbaManReadCbaLine(vOut, &Pos, Buffer, Buffer+1000) )
-            return NULL;
-    if ( !CbaManReadCbaNameAndNums(Buffer, &nNtks, &Num2, &Num3, &Num4) )
-        return NULL;
-    // start manager
-    assert( nNtks > 0 );
-    p = Cba_ManAlloc( Buffer, nNtks );
-    // start networks
-    Cba_ManForEachNtk( p, pNtk, i )
-    {
-        if ( !CbaManReadCbaLine(vOut, &Pos, Buffer, Buffer+1000) )
-        {
-            Cba_ManFree( p );
-            return NULL;
-        }
-        if ( !CbaManReadCbaNameAndNums(Buffer, &Num1, &Num2, &Num3, &Num4) )
-        {
-            Cba_ManFree( p );
-            return NULL;
-        }
-        assert( Num1 >= 0 && Num2 >= 0 && Num3 >= 0 );
-        NameId = Abc_NamStrFindOrAdd( p->pStrs, Buffer, NULL );
-        Cba_NtkAlloc( pNtk, NameId, Num1, Num2, Num3 );
-        Vec_IntFill( &pNtk->vInfo, 3 * Num4, -1 );
-    }
-    // read networks
-    Cba_ManForEachNtk( p, pNtk, i )
-        Cba_ManReadCbaNtk( vOut, &Pos, pNtk );
-    assert( Cba_ManNtkNum(p) == nNtks );
-    assert( Pos == Vec_StrSize(vOut) );
-    return p;
-}
-Cba_Man_t * Cba_ManReadCba( char * pFileName )
-{
-    Cba_Man_t * p;
-    FILE * pFile;
-    Vec_Str_t * vOut;
-    int nFileSize;
-    pFile = fopen( pFileName, "rb" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
-        return NULL;
-    }
-    // get the file size, in bytes
-    fseek( pFile, 0, SEEK_END );  
-    nFileSize = ftell( pFile );  
-    rewind( pFile ); 
-    // load the contents
-    vOut = Vec_StrAlloc( nFileSize );
-    vOut->nSize = vOut->nCap;
-    assert( nFileSize == Vec_StrSize(vOut) );
-    nFileSize = fread( Vec_StrArray(vOut), 1, Vec_StrSize(vOut), pFile );
-    assert( nFileSize == Vec_StrSize(vOut) );
-    fclose( pFile );
-    // read the networks
-    p = Cba_ManReadCbaInt( vOut );
-    if ( p != NULL )
-    {
-        ABC_FREE( p->pSpec );
-        p->pSpec = Abc_UtilStrsav( pFileName );
-    }
-    Vec_StrFree( vOut );
-    return p;
-}
-
-/**Function*************************************************************
 
-  Synopsis    [Write CBA.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cba_ManWriteCbaNtk( Vec_Str_t * vOut, Cba_Ntk_t * pNtk )
-{
-    //char * pName; int iObj, NameId;
-    Vec_StrPushBuffer( vOut, (char *)Vec_StrArray(&pNtk->vType),       Cba_NtkObjNum(pNtk) );
-    Vec_StrPushBuffer( vOut, (char *)Vec_IntArray(&pNtk->vFanin),  4 * Cba_NtkObjNum(pNtk) );
-    Vec_StrPushBuffer( vOut, (char *)Vec_IntArray(&pNtk->vInfo),  12 * Cba_NtkInfoNum(pNtk) );
-/*
-    // write input/output/box names
-    Cba_NtkForEachPiMain( pNtk, iObj, i )
-    {
-        pName = Cba_ObjNameStr( pNtk, iObj );
-        Vec_StrPrintStr( vOut, pName );
-        Vec_StrPush( vOut, '\0' );
-    }
-    Cba_NtkForEachPoMain( pNtk, iObj, i )
-    {
-        pName = Cba_ObjNameStr( pNtk, iObj );
-        Vec_StrPrintStr( vOut, pName );
-        Vec_StrPush( vOut, '\0' );
-    }
-    Cba_NtkForEachBox( pNtk, iObj )
-    {
-        pName = Cba_ObjNameStr( pNtk, iObj );  
-        Vec_StrPrintStr( vOut, pName );
-        Vec_StrPush( vOut, '\0' );
-    }
-*/
-}
-void Cba_ManWriteCbaInt( Vec_Str_t * vOut, Cba_Man_t * p )
-{
-    char Buffer[1000];
-    Cba_Ntk_t * pNtk; int i;
-    sprintf( Buffer, "# Design \"%s\" written by ABC on %s\n", Cba_ManName(p), Extra_TimeStamp() );
-    Vec_StrPrintStr( vOut, Buffer );
-    // write short info
-    sprintf( Buffer, "%s %d \n", Cba_ManName(p), Cba_ManNtkNum(p) );
-    Vec_StrPrintStr( vOut, Buffer );
-    Cba_ManForEachNtk( p, pNtk, i )
-    {
-        sprintf( Buffer, "%s %d %d %d %d \n", Cba_NtkName(pNtk), 
-            Cba_NtkPiNum(pNtk), Cba_NtkPoNum(pNtk), Cba_NtkObjNum(pNtk), Cba_NtkInfoNum(pNtk) );
-        Vec_StrPrintStr( vOut, Buffer );
-    }
-    Cba_ManForEachNtk( p, pNtk, i )
-        Cba_ManWriteCbaNtk( vOut, pNtk );
-}
-void Cba_ManWriteCba( char * pFileName, Cba_Man_t * p )
-{
-    Vec_Str_t * vOut;
-    assert( p->pMioLib == NULL );
-    vOut = Vec_StrAlloc( 10000 );
-    Cba_ManWriteCbaInt( vOut, p );
-    if ( Vec_StrSize(vOut) > 0 )
-    {
-        FILE * pFile = fopen( pFileName, "wb" );
-        if ( pFile == NULL )
-            printf( "Cannot open file \"%s\" for writing.\n", pFileName );
-        else
-        {
-            fwrite( Vec_StrArray(vOut), 1, Vec_StrSize(vOut), pFile );
-            fclose( pFile );
-        }
-    }
-    Vec_StrFree( vOut );    
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index 1a653d80..d1ad95c5 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -47,48 +47,6 @@ static inline void        Cba_AbcUpdateMan( Abc_Frame_t * pAbc, Cba_Man_t * p )
 
 /**Function********************************************************************
 
-  Synopsis    [Accessing current Cba_Ntk_t.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-void Abc_FrameImportPtr( Vec_Ptr_t * vPtr )
-{
-    Cba_Man_t * p;
-    if ( Abc_FrameGetGlobalFrame() == NULL )
-    {
-        printf( "ABC framework is not started.\n" );
-        return;
-    }
-    p = Cba_PtrTransformToCba( vPtr );
-    if ( p == NULL )
-        printf( "Converting from Ptr failed.\n" );
-    Cba_AbcUpdateMan( Abc_FrameGetGlobalFrame(), p );
-}
-Vec_Ptr_t * Abc_FrameExportPtr()
-{
-    Vec_Ptr_t * vPtr;
-    Cba_Man_t * p;
-    if ( Abc_FrameGetGlobalFrame() == NULL )
-    {
-        printf( "ABC framework is not started.\n" );
-        return NULL;
-    }
-    p = Cba_AbcGetMan( Abc_FrameGetGlobalFrame() );
-    if ( p == NULL )
-        printf( "There is no CBA design present.\n" );
-    vPtr = Cba_PtrDeriveFromCba( p );
-    if ( vPtr == NULL )
-        printf( "Converting to Ptr has failed.\n" );
-    return vPtr;
-}
-
-/**Function********************************************************************
-
   Synopsis    []
 
   Description []
@@ -181,6 +139,8 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     fclose( pFile );
+
+#if 0
     // perform reading
     if ( fUseAbc || fUsePtr )
     {
@@ -230,6 +190,8 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     Cba_AbcUpdateMan( pAbc, p );
+
+#endif
     return 0;
 usage:
     Abc_Print( -2, "usage: @read [-apvh] <file_name>\n" );
@@ -284,6 +246,8 @@ int Cba_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Cba_CommandWrite(): There is no current design.\n" );
         return 0;
     }
+
+#if 0
     if ( argc == globalUtilOptind + 1 )
         pFileName = argv[globalUtilOptind];
     else if ( argc == globalUtilOptind && p )
@@ -319,6 +283,8 @@ int Cba_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Unrecognized output file extension.\n" );
         return 0;
     }
+
+#endif
     return 0;
 usage:
     Abc_Print( -2, "usage: @write [-apvh]\n" );
@@ -376,7 +342,11 @@ int Cba_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Cba_CommandPs(): There is no current design.\n" );
         return 0;
     }
+
+#if 0
     Cba_ManPrintStats( p, nModules, fVerbose );
+
+#endif
     return 0;
 usage:
     Abc_Print( -2, "usage: @ps [-M num] [-vh]\n" );
@@ -425,6 +395,8 @@ int Cba_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Cba_CommandPut(): There is no current design.\n" );
         return 0;
     }
+
+#if 0
     pGia = Cba_ManExtract( p, fBarBufs, fVerbose );
     if ( pGia == NULL )
     {
@@ -432,6 +404,8 @@ int Cba_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     Abc_FrameUpdateGia( pAbc, pGia );
+
+#endif
     return 0;
 usage:
     Abc_Print( -2, "usage: @put [-bvh]\n" );
@@ -479,6 +453,8 @@ int Cba_CommandGet( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Cba_CommandGet(): There is no current design.\n" );
         return 0;
     }
+
+#if 0
     if ( fMapped )
     {
         if ( pAbc->pNtkCur == NULL )
@@ -498,10 +474,12 @@ int Cba_CommandGet( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNew = Cba_ManInsertGia( p, pAbc->pGia );
     }
     Cba_AbcUpdateMan( pAbc, pNew );
+
+#endif
     return 0;
 usage:
     Abc_Print( -2, "usage: @get [-mvh]\n" );
-    Abc_Print( -2, "\t         inserts AIG or mapped network into the hierarchical design\n" );
+    Abc_Print( -2, "\t         extracts AIG or mapped network into the hierarchical design\n" );
     Abc_Print( -2, "\t-m     : toggle using mapped network from main-space [default = %s]\n", fMapped? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -542,8 +520,12 @@ int Cba_CommandClp( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Cba_CommandGet(): There is no current design.\n" );
         return 0;
     }
+
+#if 0
     pNew = Cba_ManCollapse( p );
     Cba_AbcUpdateMan( pAbc, pNew );
+
+#endif
     return 0;
 usage:
     Abc_Print( -2, "usage: @clp [-vh]\n" );
@@ -593,6 +575,8 @@ int Cba_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Cba_CommandCec(): There is no current design.\n" );
         return 0;
     }
+
+#if 0
     pArgvNew = argv + globalUtilOptind;
     nArgcNew = argc - globalUtilOptind;
     if ( nArgcNew != 1 )
@@ -658,6 +642,8 @@ int Cba_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     Gia_ManStop( pFirst );
     Gia_ManStop( pSecond );
+
+#endif
     return 0;
 usage:
     Abc_Print( -2, "usage: @cec [-vh]\n" );
@@ -680,10 +666,7 @@ usage:
 ******************************************************************************/
 int Cba_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Prs_ManReadBlifTest();
-    extern void Prs_ManReadVerilogTest();
-    extern void Prs_SmtReadSmtTest();
-    //Cba_Man_t * p = Cba_AbcGetMan(pAbc);
+    Cba_Man_t * p = Cba_AbcGetMan(pAbc);
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -699,16 +682,11 @@ int Cba_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-/*
     if ( p == NULL )
     {
         Abc_Print( 1, "Cba_CommandTest(): There is no current design.\n" );
         return 0;
     }
-*/
-    //Cba_PtrTransformTestTest();
-    //Prs_ManReadVerilogTest();
-    //Prs_SmtReadSmtTest();
     return 0;
 usage:
     Abc_Print( -2, "usage: @test [-vh]\n" );
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index 09f1aea1..821e9cfd 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -1,20 +1,20 @@
 /**CFile****************************************************************
 
-  FileName    [cbaNtk.c]
+  FileName    [cba.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Hierarchical word-level netlist.]
+  PackageName [Verilog parser.]
 
-  Synopsis    [Netlist manipulation.]
+  Synopsis    [Parses several flavors of word-level Verilog.]
 
   Author      [Alan Mishchenko]
   
   Affiliation [UC Berkeley]
 
-  Date        [Ver. 1.0. Started - November 29, 2014.]
+  Date        [Ver. 1.0. Started - July 21, 2015.]
 
-  Revision    [$Id: cbaNtk.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+  Revision    [$Id: cba.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -26,491 +26,12 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Cba_Pair_t_ Cba_Pair_t;
-struct Cba_Pair_t_
-{
-    Cba_ObjType_t Type;
-    char *        pName;
-    char *        pSymb;
-};
-static const char * s_Pref = "ABC_";
-static Cba_Pair_t s_Types[CBA_BOX_UNKNOWN] =
-{ 
-    { CBA_OBJ_NONE,     "NONE",    NULL    },
-    { CBA_OBJ_PI,       "PI",      NULL    },
-    { CBA_OBJ_PO,       "PO",      NULL    },
-    { CBA_OBJ_BI,       "BI",      NULL    },
-    { CBA_OBJ_BO,       "BO",      NULL    },
-    { CBA_OBJ_BOX,      "BOX",     NULL    },
-    
-    { CBA_BOX_CF,       "CF",      "o"     },
-    { CBA_BOX_CT,       "CT",      "o"     }, 
-    { CBA_BOX_CX,       "CX",      "o"     }, 
-    { CBA_BOX_CZ,       "CZ",      "o"     },
-    { CBA_BOX_BUF,      "BUF",     "ao"    },
-    { CBA_BOX_INV,      "INV",     "ao"    },
-    { CBA_BOX_AND,      "AND",     "abo"   },
-    { CBA_BOX_NAND,     "NAND",    "abo"   },
-    { CBA_BOX_OR,       "OR",      "abo"   },
-    { CBA_BOX_NOR,      "NOR",     "abo"   },
-    { CBA_BOX_XOR,      "XOR",     "abo"   },
-    { CBA_BOX_XNOR,     "XNOR",    "abo"   },
-    { CBA_BOX_SHARP,    "SHARP",   "abo"   },
-    { CBA_BOX_SHARPL,   "SHARPL",  "abo"   },
-    { CBA_BOX_MUX,      "MUX",     "cabo"  },
-    { CBA_BOX_MAJ,      "MAJ",     "abco"  },
-    
-    { CBA_BOX_RAND,     "RAND",    "ao"    },
-    { CBA_BOX_RNAND,    "RNAND",   "ao"    },
-    { CBA_BOX_ROR,      "ROR",     "ao"    },
-    { CBA_BOX_RNOR,     "RNOR",    "ao"    },
-    { CBA_BOX_RXOR,     "RXOR",    "ao"    },
-    { CBA_BOX_RXNOR,    "RXNOR",   "ao"    },
-    
-    { CBA_BOX_LAND,     "LAND",    "abo"   },
-    { CBA_BOX_LNAND,    "LNAND",   "abo"   },
-    { CBA_BOX_LOR,      "LOR",     "abo"   },
-    { CBA_BOX_LNOR,     "LNOR",    "abo"   },
-    { CBA_BOX_LXOR,     "LXOR",    "abo"   },
-    { CBA_BOX_LXNOR,    "LXNOR",   "abo"   },
-    
-    { CBA_BOX_NMUX,     "NMUX",    "abo"   },
-    { CBA_BOX_SEL,      "SEL",     "abo"   },
-    { CBA_BOX_PSEL,     "PSEL",    "iabo"  },
-    { CBA_BOX_ENC,      "ENC",     "ao"    },
-    { CBA_BOX_PENC,     "PENC",    "ao"    },
-    { CBA_BOX_DEC,      "DEC",     "ao"    },
-    { CBA_BOX_EDEC,     "EDEC",    "abo"   },
-    
-    { CBA_BOX_ADD,      "ADD",     "iabso" },
-    { CBA_BOX_SUB,      "SUB",     "abo"   },
-    { CBA_BOX_MUL,      "MUL",     "abo"   },
-    { CBA_BOX_DIV,      "DIV",     "abo"   },
-    { CBA_BOX_MOD,      "MOD",     "abo"   },
-    { CBA_BOX_REM,      "REM",     "abo"   },
-    { CBA_BOX_POW,      "POW",     "abo"   },
-    { CBA_BOX_MIN,      "MIN",     "ao"    },
-    { CBA_BOX_ABS,      "ABS",     "ao"    },
-
-    { CBA_BOX_LTHAN,    "LTHAN",   "iabo"  },
-    { CBA_BOX_LETHAN,   "LETHAN",  "abo"   },
-    { CBA_BOX_METHAN,   "METHAN",  "abo"   },
-    { CBA_BOX_MTHAN,    "MTHAN",   "abo"   },
-    { CBA_BOX_EQU,      "EQU",     "abo"   },
-    { CBA_BOX_NEQU,     "NEQU",    "abo"   },
-    
-    { CBA_BOX_SHIL,     "SHIL",    "abo"   },
-    { CBA_BOX_SHIR,     "SHIR",    "abo"   },
-    { CBA_BOX_ROTL,     "ROTL",    "abo"   },
-    { CBA_BOX_ROTR,     "ROTR",    "abo"   },
-
-    { CBA_BOX_GATE,     "GATE",    "io"    },
-    { CBA_BOX_LUT,      "LUT",     "io"    },
-    { CBA_BOX_ASSIGN,   "ASSIGN",  "abo"   },
-    
-    { CBA_BOX_TRI,      "TRI",     "abo"   },
-    { CBA_BOX_RAM,      "RAM",     "eadro" },
-    { CBA_BOX_RAMR,     "RAMR",    "eamo"  },
-    { CBA_BOX_RAMW,     "RAMW",    "eado"  },
-    { CBA_BOX_RAMWC,    "RAMWC",   "ceado" },
-    { CBA_BOX_RAMBOX,   "RAMBOX",  "io"    },
-    
-    { CBA_BOX_LATCH,    "LATCH",   "dvsgq" },
-    { CBA_BOX_LATCHRS,  "LATCHRS", "dsrgq" },
-    { CBA_BOX_DFF,      "DFF",     "dvscq" },
-    { CBA_BOX_DFFRS,    "DFFRS",   "dsrcq" }
-}; 
-static inline int Cba_GetTypeId( Cba_ObjType_t Type )
-{
-    int i;
-    for ( i = 1; i < CBA_BOX_UNKNOWN; i++ )
-        if ( s_Types[i].Type == Type )
-            return i;
-    return -1;
-}
-void Cba_ManSetupTypes( char ** pNames, char ** pSymbs )
-{
-    Cba_ObjType_t Type;
-    for ( Type = 1; Type < CBA_BOX_UNKNOWN; Type++ )
-    {
-        int Id = Cba_GetTypeId( Type );
-        pNames[Type] = s_Types[Id].pName;
-        pSymbs[Type] = s_Types[Id].pSymb;
-    }
-}
-
-char * Cba_NtkGenerateName( Cba_Ntk_t * p, Cba_ObjType_t Type, Vec_Int_t * vBits )
-{
-    static char Buffer[100]; 
-    char * pTemp; int i, Bits;
-    char * pName = Cba_ManPrimName( p->pDesign, Type );
-    char * pSymb = Cba_ManPrimSymb( p->pDesign, Type );
-    assert( Vec_IntSize(vBits) == (int)strlen(pSymb) );
-    sprintf( Buffer, "%s%s_", s_Pref, pName );
-    pTemp = Buffer + strlen(Buffer);
-    Vec_IntForEachEntry( vBits, Bits, i )
-    {
-        sprintf( pTemp, "%c%d", pSymb[i], Bits );
-        pTemp += strlen(pTemp);
-    }
-    //Vec_IntPrint( vBits );
-    //printf( "%s\n", Buffer );
-    return Buffer;
-}
-
-Cba_ObjType_t Cba_NameToType( char * pName )
-{
-    Cba_ObjType_t i;
-    if ( strncmp(pName, s_Pref, strlen(s_Pref)) )
-        return 0;
-    pName += strlen(s_Pref);
-    for ( i = 1; i < CBA_BOX_UNKNOWN; i++ )
-        if ( !strncmp(pName, s_Types[i].pName, strlen(s_Types[i].pName)) )
-            return s_Types[i].Type;
-    return 0;
-}
-Vec_Int_t * Cba_NameToRanges( char * pName )
-{
-    static Vec_Int_t Bits, * vBits = &Bits;
-    static int pArray[10];
-    char * pTemp; 
-    int Num = 0, Count = 0;
-    // initialize array
-    vBits->pArray = pArray;
-    vBits->nSize = 0;
-    vBits->nCap = 10;
-    // check the name
-    assert( !strncmp(pName, s_Pref, strlen(s_Pref)) );
-    for ( pTemp = pName; *pTemp && !Cba_CharIsDigit(*pTemp); pTemp++ );
-    assert( Cba_CharIsDigit(*pTemp) );
-    for ( ; *pTemp; pTemp++ )
-    {
-        if ( Cba_CharIsDigit(*pTemp) )
-            Num = 10 * Num + *pTemp - '0';
-        else
-            Vec_IntPush( vBits, Num ), Count += Num, Num = 0;
-    }
-    assert( Num > 0 );
-    Vec_IntPush( vBits, Num );  Count += Num;
-    assert( Vec_IntSize(vBits) <= 10 );
-    return vBits;
-}
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Replaces fanin iOld by iNew in all fanouts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cba_NtkUpdateFanout( Cba_Ntk_t * p, int iOld, int iNew )
-{
-    int iCo;
-    assert( Cba_ObjIsCi(p, iOld) );
-    assert( Cba_ObjIsCi(p, iNew) );
-    Cba_ObjForEachFanout( p, iOld, iCo )
-    {
-        assert( Cba_ObjFanin(p, iCo) == iOld );
-        Cba_ObjCleanFanin( p, iCo );
-        Cba_ObjSetFanin( p, iCo, iNew );
-    }
-    Cba_ObjSetFanout( p, iNew, Cba_ObjFanout(p, iOld) );
-    Cba_ObjSetFanout( p, iOld, 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives fanout.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cba_NtkDeriveFanout( Cba_Ntk_t * p )
-{
-    int iCi, iCo;
-    assert( !Cba_NtkHasFanouts(p) );
-    Cba_NtkStartFanouts( p );
-    Cba_NtkForEachCo( p, iCo )
-    {
-        assert( !Cba_ObjNextFanout(p, iCo) );
-        iCi = Cba_ObjFanin(p, iCo);
-        if ( Cba_ObjFanout(p, iCi) )
-            Cba_ObjSetNextFanout( p, Cba_ObjFanout(p, iCi), iCo );
-        Cba_ObjSetFanout( p, iCi, iCo );
-    }
-    Cba_NtkForEachCo( p, iCo )
-        if ( !Cba_ObjNextFanout(p, iCo) )
-            Cba_ObjSetFanout( p, Cba_ObjFanin(p, iCo), iCo );
-}
-void Cba_ManDeriveFanout( Cba_Man_t * p )
-{
-    Cba_Ntk_t * pNtk; int i;
-    Cba_ManForEachNtk( p, pNtk, i )
-        Cba_NtkDeriveFanout( pNtk );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Assigns word-level names.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cba_ManAssignInternTwo( Cba_Ntk_t * p, int iNum, int nDigits, char * pPref, Vec_Int_t * vMap )
-{
-    char Buffer[16]; int i, NameId = 0;
-    for ( i = 0; !NameId || Vec_IntEntry(vMap, NameId); i++ )
-    {
-        if ( i == 0 )
-            sprintf( Buffer, "%s%0*d", pPref, nDigits, iNum );
-        else
-            sprintf( Buffer, "%s%0*d_%d", pPref, nDigits, iNum, i );
-        NameId = Abc_NamStrFindOrAdd( p->pDesign->pStrs, Buffer, NULL );
-    }
-    Vec_IntWriteEntry( vMap, NameId, 1 );
-    return NameId;
-}
-int Cba_ManAssignCountNames( Cba_Ntk_t * p )
-{
-    int i, iObj, iBox, Count = 0;
-    Cba_NtkForEachPiMain( p, iObj, i )
-        if ( !Cba_ObjNameInt(p, iObj) )
-            Count++;
-    Cba_NtkForEachBox( p, iBox )
-        Cba_BoxForEachBoMain( p, iBox, iObj, i )
-            if ( !Cba_ObjNameInt(p, iObj) )
-                Count++;
-    return Count;
-}
-void Cba_ManAssignInternWordNamesNtk( Cba_Ntk_t * p, Vec_Int_t * vMap )
-{
-    int k, iObj, iTerm, iName = -1, iBit = -1;
-    int nDigits, nPis = 0, nPos = 0, nNames = 1;
-    // start names
-    if ( !Cba_NtkHasNames(p) )
-        Cba_NtkStartNames(p);
-    nDigits = Abc_Base10Log( Cba_ManAssignCountNames(p) );
-    // populate map with the currently used names
-    Cba_NtkForEachCi( p, iObj )
-        if ( Cba_ObjNameInt(p, iObj) )
-            Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 1 );
-    Cba_NtkForEachBox( p, iObj )
-        if ( Cba_ObjNameInt(p, iObj) )
-            Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 1 );
-    // assign CI names
-    Cba_NtkForEachCi( p, iObj )
-    {
-        if ( Cba_ObjNameInt(p, iObj) )
-        {
-            iName = -1;
-            iBit = -1;
-            continue;
-        }
-        if ( Cba_ObjBit(p, iObj) )
-        {
-            assert( iBit > 0 );
-            Cba_ObjSetName( p, iObj, Abc_Var2Lit2(iBit++, CBA_NAME_INDEX) );
-        }
-        else
-        {
-            //int Type = Cba_ObjType(p, iObj);
-            int Range = Cba_ObjIsPi(p, iObj) ? Cba_ObjPiRange(p, iObj) : Cba_BoxBoRange(p, iObj);
-            iName = Cba_ManAssignInternTwo( p, nNames++, nDigits, (char*)(Cba_ObjIsPi(p, iObj) ? "i":"n"), vMap );
-            if ( Range == 1 )
-                Cba_ObjSetName( p, iObj, Abc_Var2Lit2(iName, CBA_NAME_BIN) );
-            else
-                Cba_ObjSetName( p, iObj, Abc_Var2Lit2(iName, CBA_NAME_WORD) );
-            iBit = 1;
-        }
-    }
-    // transfer names to the interface
-    if ( Cba_NtkInfoNum(p) )
-    {
-        for ( k = 0; k < Cba_NtkInfoNum(p); k++ )
-        {
-            //char * pName = Cba_NtkName(p);
-            if ( Cba_NtkInfoType(p, k) == 1 ) // PI
-            {
-                iObj = Cba_NtkPi(p, nPis);
-                assert( !Cba_ObjBit(p, iObj) );
-                assert( Cba_ObjNameType(p, iObj) <= CBA_NAME_WORD );
-                Cba_NtkSetInfoName( p, k, Abc_Var2Lit2(Cba_ObjNameId(p, iObj), 1) );
-                nPis += Cba_NtkInfoRange(p, k);
-            }
-            else if ( Cba_NtkInfoType(p, k) == 2 ) // PO
-            {
-                iObj = Cba_NtkPo(p, nPos);
-                assert( !Cba_ObjBit(p, iObj) );
-                iObj = Cba_ObjFanin(p, iObj);
-                assert( Cba_ObjNameType(p, iObj) <= CBA_NAME_WORD );
-                Cba_NtkSetInfoName( p, k, Abc_Var2Lit2(Cba_ObjNameId(p, iObj), 2) );
-                nPos += Cba_NtkInfoRange(p, k);
-            }
-            else assert( 0 );
-        }
-        assert( nPis == Cba_NtkPiNum(p) );
-        assert( nPos == Cba_NtkPoNum(p) );
-    }
-    // assign instance names
-    nDigits = Abc_Base10Log( Cba_NtkObjNum(p) );
-    Cba_NtkForEachBox( p, iObj )
-        if ( !Cba_ObjNameInt(p, iObj) )
-        {
-            iName = Cba_ManAssignInternTwo( p, iObj, nDigits, "g", vMap );
-            Cba_ObjSetName( p, iObj, Abc_Var2Lit2(iName, CBA_NAME_BIN) );
-        }
-    // unmark all names
-    Cba_NtkForEachPi( p, iObj, k )
-        if ( Cba_ObjNameType(p, iObj) <= CBA_NAME_WORD )
-            Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 0 );
-    Cba_NtkForEachBox( p, iObj )
-    {
-        Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 0 );
-        Cba_BoxForEachBo( p, iObj, iTerm, k )
-            if ( Cba_ObjNameType(p, iTerm) <= CBA_NAME_WORD )
-                Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iTerm), 0 );
-    }
-//    printf( "Generated %d word-level names.\n", nNames-1 );
-}
-void Cba_ManAssignInternWordNames( Cba_Man_t * p )
-{
-    Vec_Int_t * vMap = Vec_IntStart( 2*Cba_ManObjNum(p) );
-    Cba_Ntk_t * pNtk; int i;
-    Cba_ManForEachNtk( p, pNtk, i )
-        Cba_ManAssignInternWordNamesNtk( pNtk, vMap );
-    assert( Vec_IntCountEntry(vMap, 0) == Vec_IntSize(vMap) );
-    Vec_IntFree( vMap );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Count number of objects after collapsing.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cba_ManClpObjNum_rec( Cba_Ntk_t * p )
-{
-    int i, Counter = 0;
-    if ( p->Count >= 0 )
-        return p->Count;
-    Cba_NtkForEachBox( p, i )
-        Counter += Cba_ObjIsBoxUser(p, i) ? Cba_ManClpObjNum_rec( Cba_BoxNtk(p, i) ) + 3*Cba_BoxBoNum(p, i) : Cba_BoxSize(p, i);
-    return (p->Count = Counter);
-}
-int Cba_ManClpObjNum( Cba_Man_t * p )
-{
-    Cba_Ntk_t * pNtk; int i;
-    Cba_ManForEachNtk( p, pNtk, i )
-        pNtk->Count = -1;
-    return Cba_NtkPioNum( Cba_ManRoot(p) ) + Cba_ManClpObjNum_rec( Cba_ManRoot(p) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects boxes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cba_NtkDfs_rec( Cba_Ntk_t * p, int iObj, Vec_Int_t * vBoxes )
-{
-    int k, iFanin;
-    if ( Cba_ObjIsBo(p, iObj) == 1 )
-    {
-        Cba_NtkDfs_rec( p, Cba_ObjFanin(p, iObj), vBoxes );
-        return;
-    }
-    assert( Cba_ObjIsPi(p, iObj) || Cba_ObjIsBox(p, iObj) );
-    if ( Cba_ObjCopy(p, iObj) > 0 ) // visited
-        return;
-    Cba_ObjSetCopy( p, iObj, 1 );
-    Cba_BoxForEachFanin( p, iObj, iFanin, k )
-        Cba_NtkDfs_rec( p, iFanin, vBoxes );
-    Vec_IntPush( vBoxes, iObj );
-}
-Vec_Int_t * Cba_NtkDfs( Cba_Ntk_t * p )
-{
-    int i, iObj;
-    Vec_Int_t * vBoxes = Vec_IntAlloc( Cba_NtkBoxNum(p) );
-    Cba_NtkStartCopies( p ); // -1 = not visited; 1 = finished
-    Cba_NtkForEachPi( p, iObj, i )
-        Cba_ObjSetCopy( p, iObj, 1 );
-    Cba_NtkForEachPo( p, iObj, i )
-        Cba_NtkDfs_rec( p, Cba_ObjFanin(p, iObj), vBoxes );
-    return vBoxes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects user boxes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cba_NtkDfsUserBoxes_rec( Cba_Ntk_t * p, int iObj, Vec_Int_t * vBoxes )
-{
-    int k, iFanin;
-    assert( Cba_ObjIsBoxUser(p, iObj) );
-    if ( Cba_ObjCopy(p, iObj) == 1 ) // visited
-        return 1;
-    if ( Cba_ObjCopy(p, iObj) == 0 ) // loop
-        return 0;
-    Cba_ObjSetCopy( p, iObj, 0 );
-    Cba_BoxForEachFanin( p, iObj, iFanin, k )
-        if ( Cba_ObjIsBo(p, iFanin) && Cba_ObjIsBoxUser(p, Cba_ObjFanin(p, iFanin)) )
-            if ( !Cba_NtkDfsUserBoxes_rec( p, Cba_ObjFanin(p, iFanin), vBoxes ) )
-                return 0;
-    Vec_IntPush( vBoxes, iObj );
-    Cba_ObjSetCopy( p, iObj, 1 );
-    return 1;
-}
-int Cba_NtkDfsUserBoxes( Cba_Ntk_t * p )
-{
-    int iObj;
-    Cba_NtkStartCopies( p ); // -1 = not visited; 0 = on the path; 1 = finished
-    Vec_IntClear( &p->vArray );
-    Cba_NtkForEachBoxUser( p, iObj )
-        if ( !Cba_NtkDfsUserBoxes_rec( p, iObj, &p->vArray ) )
-        {
-            printf( "Cyclic dependency of user boxes is detected.\n" );
-            return 0;
-        }
-    return 1;
-}
-
-/**Function*************************************************************
-
   Synopsis    []
 
   Description []
@@ -520,80 +41,6 @@ int Cba_NtkDfsUserBoxes( Cba_Ntk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cba_NtkCollapse_rec( Cba_Ntk_t * pNew, Cba_Ntk_t * p, Vec_Int_t * vSigs )
-{
-    int i, iObj, iObjNew, iTerm;
-    Cba_NtkStartCopies( p );
-    // set PI copies
-    assert( Vec_IntSize(vSigs) == Cba_NtkPiNum(p) );
-    Cba_NtkForEachPi( p, iObj, i )
-        Cba_ObjSetCopy( p, iObj, Vec_IntEntry(vSigs, i) );
-    // duplicate internal objects and create buffers for hierarchy instances
-    Cba_NtkForEachBox( p, iObj )
-        if ( Cba_ObjIsBoxPrim( p, iObj ) )
-            Cba_BoxDup( pNew, p, iObj );
-        else
-        {
-            Cba_BoxForEachBo( p, iObj, iTerm, i )
-            {
-                iObjNew = Cba_ObjAlloc( pNew, CBA_OBJ_BI,  -1 );
-                iObjNew = Cba_ObjAlloc( pNew, CBA_BOX_BUF, -1 ); // buffer
-                iObjNew = Cba_ObjAlloc( pNew, CBA_OBJ_BO,  -1 );
-                Cba_ObjSetCopy( p, iTerm, iObjNew );
-            }
-        }
-    // duplicate user modules and connect objects
-    Cba_NtkForEachBox( p, iObj )
-        if ( Cba_ObjIsBoxPrim( p, iObj ) )
-        {
-            Cba_BoxForEachBi( p, iObj, iTerm, i )
-                Cba_ObjSetFanin( pNew, Cba_ObjCopy(p, iTerm), Cba_ObjCopy(p, Cba_ObjFanin(p, iTerm)) );
-        }
-        else
-        {
-            Vec_IntClear( vSigs );
-            Cba_BoxForEachBi( p, iObj, iTerm, i )
-                Vec_IntPush( vSigs, Cba_ObjCopy(p, Cba_ObjFanin(p, iTerm)) );
-            Cba_NtkCollapse_rec( pNew, Cba_BoxNtk(p, iObj), vSigs );
-            assert( Vec_IntSize(vSigs) == Cba_BoxBoNum(p, iObj) );
-            Cba_BoxForEachBo( p, iObj, iTerm, i )
-                Cba_ObjSetFanin( pNew, Cba_ObjCopy(p, iTerm)-2, Vec_IntEntry(vSigs, i) );
-        }
-    // collect POs
-    Vec_IntClear( vSigs );
-    Cba_NtkForEachPo( p, iObj, i )
-        Vec_IntPush( vSigs, Cba_ObjCopy(p, Cba_ObjFanin(p, iObj)) );
-}
-Cba_Man_t * Cba_ManCollapse( Cba_Man_t * p )
-{
-    int i, iObj;
-    Vec_Int_t * vSigs = Vec_IntAlloc( 1000 );
-    Cba_Man_t * pNew = Cba_ManStart( p, 1 );
-    Cba_Ntk_t * pRoot = Cba_ManRoot( p );
-    Cba_Ntk_t * pRootNew = Cba_ManRoot( pNew );
-    Cba_NtkAlloc( pRootNew, Cba_NtkNameId(pRoot), Cba_NtkPiNum(pRoot), Cba_NtkPoNum(pRoot), Cba_ManClpObjNum(p) );
-    if ( Vec_IntSize(&pRoot->vInfo) )
-        Vec_IntAppend( &pRootNew->vInfo, &pRoot->vInfo );
-    Cba_NtkForEachPi( pRoot, iObj, i )
-        Vec_IntPush( vSigs, Cba_ObjAlloc(pRootNew, CBA_OBJ_PI, -1) );
-    Cba_NtkCollapse_rec( pRootNew, pRoot, vSigs );
-    assert( Vec_IntSize(vSigs) == Cba_NtkPoNum(pRoot) );
-    Cba_NtkForEachPo( pRoot, iObj, i )
-        Cba_ObjAlloc( pRootNew, CBA_OBJ_PO, Vec_IntEntry(vSigs, i) );
-    assert( Cba_NtkObjNum(pRootNew) == Cba_NtkObjNumAlloc(pRootNew) );
-    Vec_IntFree( vSigs );
-    // transfer PI/PO names
-    if ( Cba_NtkHasNames(pRoot) )
-    {
-        Cba_NtkStartNames( pRootNew );
-        Cba_NtkForEachPi( pRoot, iObj, i )
-            Cba_ObjSetName( pRootNew, Cba_NtkPi(pRootNew, i), Cba_ObjName(pRoot, iObj) );
-        Cba_NtkForEachPoDriver( pRoot, iObj, i )
-            if ( !Cba_ObjIsPi(pRoot, iObj) )
-                Cba_ObjSetName( pRootNew, Cba_ObjCopy(pRoot, iObj), Cba_ObjName(pRoot, iObj) );
-    }
-    return pNew;
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/cba/cbaPrs.h b/src/base/cba/cbaPrs.h
index 9c7a1dfe..e8dc2602 100644
--- a/src/base/cba/cbaPrs.h
+++ b/src/base/cba/cbaPrs.h
@@ -288,6 +288,14 @@ static inline void Prs_NtkFree( Prs_Ntk_t * p )
     ABC_FREE( p );
 }
 
+static inline void Prs_ManVecFree( Vec_Ptr_t * vPrs )
+{
+    Prs_Ntk_t * pNtk; int i;
+    Vec_PtrForEachEntry( Prs_Ntk_t *, vPrs, pNtk, i )
+        Prs_NtkFree( pNtk );
+    Vec_PtrFree( vPrs );
+}
+
 static inline void Prs_ManFree( Prs_Man_t * p )
 {
     if ( p->pStrs )
@@ -333,6 +341,100 @@ static inline int Prs_ManMemory( Vec_Ptr_t * vPrs )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Other APIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Cba_ObjType_t Ptr_SopToType( char * pSop )
+{
+    if ( !strcmp(pSop, " 0\n") )         return CBA_BOX_CF;
+    if ( !strcmp(pSop, " 1\n") )         return CBA_BOX_CT;
+    if ( !strcmp(pSop, "1 1\n") )        return CBA_BOX_BUF;
+    if ( !strcmp(pSop, "0 1\n") )        return CBA_BOX_INV;
+    if ( !strcmp(pSop, "11 1\n") )       return CBA_BOX_AND;
+    if ( !strcmp(pSop, "00 1\n") )       return CBA_BOX_NOR;
+    if ( !strcmp(pSop, "00 0\n") )       return CBA_BOX_OR;
+    if ( !strcmp(pSop, "-1 1\n1- 1\n") ) return CBA_BOX_OR;
+    if ( !strcmp(pSop, "1- 1\n-1 1\n") ) return CBA_BOX_OR;
+    if ( !strcmp(pSop, "01 1\n10 1\n") ) return CBA_BOX_XOR;
+    if ( !strcmp(pSop, "10 1\n01 1\n") ) return CBA_BOX_XOR;
+    if ( !strcmp(pSop, "11 1\n00 1\n") ) return CBA_BOX_XNOR;
+    if ( !strcmp(pSop, "00 1\n11 1\n") ) return CBA_BOX_XNOR;
+    if ( !strcmp(pSop, "10 1\n") )       return CBA_BOX_SHARP;
+    if ( !strcmp(pSop, "01 1\n") )       return CBA_BOX_SHARPL;
+    assert( 0 );
+    return CBA_OBJ_NONE;
+}
+static inline char * Ptr_SopToTypeName( char * pSop )
+{
+    if ( !strcmp(pSop, " 0\n") )         return "CBA_BOX_C0";
+    if ( !strcmp(pSop, " 1\n") )         return "CBA_BOX_C1";
+    if ( !strcmp(pSop, "1 1\n") )        return "CBA_BOX_BUF";
+    if ( !strcmp(pSop, "0 1\n") )        return "CBA_BOX_INV";
+    if ( !strcmp(pSop, "11 1\n") )       return "CBA_BOX_AND";
+    if ( !strcmp(pSop, "00 1\n") )       return "CBA_BOX_NOR";
+    if ( !strcmp(pSop, "00 0\n") )       return "CBA_BOX_OR";
+    if ( !strcmp(pSop, "-1 1\n1- 1\n") ) return "CBA_BOX_OR";
+    if ( !strcmp(pSop, "1- 1\n-1 1\n") ) return "CBA_BOX_OR";
+    if ( !strcmp(pSop, "01 1\n10 1\n") ) return "CBA_BOX_XOR";
+    if ( !strcmp(pSop, "10 1\n01 1\n") ) return "CBA_BOX_XOR";
+    if ( !strcmp(pSop, "11 1\n00 1\n") ) return "CBA_BOX_XNOR";
+    if ( !strcmp(pSop, "00 1\n11 1\n") ) return "CBA_BOX_XNOR";
+    if ( !strcmp(pSop, "10 1\n") )       return "CBA_BOX_SHARP";
+    if ( !strcmp(pSop, "01 1\n") )       return "CBA_BOX_SHARPL";
+    assert( 0 );
+    return NULL;
+}
+static inline char * Ptr_TypeToName( Cba_ObjType_t Type )
+{
+    if ( Type == CBA_BOX_CF )    return "const0";
+    if ( Type == CBA_BOX_CT )    return "const1";
+    if ( Type == CBA_BOX_CX )    return "constX";
+    if ( Type == CBA_BOX_CZ )    return "constZ";
+    if ( Type == CBA_BOX_BUF )   return "buf";
+    if ( Type == CBA_BOX_INV )   return "not";
+    if ( Type == CBA_BOX_AND )   return "and";
+    if ( Type == CBA_BOX_NAND )  return "nand";
+    if ( Type == CBA_BOX_OR )    return "or";
+    if ( Type == CBA_BOX_NOR )   return "nor";
+    if ( Type == CBA_BOX_XOR )   return "xor";
+    if ( Type == CBA_BOX_XNOR )  return "xnor";
+    if ( Type == CBA_BOX_MUX )   return "mux";
+    if ( Type == CBA_BOX_MAJ )   return "maj";
+    if ( Type == CBA_BOX_SHARP ) return "sharp";
+    if ( Type == CBA_BOX_SHARPL) return "sharpl";
+    assert( 0 );
+    return "???";
+}
+static inline char * Ptr_TypeToSop( Cba_ObjType_t Type )
+{
+    if ( Type == CBA_BOX_CF )    return " 0\n";
+    if ( Type == CBA_BOX_CT )    return " 1\n";
+    if ( Type == CBA_BOX_CX )    return " 0\n";
+    if ( Type == CBA_BOX_CZ )    return " 0\n";
+    if ( Type == CBA_BOX_BUF )   return "1 1\n";
+    if ( Type == CBA_BOX_INV )   return "0 1\n";
+    if ( Type == CBA_BOX_AND )   return "11 1\n";
+    if ( Type == CBA_BOX_NAND )  return "11 0\n";
+    if ( Type == CBA_BOX_OR )    return "00 0\n";
+    if ( Type == CBA_BOX_NOR )   return "00 1\n";
+    if ( Type == CBA_BOX_XOR )   return "01 1\n10 1\n";
+    if ( Type == CBA_BOX_XNOR )  return "00 1\n11 1\n";
+    if ( Type == CBA_BOX_SHARP ) return "10 1\n";
+    if ( Type == CBA_BOX_SHARPL) return "01 1\n";
+    if ( Type == CBA_BOX_MUX )   return "11- 1\n0-1 1\n";
+    if ( Type == CBA_BOX_MAJ )   return "11- 1\n1-1 1\n-11 1\n";
+    assert( 0 );
+    return "???";
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                             ITERATORS                            ///
diff --git a/src/base/cba/cbaReadBlif.c b/src/base/cba/cbaReadBlif.c
index 4b982868..a9a752e2 100644
--- a/src/base/cba/cbaReadBlif.c
+++ b/src/base/cba/cbaReadBlif.c
@@ -43,7 +43,7 @@ typedef enum {
     PRS_BLIF_UNKNOWN   // 11:  unknown
 } Cba_BlifType_t;
 
-const char * s_BlifTypes[PRS_BLIF_UNKNOWN+1] = {
+static const char * s_BlifTypes[PRS_BLIF_UNKNOWN+1] = {
     NULL,              // 0:   unused
     ".model",          // 1:   .model   
     ".inouts",         // 2:   .inputs
diff --git a/src/base/cba/cbaReadVer.c b/src/base/cba/cbaReadVer.c
index 2704022e..ed825ba1 100644
--- a/src/base/cba/cbaReadVer.c
+++ b/src/base/cba/cbaReadVer.c
@@ -45,7 +45,7 @@ typedef enum {
     PRS_VER_UNKNOWN    // 13: unknown
 } Cba_VerType_t;
 
-const char * s_VerTypes[PRS_VER_UNKNOWN+1] = {
+static const char * s_VerTypes[PRS_VER_UNKNOWN+1] = {
     NULL,              // 0:  unused
     "input",           // 1:  input
     "output",          // 2:  output
@@ -101,7 +101,7 @@ static inline int Prs_ManIsDigit( Prs_Man_t * p )           { return Prs_CharIsD
 ***********************************************************************/
 
 // collect predefined modules names
-const char * s_VerilogModules[100] = 
+static const char * s_VerilogModules[100] = 
 {
     "const0", // CBA_BOX_CF,  
     "const1", // CBA_BOX_CT,  
@@ -120,7 +120,7 @@ const char * s_VerilogModules[100] =
     "maj",    // CBA_BOX_MAJ,  
     NULL
 };
-const char * s_KnownModules[100] = 
+static const char * s_KnownModules[100] = 
 {
     "VERIFIC_",
     "add_",                  
@@ -447,7 +447,7 @@ static inline int Prs_ManReadSignal( Prs_Man_t * p )
         return Abc_Var2Lit2( Item, CBA_PRS_NAME );
     }
 }
-int Prs_ManReadSignalList( Prs_Man_t * p, Vec_Int_t * vTemp, char LastSymb, int fAddForm )
+static int Prs_ManReadSignalList( Prs_Man_t * p, Vec_Int_t * vTemp, char LastSymb, int fAddForm )
 {
     Vec_IntClear( vTemp );
     while ( 1 )
diff --git a/src/base/cba/cbaWriteBlif.c b/src/base/cba/cbaWriteBlif.c
index 38901447..74ed2e42 100644
--- a/src/base/cba/cbaWriteBlif.c
+++ b/src/base/cba/cbaWriteBlif.c
@@ -44,14 +44,14 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Prs_ManWriteBlifArray( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vFanins )
+static void Prs_ManWriteBlifArray( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vFanins )
 {
     int i, NameId;
     Vec_IntForEachEntry( vFanins, NameId, i )
         fprintf( pFile, " %s", Prs_NtkStr(p, NameId) );
     fprintf( pFile, "\n" );
 }
-void Prs_ManWriteBlifLines( FILE * pFile, Prs_Ntk_t * p )
+static void Prs_ManWriteBlifLines( FILE * pFile, Prs_Ntk_t * p )
 {
     Vec_Int_t * vBox; 
     int i, k, FormId, ActId;
@@ -84,7 +84,7 @@ void Prs_ManWriteBlifLines( FILE * pFile, Prs_Ntk_t * p )
         }
     }
 }
-void Prs_ManWriteBlifNtk( FILE * pFile, Prs_Ntk_t * p )
+static void Prs_ManWriteBlifNtk( FILE * pFile, Prs_Ntk_t * p )
 {
     // write header
     fprintf( pFile, ".model %s\n", Prs_NtkStr(p, p->iModuleName) );
@@ -116,6 +116,7 @@ void Prs_ManWriteBlif( char * pFileName, Vec_Ptr_t * vPrs )
 }
 
 
+#if 0
 
 /**Function*************************************************************
 
@@ -226,6 +227,7 @@ void Cba_ManWriteBlif( char * pFileName, Cba_Man_t * p )
     fclose( pFile );
 }
 
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
index dfc6c87c..de99458a 100644
--- a/src/base/cba/cbaWriteVer.c
+++ b/src/base/cba/cbaWriteVer.c
@@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Prs_ManWriteVerilogConcat( FILE * pFile, Prs_Ntk_t * p, int Con )
+static void Prs_ManWriteVerilogConcat( FILE * pFile, Prs_Ntk_t * p, int Con )
 {
     extern void Prs_ManWriteVerilogArray( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSigs, int Start, int Stop, int fOdd );
     Vec_Int_t * vSigs = Prs_CatSignals(p, Con);
@@ -52,7 +52,7 @@ void Prs_ManWriteVerilogConcat( FILE * pFile, Prs_Ntk_t * p, int Con )
     Prs_ManWriteVerilogArray( pFile, p, vSigs, 0, Vec_IntSize(vSigs), 0 );
     fprintf( pFile, "}" );
 }
-void Prs_ManWriteVerilogSignal( FILE * pFile, Prs_Ntk_t * p, int Sig )
+static void Prs_ManWriteVerilogSignal( FILE * pFile, Prs_Ntk_t * p, int Sig )
 {
     int Value = Abc_Lit2Var2( Sig );
     Prs_ManType_t Type = (Prs_ManType_t)Abc_Lit2Att2( Sig );
@@ -64,7 +64,7 @@ void Prs_ManWriteVerilogSignal( FILE * pFile, Prs_Ntk_t * p, int Sig )
         Prs_ManWriteVerilogConcat( pFile, p, Value );
     else assert( 0 );
 }
-void Prs_ManWriteVerilogArray( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSigs, int Start, int Stop, int fOdd )
+static void Prs_ManWriteVerilogArray( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSigs, int Start, int Stop, int fOdd )
 {
     int i, Sig;
     assert( Vec_IntSize(vSigs) > 0 );
@@ -76,7 +76,7 @@ void Prs_ManWriteVerilogArray( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSigs, i
         fprintf( pFile, "%s", i == Stop - 1 ? "" : ", " );
     }
 }
-void Prs_ManWriteVerilogArray2( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSigs )
+static void Prs_ManWriteVerilogArray2( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSigs )
 {
     int i, FormId, ActSig;
     assert( Vec_IntSize(vSigs) % 2 == 0 );
@@ -89,7 +89,7 @@ void Prs_ManWriteVerilogArray2( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSigs )
         fprintf( pFile, ")%s", (i == Vec_IntSize(vSigs) - 2) ? "" : ", " );
     }
 }
-void Prs_ManWriteVerilogMux( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSigs )
+static void Prs_ManWriteVerilogMux( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSigs )
 {
     int i, FormId, ActSig;
     char * pStrs[4] = { " = ", " ? ", " : ", ";\n" };
@@ -105,7 +105,7 @@ void Prs_ManWriteVerilogMux( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSigs )
             break;
     }
 }
-void Prs_ManWriteVerilogBoxes( FILE * pFile, Prs_Ntk_t * p )
+static void Prs_ManWriteVerilogBoxes( FILE * pFile, Prs_Ntk_t * p )
 {
     Vec_Int_t * vBox; int i;
     Prs_NtkForEachBox( p, vBox, i )
@@ -131,7 +131,7 @@ void Prs_ManWriteVerilogBoxes( FILE * pFile, Prs_Ntk_t * p )
         }
     }
 }
-void Prs_ManWriteVerilogIos( FILE * pFile, Prs_Ntk_t * p, int SigType )
+static void Prs_ManWriteVerilogIos( FILE * pFile, Prs_Ntk_t * p, int SigType )
 {
     int NameId, RangeId, i;
     char * pSigNames[4]   = { "inout", "input", "output", "wire" }; 
@@ -142,13 +142,13 @@ void Prs_ManWriteVerilogIos( FILE * pFile, Prs_Ntk_t * p, int SigType )
     Vec_IntForEachEntryTwo( vSigs[SigType], vSigsR[SigType], NameId, RangeId, i )
         fprintf( pFile, "  %s %s%s;\n", pSigNames[SigType], RangeId ? Prs_NtkStr(p, RangeId) : "", Prs_NtkStr(p, NameId) );
 }
-void Prs_ManWriteVerilogIoOrder( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vOrder )
+static void Prs_ManWriteVerilogIoOrder( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vOrder )
 {
     int i, NameId;
     Vec_IntForEachEntry( vOrder, NameId, i )
         fprintf( pFile, "%s%s", Prs_NtkStr(p, NameId), i == Vec_IntSize(vOrder) - 1 ? "" : ", " );
 }
-void Prs_ManWriteVerilogNtk( FILE * pFile, Prs_Ntk_t * p )
+static void Prs_ManWriteVerilogNtk( FILE * pFile, Prs_Ntk_t * p )
 {
     int s;
     // write header
@@ -179,6 +179,7 @@ void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * vPrs )
 }
 
 
+#if 0
 
 /**Function*************************************************************
 
@@ -693,6 +694,7 @@ void Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p, int fUseAssign )
     Vec_StrFreeP( &p->vOut2 );
 }
 
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/cba/module.make b/src/base/cba/module.make
index 3239be1d..6e2e57be 100644
--- a/src/base/cba/module.make
+++ b/src/base/cba/module.make
@@ -1,15 +1,8 @@
 SRC +=    src/base/cba/cbaBlast.c \
     src/base/cba/cbaCba.c \
     src/base/cba/cbaCom.c \
-    src/base/cba/cbaLib.c \
     src/base/cba/cbaNtk.c \
-    src/base/cba/cbaPrsBuild.c \
-    src/base/cba/cbaPrsTrans.c \
-    src/base/cba/cbaPtr.c \
-    src/base/cba/cbaPtrAbc.c \
     src/base/cba/cbaReadBlif.c \
-    src/base/cba/cbaReadSmt.c \
     src/base/cba/cbaReadVer.c \
     src/base/cba/cbaWriteBlif.c \
-    src/base/cba/cbaWriteSmt.c \
     src/base/cba/cbaWriteVer.c