diff options
| -rw-r--r-- | abc.dsp | 64 | ||||
| -rw-r--r-- | abc.opt | bin | 52736 -> 52736 bytes | |||
| -rw-r--r-- | abc.plg | 48 | ||||
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | abclib.opt | bin | 49664 -> 49664 bytes | |||
| -rw-r--r-- | abclib.plg | 1930 | ||||
| -rw-r--r-- | src/base/abc/abc.h | 4 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 6 | ||||
| -rw-r--r-- | src/base/abci/abcMiter.c | 88 | ||||
| -rw-r--r-- | src/sat/aig/aig.h | 308 | ||||
| -rw-r--r-- | src/sat/aig/aigBalance.c | 47 | ||||
| -rw-r--r-- | src/sat/aig/aigCheck.c | 146 | ||||
| -rw-r--r-- | src/sat/aig/aigFanout.c | 423 | ||||
| -rw-r--r-- | src/sat/aig/aigMan.c | 142 | ||||
| -rw-r--r-- | src/sat/aig/aigMem.c | 246 | ||||
| -rw-r--r-- | src/sat/aig/aigNode.c | 292 | ||||
| -rw-r--r-- | src/sat/aig/aigOper.c | 175 | ||||
| -rw-r--r-- | src/sat/aig/aigReplace.c | 133 | ||||
| -rw-r--r-- | src/sat/aig/aigTable.c | 335 | ||||
| -rw-r--r-- | src/sat/aig/aigUtil.c | 60 | ||||
| -rw-r--r-- | src/sat/aig/fraigClass.c | 108 | ||||
| -rw-r--r-- | src/sat/aig/fraigCore.c | 47 | ||||
| -rw-r--r-- | src/sat/aig/fraigProve.c | 47 | ||||
| -rw-r--r-- | src/sat/aig/fraigSim.c | 238 | ||||
| -rw-r--r-- | src/sat/csat/csat_apis.c | 2 | ||||
| -rw-r--r-- | src/sat/fraig/fraigSat.c | 2 |
26 files changed, 3597 insertions, 1298 deletions
@@ -1045,6 +1045,70 @@ SOURCE=.\src\sat\csat\csat_apis.c SOURCE=.\src\sat\csat\csat_apis.h # End Source File # End Group +# Begin Group "aig" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\sat\aig\aig.h +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\aigBalance.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\aigCheck.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\aigFanout.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\aigMan.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\aigMem.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\aigNode.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\aigOper.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\aigReplace.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\aigTable.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\aigUtil.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\fraigClass.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\fraigCore.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\fraigProve.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\fraigSim.c +# End Source File +# End Group # End Group # Begin Group "opt" @@ -6,13 +6,13 @@ --------------------Configuration: abc - Win32 Debug-------------------- </h3> <h3>Command Lines</h3> -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14F9.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FE.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\seq" /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\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c -"C:\_projects\abc\src\opt\xyz\xyzCore.c" +"C:\_projects\abc\src\sat\aig\aigReplace.c" ] -Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14F9.tmp" -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FA.tmp" with contents +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FE.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FF.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 @@ -187,6 +187,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\msatClause.obj .\Debug\msatClauseVec.obj .\Debug\msatMem.obj +.\Debug\msatOrderJ.obj .\Debug\msatQueue.obj .\Debug\msatRead.obj .\Debug\msatSolverApi.obj @@ -208,6 +209,13 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\fraigUtil.obj .\Debug\fraigVec.obj .\Debug\csat_apis.obj +.\Debug\aigBalance.obj +.\Debug\aigFanout.obj +.\Debug\aigMan.obj +.\Debug\aigMem.obj +.\Debug\aigNode.obj +.\Debug\aigOper.obj +.\Debug\aigUtil.obj .\Debug\fxu.obj .\Debug\fxuCreate.obj .\Debug\fxuHeapD.obj @@ -338,14 +346,20 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\mvcPrint.obj .\Debug\mvcSort.obj .\Debug\mvcUtils.obj -.\Debug\msatOrderJ.obj +.\Debug\aigTable.obj +.\Debug\aigCheck.obj +.\Debug\aigReplace.obj +.\Debug\fraigCore.obj +.\Debug\fraigProve.obj +.\Debug\fraigSim.obj +.\Debug\fraigClass.obj ] -Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FA.tmp" +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FF.tmp" <h3>Output Window</h3> Compiling... -xyzCore.c +aigReplace.c Linking... -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp" with contents [ /nologo /o"Debug/abc.bsc" .\Debug\abcAig.sbr @@ -520,6 +534,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with cont .\Debug\msatClause.sbr .\Debug\msatClauseVec.sbr .\Debug\msatMem.sbr +.\Debug\msatOrderJ.sbr .\Debug\msatQueue.sbr .\Debug\msatRead.sbr .\Debug\msatSolverApi.sbr @@ -541,6 +556,13 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with cont .\Debug\fraigUtil.sbr .\Debug\fraigVec.sbr .\Debug\csat_apis.sbr +.\Debug\aigBalance.sbr +.\Debug\aigFanout.sbr +.\Debug\aigMan.sbr +.\Debug\aigMem.sbr +.\Debug\aigNode.sbr +.\Debug\aigOper.sbr +.\Debug\aigUtil.sbr .\Debug\fxu.sbr .\Debug\fxuCreate.sbr .\Debug\fxuHeapD.sbr @@ -671,8 +693,14 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with cont .\Debug\mvcPrint.sbr .\Debug\mvcSort.sbr .\Debug\mvcUtils.sbr -.\Debug\msatOrderJ.sbr] -Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" +.\Debug\aigTable.sbr +.\Debug\aigCheck.sbr +.\Debug\aigReplace.sbr +.\Debug\fraigCore.sbr +.\Debug\fraigProve.sbr +.\Debug\fraigSim.sbr +.\Debug\fraigClass.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp" Creating browse info file... <h3>Output Window</h3> @@ -457,6 +457,10 @@ SOURCE=.\src\base\io\ioWriteList.c SOURCE=.\src\base\io\ioWritePla.c # End Source File +# Begin Source File + +SOURCE=.\src\base\io\ioWriteVerilog.c +# End Source File # End Group # Begin Group "main" @@ -3,1308 +3,670 @@ <pre> <h1>Build Log</h1> <h3> ---------------------Configuration: abclib - Win32 Release-------------------- +--------------------Configuration: abclib - Win32 Debug-------------------- </h3> <h3>Command Lines</h3> -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP82.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F0.tmp" with contents [ -/nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /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\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"abclib\ReleaseLib/" /Fp"abclib\ReleaseLib/abclib.pch" /YX /Fo"abclib\ReleaseLib/" /Fd"abclib\ReleaseLib/" /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" +/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /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\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"abclib\DebugLib/" /Fp"abclib\DebugLib/abclib.pch" /YX /Fo"abclib\DebugLib/" /Fd"abclib\DebugLib/" /FD /GZ /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\abcVanEijk.c" -"C:\_projects\abc\src\base\abci\abcVanImp.c" -"C:\_projects\abc\src\base\abci\abcVerify.c" -"C:\_projects\abc\src\base\seq\seqAigCore.c" -"C:\_projects\abc\src\base\seq\seqAigIter.c" -"C:\_projects\abc\src\base\seq\seqCreate.c" -"C:\_projects\abc\src\base\seq\seqFpgaCore.c" -"C:\_projects\abc\src\base\seq\seqFpgaIter.c" -"C:\_projects\abc\src\base\seq\seqLatch.c" -"C:\_projects\abc\src\base\seq\seqMan.c" -"C:\_projects\abc\src\base\seq\seqMapCore.c" -"C:\_projects\abc\src\base\seq\seqMapIter.c" -"C:\_projects\abc\src\base\seq\seqRetCore.c" -"C:\_projects\abc\src\base\seq\seqRetIter.c" -"C:\_projects\abc\src\base\seq\seqShare.c" -"C:\_projects\abc\src\base\seq\seqUtil.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\ioReadBaf.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\ioWriteBaf.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\ioWriteList.c" -"C:\_projects\abc\src\base\io\ioWritePla.c" -"C:\_projects\abc\src\base\main\libSupport.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\cutOracle.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\simSeq.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\extraBddKmap.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\io\ioWriteVerilog.c" ] -Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP82.tmp" -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP83.tmp" with contents +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F0.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F1.tmp" with contents [ -/nologo /out:"abclib\abclib_release.lib" -.\abclib\ReleaseLib\abcAig.obj -.\abclib\ReleaseLib\abcCheck.obj -.\abclib\ReleaseLib\abcDfs.obj -.\abclib\ReleaseLib\abcFanio.obj -.\abclib\ReleaseLib\abcFunc.obj -.\abclib\ReleaseLib\abcLatch.obj -.\abclib\ReleaseLib\abcMinBase.obj -.\abclib\ReleaseLib\abcNames.obj -.\abclib\ReleaseLib\abcNetlist.obj -.\abclib\ReleaseLib\abcNtk.obj -.\abclib\ReleaseLib\abcObj.obj -.\abclib\ReleaseLib\abcRefs.obj -.\abclib\ReleaseLib\abcShow.obj -.\abclib\ReleaseLib\abcSop.obj -.\abclib\ReleaseLib\abcUtil.obj -.\abclib\ReleaseLib\abc.obj -.\abclib\ReleaseLib\abcAttach.obj -.\abclib\ReleaseLib\abcBalance.obj -.\abclib\ReleaseLib\abcCollapse.obj -.\abclib\ReleaseLib\abcCut.obj -.\abclib\ReleaseLib\abcDsd.obj -.\abclib\ReleaseLib\abcFpga.obj -.\abclib\ReleaseLib\abcFraig.obj -.\abclib\ReleaseLib\abcFxu.obj -.\abclib\ReleaseLib\abcMap.obj -.\abclib\ReleaseLib\abcMiter.obj -.\abclib\ReleaseLib\abcNtbdd.obj -.\abclib\ReleaseLib\abcPga.obj -.\abclib\ReleaseLib\abcPrint.obj -.\abclib\ReleaseLib\abcReconv.obj -.\abclib\ReleaseLib\abcRefactor.obj -.\abclib\ReleaseLib\abcRenode.obj -.\abclib\ReleaseLib\abcRewrite.obj -.\abclib\ReleaseLib\abcSat.obj -.\abclib\ReleaseLib\abcStrash.obj -.\abclib\ReleaseLib\abcSweep.obj -.\abclib\ReleaseLib\abcSymm.obj -.\abclib\ReleaseLib\abcTiming.obj -.\abclib\ReleaseLib\abcUnreach.obj -.\abclib\ReleaseLib\abcVanEijk.obj -.\abclib\ReleaseLib\abcVanImp.obj -.\abclib\ReleaseLib\abcVerify.obj -.\abclib\ReleaseLib\seqAigCore.obj -.\abclib\ReleaseLib\seqAigIter.obj -.\abclib\ReleaseLib\seqCreate.obj -.\abclib\ReleaseLib\seqFpgaCore.obj -.\abclib\ReleaseLib\seqFpgaIter.obj -.\abclib\ReleaseLib\seqLatch.obj -.\abclib\ReleaseLib\seqMan.obj -.\abclib\ReleaseLib\seqMapCore.obj -.\abclib\ReleaseLib\seqMapIter.obj -.\abclib\ReleaseLib\seqRetCore.obj -.\abclib\ReleaseLib\seqRetIter.obj -.\abclib\ReleaseLib\seqShare.obj -.\abclib\ReleaseLib\seqUtil.obj -.\abclib\ReleaseLib\cmd.obj -.\abclib\ReleaseLib\cmdAlias.obj -.\abclib\ReleaseLib\cmdApi.obj -.\abclib\ReleaseLib\cmdFlag.obj -.\abclib\ReleaseLib\cmdHist.obj -.\abclib\ReleaseLib\cmdUtils.obj -.\abclib\ReleaseLib\io.obj -.\abclib\ReleaseLib\ioRead.obj -.\abclib\ReleaseLib\ioReadBaf.obj -.\abclib\ReleaseLib\ioReadBench.obj -.\abclib\ReleaseLib\ioReadBlif.obj -.\abclib\ReleaseLib\ioReadEdif.obj -.\abclib\ReleaseLib\ioReadEqn.obj -.\abclib\ReleaseLib\ioReadPla.obj -.\abclib\ReleaseLib\ioReadVerilog.obj -.\abclib\ReleaseLib\ioUtil.obj -.\abclib\ReleaseLib\ioWriteBaf.obj -.\abclib\ReleaseLib\ioWriteBench.obj -.\abclib\ReleaseLib\ioWriteBlif.obj -.\abclib\ReleaseLib\ioWriteCnf.obj -.\abclib\ReleaseLib\ioWriteDot.obj -.\abclib\ReleaseLib\ioWriteEqn.obj -.\abclib\ReleaseLib\ioWriteGml.obj -.\abclib\ReleaseLib\ioWriteList.obj -.\abclib\ReleaseLib\ioWritePla.obj -.\abclib\ReleaseLib\libSupport.obj -.\abclib\ReleaseLib\main.obj -.\abclib\ReleaseLib\mainFrame.obj -.\abclib\ReleaseLib\mainInit.obj -.\abclib\ReleaseLib\mainUtils.obj -.\abclib\ReleaseLib\cuddAddAbs.obj -.\abclib\ReleaseLib\cuddAddApply.obj -.\abclib\ReleaseLib\cuddAddFind.obj -.\abclib\ReleaseLib\cuddAddInv.obj -.\abclib\ReleaseLib\cuddAddIte.obj -.\abclib\ReleaseLib\cuddAddNeg.obj -.\abclib\ReleaseLib\cuddAddWalsh.obj -.\abclib\ReleaseLib\cuddAndAbs.obj -.\abclib\ReleaseLib\cuddAnneal.obj -.\abclib\ReleaseLib\cuddApa.obj -.\abclib\ReleaseLib\cuddAPI.obj -.\abclib\ReleaseLib\cuddApprox.obj -.\abclib\ReleaseLib\cuddBddAbs.obj -.\abclib\ReleaseLib\cuddBddCorr.obj -.\abclib\ReleaseLib\cuddBddIte.obj -.\abclib\ReleaseLib\cuddBridge.obj -.\abclib\ReleaseLib\cuddCache.obj -.\abclib\ReleaseLib\cuddCheck.obj -.\abclib\ReleaseLib\cuddClip.obj -.\abclib\ReleaseLib\cuddCof.obj -.\abclib\ReleaseLib\cuddCompose.obj -.\abclib\ReleaseLib\cuddDecomp.obj -.\abclib\ReleaseLib\cuddEssent.obj -.\abclib\ReleaseLib\cuddExact.obj -.\abclib\ReleaseLib\cuddExport.obj -.\abclib\ReleaseLib\cuddGenCof.obj -.\abclib\ReleaseLib\cuddGenetic.obj -.\abclib\ReleaseLib\cuddGroup.obj -.\abclib\ReleaseLib\cuddHarwell.obj -.\abclib\ReleaseLib\cuddInit.obj -.\abclib\ReleaseLib\cuddInteract.obj -.\abclib\ReleaseLib\cuddLCache.obj -.\abclib\ReleaseLib\cuddLevelQ.obj -.\abclib\ReleaseLib\cuddLinear.obj -.\abclib\ReleaseLib\cuddLiteral.obj -.\abclib\ReleaseLib\cuddMatMult.obj -.\abclib\ReleaseLib\cuddPriority.obj -.\abclib\ReleaseLib\cuddRead.obj -.\abclib\ReleaseLib\cuddRef.obj -.\abclib\ReleaseLib\cuddReorder.obj -.\abclib\ReleaseLib\cuddSat.obj -.\abclib\ReleaseLib\cuddSign.obj -.\abclib\ReleaseLib\cuddSolve.obj -.\abclib\ReleaseLib\cuddSplit.obj -.\abclib\ReleaseLib\cuddSubsetHB.obj -.\abclib\ReleaseLib\cuddSubsetSP.obj -.\abclib\ReleaseLib\cuddSymmetry.obj -.\abclib\ReleaseLib\cuddTable.obj -.\abclib\ReleaseLib\cuddUtil.obj -.\abclib\ReleaseLib\cuddWindow.obj -.\abclib\ReleaseLib\cuddZddCount.obj -.\abclib\ReleaseLib\cuddZddFuncs.obj -.\abclib\ReleaseLib\cuddZddGroup.obj -.\abclib\ReleaseLib\cuddZddIsop.obj -.\abclib\ReleaseLib\cuddZddLin.obj -.\abclib\ReleaseLib\cuddZddMisc.obj -.\abclib\ReleaseLib\cuddZddPort.obj -.\abclib\ReleaseLib\cuddZddReord.obj -.\abclib\ReleaseLib\cuddZddSetop.obj -.\abclib\ReleaseLib\cuddZddSymm.obj -.\abclib\ReleaseLib\cuddZddUtil.obj -.\abclib\ReleaseLib\epd.obj -.\abclib\ReleaseLib\mtrBasic.obj -.\abclib\ReleaseLib\mtrGroup.obj -.\abclib\ReleaseLib\parseCore.obj -.\abclib\ReleaseLib\parseStack.obj -.\abclib\ReleaseLib\dsdApi.obj -.\abclib\ReleaseLib\dsdCheck.obj -.\abclib\ReleaseLib\dsdLocal.obj -.\abclib\ReleaseLib\dsdMan.obj -.\abclib\ReleaseLib\dsdProc.obj -.\abclib\ReleaseLib\dsdTree.obj -.\abclib\ReleaseLib\reoApi.obj -.\abclib\ReleaseLib\reoCore.obj -.\abclib\ReleaseLib\reoProfile.obj -.\abclib\ReleaseLib\reoSift.obj -.\abclib\ReleaseLib\reoSwap.obj -.\abclib\ReleaseLib\reoTest.obj -.\abclib\ReleaseLib\reoTransfer.obj -.\abclib\ReleaseLib\reoUnits.obj -.\abclib\ReleaseLib\added.obj -.\abclib\ReleaseLib\solver.obj -.\abclib\ReleaseLib\msatActivity.obj -.\abclib\ReleaseLib\msatClause.obj -.\abclib\ReleaseLib\msatClauseVec.obj -.\abclib\ReleaseLib\msatMem.obj -.\abclib\ReleaseLib\msatOrderJ.obj -.\abclib\ReleaseLib\msatQueue.obj -.\abclib\ReleaseLib\msatRead.obj -.\abclib\ReleaseLib\msatSolverApi.obj -.\abclib\ReleaseLib\msatSolverCore.obj -.\abclib\ReleaseLib\msatSolverIo.obj -.\abclib\ReleaseLib\msatSolverSearch.obj -.\abclib\ReleaseLib\msatSort.obj -.\abclib\ReleaseLib\msatVec.obj -.\abclib\ReleaseLib\fraigApi.obj -.\abclib\ReleaseLib\fraigCanon.obj -.\abclib\ReleaseLib\fraigFanout.obj -.\abclib\ReleaseLib\fraigFeed.obj -.\abclib\ReleaseLib\fraigMan.obj -.\abclib\ReleaseLib\fraigMem.obj -.\abclib\ReleaseLib\fraigNode.obj -.\abclib\ReleaseLib\fraigPrime.obj -.\abclib\ReleaseLib\fraigSat.obj -.\abclib\ReleaseLib\fraigTable.obj -.\abclib\ReleaseLib\fraigUtil.obj -.\abclib\ReleaseLib\fraigVec.obj -.\abclib\ReleaseLib\csat_apis.obj -.\abclib\ReleaseLib\fxu.obj -.\abclib\ReleaseLib\fxuCreate.obj -.\abclib\ReleaseLib\fxuHeapD.obj -.\abclib\ReleaseLib\fxuHeapS.obj -.\abclib\ReleaseLib\fxuList.obj -.\abclib\ReleaseLib\fxuMatrix.obj -.\abclib\ReleaseLib\fxuPair.obj -.\abclib\ReleaseLib\fxuPrint.obj -.\abclib\ReleaseLib\fxuReduce.obj -.\abclib\ReleaseLib\fxuSelect.obj -.\abclib\ReleaseLib\fxuSingle.obj -.\abclib\ReleaseLib\fxuUpdate.obj -.\abclib\ReleaseLib\rwrDec.obj -.\abclib\ReleaseLib\rwrEva.obj -.\abclib\ReleaseLib\rwrExp.obj -.\abclib\ReleaseLib\rwrLib.obj -.\abclib\ReleaseLib\rwrMan.obj -.\abclib\ReleaseLib\rwrPrint.obj -.\abclib\ReleaseLib\rwrUtil.obj -.\abclib\ReleaseLib\cutApi.obj -.\abclib\ReleaseLib\cutCut.obj -.\abclib\ReleaseLib\cutMan.obj -.\abclib\ReleaseLib\cutMerge.obj -.\abclib\ReleaseLib\cutNode.obj -.\abclib\ReleaseLib\cutOracle.obj -.\abclib\ReleaseLib\cutSeq.obj -.\abclib\ReleaseLib\cutTruth.obj -.\abclib\ReleaseLib\decAbc.obj -.\abclib\ReleaseLib\decFactor.obj -.\abclib\ReleaseLib\decMan.obj -.\abclib\ReleaseLib\decPrint.obj -.\abclib\ReleaseLib\decUtil.obj -.\abclib\ReleaseLib\simMan.obj -.\abclib\ReleaseLib\simSat.obj -.\abclib\ReleaseLib\simSeq.obj -.\abclib\ReleaseLib\simSupp.obj -.\abclib\ReleaseLib\simSwitch.obj -.\abclib\ReleaseLib\simSym.obj -.\abclib\ReleaseLib\simSymSat.obj -.\abclib\ReleaseLib\simSymSim.obj -.\abclib\ReleaseLib\simSymStr.obj -.\abclib\ReleaseLib\simUtils.obj -.\abclib\ReleaseLib\fpga.obj -.\abclib\ReleaseLib\fpgaCore.obj -.\abclib\ReleaseLib\fpgaCreate.obj -.\abclib\ReleaseLib\fpgaCut.obj -.\abclib\ReleaseLib\fpgaCutUtils.obj -.\abclib\ReleaseLib\fpgaFanout.obj -.\abclib\ReleaseLib\fpgaLib.obj -.\abclib\ReleaseLib\fpgaMatch.obj -.\abclib\ReleaseLib\fpgaSwitch.obj -.\abclib\ReleaseLib\fpgaTime.obj -.\abclib\ReleaseLib\fpgaTruth.obj -.\abclib\ReleaseLib\fpgaUtils.obj -.\abclib\ReleaseLib\fpgaVec.obj -.\abclib\ReleaseLib\mapper.obj -.\abclib\ReleaseLib\mapperCanon.obj -.\abclib\ReleaseLib\mapperCore.obj -.\abclib\ReleaseLib\mapperCreate.obj -.\abclib\ReleaseLib\mapperCut.obj -.\abclib\ReleaseLib\mapperCutUtils.obj -.\abclib\ReleaseLib\mapperFanout.obj -.\abclib\ReleaseLib\mapperLib.obj -.\abclib\ReleaseLib\mapperMatch.obj -.\abclib\ReleaseLib\mapperRefs.obj -.\abclib\ReleaseLib\mapperSuper.obj -.\abclib\ReleaseLib\mapperSwitch.obj -.\abclib\ReleaseLib\mapperTable.obj -.\abclib\ReleaseLib\mapperTime.obj -.\abclib\ReleaseLib\mapperTree.obj -.\abclib\ReleaseLib\mapperTruth.obj -.\abclib\ReleaseLib\mapperUtils.obj -.\abclib\ReleaseLib\mapperVec.obj -.\abclib\ReleaseLib\mio.obj -.\abclib\ReleaseLib\mioApi.obj -.\abclib\ReleaseLib\mioFunc.obj -.\abclib\ReleaseLib\mioRead.obj -.\abclib\ReleaseLib\mioUtils.obj -.\abclib\ReleaseLib\super.obj -.\abclib\ReleaseLib\superAnd.obj -.\abclib\ReleaseLib\superGate.obj -.\abclib\ReleaseLib\superWrite.obj -.\abclib\ReleaseLib\pgaCore.obj -.\abclib\ReleaseLib\pgaMan.obj -.\abclib\ReleaseLib\pgaMatch.obj -.\abclib\ReleaseLib\pgaUtil.obj -.\abclib\ReleaseLib\extraBddKmap.obj -.\abclib\ReleaseLib\extraBddMisc.obj -.\abclib\ReleaseLib\extraBddSymm.obj -.\abclib\ReleaseLib\extraUtilBitMatrix.obj -.\abclib\ReleaseLib\extraUtilCanon.obj -.\abclib\ReleaseLib\extraUtilFile.obj -.\abclib\ReleaseLib\extraUtilMemory.obj -.\abclib\ReleaseLib\extraUtilMisc.obj -.\abclib\ReleaseLib\extraUtilProgress.obj -.\abclib\ReleaseLib\extraUtilReader.obj -.\abclib\ReleaseLib\st.obj -.\abclib\ReleaseLib\stmm.obj -.\abclib\ReleaseLib\cpu_stats.obj -.\abclib\ReleaseLib\cpu_time.obj -.\abclib\ReleaseLib\datalimit.obj -.\abclib\ReleaseLib\getopt.obj -.\abclib\ReleaseLib\pathsearch.obj -.\abclib\ReleaseLib\safe_mem.obj -.\abclib\ReleaseLib\strsav.obj -.\abclib\ReleaseLib\texpand.obj -.\abclib\ReleaseLib\mvc.obj -.\abclib\ReleaseLib\mvcApi.obj -.\abclib\ReleaseLib\mvcCompare.obj -.\abclib\ReleaseLib\mvcContain.obj -.\abclib\ReleaseLib\mvcCover.obj -.\abclib\ReleaseLib\mvcCube.obj -.\abclib\ReleaseLib\mvcDivide.obj -.\abclib\ReleaseLib\mvcDivisor.obj -.\abclib\ReleaseLib\mvcList.obj -.\abclib\ReleaseLib\mvcLits.obj -.\abclib\ReleaseLib\mvcMan.obj -.\abclib\ReleaseLib\mvcOpAlg.obj -.\abclib\ReleaseLib\mvcOpBool.obj -.\abclib\ReleaseLib\mvcPrint.obj -.\abclib\ReleaseLib\mvcSort.obj -.\abclib\ReleaseLib\mvcUtils.obj +/nologo /out:"abclib\abclib_debug.lib" +.\abclib\DebugLib\abcAig.obj +.\abclib\DebugLib\abcCheck.obj +.\abclib\DebugLib\abcDfs.obj +.\abclib\DebugLib\abcFanio.obj +.\abclib\DebugLib\abcFunc.obj +.\abclib\DebugLib\abcLatch.obj +.\abclib\DebugLib\abcMinBase.obj +.\abclib\DebugLib\abcNames.obj +.\abclib\DebugLib\abcNetlist.obj +.\abclib\DebugLib\abcNtk.obj +.\abclib\DebugLib\abcObj.obj +.\abclib\DebugLib\abcRefs.obj +.\abclib\DebugLib\abcShow.obj +.\abclib\DebugLib\abcSop.obj +.\abclib\DebugLib\abcUtil.obj +.\abclib\DebugLib\abc.obj +.\abclib\DebugLib\abcAttach.obj +.\abclib\DebugLib\abcBalance.obj +.\abclib\DebugLib\abcCollapse.obj +.\abclib\DebugLib\abcCut.obj +.\abclib\DebugLib\abcDsd.obj +.\abclib\DebugLib\abcFpga.obj +.\abclib\DebugLib\abcFraig.obj +.\abclib\DebugLib\abcFxu.obj +.\abclib\DebugLib\abcMap.obj +.\abclib\DebugLib\abcMiter.obj +.\abclib\DebugLib\abcNtbdd.obj +.\abclib\DebugLib\abcPga.obj +.\abclib\DebugLib\abcPrint.obj +.\abclib\DebugLib\abcReconv.obj +.\abclib\DebugLib\abcRefactor.obj +.\abclib\DebugLib\abcRenode.obj +.\abclib\DebugLib\abcRewrite.obj +.\abclib\DebugLib\abcSat.obj +.\abclib\DebugLib\abcStrash.obj +.\abclib\DebugLib\abcSweep.obj +.\abclib\DebugLib\abcSymm.obj +.\abclib\DebugLib\abcTiming.obj +.\abclib\DebugLib\abcUnreach.obj +.\abclib\DebugLib\abcVanEijk.obj +.\abclib\DebugLib\abcVanImp.obj +.\abclib\DebugLib\abcVerify.obj +.\abclib\DebugLib\seqAigCore.obj +.\abclib\DebugLib\seqAigIter.obj +.\abclib\DebugLib\seqCreate.obj +.\abclib\DebugLib\seqFpgaCore.obj +.\abclib\DebugLib\seqFpgaIter.obj +.\abclib\DebugLib\seqLatch.obj +.\abclib\DebugLib\seqMan.obj +.\abclib\DebugLib\seqMapCore.obj +.\abclib\DebugLib\seqMapIter.obj +.\abclib\DebugLib\seqRetCore.obj +.\abclib\DebugLib\seqRetIter.obj +.\abclib\DebugLib\seqShare.obj +.\abclib\DebugLib\seqUtil.obj +.\abclib\DebugLib\cmd.obj +.\abclib\DebugLib\cmdAlias.obj +.\abclib\DebugLib\cmdApi.obj +.\abclib\DebugLib\cmdFlag.obj +.\abclib\DebugLib\cmdHist.obj +.\abclib\DebugLib\cmdUtils.obj +.\abclib\DebugLib\io.obj +.\abclib\DebugLib\ioRead.obj +.\abclib\DebugLib\ioReadBaf.obj +.\abclib\DebugLib\ioReadBench.obj +.\abclib\DebugLib\ioReadBlif.obj +.\abclib\DebugLib\ioReadEdif.obj +.\abclib\DebugLib\ioReadEqn.obj +.\abclib\DebugLib\ioReadPla.obj +.\abclib\DebugLib\ioReadVerilog.obj +.\abclib\DebugLib\ioUtil.obj +.\abclib\DebugLib\ioWriteBaf.obj +.\abclib\DebugLib\ioWriteBench.obj +.\abclib\DebugLib\ioWriteBlif.obj +.\abclib\DebugLib\ioWriteCnf.obj +.\abclib\DebugLib\ioWriteDot.obj +.\abclib\DebugLib\ioWriteEqn.obj +.\abclib\DebugLib\ioWriteGml.obj +.\abclib\DebugLib\ioWriteList.obj +.\abclib\DebugLib\ioWritePla.obj +.\abclib\DebugLib\libSupport.obj +.\abclib\DebugLib\main.obj +.\abclib\DebugLib\mainFrame.obj +.\abclib\DebugLib\mainInit.obj +.\abclib\DebugLib\mainUtils.obj +.\abclib\DebugLib\cuddAddAbs.obj +.\abclib\DebugLib\cuddAddApply.obj +.\abclib\DebugLib\cuddAddFind.obj +.\abclib\DebugLib\cuddAddInv.obj +.\abclib\DebugLib\cuddAddIte.obj +.\abclib\DebugLib\cuddAddNeg.obj +.\abclib\DebugLib\cuddAddWalsh.obj +.\abclib\DebugLib\cuddAndAbs.obj +.\abclib\DebugLib\cuddAnneal.obj +.\abclib\DebugLib\cuddApa.obj +.\abclib\DebugLib\cuddAPI.obj +.\abclib\DebugLib\cuddApprox.obj +.\abclib\DebugLib\cuddBddAbs.obj +.\abclib\DebugLib\cuddBddCorr.obj +.\abclib\DebugLib\cuddBddIte.obj +.\abclib\DebugLib\cuddBridge.obj +.\abclib\DebugLib\cuddCache.obj +.\abclib\DebugLib\cuddCheck.obj +.\abclib\DebugLib\cuddClip.obj +.\abclib\DebugLib\cuddCof.obj +.\abclib\DebugLib\cuddCompose.obj +.\abclib\DebugLib\cuddDecomp.obj +.\abclib\DebugLib\cuddEssent.obj +.\abclib\DebugLib\cuddExact.obj +.\abclib\DebugLib\cuddExport.obj +.\abclib\DebugLib\cuddGenCof.obj +.\abclib\DebugLib\cuddGenetic.obj +.\abclib\DebugLib\cuddGroup.obj +.\abclib\DebugLib\cuddHarwell.obj +.\abclib\DebugLib\cuddInit.obj +.\abclib\DebugLib\cuddInteract.obj +.\abclib\DebugLib\cuddLCache.obj +.\abclib\DebugLib\cuddLevelQ.obj +.\abclib\DebugLib\cuddLinear.obj +.\abclib\DebugLib\cuddLiteral.obj +.\abclib\DebugLib\cuddMatMult.obj +.\abclib\DebugLib\cuddPriority.obj +.\abclib\DebugLib\cuddRead.obj +.\abclib\DebugLib\cuddRef.obj +.\abclib\DebugLib\cuddReorder.obj +.\abclib\DebugLib\cuddSat.obj +.\abclib\DebugLib\cuddSign.obj +.\abclib\DebugLib\cuddSolve.obj +.\abclib\DebugLib\cuddSplit.obj +.\abclib\DebugLib\cuddSubsetHB.obj +.\abclib\DebugLib\cuddSubsetSP.obj +.\abclib\DebugLib\cuddSymmetry.obj +.\abclib\DebugLib\cuddTable.obj +.\abclib\DebugLib\cuddUtil.obj +.\abclib\DebugLib\cuddWindow.obj +.\abclib\DebugLib\cuddZddCount.obj +.\abclib\DebugLib\cuddZddFuncs.obj +.\abclib\DebugLib\cuddZddGroup.obj +.\abclib\DebugLib\cuddZddIsop.obj +.\abclib\DebugLib\cuddZddLin.obj +.\abclib\DebugLib\cuddZddMisc.obj +.\abclib\DebugLib\cuddZddPort.obj +.\abclib\DebugLib\cuddZddReord.obj +.\abclib\DebugLib\cuddZddSetop.obj +.\abclib\DebugLib\cuddZddSymm.obj +.\abclib\DebugLib\cuddZddUtil.obj +.\abclib\DebugLib\epd.obj +.\abclib\DebugLib\mtrBasic.obj +.\abclib\DebugLib\mtrGroup.obj +.\abclib\DebugLib\parseCore.obj +.\abclib\DebugLib\parseStack.obj +.\abclib\DebugLib\dsdApi.obj +.\abclib\DebugLib\dsdCheck.obj +.\abclib\DebugLib\dsdLocal.obj +.\abclib\DebugLib\dsdMan.obj +.\abclib\DebugLib\dsdProc.obj +.\abclib\DebugLib\dsdTree.obj +.\abclib\DebugLib\reoApi.obj +.\abclib\DebugLib\reoCore.obj +.\abclib\DebugLib\reoProfile.obj +.\abclib\DebugLib\reoSift.obj +.\abclib\DebugLib\reoSwap.obj +.\abclib\DebugLib\reoTest.obj +.\abclib\DebugLib\reoTransfer.obj +.\abclib\DebugLib\reoUnits.obj +.\abclib\DebugLib\added.obj +.\abclib\DebugLib\solver.obj +.\abclib\DebugLib\msatActivity.obj +.\abclib\DebugLib\msatClause.obj +.\abclib\DebugLib\msatClauseVec.obj +.\abclib\DebugLib\msatMem.obj +.\abclib\DebugLib\msatOrderJ.obj +.\abclib\DebugLib\msatQueue.obj +.\abclib\DebugLib\msatRead.obj +.\abclib\DebugLib\msatSolverApi.obj +.\abclib\DebugLib\msatSolverCore.obj +.\abclib\DebugLib\msatSolverIo.obj +.\abclib\DebugLib\msatSolverSearch.obj +.\abclib\DebugLib\msatSort.obj +.\abclib\DebugLib\msatVec.obj +.\abclib\DebugLib\fraigApi.obj +.\abclib\DebugLib\fraigCanon.obj +.\abclib\DebugLib\fraigFanout.obj +.\abclib\DebugLib\fraigFeed.obj +.\abclib\DebugLib\fraigMan.obj +.\abclib\DebugLib\fraigMem.obj +.\abclib\DebugLib\fraigNode.obj +.\abclib\DebugLib\fraigPrime.obj +.\abclib\DebugLib\fraigSat.obj +.\abclib\DebugLib\fraigTable.obj +.\abclib\DebugLib\fraigUtil.obj +.\abclib\DebugLib\fraigVec.obj +.\abclib\DebugLib\csat_apis.obj +.\abclib\DebugLib\fxu.obj +.\abclib\DebugLib\fxuCreate.obj +.\abclib\DebugLib\fxuHeapD.obj +.\abclib\DebugLib\fxuHeapS.obj +.\abclib\DebugLib\fxuList.obj +.\abclib\DebugLib\fxuMatrix.obj +.\abclib\DebugLib\fxuPair.obj +.\abclib\DebugLib\fxuPrint.obj +.\abclib\DebugLib\fxuReduce.obj +.\abclib\DebugLib\fxuSelect.obj +.\abclib\DebugLib\fxuSingle.obj +.\abclib\DebugLib\fxuUpdate.obj +.\abclib\DebugLib\rwrDec.obj +.\abclib\DebugLib\rwrEva.obj +.\abclib\DebugLib\rwrExp.obj +.\abclib\DebugLib\rwrLib.obj +.\abclib\DebugLib\rwrMan.obj +.\abclib\DebugLib\rwrPrint.obj +.\abclib\DebugLib\rwrUtil.obj +.\abclib\DebugLib\cutApi.obj +.\abclib\DebugLib\cutCut.obj +.\abclib\DebugLib\cutMan.obj +.\abclib\DebugLib\cutMerge.obj +.\abclib\DebugLib\cutNode.obj +.\abclib\DebugLib\cutOracle.obj +.\abclib\DebugLib\cutSeq.obj +.\abclib\DebugLib\cutTruth.obj +.\abclib\DebugLib\decAbc.obj +.\abclib\DebugLib\decFactor.obj +.\abclib\DebugLib\decMan.obj +.\abclib\DebugLib\decPrint.obj +.\abclib\DebugLib\decUtil.obj +.\abclib\DebugLib\simMan.obj +.\abclib\DebugLib\simSat.obj +.\abclib\DebugLib\simSeq.obj +.\abclib\DebugLib\simSupp.obj +.\abclib\DebugLib\simSwitch.obj +.\abclib\DebugLib\simSym.obj +.\abclib\DebugLib\simSymSat.obj +.\abclib\DebugLib\simSymSim.obj +.\abclib\DebugLib\simSymStr.obj +.\abclib\DebugLib\simUtils.obj +.\abclib\DebugLib\fpga.obj +.\abclib\DebugLib\fpgaCore.obj +.\abclib\DebugLib\fpgaCreate.obj +.\abclib\DebugLib\fpgaCut.obj +.\abclib\DebugLib\fpgaCutUtils.obj +.\abclib\DebugLib\fpgaFanout.obj +.\abclib\DebugLib\fpgaLib.obj +.\abclib\DebugLib\fpgaMatch.obj +.\abclib\DebugLib\fpgaSwitch.obj +.\abclib\DebugLib\fpgaTime.obj +.\abclib\DebugLib\fpgaTruth.obj +.\abclib\DebugLib\fpgaUtils.obj +.\abclib\DebugLib\fpgaVec.obj +.\abclib\DebugLib\mapper.obj +.\abclib\DebugLib\mapperCanon.obj +.\abclib\DebugLib\mapperCore.obj +.\abclib\DebugLib\mapperCreate.obj +.\abclib\DebugLib\mapperCut.obj +.\abclib\DebugLib\mapperCutUtils.obj +.\abclib\DebugLib\mapperFanout.obj +.\abclib\DebugLib\mapperLib.obj +.\abclib\DebugLib\mapperMatch.obj +.\abclib\DebugLib\mapperRefs.obj +.\abclib\DebugLib\mapperSuper.obj +.\abclib\DebugLib\mapperSwitch.obj +.\abclib\DebugLib\mapperTable.obj +.\abclib\DebugLib\mapperTime.obj +.\abclib\DebugLib\mapperTree.obj +.\abclib\DebugLib\mapperTruth.obj +.\abclib\DebugLib\mapperUtils.obj +.\abclib\DebugLib\mapperVec.obj +.\abclib\DebugLib\mio.obj +.\abclib\DebugLib\mioApi.obj +.\abclib\DebugLib\mioFunc.obj +.\abclib\DebugLib\mioRead.obj +.\abclib\DebugLib\mioUtils.obj +.\abclib\DebugLib\super.obj +.\abclib\DebugLib\superAnd.obj +.\abclib\DebugLib\superGate.obj +.\abclib\DebugLib\superWrite.obj +.\abclib\DebugLib\pgaCore.obj +.\abclib\DebugLib\pgaMan.obj +.\abclib\DebugLib\pgaMatch.obj +.\abclib\DebugLib\pgaUtil.obj +.\abclib\DebugLib\extraBddKmap.obj +.\abclib\DebugLib\extraBddMisc.obj +.\abclib\DebugLib\extraBddSymm.obj +.\abclib\DebugLib\extraUtilBitMatrix.obj +.\abclib\DebugLib\extraUtilCanon.obj +.\abclib\DebugLib\extraUtilFile.obj +.\abclib\DebugLib\extraUtilMemory.obj +.\abclib\DebugLib\extraUtilMisc.obj +.\abclib\DebugLib\extraUtilProgress.obj +.\abclib\DebugLib\extraUtilReader.obj +.\abclib\DebugLib\st.obj +.\abclib\DebugLib\stmm.obj +.\abclib\DebugLib\cpu_stats.obj +.\abclib\DebugLib\cpu_time.obj +.\abclib\DebugLib\datalimit.obj +.\abclib\DebugLib\getopt.obj +.\abclib\DebugLib\pathsearch.obj +.\abclib\DebugLib\safe_mem.obj +.\abclib\DebugLib\strsav.obj +.\abclib\DebugLib\texpand.obj +.\abclib\DebugLib\mvc.obj +.\abclib\DebugLib\mvcApi.obj +.\abclib\DebugLib\mvcCompare.obj +.\abclib\DebugLib\mvcContain.obj +.\abclib\DebugLib\mvcCover.obj +.\abclib\DebugLib\mvcCube.obj +.\abclib\DebugLib\mvcDivide.obj +.\abclib\DebugLib\mvcDivisor.obj +.\abclib\DebugLib\mvcList.obj +.\abclib\DebugLib\mvcLits.obj +.\abclib\DebugLib\mvcMan.obj +.\abclib\DebugLib\mvcOpAlg.obj +.\abclib\DebugLib\mvcOpBool.obj +.\abclib\DebugLib\mvcPrint.obj +.\abclib\DebugLib\mvcSort.obj +.\abclib\DebugLib\mvcUtils.obj +.\abclib\DebugLib\ioWriteVerilog.obj ] -Creating command line "link.exe -lib @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP83.tmp" +Creating command line "link.exe -lib @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F1.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 -abcVanEijk.c -abcVanImp.c -abcVerify.c -seqAigCore.c -seqAigIter.c -seqCreate.c -seqFpgaCore.c -seqFpgaIter.c -seqLatch.c -seqMan.c -seqMapCore.c -seqMapIter.c -seqRetCore.c -seqRetIter.c -seqShare.c -seqUtil.c -cmd.c -cmdAlias.c -cmdApi.c -cmdFlag.c -cmdHist.c -cmdUtils.c -io.c -ioRead.c -ioReadBaf.c -ioReadBench.c -ioReadBlif.c -ioReadEdif.c -ioReadEqn.c -ioReadPla.c -ioReadVerilog.c -ioUtil.c -ioWriteBaf.c -ioWriteBench.c -ioWriteBlif.c -ioWriteCnf.c -ioWriteDot.c -ioWriteEqn.c -ioWriteGml.c -ioWriteList.c -ioWritePla.c -libSupport.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 -cutOracle.c -cutSeq.c -cutTruth.c -decAbc.c -decFactor.c -decMan.c -decPrint.c -decUtil.c -simMan.c -simSat.c -simSeq.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 -extraBddKmap.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 +c:\_projects\abc\src\base\abci\abc.c(2890) : warning C4013: 'Abc_NtkMiterSat2' undefined; assuming extern returning int +ioWriteVerilog.c Creating library... -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F2.tmp" with contents [ -/nologo /o"abclib\ReleaseLib/abclib.bsc" -.\abclib\ReleaseLib\abcAig.sbr -.\abclib\ReleaseLib\abcCheck.sbr -.\abclib\ReleaseLib\abcDfs.sbr -.\abclib\ReleaseLib\abcFanio.sbr -.\abclib\ReleaseLib\abcFunc.sbr -.\abclib\ReleaseLib\abcLatch.sbr -.\abclib\ReleaseLib\abcMinBase.sbr -.\abclib\ReleaseLib\abcNames.sbr -.\abclib\ReleaseLib\abcNetlist.sbr -.\abclib\ReleaseLib\abcNtk.sbr -.\abclib\ReleaseLib\abcObj.sbr -.\abclib\ReleaseLib\abcRefs.sbr -.\abclib\ReleaseLib\abcShow.sbr -.\abclib\ReleaseLib\abcSop.sbr -.\abclib\ReleaseLib\abcUtil.sbr -.\abclib\ReleaseLib\abc.sbr -.\abclib\ReleaseLib\abcAttach.sbr -.\abclib\ReleaseLib\abcBalance.sbr -.\abclib\ReleaseLib\abcCollapse.sbr -.\abclib\ReleaseLib\abcCut.sbr -.\abclib\ReleaseLib\abcDsd.sbr -.\abclib\ReleaseLib\abcFpga.sbr -.\abclib\ReleaseLib\abcFraig.sbr -.\abclib\ReleaseLib\abcFxu.sbr -.\abclib\ReleaseLib\abcMap.sbr -.\abclib\ReleaseLib\abcMiter.sbr -.\abclib\ReleaseLib\abcNtbdd.sbr -.\abclib\ReleaseLib\abcPga.sbr -.\abclib\ReleaseLib\abcPrint.sbr -.\abclib\ReleaseLib\abcReconv.sbr -.\abclib\ReleaseLib\abcRefactor.sbr -.\abclib\ReleaseLib\abcRenode.sbr -.\abclib\ReleaseLib\abcRewrite.sbr -.\abclib\ReleaseLib\abcSat.sbr -.\abclib\ReleaseLib\abcStrash.sbr -.\abclib\ReleaseLib\abcSweep.sbr -.\abclib\ReleaseLib\abcSymm.sbr -.\abclib\ReleaseLib\abcTiming.sbr -.\abclib\ReleaseLib\abcUnreach.sbr -.\abclib\ReleaseLib\abcVanEijk.sbr -.\abclib\ReleaseLib\abcVanImp.sbr -.\abclib\ReleaseLib\abcVerify.sbr -.\abclib\ReleaseLib\seqAigCore.sbr -.\abclib\ReleaseLib\seqAigIter.sbr -.\abclib\ReleaseLib\seqCreate.sbr -.\abclib\ReleaseLib\seqFpgaCore.sbr -.\abclib\ReleaseLib\seqFpgaIter.sbr -.\abclib\ReleaseLib\seqLatch.sbr -.\abclib\ReleaseLib\seqMan.sbr -.\abclib\ReleaseLib\seqMapCore.sbr -.\abclib\ReleaseLib\seqMapIter.sbr -.\abclib\ReleaseLib\seqRetCore.sbr -.\abclib\ReleaseLib\seqRetIter.sbr -.\abclib\ReleaseLib\seqShare.sbr -.\abclib\ReleaseLib\seqUtil.sbr -.\abclib\ReleaseLib\cmd.sbr -.\abclib\ReleaseLib\cmdAlias.sbr -.\abclib\ReleaseLib\cmdApi.sbr -.\abclib\ReleaseLib\cmdFlag.sbr -.\abclib\ReleaseLib\cmdHist.sbr -.\abclib\ReleaseLib\cmdUtils.sbr -.\abclib\ReleaseLib\io.sbr -.\abclib\ReleaseLib\ioRead.sbr -.\abclib\ReleaseLib\ioReadBaf.sbr -.\abclib\ReleaseLib\ioReadBench.sbr -.\abclib\ReleaseLib\ioReadBlif.sbr -.\abclib\ReleaseLib\ioReadEdif.sbr -.\abclib\ReleaseLib\ioReadEqn.sbr -.\abclib\ReleaseLib\ioReadPla.sbr -.\abclib\ReleaseLib\ioReadVerilog.sbr -.\abclib\ReleaseLib\ioUtil.sbr -.\abclib\ReleaseLib\ioWriteBaf.sbr -.\abclib\ReleaseLib\ioWriteBench.sbr -.\abclib\ReleaseLib\ioWriteBlif.sbr -.\abclib\ReleaseLib\ioWriteCnf.sbr -.\abclib\ReleaseLib\ioWriteDot.sbr -.\abclib\ReleaseLib\ioWriteEqn.sbr -.\abclib\ReleaseLib\ioWriteGml.sbr -.\abclib\ReleaseLib\ioWriteList.sbr -.\abclib\ReleaseLib\ioWritePla.sbr -.\abclib\ReleaseLib\libSupport.sbr -.\abclib\ReleaseLib\main.sbr -.\abclib\ReleaseLib\mainFrame.sbr -.\abclib\ReleaseLib\mainInit.sbr -.\abclib\ReleaseLib\mainUtils.sbr -.\abclib\ReleaseLib\cuddAddAbs.sbr -.\abclib\ReleaseLib\cuddAddApply.sbr -.\abclib\ReleaseLib\cuddAddFind.sbr -.\abclib\ReleaseLib\cuddAddInv.sbr -.\abclib\ReleaseLib\cuddAddIte.sbr -.\abclib\ReleaseLib\cuddAddNeg.sbr -.\abclib\ReleaseLib\cuddAddWalsh.sbr -.\abclib\ReleaseLib\cuddAndAbs.sbr -.\abclib\ReleaseLib\cuddAnneal.sbr -.\abclib\ReleaseLib\cuddApa.sbr -.\abclib\ReleaseLib\cuddAPI.sbr -.\abclib\ReleaseLib\cuddApprox.sbr -.\abclib\ReleaseLib\cuddBddAbs.sbr -.\abclib\ReleaseLib\cuddBddCorr.sbr -.\abclib\ReleaseLib\cuddBddIte.sbr -.\abclib\ReleaseLib\cuddBridge.sbr -.\abclib\ReleaseLib\cuddCache.sbr -.\abclib\ReleaseLib\cuddCheck.sbr -.\abclib\ReleaseLib\cuddClip.sbr -.\abclib\ReleaseLib\cuddCof.sbr -.\abclib\ReleaseLib\cuddCompose.sbr -.\abclib\ReleaseLib\cuddDecomp.sbr -.\abclib\ReleaseLib\cuddEssent.sbr -.\abclib\ReleaseLib\cuddExact.sbr -.\abclib\ReleaseLib\cuddExport.sbr -.\abclib\ReleaseLib\cuddGenCof.sbr -.\abclib\ReleaseLib\cuddGenetic.sbr -.\abclib\ReleaseLib\cuddGroup.sbr -.\abclib\ReleaseLib\cuddHarwell.sbr -.\abclib\ReleaseLib\cuddInit.sbr -.\abclib\ReleaseLib\cuddInteract.sbr -.\abclib\ReleaseLib\cuddLCache.sbr -.\abclib\ReleaseLib\cuddLevelQ.sbr -.\abclib\ReleaseLib\cuddLinear.sbr -.\abclib\ReleaseLib\cuddLiteral.sbr -.\abclib\ReleaseLib\cuddMatMult.sbr -.\abclib\ReleaseLib\cuddPriority.sbr -.\abclib\ReleaseLib\cuddRead.sbr -.\abclib\ReleaseLib\cuddRef.sbr -.\abclib\ReleaseLib\cuddReorder.sbr -.\abclib\ReleaseLib\cuddSat.sbr -.\abclib\ReleaseLib\cuddSign.sbr -.\abclib\ReleaseLib\cuddSolve.sbr -.\abclib\ReleaseLib\cuddSplit.sbr -.\abclib\ReleaseLib\cuddSubsetHB.sbr -.\abclib\ReleaseLib\cuddSubsetSP.sbr -.\abclib\ReleaseLib\cuddSymmetry.sbr -.\abclib\ReleaseLib\cuddTable.sbr -.\abclib\ReleaseLib\cuddUtil.sbr -.\abclib\ReleaseLib\cuddWindow.sbr -.\abclib\ReleaseLib\cuddZddCount.sbr -.\abclib\ReleaseLib\cuddZddFuncs.sbr -.\abclib\ReleaseLib\cuddZddGroup.sbr -.\abclib\ReleaseLib\cuddZddIsop.sbr -.\abclib\ReleaseLib\cuddZddLin.sbr -.\abclib\ReleaseLib\cuddZddMisc.sbr -.\abclib\ReleaseLib\cuddZddPort.sbr -.\abclib\ReleaseLib\cuddZddReord.sbr -.\abclib\ReleaseLib\cuddZddSetop.sbr -.\abclib\ReleaseLib\cuddZddSymm.sbr -.\abclib\ReleaseLib\cuddZddUtil.sbr -.\abclib\ReleaseLib\epd.sbr -.\abclib\ReleaseLib\mtrBasic.sbr -.\abclib\ReleaseLib\mtrGroup.sbr -.\abclib\ReleaseLib\parseCore.sbr -.\abclib\ReleaseLib\parseStack.sbr -.\abclib\ReleaseLib\dsdApi.sbr -.\abclib\ReleaseLib\dsdCheck.sbr -.\abclib\ReleaseLib\dsdLocal.sbr -.\abclib\ReleaseLib\dsdMan.sbr -.\abclib\ReleaseLib\dsdProc.sbr -.\abclib\ReleaseLib\dsdTree.sbr -.\abclib\ReleaseLib\reoApi.sbr -.\abclib\ReleaseLib\reoCore.sbr -.\abclib\ReleaseLib\reoProfile.sbr -.\abclib\ReleaseLib\reoSift.sbr -.\abclib\ReleaseLib\reoSwap.sbr -.\abclib\ReleaseLib\reoTest.sbr -.\abclib\ReleaseLib\reoTransfer.sbr -.\abclib\ReleaseLib\reoUnits.sbr -.\abclib\ReleaseLib\added.sbr -.\abclib\ReleaseLib\solver.sbr -.\abclib\ReleaseLib\msatActivity.sbr -.\abclib\ReleaseLib\msatClause.sbr -.\abclib\ReleaseLib\msatClauseVec.sbr -.\abclib\ReleaseLib\msatMem.sbr -.\abclib\ReleaseLib\msatOrderJ.sbr -.\abclib\ReleaseLib\msatQueue.sbr -.\abclib\ReleaseLib\msatRead.sbr -.\abclib\ReleaseLib\msatSolverApi.sbr -.\abclib\ReleaseLib\msatSolverCore.sbr -.\abclib\ReleaseLib\msatSolverIo.sbr -.\abclib\ReleaseLib\msatSolverSearch.sbr -.\abclib\ReleaseLib\msatSort.sbr -.\abclib\ReleaseLib\msatVec.sbr -.\abclib\ReleaseLib\fraigApi.sbr -.\abclib\ReleaseLib\fraigCanon.sbr -.\abclib\ReleaseLib\fraigFanout.sbr -.\abclib\ReleaseLib\fraigFeed.sbr -.\abclib\ReleaseLib\fraigMan.sbr -.\abclib\ReleaseLib\fraigMem.sbr -.\abclib\ReleaseLib\fraigNode.sbr -.\abclib\ReleaseLib\fraigPrime.sbr -.\abclib\ReleaseLib\fraigSat.sbr -.\abclib\ReleaseLib\fraigTable.sbr -.\abclib\ReleaseLib\fraigUtil.sbr -.\abclib\ReleaseLib\fraigVec.sbr -.\abclib\ReleaseLib\csat_apis.sbr -.\abclib\ReleaseLib\fxu.sbr -.\abclib\ReleaseLib\fxuCreate.sbr -.\abclib\ReleaseLib\fxuHeapD.sbr -.\abclib\ReleaseLib\fxuHeapS.sbr -.\abclib\ReleaseLib\fxuList.sbr -.\abclib\ReleaseLib\fxuMatrix.sbr -.\abclib\ReleaseLib\fxuPair.sbr -.\abclib\ReleaseLib\fxuPrint.sbr -.\abclib\ReleaseLib\fxuReduce.sbr -.\abclib\ReleaseLib\fxuSelect.sbr -.\abclib\ReleaseLib\fxuSingle.sbr -.\abclib\ReleaseLib\fxuUpdate.sbr -.\abclib\ReleaseLib\rwrDec.sbr -.\abclib\ReleaseLib\rwrEva.sbr -.\abclib\ReleaseLib\rwrExp.sbr -.\abclib\ReleaseLib\rwrLib.sbr -.\abclib\ReleaseLib\rwrMan.sbr -.\abclib\ReleaseLib\rwrPrint.sbr -.\abclib\ReleaseLib\rwrUtil.sbr -.\abclib\ReleaseLib\cutApi.sbr -.\abclib\ReleaseLib\cutCut.sbr -.\abclib\ReleaseLib\cutMan.sbr -.\abclib\ReleaseLib\cutMerge.sbr -.\abclib\ReleaseLib\cutNode.sbr -.\abclib\ReleaseLib\cutOracle.sbr -.\abclib\ReleaseLib\cutSeq.sbr -.\abclib\ReleaseLib\cutTruth.sbr -.\abclib\ReleaseLib\decAbc.sbr -.\abclib\ReleaseLib\decFactor.sbr -.\abclib\ReleaseLib\decMan.sbr -.\abclib\ReleaseLib\decPrint.sbr -.\abclib\ReleaseLib\decUtil.sbr -.\abclib\ReleaseLib\simMan.sbr -.\abclib\ReleaseLib\simSat.sbr -.\abclib\ReleaseLib\simSeq.sbr -.\abclib\ReleaseLib\simSupp.sbr -.\abclib\ReleaseLib\simSwitch.sbr -.\abclib\ReleaseLib\simSym.sbr -.\abclib\ReleaseLib\simSymSat.sbr -.\abclib\ReleaseLib\simSymSim.sbr -.\abclib\ReleaseLib\simSymStr.sbr -.\abclib\ReleaseLib\simUtils.sbr -.\abclib\ReleaseLib\fpga.sbr -.\abclib\ReleaseLib\fpgaCore.sbr -.\abclib\ReleaseLib\fpgaCreate.sbr -.\abclib\ReleaseLib\fpgaCut.sbr -.\abclib\ReleaseLib\fpgaCutUtils.sbr -.\abclib\ReleaseLib\fpgaFanout.sbr -.\abclib\ReleaseLib\fpgaLib.sbr -.\abclib\ReleaseLib\fpgaMatch.sbr -.\abclib\ReleaseLib\fpgaSwitch.sbr -.\abclib\ReleaseLib\fpgaTime.sbr -.\abclib\ReleaseLib\fpgaTruth.sbr -.\abclib\ReleaseLib\fpgaUtils.sbr -.\abclib\ReleaseLib\fpgaVec.sbr -.\abclib\ReleaseLib\mapper.sbr -.\abclib\ReleaseLib\mapperCanon.sbr -.\abclib\ReleaseLib\mapperCore.sbr -.\abclib\ReleaseLib\mapperCreate.sbr -.\abclib\ReleaseLib\mapperCut.sbr -.\abclib\ReleaseLib\mapperCutUtils.sbr -.\abclib\ReleaseLib\mapperFanout.sbr -.\abclib\ReleaseLib\mapperLib.sbr -.\abclib\ReleaseLib\mapperMatch.sbr -.\abclib\ReleaseLib\mapperRefs.sbr -.\abclib\ReleaseLib\mapperSuper.sbr -.\abclib\ReleaseLib\mapperSwitch.sbr -.\abclib\ReleaseLib\mapperTable.sbr -.\abclib\ReleaseLib\mapperTime.sbr -.\abclib\ReleaseLib\mapperTree.sbr -.\abclib\ReleaseLib\mapperTruth.sbr -.\abclib\ReleaseLib\mapperUtils.sbr -.\abclib\ReleaseLib\mapperVec.sbr -.\abclib\ReleaseLib\mio.sbr -.\abclib\ReleaseLib\mioApi.sbr -.\abclib\ReleaseLib\mioFunc.sbr -.\abclib\ReleaseLib\mioRead.sbr -.\abclib\ReleaseLib\mioUtils.sbr -.\abclib\ReleaseLib\super.sbr -.\abclib\ReleaseLib\superAnd.sbr -.\abclib\ReleaseLib\superGate.sbr -.\abclib\ReleaseLib\superWrite.sbr -.\abclib\ReleaseLib\pgaCore.sbr -.\abclib\ReleaseLib\pgaMan.sbr -.\abclib\ReleaseLib\pgaMatch.sbr -.\abclib\ReleaseLib\pgaUtil.sbr -.\abclib\ReleaseLib\extraBddKmap.sbr -.\abclib\ReleaseLib\extraBddMisc.sbr -.\abclib\ReleaseLib\extraBddSymm.sbr -.\abclib\ReleaseLib\extraUtilBitMatrix.sbr -.\abclib\ReleaseLib\extraUtilCanon.sbr -.\abclib\ReleaseLib\extraUtilFile.sbr -.\abclib\ReleaseLib\extraUtilMemory.sbr -.\abclib\ReleaseLib\extraUtilMisc.sbr -.\abclib\ReleaseLib\extraUtilProgress.sbr -.\abclib\ReleaseLib\extraUtilReader.sbr -.\abclib\ReleaseLib\st.sbr -.\abclib\ReleaseLib\stmm.sbr -.\abclib\ReleaseLib\cpu_stats.sbr -.\abclib\ReleaseLib\cpu_time.sbr -.\abclib\ReleaseLib\datalimit.sbr -.\abclib\ReleaseLib\getopt.sbr -.\abclib\ReleaseLib\pathsearch.sbr -.\abclib\ReleaseLib\safe_mem.sbr -.\abclib\ReleaseLib\strsav.sbr -.\abclib\ReleaseLib\texpand.sbr -.\abclib\ReleaseLib\mvc.sbr -.\abclib\ReleaseLib\mvcApi.sbr -.\abclib\ReleaseLib\mvcCompare.sbr -.\abclib\ReleaseLib\mvcContain.sbr -.\abclib\ReleaseLib\mvcCover.sbr -.\abclib\ReleaseLib\mvcCube.sbr -.\abclib\ReleaseLib\mvcDivide.sbr -.\abclib\ReleaseLib\mvcDivisor.sbr -.\abclib\ReleaseLib\mvcList.sbr -.\abclib\ReleaseLib\mvcLits.sbr -.\abclib\ReleaseLib\mvcMan.sbr -.\abclib\ReleaseLib\mvcOpAlg.sbr -.\abclib\ReleaseLib\mvcOpBool.sbr -.\abclib\ReleaseLib\mvcPrint.sbr -.\abclib\ReleaseLib\mvcSort.sbr -.\abclib\ReleaseLib\mvcUtils.sbr] -Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84.tmp" +/nologo /o"abclib\DebugLib/abclib.bsc" +.\abclib\DebugLib\abcAig.sbr +.\abclib\DebugLib\abcCheck.sbr +.\abclib\DebugLib\abcDfs.sbr +.\abclib\DebugLib\abcFanio.sbr +.\abclib\DebugLib\abcFunc.sbr +.\abclib\DebugLib\abcLatch.sbr +.\abclib\DebugLib\abcMinBase.sbr +.\abclib\DebugLib\abcNames.sbr +.\abclib\DebugLib\abcNetlist.sbr +.\abclib\DebugLib\abcNtk.sbr +.\abclib\DebugLib\abcObj.sbr +.\abclib\DebugLib\abcRefs.sbr +.\abclib\DebugLib\abcShow.sbr +.\abclib\DebugLib\abcSop.sbr +.\abclib\DebugLib\abcUtil.sbr +.\abclib\DebugLib\abc.sbr +.\abclib\DebugLib\abcAttach.sbr +.\abclib\DebugLib\abcBalance.sbr +.\abclib\DebugLib\abcCollapse.sbr +.\abclib\DebugLib\abcCut.sbr +.\abclib\DebugLib\abcDsd.sbr +.\abclib\DebugLib\abcFpga.sbr +.\abclib\DebugLib\abcFraig.sbr +.\abclib\DebugLib\abcFxu.sbr +.\abclib\DebugLib\abcMap.sbr +.\abclib\DebugLib\abcMiter.sbr +.\abclib\DebugLib\abcNtbdd.sbr +.\abclib\DebugLib\abcPga.sbr +.\abclib\DebugLib\abcPrint.sbr +.\abclib\DebugLib\abcReconv.sbr +.\abclib\DebugLib\abcRefactor.sbr +.\abclib\DebugLib\abcRenode.sbr +.\abclib\DebugLib\abcRewrite.sbr +.\abclib\DebugLib\abcSat.sbr +.\abclib\DebugLib\abcStrash.sbr +.\abclib\DebugLib\abcSweep.sbr +.\abclib\DebugLib\abcSymm.sbr +.\abclib\DebugLib\abcTiming.sbr +.\abclib\DebugLib\abcUnreach.sbr +.\abclib\DebugLib\abcVanEijk.sbr +.\abclib\DebugLib\abcVanImp.sbr +.\abclib\DebugLib\abcVerify.sbr +.\abclib\DebugLib\seqAigCore.sbr +.\abclib\DebugLib\seqAigIter.sbr +.\abclib\DebugLib\seqCreate.sbr +.\abclib\DebugLib\seqFpgaCore.sbr +.\abclib\DebugLib\seqFpgaIter.sbr +.\abclib\DebugLib\seqLatch.sbr +.\abclib\DebugLib\seqMan.sbr +.\abclib\DebugLib\seqMapCore.sbr +.\abclib\DebugLib\seqMapIter.sbr +.\abclib\DebugLib\seqRetCore.sbr +.\abclib\DebugLib\seqRetIter.sbr +.\abclib\DebugLib\seqShare.sbr +.\abclib\DebugLib\seqUtil.sbr +.\abclib\DebugLib\cmd.sbr +.\abclib\DebugLib\cmdAlias.sbr +.\abclib\DebugLib\cmdApi.sbr +.\abclib\DebugLib\cmdFlag.sbr +.\abclib\DebugLib\cmdHist.sbr +.\abclib\DebugLib\cmdUtils.sbr +.\abclib\DebugLib\io.sbr +.\abclib\DebugLib\ioRead.sbr +.\abclib\DebugLib\ioReadBaf.sbr +.\abclib\DebugLib\ioReadBench.sbr +.\abclib\DebugLib\ioReadBlif.sbr +.\abclib\DebugLib\ioReadEdif.sbr +.\abclib\DebugLib\ioReadEqn.sbr +.\abclib\DebugLib\ioReadPla.sbr +.\abclib\DebugLib\ioReadVerilog.sbr +.\abclib\DebugLib\ioUtil.sbr +.\abclib\DebugLib\ioWriteBaf.sbr +.\abclib\DebugLib\ioWriteBench.sbr +.\abclib\DebugLib\ioWriteBlif.sbr +.\abclib\DebugLib\ioWriteCnf.sbr +.\abclib\DebugLib\ioWriteDot.sbr +.\abclib\DebugLib\ioWriteEqn.sbr +.\abclib\DebugLib\ioWriteGml.sbr +.\abclib\DebugLib\ioWriteList.sbr +.\abclib\DebugLib\ioWritePla.sbr +.\abclib\DebugLib\libSupport.sbr +.\abclib\DebugLib\main.sbr +.\abclib\DebugLib\mainFrame.sbr +.\abclib\DebugLib\mainInit.sbr +.\abclib\DebugLib\mainUtils.sbr +.\abclib\DebugLib\cuddAddAbs.sbr +.\abclib\DebugLib\cuddAddApply.sbr +.\abclib\DebugLib\cuddAddFind.sbr +.\abclib\DebugLib\cuddAddInv.sbr +.\abclib\DebugLib\cuddAddIte.sbr +.\abclib\DebugLib\cuddAddNeg.sbr +.\abclib\DebugLib\cuddAddWalsh.sbr +.\abclib\DebugLib\cuddAndAbs.sbr +.\abclib\DebugLib\cuddAnneal.sbr +.\abclib\DebugLib\cuddApa.sbr +.\abclib\DebugLib\cuddAPI.sbr +.\abclib\DebugLib\cuddApprox.sbr +.\abclib\DebugLib\cuddBddAbs.sbr +.\abclib\DebugLib\cuddBddCorr.sbr +.\abclib\DebugLib\cuddBddIte.sbr +.\abclib\DebugLib\cuddBridge.sbr +.\abclib\DebugLib\cuddCache.sbr +.\abclib\DebugLib\cuddCheck.sbr +.\abclib\DebugLib\cuddClip.sbr +.\abclib\DebugLib\cuddCof.sbr +.\abclib\DebugLib\cuddCompose.sbr +.\abclib\DebugLib\cuddDecomp.sbr +.\abclib\DebugLib\cuddEssent.sbr +.\abclib\DebugLib\cuddExact.sbr +.\abclib\DebugLib\cuddExport.sbr +.\abclib\DebugLib\cuddGenCof.sbr +.\abclib\DebugLib\cuddGenetic.sbr +.\abclib\DebugLib\cuddGroup.sbr +.\abclib\DebugLib\cuddHarwell.sbr +.\abclib\DebugLib\cuddInit.sbr +.\abclib\DebugLib\cuddInteract.sbr +.\abclib\DebugLib\cuddLCache.sbr +.\abclib\DebugLib\cuddLevelQ.sbr +.\abclib\DebugLib\cuddLinear.sbr +.\abclib\DebugLib\cuddLiteral.sbr +.\abclib\DebugLib\cuddMatMult.sbr +.\abclib\DebugLib\cuddPriority.sbr +.\abclib\DebugLib\cuddRead.sbr +.\abclib\DebugLib\cuddRef.sbr +.\abclib\DebugLib\cuddReorder.sbr +.\abclib\DebugLib\cuddSat.sbr +.\abclib\DebugLib\cuddSign.sbr +.\abclib\DebugLib\cuddSolve.sbr +.\abclib\DebugLib\cuddSplit.sbr +.\abclib\DebugLib\cuddSubsetHB.sbr +.\abclib\DebugLib\cuddSubsetSP.sbr +.\abclib\DebugLib\cuddSymmetry.sbr +.\abclib\DebugLib\cuddTable.sbr +.\abclib\DebugLib\cuddUtil.sbr +.\abclib\DebugLib\cuddWindow.sbr +.\abclib\DebugLib\cuddZddCount.sbr +.\abclib\DebugLib\cuddZddFuncs.sbr +.\abclib\DebugLib\cuddZddGroup.sbr +.\abclib\DebugLib\cuddZddIsop.sbr +.\abclib\DebugLib\cuddZddLin.sbr +.\abclib\DebugLib\cuddZddMisc.sbr +.\abclib\DebugLib\cuddZddPort.sbr +.\abclib\DebugLib\cuddZddReord.sbr +.\abclib\DebugLib\cuddZddSetop.sbr +.\abclib\DebugLib\cuddZddSymm.sbr +.\abclib\DebugLib\cuddZddUtil.sbr +.\abclib\DebugLib\epd.sbr +.\abclib\DebugLib\mtrBasic.sbr +.\abclib\DebugLib\mtrGroup.sbr +.\abclib\DebugLib\parseCore.sbr +.\abclib\DebugLib\parseStack.sbr +.\abclib\DebugLib\dsdApi.sbr +.\abclib\DebugLib\dsdCheck.sbr +.\abclib\DebugLib\dsdLocal.sbr +.\abclib\DebugLib\dsdMan.sbr +.\abclib\DebugLib\dsdProc.sbr +.\abclib\DebugLib\dsdTree.sbr +.\abclib\DebugLib\reoApi.sbr +.\abclib\DebugLib\reoCore.sbr +.\abclib\DebugLib\reoProfile.sbr +.\abclib\DebugLib\reoSift.sbr +.\abclib\DebugLib\reoSwap.sbr +.\abclib\DebugLib\reoTest.sbr +.\abclib\DebugLib\reoTransfer.sbr +.\abclib\DebugLib\reoUnits.sbr +.\abclib\DebugLib\added.sbr +.\abclib\DebugLib\solver.sbr +.\abclib\DebugLib\msatActivity.sbr +.\abclib\DebugLib\msatClause.sbr +.\abclib\DebugLib\msatClauseVec.sbr +.\abclib\DebugLib\msatMem.sbr +.\abclib\DebugLib\msatOrderJ.sbr +.\abclib\DebugLib\msatQueue.sbr +.\abclib\DebugLib\msatRead.sbr +.\abclib\DebugLib\msatSolverApi.sbr +.\abclib\DebugLib\msatSolverCore.sbr +.\abclib\DebugLib\msatSolverIo.sbr +.\abclib\DebugLib\msatSolverSearch.sbr +.\abclib\DebugLib\msatSort.sbr +.\abclib\DebugLib\msatVec.sbr +.\abclib\DebugLib\fraigApi.sbr +.\abclib\DebugLib\fraigCanon.sbr +.\abclib\DebugLib\fraigFanout.sbr +.\abclib\DebugLib\fraigFeed.sbr +.\abclib\DebugLib\fraigMan.sbr +.\abclib\DebugLib\fraigMem.sbr +.\abclib\DebugLib\fraigNode.sbr +.\abclib\DebugLib\fraigPrime.sbr +.\abclib\DebugLib\fraigSat.sbr +.\abclib\DebugLib\fraigTable.sbr +.\abclib\DebugLib\fraigUtil.sbr +.\abclib\DebugLib\fraigVec.sbr +.\abclib\DebugLib\csat_apis.sbr +.\abclib\DebugLib\fxu.sbr +.\abclib\DebugLib\fxuCreate.sbr +.\abclib\DebugLib\fxuHeapD.sbr +.\abclib\DebugLib\fxuHeapS.sbr +.\abclib\DebugLib\fxuList.sbr +.\abclib\DebugLib\fxuMatrix.sbr +.\abclib\DebugLib\fxuPair.sbr +.\abclib\DebugLib\fxuPrint.sbr +.\abclib\DebugLib\fxuReduce.sbr +.\abclib\DebugLib\fxuSelect.sbr +.\abclib\DebugLib\fxuSingle.sbr +.\abclib\DebugLib\fxuUpdate.sbr +.\abclib\DebugLib\rwrDec.sbr +.\abclib\DebugLib\rwrEva.sbr +.\abclib\DebugLib\rwrExp.sbr +.\abclib\DebugLib\rwrLib.sbr +.\abclib\DebugLib\rwrMan.sbr +.\abclib\DebugLib\rwrPrint.sbr +.\abclib\DebugLib\rwrUtil.sbr +.\abclib\DebugLib\cutApi.sbr +.\abclib\DebugLib\cutCut.sbr +.\abclib\DebugLib\cutMan.sbr +.\abclib\DebugLib\cutMerge.sbr +.\abclib\DebugLib\cutNode.sbr +.\abclib\DebugLib\cutOracle.sbr +.\abclib\DebugLib\cutSeq.sbr +.\abclib\DebugLib\cutTruth.sbr +.\abclib\DebugLib\decAbc.sbr +.\abclib\DebugLib\decFactor.sbr +.\abclib\DebugLib\decMan.sbr +.\abclib\DebugLib\decPrint.sbr +.\abclib\DebugLib\decUtil.sbr +.\abclib\DebugLib\simMan.sbr +.\abclib\DebugLib\simSat.sbr +.\abclib\DebugLib\simSeq.sbr +.\abclib\DebugLib\simSupp.sbr +.\abclib\DebugLib\simSwitch.sbr +.\abclib\DebugLib\simSym.sbr +.\abclib\DebugLib\simSymSat.sbr +.\abclib\DebugLib\simSymSim.sbr +.\abclib\DebugLib\simSymStr.sbr +.\abclib\DebugLib\simUtils.sbr +.\abclib\DebugLib\fpga.sbr +.\abclib\DebugLib\fpgaCore.sbr +.\abclib\DebugLib\fpgaCreate.sbr +.\abclib\DebugLib\fpgaCut.sbr +.\abclib\DebugLib\fpgaCutUtils.sbr +.\abclib\DebugLib\fpgaFanout.sbr +.\abclib\DebugLib\fpgaLib.sbr +.\abclib\DebugLib\fpgaMatch.sbr +.\abclib\DebugLib\fpgaSwitch.sbr +.\abclib\DebugLib\fpgaTime.sbr +.\abclib\DebugLib\fpgaTruth.sbr +.\abclib\DebugLib\fpgaUtils.sbr +.\abclib\DebugLib\fpgaVec.sbr +.\abclib\DebugLib\mapper.sbr +.\abclib\DebugLib\mapperCanon.sbr +.\abclib\DebugLib\mapperCore.sbr +.\abclib\DebugLib\mapperCreate.sbr +.\abclib\DebugLib\mapperCut.sbr +.\abclib\DebugLib\mapperCutUtils.sbr +.\abclib\DebugLib\mapperFanout.sbr +.\abclib\DebugLib\mapperLib.sbr +.\abclib\DebugLib\mapperMatch.sbr +.\abclib\DebugLib\mapperRefs.sbr +.\abclib\DebugLib\mapperSuper.sbr +.\abclib\DebugLib\mapperSwitch.sbr +.\abclib\DebugLib\mapperTable.sbr +.\abclib\DebugLib\mapperTime.sbr +.\abclib\DebugLib\mapperTree.sbr +.\abclib\DebugLib\mapperTruth.sbr +.\abclib\DebugLib\mapperUtils.sbr +.\abclib\DebugLib\mapperVec.sbr +.\abclib\DebugLib\mio.sbr +.\abclib\DebugLib\mioApi.sbr +.\abclib\DebugLib\mioFunc.sbr +.\abclib\DebugLib\mioRead.sbr +.\abclib\DebugLib\mioUtils.sbr +.\abclib\DebugLib\super.sbr +.\abclib\DebugLib\superAnd.sbr +.\abclib\DebugLib\superGate.sbr +.\abclib\DebugLib\superWrite.sbr +.\abclib\DebugLib\pgaCore.sbr +.\abclib\DebugLib\pgaMan.sbr +.\abclib\DebugLib\pgaMatch.sbr +.\abclib\DebugLib\pgaUtil.sbr +.\abclib\DebugLib\extraBddKmap.sbr +.\abclib\DebugLib\extraBddMisc.sbr +.\abclib\DebugLib\extraBddSymm.sbr +.\abclib\DebugLib\extraUtilBitMatrix.sbr +.\abclib\DebugLib\extraUtilCanon.sbr +.\abclib\DebugLib\extraUtilFile.sbr +.\abclib\DebugLib\extraUtilMemory.sbr +.\abclib\DebugLib\extraUtilMisc.sbr +.\abclib\DebugLib\extraUtilProgress.sbr +.\abclib\DebugLib\extraUtilReader.sbr +.\abclib\DebugLib\st.sbr +.\abclib\DebugLib\stmm.sbr +.\abclib\DebugLib\cpu_stats.sbr +.\abclib\DebugLib\cpu_time.sbr +.\abclib\DebugLib\datalimit.sbr +.\abclib\DebugLib\getopt.sbr +.\abclib\DebugLib\pathsearch.sbr +.\abclib\DebugLib\safe_mem.sbr +.\abclib\DebugLib\strsav.sbr +.\abclib\DebugLib\texpand.sbr +.\abclib\DebugLib\mvc.sbr +.\abclib\DebugLib\mvcApi.sbr +.\abclib\DebugLib\mvcCompare.sbr +.\abclib\DebugLib\mvcContain.sbr +.\abclib\DebugLib\mvcCover.sbr +.\abclib\DebugLib\mvcCube.sbr +.\abclib\DebugLib\mvcDivide.sbr +.\abclib\DebugLib\mvcDivisor.sbr +.\abclib\DebugLib\mvcList.sbr +.\abclib\DebugLib\mvcLits.sbr +.\abclib\DebugLib\mvcMan.sbr +.\abclib\DebugLib\mvcOpAlg.sbr +.\abclib\DebugLib\mvcOpBool.sbr +.\abclib\DebugLib\mvcPrint.sbr +.\abclib\DebugLib\mvcSort.sbr +.\abclib\DebugLib\mvcUtils.sbr +.\abclib\DebugLib\ioWriteVerilog.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F2.tmp" Creating browse info file... <h3>Output Window</h3> <h3>Results</h3> -abclib_release.lib - 0 error(s), 15 warning(s) +abclib_debug.lib - 0 error(s), 1 warning(s) </pre> </body> </html> diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index e0a27f9a..cbdf87c7 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -211,7 +211,7 @@ struct Abc_Ntk_t_ // transforming floats into ints and back static inline int Abc_Float2Int( float Val ) { return *((int *)&Val); } static inline float Abc_Int2Float( int Num ) { return *((float *)&Num); } -static inline int Abc_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); } +static inline int Abc_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); } // checking the network type static inline bool Abc_NtkIsNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_NETLIST; } @@ -487,6 +487,8 @@ extern int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode ); /*=== abcMiter.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); extern Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 ); +extern Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist ); +extern Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk ); extern int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter ); extern void Abc_NtkMiterReport( Abc_Ntk_t * pMiter ); extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 70cd2e6c..259187bf 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3745,7 +3745,9 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) } // run the command - pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose ); +// pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose ); + pNtkRes = NULL; + if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -3811,7 +3813,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - Abc_NtkTestEsop( pNtk ); +// Abc_NtkTestEsop( pNtk ); // Abc_NtkTestSop( pNtk ); // printf( "This command is currently not used.\n" ); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index b5338127..44130a20 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -350,6 +350,94 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In } +/**Function************************************************************* + + Synopsis [Derives the miter of two cofactors of one output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist ) +{ + Abc_Ntk_t * pNtkMiter; + Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter; + + assert( Abc_NtkIsStrash(pNtk) ); + assert( 1 == Abc_NtkCoNum(pNtk) ); + assert( In < Abc_NtkCiNum(pNtk) ); + + // start the new network + pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); + pNtkMiter->pName = util_strsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) ); + + // get the root output + pRoot = Abc_NtkCo( pNtk, 0 ); + + // perform strashing + Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 ); + // set the first cofactor + Abc_NtkCi(pNtk, In)->pCopy = Abc_ObjNot( Abc_NtkConst1(pNtkMiter) ); + // add the first cofactor + Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); + // save the output + pOutput1 = Abc_ObjFanin0(pRoot)->pCopy; + + // set the second cofactor + Abc_NtkCi(pNtk, In)->pCopy = Abc_NtkConst1( pNtkMiter ); + // add the second cofactor + Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); + // save the output + pOutput2 = Abc_ObjFanin0(pRoot)->pCopy; + + // create the miter of the two outputs + if ( fExist ) + pMiter = Abc_AigOr( pNtkMiter->pManFunc, pOutput1, pOutput2 ); + else + pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 ); + Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter ); + + // make sure that everything is okay + if ( !Abc_NtkCheck( pNtkMiter ) ) + { + printf( "Abc_NtkMiter: The network check has failed.\n" ); + Abc_NtkDelete( pNtkMiter ); + return NULL; + } + return pNtkMiter; +} + +/**Function************************************************************* + + Synopsis [Derives the miter of two cofactors of one output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkTemp; + Abc_Obj_t * pObj; + int i; + + Abc_NtkForEachPi( pNtk, pObj, i ) + { + if ( Abc_ObjFanoutNum(pObj) == 0 ) + continue; + pNtk = Abc_NtkMiterQuantify( pNtkTemp = pNtk, i, 1 ); + Abc_NtkDelete( pNtkTemp ); + } + + return pNtk; +} + diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h new file mode 100644 index 00000000..009a17bb --- /dev/null +++ b/src/sat/aig/aig.h @@ -0,0 +1,308 @@ +/**CFile**************************************************************** + + FileName [aig.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __AIG_H__ +#define __AIG_H__ + +/* + AIG is an And-Inv Graph with structural hashing. + It is always structurally hashed. It means that at any time: + - for each AND gate, there are no other AND gates with the same children + - the constants are propagated + - there is no single-input nodes (inverters/buffers) + Additionally the following invariants are satisfied: + - there are no dangling nodes (the nodes without fanout) + - the level of each AND gate reflects the levels of this fanins + - the AND nodes are in the topological order + - the constant 1 node has always number 0 in the object list + The operations that are performed on AIGs: + - building new nodes (Aig_And) + - performing elementary Boolean operations (Aig_Or, Aig_Xor, etc) + - replacing one node by another (Abc_AigReplace) + - propagating constants (Abc_AigReplace) + - deleting dangling nodes (Abc_AigDelete) + When AIG is duplicated, the new graph is structurally hashed too. + If this repeated hashing leads to fewer nodes, it means the original + AIG was not strictly hashed (one of the conditions above is violated). +*/ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include "vec.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//typedef int bool; +#ifndef bool +#define bool int +#endif + +typedef struct Aig_Param_t_ Aig_Param_t; +typedef struct Aig_Man_t_ Aig_Man_t; +typedef struct Aig_Node_t_ Aig_Node_t; +typedef struct Aig_Edge_t_ Aig_Edge_t; +typedef struct Aig_MemFixed_t_ Aig_MemFixed_t; +typedef struct Aig_SimInfo_t_ Aig_SimInfo_t; +typedef struct Aig_Table_t_ Aig_Table_t; + +// network types +typedef enum { + AIG_NONE = 0, // 0: unknown + AIG_PI, // 1: primary input + AIG_PO, // 2: primary output + AIG_AND // 3: internal node +} Aig_NodeType_t; + +// the AIG parameters +struct Aig_Param_t_ +{ + int nPatsRand; // the number of random patterns + int nBTLimit; // backtrack limit at the intermediate nodes + int nSeconds; // the runtime limit at the final miter +}; + +// the AIG edge +struct Aig_Edge_t_ +{ + unsigned iNode : 31; // the node + unsigned fComp : 1; // the complemented attribute +}; + +// the AIG node +struct Aig_Node_t_ // 8 words +{ + // various numbers associated with the node + int Id; // the unique number (SAT var number) of this node + int nRefs; // the reference counter + unsigned Type : 2; // the node type + unsigned fPhase : 1; // the phase of this node + unsigned fMarkA : 1; // the mask + unsigned fMarkB : 1; // the mask + unsigned fMarkC : 1; // the mask + unsigned TravId : 26; // the traversal ID + unsigned Level : 16; // the direct level of the node + unsigned LevelR : 16; // the reverse level of the node + Aig_Edge_t Fans[2]; // the fanins + int NextH; // next node in the hash table + int Data; // miscelleneous data + Aig_Man_t * pMan; // the parent manager +}; + +// the AIG manager +struct Aig_Man_t_ +{ + // the AIG parameters + Aig_Param_t Param; // the full set of AIG parameters + Aig_Param_t * pParam; // the pointer to the above set + // the nodes + Aig_Node_t * pConst1; // the constant 1 node (ID=0) + Vec_Ptr_t * vNodes; // all nodes by ID + Vec_Ptr_t * vPis; // all PIs + Vec_Ptr_t * vPos; // all POs + Aig_Table_t * pTable; // structural hash table + int nLevelMax; // the maximum level + // fanout representation + Vec_Ptr_t * vFanPivots; // fanout pivots + Vec_Ptr_t * vFanFans0; // the next fanout of the first fanin + Vec_Ptr_t * vFanFans1; // the next fanout of the second fanin + // the memory managers + Aig_MemFixed_t * mmNodes; // the memory manager for nodes + int nTravIds; // the traversal ID + // simulation info + Aig_SimInfo_t * pInfo; // random and systematic sim info for PIs + Aig_SimInfo_t * pInfoTemp; // temporary sim info for all nodes + // simulation patterns + int nPiWords; // the number of words in the PI info + int nPatsMax; // the max number of patterns + Vec_Ptr_t * vPats; // simulation patterns to try + // equivalence classes + Vec_Vec_t * vClasses; // the non-trival equivalence classes of nodes + // temporary data + Vec_Ptr_t * vFanouts; // temporary storage for fanouts of a node + Vec_Ptr_t * vToReplace; // the nodes to replace +}; + +// the AIG simulation info +struct Aig_SimInfo_t_ +{ + int Type; // the type (0 = PI, 1 = all) + int nNodes; // the number of nodes for which allocated + int nWords; // the number of words for each node + int nPatsMax; // the maximum number of patterns + int nPatsCur; // the current number of patterns + unsigned * pData; // the simulation data +}; + +// iterators over nodes, PIs, POs, ANDs +#define Aig_ManForEachNode( pMan, pNode, i ) \ + for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ ) +#define Aig_ManForEachPi( pMan, pNode, i ) \ + for ( i = 0; (i < Aig_ManPiNum(pMan)) && (((pNode) = Aig_ManPi(pMan, i)), 1); i++ ) +#define Aig_ManForEachPo( pMan, pNode, i ) \ + for ( i = 0; (i < Aig_ManPoNum(pMan)) && (((pNode) = Aig_ManPo(pMan, i)), 1); i++ ) +#define Aig_ManForEachAnd( pNtk, pNode, i ) \ + for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ ) \ + if ( Aig_NodeIsAnd(pNode) ) {} else + +// maximum/minimum operators +#define AIG_MIN(a,b) (((a) < (b))? (a) : (b)) +#define AIG_MAX(a,b) (((a) > (b))? (a) : (b)) + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); } + +static inline Aig_Node_t * Aig_ManNode( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vNodes, i); } +static inline Aig_Node_t * Aig_ManPi( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPis, i); } +static inline Aig_Node_t * Aig_ManPo( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPos, i); } + +static inline int Aig_ManNodeNum( Aig_Man_t * pMan ) { return Vec_PtrSize(pMan->vNodes); } +static inline int Aig_ManPiNum( Aig_Man_t * pMan ) { return Vec_PtrSize(pMan->vPis); } +static inline int Aig_ManPoNum( Aig_Man_t * pMan ) { return Vec_PtrSize(pMan->vPos); } +static inline int Aig_ManAndNum( Aig_Man_t * pMan ) { return Aig_ManNodeNum(pMan)-Aig_ManPiNum(pMan)-Aig_ManPoNum(pMan)-1; } + +static inline Aig_Node_t * Aig_Regular( Aig_Node_t * p ) { return (Aig_Node_t *)((unsigned)(p) & ~01); } +static inline Aig_Node_t * Aig_Not( Aig_Node_t * p ) { return (Aig_Node_t *)((unsigned)(p) ^ 01); } +static inline Aig_Node_t * Aig_NotCond( Aig_Node_t * p, int c ) { return (Aig_Node_t *)((unsigned)(p) ^ (c)); } +static inline bool Aig_IsComplement( Aig_Node_t * p ) { return (bool)(((unsigned)p) & 01); } + +static inline bool Aig_NodeIsConst( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Id == 0; } +static inline bool Aig_NodeIsPi( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Type == AIG_PI; } +static inline bool Aig_NodeIsPo( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Type == AIG_PO; } +static inline bool Aig_NodeIsAnd( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Type == AIG_AND; } + +static inline int Aig_NodeId( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Id; } +static inline int Aig_NodeRefs( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->nRefs; } +static inline bool Aig_NodePhase( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->fPhase; } +static inline int Aig_NodeLevel( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Level; } +static inline int Aig_NodeLevelR( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->LevelR; } +static inline int Aig_NodeData( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Data; } +static inline Aig_Man_t * Aig_NodeMan( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->pMan; } +static inline int Aig_NodeFaninId0( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[0].iNode; } +static inline int Aig_NodeFaninId1( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[1].iNode; } +static inline bool Aig_NodeFaninC0( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[0].fComp; } +static inline bool Aig_NodeFaninC1( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[1].fComp; } +static inline Aig_Node_t * Aig_NodeFanin0( Aig_Node_t * pNode ) { return Aig_ManNode( Aig_NodeMan(pNode), Aig_NodeFaninId0(pNode) ); } +static inline Aig_Node_t * Aig_NodeFanin1( Aig_Node_t * pNode ) { return Aig_ManNode( Aig_NodeMan(pNode), Aig_NodeFaninId1(pNode) ); } +static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode ) { return Aig_NotCond( Aig_NodeFanin0(pNode), Aig_NodeFaninC0(pNode) ); } +static inline Aig_Node_t * Aig_NodeChild1( Aig_Node_t * pNode ) { return Aig_NotCond( Aig_NodeFanin1(pNode), Aig_NodeFaninC1(pNode) ); } +static inline Aig_Node_t * Aig_NodeNextH( Aig_Node_t * pNode ) { return pNode->NextH? Aig_ManNode(pNode->pMan, pNode->NextH) : NULL; } +static inline int Aig_NodeWhatFanin( Aig_Node_t * pNode, Aig_Node_t * pFanin ) { if ( Aig_NodeFaninId0(pNode) == pFanin->Id ) return 0; if ( Aig_NodeFaninId1(pNode) == pFanin->Id ) return 1; assert(0); return -1; } +static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); } + +static inline unsigned * Aig_SimInfoForNode( Aig_SimInfo_t * p, Aig_Node_t * pNode ) { assert( p->Type ); return p->pData + p->nWords * pNode->Id; } +static inline unsigned * Aig_SimInfoForPi( Aig_SimInfo_t * p, int Num ) { assert( !p->Type ); return p->pData + p->nWords * Num; } + +static inline void Aig_NodeSetTravId( Aig_Node_t * pNode, int TravId ) { pNode->TravId = TravId; } +static inline void Aig_NodeSetTravIdCurrent( Aig_Node_t * pNode ) { pNode->TravId = pNode->pMan->nTravIds; } +static inline void Aig_NodeSetTravIdPrevious( Aig_Node_t * pNode ) { pNode->TravId = pNode->pMan->nTravIds - 1; } +static inline bool Aig_NodeIsTravIdCurrent( Aig_Node_t * pNode ) { return (bool)((int)pNode->TravId == pNode->pMan->nTravIds); } +static inline bool Aig_NodeIsTravIdPrevious( Aig_Node_t * pNode ) { return (bool)((int)pNode->TravId == pNode->pMan->nTravIds - 1); } + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== aigCheck.c ==========================================================*/ +extern bool Aig_ManCheck( Aig_Man_t * pMan ); +extern bool Aig_NodeIsAcyclic( Aig_Node_t * pNode, Aig_Node_t * pRoot ); +/*=== aigFanout.c ==========================================================*/ +extern void Aig_ManCreateFanouts( Aig_Man_t * p ); +extern void Aig_NodeAddFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanout ); +extern void Aig_NodeRemoveFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanoutToRemove ); +extern int Aig_NodeGetFanoutNum( Aig_Node_t * pNode ); +extern Vec_Ptr_t * Aig_NodeGetFanouts( Aig_Node_t * pNode ); +extern int Aig_NodeGetLevelRNew( Aig_Node_t * pNode ); +extern int Aig_ManSetLevelR( Aig_Man_t * pMan ); +extern int Aig_ManGetLevelMax( Aig_Man_t * pMan ); +extern int Aig_NodeUpdateLevel_int( Aig_Node_t * pNode ); +extern int Aig_NodeUpdateLevelR_int( Aig_Node_t * pNode ); +/*=== aigMem.c =============================================================*/ +extern Aig_MemFixed_t * Aig_MemFixedStart( int nEntrySize ); +extern void Aig_MemFixedStop( Aig_MemFixed_t * p, int fVerbose ); +extern char * Aig_MemFixedEntryFetch( Aig_MemFixed_t * p ); +extern void Aig_MemFixedEntryRecycle( Aig_MemFixed_t * p, char * pEntry ); +extern void Aig_MemFixedRestart( Aig_MemFixed_t * p ); +extern int Aig_MemFixedReadMemUsage( Aig_MemFixed_t * p ); +/*=== aigMan.c =============================================================*/ +extern void Aig_ManSetDefaultParams( Aig_Param_t * pParam ); +extern Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam ); +extern int Aig_ManCleanup( Aig_Man_t * pMan ); +extern void Aig_ManStop( Aig_Man_t * p ); +/*=== aigNode.c =============================================================*/ +extern Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p ); +extern Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p ); +extern Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin ); +extern Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 ); +extern void Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode ); +extern void Aig_NodeDisconnectAnd( Aig_Node_t * pNode ); +extern void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot ); +extern void Aig_NodePrint( Aig_Node_t * pNode ); +extern char * Aig_NodeName( Aig_Node_t * pNode ); +/*=== aigOper.c ==========================================================*/ +extern Aig_Node_t * Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ); +extern Aig_Node_t * Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ); +extern Aig_Node_t * Aig_Xor( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ); +extern Aig_Node_t * Aig_Mux( Aig_Man_t * pMan, Aig_Node_t * pC, Aig_Node_t * p1, Aig_Node_t * p0 ); +extern Aig_Node_t * Aig_Miter( Aig_Man_t * pMan, Vec_Ptr_t * vPairs ); +/*=== aigReplace.c ==========================================================*/ +extern void Aig_ManReplaceNode( Aig_Man_t * pMan, Aig_Node_t * pOld, Aig_Node_t * pNew, int fUpdateLevel ); +/*=== aigTable.c ==========================================================*/ +extern Aig_Table_t * Aig_TableCreate( int nSize ); +extern void Aig_TableFree( Aig_Table_t * p ); +extern int Aig_TableNumNodes( Aig_Table_t * p ); +extern Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ); +extern Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1, Aig_Node_t * pAnd ); +extern void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis ); +extern void Aig_TableResize( Aig_Man_t * pMan ); +extern void Aig_TableRehash( Aig_Man_t * pMan ); +/*=== aigUtil.c ==========================================================*/ +extern void Aig_ManIncrementTravId( Aig_Man_t * pMan ); +extern void Aig_PrintNode( Aig_Node_t * pNode ); + + +/*=== fraigClasses.c ==========================================================*/ +extern Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll ); +/*=== fraigSim.c ==========================================================*/ +extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type ); +extern void Aig_SimInfoClean( Aig_SimInfo_t * p ); +extern void Aig_SimInfoRandom( Aig_SimInfo_t * p ); +extern void Aig_SimInfoResize( Aig_SimInfo_t * p ); +extern void Aig_SimInfoFree( Aig_SimInfo_t * p ); +extern Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + diff --git a/src/sat/aig/aigBalance.c b/src/sat/aig/aigBalance.c new file mode 100644 index 00000000..1dd8ab01 --- /dev/null +++ b/src/sat/aig/aigBalance.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [aigBalance.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigBalance.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/aigCheck.c b/src/sat/aig/aigCheck.c new file mode 100644 index 00000000..a9facef3 --- /dev/null +++ b/src/sat/aig/aigCheck.c @@ -0,0 +1,146 @@ +/**CFile**************************************************************** + + FileName [aigCheck.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Makes sure that every node in the table is in the network and vice versa.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Aig_ManCheck( Aig_Man_t * pMan ) +{ + Aig_Node_t * pObj, * pAnd; + int i; + Aig_ManForEachNode( pMan, pObj, i ) + { + if ( pObj == pMan->pConst1 || Aig_NodeIsPi(pObj) ) + { + if ( pObj->Fans[0].iNode || pObj->Fans[1].iNode || pObj->Level ) + { + printf( "Aig_ManCheck: The AIG has non-standard constant or PI node \"%d\".\n", pObj->Id ); + return 0; + } + continue; + } + if ( Aig_NodeIsPo(pObj) ) + { + if ( pObj->Fans[1].iNode ) + { + printf( "Aig_ManCheck: The AIG has non-standard PO node \"%d\".\n", pObj->Id ); + return 0; + } + continue; + } + // consider the AND node + if ( !pObj->Fans[0].iNode || !pObj->Fans[1].iNode ) + { + printf( "Aig_ManCheck: The AIG has node \"%d\" with a constant fanin.\n", pObj->Id ); + return 0; + } + if ( pObj->Fans[0].iNode > pObj->Fans[1].iNode ) + { + printf( "Aig_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id ); + return 0; + } + if ( pObj->Level != 1 + AIG_MAX(Aig_NodeFanin0(pObj)->Level, Aig_NodeFanin1(pObj)->Level) ) + printf( "Aig_ManCheck: Node \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id ); + pAnd = Aig_TableLookupNode( pMan, Aig_NodeChild0(pObj), Aig_NodeChild1(pObj) ); + if ( pAnd != pObj ) + printf( "Aig_ManCheck: Node \"%d\" is not in the structural hashing table.\n", pObj->Id ); + } + // count the number of nodes in the table + if ( Aig_TableNumNodes(pMan->pTable) != Aig_ManAndNum(pMan) ) + { + printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Check if the node has a combination loop of depth 1 or 2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Aig_NodeIsAcyclic( Aig_Node_t * pNode, Aig_Node_t * pRoot ) +{ + Aig_Node_t * pFanin0, * pFanin1; + Aig_Node_t * pChild00, * pChild01; + Aig_Node_t * pChild10, * pChild11; + if ( !Aig_NodeIsAnd(pNode) ) + return 1; + pFanin0 = Aig_NodeFanin0(pNode); + pFanin1 = Aig_NodeFanin1(pNode); + if ( pRoot == pFanin0 || pRoot == pFanin1 ) + return 0; + if ( Aig_NodeIsPi(pFanin0) ) + { + pChild00 = NULL; + pChild01 = NULL; + } + else + { + pChild00 = Aig_NodeFanin0(pFanin0); + pChild01 = Aig_NodeFanin1(pFanin0); + if ( pRoot == pChild00 || pRoot == pChild01 ) + return 0; + } + if ( Aig_NodeIsPi(pFanin1) ) + { + pChild10 = NULL; + pChild11 = NULL; + } + else + { + pChild10 = Aig_NodeFanin0(pFanin1); + pChild11 = Aig_NodeFanin1(pFanin1); + if ( pRoot == pChild10 || pRoot == pChild11 ) + return 0; + } + return 1; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/aigFanout.c b/src/sat/aig/aigFanout.c new file mode 100644 index 00000000..aed38426 --- /dev/null +++ b/src/sat/aig/aigFanout.c @@ -0,0 +1,423 @@ +/**CFile**************************************************************** + + FileName [aigFanout.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigFanout.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Aig_Node_t * Aig_NodeFanPivot( Aig_Node_t * pNode ) { return Vec_PtrEntry(pNode->pMan->vFanPivots, pNode->Id); } +static inline Aig_Node_t * Aig_NodeFanFan0( Aig_Node_t * pNode ) { return Vec_PtrEntry(pNode->pMan->vFanFans0, pNode->Id); } +static inline Aig_Node_t * Aig_NodeFanFan1( Aig_Node_t * pNode ) { return Vec_PtrEntry(pNode->pMan->vFanFans1, pNode->Id); } +static inline Aig_Node_t ** Aig_NodeFanPivotPlace( Aig_Node_t * pNode ) { return ((Aig_Node_t **)pNode->pMan->vFanPivots->pArray) + pNode->Id; } +static inline Aig_Node_t ** Aig_NodeFanFan0Place( Aig_Node_t * pNode ) { return ((Aig_Node_t **)pNode->pMan->vFanFans0->pArray) + pNode->Id; } +static inline Aig_Node_t ** Aig_NodeFanFan1Place( Aig_Node_t * pNode ) { return ((Aig_Node_t **)pNode->pMan->vFanFans1->pArray) + pNode->Id; } +static inline void Aig_NodeSetFanPivot( Aig_Node_t * pNode, Aig_Node_t * pNode2 ) { Vec_PtrWriteEntry(pNode->pMan->vFanPivots, pNode->Id, pNode2); } +static inline void Aig_NodeSetFanFan0( Aig_Node_t * pNode, Aig_Node_t * pNode2 ) { Vec_PtrWriteEntry(pNode->pMan->vFanFans0, pNode->Id, pNode2); } +static inline void Aig_NodeSetFanFan1( Aig_Node_t * pNode, Aig_Node_t * pNode2 ) { Vec_PtrWriteEntry(pNode->pMan->vFanFans1, pNode->Id, pNode2); } +static inline Aig_Node_t * Aig_NodeNextFanout( Aig_Node_t * pNode, Aig_Node_t * pFanout ) { if ( pFanout == NULL ) return NULL; return Aig_NodeFaninId0(pFanout) == pNode->Id? Aig_NodeFanFan0(pFanout) : Aig_NodeFanFan1(pFanout); } +static inline Aig_Node_t ** Aig_NodeNextFanoutPlace( Aig_Node_t * pNode, Aig_Node_t * pFanout ) { return Aig_NodeFaninId0(pFanout) == pNode->Id? Aig_NodeFanFan0Place(pFanout) : Aig_NodeFanFan1Place(pFanout); } + +// iterator through the fanouts of the node +#define Aig_NodeForEachFanout( pNode, pFanout ) \ + for ( pFanout = Aig_NodeFanPivot(pNode); pFanout; \ + pFanout = Aig_NodeNextFanout(pNode, pFanout) ) +// safe iterator through the fanouts of the node +#define Aig_NodeForEachFanoutSafe( pNode, pFanout, pFanout2 ) \ + for ( pFanout = Aig_NodeFanPivot(pNode), \ + pFanout2 = Aig_NodeNextFanout(pNode, pFanout); \ + pFanout; \ + pFanout = pFanout2, \ + pFanout2 = Aig_NodeNextFanout(pNode, pFanout) ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the fanouts for all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCreateFanouts( Aig_Man_t * p ) +{ + Aig_Node_t * pNode; + int i; + assert( p->vFanPivots == NULL ); + p->vFanPivots = Vec_PtrStart( Aig_ManNodeNum(p) ); + p->vFanFans0 = Vec_PtrStart( Aig_ManNodeNum(p) ); + p->vFanFans1 = Vec_PtrStart( Aig_ManNodeNum(p) ); + Aig_ManForEachNode( p, pNode, i ) + { + if ( Aig_NodeIsPi(pNode) || i == 0 ) + continue; + Aig_NodeAddFaninFanout( Aig_NodeFanin0(pNode), pNode ); + if ( Aig_NodeIsPo(pNode) ) + continue; + Aig_NodeAddFaninFanout( Aig_NodeFanin1(pNode), pNode ); + } +} + +/**Function************************************************************* + + Synopsis [Creates the fanouts for all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Aig_ManResizeFanouts( Aig_Man_t * p, int nSizeNew ) +{ + assert( p->vFanPivots ); + if ( Vec_PtrSize(p->vFanPivots) < nSizeNew ) + { + Vec_PtrFillExtra( p->vFanPivots, nSizeNew + 1000, NULL ); + Vec_PtrFillExtra( p->vFanFans0, nSizeNew + 1000, NULL ); + Vec_PtrFillExtra( p->vFanFans1, nSizeNew + 1000, NULL ); + } +} + +/**Function************************************************************* + + Synopsis [Add the fanout to the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeAddFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanout ) +{ + Aig_Node_t * pPivot; + + // check that they are not complemented + assert( !Aig_IsComplement(pFanin) ); + assert( !Aig_IsComplement(pFanout) ); + // check that pFanins is a fanin of pFanout + assert( Aig_NodeFaninId0(pFanout) == pFanin->Id || Aig_NodeFaninId1(pFanout) == pFanin->Id ); + + // resize the fanout manager + Aig_ManResizeFanouts( pFanin->pMan, 1 + AIG_MAX(pFanin->Id, pFanout->Id) ); + + // consider the case of the first fanout + pPivot = Aig_NodeFanPivot(pFanin); + if ( pPivot == NULL ) + { + Aig_NodeSetFanPivot( pFanin, pFanout ); + return; + } + + // consider the case of more than one fanouts + if ( Aig_NodeFaninId0(pPivot) == pFanin->Id ) + { + if ( Aig_NodeFaninId0(pFanout) == pFanin->Id ) + { + Aig_NodeSetFanFan0( pFanout, Aig_NodeFanFan0(pPivot) ); + Aig_NodeSetFanFan0( pPivot, pFanout ); + } + else // if ( Aig_NodeFaninId1(pFanout) == pFanin->Id ) + { + Aig_NodeSetFanFan1( pFanout, Aig_NodeFanFan0(pPivot) ); + Aig_NodeSetFanFan0( pPivot, pFanout ); + } + } + else // if ( Aig_NodeFaninId1(pPivot) == pFanin->Id ) + { + assert( Aig_NodeFaninId1(pPivot) == pFanin->Id ); + if ( Aig_NodeFaninId0(pFanout) == pFanin->Id ) + { + Aig_NodeSetFanFan0( pFanout, Aig_NodeFanFan1(pPivot) ); + Aig_NodeSetFanFan1( pPivot, pFanout ); + } + else // if ( Aig_NodeFaninId1(pFanout) == pFanin->Id ) + { + Aig_NodeSetFanFan1( pFanout, Aig_NodeFanFan1(pPivot) ); + Aig_NodeSetFanFan1( pPivot, pFanout ); + } + } +} + +/**Function************************************************************* + + Synopsis [Add the fanout to the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeRemoveFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanoutToRemove ) +{ + Aig_Node_t * pFanout, * pFanout2, ** ppFanList; + // start the linked list of fanouts + ppFanList = Aig_NodeFanPivotPlace(pFanin); + // go through the fanouts + Aig_NodeForEachFanoutSafe( pFanin, pFanout, pFanout2 ) + { + // skip the fanout-to-remove + if ( pFanout == pFanoutToRemove ) + continue; + // add useful fanouts to the list + *ppFanList = pFanout; + ppFanList = Aig_NodeNextFanoutPlace( pFanin, pFanout ); + } + *ppFanList = NULL; +} + +/**Function************************************************************* + + Synopsis [Returns the number of fanouts of a node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeGetFanoutNum( Aig_Node_t * pNode ) +{ + Aig_Node_t * pFanout; + int Counter = 0; + Aig_NodeForEachFanout( pNode, pFanout ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Collect fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_NodeGetFanouts( Aig_Node_t * pNode ) +{ + Aig_Node_t * pFanout; + Vec_PtrClear( pNode->pMan->vFanouts ); + Aig_NodeForEachFanout( pNode, pFanout ) + Vec_PtrPush( pNode->pMan->vFanouts, pFanout ); + return pNode->pMan->vFanouts; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node has at least one complemented fanout.] + + Description [A fanout is complemented if the fanout's fanin edge pointing + to the given node is complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Aig_NodeHasComplFanoutEdge( Aig_Node_t * pNode ) +{ + Aig_Node_t * pFanout; + int iFanin; + Aig_NodeForEachFanout( pNode, pFanout ) + { + iFanin = Aig_NodeWhatFanin( pFanout, pNode ); + assert( iFanin >= 0 ); + if ( iFanin && Aig_NodeFaninC1(pFanout) || !iFanin && Aig_NodeFaninC0(pFanout) ) + return 1; + } + return 0; +} + + + + +/**Function************************************************************* + + Synopsis [Recursively computes and assigns the reverse level of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Aig_NodeSetLevelR_rec( Aig_Node_t * pNode ) +{ + Aig_Node_t * pFanout; + int LevelR = 0; + if ( Aig_NodeIsPo(pNode) ) + return pNode->LevelR = 0; + Aig_NodeForEachFanout( pNode, pFanout ) + if ( LevelR < Aig_NodeSetLevelR_rec(pFanout) ) + LevelR = pFanout->LevelR; + return pNode->LevelR = 1 + LevelR; +} + +/**Function************************************************************* + + Synopsis [Computes the reverse level of all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManSetLevelR( Aig_Man_t * pMan ) +{ + Aig_Node_t * pNode; + int i, LevelR = 0; + Aig_ManForEachPi( pMan, pNode, i ) + if ( LevelR < Aig_NodeSetLevelR_rec(pNode) ) + LevelR = pNode->LevelR; + return LevelR; +} + +/**Function************************************************************* + + Synopsis [Computes the global number of logic levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManGetLevelMax( Aig_Man_t * pMan ) +{ + Aig_Node_t * pNode; + int i, LevelsMax = 0; + Aig_ManForEachPo( pMan, pNode, i ) + if ( LevelsMax < (int)pNode->Level ) + LevelsMax = (int)pNode->Level; + return LevelsMax; +} + +/**Function************************************************************* + + Synopsis [Computes but does not assign the reverse level of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeGetLevelRNew( Aig_Node_t * pNode ) +{ + Aig_Node_t * pFanout; + unsigned LevelR = 0; + Aig_NodeForEachFanout( pNode, pFanout ) + LevelR = AIG_MAX( LevelR, pFanout->LevelR ); + return LevelR + !Aig_NodeIsPi(pNode); +} + + +/**Function************************************************************* + + Synopsis [Updates the direct level of one node.] + + Description [Returns 1 if direct level of at least one CO was changed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeUpdateLevel_int( Aig_Node_t * pNode ) +{ + Aig_Node_t * pFanout; + unsigned LevelNew, fStatus = 0; + Aig_NodeForEachFanout( pNode, pFanout ) + { + LevelNew = Aig_NodeGetLevelNew( pFanout ); + if ( pFanout->Level == LevelNew ) + continue; + // the level has changed + pFanout->Level = LevelNew; + if ( Aig_NodeIsPo(pNode) ) + fStatus = 1; + else + fStatus |= Aig_NodeUpdateLevel_int( pFanout ); + } + return fStatus; +} + + +/**Function************************************************************* + + Synopsis [Updates the reverse level of one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeUpdateLevelR_int( Aig_Node_t * pNode ) +{ + Aig_Node_t * pFanin; + unsigned LevelNew; + assert( !Aig_NodeIsPo(pNode) ); + pFanin = Aig_NodeFanin0(pNode); + LevelNew = Aig_NodeGetLevelRNew(pFanin); + if ( pFanin->LevelR != LevelNew ) + { + pFanin->LevelR = LevelNew; + if ( Aig_NodeIsAnd(pFanin) ) + Aig_NodeUpdateLevelR_int( pFanin ); + } + pFanin = Aig_NodeFanin1(pNode); + LevelNew = Aig_NodeGetLevelRNew(pFanin); + if ( pFanin->LevelR != LevelNew ) + { + pFanin->LevelR = LevelNew; + if ( Aig_NodeIsAnd(pFanin) ) + Aig_NodeUpdateLevelR_int( pFanin ); + } + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c new file mode 100644 index 00000000..2058f6b0 --- /dev/null +++ b/src/sat/aig/aigMan.c @@ -0,0 +1,142 @@ +/**CFile**************************************************************** + + FileName [aigMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Sets the default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManSetDefaultParams( Aig_Param_t * pParam ) +{ + memset( pParam, 0, sizeof(Aig_Param_t) ); + pParam->nPatsRand = 1024; // the number of random patterns + pParam->nBTLimit = 99; // backtrack limit at the intermediate nodes + pParam->nSeconds = 1; // the timeout for the final miter in seconds +} + +/**Function************************************************************* + + Synopsis [Starts the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam ) +{ + Aig_Man_t * p; + // set the random seed for simulation + srand( 0xDEADCAFE ); + // start the manager + p = ALLOC( Aig_Man_t, 1 ); + memset( p, 0, sizeof(Aig_Man_t) ); + p->pParam = &p->Param; + p->nTravIds = 1; + // set the defaults + *p->pParam = *pParam; + // start memory managers + p->mmNodes = Aig_MemFixedStart( sizeof(Aig_Node_t) ); + // allocate node arrays + p->vPis = Vec_PtrAlloc( 1000 ); // the array of primary inputs + p->vPos = Vec_PtrAlloc( 1000 ); // the array of primary outputs + p->vNodes = Vec_PtrAlloc( 1000 ); // the array of internal nodes + // start the table + p->pTable = Aig_TableCreate( 1000 ); + // create the constant node + p->pConst1 = Aig_NodeCreateConst( p ); + // initialize other variables + p->vFanouts = Vec_PtrAlloc( 10 ); + p->vToReplace = Vec_PtrAlloc( 10 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManCleanup( Aig_Man_t * pMan ) +{ + Aig_Node_t * pAnd; + int i, nNodesOld; + nNodesOld = Aig_ManAndNum(pMan); + Aig_ManForEachAnd( pMan, pAnd, i ) + if ( pAnd->nRefs == 0 ) + Aig_NodeDeleteAnd_rec( pMan, pAnd ); + return nNodesOld - Aig_ManAndNum(pMan); +} + +/**Function************************************************************* + + Synopsis [Stops the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManStop( Aig_Man_t * p ) +{ + if ( p->vFanPivots ) Vec_PtrFree( p->vFanPivots ); + if ( p->vFanFans0 ) Vec_PtrFree( p->vFanFans0 ); + if ( p->vFanFans1 ) Vec_PtrFree( p->vFanFans1 ); + if ( p->vClasses ) Vec_VecFree( p->vClasses ); + Aig_MemFixedStop( p->mmNodes, 0 ); + Vec_PtrFree( p->vNodes ); + Vec_PtrFree( p->vPis ); + Vec_PtrFree( p->vPos ); + Vec_PtrFree( p->vFanouts ); + Vec_PtrFree( p->vToReplace ); + Aig_TableFree( p->pTable ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/aigMem.c b/src/sat/aig/aigMem.c new file mode 100644 index 00000000..280cf98b --- /dev/null +++ b/src/sat/aig/aigMem.c @@ -0,0 +1,246 @@ +/**CFile**************************************************************** + + FileName [aigMem.c] + + PackageName [ABC: Logic synthesis and verification system.] + + Synopsis [Fixed-size-entry memory manager for the AIG package.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: aigMem.c,v 1.4 2005/07/08 01:01:31 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct Aig_MemFixed_t_ +{ + // information about individual entries + int nEntrySize; // the size of one entry + int nEntriesAlloc; // the total number of entries allocated + int nEntriesUsed; // the number of entries in use + int nEntriesMax; // the max number of entries in use + char * pEntriesFree; // the linked list of free entries + + // this is where the memory is stored + int nChunkSize; // the size of one chunk + int nChunksAlloc; // the maximum number of memory chunks + int nChunks; // the current number of memory chunks + char ** pChunks; // the allocated memory + + // statistics + int nMemoryUsed; // memory used in the allocated entries + int nMemoryAlloc; // memory allocated +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the internal memory manager.] + + Description [Can only work with entry size at least 4 byte long.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_MemFixed_t * Aig_MemFixedStart( int nEntrySize ) +{ + Aig_MemFixed_t * p; + + p = ALLOC( Aig_MemFixed_t, 1 ); + memset( p, 0, sizeof(Aig_MemFixed_t) ); + + p->nEntrySize = nEntrySize; + p->nEntriesAlloc = 0; + p->nEntriesUsed = 0; + p->pEntriesFree = NULL; + + if ( nEntrySize * (1 << 10) < (1<<16) ) + p->nChunkSize = (1 << 10); + else + p->nChunkSize = (1<<16) / nEntrySize; + if ( p->nChunkSize < 8 ) + p->nChunkSize = 8; + + p->nChunksAlloc = 64; + p->nChunks = 0; + p->pChunks = ALLOC( char *, p->nChunksAlloc ); + + p->nMemoryUsed = 0; + p->nMemoryAlloc = 0; + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the internal memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_MemFixedStop( Aig_MemFixed_t * p, int fVerbose ) +{ + int i; + if ( p == NULL ) + return; + if ( fVerbose ) + { + printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n", + p->nEntrySize, p->nChunkSize, p->nChunks ); + printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n", + p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); + } + for ( i = 0; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + free( p->pChunks ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Extracts one entry from the memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Aig_MemFixedEntryFetch( Aig_MemFixed_t * p ) +{ + char * pTemp; + int i; + + // check if there are still free entries + if ( p->nEntriesUsed == p->nEntriesAlloc ) + { // need to allocate more entries + assert( p->pEntriesFree == NULL ); + if ( p->nChunks == p->nChunksAlloc ) + { + p->nChunksAlloc *= 2; + p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + } + p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize ); + p->nMemoryAlloc += p->nEntrySize * p->nChunkSize; + // transform these entries into a linked list + pTemp = p->pEntriesFree; + for ( i = 1; i < p->nChunkSize; i++ ) + { + *((char **)pTemp) = pTemp + p->nEntrySize; + pTemp += p->nEntrySize; + } + // set the last link + *((char **)pTemp) = NULL; + // add the chunk to the chunk storage + p->pChunks[ p->nChunks++ ] = p->pEntriesFree; + // add to the number of entries allocated + p->nEntriesAlloc += p->nChunkSize; + } + // incrememt the counter of used entries + p->nEntriesUsed++; + if ( p->nEntriesMax < p->nEntriesUsed ) + p->nEntriesMax = p->nEntriesUsed; + // return the first entry in the free entry list + pTemp = p->pEntriesFree; + p->pEntriesFree = *((char **)pTemp); + return pTemp; +} + +/**Function************************************************************* + + Synopsis [Returns one entry into the memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_MemFixedEntryRecycle( Aig_MemFixed_t * p, char * pEntry ) +{ + // decrement the counter of used entries + p->nEntriesUsed--; + // add the entry to the linked list of free entries + *((char **)pEntry) = p->pEntriesFree; + p->pEntriesFree = pEntry; +} + +/**Function************************************************************* + + Synopsis [Frees all associated memory and resets the manager.] + + Description [Relocates all the memory except the first chunk.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_MemFixedRestart( Aig_MemFixed_t * p ) +{ + int i; + char * pTemp; + + // delocate all chunks except the first one + for ( i = 1; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + p->nChunks = 1; + // transform these entries into a linked list + pTemp = p->pChunks[0]; + for ( i = 1; i < p->nChunkSize; i++ ) + { + *((char **)pTemp) = pTemp + p->nEntrySize; + pTemp += p->nEntrySize; + } + // set the last link + *((char **)pTemp) = NULL; + // set the free entry list + p->pEntriesFree = p->pChunks[0]; + // set the correct statistics + p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; + p->nMemoryUsed = 0; + p->nEntriesAlloc = p->nChunkSize; + p->nEntriesUsed = 0; +} + +/**Function************************************************************* + + Synopsis [Reports the memory usage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_MemFixedReadMemUsage( Aig_MemFixed_t * p ) +{ + return p->nMemoryAlloc; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c new file mode 100644 index 00000000..afccd985 --- /dev/null +++ b/src/sat/aig/aigNode.c @@ -0,0 +1,292 @@ +/**CFile**************************************************************** + + FileName [aigNode.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Aig_Node_t * Aig_NodeCreate( Aig_Man_t * p ) +{ + Aig_Node_t * pNode; + // create the node + pNode = (Aig_Node_t *)Aig_MemFixedEntryFetch( p->mmNodes ); + memset( pNode, 0, sizeof(Aig_Node_t) ); + // assign the number and add to the array of nodes + pNode->Id = p->vNodes->nSize; + Vec_PtrPush( p->vNodes, pNode ); + return pNode; +} + +/**Function************************************************************* + + Synopsis [Creates the constant 1 node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p ) +{ + Aig_Node_t * pNode; + pNode = Aig_NodeCreate( p ); + pNode->fPhase = 1; // sim value for 000... pattern + return pNode; +} + +/**Function************************************************************* + + Synopsis [Creates a primary input node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p ) +{ + Aig_Node_t * pNode; + pNode = Aig_NodeCreate( p ); + Vec_PtrPush( p->vPis, pNode ); + pNode->fPhase = 0; // sim value for 000... pattern + return pNode; +} + +/**Function************************************************************* + + Synopsis [Creates a primary output node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin ) +{ + Aig_Node_t * pNode; + pNode = Aig_NodeCreate( p ); + Vec_PtrPush( p->vPos, pNode ); + // connect to the fanin + pNode->Fans[0].fComp = Aig_IsComplement(pFanin); + pNode->Fans[0].iNode = Aig_Regular(pFanin)->Id; + pNode->fPhase = pNode->Fans[0].fComp ^ Aig_Regular(pFanin)->fPhase; // sim value for 000... pattern + pNode->Level = Aig_Regular(pFanin)->Level; + Aig_Regular(pFanin)->nRefs++; + if ( pNode->pMan->vFanPivots ) Aig_NodeAddFaninFanout( pFanin, pNode ); + // update global level if needed + if ( p->nLevelMax < (int)pNode->Level ) + p->nLevelMax = pNode->Level; + return pNode; +} + +/**Function************************************************************* + + Synopsis [Creates a new node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 ) +{ + Aig_Node_t * pNode; + pNode = Aig_NodeCreate( p ); + Aig_NodeConnectAnd( pFanin0, pFanin1, pNode ); + return pNode; +} + +/**Function************************************************************* + + Synopsis [Connects the nodes to the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode ) +{ + assert( !Aig_IsComplement(pNode) ); + assert( Aig_NodeIsAnd(pNode) ); + // add the fanins + pNode->Fans[0].fComp = Aig_IsComplement(pFanin0); + pNode->Fans[0].iNode = Aig_Regular(pFanin0)->Id; + pNode->Fans[1].fComp = Aig_IsComplement(pFanin1); + pNode->Fans[1].iNode = Aig_Regular(pFanin1)->Id; + // compute the phase (sim value for 000... pattern) + pNode->fPhase = (pNode->Fans[0].fComp ^ Aig_Regular(pFanin0)->fPhase) & + (pNode->Fans[1].fComp ^ Aig_Regular(pFanin1)->fPhase); + pNode->Level = Aig_NodeGetLevelNew(pNode); + // reference the fanins + Aig_Regular(pFanin0)->nRefs++; + Aig_Regular(pFanin1)->nRefs++; + // add the fanouts + if ( pNode->pMan->vFanPivots ) Aig_NodeAddFaninFanout( pFanin0, pNode ); + if ( pNode->pMan->vFanPivots ) Aig_NodeAddFaninFanout( pFanin1, pNode ); + // add the node to the structural hash table + Aig_TableInsertNode( pNode->pMan, pFanin0, pFanin1, pNode ); +} + +/**Function************************************************************* + + Synopsis [Connects the nodes to the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeDisconnectAnd( Aig_Node_t * pNode ) +{ + Aig_Node_t * pFanin0, * pFanin1; + assert( !Aig_IsComplement(pNode) ); + assert( Aig_NodeIsAnd(pNode) ); + // get the fanins + pFanin0 = Aig_NodeFanin0(pNode); + pFanin1 = Aig_NodeFanin1(pNode); + // dereference the fanins + pFanin0->nRefs--; + pFanin0->nRefs--; + // remove the fanouts + if ( pNode->pMan->vFanPivots ) Aig_NodeRemoveFaninFanout( pFanin0, pNode ); + if ( pNode->pMan->vFanPivots ) Aig_NodeRemoveFaninFanout( pFanin1, pNode ); + // remove the node from the structural hash table + Aig_TableDeleteNode( pNode->pMan, pNode ); +} + +/**Function************************************************************* + + Synopsis [Performs internal deletion step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot ) +{ + Aig_Node_t * pNode0, * pNode1; + // make sure the node is regular and dangling + assert( !Aig_IsComplement(pRoot) ); + assert( pRoot->nRefs == 0 ); + assert( Aig_NodeIsAnd(pRoot) ); + // save the children + pNode0 = Aig_NodeFanin0(pRoot); + pNode1 = Aig_NodeFanin1(pRoot); + // disconnect the node + Aig_NodeDisconnectAnd( pRoot ); + // recycle the node + Vec_PtrWriteEntry( pMan->vNodes, pRoot->Id, NULL ); + Aig_MemFixedEntryRecycle( pMan->mmNodes, (char *)pRoot ); + // call recursively + if ( Aig_NodeIsAnd(pNode0) && pNode0->nRefs == 0 ) + Aig_NodeDeleteAnd_rec( pMan, pNode0 ); + if ( Aig_NodeIsAnd(pNode1) && pNode1->nRefs == 0 ) + Aig_NodeDeleteAnd_rec( pMan, pNode1 ); +} + +/**Function************************************************************* + + Synopsis [Prints the AIG node for debugging purposes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodePrint( Aig_Node_t * pNode ) +{ + Aig_Node_t * pNodeR = Aig_Regular(pNode); + if ( Aig_NodeIsPi(pNode) ) + { + printf( "PI %4s%s.\n", Aig_NodeName(pNode), Aig_IsComplement(pNode)? "\'" : "" ); + return; + } + if ( Aig_NodeIsConst(pNode) ) + { + printf( "Constant 1 %s.\n", Aig_IsComplement(pNode)? "(complemented)" : "" ); + return; + } + // print the node's function + printf( "%7s%s", Aig_NodeName(pNodeR), Aig_IsComplement(pNode)? "\'" : "" ); + printf( " = " ); + printf( "%7s%s", Aig_NodeName(Aig_NodeFanin0(pNodeR)), Aig_NodeFaninC0(pNodeR)? "\'" : "" ); + printf( " * " ); + printf( "%7s%s", Aig_NodeName(Aig_NodeFanin1(pNodeR)), Aig_NodeFaninC1(pNodeR)? "\'" : "" ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Returns the name of the node.] + + Description [The name should be used before this procedure is called again.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Aig_NodeName( Aig_Node_t * pNode ) +{ + static char Buffer[100]; + sprintf( Buffer, "%d", Aig_Regular(pNode)->Id ); + return Buffer; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/aigOper.c b/src/sat/aig/aigOper.c new file mode 100644 index 00000000..a10cc7ff --- /dev/null +++ b/src/sat/aig/aigOper.c @@ -0,0 +1,175 @@ +/**CFile**************************************************************** + + FileName [aigOper.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigOper.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ) +{ + Aig_Node_t * pAnd; + // check for trivial cases + if ( p0 == p1 ) + return p0; + if ( p0 == Aig_Not(p1) ) + return Aig_Not(pMan->pConst1); + if ( Aig_Regular(p0) == pMan->pConst1 ) + { + if ( p0 == pMan->pConst1 ) + return p1; + return Aig_Not(pMan->pConst1); + } + if ( Aig_Regular(p1) == pMan->pConst1 ) + { + if ( p1 == pMan->pConst1 ) + return p0; + return Aig_Not(pMan->pConst1); + } + // order the arguments + if ( Aig_Regular(p0)->Id > Aig_Regular(p1)->Id ) + { + if ( pAnd = Aig_TableLookupNode( pMan, p1, p0 ) ) + return pAnd; + return Aig_NodeCreateAnd( pMan, p1, p0 ); + } + else + { + if ( pAnd = Aig_TableLookupNode( pMan, p0, p1 ) ) + return pAnd; + return Aig_NodeCreateAnd( pMan, p0, p1 ); + } +} + +/**Function************************************************************* + + Synopsis [Implements Boolean OR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ) +{ + return Aig_Not( Aig_And( pMan, Aig_Not(p0), Aig_Not(p1) ) ); +} + +/**Function************************************************************* + + Synopsis [Implements Boolean XOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_Xor( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ) +{ + return Aig_Or( pMan, Aig_And(pMan, p0, Aig_Not(p1)), + Aig_And(pMan, p1, Aig_Not(p0)) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_Mux( Aig_Man_t * pMan, Aig_Node_t * pC, Aig_Node_t * p1, Aig_Node_t * p0 ) +{ + return Aig_Or( pMan, Aig_And(pMan, pC, p1), Aig_And(pMan, Aig_Not(pC), p0) ); +} + +/**Function************************************************************* + + Synopsis [Implements the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_Miter_rec( Aig_Man_t * pMan, Aig_Node_t ** ppObjs, int nObjs ) +{ + Aig_Node_t * pObj1, * pObj2; + if ( nObjs == 1 ) + return ppObjs[0]; + pObj1 = Aig_Miter_rec( pMan, ppObjs, nObjs/2 ); + pObj2 = Aig_Miter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 ); + return Aig_Or( pMan, pObj1, pObj2 ); +} + +/**Function************************************************************* + + Synopsis [Implements the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_Miter( Aig_Man_t * pMan, Vec_Ptr_t * vPairs ) +{ + int i; + if ( vPairs->nSize == 0 ) + return Aig_Not( pMan->pConst1 ); + assert( vPairs->nSize % 2 == 0 ); + // go through the cubes of the node's SOP + for ( i = 0; i < vPairs->nSize; i += 2 ) + vPairs->pArray[i/2] = Aig_Xor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] ); + vPairs->nSize = vPairs->nSize/2; + return Aig_Miter_rec( pMan, (Aig_Node_t **)vPairs->pArray, vPairs->nSize ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/aigReplace.c b/src/sat/aig/aigReplace.c new file mode 100644 index 00000000..d928fdf8 --- /dev/null +++ b/src/sat/aig/aigReplace.c @@ -0,0 +1,133 @@ +/**CFile**************************************************************** + + FileName [aigUpdate.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigUpdate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs internal replacement step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Abc_AigReplace_int( Aig_Man_t * pMan, int fUpdateLevel ) +{ + Vec_Ptr_t * vFanouts; + Aig_Node_t * pOld, * pNew, * pFanin0, * pFanin1, * pFanout, * pTemp, * pFanoutNew; + int k, iFanin; + // get the pair of nodes to replace + assert( Vec_PtrSize(pMan->vToReplace) > 0 ); + pNew = Vec_PtrPop( pMan->vToReplace ); + pOld = Vec_PtrPop( pMan->vToReplace ); + // make sure the old node is internal, regular, and has fanouts + // (the new node can be PI or internal, is complemented, and can have fanouts) + assert( !Aig_IsComplement(pOld) ); + assert( pOld->nRefs > 0 ); + assert( Aig_NodeIsAnd(pOld) ); + assert( Aig_NodeIsPo(pNew) ); + // look at the fanouts of old node + vFanouts = Aig_NodeGetFanouts( pOld ); + Vec_PtrForEachEntry( vFanouts, pFanout, k ) + { + if ( Aig_NodeIsPo(pFanout) ) + { + // patch the first fanin of the PO + pFanout->Fans[0].iNode = Aig_Regular(pNew)->Id; + pFanout->Fans[0].fComp ^= Aig_IsComplement(pNew); + continue; + } + // find the old node as a fanin of this fanout + iFanin = Aig_NodeWhatFanin( pFanout, pOld ); + assert( iFanin == 0 || iFanin == 1 ); + // get the new fanin + pFanin0 = Aig_NotCond( pNew, pFanout->Fans[iFanin].fComp ); + assert( Aig_Regular(pFanin0) != pFanout ); + // get another fanin + pFanin1 = iFanin? Aig_NodeChild0(pFanout) : Aig_NodeChild1(pFanout); + assert( Aig_Regular(pFanin1) != pFanout ); + assert( Aig_Regular(pFanin0) != Aig_Regular(pFanin1) ); + // order them + if ( Aig_Regular(pFanin0)->Id > Aig_Regular(pFanin1)->Id ) + pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp; + // check if the node with these fanins exists + if ( pFanoutNew = Aig_TableLookupNode( pMan, pFanin0, pFanin1 ) ) + { // such node exists (it may be a constant) + // schedule replacement of the old fanout by the new fanout + Vec_PtrPush( pMan->vToReplace, pFanout ); + Vec_PtrPush( pMan->vToReplace, pFanoutNew ); + continue; + } + // such node does not exist - modify the old fanout node + // (this way the change will not propagate all the way to the COs) + Aig_NodeDisconnectAnd( pFanout ); + Aig_NodeConnectAnd( pFanin0, pFanin1, pFanout ); + // recreate the old fanout with new fanins and add it to the table + assert( Aig_NodeIsAcyclic(pFanout, pFanout) ); + // update the level if requested + if ( fUpdateLevel ) + { + if ( Aig_NodeUpdateLevel_int(pFanout) ) + pMan->nLevelMax = Aig_ManGetLevelMax( pMan ); + //Aig_NodeGetLevelRNew( pFanout ); + Aig_NodeUpdateLevelR_int( pFanout ); + } + } + // if the node has no fanouts left, remove its MFFC + if ( pOld->nRefs == 0 ) + Aig_NodeDeleteAnd_rec( pMan, pOld ); +} + +/**Function************************************************************* + + Synopsis [Replaces one AIG node by the other.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManReplaceNode( Aig_Man_t * pMan, Aig_Node_t * pOld, Aig_Node_t * pNew, int fUpdateLevel ) +{ + assert( Vec_PtrSize(pMan->vToReplace) == 0 ); + Vec_PtrPush( pMan->vToReplace, pOld ); + Vec_PtrPush( pMan->vToReplace, pNew ); + while ( Vec_PtrSize(pMan->vToReplace) ) + Abc_AigReplace_int( pMan, fUpdateLevel ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/aigTable.c b/src/sat/aig/aigTable.c new file mode 100644 index 00000000..cfc94f6b --- /dev/null +++ b/src/sat/aig/aigTable.c @@ -0,0 +1,335 @@ +/**CFile**************************************************************** + + FileName [aigTable.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// the hash table +struct Aig_Table_t_ +{ + Aig_Node_t ** pBins; // the table bins + int nBins; // the size of the table + int nEntries; // the total number of entries in the table +}; + +// iterators through the entries in the linked lists of nodes +#define Aig_TableBinForEachEntry( pBin, pEnt ) \ + for ( pEnt = pBin; \ + pEnt; \ + pEnt = pEnt->NextH? Aig_ManNode(pEnt->pMan, pEnt->NextH) : NULL ) +#define Aig_TableBinForEachEntrySafe( pBin, pEnt, pEnt2 ) \ + for ( pEnt = pBin, \ + pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL; \ + pEnt; \ + pEnt = pEnt2, \ + pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL ) + +// hash key for the structural hash table +static inline unsigned Abc_HashKey2( Aig_Node_t * p0, Aig_Node_t * p1, int TableSize ) { return ((unsigned)(p0) + (unsigned)(p1) * 12582917) % TableSize; } +//static inline unsigned Abc_HashKey2( Aig_Node_t * p0, Aig_Node_t * p1, int TableSize ) { return ((unsigned)((a)->Id + (b)->Id) * ((a)->Id + (b)->Id + 1) / 2) % TableSize; } + +static unsigned int Cudd_PrimeAig( unsigned int p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Table_t * Aig_TableCreate( int nSize ) +{ + Aig_Table_t * p; + // allocate the table + p = ALLOC( Aig_Table_t, 1 ); + memset( p, 0, sizeof(Aig_Table_t) ); + // allocate and clean the bins + p->nBins = Cudd_PrimeAig(nSize); + p->pBins = ALLOC( Aig_Node_t *, p->nBins ); + memset( p->pBins, 0, sizeof(Aig_Node_t *) * p->nBins ); + return p; +} + +/**Function************************************************************* + + Synopsis [Deallocates the supergate hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TableFree( Aig_Table_t * p ) +{ + FREE( p->pBins ); + FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of nodes in the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_TableNumNodes( Aig_Table_t * p ) +{ + return p->nEntries; +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ) +{ + Aig_Node_t * pAnd; + unsigned Key; + assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id ); + assert( p0->pMan == p1->pMan ); + // get the hash key for these two nodes + Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins ); + // find the matching node in the table + Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd ) + if ( p0 == Aig_NodeChild0(pAnd) && p1 == Aig_NodeChild1(pAnd) ) + return pAnd; + return NULL; +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1, Aig_Node_t * pAnd ) +{ + unsigned Key; + assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id ); + // check if it is a good time for table resizing + if ( pMan->pTable->nEntries > 2 * pMan->pTable->nBins ) + Aig_TableResize( pMan ); + // add the node to the corresponding linked list in the table + Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins ); + pAnd->NextH = pMan->pTable->pBins[Key]->Id; + pMan->pTable->pBins[Key]->NextH = pAnd->Id; + pMan->pTable->nEntries++; + return pAnd; +} + + +/**Function************************************************************* + + Synopsis [Deletes an AIG node from the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis ) +{ + Aig_Node_t * pAnd, * pPlace = NULL; + unsigned Key; + assert( !Aig_IsComplement(pThis) ); + assert( Aig_NodeIsAnd(pThis) ); + assert( pMan == pThis->pMan ); + // get the hash key for these two nodes + Key = Abc_HashKey2( Aig_NodeChild0(pThis), Aig_NodeChild1(pThis), pMan->pTable->nBins ); + // find the matching node in the table + Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd ) + { + if ( pThis != pAnd ) + { + pPlace = pAnd; + continue; + } + if ( pPlace == NULL ) + pMan->pTable->pBins[Key] = Aig_NodeNextH(pThis); + else + pPlace->NextH = pThis->Id; + break; + } + assert( pThis == pAnd ); + pMan->pTable->nEntries--; +} + +/**Function************************************************************* + + Synopsis [Resizes the hash table of AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TableResize( Aig_Man_t * pMan ) +{ + Aig_Node_t ** pBinsNew; + Aig_Node_t * pEnt, * pEnt2; + int nBinsNew, Counter, i, clk; + unsigned Key; + +clk = clock(); + // get the new table size + nBinsNew = Cudd_PrimeCopy( 3 * pMan->pTable->nBins ); + // allocate a new array + pBinsNew = ALLOC( Aig_Node_t *, nBinsNew ); + memset( pBinsNew, 0, sizeof(Aig_Node_t *) * nBinsNew ); + // rehash the entries from the old table + Counter = 0; + for ( i = 0; i < pMan->pTable->nBins; i++ ) + Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 ) + { + Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), nBinsNew ); + pEnt->NextH = pBinsNew[Key]->Id; + pBinsNew[Key]->NextH = pEnt->Id; + Counter++; + } + assert( Counter == pMan->pTable->nEntries ); +// printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew ); +// PRT( "Time", clock() - clk ); + // replace the table and the parameters + free( pMan->pTable->pBins ); + pMan->pTable->pBins = pBinsNew; + pMan->pTable->nBins = nBinsNew; +} + +/**Function************************************************************* + + Synopsis [Resizes the hash table of AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TableRehash( Aig_Man_t * pMan ) +{ + Aig_Node_t ** pBinsNew; + Aig_Node_t * pEnt, * pEnt2; + unsigned Key; + int Counter, Temp, i; + // allocate a new array + pBinsNew = ALLOC( Aig_Node_t *, pMan->pTable->nBins ); + memset( pBinsNew, 0, sizeof(Aig_Node_t *) * pMan->pTable->nBins ); + // rehash the entries from the old table + Counter = 0; + for ( i = 0; i < pMan->pTable->nBins; i++ ) + Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 ) + { + // swap the fanins if needed + if ( pEnt->Fans[0].iNode > pEnt->Fans[1].iNode ) + { + Temp = pEnt->Fans[0].iNode; + pEnt->Fans[0].iNode = pEnt->Fans[1].iNode; + pEnt->Fans[1].iNode = Temp; + Temp = pEnt->Fans[0].fComp; + pEnt->Fans[0].fComp = pEnt->Fans[1].fComp; + pEnt->Fans[1].fComp = Temp; + } + // rehash the node + Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), pMan->pTable->nBins ); + pEnt->NextH = pBinsNew[Key]->Id; + pBinsNew[Key]->NextH = pEnt->Id; + Counter++; + } + assert( Counter == pMan->pTable->nEntries ); + // replace the table and the parameters + free( pMan->pTable->pBins ); + pMan->pTable->pBins = pBinsNew; +} + +/**Function************************************************************* + + Synopsis [Returns the smallest prime larger than the number.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned int Cudd_PrimeAig( unsigned int p ) +{ + int i,pn; + + p--; + do { + p++; + if (p&1) { + pn = 1; + i = 3; + while ((unsigned) (i * i) <= p) { + if (p % i == 0) { + pn = 0; + break; + } + i += 2; + } + } else { + pn = 0; + } + } while (!pn); + return(p); + +} /* end of Cudd_Prime */ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/aigUtil.c b/src/sat/aig/aigUtil.c new file mode 100644 index 00000000..a1c9ca44 --- /dev/null +++ b/src/sat/aig/aigUtil.c @@ -0,0 +1,60 @@ +/**CFile**************************************************************** + + FileName [aigUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Increments the current traversal ID of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManIncrementTravId( Aig_Man_t * pMan ) +{ + Aig_Node_t * pObj; + int i; + if ( pMan->nTravIds == (1<<24)-1 ) + { + pMan->nTravIds = 0; + Aig_ManForEachNode( pMan, pObj, i ) + pObj->TravId = 0; + } + pMan->nTravIds++; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c new file mode 100644 index 00000000..b3040e2a --- /dev/null +++ b/src/sat/aig/fraigClass.c @@ -0,0 +1,108 @@ +/**CFile**************************************************************** + + FileName [aigFraig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" +#include "stmm.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static unsigned Aig_ManHashKey( unsigned * pData, int nWords ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the equivalence classes of patterns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) +{ + Vec_Vec_t * vClasses; // equivalence classes + stmm_table * tSim2Node; // temporary hash table hashing key into the class number + Aig_Node_t * pNode; + unsigned uKey; + int i, * pSpot, ClassNum; + assert( pInfo->Type == 1 ); + // fill in the hash table + tSim2Node = stmm_init_table( stmm_numcmp, stmm_numhash ); + vClasses = Vec_VecAlloc( 100 ); + Aig_ManForEachNode( p, pNode, i ) + { + if ( Aig_NodeIsPo(pNode) ) + continue; + uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords ); + if ( !stmm_find_or_add( tSim2Node, (char *)uKey, (char ***)&pSpot ) ) // does not exist + *pSpot = (pNode->Id << 1) | 1; // save the node, and do nothing + else if ( (*pSpot) & 1 ) // this is a node + { + // create the class + ClassNum = Vec_VecSize( vClasses ); + Vec_VecPush( vClasses, ClassNum, (void *)((*pSpot) >> 1) ); + Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id ); + // save the class + *pSpot = (ClassNum << 1); + } + else // this is a class + { + ClassNum = (*pSpot) >> 1; + Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id ); + } + } + stmm_free_table( tSim2Node ); + return vClasses; +} + +/**Function************************************************************* + + Synopsis [Computes the hash key of the simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Aig_ManHashKey( unsigned * pData, int nWords ) +{ + static int Primes[10] = { 1009, 2207, 3779, 4001, 4877, 5381, 6427, 6829, 7213, 7919 }; + unsigned uKey; + int i; + uKey = 0; + for ( i = 0; i < nWords; i++ ) + uKey ^= pData[i] * Primes[i%10]; + return uKey; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c new file mode 100644 index 00000000..6187538b --- /dev/null +++ b/src/sat/aig/fraigCore.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [aigFraig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/fraigProve.c b/src/sat/aig/fraigProve.c new file mode 100644 index 00000000..b5cce582 --- /dev/null +++ b/src/sat/aig/fraigProve.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [aigProve.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/fraigSim.c b/src/sat/aig/fraigSim.c new file mode 100644 index 00000000..1d547621 --- /dev/null +++ b/src/sat/aig/fraigSim.c @@ -0,0 +1,238 @@ +/**CFile**************************************************************** + + FileName [aigSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Simulates all nodes using random simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManSimulateRandomFirst( Aig_Man_t * p ) +{ + Aig_SimInfo_t * pInfoPi, * pInfoAll; + assert( p->pInfo && p->pInfoTemp ); + // create random PI info + pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 ); + Aig_SimInfoRandom( pInfoPi ); + // simulate it though the circuit + pInfoAll = Aig_ManSimulateInfo( p, pInfoPi ); + // detect classes + p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll ); + Aig_SimInfoFree( pInfoAll ); + // save simulation info + p->pInfo = pInfoPi; + p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 ); +} + +/**Function************************************************************* + + Synopsis [Simulates all nodes using the given simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi ) +{ + Aig_SimInfo_t * pInfoAll; + Aig_Node_t * pNode; + unsigned * pDataPi, * pData0, * pData1, * pDataAnd; + int i, k, fComp0, fComp1; + + assert( !pInfoPi->Type ); // PI siminfo + // allocate sim info for all nodes + pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 ); + // set the constant sim info + pData1 = Aig_SimInfoForNode( pInfoAll, p->pConst1 ); + for ( k = 0; k < pInfoPi->nWords; k++ ) + pData1[k] = ~((unsigned)0); + // copy the PI siminfo + Vec_PtrForEachEntry( p->vPis, pNode, i ) + { + pDataPi = Aig_SimInfoForPi( pInfoPi, i ); + pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode ); + for ( k = 0; k < pInfoPi->nWords; k++ ) + pDataAnd[k] = pDataPi[k]; + } + // simulate the nodes + Vec_PtrForEachEntry( p->vNodes, pNode, i ) + { + if ( !Aig_NodeIsAnd(pNode) ) + continue; + pData0 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) ); + pData1 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin1(pNode) ); + pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode ); + fComp0 = Aig_NodeFaninC0(pNode); + fComp1 = Aig_NodeFaninC1(pNode); + if ( fComp0 && fComp1 ) + for ( k = 0; k < pInfoPi->nWords; k++ ) + pDataAnd[k] = ~pData0[k] & ~pData1[k]; + else if ( fComp0 ) + for ( k = 0; k < pInfoPi->nWords; k++ ) + pDataAnd[k] = ~pData0[k] & pData1[k]; + else if ( fComp1 ) + for ( k = 0; k < pInfoPi->nWords; k++ ) + pDataAnd[k] = pData0[k] & ~pData1[k]; + else + for ( k = 0; k < pInfoPi->nWords; k++ ) + pDataAnd[k] = pData0[k] & pData1[k]; + } + return pInfoAll; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type ) +{ + Aig_SimInfo_t * p; + p = ALLOC( Aig_SimInfo_t, 1 ); + memset( p, 0, sizeof(Aig_SimInfo_t) ); + p->Type = Type; + p->nNodes = nNodes; + p->nWords = nWords; + p->nPatsMax = nWords * sizeof(unsigned) * 8; + p->pData = ALLOC( unsigned, nNodes * nWords ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_SimInfoClean( Aig_SimInfo_t * p ) +{ + int i, Size = p->nNodes * p->nWords; + p->nPatsCur = 0; + for ( i = 0; i < Size; i++ ) + p->pData[i] = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_SimInfoRandom( Aig_SimInfo_t * p ) +{ + int i, Size = p->nNodes * p->nWords; + unsigned * pData; + for ( i = 0; i < Size; i++ ) + p->pData[i] = ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())); + // make sure the first bit of all nodes is 0 + for ( i = 0; i < p->nNodes; i++ ) + { + pData = p->pData + p->nWords * i; + *pData <<= 1; + } + p->nPatsCur = p->nPatsMax; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_SimInfoResize( Aig_SimInfo_t * p ) +{ + unsigned * pData; + int i, k; + assert( p->nPatsCur == p->nPatsMax ); + pData = ALLOC( unsigned, 2 * p->nNodes * p->nWords ); + for ( i = 0; i < p->nNodes; i++ ) + { + for ( k = 0; k < p->nWords; k++ ) + pData[2 * p->nWords * i + k] = p->pData[p->nWords * i + k]; + for ( k = 0; k < p->nWords; k++ ) + pData[2 * p->nWords * i + k + p->nWords] = 0; + } + p->nPatsMax *= 2; + p->nWords *= 2; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_SimInfoFree( Aig_SimInfo_t * p ) +{ + free( p->pData ); + free( p ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index 74503a2b..eb1c5374 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -291,6 +291,8 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) // check that there is no dangling nodes Abc_NtkForEachNode( pNtk, pObj, i ) { + if ( i == 0 ) + continue; if ( Abc_ObjFanoutNum(pObj) == 0 ) { printf( "CSAT_Check_Integrity: The network has dangling nodes.\n" ); diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index 13f6b50b..a9e09f61 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -233,7 +233,7 @@ clk = clock(); RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; -Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" ); +//Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" ); if ( RetValue1 == MSAT_FALSE ) { |