Version abc50829

58 files changed, 446 insertions, 989 deletions

diff --git a/Makefile b/Makefile
index 3358d267..75ad5a07 100644
--- a/Makefile
+++ b/Makefile
@@ -10,8 +10,8 @@ MODULES := src/base/abc src/base/cmd src/base/io src/base/main \
            src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \
            src/map/fpga src/map/mapper src/map/mio src/map/super \
            src/misc/extra src/misc/st src/misc/util src/misc/vec \
-	   src/opt/fxu src/opt/rwr \
-           src/sat/asat src/sat/fraig src/sat/msat src/sat/sim \
+	   src/opt/cut src/opt/fxu src/opt/rwr \
+           src/sat/asat src/sat/csat src/sat/msat src/sat/fraig src/sat/sim \
            src/seq \
            src/sop/ft src/sop/mvc
 
diff --git a/abc.opt b/abc.opt
index b387ed94..de47a195 100644
--- a/abc.opt
+++ b/abc.opt
diff --git a/abc.plg b/abc.plg
index 1e02d8fb..632ed572 100644
--- a/abc.plg
+++ b/abc.plg
@@ -3,576 +3,9 @@
 <pre>
 <h1>Build Log</h1>
 <h3>
---------------------Configuration: abc - Win32 Release--------------------
+--------------------Configuration: abc - Win32 Debug--------------------
 </h3>
 <h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F49.tmp" with contents
-[
-/nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\opt\cut" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c 
-"C:\_projects\abc\src\base\cmd\cmd.c"
-]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F49.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F4A.tmp" with contents
-[
-kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:no /pdb:"Release/abc.pdb" /machine:I386 /out:"_TEST/abc.exe" 
-.\Release\abc.obj
-.\Release\abcAig.obj
-.\Release\abcAttach.obj
-.\Release\abcBalance.obj
-.\Release\abcCheck.obj
-.\Release\abcCollapse.obj
-.\Release\abcCreate.obj
-.\Release\abcCut.obj
-.\Release\abcDfs.obj
-.\Release\abcDsd.obj
-.\Release\abcFanio.obj
-.\Release\abcFpga.obj
-.\Release\abcFraig.obj
-.\Release\abcFunc.obj
-.\Release\abcFxu.obj
-.\Release\abcLatch.obj
-.\Release\abcMap.obj
-.\Release\abcMinBase.obj
-.\Release\abcMiter.obj
-.\Release\abcNames.obj
-.\Release\abcNetlist.obj
-.\Release\abcPrint.obj
-.\Release\abcReconv.obj
-.\Release\abcRefactor.obj
-.\Release\abcRefs.obj
-.\Release\abcRenode.obj
-.\Release\abcRewrite.obj
-.\Release\abcSat.obj
-.\Release\abcSeq.obj
-.\Release\abcSeqRetime.obj
-.\Release\abcShow.obj
-.\Release\abcSop.obj
-.\Release\abcStrash.obj
-.\Release\abcSweep.obj
-.\Release\abcTiming.obj
-.\Release\abcUnreach.obj
-.\Release\abcUtil.obj
-.\Release\abcVerify.obj
-.\Release\cmd.obj
-.\Release\cmdAlias.obj
-.\Release\cmdApi.obj
-.\Release\cmdFlag.obj
-.\Release\cmdHist.obj
-.\Release\cmdUtils.obj
-.\Release\io.obj
-.\Release\ioRead.obj
-.\Release\ioReadBench.obj
-.\Release\ioReadBlif.obj
-.\Release\ioReadEdif.obj
-.\Release\ioReadPla.obj
-.\Release\ioReadVerilog.obj
-.\Release\ioUtil.obj
-.\Release\ioWriteBench.obj
-.\Release\ioWriteBlif.obj
-.\Release\ioWriteCnf.obj
-.\Release\ioWritePla.obj
-.\Release\main.obj
-.\Release\mainFrame.obj
-.\Release\mainInit.obj
-.\Release\mainUtils.obj
-.\Release\cuddAddAbs.obj
-.\Release\cuddAddApply.obj
-.\Release\cuddAddFind.obj
-.\Release\cuddAddInv.obj
-.\Release\cuddAddIte.obj
-.\Release\cuddAddNeg.obj
-.\Release\cuddAddWalsh.obj
-.\Release\cuddAndAbs.obj
-.\Release\cuddAnneal.obj
-.\Release\cuddApa.obj
-.\Release\cuddAPI.obj
-.\Release\cuddApprox.obj
-.\Release\cuddBddAbs.obj
-.\Release\cuddBddCorr.obj
-.\Release\cuddBddIte.obj
-.\Release\cuddBridge.obj
-.\Release\cuddCache.obj
-.\Release\cuddCheck.obj
-.\Release\cuddClip.obj
-.\Release\cuddCof.obj
-.\Release\cuddCompose.obj
-.\Release\cuddDecomp.obj
-.\Release\cuddEssent.obj
-.\Release\cuddExact.obj
-.\Release\cuddExport.obj
-.\Release\cuddGenCof.obj
-.\Release\cuddGenetic.obj
-.\Release\cuddGroup.obj
-.\Release\cuddHarwell.obj
-.\Release\cuddInit.obj
-.\Release\cuddInteract.obj
-.\Release\cuddLCache.obj
-.\Release\cuddLevelQ.obj
-.\Release\cuddLinear.obj
-.\Release\cuddLiteral.obj
-.\Release\cuddMatMult.obj
-.\Release\cuddPriority.obj
-.\Release\cuddRead.obj
-.\Release\cuddRef.obj
-.\Release\cuddReorder.obj
-.\Release\cuddSat.obj
-.\Release\cuddSign.obj
-.\Release\cuddSolve.obj
-.\Release\cuddSplit.obj
-.\Release\cuddSubsetHB.obj
-.\Release\cuddSubsetSP.obj
-.\Release\cuddSymmetry.obj
-.\Release\cuddTable.obj
-.\Release\cuddUtil.obj
-.\Release\cuddWindow.obj
-.\Release\cuddZddCount.obj
-.\Release\cuddZddFuncs.obj
-.\Release\cuddZddGroup.obj
-.\Release\cuddZddIsop.obj
-.\Release\cuddZddLin.obj
-.\Release\cuddZddMisc.obj
-.\Release\cuddZddPort.obj
-.\Release\cuddZddReord.obj
-.\Release\cuddZddSetop.obj
-.\Release\cuddZddSymm.obj
-.\Release\cuddZddUtil.obj
-.\Release\epd.obj
-.\Release\mtrBasic.obj
-.\Release\mtrGroup.obj
-.\Release\parseCore.obj
-.\Release\parseStack.obj
-.\Release\dsdApi.obj
-.\Release\dsdCheck.obj
-.\Release\dsdLocal.obj
-.\Release\dsdMan.obj
-.\Release\dsdProc.obj
-.\Release\dsdTree.obj
-.\Release\reoApi.obj
-.\Release\reoCore.obj
-.\Release\reoProfile.obj
-.\Release\reoSift.obj
-.\Release\reoSwap.obj
-.\Release\reoTest.obj
-.\Release\reoTransfer.obj
-.\Release\reoUnits.obj
-.\Release\mvc.obj
-.\Release\mvcApi.obj
-.\Release\mvcCompare.obj
-.\Release\mvcContain.obj
-.\Release\mvcCover.obj
-.\Release\mvcCube.obj
-.\Release\mvcDivide.obj
-.\Release\mvcDivisor.obj
-.\Release\mvcList.obj
-.\Release\mvcLits.obj
-.\Release\mvcMan.obj
-.\Release\mvcOpAlg.obj
-.\Release\mvcOpBool.obj
-.\Release\mvcPrint.obj
-.\Release\mvcSort.obj
-.\Release\mvcUtils.obj
-.\Release\ftFactor.obj
-.\Release\ftPrint.obj
-.\Release\added.obj
-.\Release\solver.obj
-.\Release\msatActivity.obj
-.\Release\msatClause.obj
-.\Release\msatClauseVec.obj
-.\Release\msatMem.obj
-.\Release\msatOrderJ.obj
-.\Release\msatQueue.obj
-.\Release\msatRead.obj
-.\Release\msatSolverApi.obj
-.\Release\msatSolverCore.obj
-.\Release\msatSolverIo.obj
-.\Release\msatSolverSearch.obj
-.\Release\msatSort.obj
-.\Release\msatVec.obj
-.\Release\fraigApi.obj
-.\Release\fraigCanon.obj
-.\Release\fraigFanout.obj
-.\Release\fraigFeed.obj
-.\Release\fraigMan.obj
-.\Release\fraigMem.obj
-.\Release\fraigNode.obj
-.\Release\fraigPrime.obj
-.\Release\fraigSat.obj
-.\Release\fraigTable.obj
-.\Release\fraigUtil.obj
-.\Release\fraigVec.obj
-.\Release\simMan.obj
-.\Release\simSat.obj
-.\Release\simSupp.obj
-.\Release\simSym.obj
-.\Release\simUnate.obj
-.\Release\simUtils.obj
-.\Release\csat_apis.obj
-.\Release\fxu.obj
-.\Release\fxuCreate.obj
-.\Release\fxuHeapD.obj
-.\Release\fxuHeapS.obj
-.\Release\fxuList.obj
-.\Release\fxuMatrix.obj
-.\Release\fxuPair.obj
-.\Release\fxuPrint.obj
-.\Release\fxuReduce.obj
-.\Release\fxuSelect.obj
-.\Release\fxuSingle.obj
-.\Release\fxuUpdate.obj
-.\Release\rwrDec.obj
-.\Release\rwrEva.obj
-.\Release\rwrExp.obj
-.\Release\rwrLib.obj
-.\Release\rwrMan.obj
-.\Release\rwrPrint.obj
-.\Release\rwrUtil.obj
-.\Release\cutMan.obj
-.\Release\cutMerge.obj
-.\Release\cutNode.obj
-.\Release\cutSeq.obj
-.\Release\cutTable.obj
-.\Release\cutTruth.obj
-.\Release\fpga.obj
-.\Release\fpgaCore.obj
-.\Release\fpgaCreate.obj
-.\Release\fpgaCut.obj
-.\Release\fpgaCutUtils.obj
-.\Release\fpgaFanout.obj
-.\Release\fpgaLib.obj
-.\Release\fpgaMatch.obj
-.\Release\fpgaTime.obj
-.\Release\fpgaTruth.obj
-.\Release\fpgaUtils.obj
-.\Release\fpgaVec.obj
-.\Release\mapper.obj
-.\Release\mapperCanon.obj
-.\Release\mapperCore.obj
-.\Release\mapperCreate.obj
-.\Release\mapperCut.obj
-.\Release\mapperCutUtils.obj
-.\Release\mapperFanout.obj
-.\Release\mapperLib.obj
-.\Release\mapperMatch.obj
-.\Release\mapperRefs.obj
-.\Release\mapperSuper.obj
-.\Release\mapperTable.obj
-.\Release\mapperTime.obj
-.\Release\mapperTree.obj
-.\Release\mapperTruth.obj
-.\Release\mapperUtils.obj
-.\Release\mapperVec.obj
-.\Release\mio.obj
-.\Release\mioApi.obj
-.\Release\mioFunc.obj
-.\Release\mioRead.obj
-.\Release\mioUtils.obj
-.\Release\super.obj
-.\Release\superAnd.obj
-.\Release\superGate.obj
-.\Release\superWrite.obj
-.\Release\extraUtilBdd.obj
-.\Release\extraUtilBitMatrix.obj
-.\Release\extraUtilCanon.obj
-.\Release\extraUtilFile.obj
-.\Release\extraUtilMemory.obj
-.\Release\extraUtilMisc.obj
-.\Release\extraUtilProgress.obj
-.\Release\extraUtilReader.obj
-.\Release\st.obj
-.\Release\stmm.obj
-.\Release\cpu_stats.obj
-.\Release\cpu_time.obj
-.\Release\datalimit.obj
-.\Release\getopt.obj
-.\Release\pathsearch.obj
-.\Release\safe_mem.obj
-.\Release\strsav.obj
-.\Release\texpand.obj
-]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F4A.tmp"
-<h3>Output Window</h3>
-Compiling...
-cmd.c
-Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F4C.tmp" with contents
-[
-/nologo /o"Release/abc.bsc" 
-.\Release\abc.sbr
-.\Release\abcAig.sbr
-.\Release\abcAttach.sbr
-.\Release\abcBalance.sbr
-.\Release\abcCheck.sbr
-.\Release\abcCollapse.sbr
-.\Release\abcCreate.sbr
-.\Release\abcCut.sbr
-.\Release\abcDfs.sbr
-.\Release\abcDsd.sbr
-.\Release\abcFanio.sbr
-.\Release\abcFpga.sbr
-.\Release\abcFraig.sbr
-.\Release\abcFunc.sbr
-.\Release\abcFxu.sbr
-.\Release\abcLatch.sbr
-.\Release\abcMap.sbr
-.\Release\abcMinBase.sbr
-.\Release\abcMiter.sbr
-.\Release\abcNames.sbr
-.\Release\abcNetlist.sbr
-.\Release\abcPrint.sbr
-.\Release\abcReconv.sbr
-.\Release\abcRefactor.sbr
-.\Release\abcRefs.sbr
-.\Release\abcRenode.sbr
-.\Release\abcRewrite.sbr
-.\Release\abcSat.sbr
-.\Release\abcSeq.sbr
-.\Release\abcSeqRetime.sbr
-.\Release\abcShow.sbr
-.\Release\abcSop.sbr
-.\Release\abcStrash.sbr
-.\Release\abcSweep.sbr
-.\Release\abcTiming.sbr
-.\Release\abcUnreach.sbr
-.\Release\abcUtil.sbr
-.\Release\abcVerify.sbr
-.\Release\cmd.sbr
-.\Release\cmdAlias.sbr
-.\Release\cmdApi.sbr
-.\Release\cmdFlag.sbr
-.\Release\cmdHist.sbr
-.\Release\cmdUtils.sbr
-.\Release\io.sbr
-.\Release\ioRead.sbr
-.\Release\ioReadBench.sbr
-.\Release\ioReadBlif.sbr
-.\Release\ioReadEdif.sbr
-.\Release\ioReadPla.sbr
-.\Release\ioReadVerilog.sbr
-.\Release\ioUtil.sbr
-.\Release\ioWriteBench.sbr
-.\Release\ioWriteBlif.sbr
-.\Release\ioWriteCnf.sbr
-.\Release\ioWritePla.sbr
-.\Release\main.sbr
-.\Release\mainFrame.sbr
-.\Release\mainInit.sbr
-.\Release\mainUtils.sbr
-.\Release\cuddAddAbs.sbr
-.\Release\cuddAddApply.sbr
-.\Release\cuddAddFind.sbr
-.\Release\cuddAddInv.sbr
-.\Release\cuddAddIte.sbr
-.\Release\cuddAddNeg.sbr
-.\Release\cuddAddWalsh.sbr
-.\Release\cuddAndAbs.sbr
-.\Release\cuddAnneal.sbr
-.\Release\cuddApa.sbr
-.\Release\cuddAPI.sbr
-.\Release\cuddApprox.sbr
-.\Release\cuddBddAbs.sbr
-.\Release\cuddBddCorr.sbr
-.\Release\cuddBddIte.sbr
-.\Release\cuddBridge.sbr
-.\Release\cuddCache.sbr
-.\Release\cuddCheck.sbr
-.\Release\cuddClip.sbr
-.\Release\cuddCof.sbr
-.\Release\cuddCompose.sbr
-.\Release\cuddDecomp.sbr
-.\Release\cuddEssent.sbr
-.\Release\cuddExact.sbr
-.\Release\cuddExport.sbr
-.\Release\cuddGenCof.sbr
-.\Release\cuddGenetic.sbr
-.\Release\cuddGroup.sbr
-.\Release\cuddHarwell.sbr
-.\Release\cuddInit.sbr
-.\Release\cuddInteract.sbr
-.\Release\cuddLCache.sbr
-.\Release\cuddLevelQ.sbr
-.\Release\cuddLinear.sbr
-.\Release\cuddLiteral.sbr
-.\Release\cuddMatMult.sbr
-.\Release\cuddPriority.sbr
-.\Release\cuddRead.sbr
-.\Release\cuddRef.sbr
-.\Release\cuddReorder.sbr
-.\Release\cuddSat.sbr
-.\Release\cuddSign.sbr
-.\Release\cuddSolve.sbr
-.\Release\cuddSplit.sbr
-.\Release\cuddSubsetHB.sbr
-.\Release\cuddSubsetSP.sbr
-.\Release\cuddSymmetry.sbr
-.\Release\cuddTable.sbr
-.\Release\cuddUtil.sbr
-.\Release\cuddWindow.sbr
-.\Release\cuddZddCount.sbr
-.\Release\cuddZddFuncs.sbr
-.\Release\cuddZddGroup.sbr
-.\Release\cuddZddIsop.sbr
-.\Release\cuddZddLin.sbr
-.\Release\cuddZddMisc.sbr
-.\Release\cuddZddPort.sbr
-.\Release\cuddZddReord.sbr
-.\Release\cuddZddSetop.sbr
-.\Release\cuddZddSymm.sbr
-.\Release\cuddZddUtil.sbr
-.\Release\epd.sbr
-.\Release\mtrBasic.sbr
-.\Release\mtrGroup.sbr
-.\Release\parseCore.sbr
-.\Release\parseStack.sbr
-.\Release\dsdApi.sbr
-.\Release\dsdCheck.sbr
-.\Release\dsdLocal.sbr
-.\Release\dsdMan.sbr
-.\Release\dsdProc.sbr
-.\Release\dsdTree.sbr
-.\Release\reoApi.sbr
-.\Release\reoCore.sbr
-.\Release\reoProfile.sbr
-.\Release\reoSift.sbr
-.\Release\reoSwap.sbr
-.\Release\reoTest.sbr
-.\Release\reoTransfer.sbr
-.\Release\reoUnits.sbr
-.\Release\mvc.sbr
-.\Release\mvcApi.sbr
-.\Release\mvcCompare.sbr
-.\Release\mvcContain.sbr
-.\Release\mvcCover.sbr
-.\Release\mvcCube.sbr
-.\Release\mvcDivide.sbr
-.\Release\mvcDivisor.sbr
-.\Release\mvcList.sbr
-.\Release\mvcLits.sbr
-.\Release\mvcMan.sbr
-.\Release\mvcOpAlg.sbr
-.\Release\mvcOpBool.sbr
-.\Release\mvcPrint.sbr
-.\Release\mvcSort.sbr
-.\Release\mvcUtils.sbr
-.\Release\ftFactor.sbr
-.\Release\ftPrint.sbr
-.\Release\added.sbr
-.\Release\solver.sbr
-.\Release\msatActivity.sbr
-.\Release\msatClause.sbr
-.\Release\msatClauseVec.sbr
-.\Release\msatMem.sbr
-.\Release\msatOrderJ.sbr
-.\Release\msatQueue.sbr
-.\Release\msatRead.sbr
-.\Release\msatSolverApi.sbr
-.\Release\msatSolverCore.sbr
-.\Release\msatSolverIo.sbr
-.\Release\msatSolverSearch.sbr
-.\Release\msatSort.sbr
-.\Release\msatVec.sbr
-.\Release\fraigApi.sbr
-.\Release\fraigCanon.sbr
-.\Release\fraigFanout.sbr
-.\Release\fraigFeed.sbr
-.\Release\fraigMan.sbr
-.\Release\fraigMem.sbr
-.\Release\fraigNode.sbr
-.\Release\fraigPrime.sbr
-.\Release\fraigSat.sbr
-.\Release\fraigTable.sbr
-.\Release\fraigUtil.sbr
-.\Release\fraigVec.sbr
-.\Release\simMan.sbr
-.\Release\simSat.sbr
-.\Release\simSupp.sbr
-.\Release\simSym.sbr
-.\Release\simUnate.sbr
-.\Release\simUtils.sbr
-.\Release\csat_apis.sbr
-.\Release\fxu.sbr
-.\Release\fxuCreate.sbr
-.\Release\fxuHeapD.sbr
-.\Release\fxuHeapS.sbr
-.\Release\fxuList.sbr
-.\Release\fxuMatrix.sbr
-.\Release\fxuPair.sbr
-.\Release\fxuPrint.sbr
-.\Release\fxuReduce.sbr
-.\Release\fxuSelect.sbr
-.\Release\fxuSingle.sbr
-.\Release\fxuUpdate.sbr
-.\Release\rwrDec.sbr
-.\Release\rwrEva.sbr
-.\Release\rwrExp.sbr
-.\Release\rwrLib.sbr
-.\Release\rwrMan.sbr
-.\Release\rwrPrint.sbr
-.\Release\rwrUtil.sbr
-.\Release\cutMan.sbr
-.\Release\cutMerge.sbr
-.\Release\cutNode.sbr
-.\Release\cutSeq.sbr
-.\Release\cutTable.sbr
-.\Release\cutTruth.sbr
-.\Release\fpga.sbr
-.\Release\fpgaCore.sbr
-.\Release\fpgaCreate.sbr
-.\Release\fpgaCut.sbr
-.\Release\fpgaCutUtils.sbr
-.\Release\fpgaFanout.sbr
-.\Release\fpgaLib.sbr
-.\Release\fpgaMatch.sbr
-.\Release\fpgaTime.sbr
-.\Release\fpgaTruth.sbr
-.\Release\fpgaUtils.sbr
-.\Release\fpgaVec.sbr
-.\Release\mapper.sbr
-.\Release\mapperCanon.sbr
-.\Release\mapperCore.sbr
-.\Release\mapperCreate.sbr
-.\Release\mapperCut.sbr
-.\Release\mapperCutUtils.sbr
-.\Release\mapperFanout.sbr
-.\Release\mapperLib.sbr
-.\Release\mapperMatch.sbr
-.\Release\mapperRefs.sbr
-.\Release\mapperSuper.sbr
-.\Release\mapperTable.sbr
-.\Release\mapperTime.sbr
-.\Release\mapperTree.sbr
-.\Release\mapperTruth.sbr
-.\Release\mapperUtils.sbr
-.\Release\mapperVec.sbr
-.\Release\mio.sbr
-.\Release\mioApi.sbr
-.\Release\mioFunc.sbr
-.\Release\mioRead.sbr
-.\Release\mioUtils.sbr
-.\Release\super.sbr
-.\Release\superAnd.sbr
-.\Release\superGate.sbr
-.\Release\superWrite.sbr
-.\Release\extraUtilBdd.sbr
-.\Release\extraUtilBitMatrix.sbr
-.\Release\extraUtilCanon.sbr
-.\Release\extraUtilFile.sbr
-.\Release\extraUtilMemory.sbr
-.\Release\extraUtilMisc.sbr
-.\Release\extraUtilProgress.sbr
-.\Release\extraUtilReader.sbr
-.\Release\st.sbr
-.\Release\stmm.sbr
-.\Release\cpu_stats.sbr
-.\Release\cpu_time.sbr
-.\Release\datalimit.sbr
-.\Release\getopt.sbr
-.\Release\pathsearch.sbr
-.\Release\safe_mem.sbr
-.\Release\strsav.sbr
-.\Release\texpand.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F4C.tmp"
-Creating browse info file...
-<h3>Output Window</h3>
 
 
 
diff --git a/abc.rc b/abc.rc
index ba6913b8..cf648fcb 100644
--- a/abc.rc
+++ b/abc.rc
@@ -32,7 +32,7 @@ alias wl write_blif
 alias wp write_pla
 alias cnf   "st; renode -c; write_cnf"
 alias prove "st; renode -c; sat"
-alias opt   "b; renode; sop; b; ps"
+alias opt   "b; renode; b; ps"
 alias share "b; renode -m; fx; b; ps"
-alias resyn "b; rwz; rfz; b; rwz; rfz; b; ps"
+alias resyn "b; rw; rf; b; rwz; rfz; b; ps"
 
diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index f8871ba9..7c949ee0 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -445,7 +445,7 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsLogicSop(pNtk) )
+    if ( !Abc_NtkIsSopLogic(pNtk) )
     {
         fprintf( pErr, "Printing factored forms can be done for SOP networks.\n" );
         return 1;
@@ -465,15 +465,11 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
             return 1;
         }
-//        Ft_FactorStartMan();
         Abc_NodePrintFactor( pOut, pNode );
-//        Ft_FactorStopMan();
         return 0;
     }
     // print the nodes
-//    Ft_FactorStartMan();
     Abc_NtkPrintFactor( pOut, pNtk );
-//    Ft_FactorStopMan();
     return 0;
 
 usage:
@@ -508,7 +504,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fProfile = 0;
+    fProfile = 1;
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "ph" ) ) != EOF )
     {
@@ -530,7 +526,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !fProfile && !Abc_NtkIsAig(pNtk) )
+    if ( !fProfile && !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "This command works only for AIGs.\n" );
         return 1;
@@ -607,7 +603,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "This command works only for AIGs.\n" );
         return 1;
@@ -664,7 +660,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsLogicBdd(pNtk) )
+    if ( !Abc_NtkIsBddLogic(pNtk) )
     {
         fprintf( pErr, "Printing BDDs can only be done for logic BDD networks.\n" );
         return 1;
@@ -738,14 +734,14 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Can only collapse a logic network.\n" );
         return 1;
     }
 
     // get the new network
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         pNtkRes = Abc_NtkCollapse( pNtk, 1 );
     else
     {
@@ -880,7 +876,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
     {
         pNtkRes = Abc_NtkBalance( pNtk, fDuplicate );
     }
@@ -992,7 +988,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Cannot renode a network that is not an AIG.\n" );
         return 1;
@@ -1065,7 +1061,7 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" );
         return 1;
@@ -1276,7 +1272,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fGlobal )
     {
         // get the new network
-        if ( !Abc_NtkIsAig(pNtk) )
+        if ( !Abc_NtkIsStrash(pNtk) )
         {
             pNtkNew = Abc_NtkStrash( pNtk, 0 );
             pNtkRes = Abc_NtkDsdGlobal( pNtkNew, fVerbose, fPrint, fShort );
@@ -1305,7 +1301,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else if ( fRecursive )
     {
-        if ( !Abc_NtkIsLogicBdd( pNtk ) )
+        if ( !Abc_NtkIsBddLogic( pNtk ) )
         {
             fprintf( pErr, "This command is only applicable to logic BDD networks.\n" );
             return 1;
@@ -1390,7 +1386,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "This command can only be applied to an AIG.\n" );
         return 1;
@@ -1499,7 +1495,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "This command can only be applied to an AIG.\n" );
         return 1;
@@ -1734,7 +1730,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         pNtkTemp = Abc_NtkStrash( pNtk, 0 );
         pNtkRes  = Abc_NtkFrames( pNtkTemp, nFrames, fInitial );
@@ -1802,7 +1798,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    if ( !Abc_NtkIsLogicBdd(pNtk) )
+    if ( !Abc_NtkIsBddLogic(pNtk) )
     {
         fprintf( pErr, "Converting to SOP is possible when node functions are BDDs.\n" );
         return 1;
@@ -1862,7 +1858,7 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    if ( !Abc_NtkIsLogicSop(pNtk) )
+    if ( !Abc_NtkIsSopLogic(pNtk) )
     {
         fprintf( pErr, "Converting to BDD is possible when node functions are SOPs.\n" );
         return 1;
@@ -1930,16 +1926,15 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
         return 0;
     }
-    if ( !(Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsLogicBdd(pNtk)) )
+    if ( !Abc_NtkIsLogic(pNtk) )
     {
-        fprintf( stdout, "First convert node representation into BDDs or SOPs.\n" );
+        fprintf( stdout, "This command can only be applied to logic network.\n" );
         return 0;
     }
-    if ( Abc_NtkIsLogicSop(pNtk) )
-    {
-//        printf( "Converting node functions from SOP to BDD.\n" );
+    if ( Abc_NtkIsMappedLogic(pNtk) )
+        Abc_NtkUnmap(pNtk);
+    if ( Abc_NtkIsSopLogic(pNtk) )
         Abc_NtkSopToBdd(pNtk);
-    }
 
     if ( Abc_NtkMiterSat( pNtk, fVerbose ) )
         printf( "The miter is satisfiable.\n" );
@@ -2006,7 +2001,7 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "The current network has no latches.\n" );
         return 0;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( stdout, "This command works only for AIGs.\n" );
         return 0;
@@ -2085,7 +2080,7 @@ int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Currently can only be applied to the logic network or an AIG.\n" );
         return 1;
@@ -2280,7 +2275,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Cut computation is available only for AIGs.\n" );
         return 1;
@@ -2415,9 +2410,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Can only fraig a logic network.\n" );
+        fprintf( pErr, "Can only fraig a logic network or an AIG.\n" );
         return 1;
     }
 
@@ -2425,7 +2420,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fVerboseP = pParams->fTryProve;
 
     // get the new network
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
     else
     {
@@ -2750,7 +2745,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Cannot sweep AIGs (use \"fraig\").\n" );
         return 1;
@@ -2848,7 +2843,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         pNtk = Abc_NtkStrash( pNtk, 0 );
         if ( pNtk == NULL )
@@ -2948,7 +2943,7 @@ int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsLogicMap(pNtk) )
+    if ( !Abc_NtkHasMapping(pNtk) )
     {
         fprintf( pErr, "Cannot unmap the network that is not mapped.\n" );
         return 1;
@@ -3010,7 +3005,7 @@ int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsLogicSop(pNtk) )
+    if ( !Abc_NtkIsSopLogic(pNtk) )
     {
         fprintf( pErr, "Can only attach gates if the nodes have SOP representations.\n" );
         return 1;
@@ -3073,7 +3068,7 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Works only for the AIG representation.\n" );
         return 1;
@@ -3148,7 +3143,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
         pNtk = Abc_NtkStrash( pNtk, 0 );
@@ -3241,7 +3236,10 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    printf( "This command is not yet implemented.\n" );
+    return 0;
+
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Works only for AIG.\n" );
         return 1;
@@ -3317,6 +3315,10 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    printf( "This command is not yet implemented.\n" );
+    return 0;
+
+
     if ( !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( pErr, "Works only for sequential AIG.\n" );
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 2366aa10..a3f7ddb7 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -43,36 +43,46 @@
 
 // network types
 typedef enum { 
-    ABC_NTK_NONE,          // 0:  unknown
-    ABC_NTK_NETLIST_SOP,   // 1:  netlist with nodes represented using SOPs
-    ABC_NTK_NETLIST_MAP,   // 2:  netlist with nodes represented using gates from the library
-    ABC_NTK_LOGIC_SOP,     // 3:  only SOP logic nodes (similar to SIS network)
-    ABC_NTK_LOGIC_BDD,     // 4:  only BDD logic nodes (similar to BDS network)
-    ABC_NTK_LOGIC_MAP,     // 5:  only mapped logic nodes (similar to mapped SIS network)
-    ABC_NTK_AIG,           // 6:  AIG or FRAIG (two input gates with c-attributes on edges)
-    ABC_NTK_SEQ,           // 7:  sequential AIG (two input gates with c- and latch-attributes on edges)
-    ABC_NTK_OTHER          // 8:  unused
+    ABC_TYPE_NONE,      // 0:  unknown
+    ABC_TYPE_NETLIST,   // 1:  network with PIs/POs, latches, nodes, and nets
+    ABC_TYPE_LOGIC,     // 2:  network with PIs/POs, latches, and nodes
+    ABC_TYPE_STRASH,    // 3:  structurally hashed AIG (two input AND gates with c-attributes on edges)
+    ABC_TYPE_SEQ,       // 4:  sequential AIG (two input AND gates with c- and latch-attributes on edges)
+    ABC_TYPE_OTHER      // 5:  unused
 } Abc_NtkType_t;
 
 // functionality types
 typedef enum { 
-    ABC_FUNC_NONE,         // 0:  unknown
-    ABC_FUNC_SOP,          // 1:  sum-of-products
-    ABC_FUNC_BDD,          // 2:  binary decision diagrams
-    ABC_FUNC_AIG,          // 3:  and-inverter graphs
-    ABC_FUNC_MAP,          // 4:  standard cell library
-    ABC_FUNC_OTHER         // 5:  unused
-} Abc_FuncType_t;
+    ABC_FUNC_NONE,      // 0:  unknown
+    ABC_FUNC_SOP,       // 1:  sum-of-products
+    ABC_FUNC_BDD,       // 2:  binary decision diagrams
+    ABC_FUNC_AIG,       // 3:  and-inverter graphs
+    ABC_FUNC_MAP,       // 4:  standard cell library
+    ABC_FUNC_OTHER      // 5:  unused
+} Abc_NtkFunc_t;
+
+// Supported type/functionality combinations:
+/*------------------------------------------|
+|           |  SOP  |  BDD  |  AIG  |  Map  |
+|-----------|-------|-------|-------|-------|
+|  Netlist  |   x   |       |       |   x   |
+|-----------|-------|-------|-------|-------|
+|  Logic    |   x   |   x   |       |   x   |
+|-----------|-------|-------|-------|-------|
+|  Strash   |       |       |   x   |       |
+|-----------|-------|-------|-------|-------|
+|  Seq      |       |       |   x   |       | 
+--------------------------------------------|*/
 
 // object types
 typedef enum { 
-    ABC_OBJ_NONE,          // 0:  unknown
-    ABC_OBJ_NET,           // 1:  net
-    ABC_OBJ_NODE,          // 2:  node
-    ABC_OBJ_LATCH,         // 3:  latch
-    ABC_OBJ_PI,            // 4:  primary input terminal
-    ABC_OBJ_PO,            // 5:  primary output terminal
-    ABC_OBJ_OTHER          // 6:  unused
+    ABC_OBJ_NONE,       // 0:  unknown
+    ABC_OBJ_NET,        // 1:  net
+    ABC_OBJ_NODE,       // 2:  node
+    ABC_OBJ_LATCH,      // 3:  latch
+    ABC_OBJ_PI,         // 4:  primary input terminal
+    ABC_OBJ_PO,         // 5:  primary output terminal
+    ABC_OBJ_OTHER       // 6:  unused
 } Abc_ObjType_t;
 
 ////////////////////////////////////////////////////////////////////////
@@ -124,7 +134,8 @@ struct Abc_Obj_t_ // 12 words
 struct Abc_Ntk_t_ 
 {
     // general information 
-    Abc_NtkType_t    Type;          // type of the network
+    Abc_NtkType_t    ntkType;       // type of the network
+    Abc_NtkFunc_t    ntkFunc;       // functionality of the network
     char *           pName;         // the network name
     char *           pSpec;         // the name of the spec file if present
     // name representation 
@@ -177,13 +188,31 @@ struct Abc_Ntk_t_
 #define ABC_MAX(a,b)      (((a) > (b))? (a) : (b))
 #define ABC_INFINITY      (10000000)
 
+// checking the network type
+static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )       { return pNtk->ntkType == ABC_TYPE_NETLIST; }
+static inline bool        Abc_NtkIsLogic( Abc_Ntk_t * pNtk )         { return pNtk->ntkType == ABC_TYPE_LOGIC;   }
+static inline bool        Abc_NtkIsStrash( Abc_Ntk_t * pNtk )        { return pNtk->ntkType == ABC_TYPE_STRASH;  }
+static inline bool        Abc_NtkIsSeq( Abc_Ntk_t * pNtk )           { return pNtk->ntkType == ABC_TYPE_SEQ;     }
+
+static inline bool        Abc_NtkHasSop( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_SOP;    }
+static inline bool        Abc_NtkHasBdd( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_BDD;    }
+static inline bool        Abc_NtkHasAig( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_AIG;    }
+static inline bool        Abc_NtkHasMapping( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_MAP;    }
+
+static inline bool        Abc_NtkIsSopNetlist( Abc_Ntk_t * pNtk )    { return pNtk->ntkFunc == ABC_FUNC_SOP && pNtk->ntkType == ABC_TYPE_NETLIST;  }
+static inline bool        Abc_NtkIsMappedNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_MAP && pNtk->ntkType == ABC_TYPE_NETLIST;  }
+static inline bool        Abc_NtkIsSopLogic( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_SOP && pNtk->ntkType == ABC_TYPE_LOGIC  ;  }
+static inline bool        Abc_NtkIsBddLogic( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_BDD && pNtk->ntkType == ABC_TYPE_LOGIC  ;  }
+static inline bool        Abc_NtkIsMappedLogic( Abc_Ntk_t * pNtk )   { return pNtk->ntkFunc == ABC_FUNC_MAP && pNtk->ntkType == ABC_TYPE_LOGIC  ;  }
+static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )          { return pNtk->nLatches == 0;      }
+
 // reading data members of the network
-static inline char *      Abc_NtkName( Abc_Ntk_t * pNtk )         { return pNtk->pName;           }
-static inline char *      Abc_NtkSpec( Abc_Ntk_t * pNtk )         { return pNtk->pSpec;           }
-static inline int         Abc_NtkTravId( Abc_Ntk_t * pNtk )       { return pNtk->nTravIds;        }    
-static inline Abc_Ntk_t * Abc_NtkExdc( Abc_Ntk_t * pNtk )         { return pNtk->pExdc;           }
-static inline Abc_Ntk_t * Abc_NtkBackup( Abc_Ntk_t * pNtk )       { return pNtk->pNetBackup;      }
-static inline int         Abc_NtkStep  ( Abc_Ntk_t * pNtk )       { return pNtk->iStep;           }
+static inline char *      Abc_NtkName( Abc_Ntk_t * pNtk )            { return pNtk->pName;           }
+static inline char *      Abc_NtkSpec( Abc_Ntk_t * pNtk )            { return pNtk->pSpec;           }
+static inline int         Abc_NtkTravId( Abc_Ntk_t * pNtk )          { return pNtk->nTravIds;        }    
+static inline Abc_Ntk_t * Abc_NtkExdc( Abc_Ntk_t * pNtk )            { return pNtk->pExdc;           }
+static inline Abc_Ntk_t * Abc_NtkBackup( Abc_Ntk_t * pNtk )          { return pNtk->pNetBackup;      }
+static inline int         Abc_NtkStep  ( Abc_Ntk_t * pNtk )          { return pNtk->iStep;           }
 
 // setting data members of the network
 static inline void        Abc_NtkSetName  ( Abc_Ntk_t * pNtk, char * pName )           { pNtk->pName      = pName;      } 
@@ -192,98 +221,83 @@ static inline void        Abc_NtkSetBackup( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNetBa
 static inline void        Abc_NtkSetStep  ( Abc_Ntk_t * pNtk, int iStep )              { pNtk->iStep      = iStep;      }
 
 // getting the number of objects 
-static inline int         Abc_NtkObjNumMax( Abc_Ntk_t * pNtk )    { return pNtk->vObjs->nSize;         }
-static inline int         Abc_NtkObjNum( Abc_Ntk_t * pNtk )       { return pNtk->nObjs;                }
-static inline int         Abc_NtkNetNum( Abc_Ntk_t * pNtk )       { return pNtk->nNets;                }
-static inline int         Abc_NtkNodeNum( Abc_Ntk_t * pNtk )      { return pNtk->nNodes;               }
-static inline int         Abc_NtkLatchNum( Abc_Ntk_t * pNtk )     { return pNtk->nLatches;             }
-static inline int         Abc_NtkPiNum( Abc_Ntk_t * pNtk )        { return pNtk->nPis;                 }
-static inline int         Abc_NtkPoNum( Abc_Ntk_t * pNtk )        { return pNtk->nPos;                 }
-static inline int         Abc_NtkCiNum( Abc_Ntk_t * pNtk )        { return pNtk->vCis->nSize;          }
-static inline int         Abc_NtkCoNum( Abc_Ntk_t * pNtk )        { return pNtk->vCos->nSize;          }
+static inline int         Abc_NtkObjNumMax( Abc_Ntk_t * pNtk )       { return pNtk->vObjs->nSize;         }
+static inline int         Abc_NtkObjNum( Abc_Ntk_t * pNtk )          { return pNtk->nObjs;                }
+static inline int         Abc_NtkNetNum( Abc_Ntk_t * pNtk )          { return pNtk->nNets;                }
+static inline int         Abc_NtkNodeNum( Abc_Ntk_t * pNtk )         { return pNtk->nNodes;               }
+static inline int         Abc_NtkLatchNum( Abc_Ntk_t * pNtk )        { return pNtk->nLatches;             }
+static inline int         Abc_NtkPiNum( Abc_Ntk_t * pNtk )           { return pNtk->nPis;                 }
+static inline int         Abc_NtkPoNum( Abc_Ntk_t * pNtk )           { return pNtk->nPos;                 }
+static inline int         Abc_NtkCiNum( Abc_Ntk_t * pNtk )           { return pNtk->vCis->nSize;          }
+static inline int         Abc_NtkCoNum( Abc_Ntk_t * pNtk )           { return pNtk->vCos->nSize;          }
 
 // reading objects
-static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i )   { assert( i < Vec_PtrSize(pNtk->vObjs) ); return pNtk->vObjs->pArray[i];  }
-static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i ) { assert( i < Vec_PtrSize(pNtk->vLats) ); return pNtk->vLats->pArray[i];  }
-static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i )    { assert( i < Abc_NtkPiNum(pNtk) ); return pNtk->vCis->pArray[i];      }
-static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i )    { assert( i < Abc_NtkPoNum(pNtk) ); return pNtk->vCos->pArray[i];      }
-static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i )    { assert( i < Abc_NtkCiNum(pNtk) ); return pNtk->vCis->pArray[i];      }
-static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i )    { assert( i < Abc_NtkCoNum(pNtk) ); return pNtk->vCos->pArray[i];      }
-
-// checking the network type
-static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )    { return pNtk->Type == ABC_NTK_NETLIST_SOP || pNtk->Type == ABC_NTK_NETLIST_MAP;   }
-static inline bool        Abc_NtkIsNetlistSop( Abc_Ntk_t * pNtk ) { return pNtk->Type == ABC_NTK_NETLIST_SOP;   }
-static inline bool        Abc_NtkIsNetlistMap( Abc_Ntk_t * pNtk ) { return pNtk->Type == ABC_NTK_NETLIST_MAP;   }
-static inline bool        Abc_NtkIsLogic( Abc_Ntk_t * pNtk )      { return pNtk->Type == ABC_NTK_LOGIC_SOP || pNtk->Type == ABC_NTK_LOGIC_BDD || pNtk->Type == ABC_NTK_LOGIC_MAP; }
-static inline bool        Abc_NtkIsLogicSop( Abc_Ntk_t * pNtk )   { return pNtk->Type == ABC_NTK_LOGIC_SOP; }
-static inline bool        Abc_NtkIsLogicBdd( Abc_Ntk_t * pNtk )   { return pNtk->Type == ABC_NTK_LOGIC_BDD; }
-static inline bool        Abc_NtkIsLogicMap( Abc_Ntk_t * pNtk )   { return pNtk->Type == ABC_NTK_LOGIC_MAP; }
-static inline bool        Abc_NtkIsAig( Abc_Ntk_t * pNtk )        { return pNtk->Type == ABC_NTK_AIG;       }
-static inline bool        Abc_NtkIsSeq( Abc_Ntk_t * pNtk )        { return pNtk->Type == ABC_NTK_SEQ;       }
-static inline bool        Abc_NtkIsMapped( Abc_Ntk_t * pNtk )     { return pNtk->Type == ABC_NTK_NETLIST_MAP || pNtk->Type == ABC_NTK_LOGIC_MAP; }
-static inline bool        Abc_NtkIsSop( Abc_Ntk_t * pNtk )        { return pNtk->Type == ABC_NTK_NETLIST_SOP || pNtk->Type == ABC_NTK_LOGIC_SOP; }
-static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )       { return Abc_NtkLatchNum(pNtk) == 0;      }
-
+static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i )      { assert( i < Vec_PtrSize(pNtk->vObjs) ); return pNtk->vObjs->pArray[i];  }
+static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i )    { assert( i < Vec_PtrSize(pNtk->vLats) ); return pNtk->vLats->pArray[i];  }
+static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkPiNum(pNtk) ); return pNtk->vCis->pArray[i];      }
+static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkPoNum(pNtk) ); return pNtk->vCos->pArray[i];      }
+static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkCiNum(pNtk) ); return pNtk->vCis->pArray[i];      }
+static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkCoNum(pNtk) ); return pNtk->vCos->pArray[i];      }
 
 // reading data members of the object
-static inline unsigned    Abc_ObjType( Abc_Obj_t * pObj )         { return pObj->Type;               }
-static inline unsigned    Abc_ObjId( Abc_Obj_t * pObj )           { return pObj->Id;                 }
-static inline int         Abc_ObjTravId( Abc_Obj_t * pObj )       { return pObj->TravId;             }
-static inline Vec_Fan_t * Abc_ObjFaninVec( Abc_Obj_t * pObj )     { return &pObj->vFanins;           }
-static inline Vec_Fan_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj )    { return &pObj->vFanouts;          }
-static inline Abc_Obj_t * Abc_ObjCopy( Abc_Obj_t * pObj )         { return pObj->pCopy;              }
-static inline Abc_Ntk_t * Abc_ObjNtk( Abc_Obj_t * pObj )          { return pObj->pNtk;               }
-static inline void *      Abc_ObjData( Abc_Obj_t * pObj )         { return pObj->pData;              }
+static inline unsigned    Abc_ObjType( Abc_Obj_t * pObj )            { return pObj->Type;               }
+static inline unsigned    Abc_ObjId( Abc_Obj_t * pObj )              { return pObj->Id;                 }
+static inline int         Abc_ObjTravId( Abc_Obj_t * pObj )          { return pObj->TravId;             }
+static inline Vec_Fan_t * Abc_ObjFaninVec( Abc_Obj_t * pObj )        { return &pObj->vFanins;           }
+static inline Vec_Fan_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj )       { return &pObj->vFanouts;          }
+static inline Abc_Obj_t * Abc_ObjCopy( Abc_Obj_t * pObj )            { return pObj->pCopy;              }
+static inline Abc_Ntk_t * Abc_ObjNtk( Abc_Obj_t * pObj )             { return pObj->pNtk;               }
+static inline void *      Abc_ObjData( Abc_Obj_t * pObj )            { return pObj->pData;              }
 
 // setting data members of the network
-static inline void        Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy )             { pObj->pCopy    =  pCopy;    } 
-static inline void        Abc_ObjSetData( Abc_Obj_t * pObj, void * pData )                  { pObj->pData    =  pData;    } 
+static inline void        Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy )  { pObj->pCopy    =  pCopy;    } 
+static inline void        Abc_ObjSetData( Abc_Obj_t * pObj, void * pData )       { pObj->pData    =  pData;    } 
 
 // working with complemented attributes of objects
-static inline bool        Abc_ObjIsComplement( Abc_Obj_t * p )    { return (bool)(((unsigned)p) & 01);           }
-static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p )         { return (Abc_Obj_t *)((unsigned)(p) & ~01);  }
-static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p )             { return (Abc_Obj_t *)((unsigned)(p) ^  01);  }
-static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c )  { return (Abc_Obj_t *)((unsigned)(p) ^ (c));  }
+static inline bool        Abc_ObjIsComplement( Abc_Obj_t * p )       { return (bool)(((unsigned)p) & 01);           }
+static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p )            { return (Abc_Obj_t *)((unsigned)(p) & ~01);  }
+static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p )                { return (Abc_Obj_t *)((unsigned)(p) ^  01);  }
+static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c )     { return (Abc_Obj_t *)((unsigned)(p) ^ (c));  }
 
 // checking the object type
-static inline bool        Abc_ObjIsNode( Abc_Obj_t * pObj )       { return pObj->Type == ABC_OBJ_NODE;   }
-static inline bool        Abc_ObjIsNet( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_NET;    }
-static inline bool        Abc_ObjIsLatch( Abc_Obj_t * pObj )      { return pObj->Type == ABC_OBJ_LATCH;  }
-static inline bool        Abc_ObjIsPi( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_PI;     }
-static inline bool        Abc_ObjIsPo( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_PO;     }
-static inline bool        Abc_ObjIsPio( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO;    }
-static inline bool        Abc_ObjIsCi( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_LATCH; }
-static inline bool        Abc_ObjIsCo( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
-static inline bool        Abc_ObjIsCio( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
+static inline bool        Abc_ObjIsNode( Abc_Obj_t * pObj )          { return pObj->Type == ABC_OBJ_NODE;   }
+static inline bool        Abc_ObjIsNet( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_NET;    }
+static inline bool        Abc_ObjIsLatch( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_LATCH;  }
+static inline bool        Abc_ObjIsPi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PI;     }
+static inline bool        Abc_ObjIsPo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO;     }
+static inline bool        Abc_ObjIsPio( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO;    }
+static inline bool        Abc_ObjIsCi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_LATCH; }
+static inline bool        Abc_ObjIsCo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
+static inline bool        Abc_ObjIsCio( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
 
 // working with fanin/fanout edges
-static inline int         Abc_ObjFaninNum( Abc_Obj_t * pObj )     { return pObj->vFanins.nSize;      }
-static inline int         Abc_ObjFanoutNum( Abc_Obj_t * pObj )    { return pObj->vFanouts.nSize;     }
-static inline int         Abc_ObjFaninId( Abc_Obj_t * pObj, int i){ return pObj->vFanins.pArray[i].iFan; }
-static inline int         Abc_ObjFaninId0( Abc_Obj_t * pObj )     { return pObj->vFanins.pArray[0].iFan; }
-static inline int         Abc_ObjFaninId1( Abc_Obj_t * pObj )     { return pObj->vFanins.pArray[1].iFan; }
-static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ){ return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ];   }
-static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )      { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ];   }
-static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )       { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )       { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )    { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj;     }
-static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )   { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj;    }
-static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].fCompl;                               }
-static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].fCompl;                               }
-static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].fCompl;                               }
+static inline int         Abc_ObjFaninNum( Abc_Obj_t * pObj )        { return pObj->vFanins.nSize;      }
+static inline int         Abc_ObjFanoutNum( Abc_Obj_t * pObj )       { return pObj->vFanouts.nSize;     }
+static inline int         Abc_ObjFaninId( Abc_Obj_t * pObj, int i)   { return pObj->vFanins.pArray[i].iFan; }
+static inline int         Abc_ObjFaninId0( Abc_Obj_t * pObj )        { return pObj->vFanins.pArray[0].iFan; }
+static inline int         Abc_ObjFaninId1( Abc_Obj_t * pObj )        { return pObj->vFanins.pArray[1].iFan; }
+static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i )   { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ];   }
+static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )         { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ];   }
+static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i )    { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )          { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )          { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )       { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj;     }
+static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )      { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj;    }
+static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i )   { return pObj->vFanins.pArray[i].fCompl;                               }
+static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[0].fCompl;                               }
+static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[1].fCompl;                               }
 static inline bool        Abc_ObjFanoutC( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) {  assert( !Abc_NtkIsLogic(pObj->pNtk) ); return (Abc_ObjFaninId0(pFanout) == (int)pObj->Id)? Abc_ObjFaninC0(pFanout) : Abc_ObjFaninC1(pFanout);  }
-static inline int         Abc_ObjFaninL( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].nLats;                                }
-static inline int         Abc_ObjFaninL0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].nLats;                                }
-static inline int         Abc_ObjFaninL1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].nLats;                                }
-static inline int         Abc_ObjFaninLMin( Abc_Obj_t * pObj )   {  assert( Abc_ObjIsNode(pObj) ); return ABC_MIN( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
-static inline int         Abc_ObjFaninLMax( Abc_Obj_t * pObj )   {  assert( Abc_ObjIsNode(pObj) ); return ABC_MAX( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
-static inline Abc_Obj_t * Abc_ObjChild( Abc_Obj_t * pObj, int i ) { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i), Abc_ObjFaninC(pObj,i) );}
-static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );  }
-static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) );  }
-static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ) { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );}
-static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );  }
-static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );  }
+static inline int         Abc_ObjFaninL( Abc_Obj_t * pObj, int i )   { return pObj->vFanins.pArray[i].nLats;                                }
+static inline int         Abc_ObjFaninL0( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[0].nLats;                                }
+static inline int         Abc_ObjFaninL1( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[1].nLats;                                }
+static inline int         Abc_ObjFaninLMin( Abc_Obj_t * pObj )       {  assert( Abc_ObjIsNode(pObj) ); return ABC_MIN( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
+static inline int         Abc_ObjFaninLMax( Abc_Obj_t * pObj )       {  assert( Abc_ObjIsNode(pObj) ); return ABC_MAX( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
+static inline Abc_Obj_t * Abc_ObjChild( Abc_Obj_t * pObj, int i )    { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i), Abc_ObjFaninC(pObj,i) );}
+static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj )          { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )          { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );}
+static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );  }
 static inline Abc_Obj_t * Abc_ObjFanoutFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) {  assert( !Abc_NtkIsLogic(pObj->pNtk) ); return (Abc_ObjFaninId0(pFanout) == (int)pObj->Id)? Abc_ObjChild0(pFanout) : Abc_ObjChild1(pFanout);  }
 static inline void        Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1;                               }
 static inline void        Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1;                              }
@@ -300,9 +314,9 @@ extern int                Abc_ObjFanoutLMin( Abc_Obj_t * pObj );
 extern int                Abc_ObjFanoutLMax( Abc_Obj_t * pObj );
 
 // checking the node type
-static inline bool        Abc_NodeIsAigAnd( Abc_Obj_t * pNode )   { assert(Abc_NtkIsAig(pNode->pNtk) || Abc_NtkIsSeq(pNode->pNtk)); return Abc_ObjFaninNum(pNode) == 2;                         }
-static inline bool        Abc_NodeIsAigChoice( Abc_Obj_t * pNode ){ assert(Abc_NtkIsAig(pNode->pNtk) || Abc_NtkIsSeq(pNode->pNtk)); return pNode->pData != NULL && Abc_ObjFanoutNum(pNode) > 0; }
-static inline bool        Abc_NodeIsConst( Abc_Obj_t * pNode )    { assert(Abc_ObjIsNode(Abc_ObjRegular(pNode)));                   return Abc_ObjFaninNum(Abc_ObjRegular(pNode)) == 0;         }
+static inline bool        Abc_NodeIsAigAnd( Abc_Obj_t * pNode )      { assert(Abc_NtkHasAig(pNode->pNtk));           return Abc_ObjFaninNum(pNode) == 2;                         }
+static inline bool        Abc_NodeIsAigChoice( Abc_Obj_t * pNode )   { assert(Abc_NtkHasAig(pNode->pNtk));           return pNode->pData != NULL && Abc_ObjFanoutNum(pNode) > 0; }
+static inline bool        Abc_NodeIsConst( Abc_Obj_t * pNode )       { assert(Abc_ObjIsNode(Abc_ObjRegular(pNode))); return Abc_ObjFaninNum(Abc_ObjRegular(pNode)) == 0;         }
 extern        bool        Abc_NodeIsConst0( Abc_Obj_t * pNode );    
 extern        bool        Abc_NodeIsConst1( Abc_Obj_t * pNode );    
 extern        bool        Abc_NodeIsBuf( Abc_Obj_t * pNode );    
@@ -398,8 +412,8 @@ extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
 extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly );
 extern void               Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
 /*=== abcCreate.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type );
-extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type );
+extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 2200bea1..f71c0a15 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -294,7 +294,7 @@ bool Abc_AigCheck( Abc_Aig_t * pMan )
             Counter++;
     if ( Counter != Abc_NtkNodeNum(pMan->pNtkAig) )
     {
-        printf( "Abc_AigCheck: The number of nodes in the structural hashing table is wrong.\n", Counter );
+        printf( "Abc_AigCheck: The number of nodes in the structural hashing table is wrong.\n" );
         return 0;
     }
     return 1;
@@ -315,7 +315,7 @@ int Abc_AigGetLevelNum( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, LevelsMax;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // perform the traversal
     LevelsMax = 0;
     Abc_NtkForEachCo( pNtk, pNode, i )
@@ -718,12 +718,21 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
         // such node does not exist - modify the old fanout node 
         // (this way the change will not propagate all the way to the COs)
         assert( Abc_ObjRegular(pFanin1) != Abc_ObjRegular(pFanin2) );             
+
+        // if the node is in the level structure, remove it
+        if ( pFanout->fMarkA )
+            Abc_AigRemoveFromLevelStructure( pMan->vLevels, pFanout );
+        // if the node is in the level structure, remove it
+        if ( pFanout->fMarkB )
+            Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanout );
+
         // remove the old fanout node from the structural hashing table
         Abc_AigAndDelete( pMan, pFanout );
         // remove the fanins of the old fanout
         Abc_ObjRemoveFanins( pFanout );
         // recreate the old fanout with new fanins and add it to the table
         Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
+
         // schedule the updated fanout for updating direct level
         assert( pFanout->fMarkA == 0 );
         pFanout->fMarkA = 1;
@@ -732,6 +741,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
         assert( pFanout->fMarkB == 0 );
         pFanout->fMarkB = 1;
         Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout );
+
         // the fanout has changed, update EXOR status of its fanouts
         Abc_ObjForEachFanout( pFanout, pFanoutFanout, v )
             if ( Abc_NodeIsAigAnd(pFanoutFanout) )
diff --git a/src/base/abc/abcAttach.c b/src/base/abc/abcAttach.c
index 47e911c9..a8e06555 100644
--- a/src/base/abc/abcAttach.c
+++ b/src/base/abc/abcAttach.c
@@ -64,7 +64,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
     Mio_Gate_t ** ppGates;
     int nGates, nFanins, i;
 
-    assert( Abc_NtkIsLogicSop(pNtk) );
+    assert( Abc_NtkIsSopLogic(pNtk) );
 
     // check that the library is available
     pGenlib = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
@@ -142,7 +142,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
     // replace SOP representation by the gate representation
     Abc_NtkForEachNode( pNtk, pNode, i )
         pNode->pData = pNode->pCopy, pNode->pCopy = NULL;
-    pNtk->Type = ABC_NTK_LOGIC_MAP;
+    pNtk->ntkFunc = ABC_FUNC_MAP;
     Extra_MmFlexStop( pNtk->pManFunc, 0 );
     pNtk->pManFunc = pGenlib;
 
diff --git a/src/base/abc/abcBalance.c b/src/base/abc/abcBalance.c
index bcf1032b..7deab3ba 100644
--- a/src/base/abc/abcBalance.c
+++ b/src/base/abc/abcBalance.c
@@ -48,9 +48,9 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkAig;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // perform balancing
-    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG );
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
     Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate );
     Abc_NtkFinalize( pNtk, pNtkAig );
     // make sure everything is okay
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index e8b00271..25d1c86c 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -57,12 +57,17 @@ bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pNet, * pNode;
     int i;
 
-    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) && !Abc_NtkIsSeq(pNtk) )
+    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( stdout, "NetworkCheck: Unknown network type.\n" );
         return 0;
     }
-    if ( Abc_NtkIsMapped(pNtk) )
+    if ( !Abc_NtkHasSop(pNtk) && !Abc_NtkHasBdd(pNtk) && !Abc_NtkHasAig(pNtk) && !Abc_NtkHasMapping(pNtk) )
+    {
+        fprintf( stdout, "NetworkCheck: Unknown functionality type.\n" );
+        return 0;
+    }
+    if ( Abc_NtkHasMapping(pNtk) )
     {
         if ( pNtk->pManFunc != Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) )
         {
@@ -110,9 +115,9 @@ bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
     }
 
     // check the nodes
-    if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
     {
-        if ( Abc_NtkIsAig(pNtk) ) 
+        if ( Abc_NtkIsStrash(pNtk) ) 
             Abc_AigCheck( pNtk->pManFunc );
     }
     else
@@ -474,7 +479,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
         return 0;
     }
     // the netlist and SOP logic network should have SOPs
-    if ( Abc_NtkIsNetlistSop(pNtk) || Abc_NtkIsLogicSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
     {
         if ( !Abc_SopCheck( pNode->pData, Abc_ObjFaninNum(pNode) ) )
         {
@@ -482,7 +487,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
             return 0;
         }
     }
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
     {
         int nSuppSize = Cudd_SupportSize(pNtk->pManFunc, pNode->pData);
         if ( nSuppSize > Abc_ObjFaninNum(pNode) )
@@ -491,7 +496,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
             return 0;
         }
     }
-    else if ( !Abc_NtkIsMapped(pNtk) )
+    else if ( !Abc_NtkHasMapping(pNtk) )
     {
         assert( 0 );
     }
diff --git a/src/base/abc/abcCollapse.c b/src/base/abc/abcCollapse.c
index 2b2da719..e07636cc 100644
--- a/src/base/abc/abcCollapse.c
+++ b/src/base/abc/abcCollapse.c
@@ -49,7 +49,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
     Abc_Ntk_t * pNtkNew;
     DdManager * dd;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // compute the global BDDs
     dd = Abc_NtkGlobalBdds( pNtk, 0 );    
@@ -230,7 +230,7 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode, * pNodeNew;
     int i;
     // start the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
     // make sure the new manager has the same number of inputs
     Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
     // process the POs
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index 7de9ea3e..9186ec5a 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -47,12 +47,13 @@ static void          Abc_ObjAdd( Abc_Obj_t * pObj );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type )
+Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 {
     Abc_Ntk_t * pNtk;
     pNtk = ALLOC( Abc_Ntk_t, 1 );
     memset( pNtk, 0, sizeof(Abc_Ntk_t) );
-    pNtk->Type        = Type;
+    pNtk->ntkType     = Type;
+    pNtk->ntkFunc     = Func;
     // start the object storage
     pNtk->vObjs       = Vec_PtrAlloc( 100 );
     pNtk->vLats       = Vec_PtrAlloc( 100 );
@@ -71,13 +72,13 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type )
     // get ready to assign the first Obj ID
     pNtk->nTravIds    = 1;
     // start the functionality manager
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNtk->pManFunc = Extra_MmFlexStart();
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    else if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+    else if ( Abc_NtkHasAig(pNtk) )
         pNtk->pManFunc = Abc_AigAlloc( pNtk );
-    else if ( Abc_NtkIsMapped(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
         pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
     else
         assert( 0 );
@@ -95,7 +96,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type )
+Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pObjNew;
@@ -103,7 +104,7 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type )
     if ( pNtk == NULL )
         return NULL;
     // start the network
-    pNtkNew = Abc_NtkAlloc( Type );
+    pNtkNew = Abc_NtkAlloc( Type, Func );
     // duplicate the name and the spec
     pNtkNew->pName = util_strsav(pNtk->pName);
     pNtkNew->pSpec = util_strsav(pNtk->pSpec);
@@ -190,7 +191,7 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName )
 {
     Abc_Ntk_t * pNtkNew; 
     // allocate the empty network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST_SOP );
+    pNtkNew = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP );
     // set the specs
     pNtkNew->pName = util_strsav( pName );
     pNtkNew->pSpec = util_strsav( pName );
@@ -244,9 +245,9 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
     if ( pNtk == NULL )
         return NULL;
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->Type );
+    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
     // copy the internal nodes
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc );
     else
     {
@@ -286,11 +287,11 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll
     char Buffer[1000];
     int i, k;
 
-    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
     assert( Abc_ObjIsCo(pNode) ); 
     
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->Type );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
     // set the name
     sprintf( Buffer, "%s_%s", pNtk->pName, Abc_ObjName(pNode) );
     pNtkNew->pName = util_strsav(Buffer);
@@ -307,14 +308,14 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll
         }
     }
     // establish connection between the constant nodes
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
 
     // copy the nodes
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         // if it is an AIG, add to the hash table
-        if ( Abc_NtkIsAig(pNtk) )
+        if ( Abc_NtkIsStrash(pNtk) )
         {
             pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
         }
@@ -359,7 +360,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t *
     
     // start the network
     Abc_NtkCleanCopy( pNtk );
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
     pNtkNew->pName = util_strsav(pNtk->pName);
 
     // collect the nodes in the TFI of the output
@@ -425,7 +426,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     }
 
     // dereference the BDDs
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         Abc_NtkForEachNode( pNtk, pObj, i )
             Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
         
@@ -458,13 +459,13 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     if ( pNtk->pManTime )
         Abc_ManTimeStop( pNtk->pManTime );
     // start the functionality manager
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         Extra_MmFlexStop( pNtk->pManFunc, 0 );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         Extra_StopManager( pNtk->pManFunc );
-    else if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+    else if ( Abc_NtkHasAig(pNtk) )
         Abc_AigFree( pNtk->pManFunc );
-    else if ( !Abc_NtkIsMapped(pNtk) )
+    else if ( !Abc_NtkHasMapping(pNtk) )
         assert( 0 );
     free( pNtk );
 }
@@ -637,17 +638,17 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pObjNew;
     pObjNew = Abc_ObjAlloc( pNtkNew, pObj->Type );
-    if ( Abc_ObjIsNode(pObj) ) // copy the function if network is the same type
+    if ( Abc_ObjIsNode(pObj) ) // copy the function if functionality is compatible
     {
-        if ( pNtkNew->Type == pObj->pNtk->Type || Abc_NtkIsNetlist(pObj->pNtk) || Abc_NtkIsNetlist(pNtkNew) ) 
+        if ( pNtkNew->ntkFunc == pObj->pNtk->ntkFunc ) 
         {
-            if ( Abc_NtkIsSop(pNtkNew) )
+            if ( Abc_NtkHasSop(pNtkNew) )
                 pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pObj->pData );
-            else if ( Abc_NtkIsLogicBdd(pNtkNew) )
+            else if ( Abc_NtkHasBdd(pNtkNew) )
                 pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData);
-            else if ( Abc_NtkIsMapped(pNtkNew) )
+            else if ( Abc_NtkHasMapping(pNtkNew) )
                 pObjNew->pData = pObj->pData;
-            else if ( !Abc_NtkIsAig(pNtkNew) && !Abc_NtkIsSeq(pNtkNew) )
+            else if ( Abc_NtkHasAig(pNtkNew) )
                 assert( 0 );
         }
     }
@@ -675,8 +676,8 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
 { 
     Abc_Obj_t * pConst1;
-    assert( Abc_NtkIsAig(pNtkAig) || Abc_NtkIsSeq(pNtkAig) );
-    assert( Abc_NtkIsLogicSop(pNtkNew) );
+    assert( Abc_NtkIsStrash(pNtkAig) );
+    assert( Abc_NtkIsSopLogic(pNtkNew) );
     pConst1 = Abc_AigConst1(pNtkAig->pManFunc);
     if ( Abc_ObjFanoutNum(pConst1) > 0 )
         pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew );
@@ -697,8 +698,8 @@ Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )
 Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
 { 
     Abc_Obj_t * pReset, * pConst1;
-    assert( Abc_NtkIsAig(pNtkAig) || Abc_NtkIsSeq(pNtkAig) );
-    assert( Abc_NtkIsLogicSop(pNtkNew) );
+    assert( Abc_NtkIsStrash(pNtkAig) );
+    assert( Abc_NtkIsSopLogic(pNtkNew) );
     pReset = Abc_AigReset(pNtkAig->pManFunc);
     if ( Abc_ObjFanoutNum(pReset) > 0 )
     {
@@ -998,12 +999,13 @@ Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )
 Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
+    assert( !Abc_NtkHasAig(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 0\n" );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadLogicZero(pNtk->pManFunc), Cudd_Ref( pNode->pData );
-    else if ( Abc_NtkIsMapped(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadConst0(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
     else
         assert( 0 );
@@ -1024,14 +1026,14 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
 Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
-    if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return Abc_AigConst1(pNtk->pManFunc);
     pNode = Abc_NtkCreateNode( pNtk );   
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 1\n" );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadOne(pNtk->pManFunc), Cudd_Ref( pNode->pData );
-    else if ( Abc_NtkIsMapped(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadConst1(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
     else
         assert( 0 );
@@ -1055,11 +1057,11 @@ Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
     Abc_ObjAddFanin( pNode, pFanin );
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, "0 1\n" );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_Not(Cudd_bddIthVar(pNtk->pManFunc,0)), Cudd_Ref( pNode->pData );
-    else if ( Abc_NtkIsMapped(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadInv(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
     else
         assert( 0 );
@@ -1083,11 +1085,11 @@ Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
     Abc_ObjAddFanin( pNode, pFanin );
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, "1 1\n" );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_bddIthVar(pNtk->pManFunc,0), Cudd_Ref( pNode->pData );
-    else if ( Abc_NtkIsMapped(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadBuf(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
     else
         assert( 0 );
@@ -1113,7 +1115,7 @@ Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
     pNode = Abc_NtkCreateNode( pNtk );   
     for ( i = 0; i < vFanins->nSize; i++ )
         Abc_ObjAddFanin( pNode, vFanins->pArray[i] );
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
     {
         char * pSop;
         pSop = Extra_MmFlexEntryFetch( pNtk->pManFunc, vFanins->nSize + 4 );
@@ -1126,7 +1128,7 @@ Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
         assert( i == vFanins->nSize + 4 );
         pNode->pData = pSop;
     }
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
     {
         DdManager * dd = pNtk->pManFunc;
         DdNode * bFunc, * bTemp;
@@ -1162,7 +1164,7 @@ Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
     pNode = Abc_NtkCreateNode( pNtk );   
     for ( i = 0; i < vFanins->nSize; i++ )
         Abc_ObjAddFanin( pNode, vFanins->pArray[i] );
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
     {
         char * pSop;
         pSop = Extra_MmFlexEntryFetch( pNtk->pManFunc, vFanins->nSize + 4 );
@@ -1175,7 +1177,7 @@ Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
         assert( i == vFanins->nSize + 4 );
         pNode->pData = pSop;
     }
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
     {
         DdManager * dd = pNtk->pManFunc;
         DdNode * bFunc, * bTemp;
@@ -1211,9 +1213,9 @@ Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t *
     Abc_ObjAddFanin( pNode, pNodeC );
     Abc_ObjAddFanin( pNode, pNode1 );
     Abc_ObjAddFanin( pNode, pNode0 );
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, "11- 1\n0-1 1\n" );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_bddIte(pNtk->pManFunc,Cudd_bddIthVar(pNtk->pManFunc,0),Cudd_bddIthVar(pNtk->pManFunc,1),Cudd_bddIthVar(pNtk->pManFunc,2)), Cudd_Ref( pNode->pData );
     else
         assert( 0 );
@@ -1260,13 +1262,13 @@ bool Abc_NodeIsConst0( Abc_Obj_t * pNode )
     Abc_Ntk_t * pNtk = pNode->pNtk;
     assert(Abc_ObjIsNode(pNode));      
     assert(Abc_NodeIsConst(pNode));
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsConst0(pNode->pData);
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         return Cudd_IsComplement(pNode->pData);
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return Abc_ObjNot(pNode) == Abc_AigConst1(pNode->pNtk->pManFunc);
-    if ( Abc_NtkIsMapped(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
         return pNode->pData == Mio_LibraryReadConst0(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
     assert( 0 );
     return 0;
@@ -1288,13 +1290,13 @@ bool Abc_NodeIsConst1( Abc_Obj_t * pNode )
     Abc_Ntk_t * pNtk = pNode->pNtk;
     assert(Abc_ObjIsNode(pNode));      
     assert(Abc_NodeIsConst(pNode));
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsConst1(pNode->pData);
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         return !Cudd_IsComplement(pNode->pData);
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return pNode == Abc_AigConst1(pNode->pNtk->pManFunc);
-    if ( Abc_NtkIsMapped(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
         return pNode->pData == Mio_LibraryReadConst1(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
     assert( 0 );
     return 0;
@@ -1317,13 +1319,13 @@ bool Abc_NodeIsBuf( Abc_Obj_t * pNode )
     assert(Abc_ObjIsNode(pNode)); 
     if ( Abc_ObjFaninNum(pNode) != 1 )
         return 0;
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsBuf(pNode->pData);
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         return !Cudd_IsComplement(pNode->pData);
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return 0;
-    if ( Abc_NtkIsMapped(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
         return pNode->pData == Mio_LibraryReadBuf(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
     assert( 0 );
     return 0;
@@ -1346,13 +1348,13 @@ bool Abc_NodeIsInv( Abc_Obj_t * pNode )
     assert(Abc_ObjIsNode(pNode)); 
     if ( Abc_ObjFaninNum(pNode) != 1 )
         return 0;
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsInv(pNode->pData);
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         return Cudd_IsComplement(pNode->pData);
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return 0;
-    if ( Abc_NtkIsMapped(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
         return pNode->pData == Mio_LibraryReadInv(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
     assert( 0 );
     return 0;
diff --git a/src/base/abc/abcCut.c b/src/base/abc/abcCut.c
index b7d83af0..f487bd1b 100644
--- a/src/base/abc/abcCut.c
+++ b/src/base/abc/abcCut.c
@@ -49,7 +49,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     int i;
     int clk = clock();
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // start the manager
     pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index e5f1bde9..2fbbee37 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -223,7 +223,7 @@ Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos )
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
     int i;
-    assert( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // set the traversal ID
     Abc_NtkIncrementTravId( pNtk );
     // start the array of nodes
diff --git a/src/base/abc/abcDsd.c b/src/base/abc/abcDsd.c
index e92907e3..d1445e75 100644
--- a/src/base/abc/abcDsd.c
+++ b/src/base/abc/abcDsd.c
@@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
     Abc_Ntk_t * pNtkNew;
     DdManager * dd;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // perform FPGA mapping
     dd = Abc_NtkGlobalBdds( pNtk, 0 );    
@@ -112,7 +112,7 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose,
         return NULL;
 
     // start the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
     // make sure the new manager has enough inputs
     Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
     // put the results into the new network (save new CO drivers in old CO drivers)
@@ -324,7 +324,7 @@ int Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose )
     Vec_Ptr_t * vNodes;
     int i;
 
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
 
     // make the network minimum base
     Abc_NtkMinimumBase( pNtk );
diff --git a/src/base/abc/abcFpga.c b/src/base/abc/abcFpga.c
index b83c376a..2316e934 100644
--- a/src/base/abc/abcFpga.c
+++ b/src/base/abc/abcFpga.c
@@ -50,7 +50,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
     Abc_Ntk_t * pNtkNew;
     Fpga_Man_t * pMan;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // print a warning about choice nodes
     if ( Abc_NtkCountChoiceNodes( pNtk ) )
@@ -105,7 +105,7 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
     Abc_Obj_t * pNode, * pFanin, * pPrev;
     int i;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // start the mapping manager and set its parameters
     pMan = Fpga_ManCreate( Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), fVerbose );
@@ -174,7 +174,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode, * pNodeNew;
     int i, nDupGates;
     // create the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
     // make the mapper point to the new network
     Fpga_CutsCleanSign( pMan );
     Fpga_ManCleanData0( pMan );
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index 724c3877..bb7d8cfa 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -92,7 +92,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     Abc_Obj_t * pNode, * pConst1, * pReset;
     int i;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // create the FRAIG manager
     pMan = Fraig_ManCreate( pParams );
@@ -148,7 +148,7 @@ Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode;//, * pNodeNew;
     int i;
     // create the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
     // make the mapper point to the new network
     Abc_NtkForEachCi( pNtk, pNode, i )
         Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy );
@@ -249,7 +249,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
 
-    if ( !Abc_NtkIsLogicSop(pNtk) )
+    if ( !Abc_NtkIsSopLogic(pNtk) )
     {
         printf( "Abc_NtkFraigTrust: Trust mode works for netlists and logic SOP networks.\n" );
         return NULL;
@@ -262,7 +262,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
     }
     
     // perform strashing
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
     Abc_NtkFraigTrustOne( pNtk, pNtkNew );
     Abc_NtkFinalize( pNtk, pNtkNew );
 
@@ -421,9 +421,9 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pStore;
     int nAndsOld;
 
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
     {
-        printf( "Convert netlist into a logic network before adding to storage.\n" );
+        printf( "The netlist need to be converted into a logic network before adding it to storage.\n" );
         return 0;
     }
 
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 8ecbd343..f616a258 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -48,7 +48,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
     DdManager * dd;
     int nFaninsMax, i;
 
-    assert( Abc_NtkIsLogicSop(pNtk) ); 
+    assert( Abc_NtkIsSopLogic(pNtk) ); 
 
     // start the functionality manager
     nFaninsMax = Abc_NtkGetFaninMax( pNtk );
@@ -74,7 +74,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
     pNtk->pManFunc = dd;
 
     // update the network type
-    pNtk->Type = ABC_NTK_LOGIC_BDD;
+    pNtk->ntkFunc = ABC_FUNC_BDD;
     return 1;
 }
 
@@ -152,12 +152,12 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
     int RetValue, i;
     Vec_Str_t * vCube;
 
-    assert( Abc_NtkIsLogicBdd(pNtk) ); 
+    assert( Abc_NtkIsBddLogic(pNtk) ); 
     Cudd_zddVarsFromBddVars( dd, 2 );
     // allocate the new manager
     pNtk->pManFunc = Extra_MmFlexStart();
     // update the network type
-    pNtk->Type = ABC_NTK_LOGIC_SOP;
+    pNtk->ntkFunc = ABC_FUNC_SOP;
 
     // go through the objects
     vCube = Vec_StrAlloc( 100 );
@@ -165,7 +165,6 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
     {
         assert( pNode->pData );
         bFunc = pNode->pData;
-//Extra_bddPrint( dd, bFunc ); printf( "\n" ); printf( "\n" );
         pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 );
         if ( pNode->pData == NULL )
             return 0;
@@ -375,7 +374,7 @@ int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFani
 ***********************************************************************/
 void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 )
 {
-    assert( Abc_NtkIsLogicBdd(pNode->pNtk) ); 
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
     *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 0 );
     *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 1 );
 }
diff --git a/src/base/abc/abcFxu.c b/src/base/abc/abcFxu.c
index 5721a50b..0c8994e1 100644
--- a/src/base/abc/abcFxu.c
+++ b/src/base/abc/abcFxu.c
@@ -54,9 +54,11 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 {
     int fCheck = 1;
 
-    assert( Abc_NtkIsLogicBdd(pNtk) || Abc_NtkIsLogicSop(pNtk) );
+    assert( Abc_NtkIsLogic(pNtk) );
     // convert nodes to SOPs
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkIsMappedLogic(pNtk) )
+        Abc_NtkUnmap(pNtk);
+    else if ( Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(pNtk);
     else
     { // to make sure the SOPs are SCC-free
diff --git a/src/base/abc/abcMap.c b/src/base/abc/abcMap.c
index 15e5c6af..f847aa40 100644
--- a/src/base/abc/abcMap.c
+++ b/src/base/abc/abcMap.c
@@ -61,7 +61,7 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
     Map_Man_t * pMan;
     int clk;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // check that the library is available
     if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == NULL )
@@ -130,7 +130,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i
     Abc_Obj_t * pNode, * pFanin, * pPrev;
     int i;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // start the mapping manager and set its parameters
     pMan = Map_ManCreate( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk), Abc_NtkPoNum(pNtk) + Abc_NtkLatchNum(pNtk), fVerbose );
@@ -202,7 +202,7 @@ Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
     int i, nDupGates;
 
     // create the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_MAP );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_MAP );
     // make the mapper point to the new network
     Map_ManCleanData( pMan );
     Abc_NtkForEachCi( pNtk, pNode, i )
@@ -388,11 +388,11 @@ int Abc_NtkUnmap( Abc_Ntk_t * pNtk )
     char * pSop;
     int i;
 
-    assert( Abc_NtkIsLogicMap(pNtk) );
+    assert( Abc_NtkIsMappedLogic(pNtk) );
     // update the functionality manager
     assert( pNtk->pManFunc == Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
     pNtk->pManFunc = Extra_MmFlexStart();
-    pNtk->Type     = ABC_NTK_LOGIC_SOP;
+    pNtk->ntkFunc  = ABC_FUNC_SOP;
     // update the nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -424,7 +424,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
 
     Map_Man_t * pMan;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // check that the library is available
     if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == NULL )
diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index d2d88ebf..2a018e35 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -45,7 +45,7 @@ int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, Counter;
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
     Counter = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
         Counter += Abc_NodeMinimumBase( pNode );
@@ -70,7 +70,7 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
     DdNode * bTemp;
     int i, nVars;
 
-    assert( Abc_NtkIsLogicBdd(pNode->pNtk) );
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) );
     assert( Abc_ObjIsNode(pNode) );
 
     // compute support
diff --git a/src/base/abc/abcMiter.c b/src/base/abc/abcMiter.c
index 7e6d4905..b8bcec4d 100644
--- a/src/base/abc/abcMiter.c
+++ b/src/base/abc/abcMiter.c
@@ -55,8 +55,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) )
         return NULL;
     // make sure the circuits are strashed 
-    fRemove1 = (!Abc_NtkIsAig(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0));
-    fRemove2 = (!Abc_NtkIsAig(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0));
+    fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0));
+    fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0));
     if ( pNtk1 && pNtk2 )
         pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb );
     if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
@@ -81,11 +81,11 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     char Buffer[100];
     Abc_Ntk_t * pNtkMiter;
 
-    assert( Abc_NtkIsAig(pNtk1) );
-    assert( Abc_NtkIsAig(pNtk2) );
+    assert( Abc_NtkIsStrash(pNtk1) );
+    assert( Abc_NtkIsStrash(pNtk2) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
     sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
     pNtkMiter->pName = util_strsav(Buffer);
 
@@ -317,13 +317,13 @@ Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
     Abc_Ntk_t * pNtkMiter;
     Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     assert( Out < Abc_NtkCoNum(pNtk) );
     assert( In1 < Abc_NtkCiNum(pNtk) );
     assert( In2 < Abc_NtkCiNum(pNtk) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
     sprintf( Buffer, "%s_%s_miter", pNtk->pName, Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
     pNtkMiter->pName = util_strsav(Buffer);
 
@@ -387,7 +387,7 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
 {
     Abc_Obj_t * pNodePo, * pChild;
     int i;
-    assert( Abc_NtkIsAig(pMiter) );
+    assert( Abc_NtkIsStrash(pMiter) );
     Abc_NtkForEachPo( pMiter, pNodePo, i )
     {
         pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,i) );
@@ -478,9 +478,9 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
     Abc_Obj_t * pLatch, * pLatchNew;
     int i, Counter;
     assert( nFrames > 0 );
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // start the new network
-    pNtkFrames = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkFrames = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
     sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
     pNtkFrames->pName = util_strsav(Buffer);
     // create new latches (or their initial values) and remember them in the new latches
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 8e10b391..f7eb0804 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -47,10 +47,10 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
     int i, k;
     assert( Abc_NtkIsNetlist(pNtk) );
     // start the network
-    if ( Abc_NtkIsNetlistSop(pNtk) )
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
+    if ( !Abc_NtkHasMapping(pNtk) )
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
     else
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_MAP );
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_MAP );
     // duplicate the nodes 
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
@@ -84,8 +84,8 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew, * pNtkTemp; 
-    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) );
-    if ( Abc_NtkIsAig(pNtk) )
+    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) );
+    if ( Abc_NtkIsStrash(pNtk) )
     {
         pNtkTemp = Abc_NtkAigToLogicSop(pNtk);
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
@@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
         Abc_NtkDelete( pNtkTemp );
     }
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkIsBddLogic(pNtk) )
     {
         Abc_NtkBddToSop(pNtk);
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
@@ -122,7 +122,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew, * pNtkTemp; 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     pNtkTemp = Abc_NtkAigToLogicSopBench( pNtk );
     pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
     Abc_NtkDelete( pNtkTemp );
@@ -152,14 +152,17 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
     char * pNameCo;
     int i, k;
 
-    assert( Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsLogicMap(pNtk) );
+    assert( Abc_NtkIsLogic(pNtk) );
     assert( Abc_NtkLogicHasSimpleCos(pNtk) );
 
+    if ( Abc_NtkIsBddLogic(pNtk) )
+        Abc_NtkBddToSop(pNtk);
+
     // start the netlist by creating PI/PO/Latch objects
-    if ( Abc_NtkIsLogicSop(pNtk) )
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST_SOP );
+    if ( Abc_NtkIsSopLogic(pNtk) )
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_NETLIST, ABC_FUNC_SOP );
     else
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST_MAP );
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_NETLIST, ABC_FUNC_BDD );
     // create the CI nets and remember them in the new CI nodes
     Abc_NtkForEachCi( pNtk, pObj, i )
     {
@@ -233,9 +236,9 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pFanin, * pNodeNew;
     int i, k;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
     // create the constant node
     Abc_NtkDupConst1( pNtk, pNtkNew );
     // duplicate the nodes and create node functions
@@ -281,7 +284,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
     {
-        if ( Abc_NtkIsAig(pNtk->pExdc) )
+        if ( Abc_NtkIsStrash(pNtk->pExdc) )
             pNtkNew->pExdc = Abc_NtkAigToLogicSop( pNtk->pExdc );
         else
             pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
@@ -309,11 +312,11 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pFanin;
     Vec_Ptr_t * vNodes;
     int i, k;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     if ( Abc_NtkCountChoiceNodes(pNtk) )
         printf( "Warning: Choice nodes are skipped.\n" );
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
     // create the constant node
     Abc_NtkDupConst1( pNtk, pNtkNew );
     // collect the nodes to be used (marks all nodes with current TravId)
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index dc7a2e7b..337dd43b 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -57,7 +57,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         fprintf( pFile, "  net = %5d", Abc_NtkNetNum(pNtk) );
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
     }
-    else if ( Abc_NtkIsAig(pNtk) )
+    else if ( Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
         if ( Num = Abc_NtkCountChoiceNodes(pNtk) )
@@ -70,26 +70,26 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
 
-    if ( Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsNetlistSop(pNtk) )   
+    if ( Abc_NtkHasSop(pNtk) )   
     {
         fprintf( pFile, "  cube = %5d",  Abc_NtkGetCubeNum(pNtk) );
 //        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
         if ( fFactored )
             fprintf( pFile, "  lit(fac) = %5d",  Abc_NtkGetLitFactNum(pNtk) );
     }
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         fprintf( pFile, "  bdd = %5d",  Abc_NtkGetBddNodeNum(pNtk) );
-    else if ( Abc_NtkIsLogicMap(pNtk) || Abc_NtkIsNetlistMap(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
     {
         fprintf( pFile, "  area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
         fprintf( pFile, "  delay = %5.2f", Abc_NtkDelayTrace(pNtk) );
     }
-    else if ( !Abc_NtkIsAig(pNtk) && !Abc_NtkIsSeq(pNtk) )
+    else if ( !Abc_NtkHasAig(pNtk) )
     {
         assert( 0 );
     }
 
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         fprintf( pFile, "  lev = %3d", Abc_AigGetLevelNum(pNtk) );
     else if ( !Abc_NtkIsSeq(pNtk) )
         fprintf( pFile, "  lev = %3d", Abc_NtkGetLevelNum(pNtk) );
@@ -180,7 +180,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
             continue;
         }
         // count the number of cases when the constant is equal to the initial value
-        if ( Abc_NtkIsAig(pNtk) )
+        if ( Abc_NtkIsStrash(pNtk) )
         {
             if ( Abc_LatchIsInit1(pLatch) == !Abc_ObjFaninC0(pLatch) )
                 Counter2++;
@@ -314,7 +314,7 @@ void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i;
-    assert( Abc_NtkIsLogicSop(pNtk) );
+    assert( Abc_NtkIsSopLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
         Abc_NodePrintFactor( pFile, pNode );
 }
@@ -369,7 +369,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
     int i, Length;
 
     // print the delay profile
-    if ( fProfile && Abc_NtkIsMapped(pNtk) )
+    if ( fProfile && Abc_NtkHasMapping(pNtk) )
     {
         int nIntervals = 12;
         float DelayMax, DelayCur, DelayDelta;
@@ -407,7 +407,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
         int LevelMax, * pLevelCounts;
         int nOutsSum, nOutsTotal;
 
-        if ( !Abc_NtkIsAig(pNtk) )
+        if ( !Abc_NtkIsStrash(pNtk) )
             Abc_NtkGetLevelNum(pNtk);
 
         LevelMax = 0;
@@ -430,7 +430,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
         free( pLevelCounts );
         return;
     }
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // find the longest name
     Length = 0;
diff --git a/src/base/abc/abcReconv.c b/src/base/abc/abcReconv.c
index 89a4d871..e02ccba0 100644
--- a/src/base/abc/abcReconv.c
+++ b/src/base/abc/abcReconv.c
@@ -472,7 +472,7 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
     Vec_Ptr_t * vVec;
     Abc_Obj_t * pNode, * pFanout;
     int i, k, v, LevelMin;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // assuming that the structure is clean
     Vec_VecForEachLevel( vLevels, vVec, i )
diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c
index 95454668..7e387b47 100644
--- a/src/base/abc/abcRefactor.c
+++ b/src/base/abc/abcRefactor.c
@@ -94,7 +94,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
     int i, nNodes;
     int clk, clkStart = clock();
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // start the managers
     pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax );
     pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index 1a8f7966..081ccfaa 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -167,16 +167,17 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t
 ***********************************************************************/
 void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain )
 {
+    Abc_Ntk_t * pNtk = pNode->pNtk;
     Abc_Obj_t * pNodeNew;
     int nNodesNew, nNodesOld;
-    nNodesOld = Abc_NtkNodeNum(pNode->pNtk);
+    nNodesOld = Abc_NtkNodeNum(pNtk);
     // create the new structure of nodes
     assert( vForm->nSize == 1 || Vec_PtrSize(vFanins) < Vec_IntSize(vForm) );
-    pNodeNew = Abc_NodeStrashDec( pNode->pNtk->pManFunc, vFanins, vForm );
+    pNodeNew = Abc_NodeStrashDec( pNtk->pManFunc, vFanins, vForm );
     // remove the old nodes
-    Abc_AigReplace( pNode->pNtk->pManFunc, pNode, pNodeNew );
+    Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew );
     // compare the gains
-    nNodesNew = Abc_NtkNodeNum(pNode->pNtk);
+    nNodesNew = Abc_NtkNodeNum(pNtk);
     assert( nGain <= nNodesOld - nNodesNew );
 }
 
diff --git a/src/base/abc/abcRenode.c b/src/base/abc/abcRenode.c
index 8037f642..c45f9763 100644
--- a/src/base/abc/abcRenode.c
+++ b/src/base/abc/abcRenode.c
@@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     assert( nThresh >= 0 );
     assert( nFaninMax > 1 );
 
@@ -74,7 +74,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
         Abc_NtkRenodeSetBounds( pNtk, nThresh, nFaninMax );
 
     // perform renoding for this boundary
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
     Abc_NtkRenodeInt( pNtk, pNtkNew );
     Abc_NtkFinalize( pNtk, pNtkNew );
 
diff --git a/src/base/abc/abcRewrite.c b/src/base/abc/abcRewrite.c
index 0b573bac..62e506bb 100644
--- a/src/base/abc/abcRewrite.c
+++ b/src/base/abc/abcRewrite.c
@@ -55,7 +55,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose )
     int i, nNodes, nGain;
     int clk, clkStart = clock();
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // start the rewriting manager
     pManRwr = Rwr_ManStart( 0 );
     if ( pManRwr == NULL )
diff --git a/src/base/abc/abcSat.c b/src/base/abc/abcSat.c
index fccb7fbc..4fb059e5 100644
--- a/src/base/abc/abcSat.c
+++ b/src/base/abc/abcSat.c
@@ -48,7 +48,7 @@ bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose )
     lbool   status;
     int clk;
 
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
     if ( Abc_NtkPoNum(pNtk) > 1 )
@@ -110,7 +110,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
     char * pSop0, * pSop1;
     int i;
 
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
 
     // start the data structures
     pSat    = solver_new();
diff --git a/src/base/abc/abcSeq.c b/src/base/abc/abcSeq.c
index 2fcbf670..d6b1b8e5 100644
--- a/src/base/abc/abcSeq.c
+++ b/src/base/abc/abcSeq.c
@@ -67,9 +67,9 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pConst, * pFanout, * pFaninNew, * pLatch;
     int i, k, fChange, Counter;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_SEQ );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_SEQ, ABC_FUNC_AIG );
     pManNew = pNtkNew->pManFunc;
 
     // set mapping of the constant nodes
@@ -200,7 +200,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
     int i, k, c;
     assert( Abc_NtkIsSeq(pNtk) );
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
     // create the constant and reset nodes
     Abc_NtkDupConst1( pNtk, pNtkNew );
     Abc_NtkDupReset( pNtk, pNtkNew );
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index 5a6e1828..730aca90 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -60,7 +60,7 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
     char * pProgGsViewName;
     int RetValue;
 
-    assert( Abc_NtkIsLogicBdd(pNode->pNtk) );
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) );
 
 #ifdef WIN32
     pProgDotName = "dot.exe";
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index bf97c5bf..19394fb3 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -56,16 +56,13 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
     int nNodes;
 
     assert( !Abc_NtkIsNetlist(pNtk) );
-    if ( Abc_NtkIsLogicBdd(pNtk) )
-    {
-//        printf( "Converting node functions from BDD to SOP.\n" );
+    if ( Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(pNtk);
-    }
     // print warning about choice nodes
     if ( Abc_NtkCountChoiceNodes( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
     // perform strashing
-    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG );
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
     Abc_NtkStrashPerform( pNtk, pNtkAig, fAllNodes );
     Abc_NtkFinalize( pNtk, pNtkAig );
     // print warning about self-feed latches
@@ -106,13 +103,10 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     Abc_Obj_t * pObj;
     int i;
     // the first network should be an AIG
-    assert( Abc_NtkIsAig(pNtk1) );
-    assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsAig(pNtk2) ); 
-    if ( Abc_NtkIsLogicBdd(pNtk2) )
-    {
-//        printf( "Converting node functions from BDD to SOP.\n" );
+    assert( Abc_NtkIsStrash(pNtk1) );
+    assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); 
+    if ( Abc_NtkIsBddLogic(pNtk2) )
         Abc_NtkBddToSop(pNtk2);
-    }
     // check that the networks have the same PIs
     // reorder PIs of pNtk2 according to pNtk1
     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1 ) )
@@ -192,7 +186,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
     assert( Abc_ObjIsNode(pNode) );
 
     // consider the case when the graph is an AIG
-    if ( Abc_NtkIsAig(pNode->pNtk) )
+    if ( Abc_NtkIsStrash(pNode->pNtk) )
     {
 //        Abc_Obj_t * pChild0, * pChild1;
 //        pChild0 = Abc_ObjFanin0(pNode);
@@ -203,7 +197,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
     }
 
     // get the SOP of the node
-    if ( Abc_NtkIsLogicMap(pNode->pNtk) )
+    if ( Abc_NtkHasMapping(pNode->pNtk) )
         pSop = Mio_GateReadSop(pNode->pData);
     else
         pSop = pNode->pData;
diff --git a/src/base/abc/abcSweep.c b/src/base/abc/abcSweep.c
index 92d354ac..47565241 100644
--- a/src/base/abc/abcSweep.c
+++ b/src/base/abc/abcSweep.c
@@ -58,7 +58,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
     Fraig_Man_t * pMan;
     stmm_table * tEquiv;
 
-    assert( !Abc_NtkIsAig(pNtk) );
+    assert( !Abc_NtkIsStrash(pNtk) );
 
     // derive the AIG
     pNtkAig = Abc_NtkStrash( pNtk, 0 );
@@ -194,7 +194,7 @@ void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv,
     // assign levels to the nodes of the network
     Abc_NtkGetLevelNum( pNtk );
     // merge nodes in the classes
-    if ( Abc_NtkIsLogicMap( pNtk ) )
+    if ( Abc_NtkHasMapping( pNtk ) )
     {
         Abc_NtkDelayTrace( pNtk );
         stmm_foreach_item( tEquiv, gen, (char **)&pList, NULL )
@@ -403,7 +403,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
     }
     Vec_PtrFree( vNodes );
     // if it is an AIG, also mark the constant 1 node
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         Abc_AigConst1(pNtk->pManFunc)->fMarkA = 1;
     // remove the non-marked nodes
     Counter = 0;
diff --git a/src/base/abc/abcTiming.c b/src/base/abc/abcTiming.c
index 9d71ace5..032d074c 100644
--- a/src/base/abc/abcTiming.c
+++ b/src/base/abc/abcTiming.c
@@ -553,7 +553,7 @@ float Abc_NtkDelayTrace( Abc_Ntk_t * pNtk )
     float tArrivalMax;
     int i;
 
-    assert( Abc_NtkIsLogicMap(pNtk) );
+    assert( Abc_NtkIsMappedLogic(pNtk) );
 
     Abc_NtkTimePrepare( pNtk );
     vNodes = Abc_NtkDfs( pNtk, 1 );
@@ -647,7 +647,7 @@ void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk )
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pObj, * pFanout;
     int i, k, nLevelsCur;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // remember the maximum number of direct levels
     pNtk->LevelMax = Abc_AigGetLevelNum(pNtk);
     // start the reverse levels
@@ -701,7 +701,7 @@ void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk )
 void Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR )
 {
     Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     assert( pNtk->vLevelsR );
     Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
     Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, LevelR );
@@ -722,7 +722,7 @@ void Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR )
 int Abc_NodeReadReverseLevel( Abc_Obj_t * pObj )
 {
     Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     assert( pNtk->vLevelsR );
     Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
     return Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
@@ -743,7 +743,7 @@ int Abc_NodeReadReverseLevel( Abc_Obj_t * pObj )
 int Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj )
 {
     Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     assert( pNtk->vLevelsR );
     return pNtk->LevelMax + 1 - Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
 }
diff --git a/src/base/abc/abcUnreach.c b/src/base/abc/abcUnreach.c
index b5a3a644..04e5c96c 100644
--- a/src/base/abc/abcUnreach.c
+++ b/src/base/abc/abcUnreach.c
@@ -282,7 +282,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     int i;
 
     // start the new network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC_BDD );
+    pNtkNew = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_BDD );
     // create PIs corresponding to LOs
     Abc_NtkForEachLatch( pNtk, pNode, i )
         pNode->pCopy = Abc_NtkCreatePi(pNtkNew);
@@ -308,13 +308,20 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     Abc_NtkForEachCo( pNtk, pNode, i )
         Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
 
-    // copy the CI/CO names
+    // store the PI names of the EXDC network
     Abc_NtkForEachLatch( pNtk, pNode, i )
         Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pNode) );
+    // store the PO names of the EXDC network
     Abc_NtkForEachPo( pNtk, pNode, i )
         Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pNode) );
     Abc_NtkForEachLatch( pNtk, pNode, i )
-        Abc_NtkLogicStoreName( Abc_NtkCo(pNtkNew,Abc_NtkPoNum(pNtk) + i), Abc_ObjName(pNode) );
+        Abc_NtkLogicStoreName( Abc_NtkCo(pNtkNew,Abc_NtkPoNum(pNtk) + i), Abc_ObjNameSuffix(pNode, "_in") );
+
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkNew );
+
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
 
     // transform the network to the SOP representation
     Abc_NtkBddToSop( pNtkNew );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 87d57947..7d2ca107 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -72,7 +72,7 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, nCubes = 0;
-    assert( Abc_NtkIsSop(pNtk) );
+    assert( Abc_NtkHasSop(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
@@ -96,7 +96,7 @@ int Abc_NtkGetLitNum( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, nLits = 0;
-    assert( Abc_NtkIsSop(pNtk) );
+    assert( Abc_NtkHasSop(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
@@ -121,16 +121,14 @@ int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk )
     Vec_Int_t * vFactor;
     Abc_Obj_t * pNode;
     int nNodes, i;
-    assert( Abc_NtkIsSop(pNtk) );
+    assert( Abc_NtkHasSop(pNtk) );
     nNodes = 0;
-//    Ft_FactorStartMan();
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         vFactor = Ft_Factor( pNode->pData );
         nNodes += Ft_FactorGetNumNodes(vFactor);
         Vec_IntFree( vFactor );
     }
-//    Ft_FactorStopMan();
     return nNodes;
 }
 
@@ -149,7 +147,7 @@ int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, nNodes = 0;
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
@@ -175,7 +173,7 @@ int Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk )
     DdNode * bCover, * zCover, * bFunc;
     DdManager * dd = pNtk->pManFunc;
     int i, nClauses = 0;
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
@@ -214,7 +212,7 @@ double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode;
     double TotalArea;
     int i;
-    assert( Abc_NtkIsLogicMap(pNtk) );
+    assert( Abc_NtkHasMapping(pNtk) );
     TotalArea = 0.0;
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -367,9 +365,12 @@ int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate )
         pDriver = Abc_ObjFanin0(pNode);
         if ( Abc_ObjIsCi(pDriver) )
         {
-            // skip the case when the CI deriver has the same name as CO
-            if ( strcmp(Abc_ObjName(pDriver), Abc_ObjName(pNode)) == 0 )
+            // skip the case when the driver is a different node with the same name
+            if ( pDriver != pNode && strcmp(Abc_ObjName(pDriver), Abc_ObjName(pNode)) == 0 )
+            {
+                assert( !Abc_ObjFaninC0(pNode) );
                 continue;
+            }
         }
         else
         {
@@ -385,9 +386,9 @@ int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate )
             if ( Abc_ObjFaninC0(pNode) )
             {
                 // change polarity of the duplicated driver
-                if ( Abc_NtkIsLogicSop(pNtk) )
+                if ( Abc_NtkHasSop(pNtk) )
                     Abc_SopComplement( pDriverNew->pData );
-                else if ( Abc_NtkIsLogicBdd(pNtk) )
+                else if ( Abc_NtkHasBdd(pNtk) )
                     pDriverNew->pData = Cudd_Not( pDriverNew->pData );
                 else
                     assert( 0 );
@@ -643,7 +644,7 @@ int Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, Counter;
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
         return 0;
     Counter = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index bd390002..d9bed264 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/base/abc/abc.c \
     src/base/abc/abcAig.c \
     src/base/abc/abcAttach.c \
+    src/base/abc/abcBalance.c \
     src/base/abc/abcCheck.c \
     src/base/abc/abcCollapse.c \
     src/base/abc/abcCreate.c \
@@ -19,9 +20,10 @@ SRC +=    src/base/abc/abc.c \
     src/base/abc/abcNames.c \
     src/base/abc/abcNetlist.c \
     src/base/abc/abcPrint.c \
+    src/base/abc/abcReconv.c \
+    src/base/abc/abcRefactor.c \
     src/base/abc/abcRefs.c \
     src/base/abc/abcRenode.c \
-    src/base/abc/abcRefactor.c \
     src/base/abc/abcRewrite.c \
     src/base/abc/abcSat.c \
     src/base/abc/abcSeq.c \
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 255791a7..84c330bf 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1300,7 +1300,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     fclose( pFile );
 
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(pNtk);
 
     // write out the current network
@@ -1423,7 +1423,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     fclose( pFile );
 
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(pNtk);
 
     // write out the current network
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 1fe73690..9ffbc3cf 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -604,7 +604,7 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
     FileName = argv[util_optind];
 
     // check the network type
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) && !Abc_NtkIsSeq(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( pAbc->Out, "Currently can only write logic networks, AIGs, and seq AIGs.\n" );
         return 0;
@@ -670,7 +670,7 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the input file name
     FileName = argv[util_optind];
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pAbc->Out, "The network should be an AIG.\n" );
         return 0;
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index f598c4e5..b5dc2fa8 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -292,12 +292,12 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
         }
         pModelName = vTokens->pArray[1];
         // allocate the empty network
-        p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST_SOP );
+        p->pNtk = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP );
         p->pNtk->pName = util_strsav( pModelName );
         p->pNtk->pSpec = util_strsav( p->pFileName );
     }
     else
-        p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST_SOP );
+        p->pNtk = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP );
 
     // read the inputs/outputs
     pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );
@@ -581,8 +581,8 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     // if this is the first line with gate, update the network type
     if ( Abc_NtkNodeNum(p->pNtk) == 0 )
     {
-        assert( p->pNtk->Type = ABC_NTK_NETLIST_SOP );
-        p->pNtk->Type = ABC_NTK_NETLIST_MAP;
+        assert( p->pNtk->ntkFunc == ABC_FUNC_SOP );
+        p->pNtk->ntkFunc = ABC_FUNC_MAP;
         Extra_MmFlexStop( p->pNtk->pManFunc, 0 );
         p->pNtk->pManFunc = pGenlib;
     }
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index 936a1c0c..53299a0c 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -271,7 +271,7 @@ Abc_Ntk_t * Io_ReadVerNetwork( Io_ReadVer_t * p )
     pModelName = vTokens->pArray[1];
 
     // allocate the empty network
-    pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST_SOP );
+    pNtk = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP );
     pNtk->pName = util_strsav( pModelName );
     pNtk->pSpec = util_strsav( p->pFileName );
 
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index 7c4a4ab1..df79227d 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -46,7 +46,7 @@ int Io_WriteBench( Abc_Ntk_t * pNtk, char * pFileName )
 {
     Abc_Ntk_t * pExdc;
     FILE * pFile;
-    assert( Abc_NtkIsNetlistSop(pNtk) );
+    assert( Abc_NtkIsSopNetlist(pNtk) );
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
     {
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 5c83aad2..5135105f 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -320,7 +320,7 @@ void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch )
 ***********************************************************************/
 void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode )
 {
-    if ( Abc_NtkIsNetlistMap(pNode->pNtk) )
+    if ( Abc_NtkHasMapping(pNode->pNtk) )
     {
         // write the .gate line
         fprintf( pFile, ".gate" );
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 144ff167..bb216bb6 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -44,9 +44,9 @@ static void Io_WriteCnfInt( FILE * pFile, Abc_Ntk_t * pNtk );
 int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
 {
     solver * pSat;
-    if ( !Abc_NtkIsLogicBdd(pNtk) )
+    if ( !Abc_NtkIsBddLogic(pNtk) )
     {
-        fprintf( stdout, "Io_WriteCnf(): Currently can process logic networks with BDDs.\n" );
+        fprintf( stdout, "Io_WriteCnf(): Currently can only process logic networks with BDDs.\n" );
         return 0;
     }
     if ( Abc_NtkPoNum(pNtk) != 1 )
diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c
index 9c78b149..25a68978 100644
--- a/src/base/io/ioWritePla.c
+++ b/src/base/io/ioWritePla.c
@@ -46,7 +46,7 @@ int Io_WritePla( Abc_Ntk_t * pNtk, char * pFileName )
     Abc_Ntk_t * pExdc;
     FILE * pFile;
 
-    assert( Abc_NtkIsNetlistSop(pNtk) );
+    assert( Abc_NtkIsSopNetlist(pNtk) );
     assert( Abc_NtkGetLevelNum(pNtk) == 1 );
 
     pFile = fopen( pFileName, "w" );
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 899f8166..cb39c481 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -2,6 +2,7 @@ SRC +=  src/base/io/io.c \
     src/base/io/ioRead.c \
     src/base/io/ioReadBench.c \
     src/base/io/ioReadBlif.c \
+    src/base/io/ioReadEdif.c \
     src/base/io/ioReadPla.c \
     src/base/io/ioReadVerilog.c \
     src/base/io/ioUtil.c \
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 38574883..2e9d9d41 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -336,7 +336,7 @@ void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p )
 {
     Abc_Ntk_t * pNtk;
     for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk) )
-        if ( Abc_NtkIsLogicMap(pNtk) )
+        if ( Abc_NtkHasMapping(pNtk) )
             Abc_NtkUnmap( pNtk );
 }
 
diff --git a/src/bdd/dsd/module.make b/src/bdd/dsd/module.make
index f6418492..f5e6673d 100644
--- a/src/bdd/dsd/module.make
+++ b/src/bdd/dsd/module.make
@@ -1,6 +1,6 @@
-SRC +=    bdd\dsd\dsdApi.c \
-    bdd\dsd\dsdCheck.c \
-    bdd\dsd\dsdLocal.c \
-    bdd\dsd\dsdMan.c \
-    bdd\dsd\dsdProc.c \
-    bdd\dsd\dsdTree.c
+SRC +=    src/bdd/dsd/dsdApi.c \
+    src/bdd/dsd/dsdCheck.c \
+    src/bdd/dsd/dsdLocal.c \
+    src/bdd/dsd/dsdMan.c \
+    src/bdd/dsd/dsdProc.c \
+    src/bdd/dsd/dsdTree.c
diff --git a/src/bdd/reo/module.make b/src/bdd/reo/module.make
index 703be139..7eb41e0e 100644
--- a/src/bdd/reo/module.make
+++ b/src/bdd/reo/module.make
@@ -1,7 +1,7 @@
-SRC +=    bdd\reo\reoApi.c \
-    bdd\reo\reoCore.c \
-    bdd\reo\reoProfile.c \
-    bdd\reo\reoSift.c \
-    bdd\reo\reoSwap.c \
-    bdd\reo\reoTransfer.c \
-    bdd\reo\reoUnits.c
+SRC +=    src/bdd/reo/reoApi.c \
+    src/bdd/reo/reoCore.c \
+    src/bdd/reo/reoProfile.c \
+    src/bdd/reo/reoSift.c \
+    src/bdd/reo/reoSwap.c \
+    src/bdd/reo/reoTransfer.c \
+    src/bdd/reo/reoUnits.c
diff --git a/src/map/mapper/mapperCore.c b/src/map/mapper/mapperCore.c
index a43bcdc1..16cbfd5c 100644
--- a/src/map/mapper/mapperCore.c
+++ b/src/map/mapper/mapperCore.c
@@ -69,7 +69,7 @@ int Map_Mapping( Map_Man_t * p )
     Map_MappingTruths( p );
     p->timeTruth = clock() - clk;
     //////////////////////////////////////////////////////////////////////
-PRT( "Truths", clock() - clk );
+//PRT( "Truths", clock() - clk );
 
     //////////////////////////////////////////////////////////////////////
     // compute the minimum-delay mapping
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index d5b0330f..6d771990 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -804,7 +804,7 @@ void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounte
         *ppCounters = pCounters;
     else
         free( pCounters );
-    printf( "The number of 3N-classes = %d.\n", nClasses );
+//    printf( "The number of 3N-classes = %d.\n", nClasses );
 }
 
 /**Function*************************************************************
@@ -870,7 +870,7 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
         *ppCounters = pCounters;
     else
         free( pCounters );
-    printf( "The number of 4N-classes = %d.\n", nClasses );
+//    printf( "The number of 4N-classes = %d.\n", nClasses );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index f3a0f743..6719ed4d 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -70,7 +70,7 @@ static inline int        Cut_CutReadLeaveNum( Cut_Cut_t * p )  {  return p->nLea
 static inline int *      Cut_CutReadLeaves( Cut_Cut_t * p )    {  return p->pLeaves;   }
 static inline void *     Cut_CutReadData( Cut_Cut_t * p )      {  return p->pData;     }
 
-static inline void *     Cut_CutWriteData( Cut_Cut_t * p, void * pData )  { p->pData = pData;  }
+static inline void       Cut_CutWriteData( Cut_Cut_t * p, void * pData )  { p->pData = pData;  }
 static inline void       Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth )  { 
     if ( p->nVarsMax == 4 )  { p->uTruth = *puTruth;  return; }
     p->pLeaves[p->nVarsMax + p->fSeq] = (int)puTruth[0];
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 1c291b33..b9bab47f 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -137,7 +137,6 @@ extern void              Rwr_ManWriteToArray( Rwr_Man_t * p );
 extern void              Rwr_ManLoadFromArray( Rwr_Man_t * p, int fVerbose );
 extern void              Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName );
 extern void              Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName );
-extern Vec_Int_t *       Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk );
 extern void              Rwr_ListAddToTail( Rwr_Node_t ** ppList, Rwr_Node_t * pNode );
 extern char *            Rwr_ManGetPractical( Rwr_Man_t * p );
 
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
index dedd86fe..65b2bd6f 100644
--- a/src/opt/rwr/rwrUtil.c
+++ b/src/opt/rwr/rwrUtil.c
@@ -25,8 +25,13 @@
 ////////////////////////////////////////////////////////////////////////
 
 // precomputed data
+#ifdef _WIN32
 unsigned short s_RwrPracticalClasses[];
 unsigned short s_RwtAigSubgraphs[];
+#else
+static unsigned short s_RwrPracticalClasses[];
+static unsigned short s_RwtAigSubgraphs[];
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -221,30 +226,6 @@ void Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the array of fanout counters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk )
-{
-    Vec_Int_t * vFanNums;
-    Abc_Obj_t * pObj;
-    int i;
-    vFanNums = Vec_IntAlloc( 0 );
-    Vec_IntFill( vFanNums, Abc_NtkObjNumMax(pNtk), -1 );
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        if ( Abc_ObjIsNode( pObj ) )
-            Vec_IntWriteEntry( vFanNums, i, Abc_ObjFanoutNum(pObj) );
-    return vFanNums;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Adds the node to the end of the list.]
 
   Description []
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index eddd7270..242de8e2 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -69,7 +69,7 @@ CSAT_Manager CSAT_InitManager()
     CSAT_Manager_t * mng;
     mng = ALLOC( CSAT_Manager_t, 1 );
     memset( mng, 0, sizeof(CSAT_Manager_t) );
-    mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC_SOP );
+    mng->pNtk = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_SOP );
     mng->pNtk->pName = util_strsav("csat_network");
     mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
     mng->vNodes  = Vec_PtrAlloc( 100 );
diff --git a/src/sat/csat/module.make b/src/sat/csat/module.make
new file mode 100644
index 00000000..5b71a03c
--- /dev/null
+++ b/src/sat/csat/module.make
@@ -0,0 +1 @@
+SRC +=  src/sat/csat/csat_apis.c
diff --git a/src/sop/ft/ftFactor.c b/src/sop/ft/ftFactor.c
index d25d0653..19f70e36 100644
--- a/src/sop/ft/ftFactor.c
+++ b/src/sop/ft/ftFactor.c
@@ -319,10 +319,10 @@ Ft_Node_t * Ft_FactorTrivialTree_rec( Vec_Int_t * vForm, Ft_Node_t ** ppNodes, i
         return ppNodes[0];
 
     // split the nodes into two parts
-//    nNodes1 = nNodes/2;
-//    nNodes2 = nNodes - nNodes1;
-    nNodes2 = nNodes/2;
-    nNodes1 = nNodes - nNodes2;
+    nNodes1 = nNodes/2;
+    nNodes2 = nNodes - nNodes1;
+//    nNodes2 = nNodes/2;
+//    nNodes1 = nNodes - nNodes2;
 
     // recursively construct the tree for the parts
     pNode1 = Ft_FactorTrivialTree_rec( vForm, ppNodes,           nNodes1, fAnd );