From 91ca630b0fd316f0843dee8b9e6d236d849eb445 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 2 Oct 2005 08:01:00 -0700 Subject: Version abc51002 --- abc.dsp | 12 + abc.opt | Bin 55808 -> 51712 bytes abc.plg | 1250 ++++++++++++++++++++-------------------- src/base/abci/abc.c | 191 +++++- src/base/abci/abcCut.c | 70 ++- src/base/abcs/abcFpgaDelay.c | 327 +++++++++++ src/base/abcs/abcFpgaSeq.c | 201 +++++++ src/base/abcs/abcRetDelay.c | 6 - src/base/abcs/abcs.h | 26 + src/misc/extra/extra.h | 1 + src/misc/extra/extraUtilMisc.c | 724 +++++++++++++++++++++++ src/misc/vec/vecFan.h | 2 +- src/opt/cut/cut.h | 53 +- src/opt/cut/cutCut.c | 205 ++++++- src/opt/cut/cutInt.h | 35 +- src/opt/cut/cutList.h | 39 +- src/opt/cut/cutMan.c | 56 +- src/opt/cut/cutMerge.c | 5 +- src/opt/cut/cutNode.c | 125 ++-- src/opt/cut/cutOracle.c | 428 ++++++++++++++ src/opt/cut/cutSeq.c | 202 +++---- src/opt/cut/cutTruth.c | 347 +---------- src/opt/rwr/rwrEva.c | 13 +- 23 files changed, 3113 insertions(+), 1205 deletions(-) create mode 100644 src/base/abcs/abcFpgaDelay.c create mode 100644 src/base/abcs/abcFpgaSeq.c create mode 100644 src/opt/cut/cutOracle.c diff --git a/abc.dsp b/abc.dsp index 823b8b4a..f711f9fb 100644 --- a/abc.dsp +++ b/abc.dsp @@ -270,6 +270,14 @@ SOURCE=.\src\base\abci\abcVerify.c # PROP Default_Filter "" # Begin Source File +SOURCE=.\src\base\abcs\abcFpgaDelay.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\abcs\abcFpgaSeq.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abcs\abcRetCore.c # End Source File # Begin Source File @@ -1130,6 +1138,10 @@ SOURCE=.\src\opt\cut\cutNode.c # End Source File # Begin Source File +SOURCE=.\src\opt\cut\cutOracle.c +# End Source File +# Begin Source File + SOURCE=.\src\opt\cut\cutSeq.c # End Source File # Begin Source File diff --git a/abc.opt b/abc.opt index 26445d3e..a7bb1300 100644 Binary files a/abc.opt and b/abc.opt differ diff --git a/abc.plg b/abc.plg index c646a85d..be2500c6 100644 --- a/abc.plg +++ b/abc.plg @@ -3,638 +3,644 @@ 
 
Build Log

 

---------------------Configuration: abc - Win32 Debug--------------------
+--------------------Configuration: abc - Win32 Release--------------------
 

 
Command Lines

-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP91B.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC8D.tmp" with contents
 [
-/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c 
-"C:\_projects\abc\src\opt\cut\cutNode.c"
+/nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /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\opt\cut\cutCut.c"
 ]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP91B.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP91C.tmp" with contents
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC8D.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC8E.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:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept 
-.\Debug\abcAig.obj
-.\Debug\abcCheck.obj
-.\Debug\abcDfs.obj
-.\Debug\abcFanio.obj
-.\Debug\abcFunc.obj
-.\Debug\abcLatch.obj
-.\Debug\abcMinBase.obj
-.\Debug\abcNames.obj
-.\Debug\abcNetlist.obj
-.\Debug\abcNtk.obj
-.\Debug\abcObj.obj
-.\Debug\abcRefs.obj
-.\Debug\abcShow.obj
-.\Debug\abcSop.obj
-.\Debug\abcUtil.obj
-.\Debug\abc.obj
-.\Debug\abcAttach.obj
-.\Debug\abcBalance.obj
-.\Debug\abcCollapse.obj
-.\Debug\abcCut.obj
-.\Debug\abcDsd.obj
-.\Debug\abcFpga.obj
-.\Debug\abcFraig.obj
-.\Debug\abcFxu.obj
-.\Debug\abcMap.obj
-.\Debug\abcMiter.obj
-.\Debug\abcNtbdd.obj
-.\Debug\abcPga.obj
-.\Debug\abcPrint.obj
-.\Debug\abcReconv.obj
-.\Debug\abcRefactor.obj
-.\Debug\abcRenode.obj
-.\Debug\abcRewrite.obj
-.\Debug\abcSat.obj
-.\Debug\abcStrash.obj
-.\Debug\abcSweep.obj
-.\Debug\abcSymm.obj
-.\Debug\abcTiming.obj
-.\Debug\abcUnreach.obj
-.\Debug\abcVerify.obj
-.\Debug\abcRetCore.obj
-.\Debug\abcRetDelay.obj
-.\Debug\abcRetImpl.obj
-.\Debug\abcRetUtil.obj
-.\Debug\abcSeq.obj
-.\Debug\abcShare.obj
-.\Debug\abcUtils.obj
-.\Debug\cmd.obj
-.\Debug\cmdAlias.obj
-.\Debug\cmdApi.obj
-.\Debug\cmdFlag.obj
-.\Debug\cmdHist.obj
-.\Debug\cmdUtils.obj
-.\Debug\io.obj
-.\Debug\ioRead.obj
-.\Debug\ioReadBench.obj
-.\Debug\ioReadBlif.obj
-.\Debug\ioReadEdif.obj
-.\Debug\ioReadEqn.obj
-.\Debug\ioReadPla.obj
-.\Debug\ioReadVerilog.obj
-.\Debug\ioUtil.obj
-.\Debug\ioWriteBench.obj
-.\Debug\ioWriteBlif.obj
-.\Debug\ioWriteCnf.obj
-.\Debug\ioWriteDot.obj
-.\Debug\ioWriteEqn.obj
-.\Debug\ioWriteGml.obj
-.\Debug\ioWritePla.obj
-.\Debug\libSupport.obj
-.\Debug\main.obj
-.\Debug\mainFrame.obj
-.\Debug\mainInit.obj
-.\Debug\mainUtils.obj
-.\Debug\cuddAddAbs.obj
-.\Debug\cuddAddApply.obj
-.\Debug\cuddAddFind.obj
-.\Debug\cuddAddInv.obj
-.\Debug\cuddAddIte.obj
-.\Debug\cuddAddNeg.obj
-.\Debug\cuddAddWalsh.obj
-.\Debug\cuddAndAbs.obj
-.\Debug\cuddAnneal.obj
-.\Debug\cuddApa.obj
-.\Debug\cuddAPI.obj
-.\Debug\cuddApprox.obj
-.\Debug\cuddBddAbs.obj
-.\Debug\cuddBddCorr.obj
-.\Debug\cuddBddIte.obj
-.\Debug\cuddBridge.obj
-.\Debug\cuddCache.obj
-.\Debug\cuddCheck.obj
-.\Debug\cuddClip.obj
-.\Debug\cuddCof.obj
-.\Debug\cuddCompose.obj
-.\Debug\cuddDecomp.obj
-.\Debug\cuddEssent.obj
-.\Debug\cuddExact.obj
-.\Debug\cuddExport.obj
-.\Debug\cuddGenCof.obj
-.\Debug\cuddGenetic.obj
-.\Debug\cuddGroup.obj
-.\Debug\cuddHarwell.obj
-.\Debug\cuddInit.obj
-.\Debug\cuddInteract.obj
-.\Debug\cuddLCache.obj
-.\Debug\cuddLevelQ.obj
-.\Debug\cuddLinear.obj
-.\Debug\cuddLiteral.obj
-.\Debug\cuddMatMult.obj
-.\Debug\cuddPriority.obj
-.\Debug\cuddRead.obj
-.\Debug\cuddRef.obj
-.\Debug\cuddReorder.obj
-.\Debug\cuddSat.obj
-.\Debug\cuddSign.obj
-.\Debug\cuddSolve.obj
-.\Debug\cuddSplit.obj
-.\Debug\cuddSubsetHB.obj
-.\Debug\cuddSubsetSP.obj
-.\Debug\cuddSymmetry.obj
-.\Debug\cuddTable.obj
-.\Debug\cuddUtil.obj
-.\Debug\cuddWindow.obj
-.\Debug\cuddZddCount.obj
-.\Debug\cuddZddFuncs.obj
-.\Debug\cuddZddGroup.obj
-.\Debug\cuddZddIsop.obj
-.\Debug\cuddZddLin.obj
-.\Debug\cuddZddMisc.obj
-.\Debug\cuddZddPort.obj
-.\Debug\cuddZddReord.obj
-.\Debug\cuddZddSetop.obj
-.\Debug\cuddZddSymm.obj
-.\Debug\cuddZddUtil.obj
-.\Debug\epd.obj
-.\Debug\mtrBasic.obj
-.\Debug\mtrGroup.obj
-.\Debug\parseCore.obj
-.\Debug\parseStack.obj
-.\Debug\dsdApi.obj
-.\Debug\dsdCheck.obj
-.\Debug\dsdLocal.obj
-.\Debug\dsdMan.obj
-.\Debug\dsdProc.obj
-.\Debug\dsdTree.obj
-.\Debug\reoApi.obj
-.\Debug\reoCore.obj
-.\Debug\reoProfile.obj
-.\Debug\reoSift.obj
-.\Debug\reoSwap.obj
-.\Debug\reoTest.obj
-.\Debug\reoTransfer.obj
-.\Debug\reoUnits.obj
-.\Debug\added.obj
-.\Debug\solver.obj
-.\Debug\msatActivity.obj
-.\Debug\msatClause.obj
-.\Debug\msatClauseVec.obj
-.\Debug\msatMem.obj
-.\Debug\msatOrderJ.obj
-.\Debug\msatQueue.obj
-.\Debug\msatRead.obj
-.\Debug\msatSolverApi.obj
-.\Debug\msatSolverCore.obj
-.\Debug\msatSolverIo.obj
-.\Debug\msatSolverSearch.obj
-.\Debug\msatSort.obj
-.\Debug\msatVec.obj
-.\Debug\fraigApi.obj
-.\Debug\fraigCanon.obj
-.\Debug\fraigFanout.obj
-.\Debug\fraigFeed.obj
-.\Debug\fraigMan.obj
-.\Debug\fraigMem.obj
-.\Debug\fraigNode.obj
-.\Debug\fraigPrime.obj
-.\Debug\fraigSat.obj
-.\Debug\fraigTable.obj
-.\Debug\fraigUtil.obj
-.\Debug\fraigVec.obj
-.\Debug\csat_apis.obj
-.\Debug\fxu.obj
-.\Debug\fxuCreate.obj
-.\Debug\fxuHeapD.obj
-.\Debug\fxuHeapS.obj
-.\Debug\fxuList.obj
-.\Debug\fxuMatrix.obj
-.\Debug\fxuPair.obj
-.\Debug\fxuPrint.obj
-.\Debug\fxuReduce.obj
-.\Debug\fxuSelect.obj
-.\Debug\fxuSingle.obj
-.\Debug\fxuUpdate.obj
-.\Debug\rwrDec.obj
-.\Debug\rwrEva.obj
-.\Debug\rwrExp.obj
-.\Debug\rwrLib.obj
-.\Debug\rwrMan.obj
-.\Debug\rwrPrint.obj
-.\Debug\rwrUtil.obj
-.\Debug\cutApi.obj
-.\Debug\cutCut.obj
-.\Debug\cutMan.obj
-.\Debug\cutMerge.obj
-.\Debug\cutNode.obj
-.\Debug\cutSeq.obj
-.\Debug\cutTruth.obj
-.\Debug\decAbc.obj
-.\Debug\decFactor.obj
-.\Debug\decMan.obj
-.\Debug\decPrint.obj
-.\Debug\decUtil.obj
-.\Debug\simMan.obj
-.\Debug\simSat.obj
-.\Debug\simSupp.obj
-.\Debug\simSwitch.obj
-.\Debug\simSym.obj
-.\Debug\simSymSat.obj
-.\Debug\simSymSim.obj
-.\Debug\simSymStr.obj
-.\Debug\simUtils.obj
-.\Debug\fpga.obj
-.\Debug\fpgaCore.obj
-.\Debug\fpgaCreate.obj
-.\Debug\fpgaCut.obj
-.\Debug\fpgaCutUtils.obj
-.\Debug\fpgaFanout.obj
-.\Debug\fpgaLib.obj
-.\Debug\fpgaMatch.obj
-.\Debug\fpgaSwitch.obj
-.\Debug\fpgaTime.obj
-.\Debug\fpgaTruth.obj
-.\Debug\fpgaUtils.obj
-.\Debug\fpgaVec.obj
-.\Debug\mapper.obj
-.\Debug\mapperCanon.obj
-.\Debug\mapperCore.obj
-.\Debug\mapperCreate.obj
-.\Debug\mapperCut.obj
-.\Debug\mapperCutUtils.obj
-.\Debug\mapperFanout.obj
-.\Debug\mapperLib.obj
-.\Debug\mapperMatch.obj
-.\Debug\mapperRefs.obj
-.\Debug\mapperSuper.obj
-.\Debug\mapperSwitch.obj
-.\Debug\mapperTable.obj
-.\Debug\mapperTime.obj
-.\Debug\mapperTree.obj
-.\Debug\mapperTruth.obj
-.\Debug\mapperUtils.obj
-.\Debug\mapperVec.obj
-.\Debug\mio.obj
-.\Debug\mioApi.obj
-.\Debug\mioFunc.obj
-.\Debug\mioRead.obj
-.\Debug\mioUtils.obj
-.\Debug\super.obj
-.\Debug\superAnd.obj
-.\Debug\superGate.obj
-.\Debug\superWrite.obj
-.\Debug\pgaCore.obj
-.\Debug\pgaMan.obj
-.\Debug\pgaMatch.obj
-.\Debug\pgaUtil.obj
-.\Debug\extraBddMisc.obj
-.\Debug\extraBddSymm.obj
-.\Debug\extraUtilBitMatrix.obj
-.\Debug\extraUtilCanon.obj
-.\Debug\extraUtilFile.obj
-.\Debug\extraUtilMemory.obj
-.\Debug\extraUtilMisc.obj
-.\Debug\extraUtilProgress.obj
-.\Debug\extraUtilReader.obj
-.\Debug\st.obj
-.\Debug\stmm.obj
-.\Debug\cpu_stats.obj
-.\Debug\cpu_time.obj
-.\Debug\datalimit.obj
-.\Debug\getopt.obj
-.\Debug\pathsearch.obj
-.\Debug\safe_mem.obj
-.\Debug\strsav.obj
-.\Debug\texpand.obj
-.\Debug\mvc.obj
-.\Debug\mvcApi.obj
-.\Debug\mvcCompare.obj
-.\Debug\mvcContain.obj
-.\Debug\mvcCover.obj
-.\Debug\mvcCube.obj
-.\Debug\mvcDivide.obj
-.\Debug\mvcDivisor.obj
-.\Debug\mvcList.obj
-.\Debug\mvcLits.obj
-.\Debug\mvcMan.obj
-.\Debug\mvcOpAlg.obj
-.\Debug\mvcOpBool.obj
-.\Debug\mvcPrint.obj
-.\Debug\mvcSort.obj
-.\Debug\mvcUtils.obj
-.\Debug\npn.obj
-.\Debug\npnGenStr.obj
-.\Debug\npnTruth.obj
-.\Debug\npnUtil.obj
+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\abcAig.obj
+.\Release\abcCheck.obj
+.\Release\abcDfs.obj
+.\Release\abcFanio.obj
+.\Release\abcFunc.obj
+.\Release\abcLatch.obj
+.\Release\abcMinBase.obj
+.\Release\abcNames.obj
+.\Release\abcNetlist.obj
+.\Release\abcNtk.obj
+.\Release\abcObj.obj
+.\Release\abcRefs.obj
+.\Release\abcShow.obj
+.\Release\abcSop.obj
+.\Release\abcUtil.obj
+.\Release\abc.obj
+.\Release\abcAttach.obj
+.\Release\abcBalance.obj
+.\Release\abcCollapse.obj
+.\Release\abcCut.obj
+.\Release\abcDsd.obj
+.\Release\abcFpga.obj
+.\Release\abcFraig.obj
+.\Release\abcFxu.obj
+.\Release\abcMap.obj
+.\Release\abcMiter.obj
+.\Release\abcNtbdd.obj
+.\Release\abcPga.obj
+.\Release\abcPrint.obj
+.\Release\abcReconv.obj
+.\Release\abcRefactor.obj
+.\Release\abcRenode.obj
+.\Release\abcRewrite.obj
+.\Release\abcSat.obj
+.\Release\abcStrash.obj
+.\Release\abcSweep.obj
+.\Release\abcSymm.obj
+.\Release\abcTiming.obj
+.\Release\abcUnreach.obj
+.\Release\abcVerify.obj
+.\Release\abcRetCore.obj
+.\Release\abcRetDelay.obj
+.\Release\abcRetImpl.obj
+.\Release\abcRetUtil.obj
+.\Release\abcSeq.obj
+.\Release\abcShare.obj
+.\Release\abcUtils.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\ioReadEqn.obj
+.\Release\ioReadPla.obj
+.\Release\ioReadVerilog.obj
+.\Release\ioUtil.obj
+.\Release\ioWriteBench.obj
+.\Release\ioWriteBlif.obj
+.\Release\ioWriteCnf.obj
+.\Release\ioWriteDot.obj
+.\Release\ioWriteEqn.obj
+.\Release\ioWriteGml.obj
+.\Release\ioWritePla.obj
+.\Release\libSupport.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\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\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\cutApi.obj
+.\Release\cutCut.obj
+.\Release\cutMan.obj
+.\Release\cutMerge.obj
+.\Release\cutNode.obj
+.\Release\cutSeq.obj
+.\Release\cutTruth.obj
+.\Release\decAbc.obj
+.\Release\decFactor.obj
+.\Release\decMan.obj
+.\Release\decPrint.obj
+.\Release\decUtil.obj
+.\Release\simMan.obj
+.\Release\simSat.obj
+.\Release\simSupp.obj
+.\Release\simSwitch.obj
+.\Release\simSym.obj
+.\Release\simSymSat.obj
+.\Release\simSymSim.obj
+.\Release\simSymStr.obj
+.\Release\simUtils.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\fpgaSwitch.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\mapperSwitch.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\pgaCore.obj
+.\Release\pgaMan.obj
+.\Release\pgaMatch.obj
+.\Release\pgaUtil.obj
+.\Release\extraBddMisc.obj
+.\Release\extraBddSymm.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
+.\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\npn.obj
+.\Release\npnGenStr.obj
+.\Release\npnTruth.obj
+.\Release\npnUtil.obj
+.\Release\abcFpgaSeq.obj
+.\Release\abcFpgaDelay.obj
+.\Release\cutOracle.obj
 ]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP91C.tmp"
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC8E.tmp"
 
Output Window

 Compiling...
-cutNode.c
+cutCut.c
 Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP91D.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC90.tmp" with contents
 [
-/nologo /o"Debug/abc.bsc" 
-.\Debug\abcAig.sbr
-.\Debug\abcCheck.sbr
-.\Debug\abcDfs.sbr
-.\Debug\abcFanio.sbr
-.\Debug\abcFunc.sbr
-.\Debug\abcLatch.sbr
-.\Debug\abcMinBase.sbr
-.\Debug\abcNames.sbr
-.\Debug\abcNetlist.sbr
-.\Debug\abcNtk.sbr
-.\Debug\abcObj.sbr
-.\Debug\abcRefs.sbr
-.\Debug\abcShow.sbr
-.\Debug\abcSop.sbr
-.\Debug\abcUtil.sbr
-.\Debug\abc.sbr
-.\Debug\abcAttach.sbr
-.\Debug\abcBalance.sbr
-.\Debug\abcCollapse.sbr
-.\Debug\abcCut.sbr
-.\Debug\abcDsd.sbr
-.\Debug\abcFpga.sbr
-.\Debug\abcFraig.sbr
-.\Debug\abcFxu.sbr
-.\Debug\abcMap.sbr
-.\Debug\abcMiter.sbr
-.\Debug\abcNtbdd.sbr
-.\Debug\abcPga.sbr
-.\Debug\abcPrint.sbr
-.\Debug\abcReconv.sbr
-.\Debug\abcRefactor.sbr
-.\Debug\abcRenode.sbr
-.\Debug\abcRewrite.sbr
-.\Debug\abcSat.sbr
-.\Debug\abcStrash.sbr
-.\Debug\abcSweep.sbr
-.\Debug\abcSymm.sbr
-.\Debug\abcTiming.sbr
-.\Debug\abcUnreach.sbr
-.\Debug\abcVerify.sbr
-.\Debug\abcRetCore.sbr
-.\Debug\abcRetDelay.sbr
-.\Debug\abcRetImpl.sbr
-.\Debug\abcRetUtil.sbr
-.\Debug\abcSeq.sbr
-.\Debug\abcShare.sbr
-.\Debug\abcUtils.sbr
-.\Debug\cmd.sbr
-.\Debug\cmdAlias.sbr
-.\Debug\cmdApi.sbr
-.\Debug\cmdFlag.sbr
-.\Debug\cmdHist.sbr
-.\Debug\cmdUtils.sbr
-.\Debug\io.sbr
-.\Debug\ioRead.sbr
-.\Debug\ioReadBench.sbr
-.\Debug\ioReadBlif.sbr
-.\Debug\ioReadEdif.sbr
-.\Debug\ioReadEqn.sbr
-.\Debug\ioReadPla.sbr
-.\Debug\ioReadVerilog.sbr
-.\Debug\ioUtil.sbr
-.\Debug\ioWriteBench.sbr
-.\Debug\ioWriteBlif.sbr
-.\Debug\ioWriteCnf.sbr
-.\Debug\ioWriteDot.sbr
-.\Debug\ioWriteEqn.sbr
-.\Debug\ioWriteGml.sbr
-.\Debug\ioWritePla.sbr
-.\Debug\libSupport.sbr
-.\Debug\main.sbr
-.\Debug\mainFrame.sbr
-.\Debug\mainInit.sbr
-.\Debug\mainUtils.sbr
-.\Debug\cuddAddAbs.sbr
-.\Debug\cuddAddApply.sbr
-.\Debug\cuddAddFind.sbr
-.\Debug\cuddAddInv.sbr
-.\Debug\cuddAddIte.sbr
-.\Debug\cuddAddNeg.sbr
-.\Debug\cuddAddWalsh.sbr
-.\Debug\cuddAndAbs.sbr
-.\Debug\cuddAnneal.sbr
-.\Debug\cuddApa.sbr
-.\Debug\cuddAPI.sbr
-.\Debug\cuddApprox.sbr
-.\Debug\cuddBddAbs.sbr
-.\Debug\cuddBddCorr.sbr
-.\Debug\cuddBddIte.sbr
-.\Debug\cuddBridge.sbr
-.\Debug\cuddCache.sbr
-.\Debug\cuddCheck.sbr
-.\Debug\cuddClip.sbr
-.\Debug\cuddCof.sbr
-.\Debug\cuddCompose.sbr
-.\Debug\cuddDecomp.sbr
-.\Debug\cuddEssent.sbr
-.\Debug\cuddExact.sbr
-.\Debug\cuddExport.sbr
-.\Debug\cuddGenCof.sbr
-.\Debug\cuddGenetic.sbr
-.\Debug\cuddGroup.sbr
-.\Debug\cuddHarwell.sbr
-.\Debug\cuddInit.sbr
-.\Debug\cuddInteract.sbr
-.\Debug\cuddLCache.sbr
-.\Debug\cuddLevelQ.sbr
-.\Debug\cuddLinear.sbr
-.\Debug\cuddLiteral.sbr
-.\Debug\cuddMatMult.sbr
-.\Debug\cuddPriority.sbr
-.\Debug\cuddRead.sbr
-.\Debug\cuddRef.sbr
-.\Debug\cuddReorder.sbr
-.\Debug\cuddSat.sbr
-.\Debug\cuddSign.sbr
-.\Debug\cuddSolve.sbr
-.\Debug\cuddSplit.sbr
-.\Debug\cuddSubsetHB.sbr
-.\Debug\cuddSubsetSP.sbr
-.\Debug\cuddSymmetry.sbr
-.\Debug\cuddTable.sbr
-.\Debug\cuddUtil.sbr
-.\Debug\cuddWindow.sbr
-.\Debug\cuddZddCount.sbr
-.\Debug\cuddZddFuncs.sbr
-.\Debug\cuddZddGroup.sbr
-.\Debug\cuddZddIsop.sbr
-.\Debug\cuddZddLin.sbr
-.\Debug\cuddZddMisc.sbr
-.\Debug\cuddZddPort.sbr
-.\Debug\cuddZddReord.sbr
-.\Debug\cuddZddSetop.sbr
-.\Debug\cuddZddSymm.sbr
-.\Debug\cuddZddUtil.sbr
-.\Debug\epd.sbr
-.\Debug\mtrBasic.sbr
-.\Debug\mtrGroup.sbr
-.\Debug\parseCore.sbr
-.\Debug\parseStack.sbr
-.\Debug\dsdApi.sbr
-.\Debug\dsdCheck.sbr
-.\Debug\dsdLocal.sbr
-.\Debug\dsdMan.sbr
-.\Debug\dsdProc.sbr
-.\Debug\dsdTree.sbr
-.\Debug\reoApi.sbr
-.\Debug\reoCore.sbr
-.\Debug\reoProfile.sbr
-.\Debug\reoSift.sbr
-.\Debug\reoSwap.sbr
-.\Debug\reoTest.sbr
-.\Debug\reoTransfer.sbr
-.\Debug\reoUnits.sbr
-.\Debug\added.sbr
-.\Debug\solver.sbr
-.\Debug\msatActivity.sbr
-.\Debug\msatClause.sbr
-.\Debug\msatClauseVec.sbr
-.\Debug\msatMem.sbr
-.\Debug\msatOrderJ.sbr
-.\Debug\msatQueue.sbr
-.\Debug\msatRead.sbr
-.\Debug\msatSolverApi.sbr
-.\Debug\msatSolverCore.sbr
-.\Debug\msatSolverIo.sbr
-.\Debug\msatSolverSearch.sbr
-.\Debug\msatSort.sbr
-.\Debug\msatVec.sbr
-.\Debug\fraigApi.sbr
-.\Debug\fraigCanon.sbr
-.\Debug\fraigFanout.sbr
-.\Debug\fraigFeed.sbr
-.\Debug\fraigMan.sbr
-.\Debug\fraigMem.sbr
-.\Debug\fraigNode.sbr
-.\Debug\fraigPrime.sbr
-.\Debug\fraigSat.sbr
-.\Debug\fraigTable.sbr
-.\Debug\fraigUtil.sbr
-.\Debug\fraigVec.sbr
-.\Debug\csat_apis.sbr
-.\Debug\fxu.sbr
-.\Debug\fxuCreate.sbr
-.\Debug\fxuHeapD.sbr
-.\Debug\fxuHeapS.sbr
-.\Debug\fxuList.sbr
-.\Debug\fxuMatrix.sbr
-.\Debug\fxuPair.sbr
-.\Debug\fxuPrint.sbr
-.\Debug\fxuReduce.sbr
-.\Debug\fxuSelect.sbr
-.\Debug\fxuSingle.sbr
-.\Debug\fxuUpdate.sbr
-.\Debug\rwrDec.sbr
-.\Debug\rwrEva.sbr
-.\Debug\rwrExp.sbr
-.\Debug\rwrLib.sbr
-.\Debug\rwrMan.sbr
-.\Debug\rwrPrint.sbr
-.\Debug\rwrUtil.sbr
-.\Debug\cutApi.sbr
-.\Debug\cutCut.sbr
-.\Debug\cutMan.sbr
-.\Debug\cutMerge.sbr
-.\Debug\cutNode.sbr
-.\Debug\cutSeq.sbr
-.\Debug\cutTruth.sbr
-.\Debug\decAbc.sbr
-.\Debug\decFactor.sbr
-.\Debug\decMan.sbr
-.\Debug\decPrint.sbr
-.\Debug\decUtil.sbr
-.\Debug\simMan.sbr
-.\Debug\simSat.sbr
-.\Debug\simSupp.sbr
-.\Debug\simSwitch.sbr
-.\Debug\simSym.sbr
-.\Debug\simSymSat.sbr
-.\Debug\simSymSim.sbr
-.\Debug\simSymStr.sbr
-.\Debug\simUtils.sbr
-.\Debug\fpga.sbr
-.\Debug\fpgaCore.sbr
-.\Debug\fpgaCreate.sbr
-.\Debug\fpgaCut.sbr
-.\Debug\fpgaCutUtils.sbr
-.\Debug\fpgaFanout.sbr
-.\Debug\fpgaLib.sbr
-.\Debug\fpgaMatch.sbr
-.\Debug\fpgaSwitch.sbr
-.\Debug\fpgaTime.sbr
-.\Debug\fpgaTruth.sbr
-.\Debug\fpgaUtils.sbr
-.\Debug\fpgaVec.sbr
-.\Debug\mapper.sbr
-.\Debug\mapperCanon.sbr
-.\Debug\mapperCore.sbr
-.\Debug\mapperCreate.sbr
-.\Debug\mapperCut.sbr
-.\Debug\mapperCutUtils.sbr
-.\Debug\mapperFanout.sbr
-.\Debug\mapperLib.sbr
-.\Debug\mapperMatch.sbr
-.\Debug\mapperRefs.sbr
-.\Debug\mapperSuper.sbr
-.\Debug\mapperSwitch.sbr
-.\Debug\mapperTable.sbr
-.\Debug\mapperTime.sbr
-.\Debug\mapperTree.sbr
-.\Debug\mapperTruth.sbr
-.\Debug\mapperUtils.sbr
-.\Debug\mapperVec.sbr
-.\Debug\mio.sbr
-.\Debug\mioApi.sbr
-.\Debug\mioFunc.sbr
-.\Debug\mioRead.sbr
-.\Debug\mioUtils.sbr
-.\Debug\super.sbr
-.\Debug\superAnd.sbr
-.\Debug\superGate.sbr
-.\Debug\superWrite.sbr
-.\Debug\pgaCore.sbr
-.\Debug\pgaMan.sbr
-.\Debug\pgaMatch.sbr
-.\Debug\pgaUtil.sbr
-.\Debug\extraBddMisc.sbr
-.\Debug\extraBddSymm.sbr
-.\Debug\extraUtilBitMatrix.sbr
-.\Debug\extraUtilCanon.sbr
-.\Debug\extraUtilFile.sbr
-.\Debug\extraUtilMemory.sbr
-.\Debug\extraUtilMisc.sbr
-.\Debug\extraUtilProgress.sbr
-.\Debug\extraUtilReader.sbr
-.\Debug\st.sbr
-.\Debug\stmm.sbr
-.\Debug\cpu_stats.sbr
-.\Debug\cpu_time.sbr
-.\Debug\datalimit.sbr
-.\Debug\getopt.sbr
-.\Debug\pathsearch.sbr
-.\Debug\safe_mem.sbr
-.\Debug\strsav.sbr
-.\Debug\texpand.sbr
-.\Debug\mvc.sbr
-.\Debug\mvcApi.sbr
-.\Debug\mvcCompare.sbr
-.\Debug\mvcContain.sbr
-.\Debug\mvcCover.sbr
-.\Debug\mvcCube.sbr
-.\Debug\mvcDivide.sbr
-.\Debug\mvcDivisor.sbr
-.\Debug\mvcList.sbr
-.\Debug\mvcLits.sbr
-.\Debug\mvcMan.sbr
-.\Debug\mvcOpAlg.sbr
-.\Debug\mvcOpBool.sbr
-.\Debug\mvcPrint.sbr
-.\Debug\mvcSort.sbr
-.\Debug\mvcUtils.sbr
-.\Debug\npn.sbr
-.\Debug\npnGenStr.sbr
-.\Debug\npnTruth.sbr
-.\Debug\npnUtil.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP91D.tmp"
+/nologo /o"Release/abc.bsc" 
+.\Release\abcAig.sbr
+.\Release\abcCheck.sbr
+.\Release\abcDfs.sbr
+.\Release\abcFanio.sbr
+.\Release\abcFunc.sbr
+.\Release\abcLatch.sbr
+.\Release\abcMinBase.sbr
+.\Release\abcNames.sbr
+.\Release\abcNetlist.sbr
+.\Release\abcNtk.sbr
+.\Release\abcObj.sbr
+.\Release\abcRefs.sbr
+.\Release\abcShow.sbr
+.\Release\abcSop.sbr
+.\Release\abcUtil.sbr
+.\Release\abc.sbr
+.\Release\abcAttach.sbr
+.\Release\abcBalance.sbr
+.\Release\abcCollapse.sbr
+.\Release\abcCut.sbr
+.\Release\abcDsd.sbr
+.\Release\abcFpga.sbr
+.\Release\abcFraig.sbr
+.\Release\abcFxu.sbr
+.\Release\abcMap.sbr
+.\Release\abcMiter.sbr
+.\Release\abcNtbdd.sbr
+.\Release\abcPga.sbr
+.\Release\abcPrint.sbr
+.\Release\abcReconv.sbr
+.\Release\abcRefactor.sbr
+.\Release\abcRenode.sbr
+.\Release\abcRewrite.sbr
+.\Release\abcSat.sbr
+.\Release\abcStrash.sbr
+.\Release\abcSweep.sbr
+.\Release\abcSymm.sbr
+.\Release\abcTiming.sbr
+.\Release\abcUnreach.sbr
+.\Release\abcVerify.sbr
+.\Release\abcRetCore.sbr
+.\Release\abcRetDelay.sbr
+.\Release\abcRetImpl.sbr
+.\Release\abcRetUtil.sbr
+.\Release\abcSeq.sbr
+.\Release\abcShare.sbr
+.\Release\abcUtils.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\ioReadEqn.sbr
+.\Release\ioReadPla.sbr
+.\Release\ioReadVerilog.sbr
+.\Release\ioUtil.sbr
+.\Release\ioWriteBench.sbr
+.\Release\ioWriteBlif.sbr
+.\Release\ioWriteCnf.sbr
+.\Release\ioWriteDot.sbr
+.\Release\ioWriteEqn.sbr
+.\Release\ioWriteGml.sbr
+.\Release\ioWritePla.sbr
+.\Release\libSupport.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\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\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\cutApi.sbr
+.\Release\cutCut.sbr
+.\Release\cutMan.sbr
+.\Release\cutMerge.sbr
+.\Release\cutNode.sbr
+.\Release\cutSeq.sbr
+.\Release\cutTruth.sbr
+.\Release\decAbc.sbr
+.\Release\decFactor.sbr
+.\Release\decMan.sbr
+.\Release\decPrint.sbr
+.\Release\decUtil.sbr
+.\Release\simMan.sbr
+.\Release\simSat.sbr
+.\Release\simSupp.sbr
+.\Release\simSwitch.sbr
+.\Release\simSym.sbr
+.\Release\simSymSat.sbr
+.\Release\simSymSim.sbr
+.\Release\simSymStr.sbr
+.\Release\simUtils.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\fpgaSwitch.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\mapperSwitch.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\pgaCore.sbr
+.\Release\pgaMan.sbr
+.\Release\pgaMatch.sbr
+.\Release\pgaUtil.sbr
+.\Release\extraBddMisc.sbr
+.\Release\extraBddSymm.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
+.\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\npn.sbr
+.\Release\npnGenStr.sbr
+.\Release\npnTruth.sbr
+.\Release\npnUtil.sbr
+.\Release\abcFpgaSeq.sbr
+.\Release\abcFpgaDelay.sbr
+.\Release\cutOracle.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC90.tmp"
 Creating browse info file...
 
Output Window

 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4e2e14a2..ca9f1dfa 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -91,6 +91,8 @@ static int Abc_CommandPipe         ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandSeq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnseq        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqFpga      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqMap       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -172,6 +174,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
@@ -2735,16 +2739,20 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cut_Params_t Params, * pParams = &Params;
     Cut_Man_t * pCutMan;
+    Cut_Oracle_t * pCutOracle;
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
+    int fOracle;
     extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
+    extern void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * pCutOracle );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fOracle = 0;
     memset( pParams, 0, sizeof(Cut_Params_t) );
     pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
     pParams->nKeepMax  = 1000;  // the max number of cuts kept at a node
@@ -2754,7 +2762,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fMulti    = 0;     // use multi-input AND-gates
     pParams->fVerbose  = 0;     // the verbosiness flag
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "KMtfdmvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "KMtfdmvoh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2795,6 +2803,9 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             pParams->fVerbose ^= 1;
             break;
+        case 'o':
+            fOracle ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -2812,20 +2823,35 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Cut computation is available only for AIGs (run \"strash\").\n" );
         return 1;
     }
+    if ( pParams->nVarsMax < CUT_SIZE_MIN || pParams->nVarsMax > CUT_SIZE_MAX )
+    {
+        fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", CUT_SIZE_MIN, CUT_SIZE_MAX );
+        return 1;
+    }
+
+    if ( fOracle )
+        pParams->fRecord = 1;
     pCutMan = Abc_NtkCuts( pNtk, pParams );
     Cut_ManPrintStats( pCutMan );
+    if ( fOracle )
+        pCutOracle = Cut_OracleStart( pCutMan );
     Cut_ManStop( pCutMan );
+    if ( fOracle )
+    {
+        Abc_NtkCutsOracle( pNtk, pCutOracle );
+        Cut_OracleStop( pCutOracle );
+    }
     return 0;
 
 usage:
     fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdmvh]\n" );
     fprintf( pErr, "\t         computes k-feasible cuts for the AIG\n" );
-    fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",     pParams->nVarsMax );
+    fprintf( pErr, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n",   CUT_SIZE_MIN, CUT_SIZE_MAX, pParams->nVarsMax );
     fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
-    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth? "yes": "no" );
-    fprintf( pErr, "\t-f     : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter? "yes": "no" );
-    fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",    pParams->fDrop? "yes": "no" );
-    fprintf( pErr, "\t-m     : toggle using multi-input AND-gates [default = %s]\n",       pParams->fMulti? "yes": "no" );
+    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth?   "yes": "no" );
+    fprintf( pErr, "\t-f     : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter?  "yes": "no" );
+    fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",    pParams->fDrop?    "yes": "no" );
+    fprintf( pErr, "\t-m     : toggle using multi-input AND-gates [default = %s]\n",       pParams->fMulti?   "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -2913,6 +2939,12 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Sequential cuts can be computed for sequential AIGs (run \"seq\").\n" );
         return 1;
     }
+    if ( pParams->nVarsMax < CUT_SIZE_MIN || pParams->nVarsMax > CUT_SIZE_MAX )
+    {
+        fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", CUT_SIZE_MIN, CUT_SIZE_MAX );
+        return 1;
+    }
+
     pCutMan = Abc_NtkSeqCuts( pNtk, pParams );
     Cut_ManPrintStats( pCutMan );
     Cut_ManStop( pCutMan );
@@ -2921,9 +2953,9 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: scut [-K num] [-M num] [-tvh]\n" );
     fprintf( pErr, "\t         computes k-feasible cuts for the sequential AIG\n" );
-    fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",     pParams->nVarsMax );
+    fprintf( pErr, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n",   CUT_SIZE_MIN, CUT_SIZE_MAX, pParams->nVarsMax );
     fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
-    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth? "yes": "no" );
+    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth?   "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -4434,6 +4466,149 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkFpgaSeq( Abc_Ntk_t * pNtk, int fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
+        return 1;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkFpgaSeq( pNtk, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: sfpga [-vh]\n" );
+    fprintf( pErr, "\t        performs integrated sequential FPGA mapping\n" );
+    fprintf( pErr, "\t-v    : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkMapSeq( Abc_Ntk_t * pNtk, int fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
+        return 1;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkMapSeq( pNtk, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: smap [-vh]\n" );
+    fprintf( pErr, "\t        performs integrated sequential standard-cell mapping" );
+    fprintf( pErr, "\t-v    : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 7cc3d65b..8081c769 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -69,7 +69,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
         if ( Abc_ObjFanoutNum(pObj) > 0 )
             Cut_NodeSetTriv( p, pObj->Id );
     // compute cuts for internal nodes
-    vNodes = Abc_AigDfs( pNtk, 0, 1 );
+    vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs
     vChoices = Vec_IntAlloc( 100 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
@@ -105,11 +105,70 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     if ( pParams->fMulti )
         Abc_NtkBalanceDetach(pNtk);
 PRT( "Total", clock() - clk );
-Abc_NtkPrintCuts_( p, pNtk, 0 );
+//Abc_NtkPrintCuts_( p, pNtk, 0 );
 //    Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
     return p;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Cut computation using the oracle.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
+{
+    Abc_Obj_t * pObj;
+    Vec_Ptr_t * vNodes;
+    int i, clk = clock();
+    int fDrop = Cut_OracleReadDrop(p);
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // prepare cut droppping
+    if ( fDrop )
+        Cut_OracleSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) );
+
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_OracleNodeSetTriv( p, pObj->Id );
+
+    // compute cuts for internal nodes
+    vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // when we reached a CO, it is time to deallocate the cuts
+        if ( Abc_ObjIsCo(pObj) )
+        {
+            if ( fDrop )
+                Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            continue;
+        }
+        // skip constant node, it has no cuts
+        if ( Abc_NodeIsConst(pObj) )
+            continue;
+        // compute the cuts to the internal node
+        Cut_OracleComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
+                Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        // consider dropping the fanins cuts
+        if ( fDrop )
+        {
+            Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId1(pObj) );
+        }
+    }
+    Vec_PtrFree( vNodes );
+//PRT( "Total", clock() - clk );
+//Abc_NtkPrintCuts_( p, pNtk, 0 );
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Computes the cuts for the network.]
@@ -156,7 +215,6 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
         // compute the cuts for the internal nodes
         Abc_AigForEachAnd( pNtk, pObj, i )
             Abc_NodeGetCutsSeq( p, pObj, nIters==0 );
-Abc_NtkPrintCuts( p, pNtk, 1 );
         // merge the new cuts with the old cuts
         Abc_NtkForEachPi( pNtk, pObj, i )
             Cut_NodeNewMergeWithOld( p, pObj->Id );
@@ -183,7 +241,7 @@ Abc_NtkPrintCuts( p, pNtk, 1 );
         pObj->fMarkC = 0;
 PRT( "Total", clock() - clk );
 printf( "Converged after %d iterations.\n", nIters );
-Abc_NtkPrintCuts( p, pNtk, 1 );
+//Abc_NtkPrintCuts( p, pNtk, 1 );
     return p;
 }
 
@@ -225,7 +283,7 @@ void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti )
     assert( Abc_NtkIsStrash(pObj->pNtk) );
     assert( Abc_ObjFaninNum(pObj) == 2 );
     return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
-        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), 1, 1, fTriv );  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv );  
 }
 
 /**Function*************************************************************
@@ -244,7 +302,7 @@ void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv )
     int CutSetNum;
     assert( Abc_NtkIsSeq(pObj->pNtk) );
     assert( Abc_ObjFaninNum(pObj) == 2 );
-//    fTriv     = pObj->fMarkC ? 0 : fTriv;
+    fTriv     = pObj->fMarkC ? 0 : fTriv;
     CutSetNum = pObj->fMarkC ? (int)pObj->pCopy : -1;
     Cut_NodeComputeCutsSeq( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
         Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj), fTriv, CutSetNum );  
diff --git a/src/base/abcs/abcFpgaDelay.c b/src/base/abcs/abcFpgaDelay.c
new file mode 100644
index 00000000..1b957093
--- /dev/null
+++ b/src/base/abcs/abcFpgaDelay.c
@@ -0,0 +1,327 @@
+/**CFile****************************************************************
+
+  FileName    [abcFpgaDelay.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Utilities working sequential AIGs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcFpgaDelay.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abcs.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the internal procedures
+static int  Abc_NtkFpgaRetimeSearch_rec( Seq_FpgaMan_t * p, Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose );
+static int  Abc_NtkFpgaRetimeForPeriod( Seq_FpgaMan_t * p, Abc_Ntk_t * pNtk, int Fi, int fVerbose );
+static int  Abc_NodeFpgaUpdateLValue( Seq_FpgaMan_t * p, Abc_Obj_t * pObj, int Fi );
+static void Abc_NtkFpgaCollect( Seq_FpgaMan_t * p );
+
+// node status after updating its arrival time
+enum { ABC_FPGA_UPDATE_FAIL, ABC_FPGA_UPDATE_NO, ABC_FPGA_UPDATE_YES };
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes AIG for optimal delay.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFpgaSeqRetimeDelayLags( Seq_FpgaMan_t * p )
+{
+    Abc_Ntk_t * pNtk = p->pNtk;
+    int fVerbose = p->fVerbose;
+    Abc_Obj_t * pNode;
+    int i, FiMax, FiBest, RetValue;
+
+    // start storage for sequential arrival times
+    assert( pNtk->pData == NULL );
+    pNtk->pData = p->vArrivals;
+
+    // get the upper bound on the clock period
+//    FiMax = Abc_NtkNodeNum(pNtk);
+    FiMax = 0;
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        if ( FiMax < (int)pNode->Level )
+            FiMax = pNode->Level;
+    FiMax += 2;
+
+    // make sure this clock period is feasible
+    assert( Abc_NtkFpgaRetimeForPeriod( p, pNtk, FiMax, fVerbose ) );
+
+    // search for the optimal clock period between 0 and nLevelMax
+    FiBest = Abc_NtkFpgaRetimeSearch_rec( p, pNtk, 0, FiMax, fVerbose );
+
+    // recompute the best LValues
+    RetValue = Abc_NtkFpgaRetimeForPeriod( p, pNtk, FiBest, fVerbose );
+    assert( RetValue );
+
+    // print the result
+    if ( fVerbose )
+    printf( "The best clock period is %3d.\n", FiBest );
+
+    // convert to lags
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        Vec_StrWriteEntry( p->vLagsMap, i, (char)Abc_NodeGetLag(Abc_NodeReadLValue(pNode), FiBest) );
+/*
+    printf( "LValues : " );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        printf( "%d=%d ", i, Abc_NodeReadLValue(pNode) );
+    printf( "\n" );
+    printf( "Lags : " );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        if ( Vec_StrEntry(vLags,i) != 0 )
+            printf( "%d=%d(%d)(%d) ", i, Vec_StrEntry(vLags,i), Abc_NodeReadLValue(pNode), Abc_NodeReadLValue(pNode) - FiBest * Vec_StrEntry(vLags,i) );
+    printf( "\n" );
+*/
+    Abc_NtkFpgaCollect( p );
+
+    pNtk->pData = NULL;
+
+    Cut_ManStop( p->pMan );
+    p->pMan = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs binary search for the optimal clock period.]
+
+  Description [Assumes that FiMin is infeasible while FiMax is feasible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkFpgaRetimeSearch_rec( Seq_FpgaMan_t * p, Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose )
+{
+    int Median;
+    assert( FiMin < FiMax );
+    if ( FiMin + 1 == FiMax )
+        return FiMax;
+    Median = FiMin + (FiMax - FiMin)/2;
+    if ( Abc_NtkFpgaRetimeForPeriod( p, pNtk, Median, fVerbose ) )
+        return Abc_NtkFpgaRetimeSearch_rec( p, pNtk, FiMin, Median, fVerbose ); // Median is feasible
+    else 
+        return Abc_NtkFpgaRetimeSearch_rec( p, pNtk, Median, FiMax, fVerbose ); // Median is infeasible
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkFpgaRetimeForPeriod( Seq_FpgaMan_t * p, Abc_Ntk_t * pNtk, int Fi, int fVerbose )
+{
+    Abc_Obj_t * pObj;
+    int i, c, RetValue, fChange, Counter;
+    char * pReason = "";
+
+    // set l-values of all nodes to be minus infinity
+    Vec_IntFill( p->vArrivals, Abc_NtkObjNumMax(pNtk), -ABC_INFINITY );
+    Vec_PtrFill( p->vBestCuts, Abc_NtkObjNumMax(pNtk),  NULL         );
+
+    // set l-values for the constant and PIs
+    pObj = Abc_NtkObj( pNtk, 0 );
+    Abc_NodeSetLValue( pObj, 0 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NodeSetLValue( pObj, 0 );
+
+    // update all values iteratively
+    Counter = 0;
+    for ( c = 0; c < 20; c++ )
+    {
+        fChange = 0;
+        Abc_NtkForEachObj( pNtk, pObj, i )
+        {
+            if ( Abc_ObjIsPi(pObj) )
+                continue;
+            if ( Abc_ObjFaninNum(pObj) == 0 )
+                continue;
+            RetValue = Abc_NodeFpgaUpdateLValue( p, pObj, Fi );
+            Counter++;
+            if ( RetValue == ABC_FPGA_UPDATE_FAIL )
+                break;
+            if ( RetValue == ABC_FPGA_UPDATE_NO ) 
+                continue;
+            fChange = 1;
+        }
+        if ( RetValue == ABC_FPGA_UPDATE_FAIL )
+            break;
+        if ( fChange == 0 )
+            break;
+    }
+    if ( c == 20 )
+    {
+        RetValue = ABC_FPGA_UPDATE_FAIL;
+        pReason = "(timeout)";
+    }
+
+    // report the results
+    if ( fVerbose )
+    {
+        if ( RetValue == ABC_FPGA_UPDATE_FAIL )
+            printf( "Period = %3d.  Iterations = %3d.  Updates = %6d.  Infeasible %s\n", Fi, c, Counter, pReason );
+        else
+            printf( "Period = %3d.  Iterations = %3d.  Updates = %6d.  Feasible\n",   Fi, c, Counter );
+    }
+    return RetValue != ABC_FPGA_UPDATE_FAIL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeFpgaUpdateLValue( Seq_FpgaMan_t * p, Abc_Obj_t * pObj, int Fi )
+{
+    Abc_Obj_t * pFanin;
+    Cut_Cut_t * pList, * pCut, * pCutBest;
+    int lValueNew, lValueOld, lValueCur, lValueFan;
+    int i;
+
+    assert( !Abc_ObjIsPi(pObj) );
+    assert( Abc_ObjFaninNum(pObj) > 0 );
+
+    if ( Abc_ObjIsPo(pObj) )
+    {
+        lValueOld = Abc_NodeReadLValue(Abc_ObjFanin0(pObj));
+        lValueNew = lValueOld - Fi * Abc_ObjFaninL0(pObj);
+        return (lValueNew > Fi)? ABC_FPGA_UPDATE_FAIL : ABC_FPGA_UPDATE_NO;
+    }
+
+    pCutBest = NULL;
+    lValueNew = ABC_INFINITY;
+    pList = Abc_NodeReadCuts( p->pMan, pObj );
+    for ( pCut = pList; pCut; pCut = pCut->pNext )
+    {
+        if ( pCut->nLeaves < 2 )
+            continue;
+        lValueCur = -ABC_INFINITY;
+        for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        {
+            pFanin    = Abc_NtkObj( pObj->pNtk, (pCut->pLeaves[i] >> CUT_SHIFT) );
+            lValueFan = Abc_NodeReadLValue(pFanin) - Fi * (pCut->pLeaves[i] & CUT_MASK);
+            lValueCur = ABC_MAX( lValueCur, lValueFan );
+        }
+        lValueCur += 1;
+        lValueNew = ABC_MIN( lValueNew, lValueCur );
+        if ( lValueNew == lValueCur )
+            pCutBest = pCut;
+    }
+
+    lValueOld = Abc_NodeReadLValue(pObj);
+//    if ( lValueNew == lValueOld )
+    if ( lValueNew <= lValueOld )
+        return ABC_FPGA_UPDATE_NO;
+
+    Abc_NodeSetLValue( pObj, lValueNew );
+    Vec_PtrWriteEntry( p->vBestCuts, pObj->Id, pCutBest );
+    return ABC_FPGA_UPDATE_YES;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Select nodes visible in the mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFpgaCollect_rec( Seq_FpgaMan_t * p, Abc_Obj_t * pNode )
+{
+    Cut_Cut_t * pCutBest;
+    Abc_Obj_t * pFanin;
+    Vec_Int_t * vLeaves;
+    int i;
+    // skip the CI
+    if ( Abc_ObjIsCi(pNode) )
+        return;
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // get the best cut of the node
+    pCutBest = Vec_PtrEntry( p->vBestCuts, pNode->Id );
+    for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
+    {
+        pFanin = Abc_NtkObj( pNode->pNtk, (pCutBest->pLeaves[i] >> CUT_SHIFT) );
+        Abc_NodeFpgaCollect_rec( p, pFanin );
+    }
+    // collect the node and its cut
+    vLeaves = Vec_IntAlloc( pCutBest->nLeaves );
+    for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
+        Vec_IntPush( vLeaves, pCutBest->pLeaves[i] );
+    Vec_PtrPush( p->vMapCuts, vLeaves );
+    Vec_PtrPush( p->vMapping, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Select nodes visible in the mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFpgaCollect( Seq_FpgaMan_t * p )
+{
+    Abc_Ntk_t * pNtk = p->pNtk;
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_PtrClear( p->vMapping );
+    Vec_PtrClear( p->vMapCuts );
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NodeFpgaCollect_rec( p, Abc_ObjFanin0(pObj) );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcFpgaSeq.c b/src/base/abcs/abcFpgaSeq.c
new file mode 100644
index 00000000..d68c2082
--- /dev/null
+++ b/src/base/abcs/abcFpgaSeq.c
@@ -0,0 +1,201 @@
+/**CFile****************************************************************
+
+  FileName    [abcFpgaSeq.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Mapping for FPGAs using sequential cuts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcFpgaSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abcs.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+Abc_Ntk_t * Abc_NtkMapSeq( Abc_Ntk_t * pNtk, int fVerbose ) { return 0; }
+
+extern Cut_Man_t *     Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
+extern void            Abc_NtkFpgaSeqRetimeDelayLags( Seq_FpgaMan_t * p );
+
+static Seq_FpgaMan_t * Abc_NtkFpgaSeqStart( Abc_Ntk_t * pNtk, int fVerbose );
+static void            Abc_NtkFpgaSeqStop( Seq_FpgaMan_t * p );
+
+static Abc_Ntk_t *     Abc_NtkFpgaSeqConstruct( Seq_FpgaMan_t * p );
+static void            Abc_NtkFpgaSeqRetime( Seq_FpgaMan_t * p, Abc_Ntk_t * pNtkNew );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes AIG for optimal delay.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFpgaSeq( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Ntk_t * pNtkNew;
+    Seq_FpgaMan_t * p;
+    Cut_Params_t Params, * pParams = &Params;
+    int clk;
+
+    assert( Abc_NtkIsSeq( pNtk ) );
+
+    // get the sequential FPGA manager
+    p = Abc_NtkFpgaSeqStart( pNtk, fVerbose );
+
+    // create the cuts
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 1000;  // the max number of cuts kept at a node
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
+    pParams->fSeq      = 1;     // compute sequential cuts
+    pParams->fVerbose  = 0;     // the verbosiness flag
+
+clk = clock();
+    p->pMan = Abc_NtkSeqCuts( pNtk, pParams );
+p->timeCuts += clock() - clk;
+
+    // find best arrival times (p->vArrivals) and free the cuts
+    // select mapping (p->vMapping) and remember best cuts (p->vMapCuts) 
+clk = clock();
+    Abc_NtkFpgaSeqRetimeDelayLags( p );
+p->timeDelay += clock() - clk;
+
+return NULL;
+
+    // construct the network
+clk = clock();
+    pNtkNew = Abc_NtkFpgaSeqConstruct( p );
+p->timeNtk += clock() - clk;
+
+    // retime the network
+clk = clock();
+    Abc_NtkFpgaSeqRetime( p, pNtkNew );
+p->timeRet += clock() - clk;
+
+    // remove temporaries
+    Abc_NtkFpgaSeqStop( p );
+
+    // check the resulting network
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkFpgaSeq(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts sequential FPGA mapper.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Seq_FpgaMan_t * Abc_NtkFpgaSeqStart( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Seq_FpgaMan_t * p;
+    // create the FPGA mapping manager
+    p = ALLOC( Seq_FpgaMan_t, 1 );
+    memset( p, 0, sizeof(Seq_FpgaMan_t) );
+    p->pNtk      = pNtk;
+    p->pMan      = NULL;
+    p->vArrivals = Vec_IntAlloc( 0 );
+    p->vBestCuts = Vec_PtrAlloc( 0 );
+    p->vMapping  = Vec_PtrAlloc( 0 );
+    p->vMapCuts  = Vec_PtrAlloc( 0 );
+    p->vLagsMap  = Vec_StrStart( Abc_NtkObjNumMax(pNtk) );
+    p->fVerbose  = fVerbose;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops sequential FPGA mapper.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFpgaSeqStop( Seq_FpgaMan_t * p )
+{
+    if ( p->fVerbose )
+    {
+        printf( "Sequential FPGA mapping stats:\n" );
+//        printf( "Total allocated   = %8d.\n", p->nCutsAlloc );
+//        printf( "Cuts per node     = %8.1f\n", ((float)(p->nCutsCur-p->nCutsTriv))/p->nNodes );
+        PRT( "Cuts   ", p->timeCuts );
+        PRT( "Arrival", p->timeDelay );
+        PRT( "Network", p->timeNtk );
+        PRT( "Retime ", p->timeRet );
+    }
+    Vec_IntFree( p->vArrivals );
+    Vec_PtrFree( p->vBestCuts );
+    Vec_PtrFree( p->vMapping );
+    Vec_VecFree( (Vec_Vec_t *)p->vMapCuts );
+    Vec_StrFree( p->vLagsMap );
+    free( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Construct the final network after mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFpgaSeqConstruct( Seq_FpgaMan_t * p )
+{
+    Abc_Ntk_t * pNtk = NULL;
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes the final network after mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFpgaSeqRetime( Seq_FpgaMan_t * p, Abc_Ntk_t * pNtkNew )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcRetDelay.c b/src/base/abcs/abcRetDelay.c
index 0697c699..0eda33c9 100644
--- a/src/base/abcs/abcRetDelay.c
+++ b/src/base/abcs/abcRetDelay.c
@@ -24,12 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// storing arrival times in the nodes
-static inline int  Abc_NodeReadLValue( Abc_Obj_t * pNode )            { return Vec_IntEntry( (pNode)->pNtk->pData, (pNode)->Id );           }
-static inline void Abc_NodeSetLValue( Abc_Obj_t * pNode, int Value )  { Vec_IntWriteEntry( (pNode)->pNtk->pData, (pNode)->Id, (Value) );    }
-//static inline int  Abc_NodeGetLag( int LValue, int Fi )               { return LValue/Fi - (int)(LValue % Fi == 0); }
-static inline int  Abc_NodeGetLag( int LValue, int Fi )               { return (LValue + 256*Fi)/Fi - 256 - (int)(LValue % Fi == 0); }
-
 // the internal procedures
 static int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose );
 static int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose );
diff --git a/src/base/abcs/abcs.h b/src/base/abcs/abcs.h
index fb45efba..e250d929 100644
--- a/src/base/abcs/abcs.h
+++ b/src/base/abcs/abcs.h
@@ -26,6 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "abc.h"
+#include "cut.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -38,6 +39,25 @@
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Seq_FpgaMan_t_ Seq_FpgaMan_t;
+struct Seq_FpgaMan_t_
+{
+    Abc_Ntk_t *    pNtk;        // the network to be mapped
+    Cut_Man_t *    pMan;        // the cut manager
+    Vec_Int_t *    vArrivals;   // the arrival times (L-Values of nodes)
+    Vec_Ptr_t *    vBestCuts;   // the best cuts for nodes
+    Vec_Ptr_t *    vMapping;    // the nodes used in the mapping
+    Vec_Ptr_t *    vMapCuts;    // the info about the cut of each mapped node
+    Vec_Str_t *    vLagsMap;    // the lags of the mapped nodes
+    int            fVerbose;    // the verbose flag
+    // runtime stats
+    int            timeCuts;    // runtime to compute the cuts
+    int            timeDelay;   // runtime to compute the L-values
+    int            timeRet;     // runtime to retime the resulting network
+    int            timeNtk;     // runtime to create the final network
+};
+
+
 // representation of latch on the edge
 typedef struct Abc_RetEdge_t_       Abc_RetEdge_t;   
 struct Abc_RetEdge_t_ // 1 word
@@ -61,6 +81,12 @@ static inline Abc_RetEdge_t  Abc_Int2RetEdge( int Num )            { return *((A
 static inline int            Abc_RetStep2Int( Abc_RetStep_t Str )  { return *((int *)&Str);           }
 static inline Abc_RetStep_t  Abc_Int2RetStep( int Num )            { return *((Abc_RetStep_t *)&Num); }
 
+// storing arrival times in the nodes
+static inline int  Abc_NodeReadLValue( Abc_Obj_t * pNode )            { return Vec_IntEntry( (pNode)->pNtk->pData, (pNode)->Id );           }
+static inline void Abc_NodeSetLValue( Abc_Obj_t * pNode, int Value )  { Vec_IntWriteEntry( (pNode)->pNtk->pData, (pNode)->Id, (Value) );    }
+//static inline int  Abc_NodeGetLag( int LValue, int Fi )               { return LValue/Fi - (int)(LValue % Fi == 0); }
+static inline int  Abc_NodeGetLag( int LValue, int Fi )               { return (LValue + 256*Fi)/Fi - 256 - (int)(LValue % Fi == 0); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 5305ae31..839aa0b4 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -283,6 +283,7 @@ extern void        Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhas
 extern unsigned short Extra_TruthPerm4One( unsigned uTruth, int Phase );
 extern unsigned    Extra_TruthPerm5One( unsigned uTruth, int Phase );
 extern void        Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes );
+extern void        Extra_TruthExpand( int nVars, int nWords, unsigned * puTruth, unsigned uPhase, unsigned * puTruthR );
 /* precomputing tables for permutation mapping */
 extern void **     Extra_ArrayAlloc( int nCols, int nRows, int Size );
 extern unsigned short ** Extra_TruthPerm43();
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index 75e91cbc..19247472 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -1303,6 +1303,635 @@ void Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes a phase of the 8-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_TruthExpand( int nVars, int nWords, unsigned * puTruth, unsigned uPhase, unsigned * puTruthR )
+{
+    // elementary truth tables
+    static unsigned uTruths[8][8] = {
+        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
+        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
+        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
+        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
+        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
+        { 0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000 }, 
+        { 0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000 }, 
+        { 0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0x00000000,0x00000000 } 
+    };
+    static char Cases[256] = {
+         0, // 00000000
+         0, // 00000001
+         1, // 00000010
+         0, // 00000011
+         2, // 00000100
+        -1, // 00000101
+        -1, // 00000110
+         0, // 00000111
+         3, // 00001000
+        -1, // 00001001
+        -1, // 00001010
+        -1, // 00001011
+        -1, // 00001100
+        -1, // 00001101
+        -1, // 00001110
+         0, // 00001111
+         4, // 00010000
+        -1, // 00010001
+        -1, // 00010010
+        -1, // 00010011
+        -1, // 00010100
+        -1, // 00010101
+        -1, // 00010110
+        -1, // 00010111
+        -1, // 00011000
+        -1, // 00011001
+        -1, // 00011010
+        -1, // 00011011
+        -1, // 00011100
+        -1, // 00011101
+        -1, // 00011110
+         0, // 00011111
+         5, // 00100000
+        -1, // 00100001
+        -1, // 00100010
+        -1, // 00100011
+        -1, // 00100100
+        -1, // 00100101
+        -1, // 00100110
+        -1, // 00100111
+        -1, // 00101000
+        -1, // 00101001
+        -1, // 00101010
+        -1, // 00101011
+        -1, // 00101100
+        -1, // 00101101
+        -1, // 00101110
+        -1, // 00101111
+        -1, // 00110000
+        -1, // 00110001
+        -1, // 00110010
+        -1, // 00110011
+        -1, // 00110100
+        -1, // 00110101
+        -1, // 00110110
+        -1, // 00110111
+        -1, // 00111000
+        -1, // 00111001
+        -1, // 00111010
+        -1, // 00111011
+        -1, // 00111100
+        -1, // 00111101
+        -1, // 00111110
+         0, // 00111111
+         6, // 01000000
+        -1, // 01000001
+        -1, // 01000010
+        -1, // 01000011
+        -1, // 01000100
+        -1, // 01000101
+        -1, // 01000110
+        -1, // 01000111
+        -1, // 01001000
+        -1, // 01001001
+        -1, // 01001010
+        -1, // 01001011
+        -1, // 01001100
+        -1, // 01001101
+        -1, // 01001110
+        -1, // 01001111
+        -1, // 01010000
+        -1, // 01010001
+        -1, // 01010010
+        -1, // 01010011
+        -1, // 01010100
+        -1, // 01010101
+        -1, // 01010110
+        -1, // 01010111
+        -1, // 01011000
+        -1, // 01011001
+        -1, // 01011010
+        -1, // 01011011
+        -1, // 01011100
+        -1, // 01011101
+        -1, // 01011110
+        -1, // 01011111
+        -1, // 01100000
+        -1, // 01100001
+        -1, // 01100010
+        -1, // 01100011
+        -1, // 01100100
+        -1, // 01100101
+        -1, // 01100110
+        -1, // 01100111
+        -1, // 01101000
+        -1, // 01101001
+        -1, // 01101010
+        -1, // 01101011
+        -1, // 01101100
+        -1, // 01101101
+        -1, // 01101110
+        -1, // 01101111
+        -1, // 01110000
+        -1, // 01110001
+        -1, // 01110010
+        -1, // 01110011
+        -1, // 01110100
+        -1, // 01110101
+        -1, // 01110110
+        -1, // 01110111
+        -1, // 01111000
+        -1, // 01111001
+        -1, // 01111010
+        -1, // 01111011
+        -1, // 01111100
+        -1, // 01111101
+        -1, // 01111110
+         0, // 01111111
+         7, // 10000000
+        -1, // 10000001
+        -1, // 10000010
+        -1, // 10000011
+        -1, // 10000100
+        -1, // 10000101
+        -1, // 10000110
+        -1, // 10000111
+        -1, // 10001000
+        -1, // 10001001
+        -1, // 10001010
+        -1, // 10001011
+        -1, // 10001100
+        -1, // 10001101
+        -1, // 10001110
+        -1, // 10001111
+        -1, // 10010000
+        -1, // 10010001
+        -1, // 10010010
+        -1, // 10010011
+        -1, // 10010100
+        -1, // 10010101
+        -1, // 10010110
+        -1, // 10010111
+        -1, // 10011000
+        -1, // 10011001
+        -1, // 10011010
+        -1, // 10011011
+        -1, // 10011100
+        -1, // 10011101
+        -1, // 10011110
+        -1, // 10011111
+        -1, // 10100000
+        -1, // 10100001
+        -1, // 10100010
+        -1, // 10100011
+        -1, // 10100100
+        -1, // 10100101
+        -1, // 10100110
+        -1, // 10100111
+        -1, // 10101000
+        -1, // 10101001
+        -1, // 10101010
+        -1, // 10101011
+        -1, // 10101100
+        -1, // 10101101
+        -1, // 10101110
+        -1, // 10101111
+        -1, // 10110000
+        -1, // 10110001
+        -1, // 10110010
+        -1, // 10110011
+        -1, // 10110100
+        -1, // 10110101
+        -1, // 10110110
+        -1, // 10110111
+        -1, // 10111000
+        -1, // 10111001
+        -1, // 10111010
+        -1, // 10111011
+        -1, // 10111100
+        -1, // 10111101
+        -1, // 10111110
+        -1, // 10111111
+        -1, // 11000000
+        -1, // 11000001
+        -1, // 11000010
+        -1, // 11000011
+        -1, // 11000100
+        -1, // 11000101
+        -1, // 11000110
+        -1, // 11000111
+        -1, // 11001000
+        -1, // 11001001
+        -1, // 11001010
+        -1, // 11001011
+        -1, // 11001100
+        -1, // 11001101
+        -1, // 11001110
+        -1, // 11001111
+        -1, // 11010000
+        -1, // 11010001
+        -1, // 11010010
+        -1, // 11010011
+        -1, // 11010100
+        -1, // 11010101
+        -1, // 11010110
+        -1, // 11010111
+        -1, // 11011000
+        -1, // 11011001
+        -1, // 11011010
+        -1, // 11011011
+        -1, // 11011100
+        -1, // 11011101
+        -1, // 11011110
+        -1, // 11011111
+        -1, // 11100000
+        -1, // 11100001
+        -1, // 11100010
+        -1, // 11100011
+        -1, // 11100100
+        -1, // 11100101
+        -1, // 11100110
+        -1, // 11100111
+        -1, // 11101000
+        -1, // 11101001
+        -1, // 11101010
+        -1, // 11101011
+        -1, // 11101100
+        -1, // 11101101
+        -1, // 11101110
+        -1, // 11101111
+        -1, // 11110000
+        -1, // 11110001
+        -1, // 11110010
+        -1, // 11110011
+        -1, // 11110100
+        -1, // 11110101
+        -1, // 11110110
+        -1, // 11110111
+        -1, // 11111000
+        -1, // 11111001
+        -1, // 11111010
+        -1, // 11111011
+        -1, // 11111100
+        -1, // 11111101
+        -1, // 11111110
+         0  // 11111111
+    };
+    static char Perms[256][8] = {
+        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000000
+        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000001
+        { 1, 0, 2, 3, 4, 5, 6, 7 }, // 00000010
+        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000011
+        { 1, 2, 0, 3, 4, 5, 6, 7 }, // 00000100
+        { 0, 2, 1, 3, 4, 5, 6, 7 }, // 00000101
+        { 2, 0, 1, 3, 4, 5, 6, 7 }, // 00000110
+        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000111
+        { 1, 2, 3, 0, 4, 5, 6, 7 }, // 00001000
+        { 0, 2, 3, 1, 4, 5, 6, 7 }, // 00001001
+        { 2, 0, 3, 1, 4, 5, 6, 7 }, // 00001010
+        { 0, 1, 3, 2, 4, 5, 6, 7 }, // 00001011
+        { 2, 3, 0, 1, 4, 5, 6, 7 }, // 00001100
+        { 0, 3, 1, 2, 4, 5, 6, 7 }, // 00001101
+        { 3, 0, 1, 2, 4, 5, 6, 7 }, // 00001110
+        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00001111
+        { 1, 2, 3, 4, 0, 5, 6, 7 }, // 00010000
+        { 0, 2, 3, 4, 1, 5, 6, 7 }, // 00010001
+        { 2, 0, 3, 4, 1, 5, 6, 7 }, // 00010010
+        { 0, 1, 3, 4, 2, 5, 6, 7 }, // 00010011
+        { 2, 3, 0, 4, 1, 5, 6, 7 }, // 00010100
+        { 0, 3, 1, 4, 2, 5, 6, 7 }, // 00010101
+        { 3, 0, 1, 4, 2, 5, 6, 7 }, // 00010110
+        { 0, 1, 2, 4, 3, 5, 6, 7 }, // 00010111
+        { 2, 3, 4, 0, 1, 5, 6, 7 }, // 00011000
+        { 0, 3, 4, 1, 2, 5, 6, 7 }, // 00011001
+        { 3, 0, 4, 1, 2, 5, 6, 7 }, // 00011010
+        { 0, 1, 4, 2, 3, 5, 6, 7 }, // 00011011
+        { 3, 4, 0, 1, 2, 5, 6, 7 }, // 00011100
+        { 0, 4, 1, 2, 3, 5, 6, 7 }, // 00011101
+        { 4, 0, 1, 2, 3, 5, 6, 7 }, // 00011110
+        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00011111
+        { 1, 2, 3, 4, 5, 0, 6, 7 }, // 00100000
+        { 0, 2, 3, 4, 5, 1, 6, 7 }, // 00100001
+        { 2, 0, 3, 4, 5, 1, 6, 7 }, // 00100010
+        { 0, 1, 3, 4, 5, 2, 6, 7 }, // 00100011
+        { 2, 3, 0, 4, 5, 1, 6, 7 }, // 00100100
+        { 0, 3, 1, 4, 5, 2, 6, 7 }, // 00100101
+        { 3, 0, 1, 4, 5, 2, 6, 7 }, // 00100110
+        { 0, 1, 2, 4, 5, 3, 6, 7 }, // 00100111
+        { 2, 3, 4, 0, 5, 1, 6, 7 }, // 00101000
+        { 0, 3, 4, 1, 5, 2, 6, 7 }, // 00101001
+        { 3, 0, 4, 1, 5, 2, 6, 7 }, // 00101010
+        { 0, 1, 4, 2, 5, 3, 6, 7 }, // 00101011
+        { 3, 4, 0, 1, 5, 2, 6, 7 }, // 00101100
+        { 0, 4, 1, 2, 5, 3, 6, 7 }, // 00101101
+        { 4, 0, 1, 2, 5, 3, 6, 7 }, // 00101110
+        { 0, 1, 2, 3, 5, 4, 6, 7 }, // 00101111
+        { 2, 3, 4, 5, 0, 1, 6, 7 }, // 00110000
+        { 0, 3, 4, 5, 1, 2, 6, 7 }, // 00110001
+        { 3, 0, 4, 5, 1, 2, 6, 7 }, // 00110010
+        { 0, 1, 4, 5, 2, 3, 6, 7 }, // 00110011
+        { 3, 4, 0, 5, 1, 2, 6, 7 }, // 00110100
+        { 0, 4, 1, 5, 2, 3, 6, 7 }, // 00110101
+        { 4, 0, 1, 5, 2, 3, 6, 7 }, // 00110110
+        { 0, 1, 2, 5, 3, 4, 6, 7 }, // 00110111
+        { 3, 4, 5, 0, 1, 2, 6, 7 }, // 00111000
+        { 0, 4, 5, 1, 2, 3, 6, 7 }, // 00111001
+        { 4, 0, 5, 1, 2, 3, 6, 7 }, // 00111010
+        { 0, 1, 5, 2, 3, 4, 6, 7 }, // 00111011
+        { 4, 5, 0, 1, 2, 3, 6, 7 }, // 00111100
+        { 0, 5, 1, 2, 3, 4, 6, 7 }, // 00111101
+        { 5, 0, 1, 2, 3, 4, 6, 7 }, // 00111110
+        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00111111
+        { 1, 2, 3, 4, 5, 6, 0, 7 }, // 01000000
+        { 0, 2, 3, 4, 5, 6, 1, 7 }, // 01000001
+        { 2, 0, 3, 4, 5, 6, 1, 7 }, // 01000010
+        { 0, 1, 3, 4, 5, 6, 2, 7 }, // 01000011
+        { 2, 3, 0, 4, 5, 6, 1, 7 }, // 01000100
+        { 0, 3, 1, 4, 5, 6, 2, 7 }, // 01000101
+        { 3, 0, 1, 4, 5, 6, 2, 7 }, // 01000110
+        { 0, 1, 2, 4, 5, 6, 3, 7 }, // 01000111
+        { 2, 3, 4, 0, 5, 6, 1, 7 }, // 01001000
+        { 0, 3, 4, 1, 5, 6, 2, 7 }, // 01001001
+        { 3, 0, 4, 1, 5, 6, 2, 7 }, // 01001010
+        { 0, 1, 4, 2, 5, 6, 3, 7 }, // 01001011
+        { 3, 4, 0, 1, 5, 6, 2, 7 }, // 01001100
+        { 0, 4, 1, 2, 5, 6, 3, 7 }, // 01001101
+        { 4, 0, 1, 2, 5, 6, 3, 7 }, // 01001110
+        { 0, 1, 2, 3, 5, 6, 4, 7 }, // 01001111
+        { 2, 3, 4, 5, 0, 6, 1, 7 }, // 01010000
+        { 0, 3, 4, 5, 1, 6, 2, 7 }, // 01010001
+        { 3, 0, 4, 5, 1, 6, 2, 7 }, // 01010010
+        { 0, 1, 4, 5, 2, 6, 3, 7 }, // 01010011
+        { 3, 4, 0, 5, 1, 6, 2, 7 }, // 01010100
+        { 0, 4, 1, 5, 2, 6, 3, 7 }, // 01010101
+        { 4, 0, 1, 5, 2, 6, 3, 7 }, // 01010110
+        { 0, 1, 2, 5, 3, 6, 4, 7 }, // 01010111
+        { 3, 4, 5, 0, 1, 6, 2, 7 }, // 01011000
+        { 0, 4, 5, 1, 2, 6, 3, 7 }, // 01011001
+        { 4, 0, 5, 1, 2, 6, 3, 7 }, // 01011010
+        { 0, 1, 5, 2, 3, 6, 4, 7 }, // 01011011
+        { 4, 5, 0, 1, 2, 6, 3, 7 }, // 01011100
+        { 0, 5, 1, 2, 3, 6, 4, 7 }, // 01011101
+        { 5, 0, 1, 2, 3, 6, 4, 7 }, // 01011110
+        { 0, 1, 2, 3, 4, 6, 5, 7 }, // 01011111
+        { 2, 3, 4, 5, 6, 0, 1, 7 }, // 01100000
+        { 0, 3, 4, 5, 6, 1, 2, 7 }, // 01100001
+        { 3, 0, 4, 5, 6, 1, 2, 7 }, // 01100010
+        { 0, 1, 4, 5, 6, 2, 3, 7 }, // 01100011
+        { 3, 4, 0, 5, 6, 1, 2, 7 }, // 01100100
+        { 0, 4, 1, 5, 6, 2, 3, 7 }, // 01100101
+        { 4, 0, 1, 5, 6, 2, 3, 7 }, // 01100110
+        { 0, 1, 2, 5, 6, 3, 4, 7 }, // 01100111
+        { 3, 4, 5, 0, 6, 1, 2, 7 }, // 01101000
+        { 0, 4, 5, 1, 6, 2, 3, 7 }, // 01101001
+        { 4, 0, 5, 1, 6, 2, 3, 7 }, // 01101010
+        { 0, 1, 5, 2, 6, 3, 4, 7 }, // 01101011
+        { 4, 5, 0, 1, 6, 2, 3, 7 }, // 01101100
+        { 0, 5, 1, 2, 6, 3, 4, 7 }, // 01101101
+        { 5, 0, 1, 2, 6, 3, 4, 7 }, // 01101110
+        { 0, 1, 2, 3, 6, 4, 5, 7 }, // 01101111
+        { 3, 4, 5, 6, 0, 1, 2, 7 }, // 01110000
+        { 0, 4, 5, 6, 1, 2, 3, 7 }, // 01110001
+        { 4, 0, 5, 6, 1, 2, 3, 7 }, // 01110010
+        { 0, 1, 5, 6, 2, 3, 4, 7 }, // 01110011
+        { 4, 5, 0, 6, 1, 2, 3, 7 }, // 01110100
+        { 0, 5, 1, 6, 2, 3, 4, 7 }, // 01110101
+        { 5, 0, 1, 6, 2, 3, 4, 7 }, // 01110110
+        { 0, 1, 2, 6, 3, 4, 5, 7 }, // 01110111
+        { 4, 5, 6, 0, 1, 2, 3, 7 }, // 01111000
+        { 0, 5, 6, 1, 2, 3, 4, 7 }, // 01111001
+        { 5, 0, 6, 1, 2, 3, 4, 7 }, // 01111010
+        { 0, 1, 6, 2, 3, 4, 5, 7 }, // 01111011
+        { 5, 6, 0, 1, 2, 3, 4, 7 }, // 01111100
+        { 0, 6, 1, 2, 3, 4, 5, 7 }, // 01111101
+        { 6, 0, 1, 2, 3, 4, 5, 7 }, // 01111110
+        { 0, 1, 2, 3, 4, 5, 6, 7 }, // 01111111
+        { 1, 2, 3, 4, 5, 6, 7, 0 }, // 10000000
+        { 0, 2, 3, 4, 5, 6, 7, 1 }, // 10000001
+        { 2, 0, 3, 4, 5, 6, 7, 1 }, // 10000010
+        { 0, 1, 3, 4, 5, 6, 7, 2 }, // 10000011
+        { 2, 3, 0, 4, 5, 6, 7, 1 }, // 10000100
+        { 0, 3, 1, 4, 5, 6, 7, 2 }, // 10000101
+        { 3, 0, 1, 4, 5, 6, 7, 2 }, // 10000110
+        { 0, 1, 2, 4, 5, 6, 7, 3 }, // 10000111
+        { 2, 3, 4, 0, 5, 6, 7, 1 }, // 10001000
+        { 0, 3, 4, 1, 5, 6, 7, 2 }, // 10001001
+        { 3, 0, 4, 1, 5, 6, 7, 2 }, // 10001010
+        { 0, 1, 4, 2, 5, 6, 7, 3 }, // 10001011
+        { 3, 4, 0, 1, 5, 6, 7, 2 }, // 10001100
+        { 0, 4, 1, 2, 5, 6, 7, 3 }, // 10001101
+        { 4, 0, 1, 2, 5, 6, 7, 3 }, // 10001110
+        { 0, 1, 2, 3, 5, 6, 7, 4 }, // 10001111
+        { 2, 3, 4, 5, 0, 6, 7, 1 }, // 10010000
+        { 0, 3, 4, 5, 1, 6, 7, 2 }, // 10010001
+        { 3, 0, 4, 5, 1, 6, 7, 2 }, // 10010010
+        { 0, 1, 4, 5, 2, 6, 7, 3 }, // 10010011
+        { 3, 4, 0, 5, 1, 6, 7, 2 }, // 10010100
+        { 0, 4, 1, 5, 2, 6, 7, 3 }, // 10010101
+        { 4, 0, 1, 5, 2, 6, 7, 3 }, // 10010110
+        { 0, 1, 2, 5, 3, 6, 7, 4 }, // 10010111
+        { 3, 4, 5, 0, 1, 6, 7, 2 }, // 10011000
+        { 0, 4, 5, 1, 2, 6, 7, 3 }, // 10011001
+        { 4, 0, 5, 1, 2, 6, 7, 3 }, // 10011010
+        { 0, 1, 5, 2, 3, 6, 7, 4 }, // 10011011
+        { 4, 5, 0, 1, 2, 6, 7, 3 }, // 10011100
+        { 0, 5, 1, 2, 3, 6, 7, 4 }, // 10011101
+        { 5, 0, 1, 2, 3, 6, 7, 4 }, // 10011110
+        { 0, 1, 2, 3, 4, 6, 7, 5 }, // 10011111
+        { 2, 3, 4, 5, 6, 0, 7, 1 }, // 10100000
+        { 0, 3, 4, 5, 6, 1, 7, 2 }, // 10100001
+        { 3, 0, 4, 5, 6, 1, 7, 2 }, // 10100010
+        { 0, 1, 4, 5, 6, 2, 7, 3 }, // 10100011
+        { 3, 4, 0, 5, 6, 1, 7, 2 }, // 10100100
+        { 0, 4, 1, 5, 6, 2, 7, 3 }, // 10100101
+        { 4, 0, 1, 5, 6, 2, 7, 3 }, // 10100110
+        { 0, 1, 2, 5, 6, 3, 7, 4 }, // 10100111
+        { 3, 4, 5, 0, 6, 1, 7, 2 }, // 10101000
+        { 0, 4, 5, 1, 6, 2, 7, 3 }, // 10101001
+        { 4, 0, 5, 1, 6, 2, 7, 3 }, // 10101010
+        { 0, 1, 5, 2, 6, 3, 7, 4 }, // 10101011
+        { 4, 5, 0, 1, 6, 2, 7, 3 }, // 10101100
+        { 0, 5, 1, 2, 6, 3, 7, 4 }, // 10101101
+        { 5, 0, 1, 2, 6, 3, 7, 4 }, // 10101110
+        { 0, 1, 2, 3, 6, 4, 7, 5 }, // 10101111
+        { 3, 4, 5, 6, 0, 1, 7, 2 }, // 10110000
+        { 0, 4, 5, 6, 1, 2, 7, 3 }, // 10110001
+        { 4, 0, 5, 6, 1, 2, 7, 3 }, // 10110010
+        { 0, 1, 5, 6, 2, 3, 7, 4 }, // 10110011
+        { 4, 5, 0, 6, 1, 2, 7, 3 }, // 10110100
+        { 0, 5, 1, 6, 2, 3, 7, 4 }, // 10110101
+        { 5, 0, 1, 6, 2, 3, 7, 4 }, // 10110110
+        { 0, 1, 2, 6, 3, 4, 7, 5 }, // 10110111
+        { 4, 5, 6, 0, 1, 2, 7, 3 }, // 10111000
+        { 0, 5, 6, 1, 2, 3, 7, 4 }, // 10111001
+        { 5, 0, 6, 1, 2, 3, 7, 4 }, // 10111010
+        { 0, 1, 6, 2, 3, 4, 7, 5 }, // 10111011
+        { 5, 6, 0, 1, 2, 3, 7, 4 }, // 10111100
+        { 0, 6, 1, 2, 3, 4, 7, 5 }, // 10111101
+        { 6, 0, 1, 2, 3, 4, 7, 5 }, // 10111110
+        { 0, 1, 2, 3, 4, 5, 7, 6 }, // 10111111
+        { 2, 3, 4, 5, 6, 7, 0, 1 }, // 11000000
+        { 0, 3, 4, 5, 6, 7, 1, 2 }, // 11000001
+        { 3, 0, 4, 5, 6, 7, 1, 2 }, // 11000010
+        { 0, 1, 4, 5, 6, 7, 2, 3 }, // 11000011
+        { 3, 4, 0, 5, 6, 7, 1, 2 }, // 11000100
+        { 0, 4, 1, 5, 6, 7, 2, 3 }, // 11000101
+        { 4, 0, 1, 5, 6, 7, 2, 3 }, // 11000110
+        { 0, 1, 2, 5, 6, 7, 3, 4 }, // 11000111
+        { 3, 4, 5, 0, 6, 7, 1, 2 }, // 11001000
+        { 0, 4, 5, 1, 6, 7, 2, 3 }, // 11001001
+        { 4, 0, 5, 1, 6, 7, 2, 3 }, // 11001010
+        { 0, 1, 5, 2, 6, 7, 3, 4 }, // 11001011
+        { 4, 5, 0, 1, 6, 7, 2, 3 }, // 11001100
+        { 0, 5, 1, 2, 6, 7, 3, 4 }, // 11001101
+        { 5, 0, 1, 2, 6, 7, 3, 4 }, // 11001110
+        { 0, 1, 2, 3, 6, 7, 4, 5 }, // 11001111
+        { 3, 4, 5, 6, 0, 7, 1, 2 }, // 11010000
+        { 0, 4, 5, 6, 1, 7, 2, 3 }, // 11010001
+        { 4, 0, 5, 6, 1, 7, 2, 3 }, // 11010010
+        { 0, 1, 5, 6, 2, 7, 3, 4 }, // 11010011
+        { 4, 5, 0, 6, 1, 7, 2, 3 }, // 11010100
+        { 0, 5, 1, 6, 2, 7, 3, 4 }, // 11010101
+        { 5, 0, 1, 6, 2, 7, 3, 4 }, // 11010110
+        { 0, 1, 2, 6, 3, 7, 4, 5 }, // 11010111
+        { 4, 5, 6, 0, 1, 7, 2, 3 }, // 11011000
+        { 0, 5, 6, 1, 2, 7, 3, 4 }, // 11011001
+        { 5, 0, 6, 1, 2, 7, 3, 4 }, // 11011010
+        { 0, 1, 6, 2, 3, 7, 4, 5 }, // 11011011
+        { 5, 6, 0, 1, 2, 7, 3, 4 }, // 11011100
+        { 0, 6, 1, 2, 3, 7, 4, 5 }, // 11011101
+        { 6, 0, 1, 2, 3, 7, 4, 5 }, // 11011110
+        { 0, 1, 2, 3, 4, 7, 5, 6 }, // 11011111
+        { 3, 4, 5, 6, 7, 0, 1, 2 }, // 11100000
+        { 0, 4, 5, 6, 7, 1, 2, 3 }, // 11100001
+        { 4, 0, 5, 6, 7, 1, 2, 3 }, // 11100010
+        { 0, 1, 5, 6, 7, 2, 3, 4 }, // 11100011
+        { 4, 5, 0, 6, 7, 1, 2, 3 }, // 11100100
+        { 0, 5, 1, 6, 7, 2, 3, 4 }, // 11100101
+        { 5, 0, 1, 6, 7, 2, 3, 4 }, // 11100110
+        { 0, 1, 2, 6, 7, 3, 4, 5 }, // 11100111
+        { 4, 5, 6, 0, 7, 1, 2, 3 }, // 11101000
+        { 0, 5, 6, 1, 7, 2, 3, 4 }, // 11101001
+        { 5, 0, 6, 1, 7, 2, 3, 4 }, // 11101010
+        { 0, 1, 6, 2, 7, 3, 4, 5 }, // 11101011
+        { 5, 6, 0, 1, 7, 2, 3, 4 }, // 11101100
+        { 0, 6, 1, 2, 7, 3, 4, 5 }, // 11101101
+        { 6, 0, 1, 2, 7, 3, 4, 5 }, // 11101110
+        { 0, 1, 2, 3, 7, 4, 5, 6 }, // 11101111
+        { 4, 5, 6, 7, 0, 1, 2, 3 }, // 11110000
+        { 0, 5, 6, 7, 1, 2, 3, 4 }, // 11110001
+        { 5, 0, 6, 7, 1, 2, 3, 4 }, // 11110010
+        { 0, 1, 6, 7, 2, 3, 4, 5 }, // 11110011
+        { 5, 6, 0, 7, 1, 2, 3, 4 }, // 11110100
+        { 0, 6, 1, 7, 2, 3, 4, 5 }, // 11110101
+        { 6, 0, 1, 7, 2, 3, 4, 5 }, // 11110110
+        { 0, 1, 2, 7, 3, 4, 5, 6 }, // 11110111
+        { 5, 6, 7, 0, 1, 2, 3, 4 }, // 11111000
+        { 0, 6, 7, 1, 2, 3, 4, 5 }, // 11111001
+        { 6, 0, 7, 1, 2, 3, 4, 5 }, // 11111010
+        { 0, 1, 7, 2, 3, 4, 5, 6 }, // 11111011
+        { 6, 7, 0, 1, 2, 3, 4, 5 }, // 11111100
+        { 0, 7, 1, 2, 3, 4, 5, 6 }, // 11111101
+        { 7, 0, 1, 2, 3, 4, 5, 6 }, // 11111110
+        { 0, 1, 2, 3, 4, 5, 6, 7 }  // 11111111
+    };
+
+    assert( uPhase > 0 && uPhase < (unsigned)(1 << nVars) );
+
+    // the same function
+    if ( Cases[uPhase] == 0 )
+    {
+        int i;
+        for ( i = 0; i < nWords; i++ )
+            puTruthR[i] = puTruth[i];
+        return;
+    }
+
+    // an elementary variable
+    if ( Cases[uPhase] > 0 )
+    {
+        int i;
+        for ( i = 0; i < nWords; i++ )
+            puTruthR[i] = uTruths[Cases[uPhase]][i];
+        return;
+    }
+
+    // truth table takes one word
+    if ( nWords == 1 )
+    {
+        int i, k, nMints, iRes;
+        char * pPerm = Perms[uPhase];
+        puTruthR[0] = 0;
+        nMints = (1 << nVars);
+        for ( i = 0; i < nMints; i++ )
+            if ( puTruth[0] & (1 << i) )
+            {
+                for ( iRes = 0, k = 0; k < nVars; k++ )
+                    if ( i & (1 << pPerm[k]) )
+                        iRes |= (1 << k);
+                puTruthR[0] |= (1 << iRes);
+            }
+        return;
+    }
+    else if ( nWords == 2 )
+    {
+        int i, k, iRes;
+        char * pPerm = Perms[uPhase];
+        puTruthR[0] = puTruthR[1] = 0;
+        for ( i = 0; i < 32; i++ )
+        {
+            if ( puTruth[0] & (1 << i) )
+            {
+                for ( iRes = 0, k = 0; k < 6; k++ )
+                    if ( i & (1 << pPerm[k]) )
+                        iRes |= (1 << k);
+                if ( iRes < 32 )
+                    puTruthR[0] |= (1 << iRes);
+                else
+                    puTruthR[1] |= (1 << (iRes-32));
+            }
+        }
+        for ( ; i < 64; i++ )
+        {
+            if ( puTruth[1] & (1 << (i-32)) )
+            {
+                for ( iRes = 0, k = 0; k < 6; k++ )
+                    if ( i & (1 << pPerm[k]) )
+                        iRes |= (1 << k);
+                if ( iRes < 32 )
+                    puTruthR[0] |= (1 << iRes);
+                else
+                    puTruthR[1] |= (1 << (iRes-32));
+            }
+        }
+    }
+    // truth table takes more than one word
+    else
+    {
+        int i, k, nMints, iRes;
+        char * pPerm = Perms[uPhase];
+        for ( i = 0; i < nWords; i++ )
+            puTruthR[i] = 0;
+        nMints = (1 << nVars);
+        for ( i = 0; i < nMints; i++ )
+            if ( puTruth[i/32] & (1 << (i%32)) )
+            {
+                for ( iRes = 0, k = 0; k < 5; k++ )
+                    if ( i & (1 << pPerm[k]) )
+                        iRes |= (1 << k);
+                puTruthR[iRes/32] |= (1 << (iRes%32));
+            }
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    [Allocated lookup table for truth table permutation.]
@@ -1410,6 +2039,35 @@ unsigned ** Extra_TruthPerm63()
     return pTable;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the elementary truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned ** Extra_Truths8()
+{
+    static unsigned uTruths[8][8] = {
+        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
+        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
+        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
+        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
+        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
+        { 0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000 }, 
+        { 0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000 }, 
+        { 0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0x00000000,0x00000000 } 
+    };
+    static unsigned * puResult[8] = {
+        uTruths[0], uTruths[1], uTruths[2], uTruths[3], uTruths[4], uTruths[5], uTruths[6], uTruths[7] 
+    };
+    return (unsigned **)puResult;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Returns the smallest prime larger than the number.]
@@ -1456,6 +2114,72 @@ unsigned int Cudd_PrimeCopy( unsigned int  p)
 /*---------------------------------------------------------------------------*/
 
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the permutation table for 8 variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_TruthExpandGeneratePermTable()
+{
+    int i, k, nOnes, Last1, First0;
+    int iOne, iZero;
+
+    printf( "\nstatic char Cases[256] = {\n" );
+    for ( i = 0; i < 256; i++ )
+    {
+        nOnes = 0;
+        Last1 = First0 = -1;
+        for ( k = 0; k < 8; k++ )
+        {
+            if ( i & (1 << k) )
+            {
+                nOnes++;
+                Last1 = k;
+            }
+            else if ( First0 == -1 )
+                First0 = k;
+        }
+        if ( Last1 + 1 == First0 || i == 255 )
+            printf( "     %d%s", 0, (i==255? " ":",") );
+        else if ( nOnes == 1 )
+            printf( "     %d,", Last1 );
+        else
+            printf( "    -%d,", 1 );
+        printf( " // " );
+        Extra_PrintBinary( stdout, &((unsigned)i), 8 );
+        printf( "\n" );
+    }
+    printf( "};\n" );
+
+    printf( "\nstatic char Perms[256][8] = {\n" );
+    for ( i = 0; i < 256; i++ )
+    {
+        printf( "    {" );
+        nOnes = 0;
+        for ( k = 0; k < 8; k++ )
+            if ( i & (1 << k) )
+                nOnes++;
+        iOne = 0;
+        iZero = nOnes;
+        for ( k = 0; k < 8; k++ )
+            if ( i & (1 << k) )
+                printf( "%s %d", (k==0? "":","), iOne++ );
+            else
+                printf( "%s %d", (k==0? "":","), iZero++ );
+        assert( iOne + iZero == 8 );
+        printf( " }%s // ", (i==255? " ":",") );
+        Extra_PrintBinary( stdout, &((unsigned)i), 8 );
+        printf( "\n" );
+    }
+    printf( "};\n" );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecFan.h b/src/misc/vec/vecFan.h
index 08d1d734..496934a1 100644
--- a/src/misc/vec/vecFan.h
+++ b/src/misc/vec/vecFan.h
@@ -40,7 +40,7 @@ typedef struct Abc_Fan_t_       Abc_Fan_t;
 struct Abc_Fan_t_ // 1 word
 {
     unsigned         iFan    : 24;  // the ID of the object
-    unsigned         nLats   :  7;  // the number of latches (up to 31)
+    unsigned         nLats   :  7;  // the number of latches (up to 127)
     unsigned         fCompl  :  1;  // the complemented attribute
 };
 
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index ecdfed72..9908f6a8 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -29,32 +29,40 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#define CUT_SIZE_MIN    3      // the min K of the K-feasible cut computation
+#define CUT_SIZE_MAX    8      // the max K of the K-feasible cut computation
+
+#define CUT_SHIFT       8      // the number of bits for storing latch number in the cut leaves
+#define CUT_MASK        0xFF   // the mask to get the stored latch number
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
 typedef struct Cut_ManStruct_t_         Cut_Man_t;
+typedef struct Cut_OracleStruct_t_      Cut_Oracle_t;
 typedef struct Cut_CutStruct_t_         Cut_Cut_t;
 typedef struct Cut_ParamsStruct_t_      Cut_Params_t;
 
 struct Cut_ParamsStruct_t_
 {
-    int  nVarsMax;      // the max cut size ("k" of the k-feasible cuts)
-    int  nKeepMax;      // the max number of cuts kept at a node
-    int  nIdsMax;       // the max number of IDs of cut objects
-    int  nCutSet;       // the number of nodes in the cut set
-    int  fTruth;        // compute truth tables
-    int  fFilter;       // filter dominated cuts
-    int  fSeq;          // compute sequential cuts
-    int  fDrop;         // drop cuts on the fly
-    int  fMulti;        // compute cuts in multi-input AND gate graph
-    int  fVerbose;      // the verbosiness flag
+    int                nVarsMax;          // the max cut size ("k" of the k-feasible cuts)
+    int                nKeepMax;          // the max number of cuts kept at a node
+    int                nIdsMax;           // the max number of IDs of cut objects
+    int                nCutSet;           // the number of nodes in the cut set
+    int                fTruth;            // compute truth tables
+    int                fFilter;           // filter dominated cuts
+    int                fSeq;              // compute sequential cuts
+    int                fDrop;             // drop cuts on the fly
+    int                fMulti;            // compute cuts in multi-input AND gate graph
+    int                fRecord;           // record the cut computation flow
+    int                fVerbose;          // the verbosiness flag
 };
 
 struct Cut_CutStruct_t_
 {
-    unsigned           uTruth     : 16;   // truth table for 4-input cuts
-    unsigned           uPhase     :  6;   // the phase when mapping into a canonical form
+    unsigned           Num0       : 11;   // temporary number
+    unsigned           Num1       : 11;   // temporary number
     unsigned           fSimul     :  1;   // the value of cut's output at 000.. pattern
     unsigned           fCompl     :  1;   // the cut is complemented
     unsigned           nVarsMax   :  4;   // the max number of vars [4-6]
@@ -64,15 +72,13 @@ struct Cut_CutStruct_t_
     int                pLeaves[0];        // the array of leaves
 };
 
-static inline unsigned * Cut_CutReadTruth( Cut_Cut_t * p )     {  if ( p->nVarsMax == 4 )  return (unsigned *)p;  return (unsigned *)(p->pLeaves + p->nVarsMax); }
-static inline unsigned   Cut_CutReadPhase( Cut_Cut_t * p )     {  return p->uPhase;    }
 static inline int        Cut_CutReadLeaveNum( Cut_Cut_t * p )  {  return p->nLeaves;   }
 static inline int *      Cut_CutReadLeaves( Cut_Cut_t * p )    {  return p->pLeaves;   }
-
+static inline unsigned * Cut_CutReadTruth( Cut_Cut_t * p )     {  return (unsigned *)(p->pLeaves + p->nVarsMax); }
 static inline void       Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth )  { 
-    if ( p->nVarsMax == 4 )  { p->uTruth = *puTruth;  return; }
-    p->pLeaves[p->nVarsMax] = (int)puTruth[0];
-    if ( p->nVarsMax == 6 )  p->pLeaves[p->nVarsMax + 1] = (int)puTruth[1];
+    int i;
+    for ( i = (p->nVarsMax <= 5) ? 0 : ((1 << (p->nVarsMax - 5)) - 1); i >= 0; i-- )
+        p->pLeaves[p->nVarsMax + i] = (int)puTruth[i];
 }
 
 ////////////////////////////////////////////////////////////////////////
@@ -104,14 +110,21 @@ extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName
 extern void             Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
 extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
 /*=== cutNode.c ==========================================================*/
-extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fNew0, int fNew1, int fTriv ); 
-extern Cut_Cut_t *      Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fNew0, int fNew1, int fTriv ); 
+extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv ); 
 extern Cut_Cut_t *      Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
 /*=== cutSeq.c ==========================================================*/
 extern void             Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int nLat0, int nLat1, int fTriv, int CutSetNum );
 extern void             Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node );
 extern int              Cut_NodeTempTransferToNew( Cut_Man_t * p, int Node, int CutSetNum );
 extern void             Cut_NodeOldTransferToNew( Cut_Man_t * p, int Node );
+/*=== cutOracle.c ==========================================================*/
+extern Cut_Oracle_t *   Cut_OracleStart( Cut_Man_t * pMan );
+extern void             Cut_OracleStop( Cut_Oracle_t * p );
+extern void             Cut_OracleSetFanoutCounts( Cut_Oracle_t * p, Vec_Int_t * vFanCounts );
+extern int              Cut_OracleReadDrop( Cut_Oracle_t * p );
+extern void             Cut_OracleNodeSetTriv( Cut_Oracle_t * p, int Node );
+extern Cut_Cut_t *      Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 );
+extern void             Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutCut.c b/src/opt/cut/cutCut.c
index 95916960..2039f0c4 100644
--- a/src/opt/cut/cutCut.c
+++ b/src/opt/cut/cutCut.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "cutInt.h"
-#include "npn.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -31,7 +30,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Start the cut computation.]
+  Synopsis    [Allocates the cut.]
 
   Description []
                
@@ -58,7 +57,7 @@ Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Start the cut computation.]
+  Synopsis    [Recybles the cut.]
 
   Description []
                
@@ -67,29 +66,145 @@ Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
+void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut )
+{
+    p->nCutsDealloc++;
+    p->nCutsCur--;
+    if ( pCut->nLeaves == 1 )
+        p->nCutsTriv--;
+    Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_CutCompare( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 )
+{
+    int i;
+    if ( pCut1->nLeaves < pCut2->nLeaves )
+        return -1;
+    if ( pCut1->nLeaves > pCut2->nLeaves )
+        return 1;
+    for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+    {
+        if ( pCut1->pLeaves[i] < pCut2->pLeaves[i] )
+            return -1;
+        if ( pCut1->pLeaves[i] > pCut2->pLeaves[i] )
+            return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutDupList( Cut_Man_t * p, Cut_Cut_t * pList )
+{
+    Cut_Cut_t * pHead = NULL, ** ppTail = &pHead;
+    Cut_Cut_t * pTemp, * pCopy;
+    if ( pList == NULL )
+        return NULL;
+    Cut_ListForEachCut( pList, pTemp )
+    {
+        pCopy = (Cut_Cut_t *)Extra_MmFixedEntryFetch( p->pMmCuts );
+        memcpy( pCopy, pTemp, p->EntrySize );
+        *ppTail = pCopy;
+        ppTail = &pCopy->pNext;
+    }
+    *ppTail = NULL;
+    return pHead;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CutRecycleList( Cut_Man_t * p, Cut_Cut_t * pList )
+{
+    Cut_Cut_t * pCut, * pCut2;
+    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+        Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of cuts in the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_CutCountList( Cut_Cut_t * pList )
+{
+    int Counter = 0;
+    Cut_ListForEachCut( pList, pList )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two NULL-terminated linked lists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeLists( Cut_Cut_t * pList1, Cut_Cut_t * pList2 )
 {
+    Cut_Cut_t * pList = NULL, ** ppTail = &pList;
     Cut_Cut_t * pCut;
-    if ( p->pParams->fSeq )
-        Node <<= 8;
-    pCut = Cut_CutAlloc( p );
-    pCut->nLeaves    = 1;
-    pCut->pLeaves[0] = Node;
-    pCut->uSign      = Cut_NodeSign( Node );
-    if ( p->pParams->fTruth )
+    while ( pList1 && pList2 )
     {
-        if ( pCut->nVarsMax == 4 )
-            Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
+        if ( Cut_CutCompare(pList1, pList2) < 0 )
+        {
+            pCut = pList1;
+            pList1 = pList1->pNext;
+        }
         else
-            Extra_BitCopy( pCut->nLeaves, p->uTruths[0], (uint8*)Cut_CutReadTruth(pCut) );
+        {
+            pCut = pList2;
+            pList2 = pList2->pNext;
+        }
+        *ppTail = pCut;
+        ppTail = &pCut->pNext;
     }
-    p->nCutsTriv++;
-    return pCut;
-} 
+    *ppTail = pList1? pList1: pList2;
+    return pList;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Start the cut computation.]
+  Synopsis    [Sets the number of the cuts in the list.]
 
   Description []
                
@@ -98,15 +213,51 @@ Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut )
+void Cut_CutNumberList( Cut_Cut_t * pList )
 {
-    p->nCutsDealloc++;
-    p->nCutsCur--;
-    if ( pCut->nLeaves == 1 )
-        p->nCutsTriv--;
-    Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
+    Cut_Cut_t * pCut;
+    int i = 0;
+    Cut_ListForEachCut( pList, pCut )
+        pCut->Num0 = i++;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates the trivial cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
+{
+    Cut_Cut_t * pCut;
+    if ( p->pParams->fSeq )
+        Node <<= CUT_SHIFT;
+    pCut = Cut_CutAlloc( p );
+    pCut->nLeaves    = 1;
+    pCut->pLeaves[0] = Node;
+    pCut->uSign      = Cut_NodeSign( Node );
+    if ( p->pParams->fTruth )
+    {
+/*
+        if ( pCut->nVarsMax == 4 )
+            Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
+        else
+            Extra_BitCopy( pCut->nLeaves, p->uTruths[0], (uint8*)Cut_CutReadTruth(pCut) );
+*/
+        unsigned * pTruth = Cut_CutReadTruth(pCut);
+        int i;
+        for ( i = 0; i < p->nTruthWords; i++ )
+            pTruth[i] = 0xAAAAAAAA;
+    }
+    p->nCutsTriv++;
+    return pCut;
+} 
+
 
 /**Function*************************************************************
 
@@ -128,9 +279,9 @@ void Cut_CutPrint( Cut_Cut_t * pCut, int fSeq )
     {
         if ( fSeq )
         {
-            printf( " %d", pCut->pLeaves[i] >> 8 );
-            if ( pCut->pLeaves[i] & 0xFF )
-                printf( "(%d)", pCut->pLeaves[i] & 0xFF );
+            printf( " %d", pCut->pLeaves[i] >> CUT_SHIFT );
+            if ( pCut->pLeaves[i] & CUT_MASK )
+                printf( "(%d)", pCut->pLeaves[i] & CUT_MASK );
         }
         else
             printf( " %d", pCut->pLeaves[i] );
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index f4178ec8..28068abf 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -29,14 +29,12 @@
 #include "extra.h"
 #include "vec.h"
 #include "cut.h"
+#include "cutList.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#define CUT_SIZE_MAX 8
-#include "cutList.h"
-
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -55,6 +53,7 @@ struct Cut_ManStruct_t_
     // memory management
     Extra_MmFixed_t *  pMmCuts;
     int                EntrySize;
+    int                nTruthWords;
     // temporary variables
     Cut_Cut_t *        pReady;
     Vec_Ptr_t *        vTemp;
@@ -62,12 +61,14 @@ struct Cut_ManStruct_t_
     int                fCompl1;
     int                fSimul;
     int                nNodeCuts;
-    // precomputations
-    uint8              uTruths[8][32];
-    unsigned           uTruthVars[6][2];
-    unsigned short **  pPerms43;
-    unsigned **        pPerms53;
-    unsigned **        pPerms54;
+    Cut_Cut_t *        pStore0[2];
+    Cut_Cut_t *        pStore1[2];
+    Cut_Cut_t *        pCompareOld;
+    Cut_Cut_t *        pCompareNew;
+    // record of the cut computation
+    Vec_Int_t *        vNodeCuts;        // the number of cuts for each node
+    Vec_Int_t *        vNodeStarts;      // the number of the starting cut of each node
+    Vec_Int_t *        vCutPairs;        // the pairs of parent cuts for each cut
     // statistics
     int                nCutsCur;
     int                nCutsMulti;
@@ -108,7 +109,8 @@ struct Cut_ManStruct_t_
 ////////////////////////////////////////////////////////////////////////
 
 // computes signature of the node
-static inline unsigned Cut_NodeSign( int Node )  { return (1 << (Node % 31)); }
+static inline unsigned Cut_NodeSign( int Node )        { return (1 << (Node % 31));                        }
+static inline int      Cut_TruthWords( int nVarsMax )  { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -116,11 +118,20 @@ static inline unsigned Cut_NodeSign( int Node )  { return (1 << (Node % 31)); }
 
 /*=== cutCut.c ==========================================================*/
 extern Cut_Cut_t *         Cut_CutAlloc( Cut_Man_t * p );
-extern Cut_Cut_t *         Cut_CutCreateTriv( Cut_Man_t * p, int Node );
 extern void                Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut );
+extern int                 Cut_CutCompare( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 );
+extern Cut_Cut_t *         Cut_CutDupList( Cut_Man_t * p, Cut_Cut_t * pList );
+extern void                Cut_CutRecycleList( Cut_Man_t * p, Cut_Cut_t * pList );
+extern int                 Cut_CutCountList( Cut_Cut_t * pList );
+extern Cut_Cut_t *         Cut_CutMergeLists( Cut_Cut_t * pList1, Cut_Cut_t * pList2 ); 
+extern void                Cut_CutNumberList( Cut_Cut_t * pList );
+extern Cut_Cut_t *         Cut_CutCreateTriv( Cut_Man_t * p, int Node );
 extern void                Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
 /*=== cutMerge.c ==========================================================*/
 extern Cut_Cut_t *         Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+/*=== cutNode.c ==========================================================*/
+extern void                Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv ); 
+extern int                 Cut_CutListVerify( Cut_Cut_t * pList );
 /*=== cutTable.c ==========================================================*/
 extern Cut_HashTable_t *   Cut_TableStart( int Size );
 extern void                Cut_TableStop( Cut_HashTable_t * pTable );
@@ -128,7 +139,7 @@ extern int                 Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t
 extern void                Cut_TableClear( Cut_HashTable_t * pTable );
 extern int                 Cut_TableReadTime( Cut_HashTable_t * pTable );
 /*=== cutTruth.c ==========================================================*/
-extern void                Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+extern void                Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutList.h b/src/opt/cut/cutList.h
index fd707e6e..ab540908 100644
--- a/src/opt/cut/cutList.h
+++ b/src/opt/cut/cutList.h
@@ -89,7 +89,42 @@ static inline void Cut_ListAdd( Cut_List_t * p, Cut_Cut_t * pCut )
 
 /**Function*************************************************************
 
-  Synopsis    [Adds one cut to the cut list.]
+  Synopsis    [Adds one cut to the cut list while preserving order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cut_ListAdd2( Cut_List_t * p, Cut_Cut_t * pCut )
+{
+    extern int Cut_CutCompare( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 );
+    Cut_Cut_t * pTemp, ** ppSpot;
+    assert( pCut->nLeaves > 0 && pCut->nLeaves <= CUT_SIZE_MAX );
+    if ( p->pHead[pCut->nLeaves] != NULL )
+    {
+        ppSpot = &p->pHead[pCut->nLeaves];
+        for ( pTemp = p->pHead[pCut->nLeaves]; pTemp; pTemp = pTemp->pNext )
+        {
+            if ( Cut_CutCompare(pCut, pTemp) < 0 )
+            {
+                *ppSpot = pCut;
+                pCut->pNext = pTemp;
+                return;
+            }
+            else
+                ppSpot = &pTemp->pNext;
+        }
+    }
+    *p->ppTail[pCut->nLeaves] = pCut;
+    p->ppTail[pCut->nLeaves] = &pCut->pNext;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive the super list from the linked list of cuts.]
 
   Description []
                
@@ -153,7 +188,7 @@ static inline Cut_Cut_t * Cut_ListFinish( Cut_List_t * p )
 {
     Cut_Cut_t * pHead = NULL, ** ppTail = &pHead;
     int i;
-    for ( i = 1; i < CUT_SIZE_MAX; i++ )
+    for ( i = 1; i <= CUT_SIZE_MAX; i++ )
     {
         if ( p->pHead[i] == NULL )
             continue;
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index c9dccb6a..30517d54 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -45,7 +45,7 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
 {
     Cut_Man_t * p;
     int clk = clock();
-    assert( pParams->nVarsMax >= 4 && pParams->nVarsMax <= CUT_SIZE_MAX );
+    assert( pParams->nVarsMax >= 3 && pParams->nVarsMax <= CUT_SIZE_MAX );
     p = ALLOC( Cut_Man_t, 1 );
     memset( p, 0, sizeof(Cut_Man_t) );
     // set and correct parameters
@@ -65,19 +65,28 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
     assert( !pParams->fTruth || pParams->nVarsMax <= 5 );
     // entry size
     p->EntrySize = sizeof(Cut_Cut_t) + pParams->nVarsMax * sizeof(int);
-    if ( pParams->fTruth && pParams->nVarsMax >= 5 && pParams->nVarsMax <= 8 )
-        p->EntrySize += (1 << (pParams->nVarsMax - 5)) * sizeof(unsigned);
+    if ( pParams->fTruth )
+    {
+        if ( pParams->nVarsMax > 8 )
+        {
+            pParams->fTruth = 0;
+            printf( "Skipping computation of truth table for more than 8 inputs.\n" );
+        }
+        else
+        {
+            p->nTruthWords = Cut_TruthWords( pParams->nVarsMax );
+            p->EntrySize += p->nTruthWords * sizeof(unsigned);
+        }
+    }
+    // enable cut computation recording
+    if ( pParams->fRecord )
+    {
+        p->vNodeCuts   = Vec_IntStart( pParams->nIdsMax );
+        p->vNodeStarts = Vec_IntStart( pParams->nIdsMax );
+        p->vCutPairs   = Vec_IntAlloc( 0 );
+    }
     // memory for cuts
     p->pMmCuts = Extra_MmFixedStart( p->EntrySize );
-    // elementary truth tables
-    Npn_StartTruth8( p->uTruths );
-    p->uTruthVars[0][1] = p->uTruthVars[0][0] = 0xAAAAAAAA;    // 1010 1010 1010 1010 1010 1010 1010 1010
-    p->uTruthVars[1][1] = p->uTruthVars[1][0] = 0xCCCCCCCC;    // 1010 1010 1010 1010 1010 1010 1010 1010
-    p->uTruthVars[2][1] = p->uTruthVars[2][0] = 0xF0F0F0F0;    // 1111 0000 1111 0000 1111 0000 1111 0000
-    p->uTruthVars[3][1] = p->uTruthVars[3][0] = 0xFF00FF00;    // 1111 1111 0000 0000 1111 1111 0000 0000
-    p->uTruthVars[4][1] = p->uTruthVars[4][0] = 0xFFFF0000;    // 1111 1111 1111 1111 0000 0000 0000 0000
-    p->uTruthVars[5][0] = 0x00000000;
-    p->uTruthVars[5][1] = 0xFFFFFFFF;
     p->vTemp = Vec_PtrAlloc( 100 );
     return p;
 }
@@ -102,14 +111,16 @@ void Cut_ManStop( Cut_Man_t * p )
         {
             int k = 0;
         }
-    if ( p->vCutsNew )   Vec_PtrFree( p->vCutsNew );
-    if ( p->vCutsOld )   Vec_PtrFree( p->vCutsOld );
-    if ( p->vCutsTemp )  Vec_PtrFree( p->vCutsTemp );
-    if ( p->vFanCounts ) Vec_IntFree( p->vFanCounts );
-    if ( p->pPerms43 )   free( p->pPerms43 );
-    if ( p->pPerms53 )   free( p->pPerms53 );
-    if ( p->pPerms54 )   free( p->pPerms54 );
-    if ( p->vTemp )      Vec_PtrFree( p->vTemp );
+    if ( p->vCutsNew )    Vec_PtrFree( p->vCutsNew );
+    if ( p->vCutsOld )    Vec_PtrFree( p->vCutsOld );
+    if ( p->vCutsTemp )   Vec_PtrFree( p->vCutsTemp );
+    if ( p->vFanCounts )  Vec_IntFree( p->vFanCounts );
+    if ( p->vTemp )       Vec_PtrFree( p->vTemp );
+
+    if ( p->vNodeCuts )   Vec_IntFree( p->vNodeCuts );
+    if ( p->vNodeStarts ) Vec_IntFree( p->vNodeStarts );
+    if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
+
     Extra_MmFixedStop( p->pMmCuts, 0 );
     free( p );
 }
@@ -146,8 +157,9 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     PRT( "Union ", p->timeUnion );
     PRT( "Filter", p->timeFilter );
     PRT( "Truth ", p->timeTruth );
-    printf( "Nodes = %d. Multi = %d.  Cuts = %d. Multi = %d.\n", 
-        p->nNodes, p->nNodesMulti, p->nCutsCur-p->nCutsTriv, p->nCutsMulti );
+//    printf( "Nodes = %d. Multi = %d.  Cuts = %d. Multi = %d.\n", 
+//        p->nNodes, p->nNodesMulti, p->nCutsCur-p->nCutsTriv, p->nCutsMulti );
+//    printf( "Count0 = %d. Count1 = %d. Count2 = %d.\n\n", p->Count0, p->Count1, p->Count2 );
 }
 
     
diff --git a/src/opt/cut/cutMerge.c b/src/opt/cut/cutMerge.c
index f9c059bf..a38d1cef 100644
--- a/src/opt/cut/cutMerge.c
+++ b/src/opt/cut/cutMerge.c
@@ -526,7 +526,7 @@ Cut_Cut_t * Cut_CutMergeTwo5( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut
                     return NULL;
             }
             pRes = Cut_CutAlloc( p );
-            pRes->uTruth = (uSign1 << 8);
+            pRes->Num1 = uSign1;
         }
         for ( i = 0; i < (int)pCut0->nLeaves; i++ )
             pRes->pLeaves[i] = pCut0->pLeaves[i];
@@ -645,7 +645,8 @@ Cut_Cut_t * Cut_CutMergeTwo5( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut
     }
     assert( Count == nNodes );
     pRes->nLeaves = nNodes;
-    pRes->uTruth = (uSign1 << 8) | uSign0;
+    pRes->Num1 = uSign1;
+    pRes->Num0 = uSign0;
     return pRes;
 }
 
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 0d0ac04c..672463b4 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -189,9 +189,6 @@ static inline int Cut_CutFilterOld( Cut_Man_t * p, Cut_Cut_t * pList, Cut_Cut_t
 {
     Cut_Cut_t * pPrev, * pTemp, * pTemp2, ** ppTail;
 
-    if ( pList == NULL )
-        return 0;
-
     // check if this cut is filtered out by smaller cuts
     pPrev = NULL;
     Cut_ListForEachCut( pList, pTemp )
@@ -250,7 +247,7 @@ static inline int Cut_CutFilterOld( Cut_Man_t * p, Cut_Cut_t * pList, Cut_Cut_t
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
+static inline int Cut_CutProcessTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
 {
     Cut_Cut_t * pCut;
     // merge the cuts
@@ -260,13 +257,11 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0,
         pCut = Cut_CutMergeTwo( p, pCut1, pCut0 );
     if ( pCut == NULL )
         return 0;
-//    if ( Root == 5 && (pCut->pLeaves[0] >> 8) == 1 && (pCut->pLeaves[1] >> 8) == 4 && (pCut->pLeaves[2] >> 8) == 6 )
-//    {
-//        int x = 0;
-//    }
     assert( p->pParams->fSeq || pCut->nLeaves > 1 );
     // set the signature
     pCut->uSign = pCut0->uSign | pCut1->uSign;
+    if ( p->pParams->fRecord )
+        pCut->Num0 = pCut0->Num0, pCut->Num1 = pCut1->Num0;
     // check containment
     if ( p->pParams->fFilter )
     {
@@ -274,15 +269,15 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0,
             return 0;
         if ( p->pParams->fSeq )
         {
-            if ( Cut_CutFilterOld(p, Cut_NodeReadCutsOld(p, Root), pCut) )
+            if ( p->pCompareOld && Cut_CutFilterOld(p, p->pCompareOld, pCut) )
                 return 0;
-            if ( Cut_CutFilterOld(p, Cut_NodeReadCutsNew(p, Root), pCut) )
+            if ( p->pCompareNew && Cut_CutFilterOld(p, p->pCompareNew, pCut) )
                 return 0;
         }
     }
     // compute the truth table
     if ( p->pParams->fTruth )
-        Cut_TruthCompute( p, pCut, pCut0, pCut1 );
+        Cut_TruthCompute( pCut, pCut0, pCut1, p->fCompl0, p->fCompl1 );
     // add to the list
     Cut_ListAdd( pSuperList, pCut );
     // return status (0 if okay; 1 if exceeded the limit)
@@ -300,16 +295,36 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0,
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fNew0, int fNew1, int fTriv )
+Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv )
 {
-    Cut_Cut_t * pList;
-    int clk = clock();
+    Cut_List_t Super, * pSuper = &Super;
+    Cut_Cut_t * pList, * pCut;
+    int clk;
     // start the number of cuts at the node
     p->nNodes++;
     p->nNodeCuts = 0;
+    // prepare information for recording
+    if ( p->pParams->fRecord )
+    {
+        Cut_CutNumberList( Cut_NodeReadCutsNew(p, Node0) );
+        Cut_CutNumberList( Cut_NodeReadCutsNew(p, Node1) );
+    }
     // compute the cuts
-    pList = Cut_NodeDoComputeCuts( p, Node, Node0, Node1, fCompl0, fCompl1, fNew0, fNew1, fTriv );
+clk = clock();
+    Cut_ListStart( pSuper );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, Cut_NodeReadCutsNew(p, Node0), Cut_NodeReadCutsNew(p, Node1), fTriv );
+    pList = Cut_ListFinish( pSuper );
 p->timeMerge += clock() - clk;
+    // verify the result of cut computation
+//    Cut_CutListVerify( pList );
+    // performing the recording
+    if ( p->pParams->fRecord )
+    {
+        Vec_IntWriteEntry( p->vNodeStarts, Node, Vec_IntSize(p->vCutPairs) );
+        Cut_ListForEachCut( pList, pCut )
+            Vec_IntPush( p->vCutPairs, ((pCut->Num1 << 16) | pCut->Num0) );
+        Vec_IntWriteEntry( p->vNodeCuts, Node, Vec_IntSize(p->vCutPairs) - Vec_IntEntry(p->vNodeStarts, Node) );
+    }
     // check if the node is over the list
     if ( p->nNodeCuts == p->pParams->nKeepMax )
         p->nCutsLimit++;
@@ -336,20 +351,15 @@ p->timeMerge += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fNew0, int fNew1, int fTriv )
+void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv )
 {
-    Cut_List_t SuperList;
-    Cut_Cut_t * pList0, * pList1, * pStop0, * pStop1, * pTemp0, * pTemp1;
+    Cut_Cut_t * pStop0, * pStop1, * pTemp0, * pTemp1;
     int i, nCutsOld, Limit;
-
     // get the cut lists of children
-    pList0 = fNew0 ? Cut_NodeReadCutsNew(p, Node0) : Cut_NodeReadCutsOld(p, Node0);
-    pList1 = fNew1 ? Cut_NodeReadCutsNew(p, Node1) : Cut_NodeReadCutsOld(p, Node1);
     if ( pList0 == NULL || pList1 == NULL )
-        return NULL;
+        return;
     // start the new list
     nCutsOld = p->nCutsCur;
-    Cut_ListStart( &SuperList );
     Limit = p->pParams->nVarsMax;
     // get the simultation bit of the node
     p->fSimul = (fCompl0 ^ pList0->fSimul) & (fCompl1 ^ pList1->fSimul);
@@ -367,23 +377,23 @@ Cut_Cut_t * Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1
     if ( fTriv ) 
     {
         pTemp0 = Cut_CutCreateTriv( p, Node );
-        Cut_ListAdd( &SuperList, pTemp0 );
+        Cut_ListAdd( pSuper, pTemp0 );
         p->nNodeCuts++;
         nCutsOld++;
     }
     // small by small
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
-        if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
-            return Cut_ListFinish( &SuperList );
+        if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
+            return;
     // small by large
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCut( pStop1, pTemp1 )
     {
         if ( (pTemp0->uSign & pTemp1->uSign) != pTemp0->uSign )
             continue;
-        if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
-            return Cut_ListFinish( &SuperList );
+        if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
+            return;
     }
     // small by large
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
@@ -391,8 +401,8 @@ Cut_Cut_t * Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1
     {
         if ( (pTemp0->uSign & pTemp1->uSign) != pTemp1->uSign )
             continue;
-        if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
-            return Cut_ListFinish( &SuperList );
+        if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
+            return;
     }
     // large by large
     Cut_ListForEachCut( pStop0, pTemp0 )
@@ -406,15 +416,14 @@ Cut_Cut_t * Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1
                 break;
         if ( i < Limit )
             continue;
-        if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
-            return Cut_ListFinish( &SuperList );
+        if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
+            return;
     } 
     if ( fTriv ) 
     {
         p->nCutsMulti += p->nCutsCur - nCutsOld;         
         p->nNodesMulti++;
     }
-    return Cut_ListFinish( &SuperList );
 }
 
 /**Function*************************************************************
@@ -430,15 +439,13 @@ Cut_Cut_t * Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1
 ***********************************************************************/
 Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
 {
-    Cut_List_t SuperList;
+    Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop;
     int i, k, Node, Root, Limit = p->pParams->nVarsMax;
     int clk = clock();
 
-    assert( p->pParams->nVarsMax <= 6 );
-
     // start the new list
-    Cut_ListStart( &SuperList );
+    Cut_ListStart( pSuper );
 
     // remember the root node to save the resulting cuts
     Root = Vec_IntEntry( vNodes, 0 );
@@ -457,7 +464,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
         pList->pNext = NULL;
         // save or recycle the elementary cut
         if ( i == 0 )
-            Cut_ListAdd( &SuperList, pList ), pTop = pList;
+            Cut_ListAdd( pSuper, pList ), pTop = pList;
         else
             Cut_CutRecycle( p, pList );
         // save all the cuts that are smaller than the limit
@@ -469,14 +476,14 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
                 break;
             }
             // check containment
-            if ( p->pParams->fFilter && Cut_CutFilterOne( p, &SuperList, pCut ) )
+            if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) )
                 continue;
             // set the complemented bit by comparing the first cut with the current cut
             pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
             pListStart = pCut->pNext;
             pCut->pNext = NULL;
             // add to the list
-            Cut_ListAdd( &SuperList, pCut );
+            Cut_ListAdd( pSuper, pCut );
             if ( ++p->nNodeCuts == p->pParams->nKeepMax )
             {
                 // recycle the rest of the cuts of this node
@@ -499,14 +506,14 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
         Cut_ListForEachCutSafe( pList, pCut, pCut2 )
         {
             // check containment
-            if ( p->pParams->fFilter && Cut_CutFilterOne( p, &SuperList, pCut ) )
+            if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) )
                 continue;
             // set the complemented bit
             pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
             pListStart = pCut->pNext;
             pCut->pNext = NULL;
             // add to the list
-            Cut_ListAdd( &SuperList, pCut );
+            Cut_ListAdd( pSuper, pCut );
             if ( ++p->nNodeCuts == p->pParams->nKeepMax )
             {
                 // recycle the rest of the cuts
@@ -523,7 +530,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
 finish :
     // set the cuts at the node
     assert( Cut_NodeReadCutsNew(p, Root) == NULL );
-    pList = Cut_ListFinish( &SuperList );
+    pList = Cut_ListFinish( pSuper );
     Cut_NodeWriteCutsNew( p, Root, pList );
 p->timeUnion += clock() - clk;
     // filter the cuts
@@ -536,6 +543,38 @@ p->timeUnion += clock() - clk;
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Verifies that the list contains only non-dominated cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_CutListVerify( Cut_Cut_t * pList )
+{ 
+    Cut_Cut_t * pCut, * pDom;
+    Cut_ListForEachCut( pList, pCut )
+    {
+        Cut_ListForEachCutStop( pList, pDom, pCut )
+        {
+            if ( Cut_CutCheckDominance( pDom, pCut ) )
+            {
+                int x = 0;
+                printf( "******************* These are contained cuts:\n" );
+                Cut_CutPrint( pDom, 1 );
+                Cut_CutPrint( pDom, 1 );
+                
+                return 0;
+            }
+        }
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/cut/cutOracle.c b/src/opt/cut/cutOracle.c
new file mode 100644
index 00000000..a254fd96
--- /dev/null
+++ b/src/opt/cut/cutOracle.c
@@ -0,0 +1,428 @@
+/**CFile****************************************************************
+
+  FileName    [cutOracle.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Procedures to compute cuts for a node using the oracle.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutOracle.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Cut_OracleStruct_t_
+{
+    // cut comptupatation parameters
+    Cut_Params_t *     pParams;
+    Vec_Int_t *        vFanCounts;
+    int                fSimul;
+    // storage for cuts
+    Vec_Ptr_t *        vCutsNew;
+    Vec_Ptr_t *        vCuts0;
+    Vec_Ptr_t *        vCuts1;
+    // oracle info 
+    Vec_Int_t *        vNodeCuts;
+    Vec_Int_t *        vNodeStarts;
+    Vec_Int_t *        vCutPairs;
+    // memory management
+    Extra_MmFixed_t *  pMmCuts;
+    int                EntrySize;
+    int                nTruthWords;
+    // stats
+    int                timeTotal;
+    int                nCuts;
+    int                nCutsTriv;
+};
+
+static Cut_Cut_t * Cut_CutStart( Cut_Oracle_t * p );
+static Cut_Cut_t * Cut_CutTriv( Cut_Oracle_t * p, int Node );
+static Cut_Cut_t * Cut_CutMerge( Cut_Oracle_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut oracle.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Oracle_t * Cut_OracleStart( Cut_Man_t * pMan )
+{
+    Cut_Oracle_t * p;
+    int clk = clock();
+
+    assert( pMan->pParams->nVarsMax >= 3 && pMan->pParams->nVarsMax <= CUT_SIZE_MAX );
+    assert( pMan->pParams->fRecord );
+
+    p = ALLOC( Cut_Oracle_t, 1 );
+    memset( p, 0, sizeof(Cut_Oracle_t) );
+
+    // set and correct parameters
+    p->pParams     = pMan->pParams;
+
+    // transfer the recording info
+    p->vNodeCuts   = pMan->vNodeCuts;    pMan->vNodeCuts   = NULL;
+    p->vNodeStarts = pMan->vNodeStarts;  pMan->vNodeStarts = NULL;
+    p->vCutPairs   = pMan->vCutPairs;    pMan->vCutPairs   = NULL;
+
+    // prepare storage for cuts
+    p->vCutsNew = Vec_PtrAlloc( p->pParams->nIdsMax );
+    Vec_PtrFill( p->vCutsNew, p->pParams->nIdsMax, NULL );
+    p->vCuts0 = Vec_PtrAlloc( 100 );
+    p->vCuts1 = Vec_PtrAlloc( 100 );
+
+    // entry size
+    p->EntrySize = sizeof(Cut_Cut_t) + p->pParams->nVarsMax * sizeof(int);
+    if ( p->pParams->fTruth )
+    {
+        if ( p->pParams->nVarsMax > 8 )
+        {
+            p->pParams->fTruth = 0;
+            printf( "Skipping computation of truth table for more than 8 inputs.\n" );
+        }
+        else
+        {
+            p->nTruthWords = Cut_TruthWords( p->pParams->nVarsMax );
+            p->EntrySize += p->nTruthWords * sizeof(unsigned);
+        }
+    }
+    // memory for cuts
+    p->pMmCuts = Extra_MmFixedStart( p->EntrySize );
+    return p;
+}
+/**Function*************************************************************
+
+  Synopsis    [Stop the cut oracle.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_OracleStop( Cut_Oracle_t * p )
+{
+    Cut_Cut_t * pCut;
+    int i;
+
+//    if ( p->pParams->fVerbose )
+    {
+        printf( "Cut computation statistics with oracle:\n" );
+        printf( "Current cuts      = %8d. (Trivial = %d.)\n", p->nCuts-p->nCutsTriv, p->nCutsTriv );
+        PRT( "Total time ", p->timeTotal );
+    }
+
+    Vec_PtrForEachEntry( p->vCutsNew, pCut, i )
+        if ( pCut != NULL )
+        {
+            int k = 0;
+        }
+    if ( p->vCuts0 )      Vec_PtrFree( p->vCuts0 );
+    if ( p->vCuts1 )      Vec_PtrFree( p->vCuts1 );
+    if ( p->vCutsNew )    Vec_PtrFree( p->vCutsNew );
+    if ( p->vFanCounts )  Vec_IntFree( p->vFanCounts );
+
+    if ( p->vNodeCuts )   Vec_IntFree( p->vNodeCuts );
+    if ( p->vNodeStarts ) Vec_IntFree( p->vNodeStarts );
+    if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
+
+    Extra_MmFixedStop( p->pMmCuts, 0 );
+    free( p ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_OracleSetFanoutCounts( Cut_Oracle_t * p, Vec_Int_t * vFanCounts )
+{
+    p->vFanCounts = vFanCounts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_OracleReadDrop( Cut_Oracle_t * p )
+{
+    return p->pParams->fDrop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the trivial cut for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_OracleNodeSetTriv( Cut_Oracle_t * p, int Node )
+{
+    assert( Vec_PtrEntry( p->vCutsNew, Node ) == NULL );
+    Vec_PtrWriteEntry( p->vCutsNew, Node, Cut_CutTriv(p, Node) );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutStart( Cut_Oracle_t * p )
+{
+    Cut_Cut_t * pCut;
+    // cut allocation
+    pCut = (Cut_Cut_t *)Extra_MmFixedEntryFetch( p->pMmCuts );
+    memset( pCut, 0, sizeof(Cut_Cut_t) );
+    pCut->nVarsMax   = p->pParams->nVarsMax;
+    pCut->fSimul     = p->fSimul;
+    p->nCuts++;
+    return pCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the trivial cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutTriv( Cut_Oracle_t * p, int Node )
+{
+    Cut_Cut_t * pCut;
+    pCut = Cut_CutStart( p );
+    pCut->nLeaves    = 1;
+    pCut->pLeaves[0] = Node;
+    if ( p->pParams->fTruth )
+    {
+        unsigned * pTruth = Cut_CutReadTruth(pCut);
+        int i;
+        for ( i = 0; i < p->nTruthWords; i++ )
+            pTruth[i] = 0xAAAAAAAA;
+    }
+    p->nCutsTriv++;
+    return pCut;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMerge( Cut_Oracle_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+    Cut_Cut_t * pCut;
+    int Limit, i, k, c;
+    // create the leaves of the new cut
+    pCut = Cut_CutStart( p );
+    Limit = p->pParams->nVarsMax;
+    for ( i = k = c = 0; c < Limit; c++ )
+    {
+        if ( k == (int)pCut1->nLeaves )
+        {
+            if ( i == (int)pCut0->nLeaves )
+            {
+                pCut->nLeaves = c;
+                return pCut;
+            }
+            pCut->pLeaves[c] = pCut0->pLeaves[i++];
+            continue;
+        }
+        if ( i == (int)pCut0->nLeaves )
+        {
+            if ( k == (int)pCut1->nLeaves )
+            {
+                pCut->nLeaves = c;
+                return pCut;
+            }
+            pCut->pLeaves[c] = pCut1->pLeaves[k++];
+            continue;
+        }
+        if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] )
+        {
+            pCut->pLeaves[c] = pCut0->pLeaves[i++];
+            continue;
+        }
+        if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] )
+        {
+            pCut->pLeaves[c] = pCut1->pLeaves[k++];
+            continue;
+        }
+        pCut->pLeaves[c] = pCut0->pLeaves[i++]; 
+        k++;
+    }
+    assert( i == (int)pCut0->nLeaves && k == (int)pCut1->nLeaves );
+    pCut->nLeaves = c;
+    return pCut;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstruct the cuts of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 )
+{
+    Cut_Cut_t * pList = NULL, ** ppTail = &pList;
+    Cut_Cut_t * pCut, * pCut0, * pCut1, * pList0, * pList1;
+    int iCutStart, nCuts, i, Entry;
+    int clk = clock();
+
+    // get the cuts of the children
+    pList0 = Vec_PtrEntry( p->vCutsNew, Node0 );
+    pList1 = Vec_PtrEntry( p->vCutsNew, Node1 );
+    assert( pList0 && pList1 );
+
+    // get the complemented attribute of the cut
+    p->fSimul = (fCompl0 ^ pList0->fSimul) & (fCompl1 ^ pList1->fSimul);
+
+    // collect the cuts
+    Vec_PtrClear( p->vCuts0 );
+    Cut_ListForEachCut( pList0, pCut )
+        Vec_PtrPush( p->vCuts0, pCut );
+    Vec_PtrClear( p->vCuts1 );
+    Cut_ListForEachCut( pList1, pCut )
+        Vec_PtrPush( p->vCuts1, pCut );
+
+    // get the first and last cuts of this node
+    nCuts = Vec_IntEntry(p->vNodeCuts, Node);
+    iCutStart = Vec_IntEntry(p->vNodeStarts, Node);
+
+    // create trivial cut
+    assert( Vec_IntEntry(p->vCutPairs, iCutStart) == 0 );
+    pCut = Cut_CutTriv( p, Node );
+    *ppTail = pCut;
+    ppTail = &pCut->pNext;
+    // create other cuts
+    for ( i = 1; i < nCuts; i++ )
+    {
+        Entry = Vec_IntEntry( p->vCutPairs, iCutStart + i );
+        pCut0 = Vec_PtrEntry( p->vCuts0, Entry & 0xFFFF );
+        pCut1 = Vec_PtrEntry( p->vCuts1, Entry >> 16 );
+        pCut  = Cut_CutMerge( p, pCut0, pCut1 );
+        *ppTail = pCut;
+        ppTail = &pCut->pNext;
+        // compute the truth table
+        if ( p->pParams->fTruth )
+            Cut_TruthCompute( pCut, pCut0, pCut1, fCompl0, fCompl1 );
+    }
+    *ppTail = NULL;
+
+    // write the new cut
+    assert( Vec_PtrEntry( p->vCutsNew, Node ) == NULL );
+    Vec_PtrWriteEntry( p->vCutsNew, Node, pList );
+p->timeTotal += clock() - clk;
+    return pList;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the cuts at the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_OracleFreeCuts( Cut_Oracle_t * p, int Node )
+{
+    Cut_Cut_t * pList, * pCut, * pCut2;
+    pList = Vec_PtrEntry( p->vCutsNew, Node );
+    if ( pList == NULL )
+        return;
+    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+        Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
+    Vec_PtrWriteEntry( p->vCutsNew, Node, pList );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Consider dropping cuts if they are useless by now.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node )
+{
+    int nFanouts;
+    assert( p->vFanCounts );
+    nFanouts = Vec_IntEntry( p->vFanCounts, Node );
+    assert( nFanouts > 0 );
+    if ( --nFanouts == 0 )
+        Cut_OracleFreeCuts( p, Node );
+    Vec_IntWriteEntry( p->vFanCounts, Node, nFanouts );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutSeq.c b/src/opt/cut/cutSeq.c
index a1887608..001d3e01 100644
--- a/src/opt/cut/cutSeq.c
+++ b/src/opt/cut/cutSeq.c
@@ -24,16 +24,13 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Cut_NodeShiftLat( Cut_Man_t * p, int Node, int nLat );
-static int  Cut_ListCount( Cut_Cut_t * pList );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Computes sequential cuts for the node from its fanins.]
+  Synopsis    [Shifts all cut leaves of the node by the given number of latches.]
 
   Description []
                
@@ -42,44 +39,99 @@ static int  Cut_ListCount( Cut_Cut_t * pList );
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int nLat0, int nLat1, int fTriv, int CutSetNum )
+static inline void Cut_NodeShiftCutLeaves( Cut_Cut_t * pList, int nLat )
 {
-    Cut_List_t List1, List2, List3;
-    Cut_Cut_t * pList1, * pList2, * pList3, * pListNew;
-    int clk = clock();
+    Cut_Cut_t * pTemp;
+    int i;
+    // shift the cuts by as many latches
+    Cut_ListForEachCut( pList, pTemp )
+    {
+        pTemp->uSign = 0;
+        for ( i = 0; i < (int)pTemp->nLeaves; i++ )
+        {
+            pTemp->pLeaves[i] += nLat;
+            pTemp->uSign      |= Cut_NodeSign( pTemp->pLeaves[i] );
+        }
+    }
+}
+
+/**Function*************************************************************
 
-//    assert( Node != Node0 );
-//    assert( Node != Node1 );
+  Synopsis    [Computes sequential cuts for the node from its fanins.]
+
+  Description []
+               
+  SideEffects []
 
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int nLat0, int nLat1, int fTriv, int CutSetNum )
+{
+    Cut_List_t Super, * pSuper = &Super;
+    Cut_Cut_t * pListNew;
+    int clk;
+    
     // get the number of cuts at the node
-    p->nNodeCuts = Cut_ListCount( Cut_NodeReadCutsOld(p, Node) );
+    p->nNodeCuts = Cut_CutCountList( Cut_NodeReadCutsOld(p, Node) );
     if ( p->nNodeCuts >= p->pParams->nKeepMax )
         return;
+
     // count only the first visit
     if ( p->nNodeCuts == 0 )
         p->nNodes++;
 
-    // shift the cuts by as many latches
-    if ( nLat0 ) Cut_NodeShiftLat( p, Node0, nLat0 );
-    if ( nLat1 ) Cut_NodeShiftLat( p, Node1, nLat1 );
-
-    // merge the old and new
-    pList1 = Cut_NodeDoComputeCuts( p, Node, Node0, Node1, fCompl0, fCompl1, 0, 1, 0 );
-    // merge the new and old
-    pList2 = Cut_NodeDoComputeCuts( p, Node, Node0, Node1, fCompl0, fCompl1, 1, 0, 0 );
-    // merge the new and new
-    pList3 = Cut_NodeDoComputeCuts( p, Node, Node0, Node1, fCompl0, fCompl1, 1, 1, fTriv );
+    // store the fanin lists
+    p->pStore0[0] = Cut_NodeReadCutsOld( p, Node0 );
+    p->pStore0[1] = Cut_NodeReadCutsNew( p, Node0 );
+    p->pStore1[0] = Cut_NodeReadCutsOld( p, Node1 );
+    p->pStore1[1] = Cut_NodeReadCutsNew( p, Node1 );
+
+    // duplicate the cut lists if fanin nodes are non-standard
+    if ( Node == Node0 || Node == Node1 || Node0 == Node1 )
+    {
+        p->pStore0[0] = Cut_CutDupList( p, p->pStore0[0] );
+        p->pStore0[1] = Cut_CutDupList( p, p->pStore0[1] );
+        p->pStore1[0] = Cut_CutDupList( p, p->pStore1[0] );
+        p->pStore1[1] = Cut_CutDupList( p, p->pStore1[1] );
+    }
+
+    // shift the cuts by as many latches and recompute signatures
+    if ( nLat0 ) Cut_NodeShiftCutLeaves( p->pStore0[0], nLat0 );
+    if ( nLat0 ) Cut_NodeShiftCutLeaves( p->pStore0[1], nLat0 );
+    if ( nLat1 ) Cut_NodeShiftCutLeaves( p->pStore1[0], nLat1 );
+    if ( nLat1 ) Cut_NodeShiftCutLeaves( p->pStore1[1], nLat1 );
+
+    // store the original lists for comparison
+    p->pCompareOld = Cut_NodeReadCutsOld( p, Node );
+    p->pCompareNew = Cut_NodeReadCutsNew( p, Node );
+
+    // merge the old and the new
+clk = clock();
+    Cut_ListStart( pSuper );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[0], p->pStore1[1], 0 );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[0], 0 );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[1], fTriv );
+    pListNew = Cut_ListFinish( pSuper );
 p->timeMerge += clock() - clk;
 
-    // merge all lists
-    Cut_ListDerive( &List1, pList1 );
-    Cut_ListDerive( &List2, pList2 );
-    Cut_ListDerive( &List3, pList3 );
-    Cut_ListAddList( &List1, &List2 );
-    Cut_ListAddList( &List1, &List3 );
+    // shift the cuts by as many latches and recompute signatures
+    if ( Node == Node0 || Node == Node1 || Node0 == Node1 )
+    {
+        Cut_CutRecycleList( p, p->pStore0[0] );
+        Cut_CutRecycleList( p, p->pStore0[1] );
+        Cut_CutRecycleList( p, p->pStore1[0] );
+        Cut_CutRecycleList( p, p->pStore1[1] );
+    }
+    else
+    {
+        if ( nLat0 ) Cut_NodeShiftCutLeaves( p->pStore0[0], -nLat0 );
+        if ( nLat0 ) Cut_NodeShiftCutLeaves( p->pStore0[1], -nLat0 );
+        if ( nLat1 ) Cut_NodeShiftCutLeaves( p->pStore1[0], -nLat1 );
+        if ( nLat1 ) Cut_NodeShiftCutLeaves( p->pStore1[1], -nLat1 );
+    }
 
     // set the lists at the node
-    pListNew = Cut_ListFinish( &List1 );
     if ( CutSetNum >= 0 )
     {
         assert( Cut_NodeReadCutsTemp(p, CutSetNum) == NULL );
@@ -91,17 +143,14 @@ p->timeMerge += clock() - clk;
         Cut_NodeWriteCutsNew( p, Node, pListNew );
     }
 
-    // shift the cuts by as many latches back
-    if ( nLat0 ) Cut_NodeShiftLat( p, Node0, -nLat0 );
-    if ( nLat1 ) Cut_NodeShiftLat( p, Node1, -nLat1 );
-
+    // mark the node if we exceeded the number of cuts
     if ( p->nNodeCuts >= p->pParams->nKeepMax )
         p->nCutsLimit++;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Merges the new cuts with the old cuts.]
 
   Description []
                
@@ -112,8 +161,7 @@ p->timeMerge += clock() - clk;
 ***********************************************************************/
 void Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node )
 {
-    Cut_List_t Old, New;
-    Cut_Cut_t * pListOld, * pListNew;
+    Cut_Cut_t * pListOld, * pListNew, * pList;
     // get the new cuts
     pListNew = Cut_NodeReadCutsNew( p, Node );
     if ( pListNew == NULL )
@@ -127,19 +175,16 @@ void Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node )
         return;
     }
     // merge the lists
-    Cut_ListDerive( &Old, pListOld );
-    Cut_ListDerive( &New, pListNew );
-    Cut_ListAddList( &Old, &New );
-    pListOld = Cut_ListFinish( &Old );
-    Cut_NodeWriteCutsOld( p, Node, pListOld );
+    pList = Cut_CutMergeLists( pListOld, pListNew );
+    Cut_NodeWriteCutsOld( p, Node, pList );
 }
 
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if something was transferred.]
+  Synopsis    [Transfers the temporary cuts to be the new cuts.]
 
-  Description []
+  Description [Returns 1 if something was transferred.]
                
   SideEffects []
 
@@ -148,16 +193,16 @@ void Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node )
 ***********************************************************************/
 int Cut_NodeTempTransferToNew( Cut_Man_t * p, int Node, int CutSetNum )
 {
-    Cut_Cut_t * pCut;
-    pCut = Cut_NodeReadCutsTemp( p, CutSetNum );
+    Cut_Cut_t * pList;
+    pList = Cut_NodeReadCutsTemp( p, CutSetNum );
     Cut_NodeWriteCutsTemp( p, CutSetNum, NULL );
-    Cut_NodeWriteCutsNew( p, Node, pCut );
-    return pCut != NULL;
+    Cut_NodeWriteCutsNew( p, Node, pList );
+    return pList != NULL;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if something was transferred.]
+  Synopsis    [Transfers the old cuts to be the new cuts.]
 
   Description []
                
@@ -168,66 +213,11 @@ int Cut_NodeTempTransferToNew( Cut_Man_t * p, int Node, int CutSetNum )
 ***********************************************************************/
 void Cut_NodeOldTransferToNew( Cut_Man_t * p, int Node )
 {
-    Cut_Cut_t * pCut;
-    pCut = Cut_NodeReadCutsOld( p, Node );
+    Cut_Cut_t * pList;
+    pList = Cut_NodeReadCutsOld( p, Node );
     Cut_NodeWriteCutsOld( p, Node, NULL );
-    Cut_NodeWriteCutsNew( p, Node, pCut );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_NodeShiftLat( Cut_Man_t * p, int Node, int nLat )
-{
-    Cut_Cut_t * pTemp;
-    int i;
-    // shift the cuts by as many latches
-    Cut_ListForEachCut( Cut_NodeReadCutsOld(p, Node), pTemp )
-    {
-        pTemp->uSign = 0;
-        for ( i = 0; i < (int)pTemp->nLeaves; i++ )
-        {
-            pTemp->pLeaves[i] += nLat;
-            pTemp->uSign      |= Cut_NodeSign( pTemp->pLeaves[i] );
-        }
-    }
-    Cut_ListForEachCut( Cut_NodeReadCutsNew(p, Node), pTemp )
-    {
-        pTemp->uSign = 0;
-        for ( i = 0; i < (int)pTemp->nLeaves; i++ )
-        {
-            pTemp->pLeaves[i] += nLat;
-            pTemp->uSign      |= Cut_NodeSign( pTemp->pLeaves[i] );
-        }
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_ListCount( Cut_Cut_t * pList )
-{
-    int Counter = 0;
-    Cut_ListForEachCut( pList, pList )
-        Counter++;
-    return Counter;
+    Cut_NodeWriteCutsNew( p, Node, pList );
+//    Cut_CutListVerify( pList );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c
index ca09f22c..344884f0 100644
--- a/src/opt/cut/cutTruth.c
+++ b/src/opt/cut/cutTruth.c
@@ -19,16 +19,11 @@
 ***********************************************************************/
 
 #include "cutInt.h"
-#include "npn.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Cut_TruthCompute4( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
-static void Cut_TruthCompute5( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
-static void Cut_TruthCompute6( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -72,340 +67,46 @@ static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-int clk = clock();
-    if ( pCut->nVarsMax == 4 )
-        Cut_TruthCompute4( p, pCut, pCut0, pCut1 );
-    else if ( pCut->nVarsMax == 5 )
-        Cut_TruthCompute5( p, pCut, pCut0, pCut1 );
-    else // if ( pCut->nVarsMax == 6 )
-        Cut_TruthCompute6( p, pCut, pCut0, pCut1 );
-
-//    Npn_VarsTest( pCut->nVarsMax, Cut_CutReadTruth(pCut) );
-p->timeTruth += clock() - clk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs truth table computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TruthCompute4( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-    unsigned * puTruthCut0, * puTruthCut1;
-    unsigned uTruth0, uTruth1, uPhase;
-
-    puTruthCut0 = Cut_CutReadTruth(pCut0);
-    puTruthCut1 = Cut_CutReadTruth(pCut1);
-
-    uPhase  = Cut_TruthPhase( pCut, pCut0 );
-    uTruth0 = Extra_TruthPerm4One( *puTruthCut0, uPhase );
-    uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
-
-    uPhase  = Cut_TruthPhase( pCut, pCut1 );
-    uTruth1 = Extra_TruthPerm4One( *puTruthCut1, uPhase );
-    uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
-
-    uTruth1 = uTruth0 & uTruth1;
-    if ( pCut->fCompl )
-        uTruth1 = ~uTruth1;
-    if ( pCut->nVarsMax == 4 )
-        uTruth1 &= 0xFFFF; 
-    Cut_CutWriteTruth( pCut, &uTruth1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs truth table computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TruthCompute5( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-    unsigned * puTruthCut0, * puTruthCut1;
-    unsigned uTruth0, uTruth1, uPhase;
-
-    puTruthCut0 = Cut_CutReadTruth(pCut0);
-    puTruthCut1 = Cut_CutReadTruth(pCut1);
-
-    uPhase  = Cut_TruthPhase( pCut, pCut0 );
-    uTruth0 = Extra_TruthPerm5One( *puTruthCut0, uPhase );
-    uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
-
-    uPhase  = Cut_TruthPhase( pCut, pCut1 );
-    uTruth1 = Extra_TruthPerm5One( *puTruthCut1, uPhase );
-    uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
-
-    uTruth1 = uTruth0 & uTruth1;
-    if ( pCut->fCompl )
-        uTruth1 = ~uTruth1;
-    Cut_CutWriteTruth( pCut, &uTruth1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs truth table computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TruthCompute6( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 )
 {
-    unsigned * puTruthCut0, * puTruthCut1;
-    unsigned uTruth0[2], uTruth1[2], uPhase;
-
-    puTruthCut0 = Cut_CutReadTruth(pCut0);
-    puTruthCut1 = Cut_CutReadTruth(pCut1);
+    static unsigned uTruth0[8], uTruth1[8];
+    int nTruthWords = Cut_TruthWords( pCut->nVarsMax );
+    unsigned * pTruthRes;
+    int i, uPhase;
 
+    // permute the first table
     uPhase = Cut_TruthPhase( pCut, pCut0 );
-    Extra_TruthPerm6One( puTruthCut0, uPhase, uTruth0 );
-    uTruth0[0] = p->fCompl0? ~uTruth0[0]: uTruth0[0];
-    uTruth0[1] = p->fCompl0? ~uTruth0[1]: uTruth0[1];
-
-    uPhase = Cut_TruthPhase( pCut, pCut1 );
-    Extra_TruthPerm6One( puTruthCut1, uPhase, uTruth1 );
-    uTruth1[0] = p->fCompl1? ~uTruth1[0]: uTruth1[0];
-    uTruth1[1] = p->fCompl1? ~uTruth1[1]: uTruth1[1];
-
-    uTruth1[0] = uTruth0[0] & uTruth1[0];
-    uTruth1[1] = uTruth0[1] & uTruth1[1];
-    if ( pCut->fCompl )
-    {
-        uTruth1[0] = ~uTruth0[0];
-        uTruth1[1] = ~uTruth0[1];
-    }
-    Cut_CutWriteTruth( pCut, uTruth1 );
-}
-
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Performs truth table computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TruthComputeOld( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-    unsigned uTruth0, uTruth1, uPhase;
-    int clk = clock();
-
-    assert( pCut->nVarsMax < 6 );
-
-    // assign the truth table
-    if ( pCut0->nLeaves == pCut->nLeaves )
-        uTruth0 = *Cut_CutReadTruth(pCut0);
-    else
+    Extra_TruthExpand( pCut->nVarsMax, nTruthWords, Cut_CutReadTruth(pCut0), uPhase, uTruth0 );
+    if ( fCompl0 ) 
     {
-        assert( pCut0->nLeaves < pCut->nLeaves );
-        uPhase = Cut_TruthPhase( pCut, pCut0 );
-        if ( pCut->nVarsMax == 4 )
-        {
-            assert( pCut0->nLeaves < 4 );
-            assert( uPhase < 16 );
-            uTruth0 = p->pPerms43[pCut0->uTruth & 0xFF][uPhase];
-        }
-        else
-        {
-            assert( pCut->nVarsMax == 5 );
-            assert( pCut0->nLeaves < 5 );
-            assert( uPhase < 32 );
-            if ( pCut0->nLeaves == 4 )
-            {
-//                Count4++;
-/*
-                if ( uPhase == 31-16 ) // 01111
-                    uTruth0 = pCut0->uTruth;
-                else if ( uPhase == 31-8 ) // 10111
-                    uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][0];
-                else if ( uPhase == 31-4 ) // 11011
-                    uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][1];
-                else if ( uPhase == 31-2 ) // 11101
-                    uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][2];
-                else if ( uPhase == 31-1 ) // 11110
-                    uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][3];
-                else
-                    assert( 0 );
-*/
-                uTruth0 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut0), uPhase );
-            }
-            else
-            {
-//                Count5++;
-//                uTruth0 = p->pPerms53[pCut0->uTruth & 0xFF][uPhase];
-                uTruth0 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut0), uPhase );
-            }
-        }
+        for ( i = 0; i < nTruthWords; i++ )
+            uTruth0[i] = ~uTruth0[i];
     }
-    uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
 
-    // assign the truth table
-    if ( pCut1->nLeaves == pCut->nLeaves )
-        uTruth0 = *Cut_CutReadTruth(pCut1);
-    else
+    // permute the second table
+    uPhase = Cut_TruthPhase( pCut, pCut1 );
+    Extra_TruthExpand( pCut->nVarsMax, nTruthWords, Cut_CutReadTruth(pCut1), uPhase, uTruth1 );
+    if ( fCompl1 ) 
     {
-        assert( pCut1->nLeaves < pCut->nLeaves );
-        uPhase = Cut_TruthPhase( pCut, pCut1 );
-        if ( pCut->nVarsMax == 4 )
-        {
-            assert( pCut1->nLeaves < 4 );
-            assert( uPhase < 16 );
-            uTruth1 = p->pPerms43[pCut1->uTruth & 0xFF][uPhase];
-        }
-        else
-        {
-            assert( pCut->nVarsMax == 5 );
-            assert( pCut1->nLeaves < 5 );
-            assert( uPhase < 32 );
-            if ( pCut1->nLeaves == 4 )
-            {
-//                Count4++;
-/*
-                if ( uPhase == 31-16 ) // 01111
-                    uTruth1 = pCut1->uTruth;
-                else if ( uPhase == 31-8 ) // 10111
-                    uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][0];
-                else if ( uPhase == 31-4 ) // 11011
-                    uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][1];
-                else if ( uPhase == 31-2 ) // 11101
-                    uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][2];
-                else if ( uPhase == 31-1 ) // 11110
-                    uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][3];
-                else
-                    assert( 0 );
-*/
-                uTruth1 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut1), uPhase );
-            }
-            else
-            {
-//                Count5++;
-//                uTruth1 = p->pPerms53[pCut1->uTruth & 0xFF][uPhase];
-                uTruth1 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut1), uPhase );
-            }
-        }
+        for ( i = 0; i < nTruthWords; i++ )
+            uTruth1[i] = ~uTruth1[i];
     }
-    uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
-    uTruth1 = uTruth0 & uTruth1;
-    if ( pCut->fCompl )
-        uTruth1 = ~uTruth1;
-    if ( pCut->nVarsMax == 4 )
-        uTruth1 &= 0xFFFF; 
-    Cut_CutWriteTruth( pCut, &uTruth1 );
-p->timeTruth += clock() - clk;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Expands the truth table according to the phase.]
-
-  Description []
-               
-  SideEffects []
 
-  SeeAlso     []
+    // write the resulting table
+    pTruthRes = Cut_CutReadTruth(pCut);
 
-***********************************************************************/
-void Extra_TruthExpand( int nVars, uint8 * puTruth, unsigned uPhase, uint8 * puTruthR )
-{
-    int i, k, m, m1;
-    assert( nVars <= 8 );
-    Extra_BitClean( nVars, puTruthR );
-    for ( m = (1 << nVars) - 1; m >= 0; m-- )
+    if ( pCut->fCompl )
     {
-        m1 = 0;
-        for ( i = k = 0; i < nVars; i++ )
-            if ( uPhase & (1 << i) )
-            {
-                if ( m & (1 << i) )
-                    m1 |= (1 << k);
-                k++;
-            }
-        if ( Extra_BitRead( puTruth, m1 ) )
-            Extra_BitSet( puTruthR, m );
+        for ( i = 0; i < nTruthWords; i++ )
+            pTruthRes[i] = ~(uTruth0[i] & uTruth1[i]);
     }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs truth table computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TruthCompute1( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-    uint8 uTruth0[32], uTruth1[32];
-    unsigned * puTruthCut0, * puTruthCut1, * puTruthCut;
-    unsigned uPhase;
-int clk = clock();
-
-    assert( pCut->nLeaves >= 2 );
-    assert( pCut->nLeaves <= 8 );
-
-    if ( pCut->nVarsMax == 4 )
+    else
     {
-        Cut_TruthCompute4( p, pCut, pCut0, pCut1 );
-        return;
+        for ( i = 0; i < nTruthWords; i++ )
+            pTruthRes[i] = uTruth0[i] & uTruth1[i];
     }
-
-    puTruthCut0 = Cut_CutReadTruth(pCut0);
-    puTruthCut1 = Cut_CutReadTruth(pCut1);
-    puTruthCut  = Cut_CutReadTruth(pCut);
-
-    uPhase = Cut_TruthPhase( pCut, pCut0 );
-    Extra_TruthExpand( pCut->nVarsMax, (uint8*)puTruthCut0, uPhase, uTruth0 );
-    if ( p->fCompl0 )
-        Extra_BitNot( pCut->nVarsMax, uTruth0 );
-
-    uPhase = Cut_TruthPhase( pCut, pCut1 );
-    Extra_TruthExpand( pCut->nVarsMax, (uint8*)puTruthCut1, uPhase, uTruth1 );
-    if ( p->fCompl1 )
-        Extra_BitNot( pCut->nVarsMax, uTruth1 );
-
-    Extra_BitAnd( pCut->nVarsMax, (uint8*)uTruth0, (uint8*)uTruth1, (uint8*)puTruthCut );
-    if ( pCut->fCompl )
-        Extra_BitNot( pCut->nVarsMax, (uint8*)puTruthCut );
-
-p->timeTruth += clock() - clk;
-
-
-//Extra_PrintBinary( stdout, (unsigned*)uTruth0, 32 ); printf( "\n" );
-//Extra_PrintBinary( stdout, (unsigned*)uTruth1, 32 ); printf( "\n" );
-//Extra_PrintBinary( stdout, puTruthCut , 32 ); printf( "\n" );
-//uPhase = 0;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 8a00cec8..fee7bfbd 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -55,7 +55,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
     Dec_Graph_t * pGraph;
     Cut_Cut_t * pCut;
     Abc_Obj_t * pFanin;
-    unsigned uPhase, uTruthBest;
+    unsigned uPhase, uTruthBest, uTruth;
     char * pPerm;
     int Required, nNodesSaved;
     int i, GainCur, GainBest = -1;
@@ -78,8 +78,9 @@ clk = clock();
         if ( pCut->nLeaves < 4 )
             continue;
         // get the fanin permutation
-        pPerm = p->pPerms4[ p->pPerms[pCut->uTruth] ];
-        uPhase = p->pPhases[pCut->uTruth];
+        uTruth = 0xFFFF & *Cut_CutReadTruth(pCut);
+        pPerm = p->pPerms4[ p->pPerms[uTruth] ];
+        uPhase = p->pPhases[uTruth];
         // collect fanins with the corresponding permutation/phase
         Vec_PtrClear( p->vFaninsCur );
         Vec_PtrFill( p->vFaninsCur, (int)pCut->nLeaves, 0 );
@@ -122,7 +123,7 @@ p->timeEval += clock() - clk2;
             GainBest  = GainCur;
             p->pGraph  = pGraph;
             p->fCompl = ((uPhase & (1<<4)) > 0);
-            uTruthBest = pCut->uTruth;
+            uTruthBest = 0xFFFF & *Cut_CutReadTruth(pCut);
             // collect fanins in the
             Vec_PtrClear( p->vFanins );
             Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
@@ -171,8 +172,10 @@ Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCu
     Dec_Graph_t * pGraphBest, * pGraphCur;
     Rwr_Node_t * pNode, * pFanin;
     int nNodesAdded, GainBest, i, k;
+    unsigned uTruth;
     // find the matching class of subgraphs
-    vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[pCut->uTruth] );
+    uTruth = 0xFFFF & *Cut_CutReadTruth(pCut);
+    vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] );
     p->nSubgraphs += vSubgraphs->nSize;
     // determine the best subgraph
     GainBest = -1;
-- 
cgit v1.2.3