diff options
| -rw-r--r-- | abc.opt | bin | 52736 -> 52736 bytes | |||
| -rw-r--r-- | abc.plg | 671 | ||||
| -rw-r--r-- | abc.rc | 1 | ||||
| -rw-r--r-- | mcnc_temp.genlib_temp | 67 | ||||
| -rw-r--r-- | mcnc_temp.super | 42 | ||||
| -rw-r--r-- | src/base/abc/abcAig.c | 45 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 49 | ||||
| -rw-r--r-- | src/base/abci/abcSat.c | 497 | ||||
| -rw-r--r-- | src/base/abci/abcVerify.c | 6 | ||||
| -rw-r--r-- | src/opt/xyz/xyz.h | 2 | ||||
| -rw-r--r-- | src/opt/xyz/xyzCore.c | 348 | ||||
| -rw-r--r-- | src/opt/xyz/xyzInt.h | 77 | ||||
| -rw-r--r-- | src/opt/xyz/xyzMinEsop.c | 38 | ||||
| -rw-r--r-- | src/opt/xyz/xyzMinMan.c | 1 | ||||
| -rw-r--r-- | src/opt/xyz/xyzMinSop.c | 346 | ||||
| -rw-r--r-- | src/opt/xyz/xyzMinUtil.c | 56 | ||||
| -rw-r--r-- | src/opt/xyz/xyzTest.c | 370 | ||||
| -rw-r--r-- | src/sat/asat/solver.h | 5 | ||||
| -rw-r--r-- | src/sat/fraig/fraigCanon.c | 4 | ||||
| -rw-r--r-- | src/sat/fraig/fraigSat.c | 22 | ||||
| -rw-r--r-- | src/sat/msat/msat.h | 1 | ||||
| -rw-r--r-- | src/sat/msat/msatClause.c | 5 | ||||
| -rw-r--r-- | src/sat/msat/msatInt.h | 1 | ||||
| -rw-r--r-- | src/sat/msat/msatSolverApi.c | 1 | ||||
| -rw-r--r-- | src/sat/msat/msatSolverCore.c | 20 |
25 files changed, 2564 insertions, 111 deletions
| Binary files differ @@ -3,9 +3,678 @@ <pre> <h1>Build Log</h1> <h3> ---------------------Configuration: abc - Win32 Release-------------------- +--------------------Configuration: abc - Win32 Debug-------------------- </h3> <h3>Command Lines</h3> +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14F9.tmp" with contents +[ +/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c +"C:\_projects\abc\src\opt\xyz\xyzCore.c" +] +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14F9.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FA.tmp" with contents +[ +kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept +.\Debug\abcAig.obj +.\Debug\abcCheck.obj +.\Debug\abcDfs.obj +.\Debug\abcFanio.obj +.\Debug\abcFunc.obj +.\Debug\abcLatch.obj +.\Debug\abcMinBase.obj +.\Debug\abcNames.obj +.\Debug\abcNetlist.obj +.\Debug\abcNtk.obj +.\Debug\abcObj.obj +.\Debug\abcRefs.obj +.\Debug\abcShow.obj +.\Debug\abcSop.obj +.\Debug\abcUtil.obj +.\Debug\abc.obj +.\Debug\abcAttach.obj +.\Debug\abcBalance.obj +.\Debug\abcCollapse.obj +.\Debug\abcCut.obj +.\Debug\abcDsd.obj +.\Debug\abcFpga.obj +.\Debug\abcFraig.obj +.\Debug\abcFxu.obj +.\Debug\abcMap.obj +.\Debug\abcMiter.obj +.\Debug\abcNtbdd.obj +.\Debug\abcPga.obj +.\Debug\abcPrint.obj +.\Debug\abcReconv.obj +.\Debug\abcRefactor.obj +.\Debug\abcRenode.obj +.\Debug\abcRewrite.obj +.\Debug\abcSat.obj +.\Debug\abcStrash.obj +.\Debug\abcSweep.obj +.\Debug\abcSymm.obj +.\Debug\abcTiming.obj +.\Debug\abcUnreach.obj +.\Debug\abcVanEijk.obj +.\Debug\abcVanImp.obj +.\Debug\abcVerify.obj +.\Debug\seqAigCore.obj +.\Debug\seqAigIter.obj +.\Debug\seqCreate.obj +.\Debug\seqFpgaCore.obj +.\Debug\seqFpgaIter.obj +.\Debug\seqLatch.obj +.\Debug\seqMan.obj +.\Debug\seqMapCore.obj +.\Debug\seqMapIter.obj +.\Debug\seqRetCore.obj +.\Debug\seqRetIter.obj +.\Debug\seqShare.obj +.\Debug\seqUtil.obj +.\Debug\cmd.obj +.\Debug\cmdAlias.obj +.\Debug\cmdApi.obj +.\Debug\cmdFlag.obj +.\Debug\cmdHist.obj +.\Debug\cmdUtils.obj +.\Debug\io.obj +.\Debug\ioRead.obj +.\Debug\ioReadBaf.obj +.\Debug\ioReadBench.obj +.\Debug\ioReadBlif.obj +.\Debug\ioReadEdif.obj +.\Debug\ioReadEqn.obj +.\Debug\ioReadPla.obj +.\Debug\ioReadVerilog.obj +.\Debug\ioUtil.obj +.\Debug\ioWriteBaf.obj +.\Debug\ioWriteBench.obj +.\Debug\ioWriteBlif.obj +.\Debug\ioWriteCnf.obj +.\Debug\ioWriteDot.obj +.\Debug\ioWriteEqn.obj +.\Debug\ioWriteGml.obj +.\Debug\ioWriteList.obj +.\Debug\ioWritePla.obj +.\Debug\ioWriteVerilog.obj +.\Debug\libSupport.obj +.\Debug\main.obj +.\Debug\mainFrame.obj +.\Debug\mainInit.obj +.\Debug\mainUtils.obj +.\Debug\cuddAddAbs.obj +.\Debug\cuddAddApply.obj +.\Debug\cuddAddFind.obj +.\Debug\cuddAddInv.obj +.\Debug\cuddAddIte.obj +.\Debug\cuddAddNeg.obj +.\Debug\cuddAddWalsh.obj +.\Debug\cuddAndAbs.obj +.\Debug\cuddAnneal.obj +.\Debug\cuddApa.obj +.\Debug\cuddAPI.obj +.\Debug\cuddApprox.obj +.\Debug\cuddBddAbs.obj +.\Debug\cuddBddCorr.obj +.\Debug\cuddBddIte.obj +.\Debug\cuddBridge.obj +.\Debug\cuddCache.obj +.\Debug\cuddCheck.obj +.\Debug\cuddClip.obj +.\Debug\cuddCof.obj +.\Debug\cuddCompose.obj +.\Debug\cuddDecomp.obj +.\Debug\cuddEssent.obj +.\Debug\cuddExact.obj +.\Debug\cuddExport.obj +.\Debug\cuddGenCof.obj +.\Debug\cuddGenetic.obj +.\Debug\cuddGroup.obj +.\Debug\cuddHarwell.obj +.\Debug\cuddInit.obj +.\Debug\cuddInteract.obj +.\Debug\cuddLCache.obj +.\Debug\cuddLevelQ.obj +.\Debug\cuddLinear.obj +.\Debug\cuddLiteral.obj +.\Debug\cuddMatMult.obj +.\Debug\cuddPriority.obj +.\Debug\cuddRead.obj +.\Debug\cuddRef.obj +.\Debug\cuddReorder.obj +.\Debug\cuddSat.obj +.\Debug\cuddSign.obj +.\Debug\cuddSolve.obj +.\Debug\cuddSplit.obj +.\Debug\cuddSubsetHB.obj +.\Debug\cuddSubsetSP.obj +.\Debug\cuddSymmetry.obj +.\Debug\cuddTable.obj +.\Debug\cuddUtil.obj +.\Debug\cuddWindow.obj +.\Debug\cuddZddCount.obj +.\Debug\cuddZddFuncs.obj +.\Debug\cuddZddGroup.obj +.\Debug\cuddZddIsop.obj +.\Debug\cuddZddLin.obj +.\Debug\cuddZddMisc.obj +.\Debug\cuddZddPort.obj +.\Debug\cuddZddReord.obj +.\Debug\cuddZddSetop.obj +.\Debug\cuddZddSymm.obj +.\Debug\cuddZddUtil.obj +.\Debug\epd.obj +.\Debug\mtrBasic.obj +.\Debug\mtrGroup.obj +.\Debug\parseCore.obj +.\Debug\parseStack.obj +.\Debug\dsdApi.obj +.\Debug\dsdCheck.obj +.\Debug\dsdLocal.obj +.\Debug\dsdMan.obj +.\Debug\dsdProc.obj +.\Debug\dsdTree.obj +.\Debug\reoApi.obj +.\Debug\reoCore.obj +.\Debug\reoProfile.obj +.\Debug\reoSift.obj +.\Debug\reoSwap.obj +.\Debug\reoTest.obj +.\Debug\reoTransfer.obj +.\Debug\reoUnits.obj +.\Debug\added.obj +.\Debug\solver.obj +.\Debug\msatActivity.obj +.\Debug\msatClause.obj +.\Debug\msatClauseVec.obj +.\Debug\msatMem.obj +.\Debug\msatQueue.obj +.\Debug\msatRead.obj +.\Debug\msatSolverApi.obj +.\Debug\msatSolverCore.obj +.\Debug\msatSolverIo.obj +.\Debug\msatSolverSearch.obj +.\Debug\msatSort.obj +.\Debug\msatVec.obj +.\Debug\fraigApi.obj +.\Debug\fraigCanon.obj +.\Debug\fraigFanout.obj +.\Debug\fraigFeed.obj +.\Debug\fraigMan.obj +.\Debug\fraigMem.obj +.\Debug\fraigNode.obj +.\Debug\fraigPrime.obj +.\Debug\fraigSat.obj +.\Debug\fraigTable.obj +.\Debug\fraigUtil.obj +.\Debug\fraigVec.obj +.\Debug\csat_apis.obj +.\Debug\fxu.obj +.\Debug\fxuCreate.obj +.\Debug\fxuHeapD.obj +.\Debug\fxuHeapS.obj +.\Debug\fxuList.obj +.\Debug\fxuMatrix.obj +.\Debug\fxuPair.obj +.\Debug\fxuPrint.obj +.\Debug\fxuReduce.obj +.\Debug\fxuSelect.obj +.\Debug\fxuSingle.obj +.\Debug\fxuUpdate.obj +.\Debug\rwrDec.obj +.\Debug\rwrEva.obj +.\Debug\rwrExp.obj +.\Debug\rwrLib.obj +.\Debug\rwrMan.obj +.\Debug\rwrPrint.obj +.\Debug\rwrUtil.obj +.\Debug\cutApi.obj +.\Debug\cutCut.obj +.\Debug\cutMan.obj +.\Debug\cutMerge.obj +.\Debug\cutNode.obj +.\Debug\cutOracle.obj +.\Debug\cutSeq.obj +.\Debug\cutTruth.obj +.\Debug\decAbc.obj +.\Debug\decFactor.obj +.\Debug\decMan.obj +.\Debug\decPrint.obj +.\Debug\decUtil.obj +.\Debug\simMan.obj +.\Debug\simSat.obj +.\Debug\simSeq.obj +.\Debug\simSupp.obj +.\Debug\simSwitch.obj +.\Debug\simSym.obj +.\Debug\simSymSat.obj +.\Debug\simSymSim.obj +.\Debug\simSymStr.obj +.\Debug\simUtils.obj +.\Debug\xyzBuild.obj +.\Debug\xyzCore.obj +.\Debug\xyzMan.obj +.\Debug\xyzMinEsop.obj +.\Debug\xyzMinMan.obj +.\Debug\xyzMinSop.obj +.\Debug\xyzMinUtil.obj +.\Debug\xyzTest.obj +.\Debug\fpga.obj +.\Debug\fpgaCore.obj +.\Debug\fpgaCreate.obj +.\Debug\fpgaCut.obj +.\Debug\fpgaCutUtils.obj +.\Debug\fpgaFanout.obj +.\Debug\fpgaLib.obj +.\Debug\fpgaMatch.obj +.\Debug\fpgaSwitch.obj +.\Debug\fpgaTime.obj +.\Debug\fpgaTruth.obj +.\Debug\fpgaUtils.obj +.\Debug\fpgaVec.obj +.\Debug\mapper.obj +.\Debug\mapperCanon.obj +.\Debug\mapperCore.obj +.\Debug\mapperCreate.obj +.\Debug\mapperCut.obj +.\Debug\mapperCutUtils.obj +.\Debug\mapperFanout.obj +.\Debug\mapperLib.obj +.\Debug\mapperMatch.obj +.\Debug\mapperRefs.obj +.\Debug\mapperSuper.obj +.\Debug\mapperSwitch.obj +.\Debug\mapperTable.obj +.\Debug\mapperTime.obj +.\Debug\mapperTree.obj +.\Debug\mapperTruth.obj +.\Debug\mapperUtils.obj +.\Debug\mapperVec.obj +.\Debug\mio.obj +.\Debug\mioApi.obj +.\Debug\mioFunc.obj +.\Debug\mioRead.obj +.\Debug\mioUtils.obj +.\Debug\super.obj +.\Debug\superAnd.obj +.\Debug\superGate.obj +.\Debug\superWrite.obj +.\Debug\pgaCore.obj +.\Debug\pgaMan.obj +.\Debug\pgaMatch.obj +.\Debug\pgaUtil.obj +.\Debug\extraBddKmap.obj +.\Debug\extraBddMisc.obj +.\Debug\extraBddSymm.obj +.\Debug\extraUtilBitMatrix.obj +.\Debug\extraUtilCanon.obj +.\Debug\extraUtilFile.obj +.\Debug\extraUtilMemory.obj +.\Debug\extraUtilMisc.obj +.\Debug\extraUtilProgress.obj +.\Debug\extraUtilReader.obj +.\Debug\st.obj +.\Debug\stmm.obj +.\Debug\cpu_stats.obj +.\Debug\cpu_time.obj +.\Debug\datalimit.obj +.\Debug\getopt.obj +.\Debug\pathsearch.obj +.\Debug\safe_mem.obj +.\Debug\strsav.obj +.\Debug\texpand.obj +.\Debug\mvc.obj +.\Debug\mvcApi.obj +.\Debug\mvcCompare.obj +.\Debug\mvcContain.obj +.\Debug\mvcCover.obj +.\Debug\mvcCube.obj +.\Debug\mvcDivide.obj +.\Debug\mvcDivisor.obj +.\Debug\mvcList.obj +.\Debug\mvcLits.obj +.\Debug\mvcMan.obj +.\Debug\mvcOpAlg.obj +.\Debug\mvcOpBool.obj +.\Debug\mvcPrint.obj +.\Debug\mvcSort.obj +.\Debug\mvcUtils.obj +.\Debug\msatOrderJ.obj +] +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FA.tmp" +<h3>Output Window</h3> +Compiling... +xyzCore.c +Linking... +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with contents +[ +/nologo /o"Debug/abc.bsc" +.\Debug\abcAig.sbr +.\Debug\abcCheck.sbr +.\Debug\abcDfs.sbr +.\Debug\abcFanio.sbr +.\Debug\abcFunc.sbr +.\Debug\abcLatch.sbr +.\Debug\abcMinBase.sbr +.\Debug\abcNames.sbr +.\Debug\abcNetlist.sbr +.\Debug\abcNtk.sbr +.\Debug\abcObj.sbr +.\Debug\abcRefs.sbr +.\Debug\abcShow.sbr +.\Debug\abcSop.sbr +.\Debug\abcUtil.sbr +.\Debug\abc.sbr +.\Debug\abcAttach.sbr +.\Debug\abcBalance.sbr +.\Debug\abcCollapse.sbr +.\Debug\abcCut.sbr +.\Debug\abcDsd.sbr +.\Debug\abcFpga.sbr +.\Debug\abcFraig.sbr +.\Debug\abcFxu.sbr +.\Debug\abcMap.sbr +.\Debug\abcMiter.sbr +.\Debug\abcNtbdd.sbr +.\Debug\abcPga.sbr +.\Debug\abcPrint.sbr +.\Debug\abcReconv.sbr +.\Debug\abcRefactor.sbr +.\Debug\abcRenode.sbr +.\Debug\abcRewrite.sbr +.\Debug\abcSat.sbr +.\Debug\abcStrash.sbr +.\Debug\abcSweep.sbr +.\Debug\abcSymm.sbr +.\Debug\abcTiming.sbr +.\Debug\abcUnreach.sbr +.\Debug\abcVanEijk.sbr +.\Debug\abcVanImp.sbr +.\Debug\abcVerify.sbr +.\Debug\seqAigCore.sbr +.\Debug\seqAigIter.sbr +.\Debug\seqCreate.sbr +.\Debug\seqFpgaCore.sbr +.\Debug\seqFpgaIter.sbr +.\Debug\seqLatch.sbr +.\Debug\seqMan.sbr +.\Debug\seqMapCore.sbr +.\Debug\seqMapIter.sbr +.\Debug\seqRetCore.sbr +.\Debug\seqRetIter.sbr +.\Debug\seqShare.sbr +.\Debug\seqUtil.sbr +.\Debug\cmd.sbr +.\Debug\cmdAlias.sbr +.\Debug\cmdApi.sbr +.\Debug\cmdFlag.sbr +.\Debug\cmdHist.sbr +.\Debug\cmdUtils.sbr +.\Debug\io.sbr +.\Debug\ioRead.sbr +.\Debug\ioReadBaf.sbr +.\Debug\ioReadBench.sbr +.\Debug\ioReadBlif.sbr +.\Debug\ioReadEdif.sbr +.\Debug\ioReadEqn.sbr +.\Debug\ioReadPla.sbr +.\Debug\ioReadVerilog.sbr +.\Debug\ioUtil.sbr +.\Debug\ioWriteBaf.sbr +.\Debug\ioWriteBench.sbr +.\Debug\ioWriteBlif.sbr +.\Debug\ioWriteCnf.sbr +.\Debug\ioWriteDot.sbr +.\Debug\ioWriteEqn.sbr +.\Debug\ioWriteGml.sbr +.\Debug\ioWriteList.sbr +.\Debug\ioWritePla.sbr +.\Debug\ioWriteVerilog.sbr +.\Debug\libSupport.sbr +.\Debug\main.sbr +.\Debug\mainFrame.sbr +.\Debug\mainInit.sbr +.\Debug\mainUtils.sbr +.\Debug\cuddAddAbs.sbr +.\Debug\cuddAddApply.sbr +.\Debug\cuddAddFind.sbr +.\Debug\cuddAddInv.sbr +.\Debug\cuddAddIte.sbr +.\Debug\cuddAddNeg.sbr +.\Debug\cuddAddWalsh.sbr +.\Debug\cuddAndAbs.sbr +.\Debug\cuddAnneal.sbr +.\Debug\cuddApa.sbr +.\Debug\cuddAPI.sbr +.\Debug\cuddApprox.sbr +.\Debug\cuddBddAbs.sbr +.\Debug\cuddBddCorr.sbr +.\Debug\cuddBddIte.sbr +.\Debug\cuddBridge.sbr +.\Debug\cuddCache.sbr +.\Debug\cuddCheck.sbr +.\Debug\cuddClip.sbr +.\Debug\cuddCof.sbr +.\Debug\cuddCompose.sbr +.\Debug\cuddDecomp.sbr +.\Debug\cuddEssent.sbr +.\Debug\cuddExact.sbr +.\Debug\cuddExport.sbr +.\Debug\cuddGenCof.sbr +.\Debug\cuddGenetic.sbr +.\Debug\cuddGroup.sbr +.\Debug\cuddHarwell.sbr +.\Debug\cuddInit.sbr +.\Debug\cuddInteract.sbr +.\Debug\cuddLCache.sbr +.\Debug\cuddLevelQ.sbr +.\Debug\cuddLinear.sbr +.\Debug\cuddLiteral.sbr +.\Debug\cuddMatMult.sbr +.\Debug\cuddPriority.sbr +.\Debug\cuddRead.sbr +.\Debug\cuddRef.sbr +.\Debug\cuddReorder.sbr +.\Debug\cuddSat.sbr +.\Debug\cuddSign.sbr +.\Debug\cuddSolve.sbr +.\Debug\cuddSplit.sbr +.\Debug\cuddSubsetHB.sbr +.\Debug\cuddSubsetSP.sbr +.\Debug\cuddSymmetry.sbr +.\Debug\cuddTable.sbr +.\Debug\cuddUtil.sbr +.\Debug\cuddWindow.sbr +.\Debug\cuddZddCount.sbr +.\Debug\cuddZddFuncs.sbr +.\Debug\cuddZddGroup.sbr +.\Debug\cuddZddIsop.sbr +.\Debug\cuddZddLin.sbr +.\Debug\cuddZddMisc.sbr +.\Debug\cuddZddPort.sbr +.\Debug\cuddZddReord.sbr +.\Debug\cuddZddSetop.sbr +.\Debug\cuddZddSymm.sbr +.\Debug\cuddZddUtil.sbr +.\Debug\epd.sbr +.\Debug\mtrBasic.sbr +.\Debug\mtrGroup.sbr +.\Debug\parseCore.sbr +.\Debug\parseStack.sbr +.\Debug\dsdApi.sbr +.\Debug\dsdCheck.sbr +.\Debug\dsdLocal.sbr +.\Debug\dsdMan.sbr +.\Debug\dsdProc.sbr +.\Debug\dsdTree.sbr +.\Debug\reoApi.sbr +.\Debug\reoCore.sbr +.\Debug\reoProfile.sbr +.\Debug\reoSift.sbr +.\Debug\reoSwap.sbr +.\Debug\reoTest.sbr +.\Debug\reoTransfer.sbr +.\Debug\reoUnits.sbr +.\Debug\added.sbr +.\Debug\solver.sbr +.\Debug\msatActivity.sbr +.\Debug\msatClause.sbr +.\Debug\msatClauseVec.sbr +.\Debug\msatMem.sbr +.\Debug\msatQueue.sbr +.\Debug\msatRead.sbr +.\Debug\msatSolverApi.sbr +.\Debug\msatSolverCore.sbr +.\Debug\msatSolverIo.sbr +.\Debug\msatSolverSearch.sbr +.\Debug\msatSort.sbr +.\Debug\msatVec.sbr +.\Debug\fraigApi.sbr +.\Debug\fraigCanon.sbr +.\Debug\fraigFanout.sbr +.\Debug\fraigFeed.sbr +.\Debug\fraigMan.sbr +.\Debug\fraigMem.sbr +.\Debug\fraigNode.sbr +.\Debug\fraigPrime.sbr +.\Debug\fraigSat.sbr +.\Debug\fraigTable.sbr +.\Debug\fraigUtil.sbr +.\Debug\fraigVec.sbr +.\Debug\csat_apis.sbr +.\Debug\fxu.sbr +.\Debug\fxuCreate.sbr +.\Debug\fxuHeapD.sbr +.\Debug\fxuHeapS.sbr +.\Debug\fxuList.sbr +.\Debug\fxuMatrix.sbr +.\Debug\fxuPair.sbr +.\Debug\fxuPrint.sbr +.\Debug\fxuReduce.sbr +.\Debug\fxuSelect.sbr +.\Debug\fxuSingle.sbr +.\Debug\fxuUpdate.sbr +.\Debug\rwrDec.sbr +.\Debug\rwrEva.sbr +.\Debug\rwrExp.sbr +.\Debug\rwrLib.sbr +.\Debug\rwrMan.sbr +.\Debug\rwrPrint.sbr +.\Debug\rwrUtil.sbr +.\Debug\cutApi.sbr +.\Debug\cutCut.sbr +.\Debug\cutMan.sbr +.\Debug\cutMerge.sbr +.\Debug\cutNode.sbr +.\Debug\cutOracle.sbr +.\Debug\cutSeq.sbr +.\Debug\cutTruth.sbr +.\Debug\decAbc.sbr +.\Debug\decFactor.sbr +.\Debug\decMan.sbr +.\Debug\decPrint.sbr +.\Debug\decUtil.sbr +.\Debug\simMan.sbr +.\Debug\simSat.sbr +.\Debug\simSeq.sbr +.\Debug\simSupp.sbr +.\Debug\simSwitch.sbr +.\Debug\simSym.sbr +.\Debug\simSymSat.sbr +.\Debug\simSymSim.sbr +.\Debug\simSymStr.sbr +.\Debug\simUtils.sbr +.\Debug\xyzBuild.sbr +.\Debug\xyzCore.sbr +.\Debug\xyzMan.sbr +.\Debug\xyzMinEsop.sbr +.\Debug\xyzMinMan.sbr +.\Debug\xyzMinSop.sbr +.\Debug\xyzMinUtil.sbr +.\Debug\xyzTest.sbr +.\Debug\fpga.sbr +.\Debug\fpgaCore.sbr +.\Debug\fpgaCreate.sbr +.\Debug\fpgaCut.sbr +.\Debug\fpgaCutUtils.sbr +.\Debug\fpgaFanout.sbr +.\Debug\fpgaLib.sbr +.\Debug\fpgaMatch.sbr +.\Debug\fpgaSwitch.sbr +.\Debug\fpgaTime.sbr +.\Debug\fpgaTruth.sbr +.\Debug\fpgaUtils.sbr +.\Debug\fpgaVec.sbr +.\Debug\mapper.sbr +.\Debug\mapperCanon.sbr +.\Debug\mapperCore.sbr +.\Debug\mapperCreate.sbr +.\Debug\mapperCut.sbr +.\Debug\mapperCutUtils.sbr +.\Debug\mapperFanout.sbr +.\Debug\mapperLib.sbr +.\Debug\mapperMatch.sbr +.\Debug\mapperRefs.sbr +.\Debug\mapperSuper.sbr +.\Debug\mapperSwitch.sbr +.\Debug\mapperTable.sbr +.\Debug\mapperTime.sbr +.\Debug\mapperTree.sbr +.\Debug\mapperTruth.sbr +.\Debug\mapperUtils.sbr +.\Debug\mapperVec.sbr +.\Debug\mio.sbr +.\Debug\mioApi.sbr +.\Debug\mioFunc.sbr +.\Debug\mioRead.sbr +.\Debug\mioUtils.sbr +.\Debug\super.sbr +.\Debug\superAnd.sbr +.\Debug\superGate.sbr +.\Debug\superWrite.sbr +.\Debug\pgaCore.sbr +.\Debug\pgaMan.sbr +.\Debug\pgaMatch.sbr +.\Debug\pgaUtil.sbr +.\Debug\extraBddKmap.sbr +.\Debug\extraBddMisc.sbr +.\Debug\extraBddSymm.sbr +.\Debug\extraUtilBitMatrix.sbr +.\Debug\extraUtilCanon.sbr +.\Debug\extraUtilFile.sbr +.\Debug\extraUtilMemory.sbr +.\Debug\extraUtilMisc.sbr +.\Debug\extraUtilProgress.sbr +.\Debug\extraUtilReader.sbr +.\Debug\st.sbr +.\Debug\stmm.sbr +.\Debug\cpu_stats.sbr +.\Debug\cpu_time.sbr +.\Debug\datalimit.sbr +.\Debug\getopt.sbr +.\Debug\pathsearch.sbr +.\Debug\safe_mem.sbr +.\Debug\strsav.sbr +.\Debug\texpand.sbr +.\Debug\mvc.sbr +.\Debug\mvcApi.sbr +.\Debug\mvcCompare.sbr +.\Debug\mvcContain.sbr +.\Debug\mvcCover.sbr +.\Debug\mvcCube.sbr +.\Debug\mvcDivide.sbr +.\Debug\mvcDivisor.sbr +.\Debug\mvcList.sbr +.\Debug\mvcLits.sbr +.\Debug\mvcMan.sbr +.\Debug\mvcOpAlg.sbr +.\Debug\mvcOpBool.sbr +.\Debug\mvcPrint.sbr +.\Debug\mvcSort.sbr +.\Debug\mvcUtils.sbr +.\Debug\msatOrderJ.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" +Creating browse info file... +<h3>Output Window</h3> @@ -74,4 +74,5 @@ alias compress "b; rw -l; rwz -l; b; rwz -l; b" alias compress2 "b; rw -l; rf -l; b; rw -l; rwz -l; b; rfz -l; rwz -l; b" alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore" alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore" +alias try "st; fpga; miter; fraig -rp" diff --git a/mcnc_temp.genlib_temp b/mcnc_temp.genlib_temp new file mode 100644 index 00000000..19f7a338 --- /dev/null +++ b/mcnc_temp.genlib_temp @@ -0,0 +1,67 @@ +# The genlib library "mcnc_temp.genlib". +GATE inv1 1.00 O=!a; + PIN a INV 1 999 0.90 0.00 0.90 0.00 +GATE inv2 2.00 O=!a; + PIN a INV 2 999 1.00 0.00 1.00 0.00 +GATE inv3 3.00 O=!a; + PIN a INV 3 999 1.10 0.00 1.10 0.00 +GATE inv4 4.00 O=!a; + PIN a INV 4 999 1.20 0.00 1.20 0.00 +GATE nand2 2.00 O=!(a*b); + PIN a INV 1 999 1.00 0.00 1.00 0.00 + PIN b INV 1 999 1.00 0.00 1.00 0.00 +GATE nand3 3.00 O=!(a*b*c); + PIN a INV 1 999 1.10 0.00 1.10 0.00 + PIN b INV 1 999 1.10 0.00 1.10 0.00 + PIN c INV 1 999 1.10 0.00 1.10 0.00 +GATE nand4 4.00 O=!(a*b*c*d); + PIN a INV 1 999 1.40 0.00 1.40 0.00 + PIN b INV 1 999 1.40 0.00 1.40 0.00 + PIN c INV 1 999 1.40 0.00 1.40 0.00 + PIN d INV 1 999 1.40 0.00 1.40 0.00 +GATE nor2 2.00 O=!(a+b); + PIN a INV 1 999 1.40 0.00 1.40 0.00 + PIN b INV 1 999 1.40 0.00 1.40 0.00 +GATE nor3 3.00 O=!(a+b+c); + PIN a INV 1 999 2.40 0.00 2.40 0.00 + PIN b INV 1 999 2.40 0.00 2.40 0.00 + PIN c INV 1 999 2.40 0.00 2.40 0.00 +GATE nor4 4.00 O=!(a+b+c+d); + PIN a INV 1 999 3.80 0.00 3.80 0.00 + PIN b INV 1 999 3.80 0.00 3.80 0.00 + PIN c INV 1 999 3.80 0.00 3.80 0.00 + PIN d INV 1 999 3.80 0.00 3.80 0.00 +GATE xora 5.00 O=a*!b+!a*b; + PIN a UNKNOWN 2 999 1.90 0.00 1.90 0.00 + PIN b UNKNOWN 2 999 1.90 0.00 1.90 0.00 +GATE xorb 5.00 O=!(a*b+!a*!b); + PIN a UNKNOWN 2 999 1.90 0.00 1.90 0.00 + PIN b UNKNOWN 2 999 1.90 0.00 1.90 0.00 +GATE xnora 5.00 O=a*b+!a*!b; + PIN a UNKNOWN 2 999 2.10 0.00 2.10 0.00 + PIN b UNKNOWN 2 999 2.10 0.00 2.10 0.00 +GATE xnorb 5.00 O=!(!a*b+a*!b); + PIN a UNKNOWN 2 999 2.10 0.00 2.10 0.00 + PIN b UNKNOWN 2 999 2.10 0.00 2.10 0.00 +GATE aoi21 3.00 O=!(a*b+c); + PIN a INV 1 999 1.60 0.00 1.60 0.00 + PIN b INV 1 999 1.60 0.00 1.60 0.00 + PIN c INV 1 999 1.60 0.00 1.60 0.00 +GATE aoi22 4.00 O=!(a*b+c*d); + PIN a INV 1 999 2.00 0.00 2.00 0.00 + PIN b INV 1 999 2.00 0.00 2.00 0.00 + PIN c INV 1 999 2.00 0.00 2.00 0.00 + PIN d INV 1 999 2.00 0.00 2.00 0.00 +GATE oai21 3.00 O=!((a+b)*c); + PIN a INV 1 999 1.60 0.00 1.60 0.00 + PIN b INV 1 999 1.60 0.00 1.60 0.00 + PIN c INV 1 999 1.60 0.00 1.60 0.00 +GATE oai22 4.00 O=!((a+b)*(c+d)); + PIN a INV 1 999 2.00 0.00 2.00 0.00 + PIN b INV 1 999 2.00 0.00 2.00 0.00 + PIN c INV 1 999 2.00 0.00 2.00 0.00 + PIN d INV 1 999 2.00 0.00 2.00 0.00 +GATE buf 1.00 O=a; + PIN a NONINV 1 999 1.00 0.00 1.00 0.00 +GATE zero 0.00 O=CONST0; +GATE one 0.00 O=CONST1; diff --git a/mcnc_temp.super b/mcnc_temp.super new file mode 100644 index 00000000..31735b8b --- /dev/null +++ b/mcnc_temp.super @@ -0,0 +1,42 @@ +# +# Supergate library derived for "mcnc_temp.genlib_temp" on Sun Dec 25 06:29:48 2005. +# +# Command line: "super -i 5 -l 1 -d 10000000.00 -a 10000000.00 -t 100 mcnc_temp.genlib_temp". +# +# The number of inputs = 5. +# The number of levels = 1. +# The maximum delay = 10000000.00. +# The maximum area = 10000000.00. +# The maximum runtime (sec) = 100. +# +# The number of attempts = 860. +# The number of supergates = 20. +# The number of functions = 0. +# The total functions = 4294967296 (2^32). +# +# Generation time (sec) = 0.01. +# +mcnc_temp.genlib_temp +5 +20 +25 +* xorb 1 0 +* nor4 2 1 0 3 +* nor3 2 1 0 +* oai22 2 1 0 3 +* oai22 2 0 1 3 +* aoi21 1 0 2 +* aoi22 2 3 1 0 +* nor2 1 0 +* oai22 2 3 1 0 +* aoi21 2 0 1 +* aoi22 2 0 1 3 +* aoi21 2 1 0 +* aoi22 2 1 0 3 +* oai21 1 0 2 +* oai21 2 0 1 +* oai21 2 1 0 +* nand2 1 0 +* nand3 2 1 0 +* nand4 2 1 0 3 +* xnora 1 0 diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 53ad88c2..167e7552 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -572,7 +572,28 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) return Abc_AigOr( pMan, Abc_AigAnd(pMan, p0, Abc_ObjNot(p1)), Abc_AigAnd(pMan, p1, Abc_ObjNot(p0)) ); } + +/**Function************************************************************* + + Synopsis [Implements the miter.] + + Description [] + + SideEffects [] + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_AigMiter_rec( Abc_Aig_t * pMan, Abc_Obj_t ** ppObjs, int nObjs ) +{ + Abc_Obj_t * pObj1, * pObj2; + if ( nObjs == 1 ) + return ppObjs[0]; + pObj1 = Abc_AigMiter_rec( pMan, ppObjs, nObjs/2 ); + pObj2 = Abc_AigMiter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 ); + return Abc_AigOr( pMan, pObj1, pObj2 ); +} + /**Function************************************************************* Synopsis [Implements the miter.] @@ -586,6 +607,30 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) ***********************************************************************/ Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs ) { + int i; + if ( vPairs->nSize == 0 ) + return Abc_ObjNot( Abc_NtkConst1(pMan->pNtkAig) ); + assert( vPairs->nSize % 2 == 0 ); + // go through the cubes of the node's SOP + for ( i = 0; i < vPairs->nSize; i += 2 ) + vPairs->pArray[i/2] = Abc_AigXor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] ); + vPairs->nSize = vPairs->nSize/2; + return Abc_AigMiter_rec( pMan, (Abc_Obj_t **)vPairs->pArray, vPairs->nSize ); +} + +/**Function************************************************************* + + Synopsis [Implements the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_AigMiter2( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs ) +{ Abc_Obj_t * pMiter, * pXor; int i; assert( vPairs->nSize % 2 == 0 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 71b76cf6..70cd2e6c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2868,6 +2868,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); return 0; } + if ( Abc_NtkIsSeq(pNtk) ) + { + fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" ); + return 0; + } + +/* if ( !Abc_NtkIsLogic(pNtk) ) { fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" ); @@ -2877,19 +2884,35 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkUnmap(pNtk); if ( Abc_NtkIsSopLogic(pNtk) ) Abc_NtkSopToBdd(pNtk); - - RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose ); - if ( RetValue == -1 ) - printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); - else if ( RetValue == 0 ) - printf( "The miter is SATISFIABLE.\n" ); +*/ + if ( Abc_NtkIsStrash(pNtk) ) + { + RetValue = Abc_NtkMiterSat2( pNtk, nSeconds, fVerbose ); + if ( RetValue == -1 ) + printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); + else if ( RetValue == 0 ) + printf( "The miter is SATISFIABLE.\n" ); + else + printf( "The miter is UNSATISFIABLE.\n" ); + } else - printf( "The miter is UNSATISFIABLE.\n" ); + { + Abc_Ntk_t * pTemp; + pTemp = Abc_NtkStrash( pNtk, 0, 0 ); + RetValue = Abc_NtkMiterSat2( pTemp, nSeconds, fVerbose ); + if ( RetValue == -1 ) + printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); + else if ( RetValue == 0 ) + printf( "The miter is SATISFIABLE.\n" ); + else + printf( "The miter is UNSATISFIABLE.\n" ); + Abc_NtkDelete( pTemp ); + } return 0; usage: fprintf( pErr, "usage: sat [-T num] [-vh]\n" ); - fprintf( pErr, "\t solves the miter\n" ); + fprintf( pErr, "\t solves the combinational miter\n" ); fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -3722,11 +3745,11 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) } // run the command - pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose ); + pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); - return 1; + return 0; } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -3788,9 +3811,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } -// Abc_NtkDeriveEsops( pNtk ); -// Abc_NtkXyz( pNtk, 128, 0, 0, 0 ); - printf( "This command is currently not used.\n" ); + Abc_NtkTestEsop( pNtk ); +// Abc_NtkTestSop( pNtk ); +// printf( "This command is currently not used.\n" ); /* // run the command diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 4a65659c..8c8636c5 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -27,6 +27,10 @@ static int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ); static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ); +static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ); + +static nMuxes; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -129,7 +133,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) Vec_Str_t * vCube; Vec_Int_t * vVars; char * pSop0, * pSop1; - int i; + int i, clk = clock(); assert( Abc_NtkIsBddLogic(pNtk) ); @@ -159,6 +163,8 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) } // Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 ); + PRT( "Creating solver", clock() - clk ); + // delete Vec_StrFree( vCube ); Vec_IntFree( vVars ); @@ -291,6 +297,495 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) } + + + + + + + + + +/**Function************************************************************* + + Synopsis [Attempts to solve the miter using an internal SAT solver.] + + Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) +{ + solver * pSat; + lbool status; + int RetValue, clk; + + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkLatchNum(pNtk) == 0 ); + + if ( Abc_NtkPoNum(pNtk) > 1 ) + fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) ); + + // load clauses into the solver + clk = clock(); + pSat = Abc_NtkMiterSatCreate2( pNtk ); + if ( pSat == NULL ) + return 1; +// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); +// PRT( "Time", clock() - clk ); + + // simplify the problem + clk = clock(); + status = solver_simplify(pSat); +// printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); +// PRT( "Time", clock() - clk ); + if ( status == 0 ) + { + solver_delete( pSat ); +// printf( "The problem is UNSATISFIABLE after simplification.\n" ); + return 1; + } + + // solve the miter + clk = clock(); + if ( fVerbose ) + pSat->verbosity = 1; + status = solver_solve( pSat, NULL, NULL, nSeconds ); + if ( status == l_Undef ) + { +// printf( "The problem timed out.\n" ); + RetValue = -1; + } + else if ( status == l_True ) + { +// printf( "The problem is SATISFIABLE.\n" ); + RetValue = 0; + } + else if ( status == l_False ) + { +// printf( "The problem is UNSATISFIABLE.\n" ); + RetValue = 1; + } + else + assert( 0 ); + PRT( "SAT solver time", clock() - clk ); + + // if the problem is SAT, get the counterexample + if ( status == l_True ) + { + Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk ); + pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize ); + Vec_IntFree( vCiIds ); + } + // free the solver + solver_delete( pSat ); + return RetValue; +} + + + + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +{ +//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses ); + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) ); +// Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); +} + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_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( !Abc_ObjIsComplement( pNode ) ); + assert( Abc_ObjIsNode( pNode ) ); + +// nVars = solver_nvars(pSat); + Var = (int)pNode->pCopy; +// 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 = Abc_ObjIsComplement(vSuper->pArray[i]); + // determine the variable numbers + Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy; +// Var1 = (int)Abc_ObjRegular(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 = Abc_ObjIsComplement(vSuper->pArray[i]); + // determine the variable numbers + Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy; +// Var1 = (int)Abc_ObjRegular(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 Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT, Abc_Obj_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( !Abc_ObjIsComplement( pNode ) ); + assert( Abc_NodeIsMuxType( pNode ) ); + // get the variable numbers + VarF = (int)pNode->pCopy; + VarI = (int)pNodeC->pCopy; + VarT = (int)Abc_ObjRegular(pNodeT)->pCopy; + VarE = (int)Abc_ObjRegular(pNodeE)->pCopy; +// VarF = (int)pNode->Id; +// VarI = (int)pNodeC->Id; +// VarT = (int)Abc_ObjRegular(pNodeT)->Id; +// VarE = (int)Abc_ObjRegular(pNodeE)->Id; + + // get the complementation flags + fCompT = Abc_ObjIsComplement(pNodeT); + fCompE = Abc_ObjIsComplement(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 Abc_NtkCollectSupergate_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux ) +{ + int RetValue1, RetValue2, i; + // check if the node is visited + if ( Abc_ObjRegular(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] == Abc_ObjNot(pNode) ) + return -1; + assert( 0 ); + return 0; + } + // if the new node is complemented or a PI, another gate begins + if ( !fFirst ) + if ( Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || Abc_ObjFanoutNum(pNode) > 1 || fStopAtMux && Abc_NodeIsMuxType(pNode) ) + { + Vec_PtrPush( vSuper, pNode ); + Abc_ObjRegular(pNode)->fMarkB = 1; + return 0; + } + assert( !Abc_ObjIsComplement(pNode) ); + assert( Abc_ObjIsNode(pNode) ); + // go through the branches + RetValue1 = Abc_NtkCollectSupergate_rec( Abc_ObjChild0(pNode), vSuper, 0, fStopAtMux ); + RetValue2 = Abc_NtkCollectSupergate_rec( Abc_ObjChild1(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 Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes ) +{ + int RetValue, i; + assert( !Abc_ObjIsComplement(pNode) ); + // collect the nodes in the implication supergate + Vec_PtrClear( vNodes ); + RetValue = Abc_NtkCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux ); + assert( vNodes->nSize > 1 ); + // unmark the visited nodes + for ( i = 0; i < vNodes->nSize; i++ ) + Abc_ObjRegular((Abc_Obj_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 Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE; + Vec_Ptr_t * vNodes, * vSuper; + Vec_Int_t * vVars; + int i, k, fUseMuxes = 1; + + assert( Abc_NtkIsStrash(pNtk) ); + + // 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 = Abc_NtkConst1(pNtk); + pNode->fMarkA = 1; + pNode->pCopy = (Abc_Obj_t *)vNodes->nSize; + Vec_PtrPush( vNodes, pNode ); + Abc_NtkClauseTriv( pSat, pNode, vVars ); + + // collect the nodes that need clauses and top-level assignments + Abc_NtkForEachCo( pNtk, pNode, i ) + { + // get the fanin + pFanin = Abc_ObjFanin0(pNode); + // create the node's variable + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + // add the trivial clause + if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) ) + return 0; + } + + // add the clauses + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + assert( !Abc_ObjIsComplement(pNode) ); + if ( !Abc_NodeIsAigAnd(pNode) ) + continue; +//printf( "%d ", pNode->Id ); + + // add the clauses + if ( fUseMuxes && Abc_NodeIsMuxType(pNode) ) + { + nMuxes++; + + pNodeC = Abc_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 = Abc_ObjRegular(pFanin); + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + } + // add the clauses + if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) ) + return 0; + } + else + { + // get the supergate + Abc_NtkCollectSupergate( pNode, fUseMuxes, vSuper ); + // add the fanin nodes to explore + Vec_PtrForEachEntry( vSuper, pFanin, k ) + { + pFanin = Abc_ObjRegular(pFanin); + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + } + // add the clauses + if ( vSuper->nSize == 0 ) + { + if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) ) + return 0; + } + else + { + if ( !Abc_NtkClauseAnd( 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 * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ) +{ + solver * pSat; + Abc_Obj_t * pNode; + int RetValue, i, clk = clock(); + + nMuxes = 0; + + pSat = solver_new(); + RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk ); + Abc_NtkForEachObj( pNtk, pNode, i ) + pNode->fMarkA = 0; + Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); + if ( RetValue == 0 ) + { + solver_delete(pSat); + return NULL; + } + printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) ); + PRT( "Creating solver", clock() - clk ); + return pSat; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 070c871d..b30a6452 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -148,6 +148,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV Fraig_ParamsSetDefault( &Params ); Params.fVerbose = fVerbose; Params.nSeconds = nSeconds; + Params.fFuncRed = 0; + Params.nPatsRand = 0; + Params.nPatsDyna = 0; pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); Fraig_ManProveMiter( pMan ); @@ -325,6 +328,9 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF Fraig_ParamsSetDefault( &Params ); Params.fVerbose = fVerbose; Params.nSeconds = nSeconds; + Params.fFuncRed = 0; + Params.nPatsRand = 0; + Params.nPatsDyna = 0; pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 ); Fraig_ManProveMiter( pMan ); diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h index f18686ff..ea488068 100644 --- a/src/opt/xyz/xyz.h +++ b/src/opt/xyz/xyz.h @@ -46,6 +46,8 @@ struct Xyz_Man_t_ Vec_Ptr_t * vObjStrs; // object structures void * pMemory; // memory for the internal data strctures Min_Man_t * pManMin; // the cub manager + int fUseEsop; // enables ESOPs + int fUseSop; // enables SOPs // arrays to map local variables Vec_Int_t * vComTo0; // mapping of common variables into first fanin Vec_Int_t * vComTo1; // mapping of common variables into second fanin diff --git a/src/opt/xyz/xyzCore.c b/src/opt/xyz/xyzCore.c index a48f749e..e5089788 100644 --- a/src/opt/xyz/xyzCore.c +++ b/src/opt/xyz/xyzCore.c @@ -27,13 +27,19 @@ static void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ); static int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ); static void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary ); - +/* static int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); static int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); static int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); static int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); static int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); static int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); +*/ + +static int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj ); +static Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ); +static Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -59,6 +65,8 @@ Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUs // create the manager p = Xyz_ManAlloc( pNtk, nFaninMax ); + p->fUseEsop = fUseEsop; + p->fUseSop = 1;//fUseSop; pNtk->pManCut = p; // perform mapping @@ -69,6 +77,8 @@ Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUs pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk ); else pNtkNew = Abc_NtkXyzDerive( p, pNtk ); +// pNtkNew = NULL; + Xyz_ManFree( p ); pNtk->pManCut = NULL; @@ -164,7 +174,10 @@ int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ) } // traverse the cone starting from this node - Abc_NtkXyzCovers_rec( p, pObj, vBoundary ); + if ( Abc_ObjGetSupp(pObj) == NULL ) + Abc_NtkXyzCovers_rec( p, pObj, vBoundary ); + + // count the number of solved cones if ( Abc_ObjGetSupp(pObj) == NULL ) fStop = 0; else @@ -225,7 +238,7 @@ void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar { Abc_Obj_t * pObj0, * pObj1; // return if the support is already computed - if ( pObj->fMarkB || pObj->fMarkA || Abc_ObjGetSupp(pObj) ) + if ( pObj->fMarkB || pObj->fMarkA )//|| Abc_ObjGetSupp(pObj) ) // why do we need Supp check here??? return; // mark as visited pObj->fMarkB = 1; @@ -236,9 +249,9 @@ void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar Abc_NtkXyzCovers_rec( p, pObj0, vBoundary ); Abc_NtkXyzCovers_rec( p, pObj1, vBoundary ); // skip the node that spaced out - if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) || // fanin is not ready - !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) || // fanin is not ready - !Abc_NodeXyzPropagateEsop(p, pObj, pObj0, pObj1) ) // node's support or covers cannot be computed + if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) || // fanin is not ready + !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) || // fanin is not ready + !Abc_NodeXyzPropagate( p, pObj ) ) // node's support or covers cannot be computed { // save the nodes of the future boundary if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) ) @@ -331,6 +344,321 @@ Vec_Int_t * Abc_NodeXyzSupport( Xyz_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * v /**Function************************************************************* + Synopsis [Propagates all types of covers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj ) +{ + Min_Cube_t * pCoverP = NULL, * pCoverN = NULL, * pCoverX = NULL; + Min_Cube_t * pCov0, * pCov1, * pCover0, * pCover1; + Vec_Int_t * vSupp, * vSupp0, * vSupp1; + Abc_Obj_t * pObj0, * pObj1; + int fCompl0, fCompl1; + + pObj0 = Abc_ObjFanin0( pObj ); + pObj1 = Abc_ObjFanin1( pObj ); + + if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); + if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); + + // get the resulting support + vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); + vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); + vSupp = Abc_NodeXyzSupport( p, vSupp0, vSupp1 ); + + // quit if support if too large + if ( vSupp->nSize > p->nFaninMax ) + { + Vec_IntFree( vSupp ); + return 0; + } + + // get the complemented attributes + fCompl0 = Abc_ObjFaninC0( pObj ); + fCompl1 = Abc_ObjFaninC1( pObj ); + + // propagate ESOP + if ( p->fUseEsop ) + { + // get the covers + pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0); + pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1); + if ( pCov0 && pCov1 ) + { + // complement the first if needed + if ( !fCompl0 ) + pCover0 = pCov0; + else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube + pCover0 = pCov0->pNext; + else + pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0; + + // complement the second if needed + if ( !fCompl1 ) + pCover1 = pCov1; + else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube + pCover1 = pCov1->pNext; + else + pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1; + + // derive the new cover + pCoverX = Abc_NodeXyzProduct( p, pCover0, pCover1, 1, vSupp->nSize ); + } + } + // propagate SOPs + if ( p->fUseSop ) + { + // get the covers for the direct polarity + pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0); + pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1); + // derive the new cover + if ( pCover0 && pCover1 ) + pCoverP = Abc_NodeXyzProduct( p, pCover0, pCover1, 0, vSupp->nSize ); + + // get the covers for the inverse polarity + pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0); + pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1); + // derive the new cover + if ( pCover0 && pCover1 ) + pCoverN = Abc_NodeXyzSum( p, pCover0, pCover1, 0, vSupp->nSize ); + } + + // if none of the covers can be computed quit + if ( !pCoverX && !pCoverP && !pCoverN ) + { + Vec_IntFree( vSupp ); + return 0; + } + + // set the covers + assert( Abc_ObjGetSupp(pObj) == NULL ); + Abc_ObjSetSupp( pObj, vSupp ); + Abc_ObjSetCover( pObj, pCoverP, 0 ); + Abc_ObjSetCover( pObj, pCoverN, 1 ); + Abc_ObjSetCover2( pObj, pCoverX ); +//printf( "%3d : %4d %4d %4d\n", pObj->Id, Min_CoverCountCubes(pCoverP), Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverX) ); + + // count statistics + p->nSupps++; + p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps ); + return 1; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ) +{ + Min_Cube_t * pCube, * pCube0, * pCube1; + Min_Cube_t * pCover; + int i, Val0, Val1; + assert( pCover0 && pCover1 ); + + // clean storage + Min_ManClean( p->pManMin, nSupp ); + // go through the cube pairs + Min_CoverForEachCube( pCover0, pCube0 ) + Min_CoverForEachCube( pCover1, pCube1 ) + { + // go through the support variables of the cubes + for ( i = 0; i < p->vPairs0->nSize; i++ ) + { + Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] ); + Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] ); + if ( (Val0 & Val1) == 0 ) + break; + } + // check disjointness + if ( i < p->vPairs0->nSize ) + continue; + + if ( p->pManMin->nCubes > p->nCubesMax ) + { + pCover = Min_CoverCollect( p->pManMin, nSupp ); +//Min_CoverWriteFile( pCover, "large", 1 ); + Min_CoverRecycle( p->pManMin, pCover ); + return NULL; + } + + // create the product cube + pCube = Min_CubeAlloc( p->pManMin ); + + // add the literals + pCube->nLits = 0; + for ( i = 0; i < nSupp; i++ ) + { + if ( p->vComTo0->pArray[i] == -1 ) + Val0 = 3; + else + Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); + + if ( p->vComTo1->pArray[i] == -1 ) + Val1 = 3; + else + Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); + + if ( (Val0 & Val1) == 3 ) + continue; + + Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 ); + pCube->nLits++; + } + // add the cube to storage + if ( fEsop ) + Min_EsopAddCube( p->pManMin, pCube ); + else + Min_SopAddCube( p->pManMin, pCube ); + } + + // minimize the cover + if ( fEsop ) + Min_EsopMinimize( p->pManMin ); + else + Min_SopMinimize( p->pManMin ); + pCover = Min_CoverCollect( p->pManMin, nSupp ); + + // quit if the cover is too large + if ( Min_CoverCountCubes(pCover) > p->nFaninMax ) + { +/* +Min_CoverWriteFile( pCover, "large", 1 ); + Min_CoverExpand( p->pManMin, pCover ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + pCover = Min_CoverCollect( p->pManMin, nSupp ); +*/ + Min_CoverRecycle( p->pManMin, pCover ); + return NULL; + } + return pCover; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ) +{ + Min_Cube_t * pCube, * pCube0, * pCube1; + Min_Cube_t * pCover; + int i, Val0, Val1; + assert( pCover0 && pCover1 ); + + // clean storage + Min_ManClean( p->pManMin, nSupp ); + Min_CoverForEachCube( pCover0, pCube0 ) + { + // create the cube + pCube = Min_CubeAlloc( p->pManMin ); + pCube->nLits = 0; + for ( i = 0; i < p->vComTo0->nSize; i++ ) + { + if ( p->vComTo0->pArray[i] == -1 ) + continue; + Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); + if ( Val0 == 3 ) + continue; + Min_CubeXorVar( pCube, i, Val0 ^ 3 ); + pCube->nLits++; + } + if ( p->pManMin->nCubes > p->nCubesMax ) + { + pCover = Min_CoverCollect( p->pManMin, nSupp ); + Min_CoverRecycle( p->pManMin, pCover ); + return NULL; + } + // add the cube to storage + if ( fEsop ) + Min_EsopAddCube( p->pManMin, pCube ); + else + Min_SopAddCube( p->pManMin, pCube ); + } + Min_CoverForEachCube( pCover1, pCube1 ) + { + // create the cube + pCube = Min_CubeAlloc( p->pManMin ); + pCube->nLits = 0; + for ( i = 0; i < p->vComTo1->nSize; i++ ) + { + if ( p->vComTo1->pArray[i] == -1 ) + continue; + Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); + if ( Val1 == 3 ) + continue; + Min_CubeXorVar( pCube, i, Val1 ^ 3 ); + pCube->nLits++; + } + if ( p->pManMin->nCubes > p->nCubesMax ) + { + pCover = Min_CoverCollect( p->pManMin, nSupp ); + Min_CoverRecycle( p->pManMin, pCover ); + return NULL; + } + // add the cube to storage + if ( fEsop ) + Min_EsopAddCube( p->pManMin, pCube ); + else + Min_SopAddCube( p->pManMin, pCube ); + } + + // minimize the cover + if ( fEsop ) + Min_EsopMinimize( p->pManMin ); + else + Min_SopMinimize( p->pManMin ); + pCover = Min_CoverCollect( p->pManMin, nSupp ); + + // quit if the cover is too large + if ( Min_CoverCountCubes(pCover) > p->nFaninMax ) + { + Min_CoverRecycle( p->pManMin, pCover ); + return NULL; + } + return pCover; +} + + + + + + + +#if 0 + + + +/**Function************************************************************* + Synopsis [] Description [] @@ -581,7 +909,7 @@ int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pC pCube->nLits++; } // add the cube to storage - while ( Min_EsopAddCube( p->pManMin, pCube ) ); + Min_EsopAddCube( p->pManMin, pCube ); } return 1; } @@ -642,7 +970,7 @@ int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCov if ( p->pManMin->nCubes >= p->nCubesMax ) return 0; // add the cube to storage - while ( Min_EsopAddCube( p->pManMin, pCube ) ); + Min_EsopAddCube( p->pManMin, pCube ); } } if ( pCover1 ) @@ -665,7 +993,7 @@ int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCov if ( p->pManMin->nCubes >= p->nCubesMax ) return 0; // add the cube to storage - while ( Min_EsopAddCube( p->pManMin, pCube ) ); + Min_EsopAddCube( p->pManMin, pCube ); } } return 1; @@ -688,7 +1016,7 @@ int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCove } - +#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h index 22950bfd..656612aa 100644 --- a/src/opt/xyz/xyzInt.h +++ b/src/opt/xyz/xyzInt.h @@ -81,10 +81,10 @@ static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uDa /*=== xyzMinEsop.c ==========================================================*/ extern void Min_EsopMinimize( Min_Man_t * p ); -extern int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); +extern void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); /*=== xyzMinSop.c ==========================================================*/ extern void Min_SopMinimize( Min_Man_t * p ); -extern int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); +extern void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); /*=== xyzMinMan.c ==========================================================*/ extern Min_Man_t * Min_ManAlloc( int nVars ); extern void Min_ManClean( Min_Man_t * p, int nSupp ); @@ -92,8 +92,10 @@ extern void Min_ManFree( Min_Man_t * p ); /*=== xyzMinUtil.c ==========================================================*/ extern void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube ); extern void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ); +extern void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p ); extern void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ); extern void Min_CoverCheck( Min_Man_t * p ); +extern int Min_CubeCheck( Min_Cube_t * pCube ); extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ); extern void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover ); extern int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover ); @@ -161,6 +163,7 @@ static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy ) Min_Cube_t * pCube; pCube = Min_CubeAlloc( p ); memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords ); + pCube->nLits = pCopy->nLits; return pCube; } @@ -538,6 +541,24 @@ static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, M } } +/**Function************************************************************* + + Synopsis [Transforms the cube into the result of distance-1 merging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist ) +{ + int w; + for ( w = 0; w < (int)pCube->nWords; w++ ) + pCube->uData[w] |= pDist->uData[w]; +} + /**Function************************************************************* @@ -579,7 +600,7 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove /**Function************************************************************* - Synopsis [Check if the cube is equal or dist1 or contained.] + Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.] Description [] @@ -588,42 +609,32 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove SeeAlso [] ***********************************************************************/ -static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew ) +static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube ) { - Min_Cube_t * pCube; + Min_Cube_t * pThis; int i; - // check identity - Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube ) - if ( Min_CubesAreEqual( pCube, pNew ) ) +/* + // this cube cannot be equal to any cube + Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) + { + if ( Min_CubesAreEqual( pCube, pThis ) ) + { + Min_CubeWrite( stdout, pCube ); + assert( 0 ); + } + } +*/ + // try to find a containing cube + for ( i = 0; i <= (int)pCube->nLits; i++ ) + Min_CoverForEachCube( p->ppStore[i], pThis ) + { + // skip the bubble + if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) return 1; - // check containment - for ( i = 0; i < (int)pNew->nLits; i++ ) - Min_CoverForEachCube( p->ppStore[i], pCube ) - if ( Min_CubeIsContained( pCube, pNew ) ) - return 1; + } return 0; } -/**Function************************************************************* - - Synopsis [Check if the cube is equal or dist1 or contained.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew ) -{ - Min_Cube_t * pCube; - Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube ) - if ( Min_CubesDistOne( pCube, pNew, NULL ) ) - return pCube; - return NULL; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c index 114e28a6..839e2410 100644 --- a/src/opt/xyz/xyzMinEsop.c +++ b/src/opt/xyz/xyzMinEsop.c @@ -62,7 +62,11 @@ void Min_EsopMinimize( Min_Man_t * p ) Synopsis [Performs one round of rewriting using distance 2 cubes.] - Description [] + Description [The weakness of this procedure is that it tries each cube + with only one distance-2 cube. If this pair does not lead to improvement + the cube is inserted into the cover anyhow, and we try another pair. + A possible improvement would be to try this cube with all distance-2 + cubes, until an improvement is found, or until all such cubes are tried.] SideEffects [] @@ -162,8 +166,8 @@ void Min_EsopRewrite( Min_Man_t * p ) // add the cubes nCubesOld = p->nCubes; - while ( Min_EsopAddCube( p, pCube ) ); - while ( Min_EsopAddCube( p, pThis ) ); + Min_EsopAddCube( p, pCube ); + Min_EsopAddCube( p, pThis ); // check if the cubes were absorbed if ( p->nCubes < nCubesOld + 2 ) continue; @@ -191,8 +195,8 @@ void Min_EsopRewrite( Min_Man_t * p ) pThis->nLits += (v11 != 3); // add them anyhow - while ( Min_EsopAddCube( p, pCube ) ); - while ( Min_EsopAddCube( p, pThis ) ); + Min_EsopAddCube( p, pCube ); + Min_EsopAddCube( p, pThis ); } // printf( "Pairs = %d ", nPairs ); } @@ -201,8 +205,8 @@ void Min_EsopRewrite( Min_Man_t * p ) Synopsis [Adds the cube to storage.] - Description [If the distance one cube is found, returns the transformed - cube. If there is no distance one, adds the given cube to storage. + Description [Returns 0 if the cube is added or removed. Returns 1 + if the cube is glued with some other cube and has to be added again. Do not forget to clean the storage!] SideEffects [] @@ -210,7 +214,7 @@ void Min_EsopRewrite( Min_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) +int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube ) { Min_Cube_t * pThis, ** ppPrev; // try to find the identical cube @@ -270,6 +274,24 @@ int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) return 0; } +/**Function************************************************************* + + Synopsis [Adds the cube to storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) +{ + assert( pCube != p->pBubble ); + assert( (int)pCube->nLits == Min_CubeCountLits(pCube) ); + while ( Min_EsopAddCubeInt( p, pCube ) ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/xyz/xyzMinMan.c b/src/opt/xyz/xyzMinMan.c index 423564c1..20314698 100644 --- a/src/opt/xyz/xyzMinMan.c +++ b/src/opt/xyz/xyzMinMan.c @@ -62,6 +62,7 @@ Min_Man_t * Min_ManAlloc( int nVars ) pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 ); pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 ); pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 ); + Min_ManClean( pMan, nVars ); return pMan; } diff --git a/src/opt/xyz/xyzMinSop.c b/src/opt/xyz/xyzMinSop.c index 1c5951fe..a5d57c66 100644 --- a/src/opt/xyz/xyzMinSop.c +++ b/src/opt/xyz/xyzMinSop.c @@ -52,10 +52,11 @@ void Min_SopMinimize( Min_Man_t * p ) nCubesOld = p->nCubes; Min_SopRewrite( p ); nIter++; +// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); } while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); +// printf( "\n" ); -// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); } /**Function************************************************************* @@ -74,8 +75,17 @@ void Min_SopRewrite( Min_Man_t * p ) Min_Cube_t * pCube, ** ppPrev; Min_Cube_t * pThis, ** ppPrevT; Min_Cube_t * pTemp; - int v00, v01, v10, v11, Var0, Var1, Index; + int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld; int nPairs = 0; +/* + { + Min_Cube_t * pCover; + pCover = Min_CoverCollect( p, p->nVars ); +printf( "\n\n" ); +Min_CoverWrite( stdout, pCover ); + Min_CoverExpand( p, pCover ); + } +*/ // insert the bubble before the first cube p->pBubble->pNext = p->ppStore[0]; @@ -127,7 +137,11 @@ void Min_SopRewrite( Min_Man_t * p ) continue; } nPairs++; - +/* +printf( "\n" ); +Min_CubeWrite( stdout, pCube ); +Min_CubeWrite( stdout, pThis ); +*/ // remove the cubes, insert the bubble instead of pCube *ppPrevT = pThis->pNext; *ppPrev = p->pBubble; @@ -135,6 +149,8 @@ void Min_SopRewrite( Min_Man_t * p ) p->pBubble->nLits = pCube->nLits; p->nCubes -= 2; + assert( pCube != p->pBubble && pThis != p->pBubble ); + // save the dist2 parameters v00 = Min_CubeGetVar( pCube, Var0 ); @@ -145,22 +161,83 @@ void Min_SopRewrite( Min_Man_t * p ) assert( v00 != 3 || v01 != 3 ); assert( v10 != 3 || v11 != 3 ); - // skip the case when rewriting is impossible +//printf( "\n" ); +//Min_CubeWrite( stdout, pCube ); +//Min_CubeWrite( stdout, pThis ); + +//printf( "\n" ); +//Min_CubeWrite( stdout, pCube ); +//Min_CubeWrite( stdout, pThis ); + + // consider the case when both cubes have non-empty literals if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 ) + { + assert( v00 == (v10 ^ 3) ); + assert( v01 == (v11 ^ 3) ); + // create the temporary cube equal to the first corner + Min_CubeXorVar( pCube, Var0, 3 ); + // check if this cube is contained + fCont0 = Min_CoverContainsCube( p, pCube ); + // create the temporary cube equal to the first corner + Min_CubeXorVar( pCube, Var0, 3 ); + Min_CubeXorVar( pCube, Var1, 3 ); +//printf( "\n" ); +//Min_CubeWrite( stdout, pCube ); +//Min_CubeWrite( stdout, pThis ); + // check if this cube is contained + fCont1 = Min_CoverContainsCube( p, pCube ); + // undo the change + Min_CubeXorVar( pCube, Var1, 3 ); + + // check if the cubes can be overwritten + if ( fCont0 && fCont1 ) + { + // one of the cubes can be recycled, the other expanded and added + Min_CubeRecycle( p, pThis ); + // remove the literals + Min_CubeXorVar( pCube, Var0, v00 ^ 3 ); + Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); + pCube->nLits -= 2; + Min_SopAddCube( p, pCube ); + } + else if ( fCont0 ) + { + // expand both cubes and add them + Min_CubeXorVar( pCube, Var0, v00 ^ 3 ); + pCube->nLits--; + Min_SopAddCube( p, pCube ); + Min_CubeXorVar( pThis, Var1, v11 ^ 3 ); + pThis->nLits--; + Min_SopAddCube( p, pThis ); + } + else if ( fCont1 ) + { + // expand both cubes and add them + Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); + pCube->nLits--; + Min_SopAddCube( p, pCube ); + Min_CubeXorVar( pThis, Var0, v10 ^ 3 ); + pThis->nLits--; + Min_SopAddCube( p, pThis ); + } + else + { + Min_SopAddCube( p, pCube ); + Min_SopAddCube( p, pThis ); + } + // otherwise, no change is possible continue; + } // if one of them does not have DC lit, move it if ( v00 != 3 && v01 != 3 ) { + assert( v10 == 3 || v11 == 3 ); pTemp = pCube; pCube = pThis; pThis = pTemp; Index = v00; v00 = v10; v10 = Index; Index = v01; v01 = v11; v11 = Index; } -//printf( "\n" ); -//Min_CubeWrite( stdout, pCube ); -//Min_CubeWrite( stdout, pThis ); - // make sure the first cube has first var DC if ( v00 != 3 ) { @@ -174,13 +251,93 @@ void Min_SopRewrite( Min_Man_t * p ) if ( v00 == 3 && v11 == 3 ) { assert( v01 != 3 && v10 != 3 ); - // try two reduced cubes - + // try the remaining minterm + // create the temporary cube equal to the first corner + Min_CubeXorVar( pCube, Var0, v10 ); + Min_CubeXorVar( pCube, Var1, 3 ); + pCube->nLits++; + // check if this cube is contained + fCont0 = Min_CoverContainsCube( p, pCube ); + // undo the cube transformations + Min_CubeXorVar( pCube, Var0, v10 ); + Min_CubeXorVar( pCube, Var1, 3 ); + pCube->nLits--; + // check the case when both are covered + if ( fCont0 ) + { + // one of the cubes can be recycled, the other expanded and added + Min_CubeRecycle( p, pThis ); + // remove the literals + Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); + pCube->nLits--; + Min_SopAddCube( p, pCube ); + } + else + { + // try two reduced cubes + Min_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits++; + // remember the cubes + nCubesOld = p->nCubes; + Min_SopAddCube( p, pCube ); + // check if the cube is absorbed + if ( p->nCubes < nCubesOld + 1 ) + { // absorbed - add the second cube + Min_SopAddCube( p, pThis ); + } + else + { // remove this cube, and try another one + assert( pCube == p->ppStore[pCube->nLits] ); + p->ppStore[pCube->nLits] = pCube->pNext; + p->nCubes--; + + // return the cube to the previous state + Min_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits--; + + // generate another reduced cube + Min_CubeXorVar( pThis, Var1, v01 ); + pThis->nLits++; + + // add both cubes + Min_SopAddCube( p, pCube ); + Min_SopAddCube( p, pThis ); + } + } } else // the first cube has DC lit { assert( v01 != 3 && v10 != 3 && v11 != 3 ); - // try reduced and expanded cube + // try the remaining minterm + // create the temporary cube equal to the minterm + Min_CubeXorVar( pThis, Var0, 3 ); + // check if this cube is contained + fCont0 = Min_CoverContainsCube( p, pThis ); + // undo the cube transformations + Min_CubeXorVar( pThis, Var0, 3 ); + // check the case when both are covered + if ( fCont0 ) + { + // one of the cubes can be recycled, the other expanded and added + Min_CubeRecycle( p, pThis ); + // remove the literals + Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); + pCube->nLits--; + Min_SopAddCube( p, pCube ); + } + else + { + // try reshaping the cubes + // reduce the first cube + Min_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits++; + // expand the second cube + Min_CubeXorVar( pThis, Var1, v11 ^ 3 ); + pThis->nLits--; + // add both cubes + Min_SopAddCube( p, pCube ); + Min_SopAddCube( p, pThis ); + } } } // printf( "Pairs = %d ", nPairs ); @@ -188,26 +345,80 @@ void Min_SopRewrite( Min_Man_t * p ) /**Function************************************************************* - Synopsis [] + Synopsis [Adds cube to the SOP cover stored in the manager.] - Description [] + Description [Returns 0 if the cube is added or removed. Returns 1 + if the cube is glued with some other cube and has to be added again.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) +int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube ) { - return 1; -} - + Min_Cube_t * pThis, * pThis2, ** ppPrev; + int i; + // try to find the identical cube + Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) + { + if ( Min_CubesAreEqual( pCube, pThis ) ) + { + Min_CubeRecycle( p, pCube ); + return 0; + } + } + // try to find a containing cube + for ( i = 0; i < (int)pCube->nLits; i++ ) + Min_CoverForEachCube( p->ppStore[i], pThis ) + { + if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) + { + Min_CubeRecycle( p, pCube ); + return 0; + } + } + // try to find distance one in the same bin + Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) + { + if ( Min_CubesDistOne( pCube, pThis, NULL ) ) + { + *ppPrev = pThis->pNext; + Min_CubesTransformOr( pCube, pThis ); + pCube->nLits--; + Min_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + // clean the other cubes using this one + for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ ) + { + ppPrev = &p->ppStore[i]; + Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 ) + { + if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) ) + { + *ppPrev = pThis->pNext; + Min_CubeRecycle( p, pThis ); + p->nCubes--; + } + else + ppPrev = &pThis->pNext; + } + } + // add the cube + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + return 0; +} /**Function************************************************************* - Synopsis [] + Synopsis [Adds the cube to storage.] Description [] @@ -216,27 +427,18 @@ int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) SeeAlso [] ***********************************************************************/ -void Min_SopDist1Merge( Min_Man_t * p ) +void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) { - Min_Cube_t * pCube, * pCube2, * pCubeNew; - int i; - for ( i = p->nVars; i >= 0; i-- ) - { - Min_CoverForEachCube( p->ppStore[i], pCube ) - Min_CoverForEachCube( pCube->pNext, pCube2 ) - { - assert( pCube->nLits == pCube2->nLits ); - if ( !Min_CubesDistOne( pCube, pCube2, NULL ) ) - continue; - pCubeNew = Min_CubesXor( p, pCube, pCube2 ); - assert( pCubeNew->nLits == pCube->nLits - 1 ); - pCubeNew->pNext = p->ppStore[pCubeNew->nLits]; - p->ppStore[pCubeNew->nLits] = pCubeNew; - p->nCubes++; - } - } + assert( Min_CubeCheck( pCube ) ); + assert( pCube != p->pBubble ); + assert( (int)pCube->nLits == Min_CubeCountLits(pCube) ); + while ( Min_SopAddCubeInt( p, pCube ) ); } + + + + /**Function************************************************************* Synopsis [] @@ -286,6 +488,38 @@ void Min_SopContain( Min_Man_t * p ) SeeAlso [] ***********************************************************************/ +void Min_SopDist1Merge( Min_Man_t * p ) +{ + Min_Cube_t * pCube, * pCube2, * pCubeNew; + int i; + for ( i = p->nVars; i >= 0; i-- ) + { + Min_CoverForEachCube( p->ppStore[i], pCube ) + Min_CoverForEachCube( pCube->pNext, pCube2 ) + { + assert( pCube->nLits == pCube2->nLits ); + if ( !Min_CubesDistOne( pCube, pCube2, NULL ) ) + continue; + pCubeNew = Min_CubesXor( p, pCube, pCube2 ); + assert( pCubeNew->nLits == pCube->nLits - 1 ); + pCubeNew->pNext = p->ppStore[pCubeNew->nLits]; + p->ppStore[pCubeNew->nLits] = pCubeNew; + p->nCubes++; + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp ) { Vec_Int_t * vVars; @@ -334,6 +568,46 @@ Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp ) return Min_CoverCollect( p, p->nVars ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Min_SopCheck( Min_Man_t * p ) +{ + Min_Cube_t * pCube, * pThis; + int i; + + pCube = Min_CubeAlloc( p ); + Min_CubeXorBit( pCube, 2*0+1 ); + Min_CubeXorBit( pCube, 2*1+1 ); + Min_CubeXorBit( pCube, 2*2+0 ); + Min_CubeXorBit( pCube, 2*3+0 ); + Min_CubeXorBit( pCube, 2*4+0 ); + Min_CubeXorBit( pCube, 2*5+1 ); + Min_CubeXorBit( pCube, 2*6+1 ); + pCube->nLits = 7; + +// Min_CubeWrite( stdout, pCube ); + + // check that the cubes contain it + for ( i = 0; i <= p->nVars; i++ ) + Min_CoverForEachCube( p->ppStore[i], pThis ) + if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) + { + Min_CubeRecycle( p, pCube ); + return 1; + } + Min_CubeRecycle( p, pCube ); + return 0; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/xyz/xyzMinUtil.c b/src/opt/xyz/xyzMinUtil.c index 0aebb815..9ec5f83f 100644 --- a/src/opt/xyz/xyzMinUtil.c +++ b/src/opt/xyz/xyzMinUtil.c @@ -92,13 +92,44 @@ void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ) SeeAlso [] ***********************************************************************/ +void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p ) +{ + Min_Cube_t * pCube; + int i; + for ( i = 0; i <= p->nVars; i++ ) + { + Min_CoverForEachCube( p->ppStore[i], pCube ) + { + printf( "%2d : ", i ); + if ( pCube == p->pBubble ) + { + printf( "Bubble\n" ); + continue; + } + Min_CubeWrite( pFile, pCube ); + } + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ) { char Buffer[1000]; Min_Cube_t * pCube; FILE * pFile; int i; - sprintf( Buffer, "%s.esop", pName ); + sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" ); for ( i = strlen(Buffer) - 1; i >= 0; i-- ) if ( Buffer[i] == '<' || Buffer[i] == '>' ) Buffer[i] = '_'; @@ -116,7 +147,7 @@ void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ) /**Function************************************************************* - Synopsis [Performs one round of rewriting using distance 2 cubes.] + Synopsis [] Description [] @@ -137,6 +168,26 @@ void Min_CoverCheck( Min_Man_t * p ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Min_CubeCheck( Min_Cube_t * pCube ) +{ + int i; + for ( i = 0; i < (int)pCube->nVars; i++ ) + if ( Min_CubeGetVar( pCube, i ) == 0 ) + return 0; + return 1; +} + +/**Function************************************************************* + Synopsis [Converts the cover from the sorted structure.] Description [] @@ -158,6 +209,7 @@ Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ) assert( i == (int)pCube->nLits ); *ppTail = pCube; ppTail = &pCube->pNext; + assert( pCube->uData[0] ); // not a bubble } } *ppTail = NULL; diff --git a/src/opt/xyz/xyzTest.c b/src/opt/xyz/xyzTest.c index 6c0a63f3..38580790 100644 --- a/src/opt/xyz/xyzTest.c +++ b/src/opt/xyz/xyzTest.c @@ -39,11 +39,377 @@ SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk ) +Min_Cube_t * Abc_NodeDeriveCoverPro( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 ) { - return NULL; + Min_Cube_t * pCover; + Min_Cube_t * pCube0, * pCube1, * pCube; + if ( pCover0 == NULL || pCover1 == NULL ) + return NULL; + // clean storage + Min_ManClean( p, p->nVars ); + // go through the cube pairs + Min_CoverForEachCube( pCover0, pCube0 ) + Min_CoverForEachCube( pCover1, pCube1 ) + { + if ( Min_CubesDisjoint( pCube0, pCube1 ) ) + continue; + pCube = Min_CubesProduct( p, pCube0, pCube1 ); + // add the cube to storage + Min_SopAddCube( p, pCube ); + } + Min_SopMinimize( p ); + pCover = Min_CoverCollect( p, p->nVars ); + assert( p->nCubes == Min_CoverCountCubes(pCover) ); + return pCover; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Abc_NodeDeriveCoverSum( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 ) +{ + Min_Cube_t * pCover; + Min_Cube_t * pThis, * pCube; + if ( pCover0 == NULL || pCover1 == NULL ) + return NULL; + // clean storage + Min_ManClean( p, p->nVars ); + // add the cubes to storage + Min_CoverForEachCube( pCover0, pThis ) + { + pCube = Min_CubeDup( p, pThis ); + Min_SopAddCube( p, pCube ); + } + Min_CoverForEachCube( pCover1, pThis ) + { + pCube = Min_CubeDup( p, pThis ); + Min_SopAddCube( p, pCube ); + } + Min_SopMinimize( p ); + pCover = Min_CoverCollect( p, p->nVars ); + assert( p->nCubes == Min_CoverCountCubes(pCover) ); + return pCover; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeDeriveSops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes ) +{ + Min_Cube_t * pCov0[2], * pCov1[2]; + Min_Cube_t * pCoverP, * pCoverN; + Abc_Obj_t * pObj; + int i, nCubes, fCompl0, fCompl1; + + // set elementary vars + Vec_PtrForEachEntry( vSupp, pObj, i ) + { + pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 ); + pObj->pNext = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 1 ); + } + + // get the cover for each node in the array + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // get the complements + fCompl0 = Abc_ObjFaninC0(pObj); + fCompl1 = Abc_ObjFaninC1(pObj); + // get the covers + pCov0[0] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy; + pCov0[1] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pNext; + pCov1[0] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy; + pCov1[1] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pNext; + // compute the covers + pCoverP = Abc_NodeDeriveCoverPro( p, pCov0[ fCompl0], pCov1[ fCompl1] ); + pCoverN = Abc_NodeDeriveCoverSum( p, pCov0[!fCompl0], pCov1[!fCompl1] ); + // set the covers + pObj->pCopy = (Abc_Obj_t *)pCoverP; + pObj->pNext = (Abc_Obj_t *)pCoverN; + } + + nCubes = ABC_MIN( Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverP) ); + +/* +printf( "\n\n" ); +Min_CoverWrite( stdout, pCoverP ); +printf( "\n\n" ); +Min_CoverWrite( stdout, pCoverN ); +*/ + +// printf( "\n" ); +// Min_CoverWrite( stdout, pCoverP ); + +// Min_CoverExpand( p, pCoverP ); +// Min_SopMinimize( p ); +// pCoverP = Min_CoverCollect( p, p->nVars ); + +// printf( "\n" ); +// Min_CoverWrite( stdout, pCoverP ); + +// nCubes = Min_CoverCountCubes(pCoverP); + + // clean the copy fields + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = pObj->pNext = NULL; + Vec_PtrForEachEntry( vSupp, pObj, i ) + pObj->pCopy = pObj->pNext = NULL; + +// Min_CoverWriteFile( pCoverP, Abc_ObjName(pRoot), 0 ); +// printf( "\n" ); +// Min_CoverWrite( stdout, pCoverP ); + +// printf( "\n" ); +// Min_CoverWrite( stdout, pCoverP ); +// printf( "\n" ); +// Min_CoverWrite( stdout, pCoverN ); + return nCubes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkTestSop( Abc_Ntk_t * pNtk ) +{ + Min_Man_t * p; + Vec_Ptr_t * vSupp, * vNodes; + Abc_Obj_t * pObj; + int i, nCubes; + assert( Abc_NtkIsStrash(pNtk) ); + + Abc_NtkCleanCopy(pNtk); + Abc_NtkCleanNext(pNtk); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) ) + { + printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) ); + continue; + } + + vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 ); + vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 ); + + printf( "%20s : Cone = %5d. Supp = %5d. ", + Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize ); +// if ( vSupp->nSize <= 128 ) + { + p = Min_ManAlloc( vSupp->nSize ); + nCubes = Abc_NodeDeriveSops( p, pObj, vSupp, vNodes ); + printf( "Cubes = %5d. ", nCubes ); + Min_ManFree( p ); + } + printf( "\n" ); + + + Vec_PtrFree( vNodes ); + Vec_PtrFree( vSupp ); + } +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Abc_NodeDeriveCover( Min_Man_t * p, Min_Cube_t * pCov0, Min_Cube_t * pCov1, int fComp0, int fComp1 ) +{ + Min_Cube_t * pCover0, * pCover1, * pCover; + Min_Cube_t * pCube0, * pCube1, * pCube; + + // complement the first if needed + if ( !fComp0 ) + pCover0 = pCov0; + else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube + pCover0 = pCov0->pNext; + else + pCover0 = p->pOne0, p->pOne0->pNext = pCov0; + + // complement the second if needed + if ( !fComp1 ) + pCover1 = pCov1; + else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube + pCover1 = pCov1->pNext; + else + pCover1 = p->pOne1, p->pOne1->pNext = pCov1; + + if ( pCover0 == NULL || pCover1 == NULL ) + return NULL; + + // clean storage + Min_ManClean( p, p->nVars ); + // go through the cube pairs + Min_CoverForEachCube( pCover0, pCube0 ) + Min_CoverForEachCube( pCover1, pCube1 ) + { + if ( Min_CubesDisjoint( pCube0, pCube1 ) ) + continue; + pCube = Min_CubesProduct( p, pCube0, pCube1 ); + // add the cube to storage + Min_EsopAddCube( p, pCube ); + } + + if ( p->nCubes > 10 ) + { +// printf( "(%d,", p->nCubes ); + Min_EsopMinimize( p ); +// printf( "%d) ", p->nCubes ); + } + + pCover = Min_CoverCollect( p, p->nVars ); + assert( p->nCubes == Min_CoverCountCubes(pCover) ); + +// if ( p->nCubes > 1000 ) +// printf( "%d ", p->nCubes ); + return pCover; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeDeriveEsops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes ) +{ + Min_Cube_t * pCover, * pCube; + Abc_Obj_t * pObj; + int i; + + // set elementary vars + Vec_PtrForEachEntry( vSupp, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 ); + + // get the cover for each node in the array + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + pCover = Abc_NodeDeriveCover( p, + (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy, + (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy, + Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + pObj->pCopy = (Abc_Obj_t *)pCover; + if ( p->nCubes > 3000 ) + return -1; + } + + // add complement if needed + if ( Abc_ObjFaninC0(pRoot) ) + { + if ( pCover && pCover->nLits == 0 ) // topmost one is the tautology cube + { + pCube = pCover; + pCover = pCover->pNext; + Min_CubeRecycle( p, pCube ); + p->nCubes--; + } + else + { + pCube = Min_CubeAlloc( p ); + pCube->pNext = pCover; + p->nCubes++; + } + } +/* + Min_CoverExpand( p, pCover ); + Min_EsopMinimize( p ); + pCover = Min_CoverCollect( p, p->nVars ); +*/ + // clean the copy fields + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = NULL; + Vec_PtrForEachEntry( vSupp, pObj, i ) + pObj->pCopy = NULL; + +// Min_CoverWriteFile( pCover, Abc_ObjName(pRoot), 1 ); +// Min_CoverWrite( stdout, pCover ); + return p->nCubes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkTestEsop( Abc_Ntk_t * pNtk ) +{ + Min_Man_t * p; + Vec_Ptr_t * vSupp, * vNodes; + Abc_Obj_t * pObj; + int i, nCubes; + assert( Abc_NtkIsStrash(pNtk) ); + + Abc_NtkCleanCopy(pNtk); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) ) + { + printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) ); + continue; + } + + vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 ); + vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 ); + + printf( "%20s : Cone = %5d. Supp = %5d. ", + Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize ); +// if ( vSupp->nSize <= 128 ) + { + p = Min_ManAlloc( vSupp->nSize ); + nCubes = Abc_NodeDeriveEsops( p, pObj, vSupp, vNodes ); + printf( "Cubes = %5d. ", nCubes ); + Min_ManFree( p ); + } + printf( "\n" ); + + + Vec_PtrFree( vNodes ); + Vec_PtrFree( vSupp ); + } +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index b82601c4..9618603c 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -52,8 +52,9 @@ static const lbool l_Undef = 0; static const lbool l_True = 1; static const lbool l_False = -1; -static inline lit neg (lit l) { return l ^ 1; } -static inline lit toLit (int v) { return v + v; } +static inline lit neg (lit l) { return l ^ 1; } +static inline lit toLit (int v) { return v + v; } +static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); } //================================================================================================= // Public interface: diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c index 97da413d..fab01368 100644 --- a/src/sat/fraig/fraigCanon.c +++ b/src/sat/fraig/fraigCanon.c @@ -68,7 +68,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_ return p1; return Fraig_Not(pMan->pConst1); } - +/* // check for less trivial cases if ( Fraig_IsComplement(p1) ) { @@ -125,7 +125,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_ return Fraig_Not(pMan->pConst1); } } - +*/ // perform level-one structural hashing if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found { diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index bc60e4e9..13f6b50b 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -41,6 +41,8 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i ); // The best way seems to be fanins followed by fanouts. Slight changes to this order // leads to big degradation in quality. +static int nMuxes; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -105,7 +107,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) } if ( p->fVerboseP ) { - PRT( "Final miter proof time", clock() - clk ); +// PRT( "Final miter proof time", clock() - clk ); } } @@ -195,6 +197,8 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * } */ + nMuxes = 0; + // get the logic cone clk = clock(); @@ -202,6 +206,9 @@ clk = clock(); // Fraig_PrepareCones( p, pOld, pNew ); p->timeTrav += clock() - clk; +// printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) ); +// PRT( "Time", clock() - clk ); + if ( fVerbose ) printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) ); @@ -226,6 +233,8 @@ clk = clock(); RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; +Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" ); + if ( RetValue1 == MSAT_FALSE ) { //p->time1 += clock() - clk; @@ -284,6 +293,7 @@ p->time3 += clock() - clk; clk = clock(); RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; + if ( RetValue1 == MSAT_FALSE ) { //p->time1 += clock() - clk; @@ -552,6 +562,7 @@ void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * Fraig_PrepareCones_rec( pMan, pNew ); Fraig_PrepareCones_rec( pMan, pOld ); + /* nVars = Msat_IntVecReadSize( pMan->vVarsInt ); pVars = Msat_IntVecReadArray( pMan->vVarsInt ); @@ -715,6 +726,8 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) ); Fraig_SupergateAddClausesMux( pMan, pNode ); // Fraig_DetectFanoutFreeConeMux( pMan, pNode ); + + nMuxes++; } else { @@ -1057,6 +1070,12 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) // t + e + f' // t' + e' + f + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return; + } + Msat_IntVecClear( p->vProj ); Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) ); Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) ); @@ -1069,6 +1088,7 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); assert( RetValue ); + } diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 37e0bbeb..40028784 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -87,6 +87,7 @@ extern void Msat_SolverPrintClauses( Msat_Solver_t * p ); extern void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName ); // access to the solver internal data extern int Msat_SolverReadVarNum( Msat_Solver_t * p ); +extern int Msat_SolverReadClauseNum( Msat_Solver_t * p ); extern int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ); extern int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ); extern int * Msat_SolverReadModelArray( Msat_Solver_t * p ); diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c index f944ed81..62b9ecad 100644 --- a/src/sat/msat/msatClause.c +++ b/src/sat/msat/msatClause.c @@ -82,6 +82,10 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, // nSeenId - 1 stands for negative // nSeenId stands for positive // Remove false literals + + // there is a bug here!!!! + // when the same var in opposite polarities is given, it drops one polarity!!! + for ( i = j = 0; i < nLits; i++ ) { // get the corresponding variable Var = MSAT_LIT2VAR(pLits[i]); @@ -190,6 +194,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, { Msat_SolverVarBumpActivity( p, pLits[i] ); // Msat_SolverVarBumpActivity( p, pLits[i] ); + p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++; } } diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index ef2375a7..3dfe2109 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -151,6 +151,7 @@ struct Msat_Solver_t_ int nSeenId; // the id of current seeing Msat_IntVec_t * vReason; // the temporary array of literals Msat_IntVec_t * vTemp; // the temporary array of literals + int * pFreq; // the number of times each var participated in conflicts // the memory manager Msat_MmStep_t * pMem; diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index dd3a5a43..4a721487 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -42,6 +42,7 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] ); ***********************************************************************/ int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; } +int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; } int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc;} int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); } int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; } diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index ed228b33..5f13694b 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -140,6 +140,9 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra int64 nConflictsOld = p->Stats.nConflicts; int64 nDecisionsOld = p->Stats.nDecisions; + p->pFreq = ALLOC( int, p->nVarsAlloc ); + memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc ); + if ( vAssumps ) { int * pAssumps, nAssumps, i; @@ -181,6 +184,23 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra } Msat_SolverCancelUntil( p, 0 ); p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks; +/* + PRT( "True solver runtime", clock() - timeStart ); + // print the statistics + { + int i, Counter = 0; + for ( i = 0; i < p->nVars; i++ ) + if ( p->pFreq[i] > 0 ) + { + printf( "%d ", p->pFreq[i] ); + Counter++; + } + if ( Counter ) + printf( "\n" ); + printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts ); + PRT( "Time", clock() - timeStart ); + } +*/ return Status; } |