diff options
31 files changed, 2108 insertions, 280 deletions
@@ -42,7 +42,7 @@ RSC=rc.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD CPP /nologo /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 "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c +# ADD CPP /nologo /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\aig" /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\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -66,7 +66,7 @@ LINK32=link.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c -# ADD CPP /nologo /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 /YX /FD /GZ /c +# ADD CPP /nologo /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\aig" /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\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 /YX /FD /GZ /c # SUBTRACT CPP /X # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" @@ -210,6 +210,10 @@ SOURCE=.\src\base\abci\abcMiter.c # End Source File # Begin Source File +SOURCE=.\src\base\abci\abcNewAig.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abci\abcNtbdd.c # End Source File # Begin Source File @@ -1098,16 +1102,32 @@ SOURCE=.\src\sat\aig\fraigClass.c # End Source File # Begin Source File +SOURCE=.\src\sat\aig\fraigCnf.c +# End Source File +# Begin Source File + SOURCE=.\src\sat\aig\fraigCore.c # End Source File # Begin Source File +SOURCE=.\src\sat\aig\fraigEngine.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 +# Begin Source File + +SOURCE=.\src\sat\aig\fraigSolver.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\aig\fraigTrav.c +# End Source File # End Group # End Group # Begin Group "opt" Binary files differ@@ -6,13 +6,13 @@ --------------------Configuration: abc - Win32 Debug-------------------- </h3> <h3>Command Lines</h3> -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FE.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E2.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\sat\aig\aigReplace.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\aig" /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\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\sat\aig\fraigSim.c" ] -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 +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E2.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E3.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 @@ -210,12 +210,21 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\fraigVec.obj .\Debug\csat_apis.obj .\Debug\aigBalance.obj +.\Debug\aigCheck.obj .\Debug\aigFanout.obj .\Debug\aigMan.obj .\Debug\aigMem.obj .\Debug\aigNode.obj .\Debug\aigOper.obj +.\Debug\aigReplace.obj +.\Debug\aigTable.obj .\Debug\aigUtil.obj +.\Debug\fraigClass.obj +.\Debug\fraigCore.obj +.\Debug\fraigProve.obj +.\Debug\fraigSim.obj +.\Debug\fraigSolver.obj +.\Debug\fraigTrav.obj .\Debug\fxu.obj .\Debug\fxuCreate.obj .\Debug\fxuHeapD.obj @@ -346,20 +355,16 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\mvcPrint.obj .\Debug\mvcSort.obj .\Debug\mvcUtils.obj -.\Debug\aigTable.obj -.\Debug\aigCheck.obj -.\Debug\aigReplace.obj -.\Debug\fraigCore.obj -.\Debug\fraigProve.obj -.\Debug\fraigSim.obj -.\Debug\fraigClass.obj +.\Debug\abcNewAig.obj +.\Debug\fraigCnf.obj +.\Debug\fraigEngine.obj ] -Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FF.tmp" +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E3.tmp" <h3>Output Window</h3> Compiling... -aigReplace.c +fraigSim.c Linking... -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E4.tmp" with contents [ /nologo /o"Debug/abc.bsc" .\Debug\abcAig.sbr @@ -557,12 +562,21 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp" with conte .\Debug\fraigVec.sbr .\Debug\csat_apis.sbr .\Debug\aigBalance.sbr +.\Debug\aigCheck.sbr .\Debug\aigFanout.sbr .\Debug\aigMan.sbr .\Debug\aigMem.sbr .\Debug\aigNode.sbr .\Debug\aigOper.sbr +.\Debug\aigReplace.sbr +.\Debug\aigTable.sbr .\Debug\aigUtil.sbr +.\Debug\fraigClass.sbr +.\Debug\fraigCore.sbr +.\Debug\fraigProve.sbr +.\Debug\fraigSim.sbr +.\Debug\fraigSolver.sbr +.\Debug\fraigTrav.sbr .\Debug\fxu.sbr .\Debug\fxuCreate.sbr .\Debug\fxuHeapD.sbr @@ -693,14 +707,10 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp" with conte .\Debug\mvcPrint.sbr .\Debug\mvcSort.sbr .\Debug\mvcUtils.sbr -.\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" +.\Debug\abcNewAig.sbr +.\Debug\fraigCnf.sbr +.\Debug\fraigEngine.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E4.tmp" Creating browse info file... <h3>Output Window</h3> @@ -6,14 +6,157 @@ --------------------Configuration: abclib - Win32 Debug-------------------- </h3> <h3>Command Lines</h3> -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F0.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP513.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 "_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\abc\abcAig.c" +"C:\_projects\abc\src\base\abc\abcCheck.c" +"C:\_projects\abc\src\base\abc\abcDfs.c" +"C:\_projects\abc\src\base\abc\abcFanio.c" +"C:\_projects\abc\src\base\abc\abcFunc.c" +"C:\_projects\abc\src\base\abc\abcLatch.c" +"C:\_projects\abc\src\base\abc\abcMinBase.c" +"C:\_projects\abc\src\base\abc\abcNames.c" +"C:\_projects\abc\src\base\abc\abcNetlist.c" +"C:\_projects\abc\src\base\abc\abcNtk.c" +"C:\_projects\abc\src\base\abc\abcObj.c" +"C:\_projects\abc\src\base\abc\abcRefs.c" +"C:\_projects\abc\src\base\abc\abcShow.c" +"C:\_projects\abc\src\base\abc\abcSop.c" +"C:\_projects\abc\src\base\abc\abcUtil.c" "C:\_projects\abc\src\base\abci\abc.c" +"C:\_projects\abc\src\base\abci\abcAttach.c" +"C:\_projects\abc\src\base\abci\abcBalance.c" +"C:\_projects\abc\src\base\abci\abcCollapse.c" +"C:\_projects\abc\src\base\abci\abcCut.c" +"C:\_projects\abc\src\base\abci\abcDsd.c" +"C:\_projects\abc\src\base\abci\abcFpga.c" +"C:\_projects\abc\src\base\abci\abcFraig.c" +"C:\_projects\abc\src\base\abci\abcFxu.c" +"C:\_projects\abc\src\base\abci\abcMap.c" +"C:\_projects\abc\src\base\abci\abcMiter.c" +"C:\_projects\abc\src\base\abci\abcNtbdd.c" +"C:\_projects\abc\src\base\abci\abcPga.c" +"C:\_projects\abc\src\base\abci\abcPrint.c" +"C:\_projects\abc\src\base\abci\abcReconv.c" +"C:\_projects\abc\src\base\abci\abcRefactor.c" +"C:\_projects\abc\src\base\abci\abcRenode.c" +"C:\_projects\abc\src\base\abci\abcRewrite.c" +"C:\_projects\abc\src\base\abci\abcSat.c" +"C:\_projects\abc\src\base\abci\abcStrash.c" +"C:\_projects\abc\src\base\abci\abcSweep.c" +"C:\_projects\abc\src\base\abci\abcSymm.c" +"C:\_projects\abc\src\base\abci\abcTiming.c" +"C:\_projects\abc\src\base\abci\abcUnreach.c" +"C:\_projects\abc\src\base\abci\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\io\ioWriteVerilog.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\sat\fraig\fraigSat.c" +"C:\_projects\abc\src\sat\csat\csat_apis.c" +"C:\_projects\abc\src\opt\fxu\fxuCreate.c" +"C:\_projects\abc\src\opt\fxu\fxuReduce.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\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\fpgaCreate.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" ] -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 +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP513.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP514.tmp" with contents [ /nologo /out:"abclib\abclib_debug.lib" .\abclib\DebugLib\abcAig.obj @@ -96,6 +239,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F1.tmp" with cont .\abclib\DebugLib\ioWriteGml.obj .\abclib\DebugLib\ioWriteList.obj .\abclib\DebugLib\ioWritePla.obj +.\abclib\DebugLib\ioWriteVerilog.obj .\abclib\DebugLib\libSupport.obj .\abclib\DebugLib\main.obj .\abclib\DebugLib\mainFrame.obj @@ -331,16 +475,158 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F1.tmp" with cont .\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\RSP15F1.tmp" +Creating command line "link.exe -lib @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP514.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 -c:\_projects\abc\src\base\abci\abc.c(2890) : warning C4013: 'Abc_NtkMiterSat2' undefined; assuming extern returning int +C:\_projects\abc\src\base\abci\abc.c(2890) : warning C4013: 'Abc_NtkMiterSat2' undefined; assuming extern returning int +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 ioWriteVerilog.c +libSupport.c +main.c +mainFrame.c +mainInit.c +mainUtils.c +fraigSat.c +csat_apis.c +fxuCreate.c +fxuReduce.c +rwrDec.c +rwrEva.c +rwrExp.c +rwrLib.c +rwrMan.c +rwrPrint.c +rwrUtil.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 +fpgaCreate.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 Creating library... -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F2.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP515.tmp" with contents [ /nologo /o"abclib\DebugLib/abclib.bsc" .\abclib\DebugLib\abcAig.sbr @@ -423,6 +709,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F2.tmp" with cont .\abclib\DebugLib\ioWriteGml.sbr .\abclib\DebugLib\ioWriteList.sbr .\abclib\DebugLib\ioWritePla.sbr +.\abclib\DebugLib\ioWriteVerilog.sbr .\abclib\DebugLib\libSupport.sbr .\abclib\DebugLib\main.sbr .\abclib\DebugLib\mainFrame.sbr @@ -657,9 +944,8 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F2.tmp" with cont .\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" +.\abclib\DebugLib\mvcUtils.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP515.tmp" Creating browse info file... <h3>Output Window</h3> diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 259187bf..5f5c4b49 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3782,8 +3782,9 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk;//, * pNtkRes; + Abc_Ntk_t * pNtk, * pNtkRes; int c; + extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3807,19 +3808,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( !Abc_NtkIsStrash(pNtk) ) + if ( Abc_NtkIsSeq(pNtk) ) { - fprintf( pErr, "Only works for strashed networks.\n" ); + fprintf( pErr, "Only works for non-sequential networks.\n" ); return 1; } // Abc_NtkTestEsop( pNtk ); // Abc_NtkTestSop( pNtk ); // printf( "This command is currently not used.\n" ); - -/* // run the command - pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); +// pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); + pNtkRes = Abc_NtkNewAig( pNtk ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -3827,7 +3827,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); -*/ return 0; usage: diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c new file mode 100644 index 00000000..33f58135 --- /dev/null +++ b/src/base/abci/abcNewAig.c @@ -0,0 +1,376 @@ +/**CFile**************************************************************** + + FileName [aigNewAig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Strashing of the current network.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: aigNewAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "extra.h" +#include "dec.h" +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ); +static Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ); + +static void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan ); +static Aig_Node_t * Abc_NodeStrashAig( Aig_Man_t * pMan, Abc_Obj_t * pNode ); +static Aig_Node_t * Abc_NodeStrashAigSopAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); +static Aig_Node_t * Abc_NodeStrashAigExorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); +static Aig_Node_t * Abc_NodeStrashAigFactorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); +extern char * Mio_GateReadSop( void * pGate ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ) +{ + Aig_Man_t * pMan; + Abc_Ntk_t * pNtkAig; + Aig_ProofType_t RetValue; + int fCleanup = 1; + int nNodes; + + assert( !Abc_NtkIsNetlist(pNtk) ); + assert( !Abc_NtkIsSeq(pNtk) ); + if ( Abc_NtkIsBddLogic(pNtk) ) + Abc_NtkBddToSop(pNtk); + // print warning about choice nodes + if ( Abc_NtkGetChoiceNum( pNtk ) ) + printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); + + // convert to the AIG manager + pMan = Abc_NtkToAig( pNtk ); + // execute a command in the AIG manager + RetValue = Aig_FraigProve( pMan ); + if ( RetValue == AIG_PROOF_SAT ) + printf( "Satisfiable.\n" ); + else if ( RetValue == AIG_PROOF_UNSAT ) + printf( "Unsatisfiable.\n" ); + else if ( RetValue == AIG_PROOF_TIMEOUT ) + printf( "Undecided.\n" ); + else + assert( 0 ); + + // convert from the AIG manager + pNtkAig = Abc_NtkFromAig( pNtk, pMan ); + Aig_ManStop( pMan ); + + // report the cleanup results + if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) + printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes ); + // duplicate EXDC + if ( pNtk->pExdc ) + pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkStrash: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) +{ + Abc_Ntk_t * pNtk; + Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; + Aig_Node_t * pAnd; + int i; + // perform strashing + pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->Data = Abc_NtkConst1(pNtk)->Id; + Abc_NtkForEachCi( pNtkOld, pObj, i ) + Aig_ManPi(pMan, i)->Data = pObj->pCopy->Id; + // rebuild the AIG + Aig_ManForEachAnd( pMan, pAnd, i ) + { + // add the first fanins + pFaninNew0 = Abc_NtkObj( pNtk, Aig_NodeFanin0(pAnd)->Data ); + pFaninNew0 = Abc_ObjNotCond( pFaninNew0, Aig_NodeFaninC0(pAnd) ); + // add the first second + pFaninNew1 = Abc_NtkObj( pNtk, Aig_NodeFanin1(pAnd)->Data ); + pFaninNew1 = Abc_ObjNotCond( pFaninNew1, Aig_NodeFaninC1(pAnd) ); + // create the new node + pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 ); + pAnd->Data = pObjNew->Id; + } + // connect the PO nodes + Abc_NtkForEachCo( pNtkOld, pObj, i ) + { + pAnd = Aig_ManPo( pMan, i ); + pFaninNew = Abc_NtkObj( pNtk, Aig_NodeFanin0(pAnd)->Data ); + pFaninNew = Abc_ObjNotCond( pFaninNew, Aig_NodeFaninC0(pAnd) ); + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); + } + return pNtk; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ) +{ + Aig_Param_t Params; + Aig_Man_t * pMan; + Abc_Obj_t * pObj; + Aig_Node_t * pFanin; + int i; + // create the manager + Aig_ManSetDefaultParams( &Params ); + pMan = Aig_ManStart( &Params ); + // create the PIs + Abc_NtkConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); + Abc_NtkForEachCi( pNtkOld, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePi(pMan); + // perform the conversion of the internal nodes + Abc_NtkStrashPerformAig( pNtkOld, pMan ); + // create the POs + Abc_NtkForEachCo( pNtkOld, pObj, i ) + { + pFanin = (Aig_Node_t *)Abc_ObjFanin0(pObj)->pCopy; + pFanin = Aig_NotCond( pFanin, Abc_ObjFaninC0(pObj) ); + pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePo( pMan, pFanin ); + } + return pMan; +} + +/**Function************************************************************* + + Synopsis [Prepares the network for strashing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan ) +{ +// ProgressBar * pProgress; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode; + int i; + vNodes = Abc_NtkDfs( pNtk, 0 ); +// pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { +// Extra_ProgressBarUpdate( pProgress, i, NULL ); + pNode->pCopy = (Abc_Obj_t *)Abc_NodeStrashAig( pMan, pNode ); + } +// Extra_ProgressBarStop( pProgress ); + Vec_PtrFree( vNodes ); +} + +/**Function************************************************************* + + Synopsis [Strashes one logic node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Abc_NodeStrashAig( Aig_Man_t * pMan, Abc_Obj_t * pNode ) +{ + int fUseFactor = 1; + char * pSop; + Aig_Node_t * pFanin0, * pFanin1; + extern int Abc_SopIsExorType( char * pSop ); + + assert( Abc_ObjIsNode(pNode) ); + + // consider the case when the graph is an AIG + if ( Abc_NtkIsStrash(pNode->pNtk) ) + { + if ( Abc_NodeIsConst(pNode) ) + return Aig_ManConst1(pMan); + pFanin0 = (Aig_Node_t *)Abc_ObjFanin0(pNode)->pCopy; + pFanin0 = Aig_NotCond( pFanin0, Abc_ObjFaninC0(pNode) ); + pFanin1 = (Aig_Node_t *)Abc_ObjFanin1(pNode)->pCopy; + pFanin1 = Aig_NotCond( pFanin1, Abc_ObjFaninC1(pNode) ); + return Aig_And( pMan, pFanin0, pFanin1 ); + } + + // get the SOP of the node + if ( Abc_NtkHasMapping(pNode->pNtk) ) + pSop = Mio_GateReadSop(pNode->pData); + else + pSop = pNode->pData; + + // consider the constant node + if ( Abc_NodeIsConst(pNode) ) + return Aig_NotCond( Aig_ManConst1(pMan), Abc_SopIsConst0(pSop) ); + + // consider the special case of EXOR function + if ( Abc_SopIsExorType(pSop) ) + return Abc_NodeStrashAigExorAig( pMan, pNode, pSop ); + + // decide when to use factoring + if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 ) + return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop ); + return Abc_NodeStrashAigSopAig( pMan, pNode, pSop ); +} + +/**Function************************************************************* + + Synopsis [Strashes one logic node using its SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Abc_NodeStrashAigSopAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ) +{ + Abc_Obj_t * pFanin; + Aig_Node_t * pAnd, * pSum; + char * pCube; + int i, nFanins; + + // get the number of node's fanins + nFanins = Abc_ObjFaninNum( pNode ); + assert( nFanins == Abc_SopGetVarNum(pSop) ); + // go through the cubes of the node's SOP + pSum = Aig_Not( Aig_ManConst1(pMan) ); + Abc_SopForEachCube( pSop, nFanins, pCube ) + { + // create the AND of literals + pAnd = Aig_ManConst1(pMan); + Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net + { + if ( pCube[i] == '1' ) + pAnd = Aig_And( pMan, pAnd, (Aig_Node_t *)pFanin->pCopy ); + else if ( pCube[i] == '0' ) + pAnd = Aig_And( pMan, pAnd, Aig_Not((Aig_Node_t *)pFanin->pCopy) ); + } + // add to the sum of cubes + pSum = Aig_Or( pMan, pSum, pAnd ); + } + // decide whether to complement the result + if ( Abc_SopIsComplement(pSop) ) + pSum = Aig_Not(pSum); + return pSum; +} + +/**Function************************************************************* + + Synopsis [Strashed n-input XOR function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Abc_NodeStrashAigExorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ) +{ + Abc_Obj_t * pFanin; + Aig_Node_t * pSum; + int i, nFanins; + // get the number of node's fanins + nFanins = Abc_ObjFaninNum( pNode ); + assert( nFanins == Abc_SopGetVarNum(pSop) ); + // go through the cubes of the node's SOP + pSum = Aig_Not( Aig_ManConst1(pMan) ); + for ( i = 0; i < nFanins; i++ ) + { + pFanin = Abc_ObjFanin( pNode, i ); + pSum = Aig_Xor( pMan, pSum, (Aig_Node_t *)pFanin->pCopy ); + } + if ( Abc_SopIsComplement(pSop) ) + pSum = Aig_Not(pSum); + return pSum; +} + +/**Function************************************************************* + + Synopsis [Strashes one logic node using its SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Abc_NodeStrashAigFactorAig( Aig_Man_t * pMan, Abc_Obj_t * pRoot, char * pSop ) +{ + Dec_Graph_t * pFForm; + Dec_Node_t * pNode; + Aig_Node_t * pAnd; + int i; + extern Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph ); + + // perform factoring + pFForm = Dec_Factor( pSop ); + // collect the fanins + Dec_GraphForEachLeaf( pFForm, pNode, i ) + pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy; + // perform strashing + pAnd = Dec_GraphToNetworkAig( pMan, pFForm ); + Dec_GraphFree( pFForm ); + return pAnd; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 8c8636c5..f7b9892e 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -534,10 +534,10 @@ int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_ Vec_IntPush( vVars, toLitCond(VarF, 1) ); if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) return 0; - + if ( VarT == VarE ) { - assert( fCompT == !fCompE ); +// assert( fCompT == !fCompE ); return 1; } @@ -774,7 +774,7 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ) RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk ); Abc_NtkForEachObj( pNtk, pNode, i ) pNode->fMarkA = 0; - Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); +// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); if ( RetValue == 0 ) { solver_delete(pSat); diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c index 865cd830..58b824d2 100644 --- a/src/bdd/dsd/dsdCheck.c +++ b/src/bdd/dsd/dsdCheck.c @@ -82,7 +82,7 @@ void Dsd_CheckCacheAllocate( int nEntries ) /**Function******************************************************************** - Synopsis [Delocates the local cache.] + Synopsis [Deallocates the local cache.] Description [] diff --git a/src/misc/extra/extraBddSymm.c b/src/misc/extra/extraBddSymm.c index 474f663f..358402b0 100644 --- a/src/misc/extra/extraBddSymm.c +++ b/src/misc/extra/extraBddSymm.c @@ -223,7 +223,7 @@ Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars ) /**Function******************************************************************** - Synopsis [Delocates symmetry information structure.] + Synopsis [Deallocates symmetry information structure.] Description [] diff --git a/src/misc/extra/extraUtilMemory.c b/src/misc/extra/extraUtilMemory.c index af1128ac..c9137c56 100644 --- a/src/misc/extra/extraUtilMemory.c +++ b/src/misc/extra/extraUtilMemory.c @@ -257,7 +257,7 @@ void Extra_MmFixedRestart( Extra_MmFixed_t * p ) int i; char * pTemp; - // delocate all chunks except the first one + // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) free( p->pChunks[i] ); p->nChunks = 1; diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c index 1416cf0d..b24773be 100644 --- a/src/opt/dec/decAbc.c +++ b/src/opt/dec/decAbc.c @@ -18,6 +18,7 @@ #include "abc.h" #include "dec.h" +#include "aig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -201,6 +202,40 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpda assert( nGain <= nNodesOld - nNodesNew ); } + +/**Function************************************************************* + + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph ) +{ + Dec_Node_t * pNode; + Aig_Node_t * pAnd0, * pAnd1; + int i; + // check for constant function + if ( Dec_GraphIsConst(pGraph) ) + return Aig_NotCond( Aig_ManConst1(pMan), Dec_GraphIsComplement(pGraph) ); + // check for a literal + if ( Dec_GraphIsVar(pGraph) ) + return Aig_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) ); + // build the AIG nodes corresponding to the AND gates of the graph + Dec_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + pAnd1 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 ); + } + // complement the result if necessary + return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c index 9da34fde..169fb218 100644 --- a/src/opt/fxu/fxu.c +++ b/src/opt/fxu/fxu.c @@ -159,7 +159,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) if ( pData->nNodesNew ) Fxu_CreateCovers( p, pData ); Fxu_MatrixDelete( p ); -// printf( "Memory usage after delocation: Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak ); +// printf( "Memory usage after deallocation: Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak ); if ( pData->nNodesNew == pData->nNodesExt ) printf( "Warning: The limit on the number of extracted divisors has been reached.\n" ); return pData->nNodesNew; diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h index 009a17bb..55a75cf5 100644 --- a/src/sat/aig/aig.h +++ b/src/sat/aig/aig.h @@ -48,6 +48,7 @@ //////////////////////////////////////////////////////////////////////// #include <stdio.h> +#include "solver.h" #include "vec.h" //////////////////////////////////////////////////////////////////////// @@ -70,6 +71,7 @@ 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; +typedef struct Aig_Pattern_t_ Aig_Pattern_t; // network types typedef enum { @@ -79,12 +81,25 @@ typedef enum { AIG_AND // 3: internal node } Aig_NodeType_t; +// proof outcomes +typedef enum { + AIG_PROOF_NONE = 0, // 0: unknown + AIG_PROOF_SAT, // 1: primary input + AIG_PROOF_UNSAT, // 2: primary output + AIG_PROOF_TIMEOUT, // 3: primary output + AIG_PROOF_FAIL // 4: internal node +} Aig_ProofType_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 + int fVerbose; // verbosity + int fSatVerbose; // verbosity of SAT }; // the AIG edge @@ -127,6 +142,13 @@ struct Aig_Man_t_ Vec_Ptr_t * vPos; // all POs Aig_Table_t * pTable; // structural hash table int nLevelMax; // the maximum level + // SAT solver and related structures + solver * pSat; + Vec_Int_t * vVar2Sat; // mapping of nodes into their SAT var numbers (for each node num) + Vec_Int_t * vSat2Var; // mapping of the SAT var numbers into nodes (for each SAT var) + Vec_Int_t * vPiSatNums; // the SAT variable numbers (for each PI) + int * pModel; // the satisfying assignment (for each PI) + int nMuxes; // the number of MUXes // fanout representation Vec_Ptr_t * vFanPivots; // fanout pivots Vec_Ptr_t * vFanFans0; // the next fanout of the first fanin @@ -136,6 +158,7 @@ struct Aig_Man_t_ int nTravIds; // the traversal ID // simulation info Aig_SimInfo_t * pInfo; // random and systematic sim info for PIs + Aig_SimInfo_t * pInfoPi; // temporary sim info for the PI nodes Aig_SimInfo_t * pInfoTemp; // temporary sim info for all nodes // simulation patterns int nPiWords; // the number of words in the PI info @@ -148,6 +171,14 @@ struct Aig_Man_t_ Vec_Ptr_t * vToReplace; // the nodes to replace }; +// the simulation patter +struct Aig_Pattern_t_ +{ + int nBits; + int nWords; + unsigned * pData; +}; + // the AIG simulation info struct Aig_SimInfo_t_ { @@ -166,9 +197,9 @@ struct Aig_SimInfo_t_ 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 ) \ +#define Aig_ManForEachAnd( pMan, pNode, i ) \ for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ ) \ - if ( Aig_NodeIsAnd(pNode) ) {} else + if ( !Aig_NodeIsAnd(pNode) ) {} else // maximum/minimum operators #define AIG_MIN(a,b) (((a) < (b))? (a) : (b)) @@ -178,8 +209,12 @@ struct Aig_SimInfo_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); } +static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); } +static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } +static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } +static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } +static inline Aig_Node_t * Aig_ManConst1( Aig_Man_t * pMan ) { return pMan->pConst1; } 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); } @@ -216,7 +251,8 @@ static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode ) { return Aig_N 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 int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); } +static inline int Aig_NodeRequiredLevel( Aig_Node_t * pNode ) { return pNode->pMan->nLevelMax + 1 - pNode->LevelR; } 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; } @@ -268,6 +304,7 @@ 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 ); +extern void Aig_PrintNode( 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 ); @@ -287,18 +324,33 @@ 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 ); +extern bool Aig_NodeIsMuxType( Aig_Node_t * pNode ); +extern Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE ); +/*=== fraigCore.c ==========================================================*/ +extern Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan ); /*=== fraigClasses.c ==========================================================*/ extern Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll ); +extern void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses ); +/*=== fraigCnf.c ==========================================================*/ +extern Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan ); +/*=== fraigEngine.c ==========================================================*/ +extern void Aig_EngineSimulateFirst( Aig_Man_t * p ); +extern int Aig_EngineSimulate( Aig_Man_t * p ); +extern void Aig_EngineSimulateRandomFirst( Aig_Man_t * p ); /*=== 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_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat ); 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 ); +extern void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll ); +extern Aig_Pattern_t * Aig_PatternAlloc( int nBits ); +extern void Aig_PatternClean( Aig_Pattern_t * pPat ); +extern void Aig_PatternRandom( Aig_Pattern_t * pPat ); +extern void Aig_PatternFree( Aig_Pattern_t * pPat ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c index 2058f6b0..3807d28a 100644 --- a/src/sat/aig/aigMan.c +++ b/src/sat/aig/aigMan.c @@ -66,10 +66,11 @@ Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam ) // start the manager p = ALLOC( Aig_Man_t, 1 ); memset( p, 0, sizeof(Aig_Man_t) ); - p->pParam = &p->Param; - p->nTravIds = 1; + p->pParam = &p->Param; + p->nTravIds = 1; + p->nPatsMax = 20; // set the defaults - *p->pParam = *pParam; + *p->pParam = *pParam; // start memory managers p->mmNodes = Aig_MemFixedStart( sizeof(Aig_Node_t) ); // allocate node arrays @@ -121,14 +122,22 @@ int Aig_ManCleanup( Aig_Man_t * pMan ) ***********************************************************************/ void Aig_ManStop( Aig_Man_t * p ) { + // SAT solver + if ( p->pSat ) solver_delete( p->pSat ); + if ( p->vVar2Sat ) Vec_IntFree( p->vVar2Sat ); + if ( p->vSat2Var ) Vec_IntFree( p->vSat2Var ); + if ( p->vPiSatNums ) Vec_IntFree( p->vPiSatNums ); + // fanouts 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 ); + // nodes Aig_MemFixedStop( p->mmNodes, 0 ); Vec_PtrFree( p->vNodes ); Vec_PtrFree( p->vPis ); Vec_PtrFree( p->vPos ); + // temporary Vec_PtrFree( p->vFanouts ); Vec_PtrFree( p->vToReplace ); Aig_TableFree( p->pTable ); diff --git a/src/sat/aig/aigMem.c b/src/sat/aig/aigMem.c index 280cf98b..32709bf6 100644 --- a/src/sat/aig/aigMem.c +++ b/src/sat/aig/aigMem.c @@ -201,7 +201,7 @@ void Aig_MemFixedRestart( Aig_MemFixed_t * p ) int i; char * pTemp; - // delocate all chunks except the first one + // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) free( p->pChunks[i] ); p->nChunks = 1; diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c index afccd985..991cc7e5 100644 --- a/src/sat/aig/aigNode.c +++ b/src/sat/aig/aigNode.c @@ -46,6 +46,7 @@ static inline Aig_Node_t * Aig_NodeCreate( Aig_Man_t * p ) 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->pMan = p; pNode->Id = p->vNodes->nSize; Vec_PtrPush( p->vNodes, pNode ); return pNode; @@ -66,6 +67,7 @@ Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p ) { Aig_Node_t * pNode; pNode = Aig_NodeCreate( p ); + pNode->Type = AIG_NONE; pNode->fPhase = 1; // sim value for 000... pattern return pNode; } @@ -86,7 +88,8 @@ 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 + pNode->Type = AIG_PI; + pNode->fPhase = 0; // sim value for 000... pattern return pNode; } @@ -105,6 +108,7 @@ Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin ) { Aig_Node_t * pNode; pNode = Aig_NodeCreate( p ); + pNode->Type = AIG_PO; Vec_PtrPush( p->vPos, pNode ); // connect to the fanin pNode->Fans[0].fComp = Aig_IsComplement(pFanin); @@ -134,6 +138,7 @@ Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t { Aig_Node_t * pNode; pNode = Aig_NodeCreate( p ); + pNode->Type = AIG_AND; Aig_NodeConnectAnd( pFanin0, pFanin1, pNode ); return pNode; } diff --git a/src/sat/aig/aigTable.c b/src/sat/aig/aigTable.c index cfc94f6b..e6fe87d6 100644 --- a/src/sat/aig/aigTable.c +++ b/src/sat/aig/aigTable.c @@ -36,7 +36,7 @@ struct Aig_Table_t_ #define Aig_TableBinForEachEntry( pBin, pEnt ) \ for ( pEnt = pBin; \ pEnt; \ - pEnt = pEnt->NextH? Aig_ManNode(pEnt->pMan, pEnt->NextH) : NULL ) + pEnt = Aig_NodeNextH(pEnt) ) #define Aig_TableBinForEachEntrySafe( pBin, pEnt, pEnt2 ) \ for ( pEnt = pBin, \ pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL; \ @@ -127,9 +127,8 @@ Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t 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 ); + 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) ) @@ -157,8 +156,8 @@ Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t 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; + pAnd->NextH = pMan->pTable->pBins[Key]? pMan->pTable->pBins[Key]->Id : 0; + pMan->pTable->pBins[Key] = pAnd; pMan->pTable->nEntries++; return pAnd; } @@ -195,7 +194,7 @@ void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis ) if ( pPlace == NULL ) pMan->pTable->pBins[Key] = Aig_NodeNextH(pThis); else - pPlace->NextH = pThis->Id; + pPlace->NextH = pThis->NextH; break; } assert( pThis == pAnd ); @@ -232,8 +231,8 @@ clk = clock(); 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; + pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0; + pBinsNew[Key] = pEnt; Counter++; } assert( Counter == pMan->pTable->nEntries ); @@ -282,8 +281,8 @@ void Aig_TableRehash( Aig_Man_t * pMan ) } // 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; + pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0; + pBinsNew[Key] = pEnt; Counter++; } assert( Counter == pMan->pTable->nEntries ); diff --git a/src/sat/aig/aigUtil.c b/src/sat/aig/aigUtil.c index a1c9ca44..40f7aba1 100644 --- a/src/sat/aig/aigUtil.c +++ b/src/sat/aig/aigUtil.c @@ -53,6 +53,136 @@ void Aig_ManIncrementTravId( Aig_Man_t * pMan ) } +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Aig_NodeIsMuxType( Aig_Node_t * pNode ) +{ + Aig_Node_t * pNode0, * pNode1; + // check that the node is regular + assert( !Aig_IsComplement(pNode) ); + // if the node is not AND, this is not MUX + if ( !Aig_NodeIsAnd(pNode) ) + return 0; + // if the children are not complemented, this is not MUX + if ( !Aig_NodeFaninC0(pNode) || !Aig_NodeFaninC1(pNode) ) + return 0; + // get children + pNode0 = Aig_NodeFanin0(pNode); + pNode1 = Aig_NodeFanin1(pNode); + // if the children are not ANDs, this is not MUX + if ( !Aig_NodeIsAnd(pNode0) || !Aig_NodeIsAnd(pNode1) ) + return 0; + // otherwise the node is MUX iff it has a pair of equal grandchildren + return (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1))) || + (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1))) || + (Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1))) || + (Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1))); +} + +/**Function************************************************************* + + Synopsis [Recognizes what nodes are control and data inputs of a MUX.] + + Description [If the node is a MUX, returns the control variable C. + Assigns nodes T and E to be the then and else variables of the MUX. + Node C is never complemented. Nodes T and E can be complemented. + This function also recognizes EXOR/NEXOR gates as MUXes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE ) +{ + Aig_Node_t * pNode0, * pNode1; + assert( !Aig_IsComplement(pNode) ); + assert( Aig_NodeIsMuxType(pNode) ); + // get children + pNode0 = Aig_NodeFanin0(pNode); + pNode1 = Aig_NodeFanin1(pNode); + // find the control variable +// if ( pNode1->p1 == Fraig_Not(pNode2->p1) ) + if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Aig_NodeFaninC0(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2); + *ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2); + return Aig_NodeChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2); + *ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2); + return Aig_NodeChild0(pNode0);//pNode1->p1; + } + } +// else if ( pNode1->p1 == Fraig_Not(pNode2->p2) ) + else if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Aig_NodeFaninC0(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1); + *ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2); + return Aig_NodeChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2); + *ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1); + return Aig_NodeChild0(pNode0);//pNode1->p1; + } + } +// else if ( pNode1->p2 == Fraig_Not(pNode2->p1) ) + else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Aig_NodeFaninC1(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2); + *ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1); + return Aig_NodeChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1); + *ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2); + return Aig_NodeChild1(pNode0);//pNode1->p2; + } + } +// else if ( pNode1->p2 == Fraig_Not(pNode2->p2) ) + else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Aig_NodeFaninC1(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1); + *ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1); + return Aig_NodeChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1); + *ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1); + return Aig_NodeChild1(pNode0);//pNode1->p2; + } + } + assert( 0 ); // this is not MUX + return NULL; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c index b3040e2a..2f2d3e0c 100644 --- a/src/sat/aig/fraigClass.c +++ b/src/sat/aig/fraigClass.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [aigFraig.c] + FileName [fraigClass.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: fraigClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -25,7 +25,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static unsigned Aig_ManHashKey( unsigned * pData, int nWords ); +static unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -44,20 +44,24 @@ static unsigned Aig_ManHashKey( unsigned * pData, int nWords ); ***********************************************************************/ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) { - Vec_Vec_t * vClasses; // equivalence classes + 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; + int i, * pSpot, Entry, 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 ) + // enumerate the nodes considered in the equivalence classes +// Aig_ManForEachNode( p, pNode, i ) + Vec_IntForEachEntry( p->vSat2Var, Entry, i ) { + pNode = Aig_ManNode( p, Entry ); + if ( Aig_NodeIsPo(pNode) ) continue; - uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords ); + uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords, pNode->fPhase ); 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 @@ -71,11 +75,24 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) } else // this is a class { - ClassNum = (*pSpot) >> 1; + ClassNum = ((*pSpot) >> 1); Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id ); } } stmm_free_table( tSim2Node ); + + // print the classes + { + Vec_Ptr_t * vVec; + printf( "PI/PO = %4d/%4d. Nodes = %7d. SatVars = %7d. Non-trivial classes = %5d: \n", + Aig_ManPiNum(p), Aig_ManPoNum(p), + Aig_ManNodeNum(p) - Aig_ManPoNum(p), + Vec_IntSize(p->vSat2Var), Vec_VecSize(vClasses) ); + + Vec_VecForEachLevel( vClasses, vVec, i ) + printf( "%d ", Vec_PtrSize(vVec) ); + printf( "\n" ); + } return vClasses; } @@ -90,17 +107,38 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) SeeAlso [] ***********************************************************************/ -unsigned Aig_ManHashKey( unsigned * pData, int nWords ) +unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase ) { 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]; + if ( fPhase ) + for ( i = 0; i < nWords; i++ ) + uKey ^= Primes[i%10] * pData[i]; + else + for ( i = 0; i < nWords; i++ ) + uKey ^= Primes[i%10] * ~pData[i]; return uKey; } + +/**Function************************************************************* + + Synopsis [Updates the equivalence classes using the simulation info.] + + Description [Records successful simulation patterns into the pattern + storage.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses ) +{ +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/aig/fraigCnf.c b/src/sat/aig/fraigCnf.c new file mode 100644 index 00000000..913165b2 --- /dev/null +++ b/src/sat/aig/fraigCnf.c @@ -0,0 +1,476 @@ +/**CFile**************************************************************** + + FileName [fraigCnf.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: fraigCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ClauseTriv( solver * pSat, Aig_Node_t * pNode, Vec_Int_t * vVars ) +{ +//printf( "Adding triv %d. %d\n", Aig_Regular(pNode)->Id, (int)pSat->solver_stats.clauses ); + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond( Aig_Regular(pNode)->Data, Aig_IsComplement(pNode) ) ); +// Vec_IntPush( vVars, toLitCond( (int)Aig_Regular(pNode)->Id, Aig_IsComplement(pNode) ) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); +} + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ClauseAnd( solver * pSat, Aig_Node_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars ) +{ + int fComp1, Var, Var1, i; +//printf( "Adding AND %d. (%d) %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->solver_stats.clauses ); + + assert( !Aig_IsComplement( pNode ) ); + assert( Aig_NodeIsAnd( pNode ) ); + +// nVars = solver_nvars(pSat); + Var = pNode->Data; +// Var = pNode->Id; + +// assert( Var < nVars ); + for ( i = 0; i < vSuper->nSize; i++ ) + { + // get the predecessor nodes + // get the complemented attributes of the nodes + fComp1 = Aig_IsComplement(vSuper->pArray[i]); + // determine the variable numbers + Var1 = Aig_Regular(vSuper->pArray[i])->Data; +// Var1 = (int)Aig_Regular(vSuper->pArray[i])->Id; + + // check that the variables are in the SAT manager +// assert( Var1 < nVars ); + + // suppose the AND-gate is A * B = C + // add !A => !C or A + !C + // fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 ); + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(Var1, fComp1) ); + Vec_IntPush( vVars, toLitCond(Var, 1 ) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + } + + // add A & B => C or !A + !B + C +// fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 ); + vVars->nSize = 0; + for ( i = 0; i < vSuper->nSize; i++ ) + { + // get the predecessor nodes + // get the complemented attributes of the nodes + fComp1 = Aig_IsComplement(vSuper->pArray[i]); + // determine the variable numbers + Var1 = Aig_Regular(vSuper->pArray[i])->Data; +// Var1 = (int)Aig_Regular(vSuper->pArray[i])->Id; + // add this variable to the array + Vec_IntPush( vVars, toLitCond(Var1, !fComp1) ); + } + Vec_IntPush( vVars, toLitCond(Var, 0) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); +} + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ClauseMux( solver * pSat, Aig_Node_t * pNode, Aig_Node_t * pNodeC, Aig_Node_t * pNodeT, Aig_Node_t * pNodeE, Vec_Int_t * vVars ) +{ + int VarF, VarI, VarT, VarE, fCompT, fCompE; +//printf( "Adding mux %d. %d\n", pNode->Id, (int)pSat->solver_stats.clauses ); + + assert( !Aig_IsComplement( pNode ) ); + assert( Aig_NodeIsMuxType( pNode ) ); + // get the variable numbers + VarF = pNode->Data; + VarI = pNodeC->Data; + VarT = Aig_Regular(pNodeT)->Data; + VarE = Aig_Regular(pNodeE)->Data; +// VarF = (int)pNode->Id; +// VarI = (int)pNodeC->Id; +// VarT = (int)Aig_Regular(pNodeT)->Id; +// VarE = (int)Aig_Regular(pNodeE)->Id; + + // get the complementation flags + fCompT = Aig_IsComplement(pNodeT); + fCompE = Aig_IsComplement(pNodeE); + + // f = ITE(i, t, e) + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + // create four clauses + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 1) ); + Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarF, 0) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 1) ); + Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarF, 1) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 0) ); + Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 0) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 0) ); + Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 1) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return 1; + } + + // two additional clauses + // t' & e' -> f' t + e + f' + // t & e -> f t' + e' + f + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 1) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 0) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ClauseCollectSupergate_rec( Aig_Node_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux ) +{ + int RetValue1, RetValue2, i; + // check if the node is visited + if ( Aig_Regular(pNode)->fMarkB ) + { + // check if the node occurs in the same polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == pNode ) + return 1; + // check if the node is present in the opposite polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == Aig_Not(pNode) ) + return -1; + assert( 0 ); + return 0; + } + // if the new node is complemented or a PI, another gate begins + if ( !fFirst ) + if ( Aig_IsComplement(pNode) || !Aig_NodeIsAnd(pNode) || Aig_NodeRefs(pNode) > 1 || fStopAtMux && Aig_NodeIsMuxType(pNode) ) + { + Vec_PtrPush( vSuper, pNode ); + Aig_Regular(pNode)->fMarkB = 1; + return 0; + } + assert( !Aig_IsComplement(pNode) ); + assert( Aig_NodeIsAnd(pNode) ); + // go through the branches + RetValue1 = Aig_ClauseCollectSupergate_rec( Aig_NodeChild0(pNode), vSuper, 0, fStopAtMux ); + RetValue2 = Aig_ClauseCollectSupergate_rec( Aig_NodeChild1(pNode), vSuper, 0, fStopAtMux ); + if ( RetValue1 == -1 || RetValue2 == -1 ) + return -1; + // return 1 if at least one branch has a duplicate + return RetValue1 || RetValue2; +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ClauseCollectSupergate( Aig_Node_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes ) +{ + int RetValue, i; + assert( !Aig_IsComplement(pNode) ); + // collect the nodes in the implication supergate + Vec_PtrClear( vNodes ); + RetValue = Aig_ClauseCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux ); + assert( vNodes->nSize > 1 ); + // unmark the visited nodes + for ( i = 0; i < vNodes->nSize; i++ ) + Aig_Regular((Aig_Node_t *)vNodes->pArray[i])->fMarkB = 0; + // if we found the node and its complement in the same implication supergate, + // return empty set of nodes (meaning that we should use constant-0 node) + if ( RetValue == -1 ) + vNodes->nSize = 0; +} + + +/**Function************************************************************* + + Synopsis [Sets up the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ClauseCreateCnfInt( solver * pSat, Aig_Man_t * pNtk ) +{ + Aig_Node_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE; + Vec_Ptr_t * vNodes, * vSuper; + Vec_Int_t * vVars; + int i, k, fUseMuxes = 1; + + // start the data structures + vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the solver + vSuper = Vec_PtrAlloc( 100 ); // the nodes belonging to the given implication supergate + vVars = Vec_IntAlloc( 100 ); // the temporary array for variables in the clause + + // add the clause for the constant node + pNode = Aig_ManConst1(pNtk); + pNode->fMarkA = 1; + pNode->Data = vNodes->nSize; + Vec_PtrPush( vNodes, pNode ); + Aig_ClauseTriv( pSat, pNode, vVars ); + + // collect the nodes that need clauses and top-level assignments + Aig_ManForEachPo( pNtk, pNode, i ) + { + // get the fanin + pFanin = Aig_NodeFanin0(pNode); + // create the node's variable + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->Data = vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + // add the trivial clause + if ( !Aig_ClauseTriv( pSat, Aig_NodeChild0(pNode), vVars ) ) + return 0; + } + + // add the clauses + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + assert( !Aig_IsComplement(pNode) ); + if ( !Aig_NodeIsAnd(pNode) ) + continue; +//printf( "%d ", pNode->Id ); + + // add the clauses + if ( fUseMuxes && Aig_NodeIsMuxType(pNode) ) + { + pNode->pMan->nMuxes++; + pNodeC = Aig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE ); + Vec_PtrClear( vSuper ); + Vec_PtrPush( vSuper, pNodeC ); + Vec_PtrPush( vSuper, pNodeT ); + Vec_PtrPush( vSuper, pNodeE ); + // add the fanin nodes to explore + Vec_PtrForEachEntry( vSuper, pFanin, k ) + { + pFanin = Aig_Regular(pFanin); + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->Data = vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + } + // add the clauses + if ( !Aig_ClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) ) + return 0; + } + else + { + // get the supergate + Aig_ClauseCollectSupergate( pNode, fUseMuxes, vSuper ); + // add the fanin nodes to explore + Vec_PtrForEachEntry( vSuper, pFanin, k ) + { + pFanin = Aig_Regular(pFanin); + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->Data = vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + } + // add the clauses + if ( vSuper->nSize == 0 ) + { + if ( !Aig_ClauseTriv( pSat, Aig_Not(pNode), vVars ) ) + return 0; + } + else + { + if ( !Aig_ClauseAnd( pSat, pNode, vSuper, vVars ) ) + return 0; + } + } + } + + // delete + Vec_IntFree( vVars ); + Vec_PtrFree( vNodes ); + Vec_PtrFree( vSuper ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Sets up the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +solver * Aig_ClauseCreateCnf( Aig_Man_t * pMan ) +{ + solver * pSat; + Aig_Node_t * pNode; + int RetValue, i, clk = clock(); + // clean the marks + Aig_ManForEachNode( pMan, pNode, i ) + pNode->fMarkA = 0, pNode->Data = -1; + // create the solver + pMan->nMuxes = 0; + pSat = solver_new(); + RetValue = Aig_ClauseCreateCnfInt( pSat, pMan ); +// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); + if ( RetValue == 0 ) + { + solver_delete(pSat); + Aig_ManForEachNode( pMan, pNode, i ) + pNode->fMarkA = 0; + return NULL; + } + printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", + pNode->pMan->nMuxes, 300.0*pNode->pMan->nMuxes/Aig_ManNodeNum(pMan) ); + PRT( "Creating solver", clock() - clk ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [Starts the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan ) +{ + Aig_Node_t * pNode; + int i; + + // make sure it has one PO + if ( Aig_ManPoNum(pMan) != 1 ) + { + printf( "The miter has other than 1 output.\n" ); + return AIG_PROOF_FAIL; + } + + // get the solver + assert( pMan->pSat == NULL ); + pMan->pSat = Aig_ClauseCreateCnf( pMan ); + if ( pMan->pSat == NULL ) + return AIG_PROOF_UNSAT; + + // get the variable mappings + pMan->vVar2Sat = Vec_IntStart( Aig_ManNodeNum(pMan) ); + pMan->vSat2Var = Vec_IntStart( solver_nvars(pMan->pSat) ); + Aig_ManForEachNode( pMan, pNode, i ) + { + Vec_IntWriteEntry( pMan->vVar2Sat, i, pNode->Data ); + if ( pNode->Data >= 0 ) Vec_IntWriteEntry( pMan->vSat2Var, pNode->Data, i ); + } + // get the SAT var numbers of the primary inputs + pMan->vPiSatNums = Vec_IntAlloc( Aig_ManPiNum(pMan) ); + Aig_ManForEachPi( pMan, pNode, i ) + Vec_IntPush( pMan->vPiSatNums, (pNode->Data >= 0)? pNode->Data : 0 ); + return AIG_PROOF_NONE; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c index 6187538b..e7df1335 100644 --- a/src/sat/aig/fraigCore.c +++ b/src/sat/aig/fraigCore.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [aigFraig.c] + FileName [fraigCore.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: fraigCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -24,13 +24,56 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Top-level equivalence checking procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan ) +{ + Aig_ProofType_t RetValue; + int clk, status; + + // create the solver + RetValue = Aig_ClauseSolverStart( pMan ); + if ( RetValue != AIG_PROOF_NONE ) + return RetValue; + // perform solving + + // simplify the problem + clk = clock(); + status = solver_simplify(pMan->pSat); + if ( status == 0 ) + { +// printf( "The problem is UNSATISFIABLE after simplification.\n" ); + return AIG_PROOF_UNSAT; + } + + // try to prove the output + RetValue = Aig_FraigProveOutput( pMan ); + if ( RetValue != AIG_PROOF_TIMEOUT ) + return RetValue; + + // create equivalence classes + Aig_EngineSimulateRandomFirst( pMan ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Top-level equivalence checking procedure.] Description [] @@ -39,6 +82,43 @@ SeeAlso [] ***********************************************************************/ +Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan ) +{ + Aig_ProofType_t RetValue; + int clk, status; + + // solve the miter + clk = clock(); + pMan->pSat->verbosity = pMan->pParam->fSatVerbose; + status = solver_solve( pMan->pSat, NULL, NULL, pMan->pParam->nSeconds ); + if ( status == l_Undef ) + { +// printf( "The problem timed out.\n" ); + RetValue = AIG_PROOF_TIMEOUT; + } + else if ( status == l_True ) + { +// printf( "The problem is SATISFIABLE.\n" ); + RetValue = AIG_PROOF_SAT; + } + else if ( status == l_False ) + { +// printf( "The problem is UNSATISFIABLE.\n" ); + RetValue = AIG_PROOF_UNSAT; + } + else + assert( 0 ); +// PRT( "SAT solver time", clock() - clk ); + + // if the problem is SAT, get the counterexample + if ( status == l_True ) + { + if ( pMan->pModel ) free( pMan->pModel ); + pMan->pModel = solver_get_model( pMan->pSat, pMan->vPiSatNums->pArray, pMan->vPiSatNums->nSize ); + printf( "%d %d %d %d\n", pMan->pModel[0], pMan->pModel[1], pMan->pModel[2], pMan->pModel[3] ); + } + return RetValue; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/aig/fraigEngine.c b/src/sat/aig/fraigEngine.c new file mode 100644 index 00000000..6214bf3b --- /dev/null +++ b/src/sat/aig/fraigEngine.c @@ -0,0 +1,131 @@ +/**CFile**************************************************************** + + FileName [fraigEngine.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: fraigEngine.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the simulation engine for the first time.] + + Description [Tries several random patterns and their distance-1 + minterms hoping to get simulation started.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_EngineSimulateFirst( Aig_Man_t * p ) +{ + Aig_Pattern_t * pPat; + int i; + assert( Vec_PtrSize(p->vPats) == 0 ); + for ( i = 0; i < p->nPatsMax; i++ ) + { + pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); + Aig_PatternRandom( pPat ); + Vec_PtrPush( p->vPats, pPat ); + if ( !Aig_EngineSimulate( p ) ) + return; + } +} + +/**Function************************************************************* + + Synopsis [Implements intelligent simulation engine.] + + Description [Assumes that the good simulation patterns have been + assigned (p->vPats). Simulates until all of them are gone. Returns 1 + if some classes are left. Returns 0 if there is no more classes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_EngineSimulate( Aig_Man_t * p ) +{ + Aig_Pattern_t * pPat; + if ( Vec_VecSize(p->vClasses) == 0 ) + return 0; + assert( Vec_PtrSize(p->vPats) > 0 ); + // process patterns + while ( Vec_PtrSize(p->vPats) > 0 && Vec_VecSize(p->vClasses) > 0 ) + { + // get the pattern and create new siminfo + pPat = Vec_PtrPop(p->vPats); + // create the new siminfo + Aig_SimInfoFromPattern( p->pInfoPi, pPat ); + // free the patter + Aig_PatternFree( pPat ); + + // simulate this info + Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp ); + // split the classes and collect the new patterns + Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses ); + } + return Vec_VecSize(p->vClasses) > 0; +} + +/**Function************************************************************* + + Synopsis [Simulates all nodes using random simulation for the first time.] + + Description [Assigns the original simulation info and the storage for the + future simulation info.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_EngineSimulateRandomFirst( 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 ); + // allocate sim info for all nodes + pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 ); + // simulate though the circuit + Aig_ManSimulateInfo( p, pInfoPi, pInfoAll ); + // detect classes + p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll ); + Aig_SimInfoFree( pInfoAll ); + // save simulation info + p->pInfo = pInfoPi; + p->pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->vPis->nSize), 0 ); + p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/fraigProve.c b/src/sat/aig/fraigProve.c index b5cce582..901f2fe2 100644 --- a/src/sat/aig/fraigProve.c +++ b/src/sat/aig/fraigProve.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [aigProve.c] + FileName [fraigProve.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: aigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: fraigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ diff --git a/src/sat/aig/fraigSim.c b/src/sat/aig/fraigSim.c index 1d547621..415b6918 100644 --- a/src/sat/aig/fraigSim.c +++ b/src/sat/aig/fraigSim.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [aigSim.c] + FileName [fraigSim.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: aigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: fraigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -30,59 +30,28 @@ /**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 [] + Description [Returns the simulation info for all nodes.] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi ) +void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll ) { - Aig_SimInfo_t * pInfoAll; Aig_Node_t * pNode; - unsigned * pDataPi, * pData0, * pData1, * pDataAnd; + unsigned * pDataPi, * pDataPo, * 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 ) + // set the PI siminfo + Aig_ManForEachPi( p, pNode, i ) { pDataPi = Aig_SimInfoForPi( pInfoPi, i ); pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode ); @@ -90,10 +59,8 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi ) pDataAnd[k] = pDataPi[k]; } // simulate the nodes - Vec_PtrForEachEntry( p->vNodes, pNode, i ) + Aig_ManForEachAnd( p, 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 ); @@ -112,13 +79,25 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi ) for ( k = 0; k < pInfoPi->nWords; k++ ) pDataAnd[k] = pData0[k] & pData1[k]; } - return pInfoAll; + // derive the PO siminfo + Aig_ManForEachPi( p, pNode, i ) + { + pDataPo = Aig_SimInfoForNode( pInfoAll, pNode ); + pDataAnd = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) ); + if ( Aig_NodeFaninC0(pNode) ) + for ( k = 0; k < pInfoPi->nWords; k++ ) + pDataPo[k] = ~pDataAnd[k]; + else + for ( k = 0; k < pInfoPi->nWords; k++ ) + pDataPo[k] = pDataAnd[k]; + } } + /**Function************************************************************* - Synopsis [] + Synopsis [Allocates the simulation info.] Description [] @@ -142,7 +121,7 @@ Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type ) /**Function************************************************************* - Synopsis [] + Synopsis [Sets the simulation info to zero.] Description [] @@ -161,7 +140,7 @@ void Aig_SimInfoClean( Aig_SimInfo_t * p ) /**Function************************************************************* - Synopsis [] + Synopsis [Sets the random simulation info.] Description [] @@ -187,7 +166,40 @@ void Aig_SimInfoRandom( Aig_SimInfo_t * p ) /**Function************************************************************* - Synopsis [] + Synopsis [Sets the random simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat ) +{ + unsigned * pData; + int i, k; + assert( p->Type == 0 ); + assert( p->nNodes == pPat->nBits ); + for ( i = 0; i < p->nNodes; i++ ) + { + // get the pointer to the bitdata for node i + pData = p->pData + p->nWords * i; + // fill in the bit data according to the pattern + if ( Aig_InfoHasBit(pPat->pData, i) ) // PI has bit set to 1 + for ( k = 0; k < p->nWords; k++ ) + pData[k] = ~((unsigned)0); + else + for ( k = 0; k < p->nWords; k++ ) + pData[k] = 0; + // flip one bit + Aig_InfoXorBit( pData, i ); + } +} + +/**Function************************************************************* + + Synopsis [Resizes the simulation info.] Description [] @@ -209,13 +221,15 @@ void Aig_SimInfoResize( Aig_SimInfo_t * p ) for ( k = 0; k < p->nWords; k++ ) pData[2 * p->nWords * i + k + p->nWords] = 0; } - p->nPatsMax *= 2; p->nWords *= 2; + p->nPatsMax *= 2; + free( p->pData ); + p->pData = pData; } /**Function************************************************************* - Synopsis [] + Synopsis [Deallocates the simulation info.] Description [] @@ -231,6 +245,80 @@ void Aig_SimInfoFree( Aig_SimInfo_t * p ) } +/**Function************************************************************* + + Synopsis [Allocates the simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Pattern_t * Aig_PatternAlloc( int nBits ) +{ + Aig_Pattern_t * pPat; + pPat = ALLOC( Aig_Pattern_t, 1 ); + memset( pPat, 0, sizeof(Aig_Pattern_t) ); + pPat->nBits = nBits; + pPat->nWords = Aig_BitWordNum(nBits); + pPat->pData = ALLOC( unsigned, pPat->nWords ); + return pPat; +} + +/**Function************************************************************* + + Synopsis [Cleans the pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_PatternClean( Aig_Pattern_t * pPat ) +{ + memset( pPat->pData, 0, sizeof(unsigned) * pPat->nWords ); +} + +/**Function************************************************************* + + Synopsis [Sets the random pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_PatternRandom( Aig_Pattern_t * pPat ) +{ + int i; + for ( i = 0; i < pPat->nWords; i++ ) + pPat->pData[i] = ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())); +} + +/**Function************************************************************* + + Synopsis [Deallocates the pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_PatternFree( Aig_Pattern_t * pPat ) +{ + free( pPat->pData ); + free( pPat ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/aig/fraigSolver.c b/src/sat/aig/fraigSolver.c new file mode 100644 index 00000000..12502951 --- /dev/null +++ b/src/sat/aig/fraigSolver.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [fraigSolver.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: fraigSolver.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/fraigTrav.c b/src/sat/aig/fraigTrav.c new file mode 100644 index 00000000..d5a09259 --- /dev/null +++ b/src/sat/aig/fraigTrav.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [fraigTrav.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: fraigTrav.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/csat/csat_apis.c b/src/sat/csat/csat_apis.c index eb1c5374..3fadd457 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -26,7 +26,7 @@ #define ABC_DEFAULT_TIMEOUT 60 // 60 seconds -struct CSAT_ManagerStruct_t +struct ABC_ManagerStruct_t { // information about the problem stmm_table * tName2Node; // the hash table mapping names to nodes @@ -43,11 +43,11 @@ struct CSAT_ManagerStruct_t Vec_Ptr_t * vNodes; // the gates in the target Vec_Int_t * vValues; // the values of gate's outputs in the target // solution - CSAT_Target_ResultT * pResult; // the result of solving the target + ABC_Target_ResultT * pResult; // the result of solving the target }; -static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars ); -static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode ); +static ABC_Target_ResultT * ABC_TargetResAlloc( int nVars ); +static char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode ); // some external procedures extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); @@ -67,11 +67,11 @@ extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); SeeAlso [] ***********************************************************************/ -CSAT_Manager CSAT_InitManager() +ABC_Manager ABC_InitManager() { - CSAT_Manager_t * mng; - mng = ALLOC( CSAT_Manager_t, 1 ); - memset( mng, 0, sizeof(CSAT_Manager_t) ); + ABC_Manager_t * mng; + mng = ALLOC( ABC_Manager_t, 1 ); + memset( mng, 0, sizeof(ABC_Manager_t) ); mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP ); mng->pNtk->pName = util_strsav("csat_network"); mng->tName2Node = stmm_init_table(strcmp, stmm_strhash); @@ -93,7 +93,7 @@ CSAT_Manager CSAT_InitManager() SeeAlso [] ***********************************************************************/ -void CSAT_QuitManager( CSAT_Manager mng ) +void ABC_QuitManager( ABC_Manager mng ) { if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name ); if ( mng->tName2Node ) stmm_free_table( mng->tName2Node ); @@ -116,15 +116,15 @@ void CSAT_QuitManager( CSAT_Manager mng ) SeeAlso [] ***********************************************************************/ -void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option ) +void ABC_SetSolveOption( ABC_Manager mng, enum ABC_OptionT option ) { mng->mode = option; if ( option == 0 ) - printf( "CSAT_SetSolveOption: Setting brute-force SAT mode.\n" ); + printf( "ABC_SetSolveOption: Setting brute-force SAT mode.\n" ); else if ( option == 1 ) - printf( "CSAT_SetSolveOption: Setting resource-aware FRAIG mode.\n" ); + printf( "ABC_SetSolveOption: Setting resource-aware FRAIG mode.\n" ); else - printf( "CSAT_SetSolveOption: Unknown solving mode.\n" ); + printf( "ABC_SetSolveOption: Unknown solving mode.\n" ); } @@ -143,7 +143,7 @@ void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option ) SeeAlso [] ***********************************************************************/ -int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr ) +int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr ) { Abc_Obj_t * pObj, * pFanin; char * pSop; @@ -151,82 +151,82 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c switch( type ) { - case CSAT_BPI: - case CSAT_BPPI: + case ABC_BPI: + case ABC_BPPI: if ( nofi != 0 ) - { printf( "CSAT_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; } // create the PI pObj = Abc_NtkCreatePi( mng->pNtk ); stmm_insert( mng->tNode2Name, (char *)pObj, name ); break; - case CSAT_CONST: - case CSAT_BAND: - case CSAT_BNAND: - case CSAT_BOR: - case CSAT_BNOR: - case CSAT_BXOR: - case CSAT_BXNOR: - case CSAT_BINV: - case CSAT_BBUF: + case ABC_CONST: + case ABC_BAND: + case ABC_BNAND: + case ABC_BOR: + case ABC_BNOR: + case ABC_BXOR: + case ABC_BXNOR: + case ABC_BINV: + case ABC_BBUF: // create the node pObj = Abc_NtkCreateNode( mng->pNtk ); // create the fanins for ( i = 0; i < nofi; i++ ) { if ( !stmm_lookup( mng->tName2Node, fanins[i], (char **)&pFanin ) ) - { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; } + { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; } Abc_ObjAddFanin( pObj, pFanin ); } // create the node function switch( type ) { - case CSAT_CONST: + case ABC_CONST: if ( nofi != 0 ) - { printf( "CSAT_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; } pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc ); break; - case CSAT_BAND: + case ABC_BAND: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL ); break; - case CSAT_BNAND: + case ABC_BNAND: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi ); break; - case CSAT_BOR: + case ABC_BOR: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL ); break; - case CSAT_BNOR: + case ABC_BNOR: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi ); break; - case CSAT_BXOR: + case ABC_BXOR: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; } if ( nofi > 2 ) - { printf( "CSAT_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; } pSop = Abc_SopCreateXor( mng->pNtk->pManFunc, nofi ); break; - case CSAT_BXNOR: + case ABC_BXNOR: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; } if ( nofi > 2 ) - { printf( "CSAT_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; } pSop = Abc_SopCreateNxor( mng->pNtk->pManFunc, nofi ); break; - case CSAT_BINV: + case ABC_BINV: if ( nofi != 1 ) - { printf( "CSAT_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } + { printf( "ABC_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } pSop = Abc_SopCreateInv( mng->pNtk->pManFunc ); break; - case CSAT_BBUF: + case ABC_BBUF: if ( nofi != 1 ) - { printf( "CSAT_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } + { printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc ); break; default : @@ -234,24 +234,24 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c } Abc_ObjSetData( pObj, pSop ); break; - case CSAT_BPPO: - case CSAT_BPO: + case ABC_BPPO: + case ABC_BPO: if ( nofi != 1 ) - { printf( "CSAT_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } + { printf( "ABC_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } // create the PO pObj = Abc_NtkCreatePo( mng->pNtk ); stmm_insert( mng->tNode2Name, (char *)pObj, name ); // connect to the PO fanin if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) ) - { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; } + { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; } Abc_ObjAddFanin( pObj, pFanin ); break; default: - printf( "CSAT_AddGate: Unknown gate type.\n" ); + printf( "ABC_AddGate: Unknown gate type.\n" ); break; } if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) ) - { printf( "CSAT_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; } + { printf( "ABC_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; } return 1; } @@ -267,7 +267,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c SeeAlso [] ***********************************************************************/ -int CSAT_Check_Integrity( CSAT_Manager mng ) +int ABC_Check_Integrity( ABC_Manager mng ) { Abc_Ntk_t * pNtk = mng->pNtk; Abc_Obj_t * pObj; @@ -276,15 +276,15 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) // this procedure also finalizes construction of the ABC network Abc_NtkFixNonDrivenNets( pNtk ); Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) ); + Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) ); Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) ); + Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); // make sure everything is okay with the network structure if ( !Abc_NtkDoCheck( pNtk ) ) { - printf( "CSAT_Check_Integrity: The internal network check has failed.\n" ); + printf( "ABC_Check_Integrity: The internal network check has failed.\n" ); return 0; } @@ -295,7 +295,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) continue; if ( Abc_ObjFanoutNum(pObj) == 0 ) { - printf( "CSAT_Check_Integrity: The network has dangling nodes.\n" ); + printf( "ABC_Check_Integrity: The network has dangling nodes.\n" ); return 0; } } @@ -313,7 +313,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) SeeAlso [] ***********************************************************************/ -void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime ) +void ABC_SetTimeLimit( ABC_Manager mng, int runtime ) { mng->nSeconds = runtime; } @@ -329,9 +329,9 @@ void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime ) SeeAlso [] ***********************************************************************/ -void CSAT_SetLearnLimit( CSAT_Manager mng, int num ) +void ABC_SetLearnLimit( ABC_Manager mng, int num ) { - printf( "CSAT_SetLearnLimit: The resource limit is not implemented (warning).\n" ); + printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" ); } /**Function************************************************************* @@ -345,9 +345,9 @@ void CSAT_SetLearnLimit( CSAT_Manager mng, int num ) SeeAlso [] ***********************************************************************/ -void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num ) +void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num ) { - printf( "CSAT_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" ); + printf( "ABC_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" ); } /**Function************************************************************* @@ -361,9 +361,9 @@ void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num ) SeeAlso [] ***********************************************************************/ -void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num ) +void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num ) { - printf( "CSAT_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" ); + printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" ); } /**Function************************************************************* @@ -377,7 +377,7 @@ void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num ) SeeAlso [] ***********************************************************************/ -void CSAT_EnableDump( CSAT_Manager mng, char * dump_file ) +void ABC_EnableDump( ABC_Manager mng, char * dump_file ) { FREE( mng->pDumpFileName ); mng->pDumpFileName = util_strsav( dump_file ); @@ -398,12 +398,12 @@ void CSAT_EnableDump( CSAT_Manager mng, char * dump_file ) SeeAlso [] ***********************************************************************/ -int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values ) +int ABC_AddTarget( ABC_Manager mng, int nog, char ** names, int * values ) { Abc_Obj_t * pObj; int i; if ( nog < 1 ) - { printf( "CSAT_AddTarget: The target has no gates.\n" ); return 0; } + { printf( "ABC_AddTarget: The target has no gates.\n" ); return 0; } // clear storage for the target mng->nog = 0; Vec_PtrClear( mng->vNodes ); @@ -412,10 +412,10 @@ int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values ) for ( i = 0; i < nog; i++ ) { if ( !stmm_lookup( mng->tName2Node, names[i], (char **)&pObj ) ) - { printf( "CSAT_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; } + { printf( "ABC_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; } Vec_PtrPush( mng->vNodes, pObj ); if ( values[i] < 0 || values[i] > 1 ) - { printf( "CSAT_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; } + { printf( "ABC_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; } Vec_IntPush( mng->vValues, values[i] ); } mng->nog = nog; @@ -427,14 +427,14 @@ int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values ) Synopsis [Initialize the solver internal data structure.] Description [Prepares the solver to work on one specific target - set by calling CSAT_AddTarget before.] + set by calling ABC_AddTarget before.] SideEffects [] SeeAlso [] ***********************************************************************/ -void CSAT_SolveInit( CSAT_Manager mng ) +void ABC_SolveInit( ABC_Manager mng ) { Fraig_Params_t * pParams = &mng->Params; int nWords1, nWords2, nWordsMin; @@ -442,7 +442,7 @@ void CSAT_SolveInit( CSAT_Manager mng ) // check if the target is available assert( mng->nog == Vec_PtrSize(mng->vNodes) ); if ( mng->nog == 0 ) - { printf( "CSAT_SolveInit: Target is not specified by CSAT_AddTarget().\n" ); return; } + { printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; } // free the previous target network if present if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget ); @@ -485,13 +485,13 @@ void CSAT_SolveInit( CSAT_Manager mng ) SeeAlso [] ***********************************************************************/ -void CSAT_AnalyzeTargets( CSAT_Manager mng ) +void ABC_AnalyzeTargets( ABC_Manager mng ) { } /**Function************************************************************* - Synopsis [Solves the targets added by CSAT_AddTarget().] + Synopsis [Solves the targets added by ABC_AddTarget().] Description [] @@ -500,7 +500,7 @@ void CSAT_AnalyzeTargets( CSAT_Manager mng ) SeeAlso [] ***********************************************************************/ -enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) +enum ABC_StatusT ABC_Solve( ABC_Manager mng ) { Fraig_Man_t * pMan; Abc_Ntk_t * pCnf; @@ -509,7 +509,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) // check if the target network is available if ( mng->pTarget == NULL ) - { printf( "CSAT_Solve: Target network is not derived by CSAT_SolveInit().\n" ); return UNDETERMINED; } + { printf( "ABC_Solve: Target network is not derived by ABC_SolveInit().\n" ); return UNDETERMINED; } // optimizations of the target go here // for example, to enable one pass of rewriting, uncomment this line @@ -522,7 +522,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 ); // analyze the result - mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); + mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); if ( RetValue == -1 ) mng->pResult->status = UNDETERMINED; else if ( RetValue == 1 ) @@ -533,7 +533,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) // create the array of PI names and values for ( i = 0; i < mng->pResult->no_sig; i++ ) { - mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given + mng->pResult->names[i] = ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given mng->pResult->values[i] = pCnf->pModel[i]; } FREE( mng->pTarget->pModel ); @@ -549,7 +549,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) RetValue = Fraig_ManCheckMiter( pMan ); // analyze the result - mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); + mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); if ( RetValue == -1 ) mng->pResult->status = UNDETERMINED; else if ( RetValue == 1 ) @@ -562,7 +562,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) // create the array of PI names and values for ( i = 0; i < mng->pResult->no_sig; i++ ) { - mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given + mng->pResult->names[i] = ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given mng->pResult->values[i] = pModel[i]; } } @@ -584,14 +584,14 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) Synopsis [Gets the solve status of a target.] - Description [TargetID: the target id returned by CSAT_AddTarget().] + Description [TargetID: the target id returned by ABC_AddTarget().] SideEffects [] SeeAlso [] ***********************************************************************/ -CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID ) +ABC_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID ) { return mng->pResult; } @@ -607,7 +607,7 @@ CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID ) SeeAlso [] ***********************************************************************/ -void CSAT_Dump_Bench_File( CSAT_Manager mng ) +void ABC_Dump_Bench_File( ABC_Manager mng ) { Abc_Ntk_t * pNtkTemp, * pNtkAig; char * pFileName; @@ -617,7 +617,7 @@ void CSAT_Dump_Bench_File( CSAT_Manager mng ) pNtkTemp = Abc_NtkLogicToNetlistBench( pNtkAig ); Abc_NtkDelete( pNtkAig ); if ( pNtkTemp == NULL ) - { printf( "CSAT_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; } + { printf( "ABC_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; } pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench"; Io_WriteBench( pNtkTemp, pFileName ); Abc_NtkDelete( pNtkTemp ); @@ -636,11 +636,11 @@ void CSAT_Dump_Bench_File( CSAT_Manager mng ) SeeAlso [] ***********************************************************************/ -CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars ) +ABC_Target_ResultT * ABC_TargetResAlloc( int nVars ) { - CSAT_Target_ResultT * p; - p = ALLOC( CSAT_Target_ResultT, 1 ); - memset( p, 0, sizeof(CSAT_Target_ResultT) ); + ABC_Target_ResultT * p; + p = ALLOC( ABC_Target_ResultT, 1 ); + memset( p, 0, sizeof(ABC_Target_ResultT) ); p->no_sig = nVars; p->names = ALLOC( char *, nVars ); p->values = ALLOC( int, nVars ); @@ -660,7 +660,7 @@ CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars ) SeeAlso [] ***********************************************************************/ -void CSAT_TargetResFree( CSAT_Target_ResultT * p ) +void ABC_TargetResFree( ABC_Target_ResultT * p ) { if ( p == NULL ) return; @@ -680,7 +680,7 @@ void CSAT_TargetResFree( CSAT_Target_ResultT * p ) SeeAlso [] ***********************************************************************/ -char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode ) +char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode ) { char * pName = NULL; if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) ) diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index e567241f..3e04c7df 100644 --- a/src/sat/csat/csat_apis.h +++ b/src/sat/csat/csat_apis.h @@ -16,8 +16,8 @@ ***********************************************************************/ -#ifndef __CSAT_APIS_H__ -#define __CSAT_APIS_H__ +#ifndef __ABC_APIS_H__ +#define __ABC_APIS_H__ //////////////////////////////////////////////////////////////////////// /// INCLUDES /// @@ -32,37 +32,37 @@ //////////////////////////////////////////////////////////////////////// -typedef struct CSAT_ManagerStruct_t CSAT_Manager_t; -typedef struct CSAT_ManagerStruct_t * CSAT_Manager; +typedef struct ABC_ManagerStruct_t ABC_Manager_t; +typedef struct ABC_ManagerStruct_t * ABC_Manager; // GateType defines the gate type that can be added to circuit by -// CSAT_AddGate(); -#ifndef _CSAT_GATE_TYPE_ -#define _CSAT_GATE_TYPE_ +// ABC_AddGate(); +#ifndef _ABC_GATE_TYPE_ +#define _ABC_GATE_TYPE_ enum GateType { - CSAT_CONST = 0, // constant gate - CSAT_BPI, // boolean PI - CSAT_BPPI, // bit level PSEUDO PRIMARY INPUT - CSAT_BAND, // bit level AND - CSAT_BNAND, // bit level NAND - CSAT_BOR, // bit level OR - CSAT_BNOR, // bit level NOR - CSAT_BXOR, // bit level XOR - CSAT_BXNOR, // bit level XNOR - CSAT_BINV, // bit level INVERTER - CSAT_BBUF, // bit level BUFFER - CSAT_BPPO, // bit level PSEUDO PRIMARY OUTPUT - CSAT_BPO // boolean PO + ABC_CONST = 0, // constant gate + ABC_BPI, // boolean PI + ABC_BPPI, // bit level PSEUDO PRIMARY INPUT + ABC_BAND, // bit level AND + ABC_BNAND, // bit level NAND + ABC_BOR, // bit level OR + ABC_BNOR, // bit level NOR + ABC_BXOR, // bit level XOR + ABC_BXNOR, // bit level XNOR + ABC_BINV, // bit level INVERTER + ABC_BBUF, // bit level BUFFER + ABC_BPPO, // bit level PSEUDO PRIMARY OUTPUT + ABC_BPO // boolean PO }; #endif -//CSAT_StatusT defines the return value by CSAT_Solve(); -#ifndef _CSAT_STATUS_ -#define _CSAT_STATUS_ -enum CSAT_StatusT +//ABC_StatusT defines the return value by ABC_Solve(); +#ifndef _ABC_STATUS_ +#define _ABC_STATUS_ +enum ABC_StatusT { UNDETERMINED = 0, UNSATISFIABLE, @@ -76,11 +76,11 @@ enum CSAT_StatusT #endif -// CSAT_OptionT defines the solver option about learning -// which is used by CSAT_SetSolveOption(); -#ifndef _CSAT_OPTION_ -#define _CSAT_OPTION_ -enum CSAT_OptionT +// ABC_OptionT defines the solver option about learning +// which is used by ABC_SetSolveOption(); +#ifndef _ABC_OPTION_ +#define _ABC_OPTION_ +enum ABC_OptionT { BASE_LINE = 0, IMPLICT_LEARNING, //default @@ -89,12 +89,12 @@ enum CSAT_OptionT #endif -#ifndef _CSAT_Target_Result -#define _CSAT_Target_Result -typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT; -struct _CSAT_Target_ResultT +#ifndef _ABC_Target_Result +#define _ABC_Target_Result +typedef struct _ABC_Target_ResultT ABC_Target_ResultT; +struct _ABC_Target_ResultT { - enum CSAT_StatusT status; // solve status of the target + enum ABC_StatusT status; // solve status of the target int num_dec; // num of decisions to solve the target int num_imp; // num of implications to solve the target int num_cftg; // num of conflict gates learned @@ -118,10 +118,10 @@ struct _CSAT_Target_ResultT //////////////////////////////////////////////////////////////////////// // create a new manager -extern CSAT_Manager CSAT_InitManager(void); +extern ABC_Manager ABC_InitManager(void); // set solver options for learning -extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option); +extern void ABC_SetSolveOption(ABC_Manager mng, enum ABC_OptionT option); // add a gate to the circuit // the meaning of the parameters are: @@ -129,7 +129,7 @@ extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_Opt // name: the name of the gate to be added, name should be unique in a circuit. // nofi: number of fanins of the gate to be added; // fanins: the name array of fanins of the gate to be added -extern int CSAT_AddGate(CSAT_Manager mng, +extern int ABC_AddGate(ABC_Manager mng, enum GateType type, char* name, int nofi, @@ -138,38 +138,38 @@ extern int CSAT_AddGate(CSAT_Manager mng, // check if there are gates that are not used by any primary ouput. // if no such gates exist, return 1 else return 0; -extern int CSAT_Check_Integrity(CSAT_Manager mng); +extern int ABC_Check_Integrity(ABC_Manager mng); // set time limit for solving a target. // runtime: time limit (in second). -extern void CSAT_SetTimeLimit(CSAT_Manager mng, int runtime); -extern void CSAT_SetLearnLimit(CSAT_Manager mng, int num); -extern void CSAT_SetSolveBacktrackLimit(CSAT_Manager mng, int num); -extern void CSAT_SetLearnBacktrackLimit(CSAT_Manager mng, int num); -extern void CSAT_EnableDump(CSAT_Manager mng, char* dump_file); +extern void ABC_SetTimeLimit(ABC_Manager mng, int runtime); +extern void ABC_SetLearnLimit(ABC_Manager mng, int num); +extern void ABC_SetSolveBacktrackLimit(ABC_Manager mng, int num); +extern void ABC_SetLearnBacktrackLimit(ABC_Manager mng, int num); +extern void ABC_EnableDump(ABC_Manager mng, char* dump_file); // the meaning of the parameters are: // nog: number of gates that are in the targets // names: name array of gates // values: value array of the corresponding gates given in "names" to be // solved. the relation of them is AND. -extern int CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values); +extern int ABC_AddTarget(ABC_Manager mng, int nog, char**names, int* values); // initialize the solver internal data structure. -extern void CSAT_SolveInit(CSAT_Manager mng); -extern void CSAT_AnalyzeTargets(CSAT_Manager mng); +extern void ABC_SolveInit(ABC_Manager mng); +extern void ABC_AnalyzeTargets(ABC_Manager mng); -// solve the targets added by CSAT_AddTarget() -extern enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng); +// solve the targets added by ABC_AddTarget() +extern enum ABC_StatusT ABC_Solve(ABC_Manager mng); // get the solve status of a target -// TargetID: the target id returned by CSAT_AddTarget(). -extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID); -extern void CSAT_Dump_Bench_File(CSAT_Manager mng); +// TargetID: the target id returned by ABC_AddTarget(). +extern ABC_Target_ResultT * ABC_Get_Target_Result(ABC_Manager mng, int TargetID); +extern void ABC_Dump_Bench_File(ABC_Manager mng); // ADDED PROCEDURES: -extern void CSAT_QuitManager( CSAT_Manager mng ); -extern void CSAT_TargetResFree( CSAT_Target_ResultT * p ); +extern void ABC_QuitManager( ABC_Manager mng ); +extern void ABC_TargetResFree( ABC_Target_ResultT * p ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/fraig/fraigMem.c b/src/sat/fraig/fraigMem.c index 7dc46430..500431c6 100644 --- a/src/sat/fraig/fraigMem.c +++ b/src/sat/fraig/fraigMem.c @@ -201,7 +201,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p ) int i; char * pTemp; - // delocate all chunks except the first one + // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) free( p->pChunks[i] ); p->nChunks = 1; diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c index 40aa223b..30bf4a96 100644 --- a/src/sat/msat/msatMem.c +++ b/src/sat/msat/msatMem.c @@ -231,7 +231,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p ) int i; char * pTemp; - // delocate all chunks except the first one + // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) free( p->pChunks[i] ); p->nChunks = 1; |