diff options
35 files changed, 2103 insertions, 809 deletions
@@ -418,6 +418,10 @@ SOURCE=.\src\base\io\ioWritePla.c # PROP Default_Filter "" # Begin Source File +SOURCE=.\src\base\main\libSupport.c +# End Source File +# Begin Source File + SOURCE=.\src\base\main\main.c # End Source File # Begin Source File Binary files differ@@ -3,16 +3,52 @@ <pre> <h1>Build Log</h1> <h3> ---------------------Configuration: abc - Win32 Debug-------------------- +--------------------Configuration: abc - Win32 Release-------------------- </h3> <h3>Command Lines</h3> -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1DD5.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211A.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\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 +/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\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c +"C:\_projects\abc\src\base\abc\abcAig.c" +"C:\_projects\abc\src\base\abc\abcCheck.c" +"C:\_projects\abc\src\base\abc\abcDfs.c" +"C:\_projects\abc\src\base\abc\abcFanio.c" +"C:\_projects\abc\src\base\abc\abcFunc.c" +"C:\_projects\abc\src\base\abc\abcLatch.c" +"C:\_projects\abc\src\base\abc\abcMinBase.c" +"C:\_projects\abc\src\base\abc\abcNames.c" "C:\_projects\abc\src\base\abc\abcNetlist.c" +"C:\_projects\abc\src\base\abc\abcNtk.c" +"C:\_projects\abc\src\base\abc\abcObj.c" +"C:\_projects\abc\src\base\abc\abcRefs.c" +"C:\_projects\abc\src\base\abc\abcShow.c" +"C:\_projects\abc\src\base\abc\abcSop.c" "C:\_projects\abc\src\base\abc\abcUtil.c" "C:\_projects\abc\src\base\abci\abc.c" +"C:\_projects\abc\src\base\abci\abcAttach.c" +"C:\_projects\abc\src\base\abci\abcBalance.c" +"C:\_projects\abc\src\base\abci\abcCollapse.c" +"C:\_projects\abc\src\base\abci\abcCut.c" +"C:\_projects\abc\src\base\abci\abcDsd.c" +"C:\_projects\abc\src\base\abci\abcFpga.c" +"C:\_projects\abc\src\base\abci\abcFraig.c" +"C:\_projects\abc\src\base\abci\abcFxu.c" +"C:\_projects\abc\src\base\abci\abcMap.c" +"C:\_projects\abc\src\base\abci\abcMiter.c" +"C:\_projects\abc\src\base\abci\abcNtbdd.c" +"C:\_projects\abc\src\base\abci\abcPga.c" "C:\_projects\abc\src\base\abci\abcPrint.c" +"C:\_projects\abc\src\base\abci\abcReconv.c" +"C:\_projects\abc\src\base\abci\abcRefactor.c" +"C:\_projects\abc\src\base\abci\abcRenode.c" +"C:\_projects\abc\src\base\abci\abcRewrite.c" +"C:\_projects\abc\src\base\abci\abcSat.c" +"C:\_projects\abc\src\base\abci\abcStrash.c" +"C:\_projects\abc\src\base\abci\abcSweep.c" +"C:\_projects\abc\src\base\abci\abcSymm.c" +"C:\_projects\abc\src\base\abci\abcTiming.c" +"C:\_projects\abc\src\base\abci\abcUnreach.c" +"C:\_projects\abc\src\base\abci\abcVerify.c" "C:\_projects\abc\src\base\abcs\abcRetCore.c" "C:\_projects\abc\src\base\abcs\abcRetDelay.c" "C:\_projects\abc\src\base\abcs\abcRetImpl.c" @@ -20,319 +56,610 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1DD5.tmp" with cont "C:\_projects\abc\src\base\abcs\abcSeq.c" "C:\_projects\abc\src\base\abcs\abcShare.c" "C:\_projects\abc\src\base\abcs\abcUtils.c" +"C:\_projects\abc\src\base\cmd\cmd.c" +"C:\_projects\abc\src\base\cmd\cmdAlias.c" +"C:\_projects\abc\src\base\cmd\cmdApi.c" +"C:\_projects\abc\src\base\cmd\cmdFlag.c" +"C:\_projects\abc\src\base\cmd\cmdHist.c" +"C:\_projects\abc\src\base\cmd\cmdUtils.c" +"C:\_projects\abc\src\base\io\io.c" +"C:\_projects\abc\src\base\io\ioRead.c" +"C:\_projects\abc\src\base\io\ioReadBench.c" +"C:\_projects\abc\src\base\io\ioReadBlif.c" +"C:\_projects\abc\src\base\io\ioReadEdif.c" +"C:\_projects\abc\src\base\io\ioReadEqn.c" +"C:\_projects\abc\src\base\io\ioReadPla.c" +"C:\_projects\abc\src\base\io\ioReadVerilog.c" +"C:\_projects\abc\src\base\io\ioUtil.c" +"C:\_projects\abc\src\base\io\ioWriteBench.c" +"C:\_projects\abc\src\base\io\ioWriteBlif.c" +"C:\_projects\abc\src\base\io\ioWriteCnf.c" +"C:\_projects\abc\src\base\io\ioWriteDot.c" +"C:\_projects\abc\src\base\io\ioWriteEqn.c" +"C:\_projects\abc\src\base\io\ioWriteGml.c" +"C:\_projects\abc\src\base\io\ioWritePla.c" +"C:\_projects\abc\src\base\main\main.c" +"C:\_projects\abc\src\base\main\mainFrame.c" +"C:\_projects\abc\src\base\main\mainInit.c" +"C:\_projects\abc\src\base\main\mainUtils.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddAbs.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddApply.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddFind.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddInv.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddIte.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddNeg.c" +"C:\_projects\abc\src\bdd\cudd\cuddAddWalsh.c" +"C:\_projects\abc\src\bdd\cudd\cuddAndAbs.c" +"C:\_projects\abc\src\bdd\cudd\cuddAnneal.c" +"C:\_projects\abc\src\bdd\cudd\cuddApa.c" +"C:\_projects\abc\src\bdd\cudd\cuddAPI.c" +"C:\_projects\abc\src\bdd\cudd\cuddApprox.c" +"C:\_projects\abc\src\bdd\cudd\cuddBddAbs.c" +"C:\_projects\abc\src\bdd\cudd\cuddBddCorr.c" +"C:\_projects\abc\src\bdd\cudd\cuddBddIte.c" +"C:\_projects\abc\src\bdd\cudd\cuddBridge.c" +"C:\_projects\abc\src\bdd\cudd\cuddCache.c" +"C:\_projects\abc\src\bdd\cudd\cuddCheck.c" +"C:\_projects\abc\src\bdd\cudd\cuddClip.c" +"C:\_projects\abc\src\bdd\cudd\cuddCof.c" +"C:\_projects\abc\src\bdd\cudd\cuddCompose.c" +"C:\_projects\abc\src\bdd\cudd\cuddDecomp.c" +"C:\_projects\abc\src\bdd\cudd\cuddEssent.c" +"C:\_projects\abc\src\bdd\cudd\cuddExact.c" +"C:\_projects\abc\src\bdd\cudd\cuddExport.c" +"C:\_projects\abc\src\bdd\cudd\cuddGenCof.c" +"C:\_projects\abc\src\bdd\cudd\cuddGenetic.c" +"C:\_projects\abc\src\bdd\cudd\cuddGroup.c" +"C:\_projects\abc\src\bdd\cudd\cuddHarwell.c" +"C:\_projects\abc\src\bdd\cudd\cuddInit.c" +"C:\_projects\abc\src\bdd\cudd\cuddInteract.c" +"C:\_projects\abc\src\bdd\cudd\cuddLCache.c" +"C:\_projects\abc\src\bdd\cudd\cuddLevelQ.c" +"C:\_projects\abc\src\bdd\cudd\cuddLinear.c" +"C:\_projects\abc\src\bdd\cudd\cuddLiteral.c" +"C:\_projects\abc\src\bdd\cudd\cuddMatMult.c" +"C:\_projects\abc\src\bdd\cudd\cuddPriority.c" +"C:\_projects\abc\src\bdd\cudd\cuddRead.c" +"C:\_projects\abc\src\bdd\cudd\cuddRef.c" +"C:\_projects\abc\src\bdd\cudd\cuddReorder.c" +"C:\_projects\abc\src\bdd\cudd\cuddSat.c" +"C:\_projects\abc\src\bdd\cudd\cuddSign.c" +"C:\_projects\abc\src\bdd\cudd\cuddSolve.c" +"C:\_projects\abc\src\bdd\cudd\cuddSplit.c" +"C:\_projects\abc\src\bdd\cudd\cuddSubsetHB.c" +"C:\_projects\abc\src\bdd\cudd\cuddSubsetSP.c" +"C:\_projects\abc\src\bdd\cudd\cuddSymmetry.c" +"C:\_projects\abc\src\bdd\cudd\cuddTable.c" +"C:\_projects\abc\src\bdd\cudd\cuddUtil.c" +"C:\_projects\abc\src\bdd\cudd\cuddWindow.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddCount.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddFuncs.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddGroup.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddIsop.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddLin.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddMisc.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddPort.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddReord.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddSetop.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddSymm.c" +"C:\_projects\abc\src\bdd\cudd\cuddZddUtil.c" +"C:\_projects\abc\src\bdd\epd\epd.c" +"C:\_projects\abc\src\bdd\mtr\mtrBasic.c" +"C:\_projects\abc\src\bdd\mtr\mtrGroup.c" +"C:\_projects\abc\src\bdd\parse\parseCore.c" +"C:\_projects\abc\src\bdd\parse\parseStack.c" +"C:\_projects\abc\src\bdd\dsd\dsdApi.c" +"C:\_projects\abc\src\bdd\dsd\dsdCheck.c" +"C:\_projects\abc\src\bdd\dsd\dsdLocal.c" +"C:\_projects\abc\src\bdd\dsd\dsdMan.c" +"C:\_projects\abc\src\bdd\dsd\dsdProc.c" +"C:\_projects\abc\src\bdd\dsd\dsdTree.c" +"C:\_projects\abc\src\bdd\reo\reoApi.c" +"C:\_projects\abc\src\bdd\reo\reoCore.c" +"C:\_projects\abc\src\bdd\reo\reoProfile.c" +"C:\_projects\abc\src\bdd\reo\reoSift.c" +"C:\_projects\abc\src\bdd\reo\reoSwap.c" +"C:\_projects\abc\src\bdd\reo\reoTest.c" +"C:\_projects\abc\src\bdd\reo\reoTransfer.c" +"C:\_projects\abc\src\bdd\reo\reoUnits.c" +"C:\_projects\abc\src\sat\asat\added.c" +"C:\_projects\abc\src\sat\asat\solver.c" +"C:\_projects\abc\src\sat\msat\msatActivity.c" +"C:\_projects\abc\src\sat\msat\msatClause.c" +"C:\_projects\abc\src\sat\msat\msatClauseVec.c" +"C:\_projects\abc\src\sat\msat\msatMem.c" +"C:\_projects\abc\src\sat\msat\msatOrderJ.c" +"C:\_projects\abc\src\sat\msat\msatQueue.c" +"C:\_projects\abc\src\sat\msat\msatRead.c" +"C:\_projects\abc\src\sat\msat\msatSolverApi.c" +"C:\_projects\abc\src\sat\msat\msatSolverCore.c" +"C:\_projects\abc\src\sat\msat\msatSolverIo.c" +"C:\_projects\abc\src\sat\msat\msatSolverSearch.c" +"C:\_projects\abc\src\sat\msat\msatSort.c" +"C:\_projects\abc\src\sat\msat\msatVec.c" +"C:\_projects\abc\src\sat\fraig\fraigApi.c" +"C:\_projects\abc\src\sat\fraig\fraigCanon.c" +"C:\_projects\abc\src\sat\fraig\fraigFanout.c" +"C:\_projects\abc\src\sat\fraig\fraigFeed.c" +"C:\_projects\abc\src\sat\fraig\fraigMan.c" +"C:\_projects\abc\src\sat\fraig\fraigMem.c" +"C:\_projects\abc\src\sat\fraig\fraigNode.c" +"C:\_projects\abc\src\sat\fraig\fraigPrime.c" +"C:\_projects\abc\src\sat\fraig\fraigSat.c" +"C:\_projects\abc\src\sat\fraig\fraigTable.c" +"C:\_projects\abc\src\sat\fraig\fraigUtil.c" +"C:\_projects\abc\src\sat\fraig\fraigVec.c" +"C:\_projects\abc\src\sat\csat\csat_apis.c" +"C:\_projects\abc\src\opt\fxu\fxu.c" +"C:\_projects\abc\src\opt\fxu\fxuCreate.c" +"C:\_projects\abc\src\opt\fxu\fxuHeapD.c" +"C:\_projects\abc\src\opt\fxu\fxuHeapS.c" +"C:\_projects\abc\src\opt\fxu\fxuList.c" +"C:\_projects\abc\src\opt\fxu\fxuMatrix.c" +"C:\_projects\abc\src\opt\fxu\fxuPair.c" +"C:\_projects\abc\src\opt\fxu\fxuPrint.c" +"C:\_projects\abc\src\opt\fxu\fxuReduce.c" +"C:\_projects\abc\src\opt\fxu\fxuSelect.c" +"C:\_projects\abc\src\opt\fxu\fxuSingle.c" +"C:\_projects\abc\src\opt\fxu\fxuUpdate.c" +"C:\_projects\abc\src\opt\rwr\rwrDec.c" +"C:\_projects\abc\src\opt\rwr\rwrEva.c" +"C:\_projects\abc\src\opt\rwr\rwrExp.c" +"C:\_projects\abc\src\opt\rwr\rwrLib.c" +"C:\_projects\abc\src\opt\rwr\rwrMan.c" +"C:\_projects\abc\src\opt\rwr\rwrPrint.c" +"C:\_projects\abc\src\opt\rwr\rwrUtil.c" +"C:\_projects\abc\src\opt\cut\cutApi.c" +"C:\_projects\abc\src\opt\cut\cutCut.c" +"C:\_projects\abc\src\opt\cut\cutMan.c" +"C:\_projects\abc\src\opt\cut\cutMerge.c" +"C:\_projects\abc\src\opt\cut\cutNode.c" +"C:\_projects\abc\src\opt\cut\cutSeq.c" +"C:\_projects\abc\src\opt\cut\cutTruth.c" +"C:\_projects\abc\src\opt\dec\decAbc.c" +"C:\_projects\abc\src\opt\dec\decFactor.c" +"C:\_projects\abc\src\opt\dec\decMan.c" +"C:\_projects\abc\src\opt\dec\decPrint.c" +"C:\_projects\abc\src\opt\dec\decUtil.c" +"C:\_projects\abc\src\opt\sim\simMan.c" +"C:\_projects\abc\src\opt\sim\simSat.c" +"C:\_projects\abc\src\opt\sim\simSupp.c" +"C:\_projects\abc\src\opt\sim\simSwitch.c" +"C:\_projects\abc\src\opt\sim\simSym.c" +"C:\_projects\abc\src\opt\sim\simSymSat.c" +"C:\_projects\abc\src\opt\sim\simSymSim.c" +"C:\_projects\abc\src\opt\sim\simSymStr.c" +"C:\_projects\abc\src\opt\sim\simUtils.c" +"C:\_projects\abc\src\map\fpga\fpga.c" +"C:\_projects\abc\src\map\fpga\fpgaCore.c" +"C:\_projects\abc\src\map\fpga\fpgaCreate.c" +"C:\_projects\abc\src\map\fpga\fpgaCut.c" +"C:\_projects\abc\src\map\fpga\fpgaCutUtils.c" +"C:\_projects\abc\src\map\fpga\fpgaFanout.c" +"C:\_projects\abc\src\map\fpga\fpgaLib.c" +"C:\_projects\abc\src\map\fpga\fpgaMatch.c" +"C:\_projects\abc\src\map\fpga\fpgaSwitch.c" +"C:\_projects\abc\src\map\fpga\fpgaTime.c" +"C:\_projects\abc\src\map\fpga\fpgaTruth.c" +"C:\_projects\abc\src\map\fpga\fpgaUtils.c" +"C:\_projects\abc\src\map\fpga\fpgaVec.c" +"C:\_projects\abc\src\map\mapper\mapper.c" +"C:\_projects\abc\src\map\mapper\mapperCanon.c" +"C:\_projects\abc\src\map\mapper\mapperCore.c" +"C:\_projects\abc\src\map\mapper\mapperCreate.c" +"C:\_projects\abc\src\map\mapper\mapperCut.c" +"C:\_projects\abc\src\map\mapper\mapperCutUtils.c" +"C:\_projects\abc\src\map\mapper\mapperFanout.c" +"C:\_projects\abc\src\map\mapper\mapperLib.c" +"C:\_projects\abc\src\map\mapper\mapperMatch.c" +"C:\_projects\abc\src\map\mapper\mapperRefs.c" +"C:\_projects\abc\src\map\mapper\mapperSuper.c" +"C:\_projects\abc\src\map\mapper\mapperSwitch.c" +"C:\_projects\abc\src\map\mapper\mapperTable.c" +"C:\_projects\abc\src\map\mapper\mapperTime.c" +"C:\_projects\abc\src\map\mapper\mapperTree.c" +"C:\_projects\abc\src\map\mapper\mapperTruth.c" +"C:\_projects\abc\src\map\mapper\mapperUtils.c" +"C:\_projects\abc\src\map\mapper\mapperVec.c" +"C:\_projects\abc\src\map\mio\mio.c" +"C:\_projects\abc\src\map\mio\mioApi.c" +"C:\_projects\abc\src\map\mio\mioFunc.c" +"C:\_projects\abc\src\map\mio\mioRead.c" +"C:\_projects\abc\src\map\mio\mioUtils.c" +"C:\_projects\abc\src\map\super\super.c" +"C:\_projects\abc\src\map\super\superAnd.c" +"C:\_projects\abc\src\map\super\superGate.c" +"C:\_projects\abc\src\map\super\superWrite.c" +"C:\_projects\abc\src\map\pga\pgaCore.c" +"C:\_projects\abc\src\map\pga\pgaMan.c" +"C:\_projects\abc\src\map\pga\pgaMatch.c" +"C:\_projects\abc\src\map\pga\pgaUtil.c" +"C:\_projects\abc\src\misc\extra\extraBddMisc.c" +"C:\_projects\abc\src\misc\extra\extraBddSymm.c" +"C:\_projects\abc\src\misc\extra\extraUtilBitMatrix.c" +"C:\_projects\abc\src\misc\extra\extraUtilCanon.c" +"C:\_projects\abc\src\misc\extra\extraUtilFile.c" +"C:\_projects\abc\src\misc\extra\extraUtilMemory.c" +"C:\_projects\abc\src\misc\extra\extraUtilMisc.c" +"C:\_projects\abc\src\misc\extra\extraUtilProgress.c" +"C:\_projects\abc\src\misc\extra\extraUtilReader.c" +"C:\_projects\abc\src\misc\st\st.c" +"C:\_projects\abc\src\misc\st\stmm.c" +"C:\_projects\abc\src\misc\util\cpu_stats.c" +"C:\_projects\abc\src\misc\util\cpu_time.c" +"C:\_projects\abc\src\misc\util\datalimit.c" +"C:\_projects\abc\src\misc\util\getopt.c" +"C:\_projects\abc\src\misc\util\pathsearch.c" +"C:\_projects\abc\src\misc\util\safe_mem.c" +"C:\_projects\abc\src\misc\util\strsav.c" +"C:\_projects\abc\src\misc\util\texpand.c" +"C:\_projects\abc\src\misc\mvc\mvc.c" +"C:\_projects\abc\src\misc\mvc\mvcApi.c" +"C:\_projects\abc\src\misc\mvc\mvcCompare.c" +"C:\_projects\abc\src\misc\mvc\mvcContain.c" +"C:\_projects\abc\src\misc\mvc\mvcCover.c" +"C:\_projects\abc\src\misc\mvc\mvcCube.c" +"C:\_projects\abc\src\misc\mvc\mvcDivide.c" +"C:\_projects\abc\src\misc\mvc\mvcDivisor.c" +"C:\_projects\abc\src\misc\mvc\mvcList.c" +"C:\_projects\abc\src\misc\mvc\mvcLits.c" +"C:\_projects\abc\src\misc\mvc\mvcMan.c" +"C:\_projects\abc\src\misc\mvc\mvcOpAlg.c" +"C:\_projects\abc\src\misc\mvc\mvcOpBool.c" +"C:\_projects\abc\src\misc\mvc\mvcPrint.c" +"C:\_projects\abc\src\misc\mvc\mvcSort.c" +"C:\_projects\abc\src\misc\mvc\mvcUtils.c" +"C:\_projects\abc\src\base\main\libSupport.c" ] -Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1DD5.tmp" -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1DD6.tmp" with contents +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211A.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211B.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\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 +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\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\libSupport.obj ] -Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1DD6.tmp" +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211B.tmp" <h3>Output Window</h3> Compiling... +abcAig.c +abcCheck.c +abcDfs.c +abcFanio.c +abcFunc.c +abcLatch.c +abcMinBase.c +abcNames.c abcNetlist.c +abcNtk.c +abcObj.c +abcRefs.c +abcShow.c +abcSop.c abcUtil.c abc.c +abcAttach.c +abcBalance.c +abcCollapse.c +abcCut.c +abcDsd.c +abcFpga.c +abcFraig.c +abcFxu.c +abcMap.c +abcMiter.c +abcNtbdd.c +abcPga.c abcPrint.c +abcReconv.c +abcRefactor.c +abcRenode.c +abcRewrite.c +abcSat.c +abcStrash.c +abcSweep.c +abcSymm.c +abcTiming.c +abcUnreach.c +abcVerify.c abcRetCore.c abcRetDelay.c abcRetImpl.c @@ -340,318 +667,588 @@ abcRetUtil.c abcSeq.c abcShare.c abcUtils.c +cmd.c +cmdAlias.c +cmdApi.c +cmdFlag.c +cmdHist.c +cmdUtils.c +io.c +ioRead.c +ioReadBench.c +ioReadBlif.c +ioReadEdif.c +ioReadEqn.c +ioReadPla.c +ioReadVerilog.c +ioUtil.c +ioWriteBench.c +ioWriteBlif.c +ioWriteCnf.c +ioWriteDot.c +ioWriteEqn.c +ioWriteGml.c +ioWritePla.c +main.c +mainFrame.c +mainInit.c +mainUtils.c +cuddAddAbs.c +cuddAddApply.c +cuddAddFind.c +cuddAddInv.c +cuddAddIte.c +cuddAddNeg.c +cuddAddWalsh.c +cuddAndAbs.c +cuddAnneal.c +cuddApa.c +C:\_projects\abc\src\bdd\cudd\cuddApa.c(181) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data +C:\_projects\abc\src\bdd\cudd\cuddApa.c(213) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data +C:\_projects\abc\src\bdd\cudd\cuddApa.c(530) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data +C:\_projects\abc\src\bdd\cudd\cuddApa.c(588) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data +cuddAPI.c +cuddApprox.c +cuddBddAbs.c +cuddBddCorr.c +cuddBddIte.c +cuddBridge.c +cuddCache.c +C:\_projects\abc\src\bdd\cudd\cuddCache.c(902) : warning C4146: unary minus operator applied to unsigned type, result still unsigned +cuddCheck.c +cuddClip.c +cuddCof.c +cuddCompose.c +cuddDecomp.c +cuddEssent.c +cuddExact.c +cuddExport.c +cuddGenCof.c +cuddGenetic.c +cuddGroup.c +C:\_projects\abc\src\bdd\cudd\cuddGroup.c(2062) : warning C4018: '<=' : signed/unsigned mismatch +cuddHarwell.c +cuddInit.c +cuddInteract.c +cuddLCache.c +C:\_projects\abc\src\bdd\cudd\cuddLCache.c(1387) : warning C4146: unary minus operator applied to unsigned type, result still unsigned +cuddLevelQ.c +cuddLinear.c +cuddLiteral.c +cuddMatMult.c +cuddPriority.c +cuddRead.c +cuddRef.c +cuddReorder.c +C:\_projects\abc\src\bdd\cudd\cuddReorder.c(395) : warning C4146: unary minus operator applied to unsigned type, result still unsigned +cuddSat.c +C:\_projects\abc\src\bdd\cudd\cuddReorder.c(2016) : warning C4700: local variable 'minLevel' used without having been initialized +C:\_projects\abc\src\bdd\cudd\cuddReorder.c(2020) : warning C4700: local variable 'maxLevel' used without having been initialized +cuddSign.c +cuddSolve.c +cuddSplit.c +cuddSubsetHB.c +cuddSubsetSP.c +cuddSymmetry.c +cuddTable.c +C:\_projects\abc\src\bdd\cudd\cuddTable.c(1822) : warning C4018: '<' : signed/unsigned mismatch +C:\_projects\abc\src\bdd\cudd\cuddTable.c(1927) : warning C4018: '<' : signed/unsigned mismatch +C:\_projects\abc\src\bdd\cudd\cuddTable.c(2235) : warning C4018: '<' : signed/unsigned mismatch +C:\_projects\abc\src\bdd\cudd\cuddTable.c(2303) : warning C4018: '<' : signed/unsigned mismatch +C:\_projects\abc\src\bdd\cudd\cuddTable.c(2358) : warning C4146: unary minus operator applied to unsigned type, result still unsigned +cuddUtil.c +cuddWindow.c +cuddZddCount.c +cuddZddFuncs.c +cuddZddGroup.c +cuddZddIsop.c +cuddZddLin.c +cuddZddMisc.c +cuddZddPort.c +cuddZddReord.c +cuddZddSetop.c +cuddZddSymm.c +cuddZddUtil.c +epd.c +mtrBasic.c +mtrGroup.c +parseCore.c +parseStack.c +dsdApi.c +dsdCheck.c +dsdLocal.c +dsdMan.c +dsdProc.c +dsdTree.c +reoApi.c +reoCore.c +reoProfile.c +reoSift.c +reoSwap.c +reoTest.c +reoTransfer.c +reoUnits.c +added.c +solver.c +msatActivity.c +msatClause.c +msatClauseVec.c +msatMem.c +msatOrderJ.c +msatQueue.c +msatRead.c +msatSolverApi.c +msatSolverCore.c +msatSolverIo.c +msatSolverSearch.c +msatSort.c +msatVec.c +fraigApi.c +fraigCanon.c +fraigFanout.c +fraigFeed.c +fraigMan.c +fraigMem.c +fraigNode.c +fraigPrime.c +fraigSat.c +fraigTable.c +fraigUtil.c +fraigVec.c +csat_apis.c +fxu.c +fxuCreate.c +fxuHeapD.c +fxuHeapS.c +fxuList.c +fxuMatrix.c +fxuPair.c +fxuPrint.c +fxuReduce.c +fxuSelect.c +fxuSingle.c +fxuUpdate.c +rwrDec.c +rwrEva.c +rwrExp.c +rwrLib.c +rwrMan.c +rwrPrint.c +rwrUtil.c +cutApi.c +cutCut.c +cutMan.c +cutMerge.c +cutNode.c +cutSeq.c +cutTruth.c +decAbc.c +decFactor.c +decMan.c +decPrint.c +decUtil.c +simMan.c +simSat.c +simSupp.c +simSwitch.c +simSym.c +simSymSat.c +simSymSim.c +simSymStr.c +simUtils.c +fpga.c +fpgaCore.c +fpgaCreate.c +fpgaCut.c +fpgaCutUtils.c +fpgaFanout.c +fpgaLib.c +fpgaMatch.c +fpgaSwitch.c +fpgaTime.c +fpgaTruth.c +fpgaUtils.c +fpgaVec.c +mapper.c +mapperCanon.c +mapperCore.c +mapperCreate.c +mapperCut.c +mapperCutUtils.c +mapperFanout.c +mapperLib.c +mapperMatch.c +mapperRefs.c +mapperSuper.c +mapperSwitch.c +mapperTable.c +mapperTime.c +mapperTree.c +mapperTruth.c +mapperUtils.c +mapperVec.c +mio.c +mioApi.c +mioFunc.c +mioRead.c +mioUtils.c +super.c +superAnd.c +superGate.c +superWrite.c +pgaCore.c +pgaMan.c +pgaMatch.c +pgaUtil.c +extraBddMisc.c +extraBddSymm.c +extraUtilBitMatrix.c +extraUtilCanon.c +extraUtilFile.c +extraUtilMemory.c +extraUtilMisc.c +extraUtilProgress.c +extraUtilReader.c +st.c +stmm.c +cpu_stats.c +cpu_time.c +datalimit.c +getopt.c +pathsearch.c +safe_mem.c +strsav.c +texpand.c +mvc.c +mvcApi.c +mvcCompare.c +mvcContain.c +mvcCover.c +mvcCube.c +mvcDivide.c +mvcDivisor.c +mvcList.c +mvcLits.c +mvcMan.c +mvcOpAlg.c +mvcOpBool.c +mvcPrint.c +mvcSort.c +mvcUtils.c +libSupport.c Linking... -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1DD8.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211D.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\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] -Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1DD8.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\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\libSupport.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP211D.tmp" Creating browse info file... <h3>Output Window</h3> <h3>Results</h3> -abc.exe - 0 error(s), 0 warning(s) +abc.exe - 0 error(s), 15 warning(s) </pre> </body> </html> @@ -36,6 +36,7 @@ alias r read alias ren renode alias rl read_blif alias rb read_bench +alias ret retime alias rp read_pla alias rv read_verilog alias rsup read_super mcnc5_old.super @@ -63,4 +64,3 @@ alias sharedsd "b; ren; dsd -g; sw; fx; b" alias resyn "b; rw; rwz; b; rwz; b" alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" alias thin "rwz; rfz; b; ps" - diff --git a/regtest.script b/regtest.script new file mode 100644 index 00000000..a047af53 --- /dev/null +++ b/regtest.script @@ -0,0 +1,103 @@ +r examples/apex4.pla +resyn +sharem +fpga +cec +ps + +clp +share +resyn +map +cec +ps + +r examples/C2670.blif +resyn +fpga +cec +ps + +u +map +cec +ps + +r examples/frg2.blif +dsd +muxes +cec +clp +share +resyn +map +cec +ps + +r examples/pj1.blif +resyn +fpga +cec +ps + +u +map +cec +ps + +r examples/s38584.bench +resyn +fpga +cec +ps + +u +map +cec +ps + +r examples/ac.v +resyn +fpga +cec +ps + +u +map +cec +ps + +r examples/s444.blif +b +esd -v +dsd +cec +ps + +r examples/i10.blif +fpga +cec +ps +u +map +cec +ps + +r examples/i10.blif +b +fraig_store +resyn +fraig_store +resyn2 +fraig_store +fraig_restore +fpga +cec +ps + +u +map +cec +ps + +time diff --git a/regtest_output.txt b/regtest_output.txt new file mode 100644 index 00000000..f66ee380 --- /dev/null +++ b/regtest_output.txt @@ -0,0 +1,165 @@ +UC Berkeley, ABC 1.01 (compiled Sep 5 2005 23:36:08) +abc 01> so regtest.script +abc - > r examples/apex4.pla +abc - > resyn +abc - > sharem +abc - > fpga +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +examples/apex4.pla: i/o = 9/ 19 lat = 0 nd = 784 cube = 1985 lev = 5 +abc - > +abc - > clp +The shared BDD size is 917 nodes. +abc - > share +abc - > resyn +abc - > map +A simple supergate library is derived from gate library "mcnc_temp.genlib". +Loaded 20 unique 5-input supergates from "mcnc_temp.super". Time = 0.02 sec +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +examples/apex4.pla: i/o = 9/ 19 lat = 0 nd = 1816 area = 4599.00 delay = 11.50 lev = 11 +abc - > +abc - > r examples/C2670.blif +abc - > resyn +abc - > fpga +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +C2670.iscas : i/o = 233/ 140 lat = 0 nd = 169 cube = 482 lev = 6 +abc - > +abc - > u +abc - > map +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +C2670.iscas : i/o = 233/ 140 lat = 0 nd = 465 area = 1142.00 delay = 15.50 lev = 14 +abc - > +abc - > r examples/frg2.blif +abc - > dsd +abc - > muxes +abc - > cec +Networks are equivalent after fraiging. +abc - > clp +The shared BDD size is 1111 nodes. +abc - > share +abc - > resyn +abc - > map +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +frg2 : i/o = 143/ 139 lat = 0 nd = 540 area = 1360.00 delay = 10.10 lev = 9 +abc - > +abc - > r examples/pj1.blif +abc - > resyn +abc - > fpga +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +exCombCkt : i/o = 1769/1063 lat = 0 nd = 4730 cube = 10662 lev = 12 +abc - > +abc - > u +abc - > map +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +exCombCkt : i/o = 1769/1063 lat = 0 nd = 10396 area = 25170.00 delay = 29.20 lev = 27 +abc - > +abc - > r examples/s38584.bench +abc - > resyn +The network has 26 self-feeding latches. +abc - > fpga +abc - > cec +The network has 26 self-feeding latches. +The network has 26 self-feeding latches. +Networks are equivalent after fraiging. +abc - > ps +examples/s38584.bench: i/o = 12/ 278 lat = 1452 nd = 3239 cube = 6769 lev = 7 +abc - > +abc - > u +abc - > map +The network has 26 self-feeding latches. +abc - > cec +The network has 26 self-feeding latches. +The network has 26 self-feeding latches. +Networks are equivalent after fraiging. +abc - > ps +examples/s38584.bench: i/o = 12/ 278 lat = 1452 nd = 8522 area = 19305.00 delay = 20.60 lev = 17 +abc - > +abc - > r examples/ac.v +abc - > resyn +abc - > fpga +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +ac97_ctrl : i/o = 84/ 48 lat = 2199 nd = 3652 cube = 9391 lev = 3 +abc - > +abc - > u +abc - > map +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +ac97_ctrl : i/o = 84/ 48 lat = 2199 nd = 8337 area = 19861.00 delay = 8.10 lev = 8 +abc - > +abc - > r examples/s444.blif +abc - > b +abc - > esd -v +The shared BDD size is 181 nodes. +BDD nodes in the transition relation before reordering 557. +BDD nodes in the transition relation after reordering 456. +Reachability analysis completed in 151 iterations. +The number of minterms in the reachable state set = 8865. +BDD nodes in the unreachable states before reordering 124. +BDD nodes in the unreachable states after reordering 113. +abc - > dsd +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +iscas\s444.bench: i/o = 3/ 6 lat = 21 nd = 81 cube = 119 lev = 7 +abc - > +abc - > r examples/i10.blif +abc - > fpga +The network was strashed and balanced before FPGA mapping. +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +i10 : i/o = 257/ 224 lat = 0 nd = 741 cube = 1616 lev = 11 +abc - > u +abc - > map +The network was strashed and balanced before mapping. +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +i10 : i/o = 257/ 224 lat = 0 nd = 1659 area = 4215.00 delay = 30.80 lev = 27 +abc - > +abc - > r examples/i10.blif +abc - > b +abc - > fraig_store +The number of AIG nodes added to storage = 2425. +abc - > resyn +abc - > fraig_store +The number of AIG nodes added to storage = 1678. +abc - > resyn2 +abc - > fraig_store +The number of AIG nodes added to storage = 1323. +abc - > fraig_restore +Currently stored 3 networks with 5426 nodes will be fraiged. +abc - > fpga +Performing FPGA mapping with choices. +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +i10 : i/o = 257/ 224 lat = 0 nd = 674 cube = 1498 lev = 10 +abc - > +abc - > u +abc - > map +Performing mapping with choices. +abc - > cec +Networks are equivalent after fraiging. +abc - > ps +i10 : i/o = 257/ 224 lat = 0 nd = 1505 area = 3561.00 delay = 25.00 lev = 22 +abc - > +abc 109> time +elapse: 77.52 seconds, total: 77.52 seconds +abc 109>
\ No newline at end of file diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index c0fec75d..db66c49b 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -249,12 +249,12 @@ static inline int Abc_NtkCiNum( Abc_Ntk_t * pNtk ) { return pN static inline int Abc_NtkCoNum( Abc_Ntk_t * pNtk ) { return pNtk->vCos->nSize; } // reading objects -static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i ) { assert( i < Vec_PtrSize(pNtk->vObjs) ); return pNtk->vObjs->pArray[i]; } -static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i ) { assert( i < Vec_PtrSize(pNtk->vLats) ); return pNtk->vLats->pArray[i]; } -static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkPiNum(pNtk) ); return pNtk->vCis->pArray[i]; } -static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkPoNum(pNtk) ); return pNtk->vCos->pArray[i]; } -static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkCiNum(pNtk) ); return pNtk->vCis->pArray[i]; } -static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkCoNum(pNtk) ); return pNtk->vCos->pArray[i]; } +static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i ) { assert( i < Vec_PtrSize(pNtk->vObjs) ); return (Abc_Obj_t *)pNtk->vObjs->pArray[i]; } +static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i ) { assert( i < Vec_PtrSize(pNtk->vLats) ); return (Abc_Obj_t *)pNtk->vLats->pArray[i]; } +static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkPiNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCis->pArray[i]; } +static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkPoNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCos->pArray[i]; } +static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkCiNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCis->pArray[i]; } +static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i ) { assert( i < Abc_NtkCoNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCos->pArray[i]; } // reading data members of the object static inline unsigned Abc_ObjType( Abc_Obj_t * pObj ) { return pObj->Type; } @@ -293,13 +293,13 @@ static inline int Abc_ObjFanoutNum( Abc_Obj_t * pObj ) { return pO static inline int Abc_ObjFaninId( Abc_Obj_t * pObj, int i) { return pObj->vFanins.pArray[i].iFan; } static inline int Abc_ObjFaninId0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].iFan; } static inline int Abc_ObjFaninId1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].iFan; } -static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ]; } -static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ]; } -static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan ]; } -static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan ]; } -static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan ]; } -static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj ) { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj; } -static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj ) { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj; } +static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ]; } +static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ]; } +static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan ]; } +static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan ]; } +static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan ]; } +static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj); } +static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj); } static inline bool Abc_ObjFaninC( Abc_Obj_t * pObj, int i ) { return pObj->vFanins.pArray[i].fCompl; } static inline bool Abc_ObjFaninC0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].fCompl; } static inline bool Abc_ObjFaninC1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].fCompl; } @@ -421,6 +421,8 @@ extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode ); extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode ); extern void Abc_AigPrintNode( Abc_Obj_t * pNode ); extern bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot ); +extern void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan ); +extern void Abc_AigRehash( Abc_Aig_t * pMan ); /*=== abcAttach.c ==========================================================*/ extern int Abc_NtkAttach( Abc_Ntk_t * pNtk ); /*=== abcBalance.c ==========================================================*/ diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 3e90aa76..639f4926 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -409,6 +409,7 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * Key = Abc_HashKey2( p0, p1, pMan->nBins ); pAnd->pNext = pMan->pBins[Key]; pMan->pBins[Key] = pAnd; + pMan->nEntries++; // create the cuts if defined // if ( pAnd->pNtk->pManCut ) // Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd ); @@ -542,6 +543,57 @@ clk = clock(); pMan->nBins = nBinsNew; } +/**Function************************************************************* + + Synopsis [Resizes the hash table of AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_AigRehash( Abc_Aig_t * pMan ) +{ + Abc_Obj_t ** pBinsNew; + Abc_Obj_t * pEnt, * pEnt2; + Abc_Fan_t * pArray; + unsigned Key; + int Counter, Temp, i; + + // allocate a new array + pBinsNew = ALLOC( Abc_Obj_t *, pMan->nBins ); + memset( pBinsNew, 0, sizeof(Abc_Obj_t *) * pMan->nBins ); + // rehash the entries from the old table + Counter = 0; + for ( i = 0; i < pMan->nBins; i++ ) + Abc_AigBinForEachEntrySafe( pMan->pBins[i], pEnt, pEnt2 ) + { + // swap the fanins if needed + pArray = pEnt->vFanins.pArray; + if ( pArray[0].iFan > pArray[1].iFan ) + { + Temp = pArray[0].iFan; + pArray[0].iFan = pArray[1].iFan; + pArray[1].iFan = Temp; + Temp = pArray[0].fCompl; + pArray[0].fCompl = pArray[1].fCompl; + pArray[1].fCompl = Temp; + } + // rehash the node + Key = Abc_HashKey2( Abc_ObjChild0(pEnt), Abc_ObjChild1(pEnt), pMan->nBins ); + pEnt->pNext = pBinsNew[Key]; + pBinsNew[Key] = pEnt; + Counter++; + } + assert( Counter == pMan->nEntries ); + // replace the table and the parameters + free( pMan->pBins ); + pMan->pBins = pBinsNew; +} + + @@ -1157,6 +1209,34 @@ bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot ) return 1; } +/**Function************************************************************* + + Synopsis [Resizes the hash table of AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan ) +{ + Abc_Obj_t * pEnt; + int i; + for ( i = 0; i < pMan->nBins; i++ ) + Abc_AigBinForEachEntry( pMan->pBins[i], pEnt ) + { + if ( Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id > Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id ) + { + int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id; + int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id; + int x = 0; + printf( "Node %d has incorrect ordering of fanins.\n", pEnt->Id ); + } + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c index 53ac6e07..619cce23 100644 --- a/src/base/abc/abcNames.c +++ b/src/base/abc/abcNames.c @@ -283,6 +283,7 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pObj) ); Abc_NtkForEachPo( pNtk, pObj, i ) Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pObj) ); + if ( !Abc_NtkIsSeq(pNtk) ) Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) ); } diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index a237f75e..2720f169 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -72,7 +72,10 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func ) else if ( Abc_NtkHasBdd(pNtk) ) pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); else if ( Abc_NtkHasAig(pNtk) ) - pNtk->pManFunc = Abc_AigAlloc( pNtk ); + { + if ( Abc_NtkIsStrash(pNtk) ) + pNtk->pManFunc = Abc_AigAlloc( pNtk ); + } else if ( Abc_NtkHasMapping(pNtk) ) pNtk->pManFunc = Abc_FrameReadLibGen(); else @@ -266,7 +269,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) // start the network pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc ); // copy the internal nodes - if ( Abc_NtkHasAig(pNtk) ) + if ( Abc_NtkIsStrash(pNtk) ) Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc ); else { @@ -278,6 +281,23 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) Abc_NtkForEachObj( pNtk, pObj, i ) Abc_ObjForEachFanin( pObj, pFanin, k ) Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + // if it is a sequential networ, transfer attributes on edges + if ( Abc_NtkIsSeq(pNtk) ) + { + pNtkNew->vInits = Vec_IntStart( 2 * Abc_NtkObjNumMax(pNtkNew) ); + Abc_NtkForEachObj( pNtk, pObj, i ) + { + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + if ( Abc_ObjFaninC(pObj, k) ) + Abc_ObjSetFaninC( pObj->pCopy, k ); + if ( Abc_ObjFaninL(pObj, k) > 0 ) + Abc_ObjSetFaninL( pObj->pCopy, k, Abc_ObjFaninL(pObj, k) ); + } + Vec_IntWriteEntry( pNtkNew->vInits, 2*pObj->pCopy->Id+0, Vec_IntEntry(pNtk->vInits, 2*pObj->Id+0) ); + Vec_IntWriteEntry( pNtkNew->vInits, 2*pObj->pCopy->Id+1, Vec_IntEntry(pNtk->vInits, 2*pObj->Id+1) ); + } + } } // duplicate the EXDC Ntk if ( pNtk->pExdc ) @@ -504,7 +524,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) Vec_PtrFree( pNtk->vPtrTemp ); Vec_IntFree( pNtk->vIntTemp ); Vec_StrFree( pNtk->vStrTemp ); - if ( pNtk->vInits ) Vec_IntFree( pNtk->vInits ); + if ( pNtk->vInits ) Vec_IntFree( pNtk->vInits ); + if ( pNtk->pModel ) free( pNtk->pModel ); // free the hash table of Obj name into Obj ID stmm_free_table( pNtk->tName2Net ); stmm_free_table( pNtk->tObj2Name ); @@ -526,7 +547,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) else if ( Abc_NtkHasBdd(pNtk) ) Extra_StopManager( pNtk->pManFunc ); else if ( Abc_NtkHasAig(pNtk) ) - Abc_AigFree( pNtk->pManFunc ); + { + if ( Abc_NtkIsStrash(pNtk) ) + Abc_AigFree( pNtk->pManFunc ); + } else if ( !Abc_NtkHasMapping(pNtk) ) assert( 0 ); free( pNtk ); diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index 15753f4e..9471bb3f 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -158,7 +158,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ) pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData); else if ( Abc_NtkHasMapping(pNtkNew) ) pObjNew->pData = pObj->pData; - else if ( Abc_NtkHasAig(pNtkNew) ) + else if ( Abc_NtkIsStrash(pNtkNew) ) assert( 0 ); } } @@ -191,6 +191,13 @@ Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew ) pConst1 = Abc_AigConst1(pNtkAig->pManFunc); if ( Abc_ObjFanoutNum(pConst1) > 0 ) pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew ); + else + { + // skip the 0-th entry to allow one-to-one match of object IDs + if ( pConst1->Id == 0 && pNtkNew->nNodes == 0 ) + Vec_PtrPush( pNtkNew->vObjs, NULL ); + } + return pConst1->pCopy; } diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index 20a64246..e36f5219 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -96,7 +96,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk ) char FileNameDot[200]; int i; - assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkHasAig(pNtk) ); // create the file name Abc_ShowGetFileName( pNtk->pName, FileNameDot ); // check that the file can be opened diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4745273e..16be21fd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -86,6 +86,7 @@ static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandPga ( 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_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -163,6 +164,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "FPGA mapping", "pga", Abc_CommandPga, 1 ); 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, "Verification", "cec", Abc_CommandCec, 0 ); @@ -949,9 +951,9 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( !Abc_NtkIsStrash(pNtk) ) + if ( !Abc_NtkHasAig(pNtk) ) { - fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\").\n" ); + fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\" or \"seq\").\n" ); return 1; } Abc_NtkShowAig( pNtk ); @@ -3906,7 +3908,6 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; - extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3931,8 +3932,8 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - printf( "This command is not yet implemented.\n" ); - return 0; +// printf( "This command is not yet implemented.\n" ); +// return 0; if ( !Abc_NtkIsStrash(pNtk) ) { @@ -3959,7 +3960,81 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: seq [-h]\n" ); - fprintf( pErr, "\t converts AIG into sequential AIG (while sweeping latches)\n" ); + fprintf( pErr, "\t converts AIG into sequential AIG\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + int fShare; + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fShare = 1; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "sh" ) ) != EOF ) + { + switch ( c ) + { + case 's': + fShare ^= 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; + } + + // share the latches on the fanout edges + if ( fShare ) + Abc_NtkSeqShareFanouts(pNtk); + + // get the new network + pNtkRes = Abc_NtkSeqToLogicSop( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Converting sequential AIG into an SOP logic network has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: unseq [-sh]\n" ); + fprintf( pErr, "\t converts sequential AIG into an SOP logic network\n" ); + fprintf( pErr, "\t-s : toggle sharing latches [default = %s]\n", fShare? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -3991,7 +4066,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fForward = 0; + fForward = 1; fBackward = 0; fInitial = 0; util_getopt_reset(); @@ -4021,10 +4096,6 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - printf( "This command is not yet implemented.\n" ); - return 0; - - if ( !Abc_NtkIsSeq(pNtk) ) { fprintf( pErr, "Works only for sequential AIG.\n" ); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 20f41c56..01317d1d 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -501,7 +501,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames->pManFunc), Abc_LatchIsInit0(pLatch) ); } if ( Counter ) - printf( "Warning: %d uninitialized latches are replaced by free variables.\n", Counter ); + printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter ); } // create the timeframes @@ -521,12 +521,18 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) Abc_NtkForEachLatch( pNtk, pLatch, i ) { pLatchNew = Abc_NtkLatch(pNtkFrames, i); - Abc_ObjAddFanin( pLatchNew, Abc_ObjFanin0(pLatch)->pCopy ); + Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); Vec_PtrPush( pNtkFrames->vCis, pLatchNew ); Vec_PtrPush( pNtkFrames->vCos, pLatchNew ); Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); } } + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pLatch->pNext = NULL; + + // remove dangling nodes + Abc_AigCleanup( pNtkFrames->pManFunc ); + // make sure that everything is okay if ( !Abc_NtkCheck( pNtkFrames ) ) { @@ -586,7 +592,9 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_ } // transfer the implementation of the latch drivers to the latches Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pCopy = Abc_ObjChild0Copy(pLatch); + pLatch->pNext = Abc_ObjChild0Copy(pLatch); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pLatch->pCopy = pLatch->pNext; } diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c index 3d9534c8..421e3059 100644 --- a/src/base/abci/abcRefactor.c +++ b/src/base/abci/abcRefactor.c @@ -144,6 +144,8 @@ pManRef->timeTotal = clock() - clkStart; Abc_NtkManRefStop( pManRef ); // put the nodes into the DFS order and reassign their IDs Abc_NtkReassignIds( pNtk ); + Abc_AigRehash( pNtk->pManFunc ); +// Abc_AigCheckFaninOrder( pNtk->pManFunc ); // fix the levels if ( fUpdateLevel ) Abc_NtkStopReverseLevels( pNtk ); diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index 91a99a57..b70d30e6 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -115,6 +115,8 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart ); pNtk->pManCut = NULL; // put the nodes into the DFS order and reassign their IDs Abc_NtkReassignIds( pNtk ); + Abc_AigRehash( pNtk->pManFunc ); +// Abc_AigCheckFaninOrder( pNtk->pManFunc ); // fix the levels if ( fUpdateLevel ) Abc_NtkStopReverseLevels( pNtk ); diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index b335086f..e5bc2547 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -52,7 +52,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) assert( Abc_NtkLatchNum(pNtk) == 0 ); if ( Abc_NtkPoNum(pNtk) > 1 ) - fprintf( stdout, "Warning: The miter has more than 1 output. SAT will try to prove all of them.\n" ); + fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) ); // load clauses into the solver clk = clock(); @@ -65,11 +65,11 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) status = solver_simplify(pSat); // printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); // PRT( "Time", clock() - clk ); - if ( status == l_False ) + if ( status == 0 ) { solver_delete( pSat ); - printf( "The problem is UNSATISFIABLE after simplification.\n" ); - return 0; +// printf( "The problem is UNSATISFIABLE after simplification.\n" ); + return -1; } // solve the miter @@ -146,8 +146,10 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ); } // add clauses for each PO - Abc_NtkForEachPo( pNtk, pNode, i ) - Abc_NodeAddClausesTop( pSat, pNode, vVars ); +// Abc_NtkForEachPo( pNtk, pNode, i ) +// Abc_NodeAddClausesTop( pSat, pNode, vVars ); + + Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ); // delete Vec_StrFree( vCube ); diff --git a/src/base/abcs/abcRetImpl.c b/src/base/abcs/abcRetImpl.c index 84b386bb..ea849c1c 100644 --- a/src/base/abcs/abcRetImpl.c +++ b/src/base/abcs/abcRetImpl.c @@ -224,7 +224,7 @@ void Abc_ObjRetimeForward( Abc_Obj_t * pObj ) Init = ABC_INIT_DC; // add the init values to the fanouts Abc_ObjForEachFanout( pObj, pFanout, i ) - Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pFanout, pObj), Init ); + Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout), Init ); } /**Function************************************************************* diff --git a/src/base/abcs/abcSeq.c b/src/base/abcs/abcSeq.c index 3b266182..4a29fe0e 100644 --- a/src/base/abcs/abcSeq.c +++ b/src/base/abcs/abcSeq.c @@ -73,18 +73,21 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkNew; Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj, * pFanin; - int i, Init, nLatches; + Abc_Obj_t * pObj, * pFaninNew; + unsigned Init; + int i, nLatches; // make sure it is an AIG without self-feeding latches assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 ); // start the network + Abc_NtkCleanCopy( pNtk ); pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG ); // duplicate the name and the spec pNtkNew->pName = util_strsav(pNtk->pName); pNtkNew->pSpec = util_strsav(pNtk->pSpec); // clone const/PIs/POs Abc_NtkDupObj(pNtkNew, Abc_AigConst1(pNtk->pManFunc) ); + pNtkNew->nNodes -= 1; Abc_NtkForEachPi( pNtk, pObj, i ) Abc_NtkDupObj(pNtkNew, pObj); Abc_NtkForEachPo( pNtk, pObj, i ) @@ -98,8 +101,11 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) vNodes = Abc_AigDfs( pNtk, 0, 0 ); Vec_PtrForEachEntry( vNodes, pObj, i ) { + if ( Abc_ObjFaninNum(pObj) != 2 ) + continue; Abc_NtkDupObj(pNtkNew, pObj); pObj->pCopy->fPhase = pObj->fPhase; // needed for choices + pObj->pCopy->Level = pObj->Level; } // relink the choice nodes Vec_PtrForEachEntry( vNodes, pObj, i ) @@ -114,20 +120,33 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) // skip the constant and the PIs if ( Abc_ObjFaninNum(pObj) == 0 ) continue; + if ( Abc_ObjIsLatch(pObj) ) + continue; // process the first fanin - pFanin = Abc_NodeAigToSeq( pObj, 0, &nLatches, &Init ); - Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin) ); + pFaninNew = Abc_NodeAigToSeq( pObj, 0, &nLatches, &Init ); + if ( nLatches > ABC_MAX_EDGE_LATCH ) + { + printf( "The number of latches on an edge (%d) exceeds the limit (%d).\n", nLatches, ABC_MAX_EDGE_LATCH ); + nLatches = ABC_MAX_EDGE_LATCH; + } + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); Abc_ObjAddFaninL0( pObj->pCopy, nLatches ); - Vec_IntWriteEntry( pNtkNew->vInits, 2 * i + 0, Init ); + Vec_IntWriteEntry( pNtkNew->vInits, 2 * pObj->pCopy->Id + 0, Init ); if ( Abc_ObjFaninNum(pObj) == 1 ) continue; // process the second fanin - pFanin = Abc_NodeAigToSeq( pObj, 1, &nLatches, &Init ); - Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin) ); + pFaninNew = Abc_NodeAigToSeq( pObj, 1, &nLatches, &Init ); + if ( nLatches > ABC_MAX_EDGE_LATCH ) + { + printf( "The number of latches on an edge (%d) exceeds the limit (%d).\n", nLatches, ABC_MAX_EDGE_LATCH ); + nLatches = ABC_MAX_EDGE_LATCH; + } + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); Abc_ObjAddFaninL1( pObj->pCopy, nLatches ); - Vec_IntWriteEntry( pNtkNew->vInits, 2 * i + 1, Init ); + Vec_IntWriteEntry( pNtkNew->vInits, 2 * pObj->pCopy->Id + 1, Init ); } // set the cutset composed of latch drivers + Vec_PtrFree( pNtkNew->vLats ); pNtkNew->vLats = Abc_NtkAigCutsetCopy( pNtk ); // copy EXDC and check correctness if ( pNtkNew->pExdc ) @@ -179,21 +198,24 @@ Vec_Ptr_t * Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk ) ***********************************************************************/ Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsigned * pnInit ) { - Abc_Obj_t * pFanin; + Abc_Obj_t * pFanin, * pFaninNew; Abc_InitType_t Init; // get the given fanin of the node pFanin = Abc_ObjFanin( pObj, Num ); + // if fanin is the internal node, return its copy in the corresponding polarity if ( !Abc_ObjIsLatch(pFanin) ) { *pnLatches = 0; *pnInit = 0; - return Abc_ObjChild( pObj, Num ); + return Abc_ObjNotCond( pFanin->pCopy, Abc_ObjFaninC(pObj, Num) ); } - pFanin = Abc_NodeAigToSeq( pFanin, 0, pnLatches, pnInit ); - // get the new initial state - Init = Abc_LatchInit(pObj); + // fanin is a latch + // get the new fanins + pFaninNew = Abc_NodeAigToSeq( pFanin, 0, pnLatches, pnInit ); + // get the initial state + Init = Abc_LatchInit(pFanin); // complement the initial state if the inv is retimed over the latch - if ( Abc_ObjIsComplement(pFanin) ) + if ( Abc_ObjIsComplement(pFaninNew) ) { if ( Init == ABC_INIT_ZERO ) Init = ABC_INIT_ONE; @@ -205,7 +227,7 @@ Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsign // update the latch number and initial state (*pnLatches)++; (*pnInit) = ((*pnInit) << 2) | Init; - return Abc_ObjNotCond( pFanin, Abc_ObjFaninC(pObj,Num) ); + return Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC(pObj, Num) ); } @@ -225,16 +247,24 @@ Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsign Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pObjNew, * pFaninNew; + Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pConst1; int i, nCutNodes, nDigits; unsigned Init; + int nLatchMax = 0; + assert( Abc_NtkIsSeq(pNtk) ); // start the network without latches nCutNodes = pNtk->vLats->nSize; pNtk->vLats->nSize = 0; pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); pNtk->vLats->nSize = nCutNodes; // create the constant node - Abc_NtkDupConst1( pNtk, pNtkNew ); +// Abc_NtkDupConst1( pNtk, pNtkNew ); + pConst1 = Abc_NtkObj(pNtk,0); + if ( !Abc_ObjIsNode(pConst1) ) + pConst1 = NULL; + if ( pConst1 && Abc_ObjFanoutNum(pConst1) > 0 ) + pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew ); + // duplicate the nodes, create node functions Abc_NtkForEachNode( pNtk, pObj, i ) { @@ -254,9 +284,12 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) // connect the objects Abc_NtkForEachObj( pNtk, pObj, i ) { + assert( (int)pObj->Id == i ); // skip PIs and the constant if ( Abc_ObjFaninNum(pObj) == 0 ) continue; + if ( nLatchMax < Abc_ObjFaninL0(pObj) ) + nLatchMax = Abc_ObjFaninL0(pObj); // get the initial states of the latches on the fanin edge of this node Init = Vec_IntEntry( pNtk->vInits, 2 * pObj->Id ); // create the edge @@ -269,6 +302,8 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) Abc_ObjSetFaninC( pObj->pCopy, 0 ); continue; } + if ( nLatchMax < Abc_ObjFaninL0(pObj) ) + nLatchMax = Abc_ObjFaninL0(pObj); // get the initial states of the latches on the fanin edge of this node Init = Vec_IntEntry( pNtk->vInits, 2 * pObj->Id + 1 ); // create the edge @@ -276,6 +311,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); // the complemented edges are subsumed by the node function } + printf( "The max edge latch num = %d.\n", nLatchMax ); // count the number of digits in the latch names nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) ); // add the latches and their names @@ -289,11 +325,8 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) } // fix the problem with complemented and duplicated CO edges Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); - // duplicate the EXDC network - if ( pNtk->pExdc ) - fprintf( stdout, "Warning: EXDC network is not copied.\n" ); if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkSeqToLogic(): Network check has failed.\n" ); + fprintf( stdout, "Abc_NtkSeqToLogicSop(): Network check has failed.\n" ); return pNtkNew; } @@ -313,7 +346,10 @@ Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, int nLa { Abc_Obj_t * pLatch; if ( nLatches == 0 ) + { + assert( pFanin->pCopy ); return pFanin->pCopy; + } pFanin = Abc_NodeSeqToLogic( pNtkNew, pFanin, nLatches - 1, Init >> 2 ); pLatch = Abc_NtkCreateLatch( pNtkNew ); pLatch->pData = (void *)(Init & 3); diff --git a/src/base/abcs/abcShare.c b/src/base/abcs/abcShare.c index 4f12b7bc..d74d2577 100644 --- a/src/base/abcs/abcShare.c +++ b/src/base/abcs/abcShare.c @@ -25,7 +25,7 @@ //////////////////////////////////////////////////////////////////////// static void Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); -static void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, int Init, Vec_Ptr_t * vNodes ); +static void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -124,6 +124,8 @@ void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vN Vec_PtrClear( vNodes ); Abc_ObjForEachFanout( pNode, pFanout, i ) { + if ( Abc_ObjFanoutL(pNode, pFanout) == 0 ) + continue; Type = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pNode, pFanout) ); if ( Type == Init ) InitNew = Init; diff --git a/src/base/abcs/abcUtils.c b/src/base/abcs/abcUtils.c index a9f3254c..6b42b9a9 100644 --- a/src/base/abcs/abcUtils.c +++ b/src/base/abcs/abcUtils.c @@ -76,6 +76,41 @@ int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk ) return Counter; } +/**Function************************************************************* + + Synopsis [Generates the printable edge label with the initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge ) +{ + static char Buffer[ABC_MAX_EDGE_LATCH + 1]; + Abc_InitType_t Init; + int nLatches, i; + + nLatches = Abc_ObjFaninL( pObj, Edge ); + assert( nLatches <= ABC_MAX_EDGE_LATCH ); + for ( i = 0; i < nLatches; i++ ) + { + Init = Abc_ObjFaninLGetInitOne( pObj, Edge, i ); + if ( Init == ABC_INIT_NONE ) + Buffer[i] = '_'; + else if ( Init == ABC_INIT_ZERO ) + Buffer[i] = '0'; + else if ( Init == ABC_INIT_ONE ) + Buffer[i] = '1'; + else if ( Init == ABC_INIT_DC ) + Buffer[i] = 'x'; + else assert( 0 ); + } + Buffer[nLatches] = 0; + return Buffer; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abcs/abc_.c b/src/base/abcs/abc_.c deleted file mode 100644 index bef3836f..00000000 --- a/src/base/abcs/abc_.c +++ /dev/null @@ -1,47 +0,0 @@ -/**CFile**************************************************************** - - FileName [abc_.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abcs/abcs.h b/src/base/abcs/abcs.h index ba0442c0..024fe57a 100644 --- a/src/base/abcs/abcs.h +++ b/src/base/abcs/abcs.h @@ -164,11 +164,17 @@ static inline void Abc_ObjFaninLSetInit( Abc_Obj_t * pObj, int Edge, unsigned In Vec_IntWriteEntry( pObj->pNtk->vInits, 2 * pObj->Id + Edge, Init ); } +// getting the init value of the given latch on the edge +static inline Abc_InitType_t Abc_ObjFaninLGetInitOne( Abc_Obj_t * pObj, int Edge, int iLatch ) +{ + return 0x3 & (Abc_ObjFaninLGetInit(pObj, Edge) >> (2*iLatch)); +} + // setting the init value of the given latch on the edge static inline void Abc_ObjFaninLSetInitOne( Abc_Obj_t * pObj, int Edge, int iLatch, Abc_InitType_t Init ) { unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge); - unsigned EntryNew = (EntryCur & ~(0x3 << iLatch)) | (Init << iLatch); + unsigned EntryNew = (EntryCur & ~(0x3 << (2*iLatch))) | (Init << (2*iLatch)); assert( iLatch < Abc_ObjFaninL(pObj, Edge) ); Abc_ObjFaninLSetInit( pObj, Edge, EntryNew ); } @@ -305,7 +311,7 @@ extern void Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk ); /*=== abcUtil.c ==============================================================*/ extern int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk ); - +extern char * Abc_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/io/io.c b/src/base/io/io.c index 89703214..7a6ca49f 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -876,9 +876,9 @@ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - if ( !Abc_NtkIsStrash(pAbc->pNtkCur) ) + if ( !Abc_NtkHasAig(pAbc->pNtkCur) ) { - fprintf( stdout, "IoCommandWriteDot(): Currently can only process logic networks with BDDs.\n" ); + fprintf( stdout, "IoCommandWriteDot(): Currently can only process AIGs.\n" ); return 0; } diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 97258c81..cd297db7 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "io.h" +#include "abcs.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -191,7 +192,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, fprintf( pFile, " rank = same;\n" ); // the labeling node of this level fprintf( pFile, " Level%d;\n", LevelMax ); - // generat the PO nodes + // generate the PO nodes Vec_PtrForEachEntry( vNodes, pNode, i ) { if ( !Abc_ObjIsCo(pNode) ) @@ -242,7 +243,19 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, Vec_PtrForEachEntry( vNodes, pNode, i ) { if ( !Abc_ObjIsCi(pNode) ) + { + // check if the costant node is present + if ( Abc_ObjFaninNum(pNode) == 0 && Abc_ObjFanoutNum(pNode) > 0 ) + { + fprintf( pFile, " Node%d [label = \"Const1\"", pNode->Id ); + fprintf( pFile, ", shape = ellipse" ); + if ( pNode->fMarkB ) + fprintf( pFile, ", style = filled" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } continue; + } fprintf( pFile, " Node%d%s [label = \"%s%s\"", pNode->Id, (Abc_ObjIsLatch(pNode)? "_out":""), Abc_ObjName(pNode), (Abc_ObjIsLatch(pNode)? "_out":"") ); fprintf( pFile, ", shape = %s", (Abc_ObjIsLatch(pNode)? "box":"triangle") ); @@ -277,7 +290,11 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, fprintf( pFile, "Node%d%s", pNode->Id, (Abc_ObjIsLatch(pNode)? "_in":"") ); fprintf( pFile, " -> " ); fprintf( pFile, "Node%d%s", Abc_ObjFaninId0(pNode), (Abc_ObjIsLatch(Abc_ObjFanin0(pNode))? "_out":"") ); - fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dotted" : "bold" ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", Abc_ObjFaninC0(pNode)? "dotted" : "bold" ); + if ( Abc_ObjFaninL0(pNode) > 0 ) + fprintf( pFile, ", label = \"%s\"", Abc_ObjFaninGetInitPrintable(pNode,0) ); + fprintf( pFile, "]" ); fprintf( pFile, ";\n" ); } if ( Abc_ObjFaninNum(pNode) == 1 ) @@ -288,7 +305,11 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, fprintf( pFile, "Node%d", pNode->Id ); fprintf( pFile, " -> " ); fprintf( pFile, "Node%d%s", Abc_ObjFaninId1(pNode), (Abc_ObjIsLatch(Abc_ObjFanin1(pNode))? "_out":"") ); - fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dotted" : "bold" ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", Abc_ObjFaninC1(pNode)? "dotted" : "bold" ); + if ( Abc_ObjFaninL1(pNode) > 0 ) + fprintf( pFile, ", label = \"%s\"", Abc_ObjFaninGetInitPrintable(pNode,1) ); + fprintf( pFile, "]" ); fprintf( pFile, ";\n" ); } // generate the edges between the equivalent nodes diff --git a/src/base/main/libSupport.c b/src/base/main/libSupport.c new file mode 100644 index 00000000..51c137cf --- /dev/null +++ b/src/base/main/libSupport.c @@ -0,0 +1,164 @@ +/**CFile**************************************************************** + + FileName [libSupport.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The main package.] + + Synopsis [Support for external libaries.] + + Author [Mike Case] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: libSupport.c,v 1.1 2005/09/06 19:59:51 casem Exp $] + +***********************************************************************/ + +#include "mainInt.h" +#include <stdio.h> +#include <string.h> + +#ifndef WIN32 +# include <sys/types.h> +# include <dirent.h> +# include <dlfcn.h> +#endif + +#define MAX_LIBS 256 +static void* libHandles[MAX_LIBS+1]; // will be null terminated + +typedef void (*lib_init_end_func) (Abc_Frame_t * pAbc); + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// This will find all the ABC library extensions in the current directory and load them all. +//////////////////////////////////////////////////////////////////////////////////////////////////// +void open_libs() { + int curr_lib = 0; + +#ifdef WIN32 + printf("Warning: open_libs WIN32 not implemented.\n"); +#else + DIR* dirp; + struct dirent* dp; + + dirp = opendir("."); + while ((dp = readdir(dirp)) != NULL) { + if ((strncmp("libabc_", dp->d_name, 7) == 0) && + (strcmp(".so", dp->d_name + strlen(dp->d_name) - 3) == 0)) { + + // make sure we don't overflow the handle array + if (curr_lib >= MAX_LIBS) { + printf("Warning: maximum number of ABC libraries (%d) exceeded. Not loading %s.\n", + MAX_LIBS, + dp->d_name); + } + + // attempt to load it + else { + char* szPrefixed = malloc((strlen(dp->d_name) + 3) * sizeof(char)); + strcpy(szPrefixed, "./"); + strcat(szPrefixed, dp->d_name); + + libHandles[curr_lib] = dlopen(szPrefixed, RTLD_NOW | RTLD_LOCAL); + + // did the load succeed? + if (libHandles[curr_lib] != 0) { + printf("Loaded ABC library: %s (Abc library extension #%d)\n", szPrefixed, curr_lib); + curr_lib++; + } else { + printf("Warning: failed to load ABC library %s:\n\t%s\n", szPrefixed, dlerror()); + } + + free(szPrefixed); + } + } + } + closedir(dirp); +#endif + + // null terminate the list of handles + libHandles[curr_lib] = 0; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// This will close all open ABC library extensions +//////////////////////////////////////////////////////////////////////////////////////////////////// +void close_libs() { +#ifdef WIN32 + printf("Warning: close_libs WIN32 not implemented.\n"); +#else + int i; + for (i = 0; libHandles[i] != 0; i++) { + if (dlclose(libHandles[i]) != 0) { + printf("Warning: failed to close library %d\n", i); + } + libHandles[i] = 0; + } +#endif +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// This will get a pointer to a function inside of an open library +//////////////////////////////////////////////////////////////////////////////////////////////////// +void* get_fnct_ptr(int lib_num, char* sym_name) { +#ifdef WIN32 + printf("Warning: get_fnct_ptr WIN32 not implemented.\n"); + return 0; +#else + return dlsym(libHandles[lib_num], sym_name); +#endif +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// This will call an initialization function in every open library. +//////////////////////////////////////////////////////////////////////////////////////////////////// +void call_inits(Abc_Frame_t* pAbc) { + int i; + lib_init_end_func init_func; + for (i = 0; libHandles[i] != 0; i++) { + init_func = (lib_init_end_func) get_fnct_ptr(i, "abc_init"); + if (init_func == 0) { + printf("Warning: Failed to initialize library %d.\n", i); + } else { + (*init_func)(pAbc); + } + } +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// This will call a shutdown function in every open library. +//////////////////////////////////////////////////////////////////////////////////////////////////// +void call_ends(Abc_Frame_t* pAbc) { + int i; + lib_init_end_func end_func; + for (i = 0; libHandles[i] != 0; i++) { + end_func = (lib_init_end_func) get_fnct_ptr(i, "abc_end"); + if (end_func == 0) { + printf("Warning: Failed to end library %d.\n", i); + } else { + (*end_func)(pAbc); + } + } +} + +void Libs_Init(Abc_Frame_t * pAbc) +{ + open_libs(); + call_inits(pAbc); +} + +void Libs_End(Abc_Frame_t * pAbc) +{ + call_ends(pAbc); + + // It's good practice to close our libraries at this point, but this can mess up any backtrace printed by Valgind. + // close_libs(); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/base/main/main.c b/src/base/main/main.c index 43ad6956..6668d088 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -216,7 +216,7 @@ int main( int argc, char * argv[] ) } // if the memory should be freed, quit packages - if ( fStatus == -2 ) + if ( fStatus < 0 ) { // perform uninitializations Abc_FrameEnd( pAbc ); diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c index 13710dcb..186d58fe 100644 --- a/src/base/main/mainInit.c +++ b/src/base/main/mainInit.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: mainInit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: mainInit.c,v 1.3 2005/09/14 22:53:37 casem Exp $] ***********************************************************************/ @@ -38,6 +38,8 @@ extern void Mio_Init( Abc_Frame_t * pAbc ); extern void Mio_End ( Abc_Frame_t * pAbc ); extern void Super_Init( Abc_Frame_t * pAbc ); extern void Super_End ( Abc_Frame_t * pAbc ); +extern void Libs_Init(Abc_Frame_t * pAbc); +extern void Libs_End(Abc_Frame_t * pAbc); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -63,6 +65,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc ) Map_Init( pAbc ); Mio_Init( pAbc ); Super_Init( pAbc ); + Libs_Init( pAbc ); } @@ -86,6 +89,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc ) Map_End( pAbc ); Mio_End( pAbc ); Super_End( pAbc ); + Libs_End( pAbc ); } diff --git a/src/base/main/module.make b/src/base/main/module.make index 59e1315e..7a04e533 100644 --- a/src/base/main/module.make +++ b/src/base/main/module.make @@ -1,4 +1,5 @@ SRC += src/base/main/main.c \ src/base/main/mainFrame.c \ src/base/main/mainInit.c \ - src/base/main/mainUtils.c + src/base/main/mainUtils.c \ + src/base/main/libSupport.c diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c index 08c029e1..543ad387 100644 --- a/src/bdd/dsd/dsdProc.c +++ b/src/bdd/dsd/dsdProc.c @@ -1255,7 +1255,7 @@ EXIT: s_CacheEntries++; -#if 0 +/* if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 ) { // write the function, for which verification does not work @@ -1277,7 +1277,7 @@ EXIT: cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask ); Cudd_RecursiveDerefZdd( dd, zNewFunc ); } -#endif +*/ } diff --git a/src/map/pga/pgaMan.c b/src/map/pga/pgaMan.c index d7573ecf..b75a26c6 100644 --- a/src/map/pga/pgaMan.c +++ b/src/map/pga/pgaMan.c @@ -75,6 +75,7 @@ Pga_Man_t * Pga_ManStart( Pga_Params_t * pParams ) { printf( "The nodes of the network are not DFS ordered.\n" ); // Abc_NtkReassignIds( pNtk ); +// Abc_AigRehash( pNtk->pManFunc ); return NULL; } // make sure there are no dangling nodes (unless they are choices) diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index 0ad5fd1e..9179336f 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -50,13 +50,13 @@ struct Vec_Vec_t_ // iterators through levels #define Vec_VecForEachLevel( vGlob, vVec, i ) \ - for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ ) + for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) #define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart ) \ - for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ ) + for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) #define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ - for ( i = LevelStart; (i <= LevelStop) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ ) + for ( i = LevelStart; (i <= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ ) #define Vec_VecForEachLevelReverse( vGlob, vVec, i ) \ - for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i-- ) + for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) // iteratores through entries #define Vec_VecForEachEntry( vGlob, pEntry, i, k ) \ @@ -234,7 +234,7 @@ static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry ) p->pArray[i] = Vec_PtrAlloc( 0 ); p->nSize = Level + 1; } - Vec_PtrPush( p->pArray[Level], Entry ); + Vec_PtrPush( (Vec_Ptr_t*)p->pArray[Level], Entry ); } /**Function************************************************************* @@ -253,7 +253,7 @@ static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry ) if ( p->nSize < Level + 1 ) Vec_VecPush( p, Level, Entry ); else - Vec_PtrPushUnique( p->pArray[Level], Entry ); + Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index 98024a7f..d248b115 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -317,11 +317,11 @@ static void clause_remove(solver* s, clause* c) vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); if (clause_learnt(c)){ - s->stats.learnts--; - s->stats.learnts_literals -= clause_size(c); + s->solver_stats.learnts--; + s->solver_stats.learnts_literals -= clause_size(c); }else{ - s->stats.clauses--; - s->stats.clauses_literals -= clause_size(c); + s->solver_stats.clauses--; + s->solver_stats.clauses_literals -= clause_size(c); } free(c); @@ -409,7 +409,7 @@ static inline bool enqueue(solver* s, lit l, clause* from) s->trail[s->qtail++] = l; order_assigned(s, v); - return true; + return 1; } } @@ -465,8 +465,8 @@ static void solver_record(solver* s, vec* cls) if (c != 0) { vec_push(&s->learnts,(void*)c); act_clause_bump(s,c); - s->stats.learnts++; - s->stats.learnts_literals += vec_size(cls); + s->solver_stats.learnts++; + s->solver_stats.learnts_literals += vec_size(cls); } } @@ -521,7 +521,7 @@ static bool solver_lit_removable(solver* s, lit l, int minl) for (j = top; j < vec_size(&s->tagged); j++) tags[tagged[j]] = l_Undef; vec_resize(&s->tagged,top); - return false; + return 0; } } }else{ @@ -541,14 +541,14 @@ static bool solver_lit_removable(solver* s, lit l, int minl) for (j = top; j < vec_size(&s->tagged); j++) tags[tagged[j]] = l_Undef; vec_resize(&s->tagged,top); - return false; + return 0; } } } } } - return true; + return 1; } static void solver_analyze(solver* s, clause* c, vec* learnt) @@ -627,9 +627,9 @@ static void solver_analyze(solver* s, clause* c, vec* learnt) } // update size of learnt + statistics - s->stats.max_literals += vec_size(learnt); + s->solver_stats.max_literals += vec_size(learnt); vec_resize(learnt,j); - s->stats.tot_literals += j; + s->solver_stats.tot_literals += j; // clear tags tagged = (int*)vec_begin(&s->tagged); @@ -684,7 +684,7 @@ clause* solver_propagate(solver* s) clause **end = begin + vec_size(ws); clause **i, **j; - s->stats.propagations++; + s->solver_stats.propagations++; s->simpdb_props--; //printf("checking lit %d: "L_LIT"\n", vec_size(ws), L_lit(p)); @@ -746,7 +746,7 @@ clause* solver_propagate(solver* s) i++; } - s->stats.inspects += j - (clause**)vec_begin(ws); + s->solver_stats.inspects += j - (clause**)vec_begin(ws); vec_resize(ws,j - (clause**)vec_begin(ws)); } @@ -796,7 +796,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) assert(s->root_level == solver_dlevel(s)); - s->stats.starts++; + s->solver_stats.starts++; s->var_decay = (float)(1 / var_decay ); s->cla_decay = (float)(1 / clause_decay); vec_resize(&s->model,0); @@ -811,7 +811,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) #ifdef VERBOSEDEBUG printf(L_IND"**CONFLICT**\n", L_ind); #endif - s->stats.conflicts++; conflictC++; + s->solver_stats.conflicts++; conflictC++; if (solver_dlevel(s) == s->root_level){ vec_delete(&learnt_clause); return l_False; @@ -845,7 +845,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) solver_reducedb(s); // New variable decision: - s->stats.decisions++; + s->solver_stats.decisions++; next = order_select(s,(float)random_var_freq); if (next == var_Undef){ @@ -910,17 +910,17 @@ solver* solver_new(void) s->binary->size_learnt = (2 << 1); s->verbosity = 0; - s->stats.starts = 0; - s->stats.decisions = 0; - s->stats.propagations = 0; - s->stats.inspects = 0; - s->stats.conflicts = 0; - s->stats.clauses = 0; - s->stats.clauses_literals = 0; - s->stats.learnts = 0; - s->stats.learnts_literals = 0; - s->stats.max_literals = 0; - s->stats.tot_literals = 0; + s->solver_stats.starts = 0; + s->solver_stats.decisions = 0; + s->solver_stats.propagations = 0; + s->solver_stats.inspects = 0; + s->solver_stats.conflicts = 0; + s->solver_stats.clauses = 0; + s->solver_stats.clauses_literals = 0; + s->solver_stats.learnts = 0; + s->solver_stats.learnts_literals = 0; + s->solver_stats.max_literals = 0; + s->solver_stats.tot_literals = 0; return s; } @@ -973,7 +973,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end) lbool* values; lit last; - if (begin == end) return false; + if (begin == end) return 0; //printlits(begin,end); printf("\n"); // insertion sort @@ -996,7 +996,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end) //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); lbool sig = !lit_sign(*i); sig += sig - 1; if (*i == neg(last) || sig == values[lit_var(*i)]) - return true; // tautology + return 1; // tautology else if (*i != last && values[lit_var(*i)] == l_Undef) last = *j++ = *i; } @@ -1004,7 +1004,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end) //printf("final: "); printlits(begin,j); printf("\n"); if (j == begin) // empty clause - return false; + return 0; else if (j - begin == 1) // unit clause return enqueue(s,*begin,(clause*)0); @@ -1012,10 +1012,10 @@ bool solver_addclause(solver* s, lit* begin, lit* end) vec_push(&s->clauses,clause_new(s,begin,j,0)); - s->stats.clauses++; - s->stats.clauses_literals += j - begin; + s->solver_stats.clauses++; + s->solver_stats.clauses_literals += j - begin; - return true; + return 1; } @@ -1027,10 +1027,10 @@ bool solver_simplify(solver* s) assert(solver_dlevel(s) == 0); if (solver_propagate(s) != 0) - return false; + return 0; if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) - return true; + return 1; reasons = s->reasons; for (type = 0; type < 2; type++){ @@ -1050,13 +1050,13 @@ bool solver_simplify(solver* s) s->simpdb_assigns = s->qhead; // (shouldn't depend on 'stats' really, but it will do for now) - s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals); + s->simpdb_props = (int)(s->solver_stats.clauses_literals + s->solver_stats.learnts_literals); - return true; + return 1; } -int solver_solve(solver* s, lit* begin, lit* end, int nSeconds) +bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds) { double nof_conflicts = 100; double nof_learnts = solver_nclauses(s) / 3; @@ -1068,7 +1068,7 @@ int solver_solve(solver* s, lit* begin, lit* end, int nSeconds) for (i = begin; i < end; i++) if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){ solver_canceluntil(s,0); - return false; } + return l_False; } s->root_level = solver_dlevel(s); @@ -1080,17 +1080,17 @@ int solver_solve(solver* s, lit* begin, lit* end, int nSeconds) } while (status == l_Undef){ - double Ratio = (s->stats.learnts == 0)? 0.0 : - s->stats.learnts_literals / (double)s->stats.learnts; + double Ratio = (s->solver_stats.learnts == 0)? 0.0 : + s->solver_stats.learnts_literals / (double)s->solver_stats.learnts; if (s->verbosity >= 1){ printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", - (double)s->stats.conflicts, - (double)s->stats.clauses, - (double)s->stats.clauses_literals, + (double)s->solver_stats.conflicts, + (double)s->solver_stats.clauses, + (double)s->solver_stats.clauses_literals, (double)nof_learnts, - (double)s->stats.learnts, - (double)s->stats.learnts_literals, + (double)s->solver_stats.learnts, + (double)s->solver_stats.learnts_literals, Ratio, s->progress_estimate*100); fflush(stdout); diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index 8e981198..9f80bc7e 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -36,16 +36,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define bool int #endif -static const bool true = 1; -static const bool false = 0; - typedef int lit; typedef char lbool; #ifdef _WIN32 -typedef signed __int64 sint64; // compatible with MS VS 6.0 +typedef signed __int64 sint64; // compatible with MS VS 6.0 #else -typedef long long sint64; +typedef long long sint64; #endif static const int var_Undef = -1; @@ -132,7 +129,7 @@ struct solver_t double progress_estimate; int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - stats stats; + stats solver_stats; }; #endif diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index fcb1018f..d54a3119 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -123,26 +123,32 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) int Fraig_ManCheckMiter( Fraig_Man_t * p ) { Fraig_Node_t * pNode; + int i; FREE( p->pModel ); - // get the output node (it can be complemented!) - pNode = p->vOutputs->pArray[0]; - // if the miter is constant 0, the problem is UNSAT - if ( pNode == Fraig_Not(p->pConst1) ) - return 1; - // consider the special case when the miter is constant 1 - if ( pNode == p->pConst1 ) + for ( i = 0; i < p->vOutputs->nSize; i++ ) { - // in this case, any counter example will do to distinquish it from constant 0 - // here we pick the counter example composed of all zeros - p->pModel = Fraig_ManAllocCounterExample( p ); - return 0; + // get the output node (it can be complemented!) + pNode = p->vOutputs->pArray[i]; + // if the miter is constant 0, the problem is UNSAT + if ( pNode == Fraig_Not(p->pConst1) ) + continue; + // consider the special case when the miter is constant 1 + if ( pNode == p->pConst1 ) + { + // in this case, any counter example will do to distinquish it from constant 0 + // here we pick the counter example composed of all zeros + p->pModel = Fraig_ManAllocCounterExample( p ); + return 0; + } + // save the counter example + p->pModel = Fraig_ManSaveCounterExample( p, pNode ); + // if the model is not found, return undecided + if ( p->pModel == NULL ) + return -1; + else + return 0; } - // save the counter example - p->pModel = Fraig_ManSaveCounterExample( p, pNode ); - // if the model is not found, return undecided - if ( p->pModel == NULL ) - return -1; - return 0; + return 1; } |