diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-17 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-17 08:01:00 -0700 |
| commit | d63a0cbbfd3979bb1423946fd1853411fbc66210 (patch) | |
| tree | f3e981717d69b3f725ccbdd9a0ad70c9fe9f320e | |
| parent | 05772a795bf5808ff30008fc2a36ec965e18c50e (diff) | |
| download | abc-d63a0cbbfd3979bb1423946fd1853411fbc66210.tar.gz abc-d63a0cbbfd3979bb1423946fd1853411fbc66210.tar.bz2 abc-d63a0cbbfd3979bb1423946fd1853411fbc66210.zip | |
Version abc80717
45 files changed, 4983 insertions, 3335 deletions
@@ -14,7 +14,7 @@ MODULES := \ src/map/fpga src/map/mapper src/map/mio src/map/super \ src/map/if \ src/misc/extra src/misc/mvc src/misc/st src/misc/util \ - src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \ + src/misc/nm src/misc/vec src/misc/hash \ src/misc/bzlib src/misc/zlib \ src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/mfs \ src/opt/sim src/opt/ret src/opt/res src/opt/lpk src/opt/fret \ @@ -42,7 +42,7 @@ RSC=rc.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /FR /YX /FD /c +# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -66,7 +66,7 @@ LINK32=link.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c -# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /FR /YX /FD /GZ /c +# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c # SUBTRACT CPP /X # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" @@ -242,10 +242,6 @@ SOURCE=.\src\base\abci\abcDsd.c # End Source File # Begin Source File -SOURCE=.\src\base\abci\abcEspresso.c -# End Source File -# Begin Source File - SOURCE=.\src\base\abci\abcExtract.c # End Source File # Begin Source File @@ -1194,6 +1190,10 @@ SOURCE=.\src\sat\bsat\satInterA.c # End Source File # Begin Source File +SOURCE=.\src\sat\bsat\satInterB.c +# End Source File +# Begin Source File + SOURCE=.\src\sat\bsat\satInterP.c # End Source File # Begin Source File @@ -1940,86 +1940,10 @@ SOURCE=.\src\map\if\ifUtil.c # Begin Group "pcm" # PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\map\pcm\pcmCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\pcm\pcmCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\pcm\pcmInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\pcm\pcmMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\pcm\pcmMap.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\pcm\pcmReduce.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\pcm\pcmTime.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\pcm\pcmTruth.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\pcm\pcmUtil.c -# End Source File # End Group # Begin Group "ply" # PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\map\ply\ply.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\ply\plyAbc.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\ply\plyAig.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\ply\plyInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\ply\plyIter.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\ply\plyLib.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\ply\plyMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\ply\plyMap.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\ply\plyNtk.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\ply\plyPar.c -# End Source File # End Group # End Group # Begin Group "misc" @@ -2221,186 +2145,6 @@ SOURCE=.\src\misc\vec\vecStr.h SOURCE=.\src\misc\vec\vecVec.h # End Source File # End Group -# Begin Group "espresso" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\misc\espresso\cofactor.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cols.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\compl.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\contain.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cubehack.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cubestr.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cvrin.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cvrm.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cvrmisc.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cvrout.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\dominate.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\equiv.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\espresso.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\espresso.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\essen.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\exact.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\expand.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\gasp.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\gimpel.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\globals.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\hack.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\indep.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\irred.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\map.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\matrix.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\mincov.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\mincov.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\mincov_int.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\opo.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\pair.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\part.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\primes.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\reduce.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\rows.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\set.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\setc.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\sharp.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\sminterf.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\solution.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\sparse.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\sparse.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\sparse_int.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\unate.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\verify.c -# End Source File -# End Group # Begin Group "util" # PROP Default_Filter "" diff --git a/abclib.dsp b/abclib.dsp deleted file mode 100644 index df244f0f..00000000 --- a/abclib.dsp +++ /dev/null @@ -1,2844 +0,0 @@ -# Microsoft Developer Studio Project File - Name="abclib" - Package Owner=<4> -# Microsoft Developer Studio Generated Build File, Format Version 6.00 -# ** DO NOT EDIT ** - -# TARGTYPE "Win32 (x86) Static Library" 0x0104 - -CFG=abclib - Win32 Debug -!MESSAGE This is not a valid makefile. To build this project using NMAKE, -!MESSAGE use the Export Makefile command and run -!MESSAGE -!MESSAGE NMAKE /f "abclib.mak". -!MESSAGE -!MESSAGE You can specify a configuration when running NMAKE -!MESSAGE by defining the macro CFG on the command line. For example: -!MESSAGE -!MESSAGE NMAKE /f "abclib.mak" CFG="abclib - Win32 Debug" -!MESSAGE -!MESSAGE Possible choices for configuration are: -!MESSAGE -!MESSAGE "abclib - Win32 Release" (based on "Win32 (x86) Static Library") -!MESSAGE "abclib - Win32 Debug" (based on "Win32 (x86) Static Library") -!MESSAGE - -# Begin Project -# PROP AllowPerConfigDependencies 0 -# PROP Scc_ProjName "" -# PROP Scc_LocalPath "" -CPP=cl.exe -RSC=rc.exe - -!IF "$(CFG)" == "abclib - Win32 Release" - -# PROP BASE Use_MFC 0 -# PROP BASE Use_Debug_Libraries 0 -# PROP BASE Output_Dir "abclib___Win32_Release" -# PROP BASE Intermediate_Dir "abclib___Win32_Release" -# PROP BASE Target_Dir "" -# PROP Use_MFC 0 -# PROP Use_Debug_Libraries 0 -# PROP Output_Dir "abclib\ReleaseLib" -# PROP Intermediate_Dir "abclib\ReleaseLib" -# PROP Target_Dir "" -# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c -# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c -# ADD BASE RSC /l 0x409 /d "NDEBUG" -# ADD RSC /l 0x409 /d "NDEBUG" -BSC32=bscmake.exe -# ADD BASE BSC32 /nologo -# ADD BSC32 /nologo -LIB32=link.exe -lib -# ADD BASE LIB32 /nologo -# ADD LIB32 /nologo /out:"abclib\abclib_release.lib" - -!ELSEIF "$(CFG)" == "abclib - Win32 Debug" - -# PROP BASE Use_MFC 0 -# PROP BASE Use_Debug_Libraries 1 -# PROP BASE Output_Dir "abclib___Win32_Debug" -# PROP BASE Intermediate_Dir "abclib___Win32_Debug" -# PROP BASE Target_Dir "" -# PROP Use_MFC 0 -# PROP Use_Debug_Libraries 1 -# PROP Output_Dir "abclib\DebugLib" -# PROP Intermediate_Dir "abclib\DebugLib" -# PROP Target_Dir "" -# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /YX /FD /GZ /c -# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c -# ADD BASE RSC /l 0x409 /d "_DEBUG" -# ADD RSC /l 0x409 /d "_DEBUG" -BSC32=bscmake.exe -# ADD BASE BSC32 /nologo -# ADD BSC32 /nologo -LIB32=link.exe -lib -# ADD BASE LIB32 /nologo -# ADD LIB32 /nologo /out:"abclib\abclib_debug.lib" - -!ENDIF - -# Begin Target - -# Name "abclib - Win32 Release" -# Name "abclib - Win32 Debug" -# Begin Group "Source Files" - -# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat" -# Begin Group "base" - -# PROP Default_Filter "" -# Begin Group "abc" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\base\abc\abc.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcAig.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcBlifMv.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcCheck.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcDfs.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcFanio.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcFunc.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcHie.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcLatch.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcLib.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcMinBase.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcNames.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcNetlist.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcNtk.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcObj.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcRefs.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcShow.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcSop.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc\abcUtil.c -# End Source File -# End Group -# Begin Group "abci" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\base\abci\abc.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcAttach.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcAuto.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcBalance.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcBmc.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcCas.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcClpBdd.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcClpSop.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcDar.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcDebug.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcDress.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcDsd.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcEspresso.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcExtract.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcFpga.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcFpgaFast.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcFraig.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcFxu.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcGen.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcHaig.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcIf.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcIvy.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcLut.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcMap.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcMeasure.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcMini.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcMiter.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcMulti.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcMv.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcNtbdd.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcOdc.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcOrder.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcPart.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcPrint.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcProve.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcQbf.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcQuant.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcRec.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcReconv.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcRefactor.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcRenode.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcReorder.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcRestruct.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcResub.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcRewrite.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcRr.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcSat.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcStrash.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcSweep.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcSymm.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcTiming.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcUnate.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcUnreach.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcVerify.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abci\abcXsim.c -# End Source File -# End Group -# Begin Group "cmd" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\base\cmd\cmd.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\cmd\cmd.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\cmd\cmdAlias.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\cmd\cmdApi.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\cmd\cmdFlag.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\cmd\cmdHist.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\cmd\cmdInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\cmd\cmdUtils.c -# End Source File -# End Group -# Begin Group "io" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\base\io\io.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\io.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadAiger.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadBaf.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadBench.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadBlif.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadBlifAig.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadBlifMv.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadDsd.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadEdif.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadEqn.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadPla.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioReadVerilog.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioUtil.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteAiger.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteBaf.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteBench.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteBlif.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteBlifMv.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteCnf.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteDot.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteEqn.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteGml.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteList.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWritePla.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\io\ioWriteVerilog.c -# End Source File -# End Group -# Begin Group "main" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\base\main\libSupport.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\main\main.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\main\main.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\main\mainFrame.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\main\mainInit.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\main\mainInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\main\mainUtils.c -# End Source File -# End Group -# Begin Group "ver" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\base\ver\ver.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\ver\verCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\ver\verFormula.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\ver\verParse.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\ver\verStream.c -# End Source File -# End Group -# End Group -# Begin Group "bdd" - -# PROP Default_Filter "" -# Begin Group "cudd" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\bdd\cudd\cudd.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddAddAbs.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddAddApply.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddAddFind.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddAddInv.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddAddIte.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddAddNeg.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddAddWalsh.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddAndAbs.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddAnneal.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddApa.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddAPI.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddApprox.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddBddAbs.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddBddCorr.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddBddIte.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddBridge.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddCache.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddCheck.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddClip.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddCof.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddCompose.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddDecomp.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddEssent.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddExact.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddExport.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddGenCof.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddGenetic.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddGroup.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddHarwell.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddInit.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddInteract.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddLCache.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddLevelQ.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddLinear.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddLiteral.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddMatMult.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddPriority.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddRead.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddRef.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddReorder.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddSat.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddSign.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddSolve.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddSplit.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddSubsetHB.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddSubsetSP.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddSymmetry.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddTable.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddUtil.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddWindow.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddCount.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddFuncs.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddGroup.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddIsop.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddLin.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddMisc.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddPort.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddReord.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddSetop.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddSymm.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cudd\cuddZddUtil.c -# End Source File -# End Group -# Begin Group "epd" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\bdd\epd\epd.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\epd\epd.h -# End Source File -# End Group -# Begin Group "mtr" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\bdd\mtr\mtr.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\mtr\mtrBasic.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\mtr\mtrGroup.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\mtr\mtrInt.h -# End Source File -# End Group -# Begin Group "parse" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\bdd\parse\parse.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\parse\parseCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\parse\parseEqn.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\parse\parseInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\parse\parseStack.c -# End Source File -# End Group -# Begin Group "dsd" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\bdd\dsd\dsd.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\dsd\dsdApi.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\dsd\dsdCheck.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\dsd\dsdInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\dsd\dsdLocal.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\dsd\dsdMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\dsd\dsdProc.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\dsd\dsdTree.c -# End Source File -# End Group -# Begin Group "reo" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\bdd\reo\reo.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\reo\reoApi.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\reo\reoCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\reo\reoProfile.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\reo\reoSift.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\reo\reoSwap.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\reo\reoTest.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\reo\reoTransfer.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\reo\reoUnits.c -# End Source File -# End Group -# Begin Group "cas" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\bdd\cas\cas.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cas\casCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\cas\casDec.c -# End Source File -# End Group -# End Group -# Begin Group "sat" - -# PROP Default_Filter "" -# Begin Group "msat" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\sat\msat\msat.h -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatActivity.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatClause.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatClauseVec.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatMem.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatOrderH.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatQueue.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatRead.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatSolverApi.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatSolverCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatSolverIo.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatSolverSearch.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatSort.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\msat\msatVec.c -# End Source File -# End Group -# Begin Group "fraig" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\sat\fraig\fraig.h -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigApi.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigCanon.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigChoice.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigFanout.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigFeed.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigMem.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigNode.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigPrime.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigSat.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigTable.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigUtil.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\fraig\fraigVec.c -# End Source File -# End Group -# Begin Group "csat" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\sat\csat\csat_apis.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\csat\csat_apis.h -# End Source File -# End Group -# Begin Group "bsat" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\sat\bsat\satInter.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\bsat\satMem.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\bsat\satMem.h -# End Source File -# Begin Source File - -SOURCE=.\src\sat\bsat\satSolver.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\bsat\satSolver.h -# End Source File -# Begin Source File - -SOURCE=.\src\sat\bsat\satStore.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\bsat\satStore.h -# End Source File -# Begin Source File - -SOURCE=.\src\sat\bsat\satTrace.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\bsat\satUtil.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\bsat\satVec.h -# End Source File -# End Group -# Begin Group "proof" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\sat\proof\pr.c -# End Source File -# Begin Source File - -SOURCE=.\src\sat\proof\pr.h -# End Source File -# End Group -# End Group -# Begin Group "opt" - -# PROP Default_Filter "" -# Begin Group "fxu" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\opt\fxu\fxu.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxu.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuCreate.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuHeapD.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuHeapS.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuList.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuMatrix.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuPair.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuPrint.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuReduce.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuSelect.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuSingle.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\fxu\fxuUpdate.c -# End Source File -# End Group -# Begin Group "rwr" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\opt\rwr\rwr.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\rwr\rwrDec.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\rwr\rwrEva.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\rwr\rwrExp.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\rwr\rwrLib.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\rwr\rwrMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\rwr\rwrPrint.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\rwr\rwrTemp.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\rwr\rwrUtil.c -# End Source File -# End Group -# Begin Group "cut" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\opt\cut\cut.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutApi.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutExpand.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutList.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutMerge.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutNode.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutOracle.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutPre22.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutSeq.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\cut\cutTruth.c -# End Source File -# End Group -# Begin Group "dec" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\opt\dec\dec.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\dec\decAbc.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\dec\decFactor.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\dec\decMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\dec\decPrint.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\dec\decUtil.c -# End Source File -# End Group -# Begin Group "sim" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\opt\sim\sim.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\sim\simMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\sim\simSat.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\sim\simSeq.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\sim\simSupp.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\sim\simSwitch.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\sim\simSym.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\sim\simSymSat.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\sim\simSymSim.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\sim\simSymStr.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\sim\simUtils.c -# End Source File -# End Group -# Begin Group "ret" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\opt\ret\retArea.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\ret\retCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\ret\retDelay.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\ret\retFlow.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\ret\retIncrem.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\ret\retInit.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\ret\retInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\ret\retLvalue.c -# End Source File -# End Group -# Begin Group "res" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\opt\res\res.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\res\resCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\res\resDivs.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\res\resFilter.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\res\resInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\res\resSat.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\res\resSim.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\res\resStrash.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\res\resWin.c -# End Source File -# End Group -# Begin Group "lpk" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\opt\lpk\lpk.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkAbcDec.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkAbcDsd.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkAbcMux.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkAbcUtil.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkMap.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkMulti.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkMux.c -# End Source File -# Begin Source File - -SOURCE=.\src\opt\lpk\lpkSets.c -# End Source File -# End Group -# End Group -# Begin Group "map" - -# PROP Default_Filter "" -# Begin Group "fpga" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\map\fpga\fpga.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpga.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaCreate.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaCutUtils.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaFanout.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaLib.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaMatch.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaSwitch.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaTime.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaTruth.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaUtils.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\fpga\fpgaVec.c -# End Source File -# End Group -# Begin Group "mapper" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\map\mapper\mapper.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapper.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperCanon.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperCreate.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperCutUtils.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperFanout.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperLib.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperMatch.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperRefs.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperSuper.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperSwitch.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperTable.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperTime.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperTree.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperTruth.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperUtils.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mapper\mapperVec.c -# End Source File -# End Group -# Begin Group "mio" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\map\mio\mio.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mio\mio.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\mio\mioApi.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mio\mioFunc.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mio\mioInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\mio\mioRead.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\mio\mioUtils.c -# End Source File -# End Group -# Begin Group "super" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\map\super\super.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\super\super.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\super\superAnd.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\super\superGate.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\super\superInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\super\superWrite.c -# End Source File -# End Group -# Begin Group "if" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\map\if\if.h -# End Source File -# Begin Source File - -SOURCE=.\src\map\if\ifCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\if\ifCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\if\ifMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\if\ifMap.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\if\ifReduce.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\if\ifSeq.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\if\ifTime.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\if\ifTruth.c -# End Source File -# Begin Source File - -SOURCE=.\src\map\if\ifUtil.c -# End Source File -# End Group -# End Group -# Begin Group "misc" - -# PROP Default_Filter "" -# Begin Group "extra" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\misc\extra\extra.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddAuto.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddCas.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddKmap.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddMisc.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddSymm.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddUnate.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraUtilBitMatrix.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraUtilCanon.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraUtilFile.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraUtilMemory.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraUtilMisc.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraUtilProgress.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraUtilReader.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraUtilTruth.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraUtilUtil.c -# End Source File -# End Group -# Begin Group "st" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\misc\st\st.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\st\st.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\st\stmm.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\st\stmm.h -# End Source File -# End Group -# Begin Group "util" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\misc\util\util_hack.h -# End Source File -# End Group -# Begin Group "mvc" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\misc\mvc\mvc.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvc.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcApi.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcCompare.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcContain.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcCover.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcCube.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcDivide.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcDivisor.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcList.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcLits.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcOpAlg.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcOpBool.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcPrint.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcSort.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\mvc\mvcUtils.c -# End Source File -# End Group -# Begin Group "vec" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\misc\vec\vec.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\vec\vecAtt.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\vec\vecFlt.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\vec\vecInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\vec\vecPtr.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\vec\vecStr.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\vec\vecVec.h -# End Source File -# End Group -# Begin Group "espresso" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\misc\espresso\cofactor.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cols.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\compl.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\contain.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cubehack.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cubestr.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cvrin.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cvrm.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cvrmisc.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\cvrout.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\dominate.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\equiv.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\espresso.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\espresso.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\essen.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\exact.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\expand.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\gasp.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\gimpel.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\globals.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\hack.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\indep.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\irred.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\map.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\matrix.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\mincov.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\mincov.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\mincov_int.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\opo.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\pair.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\part.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\primes.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\reduce.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\rows.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\set.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\setc.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\sharp.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\sminterf.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\solution.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\sparse.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\sparse.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\sparse_int.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\unate.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\util_old.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\espresso\verify.c -# End Source File -# End Group -# Begin Group "nm" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\misc\nm\nm.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\nm\nmApi.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\nm\nmInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\nm\nmTable.c -# End Source File -# End Group -# Begin Group "hash" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\misc\hash\hash.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\hash\hashFlt.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\hash\hashInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\hash\hashPtr.h -# End Source File -# End Group -# End Group -# Begin Group "ai" - -# PROP Default_Filter "" -# Begin Group "hop" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\hop\hop.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\hop\hopBalance.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\hop\hopCheck.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\hop\hopDfs.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\hop\hopMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\hop\hopMem.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\hop\hopObj.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\hop\hopOper.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\hop\hopTable.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\hop\hopUtil.c -# End Source File -# End Group -# Begin Group "ivy" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\ivy\ivy.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyBalance.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyCanon.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyCheck.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyCutTrav.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyDfs.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyDsd.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyFanout.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyFastMap.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyFraig.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyHaig.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyMem.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyMulti.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyObj.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyOper.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyResyn.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyRwr.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivySeq.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyShow.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyTable.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ivy\ivyUtil.c -# End Source File -# End Group -# Begin Group "rwt" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\rwt\rwt.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\rwt\rwtDec.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\rwt\rwtMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\rwt\rwtUtil.c -# End Source File -# End Group -# Begin Group "deco" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\deco\deco.h -# End Source File -# End Group -# Begin Group "mem" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\mem\mem.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\mem\mem.h -# End Source File -# End Group -# Begin Group "ioa" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\ioa\ioa.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ioa\ioaReadAig.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ioa\ioaUtil.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\ioa\ioaWriteAig.c -# End Source File -# End Group -# Begin Group "dar" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\dar\dar.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darBalance.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darData.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darLib.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darPrec.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darRefact.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darResub.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\dar\darScript.c -# End Source File -# End Group -# Begin Group "fra" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\fra\fra.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraBmc.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraCec.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraClass.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraCnf.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraImp.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraInd.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraLcr.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraPart.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraSat.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraSec.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\fra\fraSim.c -# End Source File -# End Group -# Begin Group "cnf" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\cnf\cnf.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\cnf\cnfCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\cnf\cnfCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\cnf\cnfData.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\cnf\cnfMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\cnf\cnfMap.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\cnf\cnfPost.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\cnf\cnfUtil.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\cnf\cnfWrite.c -# End Source File -# End Group -# Begin Group "csw" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\csw\csw.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\csw\cswCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\csw\cswCut.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\csw\cswInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\csw\cswMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\csw\cswTable.c -# End Source File -# End Group -# Begin Group "kit" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\kit\cloud.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\cloud.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kit.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kitAig.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kitBdd.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kitCloud.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kitDsd.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kitFactor.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kitGraph.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kitHop.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kitIsop.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kitSop.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\kit\kitTruth.c -# End Source File -# End Group -# Begin Group "bdc" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\bdc\bdc.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\bdc\bdcCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\bdc\bdcDec.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\bdc\bdcInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\bdc\bdcTable.c -# End Source File -# End Group -# Begin Group "aig" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\aig\aig.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigCheck.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigDfs.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigFanout.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigMem.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigMffc.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigObj.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigOper.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigOrder.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigPart.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigRepr.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigRet.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigScl.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigSeq.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigShow.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigTable.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigTime.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigTiming.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigTruth.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigTsim.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigUtil.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\aig\aigWin.c -# End Source File -# End Group -# Begin Group "bar" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\bar\bar.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\bar\bar.h -# End Source File -# End Group -# End Group -# End Group -# Begin Group "Header Files" - -# PROP Default_Filter "h;hpp;hxx;hm;inl" -# End Group -# End Target -# End Project diff --git a/abclib.dsw b/abclib.dsw deleted file mode 100644 index 260ade17..00000000 --- a/abclib.dsw +++ /dev/null @@ -1,29 +0,0 @@ -Microsoft Developer Studio Workspace File, Format Version 6.00 -# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE! - -############################################################################### - -Project: "abclib"=.\abclib.dsp - Package Owner=<4> - -Package=<5> -{{{ -}}} - -Package=<4> -{{{ -}}} - -############################################################################### - -Global: - -Package=<5> -{{{ -}}} - -Package=<3> -{{{ -}}} - -############################################################################### - diff --git a/abctestlib.dsp b/abctestlib.dsp deleted file mode 100644 index e901cbda..00000000 --- a/abctestlib.dsp +++ /dev/null @@ -1,102 +0,0 @@ -# Microsoft Developer Studio Project File - Name="abctestlib" - Package Owner=<4> -# Microsoft Developer Studio Generated Build File, Format Version 6.00 -# ** DO NOT EDIT ** - -# TARGTYPE "Win32 (x86) Console Application" 0x0103 - -CFG=abctestlib - Win32 Debug -!MESSAGE This is not a valid makefile. To build this project using NMAKE, -!MESSAGE use the Export Makefile command and run -!MESSAGE -!MESSAGE NMAKE /f "abctestlib.mak". -!MESSAGE -!MESSAGE You can specify a configuration when running NMAKE -!MESSAGE by defining the macro CFG on the command line. For example: -!MESSAGE -!MESSAGE NMAKE /f "abctestlib.mak" CFG="abctestlib - Win32 Debug" -!MESSAGE -!MESSAGE Possible choices for configuration are: -!MESSAGE -!MESSAGE "abctestlib - Win32 Release" (based on "Win32 (x86) Console Application") -!MESSAGE "abctestlib - Win32 Debug" (based on "Win32 (x86) Console Application") -!MESSAGE - -# Begin Project -# PROP AllowPerConfigDependencies 0 -# PROP Scc_ProjName "" -# PROP Scc_LocalPath "" -CPP=cl.exe -RSC=rc.exe - -!IF "$(CFG)" == "abctestlib - Win32 Release" - -# PROP BASE Use_MFC 0 -# PROP BASE Use_Debug_Libraries 0 -# PROP BASE Output_Dir "Release" -# PROP BASE Intermediate_Dir "Release" -# PROP BASE Target_Dir "" -# PROP Use_MFC 0 -# PROP Use_Debug_Libraries 0 -# PROP Output_Dir "Release" -# PROP Intermediate_Dir "Release" -# PROP Ignore_Export_Lib 0 -# PROP Target_Dir "" -# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD BASE RSC /l 0x409 /d "NDEBUG" -# ADD RSC /l 0x409 /d "NDEBUG" -BSC32=bscmake.exe -# ADD BASE BSC32 /nologo -# ADD BSC32 /nologo -LINK32=link.exe -# ADD BASE LINK32 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 /machine:I386 -# ADD LINK32 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 C:\_projects\abc\abclib\abclib_release.lib /nologo /subsystem:console /machine:I386 /out:"_TEST/abctestlib.exe" - -!ELSEIF "$(CFG)" == "abctestlib - Win32 Debug" - -# PROP BASE Use_MFC 0 -# PROP BASE Use_Debug_Libraries 1 -# PROP BASE Output_Dir "Debug" -# PROP BASE Intermediate_Dir "Debug" -# PROP BASE Target_Dir "" -# PROP Use_MFC 0 -# PROP Use_Debug_Libraries 1 -# PROP Output_Dir "Debug" -# PROP Intermediate_Dir "Debug" -# PROP Ignore_Export_Lib 0 -# PROP Target_Dir "" -# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c -# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /FR /YX /FD /GZ /c -# ADD BASE RSC /l 0x409 /d "_DEBUG" -# ADD RSC /l 0x409 /d "_DEBUG" -BSC32=bscmake.exe -# ADD BASE BSC32 /nologo -# ADD BSC32 /nologo -LINK32=link.exe -# ADD BASE LINK32 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 /debug /machine:I386 /pdbtype:sept -# ADD LINK32 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 C:\_projects\abc\abclib\abclib_debug.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abctestlib.exe" /pdbtype:sept - -!ENDIF - -# Begin Target - -# Name "abctestlib - Win32 Release" -# Name "abctestlib - Win32 Debug" -# Begin Group "Source Files" - -# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat" -# Begin Source File - -SOURCE=.\demo.c -# End Source File -# End Group -# Begin Group "Header Files" - -# PROP Default_Filter "h;hpp;hxx;hm;inl" -# End Group -# Begin Group "Resource Files" - -# PROP Default_Filter "ico;cur;bmp;dlg;rc2;rct;bin;rgs;gif;jpg;jpeg;jpe" -# End Group -# End Target -# End Project diff --git a/abctestlib.dsw b/abctestlib.dsw deleted file mode 100644 index 7ae6cac9..00000000 --- a/abctestlib.dsw +++ /dev/null @@ -1,29 +0,0 @@ -Microsoft Developer Studio Workspace File, Format Version 6.00 -# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE! - -############################################################################### - -Project: "abctestlib"=.\abctestlib.dsp - Package Owner=<4> - -Package=<5> -{{{ -}}} - -Package=<4> -{{{ -}}} - -############################################################################### - -Global: - -Package=<5> -{{{ -}}} - -Package=<3> -{{{ -}}} - -############################################################################### - diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 96aa1c93..93ca298a 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -505,6 +505,7 @@ extern int Aig_ManPoCleanup( Aig_Man_t * p ); extern void Aig_ManPrintStats( Aig_Man_t * p ); extern void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew ); extern void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs ); +extern void Aig_ManFlipFirstPo( Aig_Man_t * p ); /*=== aigMem.c ==========================================================*/ extern void Aig_ManStartMemory( Aig_Man_t * p ); extern void Aig_ManStopMemory( Aig_Man_t * p ); diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index dae7e42b..a1c3eb01 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -433,6 +433,23 @@ void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs ) p->nTruePos = Aig_ManPoNum(p) - nRegs; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManFlipFirstPo( Aig_Man_t * p ) +{ + Aig_ObjChild0Flip( Aig_ManPo(p, 0) ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index e3e6bfe1..f1c446fe 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -238,26 +238,26 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ) SeeAlso [] ***********************************************************************/ -void Cnf_DataWriteIntoFile_old( Cnf_Dat_t * p, char * pFileName, int fReadable ) +void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable ) { - FILE * pFile; + gzFile pFile; int * pLit, * pStop, i; - pFile = fopen( pFileName, "w" ); + pFile = gzopen( pFileName, "wb" ); if ( pFile == NULL ) { printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" ); return; } - fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); - fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); + gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); + gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); for ( i = 0; i < p->nClauses; i++ ) { for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) - fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); - fprintf( pFile, "0\n" ); + gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); + gzprintf( pFile, "0\n" ); } - fprintf( pFile, "\n" ); - fclose( pFile ); + gzprintf( pFile, "\n" ); + gzclose( pFile ); } /**Function************************************************************* @@ -273,24 +273,29 @@ void Cnf_DataWriteIntoFile_old( Cnf_Dat_t * p, char * pFileName, int fReadable ) ***********************************************************************/ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) { - gzFile pFile; + FILE * pFile; int * pLit, * pStop, i; - pFile = gzopen( pFileName, "wb" ); + if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) ) + { + Cnf_DataWriteIntoFileGz( p, pFileName, fReadable ); + return; + } + pFile = fopen( pFileName, "w" ); if ( pFile == NULL ) { printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" ); return; } - gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); - gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); + fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); + fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); for ( i = 0; i < p->nClauses; i++ ) { for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) - gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); - gzprintf( pFile, "0\n" ); + fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); + fprintf( pFile, "0\n" ); } - gzprintf( pFile, "\n" ); - gzclose( pFile ); + fprintf( pFile, "\n" ); + fclose( pFile ); } /**Function************************************************************* diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 96c0de77..3365ac9a 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -389,11 +389,11 @@ PRT( "Time", clock() - clkTotal ); clk = clock(); if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 ) { - extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth ); + extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose, int * pDepth ); int Depth; pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); - RetValue = Saig_Interpolate( pNew, 5000, 0, 1, pParSec->fVeryVerbose, &Depth ); + RetValue = Saig_Interpolate( pNew, 5000, 0, 1, 0, pParSec->fVeryVerbose, &Depth ); if ( pParSec->fVerbose ) { if ( RetValue == 1 ) diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index 105f4c4a..6eb2cc95 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -876,6 +876,8 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine ) p->pNtk->attrWhite = 0; else if ( strcmp( pToken, "box" ) == 0 ) p->pNtk->attrBox = 1; + else if ( strcmp( pToken, "logic" ) == 0 ) + p->pNtk->attrBox = 0; else if ( strcmp( pToken, "white" ) == 0 ) p->pNtk->attrWhite = 1; else if ( strcmp( pToken, "comb" ) == 0 ) diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h index e3d0a061..222130f3 100644 --- a/src/aig/nwk/nwk.h +++ b/src/aig/nwk/nwk.h @@ -24,7 +24,7 @@ #ifdef __cplusplus extern "C" { #endif - + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -86,7 +86,10 @@ struct Nwk_Obj_t_ Nwk_Man_t * pMan; // the manager Hop_Obj_t * pFunc; // functionality void * pCopy; // temporary pointer - void * pNext; // temporary pointer + union { + void * pNext; // temporary pointer + int iTemp; // temporary number + }; // node information unsigned Type : 3; // object type unsigned fInvert : 1; // complemented attribute diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c index d9a41849..252546e8 100644 --- a/src/aig/nwk/nwkMan.c +++ b/src/aig/nwk/nwkMan.c @@ -153,7 +153,7 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl ) ParsBest.Nodes = ParsNew.Nodes; ParsBest.nPis = ParsNew.nPis; ParsBest.nPos = ParsNew.nPos; - // writ the network + // write the network Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" ); // Nwk_ManDumpBlif( pNtk, "best_map.blif", NULL, NULL ); return 1; diff --git a/src/aig/nwk/nwkMerge.c b/src/aig/nwk/nwkMerge.c index 1a5255d3..531bc1c0 100644 --- a/src/aig/nwk/nwkMerge.c +++ b/src/aig/nwk/nwkMerge.c @@ -348,6 +348,45 @@ void Nwk_ManGraphPrepare( Nwk_Grf_t * p ) /**Function************************************************************* + Synopsis [Sort pairs by the first vertex in the topological order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphSortPairs( Nwk_Grf_t * p ) +{ + int nSize = Vec_IntSize(p->vPairs); + int * pIdToPair, i; + // allocate storage + pIdToPair = ALLOC( int, p->nObjs+1 ); + for ( i = 0; i <= p->nObjs; i++ ) + pIdToPair[i] = -1; + // create mapping + for ( i = 0; i < p->vPairs->nSize; i += 2 ) + { + assert( pIdToPair[ p->vPairs->pArray[i] ] == -1 ); + pIdToPair[ p->vPairs->pArray[i] ] = p->vPairs->pArray[i+1]; + } + // recreate pairs + Vec_IntClear( p->vPairs ); + for ( i = 0; i <= p->nObjs; i++ ) + if ( pIdToPair[i] >= 0 ) + { + assert( i < pIdToPair[i] ); + Vec_IntPush( p->vPairs, i ); + Vec_IntPush( p->vPairs, pIdToPair[i] ); + } + assert( nSize == Vec_IntSize(p->vPairs) ); + free( pIdToPair ); +} + + +/**Function************************************************************* + Synopsis [Updates the problem after pulling out one edge.] Description [] @@ -615,6 +654,7 @@ void Nwk_ManGraphSolve( Nwk_Grf_t * p ) if ( j == NWK_MAX_LIST + 1 ) break; } + Nwk_ManGraphSortPairs( p ); } /**Function************************************************************* @@ -982,6 +1022,9 @@ Vec_Int_t * Nwk_ManLutMerge( Nwk_Man_t * pNtk, Nwk_LMPars_t * pPars ) Nwk_ManGraphReportMemoryUsage( p ); } vResult = p->vPairs; p->vPairs = NULL; + for ( i = 0; i < vResult->nSize; i += 2 ) + printf( "(%d,%d) ", vResult->pArray[i], vResult->pArray[i+1] ); + printf( "\n" ); Nwk_ManGraphFree( p ); return vResult; } diff --git a/src/aig/nwk2/module.make b/src/aig/nwk2/module.make new file mode 100644 index 00000000..226a68ef --- /dev/null +++ b/src/aig/nwk2/module.make @@ -0,0 +1,7 @@ +SRC += src/aig/nwk/nwkCheck.c \ + src/aig/nwk/nwkDfs.c \ + src/aig/nwk/nwkFanio.c \ + src/aig/nwk/nwkMan.c \ + src/aig/nwk/nwkMerge.c \ + src/aig/nwk/nwkObj.c \ + src/aig/nwk/nwkUtil.c diff --git a/src/aig/nwk2/nwk.h b/src/aig/nwk2/nwk.h new file mode 100644 index 00000000..465bd651 --- /dev/null +++ b/src/aig/nwk2/nwk.h @@ -0,0 +1,278 @@ +/**CFile**************************************************************** + + FileName [nwk.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Logic network representation.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwk.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $] + +***********************************************************************/ + +#ifndef __NWK_H__ +#define __NWK_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig.h" +#include "hop.h" +#include "tim.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Nwk_Man_t_ Nwk_Man_t; +typedef struct Nwk_Obj_t_ Nwk_Obj_t; + +// object types +typedef enum { + NWK_OBJ_NONE, // 0: non-existant object + NWK_OBJ_CI, // 1: combinational input + NWK_OBJ_CO, // 2: combinational output + NWK_OBJ_NODE, // 3: logic node + NWK_OBJ_LATCH, // 4: register + NWK_OBJ_VOID // 5: unused object +} Nwk_Type_t; + +struct Nwk_Man_t_ +{ + // models of this design + char * pName; // the name of this design + char * pSpec; // the name of input file + // node representation + Vec_Ptr_t * vCis; // the primary inputs of the extracted part + Vec_Ptr_t * vCos; // the primary outputs of the extracted part + Vec_Ptr_t * vObjs; // the objects in the topological order + int nObjs[NWK_OBJ_VOID]; // counter of objects of each type + int nFanioPlus; // the number of extra fanins/fanouts alloc by default + // functionality, timing, memory, etc + Hop_Man_t * pManHop; // the functionality representation + Tim_Man_t * pManTime; // the timing manager +// If_Lib_t * pLutLib; // the LUT library + Aig_MmFlex_t * pMemObjs; // memory for objects + Vec_Ptr_t * vTemp; // array used for incremental updates + int nTravIds; // the counter of traversal IDs + int nRealloced; // the number of realloced nodes + // sequential information + int nLatches; // the total number of latches + int nTruePis; // the number of true primary inputs + int nTruePos; // the number of true primary outputs +}; + +struct Nwk_Obj_t_ +{ + Nwk_Man_t * pMan; // the manager + Hop_Obj_t * pFunc; // functionality + void * pCopy; // temporary pointer + union { + void * pNext; // temporary pointer + int iTemp; // temporary number + }; + // node information + unsigned Type : 3; // object type + unsigned fInvert : 1; // complemented attribute + unsigned MarkA : 1; // temporary mark + unsigned MarkB : 1; // temporary mark + unsigned MarkC : 1; // temporary mark + unsigned PioId : 25; // number of this node in the PI/PO list + int Id; // unique ID + int TravId; // traversal ID + // timing information + int Level; // the topological level + float tArrival; // the arrival time + float tRequired; // the required time + float tSlack; // the slack + // fanin/fanout representation + int nFanins; // the number of fanins + int nFanouts; // the number of fanouts + int nFanioAlloc; // the number of allocated fanins/fanouts + Nwk_Obj_t ** pFanio; // fanins/fanouts +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// INLINED FUNCTIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Nwk_ManCiNum( Nwk_Man_t * p ) { return p->nObjs[NWK_OBJ_CI]; } +static inline int Nwk_ManCoNum( Nwk_Man_t * p ) { return p->nObjs[NWK_OBJ_CO]; } +static inline int Nwk_ManNodeNum( Nwk_Man_t * p ) { return p->nObjs[NWK_OBJ_NODE]; } +static inline int Nwk_ManLatchNum( Nwk_Man_t * p ) { return p->nObjs[NWK_OBJ_LATCH]; } +static inline int Nwk_ManObjNumMax( Nwk_Man_t * p ) { return Vec_PtrSize(p->vObjs); } + +static inline Nwk_Obj_t * Nwk_ManCi( Nwk_Man_t * p, int i ) { return (Nwk_Obj_t *)Vec_PtrEntry( p->vCis, i ); } +static inline Nwk_Obj_t * Nwk_ManCo( Nwk_Man_t * p, int i ) { return (Nwk_Obj_t *)Vec_PtrEntry( p->vCos, i ); } +static inline Nwk_Obj_t * Nwk_ManObj( Nwk_Man_t * p, int i ) { return (Nwk_Obj_t *)Vec_PtrEntry( p->vObjs, i ); } + +static inline int Nwk_ObjId( Nwk_Obj_t * p ) { return p->Id; } +static inline int Nwk_ObjPioNum( Nwk_Obj_t * p ) { return p->PioId; } +static inline int Nwk_ObjFaninNum( Nwk_Obj_t * p ) { return p->nFanins; } +static inline int Nwk_ObjFanoutNum( Nwk_Obj_t * p ) { return p->nFanouts; } + +static inline Nwk_Obj_t * Nwk_ObjFanin0( Nwk_Obj_t * p ) { return p->pFanio[0]; } +static inline Nwk_Obj_t * Nwk_ObjFanout0( Nwk_Obj_t * p ) { return p->pFanio[p->nFanins]; } +static inline Nwk_Obj_t * Nwk_ObjFanin( Nwk_Obj_t * p, int i ) { return p->pFanio[i]; } +static inline Nwk_Obj_t * Nwk_ObjFanout( Nwk_Obj_t * p, int i ) { return p->pFanio[p->nFanins+1]; } + +static inline int Nwk_ObjIsNone( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_NONE; } +static inline int Nwk_ObjIsCi( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_CI; } +static inline int Nwk_ObjIsCo( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_CO; } +static inline int Nwk_ObjIsNode( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_NODE; } +static inline int Nwk_ObjIsLatch( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_LATCH; } +static inline int Nwk_ObjIsPi( Nwk_Obj_t * p ) { return Nwk_ObjIsCi(p) && (p->pMan->pManTime == NULL || Tim_ManBoxForCi(p->pMan->pManTime, p->PioId) == -1); } +static inline int Nwk_ObjIsPo( Nwk_Obj_t * p ) { return Nwk_ObjIsCo(p) && (p->pMan->pManTime == NULL || Tim_ManBoxForCo(p->pMan->pManTime, p->PioId) == -1); } +static inline int Nwk_ObjIsLi( Nwk_Obj_t * p ) { return p->pMan->nTruePos && Nwk_ObjIsCo(p) && (int)p->PioId >= p->pMan->nTruePos; } +static inline int Nwk_ObjIsLo( Nwk_Obj_t * p ) { return p->pMan->nTruePis && Nwk_ObjIsCi(p) && (int)p->PioId >= p->pMan->nTruePis; } + +static inline float Nwk_ObjArrival( Nwk_Obj_t * pObj ) { return pObj->tArrival; } +static inline float Nwk_ObjRequired( Nwk_Obj_t * pObj ) { return pObj->tRequired; } +static inline float Nwk_ObjSlack( Nwk_Obj_t * pObj ) { return pObj->tSlack; } +static inline void Nwk_ObjSetArrival( Nwk_Obj_t * pObj, float Time ) { pObj->tArrival = Time; } +static inline void Nwk_ObjSetRequired( Nwk_Obj_t * pObj, float Time ) { pObj->tRequired = Time; } +static inline void Nwk_ObjSetSlack( Nwk_Obj_t * pObj, float Time ) { pObj->tSlack = Time; } + +static inline int Nwk_ObjLevel( Nwk_Obj_t * pObj ) { return pObj->Level; } +static inline void Nwk_ObjSetLevel( Nwk_Obj_t * pObj, int Level ) { pObj->Level = Level; } + +static inline void Nwk_ObjSetTravId( Nwk_Obj_t * pObj, int TravId ) { pObj->TravId = TravId; } +static inline void Nwk_ObjSetTravIdCurrent( Nwk_Obj_t * pObj ) { pObj->TravId = pObj->pMan->nTravIds; } +static inline void Nwk_ObjSetTravIdPrevious( Nwk_Obj_t * pObj ) { pObj->TravId = pObj->pMan->nTravIds - 1; } +static inline int Nwk_ObjIsTravIdCurrent( Nwk_Obj_t * pObj ) { return pObj->TravId == pObj->pMan->nTravIds; } +static inline int Nwk_ObjIsTravIdPrevious( Nwk_Obj_t * pObj ) { return pObj->TravId == pObj->pMan->nTravIds - 1; } + +static inline int Nwk_ManTimeEqual( float f1, float f2, float Eps ) { return (f1 < f2 + Eps) && (f2 < f1 + Eps); } +static inline int Nwk_ManTimeLess( float f1, float f2, float Eps ) { return (f1 < f2 + Eps); } +static inline int Nwk_ManTimeMore( float f1, float f2, float Eps ) { return (f1 + Eps > f2); } + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +#define Nwk_ManForEachCi( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vCis, pObj, i ) +#define Nwk_ManForEachCo( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vCos, pObj, i ) +#define Nwk_ManForEachPi( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vCis, pObj, i ) \ + if ( !Nwk_ObjIsPi(pObj) ) {} else +#define Nwk_ManForEachPo( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vCos, pObj, i ) \ + if ( !Nwk_ObjIsPo(pObj) ) {} else +#define Nwk_ManForEachObj( p, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(p->vObjs)) && (((pObj) = Vec_PtrEntry(p->vObjs, i)), 1); i++ ) \ + if ( pObj == NULL ) {} else +#define Nwk_ManForEachNode( p, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(p->vObjs)) && (((pObj) = Vec_PtrEntry(p->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Nwk_ObjIsNode(pObj) ) {} else +#define Nwk_ManForEachLatch( p, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(p->vObjs)) && (((pObj) = Vec_PtrEntry(p->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Nwk_ObjIsLatch(pObj) ) {} else + +#define Nwk_ObjForEachFanin( pObj, pFanin, i ) \ + for ( i = 0; (i < (int)(pObj)->nFanins) && ((pFanin) = (pObj)->pFanio[i]); i++ ) +#define Nwk_ObjForEachFanout( pObj, pFanout, i ) \ + for ( i = 0; (i < (int)(pObj)->nFanouts) && ((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]); i++ ) + +// sequential iterators +#define Nwk_ManForEachPiSeq( p, pObj, i ) \ + Vec_PtrForEachEntryStop( p->vCis, pObj, i, (p)->nTruePis ) +#define Nwk_ManForEachPoSeq( p, pObj, i ) \ + Vec_PtrForEachEntryStop( p->vCos, pObj, i, (p)->nTruePos ) +#define Nwk_ManForEachLoSeq( p, pObj, i ) \ + for ( i = 0; (i < (p)->nLatches) && (((pObj) = Vec_PtrEntry(p->vCis, i+(p)->nTruePis)), 1); i++ ) +#define Nwk_ManForEachLiSeq( p, pObj, i ) \ + for ( i = 0; (i < (p)->nLatches) && (((pObj) = Vec_PtrEntry(p->vCos, i+(p)->nTruePos)), 1); i++ ) +#define Nwk_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) \ + for ( i = 0; (i < (p)->nLatches) && (((pObjLi) = Nwk_ManCo(p, i+(p)->nTruePos)), 1) \ + && (((pObjLo) = Nwk_ManCi(p, i+(p)->nTruePis)), 1); i++ ) + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== nwkCheck.c ==========================================================*/ +extern int Nwk_ManCheck( Nwk_Man_t * p ); +/*=== nwkDfs.c ==========================================================*/ +extern int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk ); +extern int Nwk_ManLevelBackup( Nwk_Man_t * pNtk ); +extern int Nwk_ManLevel( Nwk_Man_t * pNtk ); +extern int Nwk_ManLevelMax( Nwk_Man_t * pNtk ); +extern Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk ); +extern Vec_Ptr_t * Nwk_ManDfs( Nwk_Man_t * pNtk ); +extern Vec_Ptr_t * Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes ); +extern Vec_Ptr_t * Nwk_ManDfsReverse( Nwk_Man_t * pNtk ); +extern Vec_Ptr_t * Nwk_ManSupportNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes ); +extern void Nwk_ManSupportSum( Nwk_Man_t * pNtk ); +extern int Nwk_ObjMffcLabel( Nwk_Obj_t * pNode ); +/*=== nwkFanio.c ==========================================================*/ +extern void Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes ); +extern void Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes ); +extern int Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ); +extern int Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout ); +extern void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ); +extern void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ); +extern void Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew ); +extern void Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo ); +extern void Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew ); +/*=== nwkMan.c ============================================================*/ +extern Nwk_Man_t * Nwk_ManAlloc(); +extern void Nwk_ManFree( Nwk_Man_t * p ); +//extern void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl ); +/*=== nwkObj.c ============================================================*/ +extern Nwk_Obj_t * Nwk_ManCreateCi( Nwk_Man_t * pMan, int nFanouts ); +extern Nwk_Obj_t * Nwk_ManCreateCo( Nwk_Man_t * pMan ); +extern Nwk_Obj_t * Nwk_ManCreateNode( Nwk_Man_t * pMan, int nFanins, int nFanouts ); +extern Nwk_Obj_t * Nwk_ManCreateBox( Nwk_Man_t * pMan, int nFanins, int nFanouts ); +extern Nwk_Obj_t * Nwk_ManCreateLatch( Nwk_Man_t * pMan ); +extern void Nwk_ManDeleteNode( Nwk_Obj_t * pObj ); +extern void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj ); +/*=== nwkUtil.c ============================================================*/ +extern void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk ); +extern int Nwk_ManGetFaninMax( Nwk_Man_t * pNtk ); +extern int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk ); +extern int Nwk_ManPiNum( Nwk_Man_t * pNtk ); +extern int Nwk_ManPoNum( Nwk_Man_t * pNtk ); +extern int Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk ); +extern int Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 ); +extern int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 ); +extern void Nwk_ObjPrint( Nwk_Obj_t * pObj ); +extern void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames ); +extern void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk ); +extern void Nwk_ManCleanMarks( Nwk_Man_t * pNtk ); +extern void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/nwk2/nwkCheck.c b/src/aig/nwk2/nwkCheck.c new file mode 100644 index 00000000..6922e439 --- /dev/null +++ b/src/aig/nwk2/nwkCheck.c @@ -0,0 +1,73 @@ +/**CFile**************************************************************** + + FileName [nwkCheck.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Logic network representation.] + + Synopsis [Consistency checking procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwkCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "nwk.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checking the logic network for consistency.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManCheck( Nwk_Man_t * p ) +{ + Nwk_Obj_t * pObj; + int i, k, m; + // check if the nodes have duplicated fanins + Nwk_ManForEachNode( p, pObj, i ) + { + for ( k = 0; k < pObj->nFanins; k++ ) + for ( m = k + 1; m < pObj->nFanins; m++ ) + if ( pObj->pFanio[k] == pObj->pFanio[m] ) + printf( "Node %d has duplicated fanin %d.\n", pObj->Id, pObj->pFanio[k]->Id ); + } +/* + // check if all nodes are in the correct fanin/fanout relationship + Nwk_ManForEachObj( p, pObj, i ) + { + Nwk_ObjForEachFanin( pObj, pNext, k ) + if ( Nwk_ObjFindFanout( pNext, pObj ) == -1 ) + printf( "Nwk_ManCheck(): Object %d has fanin %d which does not have a corresponding fanout.\n", pObj->Id, pNext->Id ); + Nwk_ObjForEachFanout( pObj, pNext, k ) + if ( Nwk_ObjFindFanin( pNext, pObj ) == -1 ) + printf( "Nwk_ManCheck(): Object %d has fanout %d which does not have a corresponding fanin.\n", pObj->Id, pNext->Id ); + } +*/ + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/nwk2/nwkDfs.c b/src/aig/nwk2/nwkDfs.c new file mode 100644 index 00000000..c1c77349 --- /dev/null +++ b/src/aig/nwk2/nwkDfs.c @@ -0,0 +1,659 @@ +/**CFile**************************************************************** + + FileName [nwkDfs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Logic network representation.] + + Synopsis [DFS traversals.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwkDfs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "nwk.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Verifies that the objects are in a topo order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pObj, * pNext; + int i, k, iBox, iTerm1, nTerms; + Nwk_ManIncrementTravId( pNtk ); + Nwk_ManForEachObj( pNtk, pObj, i ) + { + if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) ) + { + Nwk_ObjForEachFanin( pObj, pNext, k ) + { + if ( !Nwk_ObjIsTravIdCurrent(pNext) ) + { + printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id ); + return 0; + } + } + } + else if ( Nwk_ObjIsCi(pObj) ) + { + if ( pNtk->pManTime ) + { + iBox = Tim_ManBoxForCi( pNtk->pManTime, pObj->PioId ); + if ( iBox >= 0 ) // this is not a true PI + { + iTerm1 = Tim_ManBoxInputFirst( pNtk->pManTime, iBox ); + nTerms = Tim_ManBoxInputNum( pNtk->pManTime, iBox ); + for ( k = 0; k < nTerms; k++ ) + { + pNext = Nwk_ManCo( pNtk, iTerm1 + k ); + if ( !Nwk_ObjIsTravIdCurrent(pNext) ) + { + printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id ); + return 0; + } + } + } + } + } + else + assert( 0 ); + Nwk_ObjSetTravIdCurrent( pObj ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes the number of logic levels not counting PIs/POs.] + + Description [Assumes that white boxes have unit level.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManLevelBackup( Nwk_Man_t * pNtk ) +{ + Tim_Man_t * pManTimeUnit; + Nwk_Obj_t * pObj, * pFanin; + int i, k, LevelMax, Level; + assert( Nwk_ManVerifyTopoOrder(pNtk) ); + // clean the levels + Nwk_ManForEachObj( pNtk, pObj, i ) + Nwk_ObjSetLevel( pObj, 0 ); + // perform level computation + LevelMax = 0; + pManTimeUnit = pNtk->pManTime ? Tim_ManDupUnit( pNtk->pManTime ) : NULL; + if ( pManTimeUnit ) + Tim_ManIncrementTravId( pManTimeUnit ); + Nwk_ManForEachObj( pNtk, pObj, i ) + { + if ( Nwk_ObjIsCi(pObj) ) + { + Level = pManTimeUnit? (int)Tim_ManGetCiArrival( pManTimeUnit, pObj->PioId ) : 0; + Nwk_ObjSetLevel( pObj, Level ); + } + else if ( Nwk_ObjIsCo(pObj) ) + { + Level = Nwk_ObjLevel( Nwk_ObjFanin0(pObj) ); + if ( pManTimeUnit ) + Tim_ManSetCoArrival( pManTimeUnit, pObj->PioId, (float)Level ); + Nwk_ObjSetLevel( pObj, Level ); + if ( LevelMax < Nwk_ObjLevel(pObj) ) + LevelMax = Nwk_ObjLevel(pObj); + } + else if ( Nwk_ObjIsNode(pObj) ) + { + Level = 0; + Nwk_ObjForEachFanin( pObj, pFanin, k ) + if ( Level < Nwk_ObjLevel(pFanin) ) + Level = Nwk_ObjLevel(pFanin); + Nwk_ObjSetLevel( pObj, Level + 1 ); + } + else + assert( 0 ); + } + // set the old timing manager + if ( pManTimeUnit ) + Tim_ManStop( pManTimeUnit ); + return LevelMax; +} + +/**Function************************************************************* + + Synopsis [Computes the number of logic levels not counting PIs/POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManLevel_rec( Nwk_Obj_t * pObj ) +{ + Tim_Man_t * pManTime = pObj->pMan->pManTime; + Nwk_Obj_t * pNext; + int i, iBox, iTerm1, nTerms, LevelMax = 0; + if ( Nwk_ObjIsTravIdCurrent( pObj ) ) + return; + Nwk_ObjSetTravIdCurrent( pObj ); + if ( Nwk_ObjIsCi(pObj) ) + { + if ( pManTime ) + { + iBox = Tim_ManBoxForCi( pManTime, pObj->PioId ); + if ( iBox >= 0 ) // this is not a true PI + { + iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox ); + nTerms = Tim_ManBoxInputNum( pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Nwk_ManCo(pObj->pMan, iTerm1 + i); + Nwk_ManLevel_rec( pNext ); + if ( LevelMax < Nwk_ObjLevel(pNext) ) + LevelMax = Nwk_ObjLevel(pNext); + } + LevelMax++; + } + } + } + else if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) ) + { + Nwk_ObjForEachFanin( pObj, pNext, i ) + { + Nwk_ManLevel_rec( pNext ); + if ( LevelMax < Nwk_ObjLevel(pNext) ) + LevelMax = Nwk_ObjLevel(pNext); + } + if ( Nwk_ObjIsNode(pObj) && Nwk_ObjFaninNum(pObj) > 0 ) + LevelMax++; + } + else + assert( 0 ); + Nwk_ObjSetLevel( pObj, LevelMax ); +} + +/**Function************************************************************* + + Synopsis [Computes the number of logic levels not counting PIs/POs.] + + Description [Does not assume that the objects are in a topo order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManLevel( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pObj; + int i, LevelMax = 0; + Nwk_ManForEachObj( pNtk, pObj, i ) + Nwk_ObjSetLevel( pObj, 0 ); + Nwk_ManIncrementTravId( pNtk ); + Nwk_ManForEachPo( pNtk, pObj, i ) + { + Nwk_ManLevel_rec( pObj ); + if ( LevelMax < Nwk_ObjLevel(pObj) ) + LevelMax = Nwk_ObjLevel(pObj); + } + Nwk_ManForEachCi( pNtk, pObj, i ) + { + Nwk_ManLevel_rec( pObj ); + if ( LevelMax < Nwk_ObjLevel(pObj) ) + LevelMax = Nwk_ObjLevel(pObj); + } + return LevelMax; +} + +/**Function************************************************************* + + Synopsis [Computes the number of logic levels not counting PIs/POs.] + + Description [Does not assume that the objects are in a topo order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManLevelMax( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pObj; + int i, LevelMax = 0; + Nwk_ManForEachPo( pNtk, pObj, i ) + if ( LevelMax < Nwk_ObjLevel(pObj) ) + LevelMax = Nwk_ObjLevel(pObj); + return LevelMax; +} + +/**Function************************************************************* + + Synopsis [Returns the array of objects in the AIG manager ordered by level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pObj; + Vec_Vec_t * vLevels; + int nLevels, i; +// assert( Nwk_ManVerifyLevel(pNtk) ); + nLevels = Nwk_ManLevelMax( pNtk ); + vLevels = Vec_VecStart( nLevels + 1 ); + Nwk_ManForEachNode( pNtk, pObj, i ) + { + assert( Nwk_ObjLevel(pObj) <= nLevels ); + Vec_VecPush( vLevels, Nwk_ObjLevel(pObj), pObj ); + } + return vLevels; +} + + + +/**Function************************************************************* + + Synopsis [Performs DFS for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManDfs_rec( Nwk_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + Nwk_Obj_t * pNext; + int i; + if ( Nwk_ObjIsTravIdCurrent( pObj ) ) + return; + Nwk_ObjSetTravIdCurrent( pObj ); + Nwk_ObjForEachFanin( pObj, pNext, i ) + Nwk_ManDfs_rec( pNext, vNodes ); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Returns the DFS ordered array of all objects except latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Nwk_ManDfs( Nwk_Man_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Nwk_Obj_t * pObj; + int i; + Nwk_ManIncrementTravId( pNtk ); + vNodes = Vec_PtrAlloc( 100 ); + Nwk_ManForEachObj( pNtk, pObj, i ) + { + if ( Nwk_ObjIsCi(pObj) ) + { + Nwk_ObjSetTravIdCurrent( pObj ); + Vec_PtrPush( vNodes, pObj ); + } + else if ( Nwk_ObjIsCo(pObj) ) + Nwk_ManDfs_rec( pObj, vNodes ); + } + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Performs DFS for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManDfsNodes_rec( Nwk_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + Nwk_Obj_t * pNext; + int i; + if ( Nwk_ObjIsTravIdCurrent( pObj ) ) + return; + Nwk_ObjSetTravIdCurrent( pObj ); + if ( Nwk_ObjIsCi(pObj) ) + return; + assert( Nwk_ObjIsNode(pObj) ); + Nwk_ObjForEachFanin( pObj, pNext, i ) + Nwk_ManDfsNodes_rec( pNext, vNodes ); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Returns the set of internal nodes rooted in the given nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes ) +{ + Vec_Ptr_t * vNodes; + int i; + // set the traversal ID + Nwk_ManIncrementTravId( pNtk ); + // start the array of nodes + vNodes = Vec_PtrAlloc( 100 ); + // go through the PO nodes and call for each of them + for ( i = 0; i < nNodes; i++ ) + if ( Nwk_ObjIsCo(ppNodes[i]) ) + Nwk_ManDfsNodes_rec( Nwk_ObjFanin0(ppNodes[i]), vNodes ); + else + Nwk_ManDfsNodes_rec( ppNodes[i], vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Performs DFS for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManDfsReverse_rec( Nwk_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + Nwk_Obj_t * pNext; + int i, iBox, iTerm1, nTerms; + if ( Nwk_ObjIsTravIdCurrent( pObj ) ) + return; + Nwk_ObjSetTravIdCurrent( pObj ); + if ( Nwk_ObjIsCo(pObj) ) + { + if ( pObj->pMan->pManTime ) + { + iBox = Tim_ManBoxForCo( pObj->pMan->pManTime, pObj->PioId ); + if ( iBox >= 0 ) // this is not a true PO + { + iTerm1 = Tim_ManBoxOutputFirst( pObj->pMan->pManTime, iBox ); + nTerms = Tim_ManBoxOutputNum( pObj->pMan->pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Nwk_ManCi(pObj->pMan, iTerm1 + i); + Nwk_ManDfsReverse_rec( pNext, vNodes ); + } + } + } + } + else if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) ) + { + Nwk_ObjForEachFanout( pObj, pNext, i ) + Nwk_ManDfsReverse_rec( pNext, vNodes ); + } + else + assert( 0 ); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Returns the DFS ordered array of all objects except latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Nwk_ManDfsReverse( Nwk_Man_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Nwk_Obj_t * pObj; + int i; + Nwk_ManIncrementTravId( pNtk ); + vNodes = Vec_PtrAlloc( 100 ); + Nwk_ManForEachPi( pNtk, pObj, i ) + Nwk_ManDfsReverse_rec( pObj, vNodes ); + // add nodes without fanins + Nwk_ManForEachNode( pNtk, pObj, i ) + if ( Nwk_ObjFaninNum(pObj) == 0 && !Nwk_ObjIsTravIdCurrent(pObj) ) + Vec_PtrPush( vNodes, pObj ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Performs DFS for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManSupportNodes_rec( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ + Nwk_Obj_t * pFanin; + int i; + // if this node is already visited, skip + if ( Nwk_ObjIsTravIdCurrent( pNode ) ) + return; + // mark the node as visited + Nwk_ObjSetTravIdCurrent( pNode ); + // collect the CI + if ( Nwk_ObjIsCi(pNode) ) + { + Vec_PtrPush( vNodes, pNode ); + return; + } + assert( Nwk_ObjIsNode( pNode ) ); + // visit the transitive fanin of the node + Nwk_ObjForEachFanin( pNode, pFanin, i ) + Nwk_ManSupportNodes_rec( pFanin, vNodes ); +} + +/**Function************************************************************* + + Synopsis [Returns the set of CI nodes in the support of the given nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Nwk_ManSupportNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes ) +{ + Vec_Ptr_t * vNodes; + int i; + // set the traversal ID + Nwk_ManIncrementTravId( pNtk ); + // start the array of nodes + vNodes = Vec_PtrAlloc( 100 ); + // go through the PO nodes and call for each of them + for ( i = 0; i < nNodes; i++ ) + if ( Nwk_ObjIsCo(ppNodes[i]) ) + Nwk_ManSupportNodes_rec( Nwk_ObjFanin0(ppNodes[i]), vNodes ); + else + Nwk_ManSupportNodes_rec( ppNodes[i], vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Computes the sum total of supports of all outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManSupportSum( Nwk_Man_t * pNtk ) +{ + Vec_Ptr_t * vSupp; + Nwk_Obj_t * pObj; + int i, nTotalSupps = 0; + Nwk_ManForEachCo( pNtk, pObj, i ) + { + vSupp = Nwk_ManSupportNodes( pNtk, &pObj, 1 ); + nTotalSupps += Vec_PtrSize( vSupp ); + Vec_PtrFree( vSupp ); + } + printf( "Total supports = %d.\n", nTotalSupps ); +} + + +/**Function************************************************************* + + Synopsis [Dereferences the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ObjDeref_rec( Nwk_Obj_t * pNode ) +{ + Nwk_Obj_t * pFanin; + int i, Counter = 1; + if ( Nwk_ObjIsCi(pNode) ) + return 0; + Nwk_ObjForEachFanin( pNode, pFanin, i ) + { + assert( pFanin->nFanouts > 0 ); + if ( --pFanin->nFanouts == 0 ) + Counter += Nwk_ObjDeref_rec( pFanin ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [References the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ObjRef_rec( Nwk_Obj_t * pNode ) +{ + Nwk_Obj_t * pFanin; + int i, Counter = 1; + if ( Nwk_ObjIsCi(pNode) ) + return 0; + Nwk_ObjForEachFanin( pNode, pFanin, i ) + { + if ( pFanin->nFanouts++ == 0 ) + Counter += Nwk_ObjRef_rec( pFanin ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Collects the internal and boundary nodes in the derefed MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ObjMffcLabel_rec( Nwk_Obj_t * pNode, int fTopmost ) +{ + Nwk_Obj_t * pFanin; + int i; + // add to the new support nodes + if ( !fTopmost && (Nwk_ObjIsCi(pNode) || pNode->nFanouts > 0) ) + return; + // skip visited nodes + if ( Nwk_ObjIsTravIdCurrent(pNode) ) + return; + Nwk_ObjSetTravIdCurrent(pNode); + // recur on the children + Nwk_ObjForEachFanin( pNode, pFanin, i ) + Nwk_ObjMffcLabel_rec( pFanin, 0 ); + // collect the internal node +// printf( "%d ", pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Collects the internal nodes of the MFFC limited by cut.] + + Description [] + + SideEffects [Increments the trav ID and marks visited nodes.] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ObjMffcLabel( Nwk_Obj_t * pNode ) +{ + int Count1, Count2; + // dereference the node + Count1 = Nwk_ObjDeref_rec( pNode ); + // collect the nodes inside the MFFC + Nwk_ManIncrementTravId( pNode->pMan ); + Nwk_ObjMffcLabel_rec( pNode, 1 ); + // reference it back + Count2 = Nwk_ObjRef_rec( pNode ); + assert( Count1 == Count2 ); + return Count1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/nwk2/nwkFanio.c b/src/aig/nwk2/nwkFanio.c new file mode 100644 index 00000000..4068a1a5 --- /dev/null +++ b/src/aig/nwk2/nwkFanio.c @@ -0,0 +1,309 @@ +/**CFile**************************************************************** + + FileName [nwkFanio.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Logic network representation.] + + Synopsis [Manipulation of fanins/fanouts.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwkFanio.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "nwk.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collects fanins of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ + Nwk_Obj_t * pFanin; + int i; + Vec_PtrClear(vNodes); + Nwk_ObjForEachFanin( pNode, pFanin, i ) + Vec_PtrPush( vNodes, pFanin ); +} + +/**Function************************************************************* + + Synopsis [Collects fanouts of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ + Nwk_Obj_t * pFanout; + int i; + Vec_PtrClear(vNodes); + Nwk_ObjForEachFanout( pNode, pFanout, i ) + Vec_PtrPush( vNodes, pFanout ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of the fanin of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ) +{ + Nwk_Obj_t * pTemp; + int i; + Nwk_ObjForEachFanin( pObj, pTemp, i ) + if ( pTemp == pFanin ) + return i; + return -1; +} + +/**Function************************************************************* + + Synopsis [Returns the number of the fanout of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout ) +{ + Nwk_Obj_t * pTemp; + int i; + Nwk_ObjForEachFanout( pObj, pTemp, i ) + if ( pTemp == pFanout ) + return i; + return -1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node has to be reallocated.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Nwk_ObjReallocIsNeeded( Nwk_Obj_t * pObj ) +{ + return pObj->nFanins + pObj->nFanouts == pObj->nFanioAlloc; +} + +/**Function************************************************************* + + Synopsis [Reallocates the object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Nwk_Obj_t * Nwk_ManReallocNode( Nwk_Obj_t * pObj ) +{ + Nwk_Obj_t ** pFanioOld = pObj->pFanio; + assert( Nwk_ObjReallocIsNeeded(pObj) ); + pObj->pFanio = (Nwk_Obj_t **)Aig_MmFlexEntryFetch( pObj->pMan->pMemObjs, 2 * pObj->nFanioAlloc * sizeof(Nwk_Obj_t *) ); + memmove( pObj->pFanio, pFanioOld, pObj->nFanioAlloc * sizeof(Nwk_Obj_t *) ); + pObj->nFanioAlloc *= 2; + pObj->pMan->nRealloced++; + return NULL; +} + +/**Function************************************************************* + + Synopsis [Creates fanout/fanin relationship between the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ) +{ + int i; + assert( pObj->pMan == pFanin->pMan ); + assert( pObj->Id >= 0 && pFanin->Id >= 0 ); + if ( Nwk_ObjReallocIsNeeded(pObj) ) + Nwk_ManReallocNode( pObj ); + if ( Nwk_ObjReallocIsNeeded(pFanin) ) + Nwk_ManReallocNode( pFanin ); + for ( i = pObj->nFanins + pObj->nFanouts; i > pObj->nFanins; i-- ) + pObj->pFanio[i] = pObj->pFanio[i-1]; + pObj->pFanio[pObj->nFanins++] = pFanin; + pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj; + pObj->Level = AIG_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Removes fanout/fanin relationship between the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ) +{ + int i, k, Limit; + // remove pFanin from the fanin list of pObj + Limit = pObj->nFanins + pObj->nFanouts; + for ( k = i = 0; i < Limit; i++ ) + if ( pObj->pFanio[i] != pFanin ) + pObj->pFanio[k++] = pObj->pFanio[i]; + assert( i == k + 1 ); // if it fails, likely because of duplicated fanin + pObj->nFanins--; + // remove pObj from the fanout list of pFanin + Limit = pFanin->nFanins + pFanin->nFanouts; + for ( k = i = pFanin->nFanins; i < Limit; i++ ) + if ( pFanin->pFanio[i] != pObj ) + pFanin->pFanio[k++] = pFanin->pFanio[i]; + assert( i == k + 1 ); // if it fails, likely because of duplicated fanout + pFanin->nFanouts--; +} + +/**Function************************************************************* + + Synopsis [Replaces a fanin of the node.] + + Description [The node is pObj. An old fanin of this node (pFaninOld) has to be + replaced by a new fanin (pFaninNew). Assumes that the node and the old fanin + are not complemented. The new fanin can be complemented. In this case, the + polarity of the new fanin will change, compared to the polarity of the old fanin.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew ) +{ + int i, k, iFanin, Limit; + assert( pFaninOld != pFaninNew ); + assert( pObj != pFaninOld ); + assert( pObj != pFaninNew ); + assert( pObj->pMan == pFaninOld->pMan ); + assert( pObj->pMan == pFaninNew->pMan ); + // update the fanin + iFanin = Nwk_ObjFindFanin( pObj, pFaninOld ); + if ( iFanin == -1 ) + { + printf( "Nwk_ObjPatchFanin(); Error! Node %d is not among", pFaninOld->Id ); + printf( " the fanins of node %d...\n", pObj->Id ); + return; + } + pObj->pFanio[iFanin] = pFaninNew; + // remove pObj from the fanout list of pFaninOld + Limit = pFaninOld->nFanins + pFaninOld->nFanouts; + for ( k = i = pFaninOld->nFanins; i < Limit; i++ ) + if ( pFaninOld->pFanio[i] != pObj ) + pFaninOld->pFanio[k++] = pFaninOld->pFanio[i]; + pFaninOld->nFanouts--; + // add pObj to the fanout list of pFaninNew + if ( Nwk_ObjReallocIsNeeded(pFaninNew) ) + Nwk_ManReallocNode( pFaninNew ); + pFaninNew->pFanio[pFaninNew->nFanins + pFaninNew->nFanouts++] = pObj; +} + + +/**Function************************************************************* + + Synopsis [Transfers fanout from the old node to the new node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo ) +{ + Vec_Ptr_t * vFanouts = pNodeFrom->pMan->vTemp; + Nwk_Obj_t * pTemp; + int nFanoutsOld, i; + assert( !Nwk_ObjIsCo(pNodeFrom) && !Nwk_ObjIsCo(pNodeTo) ); + assert( pNodeFrom->pMan == pNodeTo->pMan ); + assert( pNodeFrom != pNodeTo ); + assert( Nwk_ObjFanoutNum(pNodeFrom) > 0 ); + // get the fanouts of the old node + nFanoutsOld = Nwk_ObjFanoutNum(pNodeTo); + Nwk_ObjCollectFanouts( pNodeFrom, vFanouts ); + // patch the fanin of each of them + Vec_PtrForEachEntry( vFanouts, pTemp, i ) + Nwk_ObjPatchFanin( pTemp, pNodeFrom, pNodeTo ); + assert( Nwk_ObjFanoutNum(pNodeFrom) == 0 ); + assert( Nwk_ObjFanoutNum(pNodeTo) == nFanoutsOld + Vec_PtrSize(vFanouts) ); +} + +/**Function************************************************************* + + Synopsis [Replaces the node by a new node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew ) +{ + assert( pNodeOld->pMan == pNodeNew->pMan ); + assert( pNodeOld != pNodeNew ); + assert( Nwk_ObjFanoutNum(pNodeOld) > 0 ); + // transfer the fanouts to the old node + Nwk_ObjTransferFanout( pNodeOld, pNodeNew ); + // remove the old node + Nwk_ManDeleteNode_rec( pNodeOld ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/nwk2/nwkMan.c b/src/aig/nwk2/nwkMan.c new file mode 100644 index 00000000..962cafd4 --- /dev/null +++ b/src/aig/nwk2/nwkMan.c @@ -0,0 +1,239 @@ +/**CFile**************************************************************** + + FileName [nwkMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Logic network representation.] + + Synopsis [Network manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwkMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "nwk.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Man_t * Nwk_ManAlloc() +{ + Nwk_Man_t * p; + p = ALLOC( Nwk_Man_t, 1 ); + memset( p, 0, sizeof(Nwk_Man_t) ); + p->vCis = Vec_PtrAlloc( 1000 ); + p->vCos = Vec_PtrAlloc( 1000 ); + p->vObjs = Vec_PtrAlloc( 1000 ); + p->vTemp = Vec_PtrAlloc( 1000 ); + p->nFanioPlus = 2; + p->pMemObjs = Aig_MmFlexStart(); + p->pManHop = Hop_ManStart(); + return p; +} + +/**Function************************************************************* + + Synopsis [Deallocates the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManFree( Nwk_Man_t * p ) +{ +// printf( "The number of realloced nodes = %d.\n", p->nRealloced ); + if ( p->pName ) free( p->pName ); + if ( p->pSpec ) free( p->pSpec ); + if ( p->vCis ) Vec_PtrFree( p->vCis ); + if ( p->vCos ) Vec_PtrFree( p->vCos ); + if ( p->vObjs ) Vec_PtrFree( p->vObjs ); + if ( p->vTemp ) Vec_PtrFree( p->vTemp ); + if ( p->pManTime ) Tim_ManStop( p->pManTime ); + if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 ); + if ( p->pManHop ) Hop_ManStop( p->pManHop ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Prints stats of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +/* +void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib ) +{ + Nwk_Obj_t * pObj; + int i, Counters[256] = {0}; + Nwk_ManForEachNode( p, pObj, i ) + Counters[Nwk_ObjFaninNum(pObj)]++; + printf( "LUTs by size: " ); + for ( i = 0; i <= pLutLib->LutMax; i++ ) + printf( "%d:%d ", i, Counters[i] ); +} +*/ + +/**Function************************************************************* + + Synopsis [If the network is best, saves it in "best.blif" and returns 1.] + + Description [If the networks are incomparable, saves the new network, + returns its parameters in the internal parameter structure, and returns 1. + If the new network is not a logic network, quits without saving and returns 0.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl ) +{ + extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, void * pNtl, char * pFileName ); + extern void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames ); + static struct ParStruct { + char * pName; // name of the best saved network + int Depth; // depth of the best saved network + int Flops; // flops in the best saved network + int Nodes; // nodes in the best saved network + int nPis; // the number of primary inputs + int nPos; // the number of primary outputs + } ParsNew, ParsBest = { 0 }; + // free storage for the name + if ( pNtk == NULL ) + { + FREE( ParsBest.pName ); + return 0; + } + // get the parameters + ParsNew.Depth = Nwk_ManLevel( pNtk ); + ParsNew.Flops = Nwk_ManLatchNum( pNtk ); + ParsNew.Nodes = Nwk_ManNodeNum( pNtk ); + ParsNew.nPis = Nwk_ManPiNum( pNtk ); + ParsNew.nPos = Nwk_ManPoNum( pNtk ); + // reset the parameters if the network has the same name + if ( ParsBest.pName == NULL || + strcmp(ParsBest.pName, pNtk->pName) || + ParsBest.Depth > ParsNew.Depth || + (ParsBest.Depth == ParsNew.Depth && ParsBest.Flops > ParsNew.Flops) || + (ParsBest.Depth == ParsNew.Depth && ParsBest.Flops == ParsNew.Flops && ParsBest.Nodes > ParsNew.Nodes) ) + { + FREE( ParsBest.pName ); + ParsBest.pName = Aig_UtilStrsav( pNtk->pName ); + ParsBest.Depth = ParsNew.Depth; + ParsBest.Flops = ParsNew.Flops; + ParsBest.Nodes = ParsNew.Nodes; + ParsBest.nPis = ParsNew.nPis; + ParsBest.nPos = ParsNew.nPos; + // write the network +// Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" ); +// Nwk_ManDumpBlif( pNtk, "best_map.blif", NULL, NULL ); + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Nwk_FileNameGeneric( char * FileName ) +{ + char * pDot, * pRes; + pRes = Aig_UtilStrsav( FileName ); + if ( (pDot = strrchr( pRes, '.' )) ) + *pDot = 0; + return pRes; +} + +/**Function************************************************************* + + Synopsis [Prints stats of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +/* +void Nwk_ManPrintStats( Nwk_Man_t * pNtk, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl ) +{ + extern int Ntl_ManLatchNum( void * p ); + extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, void * pNtl, char * pFileName ); + if ( fSaveBest ) + Nwk_ManCompareAndSaveBest( pNtk, pNtl ); + if ( fDumpResult ) + { + char Buffer[1000] = {0}; + char * pNameGen = pNtk->pSpec? Nwk_FileNameGeneric( pNtk->pSpec ) : "nameless_"; + sprintf( Buffer, "%s_dump.blif", pNameGen ); + Ioa_WriteBlifLogic( pNtk, pNtl, Buffer ); +// sprintf( Buffer, "%s_dump_map.blif", pNameGen ); +// Nwk_ManDumpBlif( pNtk, Buffer, NULL, NULL ); + if ( pNtk->pSpec ) free( pNameGen ); + } + + pNtk->pLutLib = pLutLib; + printf( "%-15s : ", pNtk->pName ); + printf( "pi = %5d ", Nwk_ManPiNum(pNtk) ); + printf( "po = %5d ", Nwk_ManPoNum(pNtk) ); + printf( "ci = %5d ", Nwk_ManCiNum(pNtk) ); + printf( "co = %5d ", Nwk_ManCoNum(pNtk) ); + printf( "lat = %5d ", Ntl_ManLatchNum(pNtl) ); + printf( "node = %5d ", Nwk_ManNodeNum(pNtk) ); + printf( "edge = %5d ", Nwk_ManGetTotalFanins(pNtk) ); + printf( "aig = %6d ", Nwk_ManGetAigNodeNum(pNtk) ); + printf( "lev = %3d ", Nwk_ManLevel(pNtk) ); +// printf( "lev2 = %3d ", Nwk_ManLevelBackup(pNtk) ); + printf( "delay = %5.2f ", Nwk_ManDelayTraceLut(pNtk) ); + Nwk_ManPrintLutSizes( pNtk, pLutLib ); + printf( "\n" ); +// Nwk_ManDelayTracePrint( pNtk, pLutLib ); + fflush( stdout ); +} +*/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/nwk2/nwkMerge.c b/src/aig/nwk2/nwkMerge.c new file mode 100644 index 00000000..1a5255d3 --- /dev/null +++ b/src/aig/nwk2/nwkMerge.c @@ -0,0 +1,993 @@ +/**CFile**************************************************************** + + FileName [nwkMerge.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [LUT merging algorithm.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwkMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "nwk.h" +#include "nwkMerge.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates the graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Grf_t * Nwk_ManGraphAlloc( int nVertsMax ) +{ + Nwk_Grf_t * p; + p = ALLOC( Nwk_Grf_t, 1 ); + memset( p, 0, sizeof(Nwk_Grf_t) ); + p->nVertsMax = nVertsMax; + p->nEdgeHash = Aig_PrimeCudd( 3 * nVertsMax ); + p->pEdgeHash = CALLOC( Nwk_Edg_t *, p->nEdgeHash ); + p->pMemEdges = Aig_MmFixedStart( sizeof(Nwk_Edg_t), p->nEdgeHash ); + p->vPairs = Vec_IntAlloc( 1000 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Deallocates the graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphFree( Nwk_Grf_t * p ) +{ + if ( p->vPairs ) Vec_IntFree( p->vPairs ); + if ( p->pMemEdges ) Aig_MmFixedStop( p->pMemEdges, 0 ); + if ( p->pMemVerts ) Aig_MmFlexStop( p->pMemVerts, 0 ); + FREE( p->pVerts ); + FREE( p->pEdgeHash ); + FREE( p->pMapLut2Id ); + FREE( p->pMapId2Lut ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Prepares the graph for solving the problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphReportMemoryUsage( Nwk_Grf_t * p ) +{ + p->nMemBytes1 = + sizeof(Nwk_Grf_t) + + sizeof(void *) * p->nEdgeHash + + sizeof(int) * (p->nObjs + p->nVertsMax) + + sizeof(Nwk_Edg_t) * p->nEdges; + p->nMemBytes2 = + sizeof(Nwk_Vrt_t) * p->nVerts + + sizeof(int) * 2 * p->nEdges; + printf( "Memory usage stats: Preprocessing = %.2f Mb. Solving = %.2f Mb.\n", + 1.0 * p->nMemBytes1 / (1<<20), 1.0 * p->nMemBytes2 / (1<<20) ); +} + + +/**Function************************************************************* + + Synopsis [Finds or adds the edge to the graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphHashEdge( Nwk_Grf_t * p, int iLut1, int iLut2 ) +{ + Nwk_Edg_t * pEntry; + unsigned Key; + if ( iLut1 == iLut2 ) + return; + if ( iLut1 > iLut2 ) + { + Key = iLut1; + iLut1 = iLut2; + iLut2 = Key; + } + assert( iLut1 < iLut2 ); + if ( p->nObjs < iLut2 ) + p->nObjs = iLut2; + Key = (unsigned)(741457 * iLut1 + 4256249 * iLut2) % p->nEdgeHash; + for ( pEntry = p->pEdgeHash[Key]; pEntry; pEntry = pEntry->pNext ) + if ( pEntry->iNode1 == iLut1 && pEntry->iNode2 == iLut2 ) + return; + pEntry = (Nwk_Edg_t *)Aig_MmFixedEntryFetch( p->pMemEdges ); + pEntry->iNode1 = iLut1; + pEntry->iNode2 = iLut2; + pEntry->pNext = p->pEdgeHash[Key]; + p->pEdgeHash[Key] = pEntry; + p->nEdges++; +} + +/**Function************************************************************* + + Synopsis [Adds one entry to the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphListAdd( Nwk_Grf_t * p, int * pList, Nwk_Vrt_t * pVertex ) +{ + if ( *pList ) + { + Nwk_Vrt_t * pHead; + pHead = p->pVerts[*pList]; + pVertex->iPrev = 0; + pVertex->iNext = pHead->Id; + pHead->iPrev = pVertex->Id; + } + *pList = pVertex->Id; +} + +/**Function************************************************************* + + Synopsis [Deletes one entry from the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphListDelete( Nwk_Grf_t * p, int * pList, Nwk_Vrt_t * pVertex ) +{ + assert( *pList ); + if ( pVertex->iPrev ) + { +// assert( p->pVerts[pVertex->iPrev]->iNext == pVertex->Id ); + p->pVerts[pVertex->iPrev]->iNext = pVertex->iNext; + } + if ( pVertex->iNext ) + { +// assert( p->pVerts[pVertex->iNext]->iPrev == pVertex->Id ); + p->pVerts[pVertex->iNext]->iPrev = pVertex->iPrev; + } + if ( *pList == pVertex->Id ) + *pList = pVertex->iNext; + pVertex->iPrev = pVertex->iNext = 0; +} + +/**Function************************************************************* + + Synopsis [Inserts the edge into one of the linked lists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphListInsert( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex ) +{ + Nwk_Vrt_t * pNext; + assert( pVertex->nEdges > 0 ); + + if ( pVertex->nEdges == 1 ) + { + pNext = p->pVerts[ pVertex->pEdges[0] ]; + if ( pNext->nEdges >= NWK_MAX_LIST ) + Nwk_ManGraphListAdd( p, p->pLists1 + NWK_MAX_LIST, pVertex ); + else + Nwk_ManGraphListAdd( p, p->pLists1 + pNext->nEdges, pVertex ); + } + else + { + if ( pVertex->nEdges >= NWK_MAX_LIST ) + Nwk_ManGraphListAdd( p, p->pLists2 + NWK_MAX_LIST, pVertex ); + else + Nwk_ManGraphListAdd( p, p->pLists2 + pVertex->nEdges, pVertex ); + } +} + +/**Function************************************************************* + + Synopsis [Extracts the edge from one of the linked lists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphListExtract( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex ) +{ + Nwk_Vrt_t * pNext; + assert( pVertex->nEdges > 0 ); + + if ( pVertex->nEdges == 1 ) + { + pNext = p->pVerts[ pVertex->pEdges[0] ]; + if ( pNext->nEdges >= NWK_MAX_LIST ) + Nwk_ManGraphListDelete( p, p->pLists1 + NWK_MAX_LIST, pVertex ); + else + Nwk_ManGraphListDelete( p, p->pLists1 + pNext->nEdges, pVertex ); + } + else + { + if ( pVertex->nEdges >= NWK_MAX_LIST ) + Nwk_ManGraphListDelete( p, p->pLists2 + NWK_MAX_LIST, pVertex ); + else + Nwk_ManGraphListDelete( p, p->pLists2 + pVertex->nEdges, pVertex ); + } +} + +/**Function************************************************************* + + Synopsis [Prepares the graph for solving the problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphPrepare( Nwk_Grf_t * p ) +{ + Nwk_Edg_t * pEntry; + Nwk_Vrt_t * pVertex; + int * pnEdges, nBytes, i; + // allocate memory for the present objects + p->pMapLut2Id = ALLOC( int, p->nObjs+1 ); + p->pMapId2Lut = ALLOC( int, p->nVertsMax+1 ); + memset( p->pMapLut2Id, 0xff, sizeof(int) * (p->nObjs+1) ); + memset( p->pMapId2Lut, 0xff, sizeof(int) * (p->nVertsMax+1) ); + // mark present objects + Nwk_GraphForEachEdge( p, pEntry, i ) + { + assert( pEntry->iNode1 <= p->nObjs ); + assert( pEntry->iNode2 <= p->nObjs ); + p->pMapLut2Id[ pEntry->iNode1 ] = 0; + p->pMapLut2Id[ pEntry->iNode2 ] = 0; + } + // map objects + p->nVerts = 0; + for ( i = 0; i <= p->nObjs; i++ ) + { + if ( p->pMapLut2Id[i] == 0 ) + { + p->pMapLut2Id[i] = ++p->nVerts; + p->pMapId2Lut[p->nVerts] = i; + } + } + // count the edges and mark present objects + pnEdges = CALLOC( int, p->nVerts+1 ); + Nwk_GraphForEachEdge( p, pEntry, i ) + { + // translate into vertices + assert( pEntry->iNode1 <= p->nObjs ); + assert( pEntry->iNode2 <= p->nObjs ); + pEntry->iNode1 = p->pMapLut2Id[pEntry->iNode1]; + pEntry->iNode2 = p->pMapLut2Id[pEntry->iNode2]; + // count the edges + assert( pEntry->iNode1 <= p->nVerts ); + assert( pEntry->iNode2 <= p->nVerts ); + pnEdges[pEntry->iNode1]++; + pnEdges[pEntry->iNode2]++; + } + // allocate the real graph + p->pMemVerts = Aig_MmFlexStart(); + p->pVerts = ALLOC( Nwk_Vrt_t *, p->nVerts + 1 ); + p->pVerts[0] = NULL; + for ( i = 1; i <= p->nVerts; i++ ) + { + assert( pnEdges[i] > 0 ); + nBytes = sizeof(Nwk_Vrt_t) + sizeof(int) * pnEdges[i]; + p->pVerts[i] = (Nwk_Vrt_t *)Aig_MmFlexEntryFetch( p->pMemVerts, nBytes ); + memset( p->pVerts[i], 0, nBytes ); + p->pVerts[i]->Id = i; + } + // add edges to the real graph + Nwk_GraphForEachEdge( p, pEntry, i ) + { + pVertex = p->pVerts[pEntry->iNode1]; + pVertex->pEdges[ pVertex->nEdges++ ] = pEntry->iNode2; + pVertex = p->pVerts[pEntry->iNode2]; + pVertex->pEdges[ pVertex->nEdges++ ] = pEntry->iNode1; + } + // put vertices into the data structure + for ( i = 1; i <= p->nVerts; i++ ) + { + assert( p->pVerts[i]->nEdges == pnEdges[i] ); + Nwk_ManGraphListInsert( p, p->pVerts[i] ); + } + // clean up + Aig_MmFixedStop( p->pMemEdges, 0 ); p->pMemEdges = NULL; + FREE( p->pEdgeHash ); +// p->nEdgeHash = 0; + free( pnEdges ); +} + +/**Function************************************************************* + + Synopsis [Updates the problem after pulling out one edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphCheckLists( Nwk_Grf_t * p ) +{ + Nwk_Vrt_t * pVertex, * pNext; + int i, j; + assert( p->pLists1[0] == 0 ); + for ( i = 1; i <= NWK_MAX_LIST; i++ ) + if ( p->pLists1[i] ) + { + pVertex = p->pVerts[ p->pLists1[i] ]; + assert( pVertex->nEdges == 1 ); + pNext = p->pVerts[ pVertex->pEdges[0] ]; + assert( pNext->nEdges == i || pNext->nEdges > NWK_MAX_LIST ); + } + // find the next vertext to extract + assert( p->pLists2[0] == 0 ); + assert( p->pLists2[1] == 0 ); + for ( j = 2; j <= NWK_MAX_LIST; j++ ) + if ( p->pLists2[j] ) + { + pVertex = p->pVerts[ p->pLists2[j] ]; + assert( pVertex->nEdges == j || pVertex->nEdges > NWK_MAX_LIST ); + } +} + +/**Function************************************************************* + + Synopsis [Extracts the edge from one of the linked lists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Nwk_ManGraphVertexRemoveEdge( Nwk_Vrt_t * pThis, Nwk_Vrt_t * pNext ) +{ + int k; + for ( k = 0; k < pThis->nEdges; k++ ) + if ( pThis->pEdges[k] == pNext->Id ) + break; + assert( k < pThis->nEdges ); + pThis->nEdges--; + for ( ; k < pThis->nEdges; k++ ) + pThis->pEdges[k] = pThis->pEdges[k+1]; +} + +/**Function************************************************************* + + Synopsis [Updates the problem after pulling out one edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphUpdate( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex, Nwk_Vrt_t * pNext ) +{ + Nwk_Vrt_t * pChanged, * pOther; + int i, k; +// Nwk_ManGraphCheckLists( p ); + Nwk_ManGraphListExtract( p, pVertex ); + Nwk_ManGraphListExtract( p, pNext ); + // update neihbors of pVertex + Nwk_VertexForEachAdjacent( p, pVertex, pChanged, i ) + { + if ( pChanged == pNext ) + continue; + Nwk_ManGraphListExtract( p, pChanged ); + // move those that use this one + if ( pChanged->nEdges > 1 ) + Nwk_VertexForEachAdjacent( p, pChanged, pOther, k ) + { + if ( pOther == pVertex || pOther->nEdges > 1 ) + continue; + assert( pOther->nEdges == 1 ); + Nwk_ManGraphListExtract( p, pOther ); + pChanged->nEdges--; + Nwk_ManGraphListInsert( p, pOther ); + pChanged->nEdges++; + } + // remove the edge + Nwk_ManGraphVertexRemoveEdge( pChanged, pVertex ); + // add the changed vertex back + if ( pChanged->nEdges > 0 ) + Nwk_ManGraphListInsert( p, pChanged ); + } + // update neihbors of pNext + Nwk_VertexForEachAdjacent( p, pNext, pChanged, i ) + { + if ( pChanged == pVertex ) + continue; + Nwk_ManGraphListExtract( p, pChanged ); + // move those that use this one + if ( pChanged->nEdges > 1 ) + Nwk_VertexForEachAdjacent( p, pChanged, pOther, k ) + { + if ( pOther == pNext || pOther->nEdges > 1 ) + continue; + assert( pOther->nEdges == 1 ); + Nwk_ManGraphListExtract( p, pOther ); + pChanged->nEdges--; + Nwk_ManGraphListInsert( p, pOther ); + pChanged->nEdges++; + } + // remove the edge + Nwk_ManGraphVertexRemoveEdge( pChanged, pNext ); + // add the changed vertex back + if ( pChanged->nEdges > 0 ) + Nwk_ManGraphListInsert( p, pChanged ); + } + // add to the result + if ( pVertex->Id < pNext->Id ) + { + Vec_IntPush( p->vPairs, p->pMapId2Lut[pVertex->Id] ); + Vec_IntPush( p->vPairs, p->pMapId2Lut[pNext->Id] ); + } + else + { + Vec_IntPush( p->vPairs, p->pMapId2Lut[pNext->Id] ); + Vec_IntPush( p->vPairs, p->pMapId2Lut[pVertex->Id] ); + } +// Nwk_ManGraphCheckLists( p ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of entries in the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManGraphListLength( Nwk_Grf_t * p, int List ) +{ + Nwk_Vrt_t * pThis; + int fVerbose = 0; + int Counter = 0; + Nwk_ListForEachVertex( p, List, pThis ) + { + if ( fVerbose && Counter < 20 ) + printf( "%d ", p->pVerts[pThis->pEdges[0]]->nEdges ); + Counter++; + } + if ( fVerbose ) + printf( "\n" ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns the adjacent vertex with the mininum number of edges.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Vrt_t * Nwk_ManGraphListFindMinEdge( Nwk_Grf_t * p, Nwk_Vrt_t * pVert ) +{ + Nwk_Vrt_t * pThis, * pMinCost = NULL; + int k; + Nwk_VertexForEachAdjacent( p, pVert, pThis, k ) + { + if ( pMinCost == NULL || pMinCost->nEdges > pThis->nEdges ) + pMinCost = pThis; + } + return pMinCost; +} + +/**Function************************************************************* + + Synopsis [Finds the best vertext in the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Vrt_t * Nwk_ManGraphListFindMin( Nwk_Grf_t * p, int List ) +{ + Nwk_Vrt_t * pThis, * pMinCost = NULL; + int k, Counter = 10000, BestCost = 1000000; + Nwk_ListForEachVertex( p, List, pThis ) + { + for ( k = 0; k < pThis->nEdges; k++ ) + { + if ( pMinCost == NULL || BestCost > p->pVerts[pThis->pEdges[k]]->nEdges ) + { + BestCost = p->pVerts[pThis->pEdges[k]]->nEdges; + pMinCost = pThis; + } + } + if ( --Counter == 0 ) + break; + } + return pMinCost; +} + +/**Function************************************************************* + + Synopsis [Solves the problem by extracting one edge at a time.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManGraphSolve( Nwk_Grf_t * p ) +{ + Nwk_Vrt_t * pVertex, * pNext; + int i, j; + Nwk_ManGraphPrepare( p ); + while ( 1 ) + { + // find the next vertex to extract + assert( p->pLists1[0] == 0 ); + for ( i = 1; i <= NWK_MAX_LIST; i++ ) + if ( p->pLists1[i] ) + { +// printf( "%d ", i ); +// printf( "ListA = %2d. Length = %5d.\n", i, Nwk_ManGraphListLength(p,p->pLists1[i]) ); + pVertex = p->pVerts[ p->pLists1[i] ]; + assert( pVertex->nEdges == 1 ); + pNext = p->pVerts[ pVertex->pEdges[0] ]; + Nwk_ManGraphUpdate( p, pVertex, pNext ); + break; + } + if ( i < NWK_MAX_LIST + 1 ) + continue; + // find the next vertex to extract + assert( p->pLists2[0] == 0 ); + assert( p->pLists2[1] == 0 ); + for ( j = 2; j <= NWK_MAX_LIST; j++ ) + if ( p->pLists2[j] ) + { +// printf( "***%d ", j ); +// printf( "ListB = %2d. Length = %5d.\n", j, Nwk_ManGraphListLength(p,p->pLists2[j]) ); + pVertex = Nwk_ManGraphListFindMin( p, p->pLists2[j] ); + assert( pVertex->nEdges == j || j == NWK_MAX_LIST ); + pNext = Nwk_ManGraphListFindMinEdge( p, pVertex ); + Nwk_ManGraphUpdate( p, pVertex, pNext ); + break; + } + if ( j == NWK_MAX_LIST + 1 ) + break; + } +} + +/**Function************************************************************* + + Synopsis [Reads graph from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Grf_t * Nwk_ManLutMergeReadGraph( char * pFileName ) +{ + Nwk_Grf_t * p; + FILE * pFile; + char Buffer[100]; + int nNodes, nEdges, iNode1, iNode2; + pFile = fopen( pFileName, "r" ); + fscanf( pFile, "%s %d", Buffer, &nNodes ); + fscanf( pFile, "%s %d", Buffer, &nEdges ); + p = Nwk_ManGraphAlloc( nNodes ); + while ( fscanf( pFile, "%s %d %d", Buffer, &iNode1, &iNode2 ) == 3 ) + Nwk_ManGraphHashEdge( p, iNode1, iNode2 ); + assert( p->nEdges == nEdges ); + fclose( pFile ); + return p; +} + +/**Function************************************************************* + + Synopsis [Solves the graph coming from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManLutMergeGraphTest( char * pFileName ) +{ + int nPairs; + Nwk_Grf_t * p; + int clk = clock(); + p = Nwk_ManLutMergeReadGraph( pFileName ); + PRT( "Reading", clock() - clk ); + clk = clock(); + Nwk_ManGraphSolve( p ); + printf( "GRAPH: Nodes = %6d. Edges = %6d. Pairs = %6d. ", + p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 ); + PRT( "Solving", clock() - clk ); + nPairs = Vec_IntSize(p->vPairs)/2; + Nwk_ManGraphReportMemoryUsage( p ); + Nwk_ManGraphFree( p ); + return nPairs; +} + + + + +/**Function************************************************************* + + Synopsis [Marks the fanins of the node with the current trav ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManMarkFanins_rec( Nwk_Obj_t * pLut, int nLevMin ) +{ + Nwk_Obj_t * pNext; + int i; + if ( !Nwk_ObjIsNode(pLut) ) + return; + if ( Nwk_ObjIsTravIdCurrent( pLut ) ) + return; + Nwk_ObjSetTravIdCurrent( pLut ); + if ( Nwk_ObjLevel(pLut) < nLevMin ) + return; + Nwk_ObjForEachFanin( pLut, pNext, i ) + Nwk_ManMarkFanins_rec( pNext, nLevMin ); +} + +/**Function************************************************************* + + Synopsis [Marks the fanouts of the node with the current trav ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManMarkFanouts_rec( Nwk_Obj_t * pLut, int nLevMax, int nFanMax ) +{ + Nwk_Obj_t * pNext; + int i; + if ( !Nwk_ObjIsNode(pLut) ) + return; + if ( Nwk_ObjIsTravIdCurrent( pLut ) ) + return; + Nwk_ObjSetTravIdCurrent( pLut ); + if ( Nwk_ObjLevel(pLut) > nLevMax ) + return; + if ( Nwk_ObjFanoutNum(pLut) > nFanMax ) + return; + Nwk_ObjForEachFanout( pLut, pNext, i ) + Nwk_ManMarkFanouts_rec( pNext, nLevMax, nFanMax ); +} + +/**Function************************************************************* + + Synopsis [Collects the circle of nodes around the given set.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManCollectCircle( Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, int nFanMax ) +{ + Nwk_Obj_t * pObj, * pNext; + int i, k; + Vec_PtrClear( vNext ); + Vec_PtrForEachEntry( vStart, pObj, i ) + { + Nwk_ObjForEachFanin( pObj, pNext, k ) + { + if ( !Nwk_ObjIsNode(pNext) ) + continue; + if ( Nwk_ObjIsTravIdCurrent( pNext ) ) + continue; + Nwk_ObjSetTravIdCurrent( pNext ); + Vec_PtrPush( vNext, pNext ); + } + Nwk_ObjForEachFanout( pObj, pNext, k ) + { + if ( !Nwk_ObjIsNode(pNext) ) + continue; + if ( Nwk_ObjIsTravIdCurrent( pNext ) ) + continue; + Nwk_ObjSetTravIdCurrent( pNext ); + if ( Nwk_ObjFanoutNum(pNext) > nFanMax ) + continue; + Vec_PtrPush( vNext, pNext ); + } + } +} + +/**Function************************************************************* + + Synopsis [Collects the circle of nodes removes from the given one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManCollectNonOverlapCands( Nwk_Obj_t * pLut, Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars ) +{ + Vec_Ptr_t * vTemp; + Nwk_Obj_t * pObj; + int i, k; + Vec_PtrClear( vCands ); + if ( pPars->nMaxSuppSize - Nwk_ObjFaninNum(pLut) <= 1 ) + return; + + // collect nodes removed by this distance + assert( pPars->nMaxDistance > 0 ); + Vec_PtrClear( vStart ); + Vec_PtrPush( vStart, pLut ); + Nwk_ManIncrementTravId( pLut->pMan ); + Nwk_ObjSetTravIdCurrent( pLut ); + for ( i = 1; i <= pPars->nMaxDistance; i++ ) + { + Nwk_ManCollectCircle( vStart, vNext, pPars->nMaxFanout ); + vTemp = vStart; + vStart = vNext; + vNext = vTemp; + // collect the nodes in vStart + Vec_PtrForEachEntry( vStart, pObj, k ) + Vec_PtrPush( vCands, pObj ); + } + + // mark the TFI/TFO nodes + Nwk_ManIncrementTravId( pLut->pMan ); + if ( pPars->fUseTfiTfo ) + Nwk_ObjSetTravIdCurrent( pLut ); + else + { + Nwk_ObjSetTravIdPrevious( pLut ); + Nwk_ManMarkFanins_rec( pLut, Nwk_ObjLevel(pLut) - pPars->nMaxDistance ); + Nwk_ObjSetTravIdPrevious( pLut ); + Nwk_ManMarkFanouts_rec( pLut, Nwk_ObjLevel(pLut) + pPars->nMaxDistance, pPars->nMaxFanout ); + } + + // collect nodes satisfying the following conditions: + // - they are close enough in terms of distance + // - they are not in the TFI/TFO of the LUT + // - they have no more than the given number of fanins + // - they have no more than the given diff in delay + k = 0; + Vec_PtrForEachEntry( vCands, pObj, i ) + { + if ( Nwk_ObjIsTravIdCurrent(pObj) ) + continue; + if ( Nwk_ObjFaninNum(pLut) + Nwk_ObjFaninNum(pObj) > pPars->nMaxSuppSize ) + continue; + if ( Nwk_ObjLevel(pLut) - Nwk_ObjLevel(pObj) > pPars->nMaxLevelDiff || + Nwk_ObjLevel(pObj) - Nwk_ObjLevel(pLut) > pPars->nMaxLevelDiff ) + continue; + Vec_PtrWriteEntry( vCands, k++, pObj ); + } + Vec_PtrShrink( vCands, k ); +} + + +/**Function************************************************************* + + Synopsis [Count the total number of fanins.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManCountTotalFanins( Nwk_Obj_t * pLut, Nwk_Obj_t * pCand ) +{ + Nwk_Obj_t * pFanin; + int i, nCounter = Nwk_ObjFaninNum(pLut); + Nwk_ObjForEachFanin( pCand, pFanin, i ) + nCounter += !pFanin->MarkC; + return nCounter; +} + +/**Function************************************************************* + + Synopsis [Collects overlapping candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwl_ManCollectOverlapCands( Nwk_Obj_t * pLut, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars ) +{ + Nwk_Obj_t * pFanin, * pObj; + int i, k; + // mark fanins of pLut + Nwk_ObjForEachFanin( pLut, pFanin, i ) + pFanin->MarkC = 1; + // collect the matching fanouts of each fanin of the node + Vec_PtrClear( vCands ); + Nwk_ManIncrementTravId( pLut->pMan ); + Nwk_ObjSetTravIdCurrent( pLut ); + Nwk_ObjForEachFanin( pLut, pFanin, i ) + { + if ( !Nwk_ObjIsNode(pFanin) ) + continue; + if ( Nwk_ObjFanoutNum(pFanin) > pPars->nMaxFanout ) + continue; + Nwk_ObjForEachFanout( pFanin, pObj, k ) + { + if ( !Nwk_ObjIsNode(pObj) ) + continue; + if ( Nwk_ObjIsTravIdCurrent( pObj ) ) + continue; + Nwk_ObjSetTravIdCurrent( pObj ); + // check the difference in delay + if ( Nwk_ObjLevel(pLut) - Nwk_ObjLevel(pObj) > pPars->nMaxLevelDiff || + Nwk_ObjLevel(pObj) - Nwk_ObjLevel(pLut) > pPars->nMaxLevelDiff ) + continue; + // check the total number of fanins of the node + if ( Nwk_ManCountTotalFanins(pLut, pObj) > pPars->nMaxSuppSize ) + continue; + Vec_PtrPush( vCands, pObj ); + } + } + // unmark fanins of pLut + Nwk_ObjForEachFanin( pLut, pFanin, i ) + pFanin->MarkC = 0; +} + +/**Function************************************************************* + + Synopsis [Performs LUT merging with parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Nwk_ManLutMerge( Nwk_Man_t * pNtk, Nwk_LMPars_t * pPars ) +{ + Nwk_Grf_t * p; + Vec_Int_t * vResult; + Vec_Ptr_t * vStart, * vNext, * vCands1, * vCands2; + Nwk_Obj_t * pLut, * pCand; + int i, k, nVertsMax, nCands, clk = clock(); + // count the number of vertices + nVertsMax = 0; + Nwk_ManForEachNode( pNtk, pLut, i ) + nVertsMax += (int)(Nwk_ObjFaninNum(pLut) <= pPars->nMaxLutSize); + p = Nwk_ManGraphAlloc( nVertsMax ); + // create graph + vStart = Vec_PtrAlloc( 1000 ); + vNext = Vec_PtrAlloc( 1000 ); + vCands1 = Vec_PtrAlloc( 1000 ); + vCands2 = Vec_PtrAlloc( 1000 ); + nCands = 0; + Nwk_ManForEachNode( pNtk, pLut, i ) + { + if ( Nwk_ObjFaninNum(pLut) > pPars->nMaxLutSize ) + continue; + Nwl_ManCollectOverlapCands( pLut, vCands1, pPars ); + if ( pPars->fUseDiffSupp ) + Nwk_ManCollectNonOverlapCands( pLut, vStart, vNext, vCands2, pPars ); + if ( Vec_PtrSize(vCands1) == 0 && Vec_PtrSize(vCands2) == 0 ) + continue; + nCands += Vec_PtrSize(vCands1) + Vec_PtrSize(vCands2); + // save candidates + Vec_PtrForEachEntry( vCands1, pCand, k ) + Nwk_ManGraphHashEdge( p, Nwk_ObjId(pLut), Nwk_ObjId(pCand) ); + Vec_PtrForEachEntry( vCands2, pCand, k ) + Nwk_ManGraphHashEdge( p, Nwk_ObjId(pLut), Nwk_ObjId(pCand) ); + // print statistics about this node + if ( pPars->fVeryVerbose ) + printf( "Node %6d : Fanins = %d. Fanouts = %3d. Cand1 = %3d. Cand2 = %3d.\n", + Nwk_ObjId(pLut), Nwk_ObjFaninNum(pLut), Nwk_ObjFaninNum(pLut), + Vec_PtrSize(vCands1), Vec_PtrSize(vCands2) ); + } + Vec_PtrFree( vStart ); + Vec_PtrFree( vNext ); + Vec_PtrFree( vCands1 ); + Vec_PtrFree( vCands2 ); + if ( pPars->fVerbose ) + { + printf( "Mergable LUTs = %6d. Total cands = %6d. ", p->nVertsMax, nCands ); + PRT( "Deriving graph", clock() - clk ); + } + // solve the graph problem + clk = clock(); + Nwk_ManGraphSolve( p ); + if ( pPars->fVerbose ) + { + printf( "GRAPH: Nodes = %6d. Edges = %6d. Pairs = %6d. ", + p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 ); + PRT( "Solving", clock() - clk ); + Nwk_ManGraphReportMemoryUsage( p ); + } + vResult = p->vPairs; p->vPairs = NULL; + Nwk_ManGraphFree( p ); + return vResult; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/nwk2/nwkMerge.h b/src/aig/nwk2/nwkMerge.h new file mode 100644 index 00000000..df426681 --- /dev/null +++ b/src/aig/nwk2/nwkMerge.h @@ -0,0 +1,149 @@ +/**CFile**************************************************************** + + FileName [nwkMerge.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Logic network representation.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwkMerge.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $] + +***********************************************************************/ + +#ifndef __NWK_MERGE_H__ +#define __NWK_MERGE_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +#define NWK_MAX_LIST 16 + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// the LUT merging parameters +typedef struct Nwk_LMPars_t_ Nwk_LMPars_t; +struct Nwk_LMPars_t_ +{ + int nMaxLutSize; // the max LUT size for merging (N=5) + int nMaxSuppSize; // the max total support size after merging (S=5) + int nMaxDistance; // the max number of nodes separating LUTs + int nMaxLevelDiff; // the max difference in levels + int nMaxFanout; // the max number of fanouts to traverse + int fUseDiffSupp; // enables the use of nodes with different support + int fUseTfiTfo; // enables the use of TFO/TFO nodes as candidates + int fVeryVerbose; // enables additional verbose output + int fVerbose; // enables verbose output +}; + +// edge of the graph +typedef struct Nwk_Edg_t_ Nwk_Edg_t; +struct Nwk_Edg_t_ +{ + int iNode1; // the first node + int iNode2; // the second node + Nwk_Edg_t * pNext; // the next edge +}; + +// vertex of the graph +typedef struct Nwk_Vrt_t_ Nwk_Vrt_t; +struct Nwk_Vrt_t_ +{ + int Id; // the vertex number + int iPrev; // the previous vertex in the list + int iNext; // the next vertex in the list + int nEdges; // the number of edges + int pEdges[0]; // the array of edges +}; + +// the connectivity graph +typedef struct Nwk_Grf_t_ Nwk_Grf_t; +struct Nwk_Grf_t_ +{ + // preliminary graph representation + int nObjs; // the number of objects + int nVertsMax; // the upper bound on the number of vertices + int nEdgeHash; // an approximate number of edges + Nwk_Edg_t ** pEdgeHash; // hash table for edges + Aig_MmFixed_t * pMemEdges; // memory for edges + // graph representation + int nEdges; // the number of edges + int nVerts; // the number of vertices + Nwk_Vrt_t ** pVerts; // the array of vertices + Aig_MmFlex_t * pMemVerts; // memory for vertices + // intermediate data + int pLists1[NWK_MAX_LIST+1]; // lists of nodes with one edge + int pLists2[NWK_MAX_LIST+1]; // lists of nodes with more than one edge + // the results of matching + Vec_Int_t * vPairs; // pairs matched in the graph + // object mappings + int * pMapLut2Id; // LUT numbers into vertex IDs + int * pMapId2Lut; // vertex IDs into LUT numbers + // other things + int nMemBytes1; // memory usage in bytes + int nMemBytes2; // memory usage in bytes +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#define Nwk_GraphForEachEdge( p, pEdge, k ) \ + for ( k = 0; k < p->nEdgeHash; k++ ) \ + for ( pEdge = p->pEdgeHash[k]; pEdge; pEdge = pEdge->pNext ) + +#define Nwk_ListForEachVertex( p, List, pVrt ) \ + for ( pVrt = List? p->pVerts[List] : NULL; pVrt; \ + pVrt = pVrt->iNext? p->pVerts[pVrt->iNext] : NULL ) + +#define Nwk_VertexForEachAdjacent( p, pVrt, pNext, k ) \ + for ( k = 0; (k < pVrt->nEdges) && (((pNext) = p->pVerts[pVrt->pEdges[k]]), 1); k++ ) + +//////////////////////////////////////////////////////////////////////// +/// INLINED FUNCTIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== nwkMerge.c ==========================================================*/ +extern Nwk_Grf_t * Nwk_ManGraphAlloc( int nVertsMax ); +extern void Nwk_ManGraphFree( Nwk_Grf_t * p ); +extern void Nwk_ManGraphReportMemoryUsage( Nwk_Grf_t * p ); +extern void Nwk_ManGraphHashEdge( Nwk_Grf_t * p, int iLut1, int iLut2 ); +extern void Nwk_ManGraphSolve( Nwk_Grf_t * p ); +extern int Nwk_ManLutMergeGraphTest( char * pFileName ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/nwk2/nwkObj.c b/src/aig/nwk2/nwkObj.c new file mode 100644 index 00000000..58587f07 --- /dev/null +++ b/src/aig/nwk2/nwkObj.c @@ -0,0 +1,199 @@ +/**CFile**************************************************************** + + FileName [nwkObj.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Logic network representation.] + + Synopsis [Manipulation of objects.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwkObj.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "nwk.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates an object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Obj_t * Nwk_ManCreateObj( Nwk_Man_t * p, int nFanins, int nFanouts ) +{ + Nwk_Obj_t * pObj; + pObj = (Nwk_Obj_t *)Aig_MmFlexEntryFetch( p->pMemObjs, sizeof(Nwk_Obj_t) + (nFanins + nFanouts + p->nFanioPlus) * sizeof(Nwk_Obj_t *) ); + memset( pObj, 0, sizeof(Nwk_Obj_t) ); + pObj->pFanio = (Nwk_Obj_t **)((char *)pObj + sizeof(Nwk_Obj_t)); + pObj->Id = Vec_PtrSize( p->vObjs ); + Vec_PtrPush( p->vObjs, pObj ); + pObj->pMan = p; + pObj->nFanioAlloc = nFanins + nFanouts + p->nFanioPlus; + return pObj; +} + + +/**Function************************************************************* + + Synopsis [Creates a primary input.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Obj_t * Nwk_ManCreateCi( Nwk_Man_t * p, int nFanouts ) +{ + Nwk_Obj_t * pObj; + pObj = Nwk_ManCreateObj( p, 1, nFanouts ); + pObj->PioId = Vec_PtrSize( p->vCis ); + Vec_PtrPush( p->vCis, pObj ); + pObj->Type = NWK_OBJ_CI; + p->nObjs[NWK_OBJ_CI]++; + return pObj; +} + +/**Function************************************************************* + + Synopsis [Creates a primary output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Obj_t * Nwk_ManCreateCo( Nwk_Man_t * p ) +{ + Nwk_Obj_t * pObj; + pObj = Nwk_ManCreateObj( p, 1, 1 ); + pObj->PioId = Vec_PtrSize( p->vCos ); + Vec_PtrPush( p->vCos, pObj ); + pObj->Type = NWK_OBJ_CO; + p->nObjs[NWK_OBJ_CO]++; + return pObj; +} + +/**Function************************************************************* + + Synopsis [Creates a latch.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Obj_t * Nwk_ManCreateLatch( Nwk_Man_t * p ) +{ + Nwk_Obj_t * pObj; + pObj = Nwk_ManCreateObj( p, 1, 1 ); + pObj->Type = NWK_OBJ_LATCH; + p->nObjs[NWK_OBJ_LATCH]++; + return pObj; +} + +/**Function************************************************************* + + Synopsis [Creates a node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Nwk_Obj_t * Nwk_ManCreateNode( Nwk_Man_t * p, int nFanins, int nFanouts ) +{ + Nwk_Obj_t * pObj; + pObj = Nwk_ManCreateObj( p, nFanins, nFanouts ); + pObj->Type = NWK_OBJ_NODE; + p->nObjs[NWK_OBJ_NODE]++; + return pObj; +} + + +/**Function************************************************************* + + Synopsis [Deletes the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManDeleteNode( Nwk_Obj_t * pObj ) +{ + Vec_Ptr_t * vNodes = pObj->pMan->vTemp; + Nwk_Obj_t * pTemp; + int i; + assert( Nwk_ObjFanoutNum(pObj) == 0 ); + // delete fanins + Nwk_ObjCollectFanins( pObj, vNodes ); + Vec_PtrForEachEntry( vNodes, pTemp, i ) + Nwk_ObjDeleteFanin( pObj, pTemp ); + // remove from the list of objects + Vec_PtrWriteEntry( pObj->pMan->vObjs, pObj->Id, NULL ); + pObj->pMan->nObjs[pObj->Type]--; + memset( pObj, 0, sizeof(Nwk_Obj_t) ); + pObj->Id = -1; +} + +/**Function************************************************************* + + Synopsis [Deletes the node and MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj ) +{ + Vec_Ptr_t * vNodes; + int i; + assert( !Nwk_ObjIsCi(pObj) ); + assert( Nwk_ObjFanoutNum(pObj) == 0 ); + vNodes = Vec_PtrAlloc( 100 ); + Nwk_ObjCollectFanins( pObj, vNodes ); + Nwk_ManDeleteNode( pObj ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + if ( Nwk_ObjIsNode(pObj) && Nwk_ObjFanoutNum(pObj) == 0 ) + Nwk_ManDeleteNode_rec( pObj ); + Vec_PtrFree( vNodes ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/nwk2/nwkUtil.c b/src/aig/nwk2/nwkUtil.c new file mode 100644 index 00000000..d6daca4e --- /dev/null +++ b/src/aig/nwk2/nwkUtil.c @@ -0,0 +1,515 @@ +/**CFile**************************************************************** + + FileName [nwkUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Logic network representation.] + + Synopsis [Various utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwkUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "nwk.h" +#include "kit.h" +#include <math.h> + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Increments the current traversal ID of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pObj; + int i; + if ( pNtk->nTravIds >= (1<<26)-1 ) + { + pNtk->nTravIds = 0; + Nwk_ManForEachObj( pNtk, pObj, i ) + pObj->TravId = 0; + } + pNtk->nTravIds++; +} + +/**Function************************************************************* + + Synopsis [Reads the maximum number of fanins of a node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManGetFaninMax( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pNode; + int i, nFaninsMax = 0; + Nwk_ManForEachNode( pNtk, pNode, i ) + { + if ( nFaninsMax < Nwk_ObjFaninNum(pNode) ) + nFaninsMax = Nwk_ObjFaninNum(pNode); + } + return nFaninsMax; +} + +/**Function************************************************************* + + Synopsis [Reads the total number of all fanins.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pNode; + int i, nFanins = 0; + Nwk_ManForEachNode( pNtk, pNode, i ) + nFanins += Nwk_ObjFaninNum(pNode); + return nFanins; +} + + +/**Function************************************************************* + + Synopsis [Returns the number of true PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManPiNum( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pNode; + int i, Counter = 0; + Nwk_ManForEachCi( pNtk, pNode, i ) + Counter += Nwk_ObjIsPi( pNode ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns the number of true POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManPoNum( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pNode; + int i, Counter = 0; + Nwk_ManForEachCo( pNtk, pNode, i ) + Counter += Nwk_ObjIsPo( pNode ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Reads the number of AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pNode; + int i, nNodes = 0; + Nwk_ManForEachNode( pNtk, pNode, i ) + { + if ( pNode->pFunc == NULL ) + { + printf( "Nwk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.\n", pNode->Id ); + continue; + } + if ( Nwk_ObjFaninNum(pNode) < 2 ) + continue; + nNodes += Hop_DagSize( pNode->pFunc ); + } + return nNodes; +} + +/**Function************************************************************* + + Synopsis [Procedure used for sorting the nodes in increasing order of levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 ) +{ + int Diff = (*pp1)->Level - (*pp2)->Level; + if ( Diff < 0 ) + return -1; + if ( Diff > 0 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Procedure used for sorting the nodes in decreasing order of levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 ) +{ + int Diff = (*pp1)->Level - (*pp2)->Level; + if ( Diff > 0 ) + return -1; + if ( Diff < 0 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Prints the objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ObjPrint( Nwk_Obj_t * pObj ) +{ + Nwk_Obj_t * pNext; + int i; + printf( "ObjId = %5d. ", pObj->Id ); + if ( Nwk_ObjIsPi(pObj) ) + printf( "PI" ); + if ( Nwk_ObjIsPo(pObj) ) + printf( "PO" ); + if ( Nwk_ObjIsNode(pObj) ) + printf( "Node" ); + printf( " Fanins = " ); + Nwk_ObjForEachFanin( pObj, pNext, i ) + printf( "%d ", pNext->Id ); + printf( " Fanouts = " ); + Nwk_ObjForEachFanout( pObj, pNext, i ) + printf( "%d ", pNext->Id ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Dumps the BLIF file for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames ) +{ + FILE * pFile; + Vec_Ptr_t * vNodes; + Vec_Int_t * vTruth; + Vec_Int_t * vCover; + Nwk_Obj_t * pObj, * pFanin; + Aig_MmFlex_t * pMem; + char * pSop = NULL; + unsigned * pTruth; + int i, k, nDigits; + if ( Nwk_ManPoNum(pNtk) == 0 ) + { + printf( "Nwk_ManDumpBlif(): Network does not have POs.\n" ); + return; + } + // collect nodes in the DFS order + nDigits = Aig_Base10Log( Nwk_ManObjNumMax(pNtk) ); + // write the file + pFile = fopen( pFileName, "w" ); + fprintf( pFile, "# BLIF file written by procedure Nwk_ManDumpBlif()\n" ); +// fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" ); + fprintf( pFile, ".model %s\n", pNtk->pName ); + // write PIs + fprintf( pFile, ".inputs" ); + Nwk_ManForEachCi( pNtk, pObj, i ) + if ( vPiNames ) + fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, i) ); + else + fprintf( pFile, " n%0*d", nDigits, pObj->Id ); + fprintf( pFile, "\n" ); + // write POs + fprintf( pFile, ".outputs" ); + Nwk_ManForEachCo( pNtk, pObj, i ) + if ( vPoNames ) + fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, i) ); + else + fprintf( pFile, " n%0*d", nDigits, pObj->Id ); + fprintf( pFile, "\n" ); + // write nodes + pMem = Aig_MmFlexStart(); + vTruth = Vec_IntAlloc( 1 << 16 ); + vCover = Vec_IntAlloc( 1 << 16 ); + vNodes = Nwk_ManDfs( pNtk ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + if ( !Nwk_ObjIsNode(pObj) ) + continue; + // derive SOP for the AIG + pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 ); + if ( Hop_IsComplement(pObj->pFunc) ) + Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) ); + pSop = Kit_PlaFromTruth( pMem, pTruth, Nwk_ObjFaninNum(pObj), vCover ); + // write the node + fprintf( pFile, ".names" ); + if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) ) + { + Nwk_ObjForEachFanin( pObj, pFanin, k ) + if ( vPiNames && Nwk_ObjIsPi(pFanin) ) + fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(pFanin)) ); + else + fprintf( pFile, " n%0*d", nDigits, pFanin->Id ); + } + fprintf( pFile, " n%0*d\n", nDigits, pObj->Id ); + // write the function + fprintf( pFile, "%s", pSop ); + } + Vec_IntFree( vCover ); + Vec_IntFree( vTruth ); + Vec_PtrFree( vNodes ); + Aig_MmFlexStop( pMem, 0 ); + // write POs + Nwk_ManForEachCo( pNtk, pObj, i ) + { + fprintf( pFile, ".names" ); + if ( vPiNames && Nwk_ObjIsPi(Nwk_ObjFanin0(pObj)) ) + fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(Nwk_ObjFanin0(pObj))) ); + else + fprintf( pFile, " n%0*d", nDigits, Nwk_ObjFanin0(pObj)->Id ); + if ( vPoNames ) + fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Nwk_ObjPioNum(pObj)) ); + else + fprintf( pFile, " n%0*d\n", nDigits, pObj->Id ); + fprintf( pFile, "%d 1\n", !pObj->fInvert ); + } + fprintf( pFile, ".end\n\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Prints the distribution of fanins/fanouts in the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk ) +{ + char Buffer[100]; + Nwk_Obj_t * pNode; + Vec_Int_t * vFanins, * vFanouts; + int nFanins, nFanouts, nFaninsMax, nFanoutsMax, nFaninsAll, nFanoutsAll; + int i, k, nSizeMax; + + // determine the largest fanin and fanout + nFaninsMax = nFanoutsMax = 0; + nFaninsAll = nFanoutsAll = 0; + Nwk_ManForEachNode( pNtk, pNode, i ) + { + nFanins = Nwk_ObjFaninNum(pNode); + nFanouts = Nwk_ObjFanoutNum(pNode); + nFaninsAll += nFanins; + nFanoutsAll += nFanouts; + nFaninsMax = AIG_MAX( nFaninsMax, nFanins ); + nFanoutsMax = AIG_MAX( nFanoutsMax, nFanouts ); + } + + // allocate storage for fanin/fanout numbers + nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) ); + vFanins = Vec_IntStart( nSizeMax ); + vFanouts = Vec_IntStart( nSizeMax ); + + // count the number of fanins and fanouts + Nwk_ManForEachNode( pNtk, pNode, i ) + { + nFanins = Nwk_ObjFaninNum(pNode); + nFanouts = Nwk_ObjFanoutNum(pNode); +// nFanouts = Nwk_NodeMffcSize(pNode); + + if ( nFanins < 10 ) + Vec_IntAddToEntry( vFanins, nFanins, 1 ); + else if ( nFanins < 100 ) + Vec_IntAddToEntry( vFanins, 10 + nFanins/10, 1 ); + else if ( nFanins < 1000 ) + Vec_IntAddToEntry( vFanins, 20 + nFanins/100, 1 ); + else if ( nFanins < 10000 ) + Vec_IntAddToEntry( vFanins, 30 + nFanins/1000, 1 ); + else if ( nFanins < 100000 ) + Vec_IntAddToEntry( vFanins, 40 + nFanins/10000, 1 ); + else if ( nFanins < 1000000 ) + Vec_IntAddToEntry( vFanins, 50 + nFanins/100000, 1 ); + else if ( nFanins < 10000000 ) + Vec_IntAddToEntry( vFanins, 60 + nFanins/1000000, 1 ); + + if ( nFanouts < 10 ) + Vec_IntAddToEntry( vFanouts, nFanouts, 1 ); + else if ( nFanouts < 100 ) + Vec_IntAddToEntry( vFanouts, 10 + nFanouts/10, 1 ); + else if ( nFanouts < 1000 ) + Vec_IntAddToEntry( vFanouts, 20 + nFanouts/100, 1 ); + else if ( nFanouts < 10000 ) + Vec_IntAddToEntry( vFanouts, 30 + nFanouts/1000, 1 ); + else if ( nFanouts < 100000 ) + Vec_IntAddToEntry( vFanouts, 40 + nFanouts/10000, 1 ); + else if ( nFanouts < 1000000 ) + Vec_IntAddToEntry( vFanouts, 50 + nFanouts/100000, 1 ); + else if ( nFanouts < 10000000 ) + Vec_IntAddToEntry( vFanouts, 60 + nFanouts/1000000, 1 ); + } + + printf( "The distribution of fanins and fanouts in the network:\n" ); + printf( " Number Nodes with fanin Nodes with fanout\n" ); + for ( k = 0; k < nSizeMax; k++ ) + { + if ( vFanins->pArray[k] == 0 && vFanouts->pArray[k] == 0 ) + continue; + if ( k < 10 ) + printf( "%15d : ", k ); + else + { + sprintf( Buffer, "%d - %d", (int)pow(10, k/10) * (k%10), (int)pow(10, k/10) * (k%10+1) - 1 ); + printf( "%15s : ", Buffer ); + } + if ( vFanins->pArray[k] == 0 ) + printf( " " ); + else + printf( "%12d ", vFanins->pArray[k] ); + printf( " " ); + if ( vFanouts->pArray[k] == 0 ) + printf( " " ); + else + printf( "%12d ", vFanouts->pArray[k] ); + printf( "\n" ); + } + Vec_IntFree( vFanins ); + Vec_IntFree( vFanouts ); + + printf( "Fanins: Max = %d. Ave = %.2f. Fanouts: Max = %d. Ave = %.2f.\n", + nFaninsMax, 1.0*nFaninsAll/Nwk_ManNodeNum(pNtk), + nFanoutsMax, 1.0*nFanoutsAll/Nwk_ManNodeNum(pNtk) ); +} + +/**Function************************************************************* + + Synopsis [Cleans the temporary marks of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManCleanMarks( Nwk_Man_t * pMan ) +{ + Nwk_Obj_t * pObj; + int i; + Nwk_ManForEachObj( pMan, pObj, i ) + pObj->MarkA = pObj->MarkB = 0; +} + +/**Function************************************************************* + + Synopsis [Minimizes the support of all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ) +{ + unsigned * pTruth; + Vec_Int_t * vTruth; + Nwk_Obj_t * pObj, * pFanin, * pObjNew; + int uSupp, nSuppSize, i, k, Counter = 0; + vTruth = Vec_IntAlloc( 1 << 16 ); + Nwk_ManForEachNode( pNtk, pObj, i ) + { + pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 ); + nSuppSize = Kit_TruthSupportSize(pTruth, Nwk_ObjFaninNum(pObj)); + if ( nSuppSize == Nwk_ObjFaninNum(pObj) ) + continue; + Counter++; + uSupp = Kit_TruthSupport( pTruth, Nwk_ObjFaninNum(pObj) ); + // create new node with the given support + pObjNew = Nwk_ManCreateNode( pNtk, nSuppSize, Nwk_ObjFanoutNum(pObj) ); + Nwk_ObjForEachFanin( pObj, pFanin, k ) + if ( uSupp & (1 << k) ) + Nwk_ObjAddFanin( pObjNew, pFanin ); + pObjNew->pFunc = Hop_Remap( pNtk->pManHop, pObj->pFunc, uSupp, Nwk_ObjFaninNum(pObj) ); + if ( fVerbose ) + printf( "Reducing node %d fanins from %d to %d.\n", + pObj->Id, Nwk_ObjFaninNum(pObj), Nwk_ObjFaninNum(pObjNew) ); + Nwk_ObjReplace( pObj, pObjNew ); + } + if ( fVerbose && Counter ) + printf( "Support minimization reduced support of %d nodes.\n", Counter ); + Vec_IntFree( vTruth ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/nwk2/nwk_.c b/src/aig/nwk2/nwk_.c new file mode 100644 index 00000000..81cffbbf --- /dev/null +++ b/src/aig/nwk2/nwk_.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [nwk_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: nwk_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "nwk.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index f3bd028a..08275ff3 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -85,7 +85,7 @@ extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); /*=== saigInter.c ==========================================================*/ -extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth ); +extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose, int * pDepth ); /*=== saigMiter.c ==========================================================*/ extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); /*=== saigPhase.c ==========================================================*/ diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index ae8d02ec..527f372d 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -336,6 +336,68 @@ sat_solver * Saig_DeriveSatSolver( /**Function************************************************************* + Synopsis [Checks constainment of two interpolants.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ) +{ + Aig_Man_t * pMiter, * pAigTemp; + int RetValue; + pMiter = Aig_ManCreateMiter( pNew, pOld, 1 ); +// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); +// Aig_ManStop( pAigTemp ); + RetValue = Fra_FraigMiterStatus( pMiter ); + if ( RetValue == -1 ) + { + pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); + RetValue = Fra_FraigMiterStatus( pAigTemp ); + Aig_ManStop( pAigTemp ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); + } + assert( RetValue != -1 ); + Aig_ManStop( pMiter ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Checks constainment of two interpolants.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld ) +{ + Aig_Man_t * pMiter, * pAigTemp; + int RetValue; + pMiter = Aig_ManCreateMiter( pNew, pOld, 0 ); +// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); +// Aig_ManStop( pAigTemp ); + RetValue = Fra_FraigMiterStatus( pMiter ); + if ( RetValue == -1 ) + { + pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); + RetValue = Fra_FraigMiterStatus( pAigTemp ); + Aig_ManStop( pAigTemp ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); + } + assert( RetValue != -1 ); + Aig_ManStop( pMiter ); + return RetValue; +} + +/**Function************************************************************* + Synopsis [Performs one SAT run with interpolation.] Description [Returns 1 if proven. 0 if failed. -1 if undecided.] @@ -345,11 +407,12 @@ sat_solver * Saig_DeriveSatSolver( SeeAlso [] ***********************************************************************/ -int Saig_PerformOneStep( Saig_IntMan_t * p ) +int Saig_PerformOneStep_old( Saig_IntMan_t * p, int fUseIp ) { sat_solver * pSat; void * pSatCnf = NULL; - Inta_Man_t * pManInter; + Inta_Man_t * pManInterA; + Intb_Man_t * pManInterB; int clk, status, RetValue; assert( p->pInterNew == NULL ); @@ -380,9 +443,18 @@ p->timeSat += clock() - clk; // create the resulting manager clk = clock(); - pManInter = Inta_ManAlloc(); - p->pInterNew = Inta_ManInterpolate( pManInter, pSatCnf, p->vVarsAB, 0 ); - Inta_ManFree( pManInter ); + if ( !fUseIp ) + { + pManInterA = Inta_ManAlloc(); + p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); + Inta_ManFree( pManInterA ); + } + else + { + pManInterB = Intb_ManAlloc(); + p->pInterNew = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 ); + Intb_ManFree( pManInterB ); + } p->timeInt += clock() - clk; Sto_ManFree( pSatCnf ); return RetValue; @@ -390,7 +462,7 @@ p->timeInt += clock() - clk; /**Function************************************************************* - Synopsis [Checks constainment of two interpolants.] + Synopsis [] Description [] @@ -399,23 +471,192 @@ p->timeInt += clock() - clk; SeeAlso [] ***********************************************************************/ -int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ) +Aig_Man_t * Aig_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther ) { - Aig_Man_t * pMiter, * pAigTemp; - int RetValue; - pMiter = Aig_ManCreateMiter( pNew, pOld, 1 ); -// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); -// Aig_ManStop( pAigTemp ); - RetValue = Fra_FraigMiterStatus( pMiter ); - if ( RetValue == -1 ) + Aig_Man_t * pInterC; + assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) ); + pInterC = Aig_ManDupSimple( pInter ); + Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 ); + assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) ); + return pInterC; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_VerifyInterpolant1( Inta_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter ) +{ + extern Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ); + Aig_Man_t * pLower, * pUpper, * pInterC; + int RetValue1, RetValue2; + + pLower = Inta_ManDeriveClauses( pMan, pCnf, 1 ); + pUpper = Inta_ManDeriveClauses( pMan, pCnf, 0 ); + Aig_ManFlipFirstPo( pUpper ); + + pInterC = Aig_ManDupExpand( pInter, pLower ); + RetValue1 = Saig_ManCheckContainment( pLower, pInterC ); + Aig_ManStop( pInterC ); + + pInterC = Aig_ManDupExpand( pInter, pUpper ); + RetValue2 = Saig_ManCheckContainment( pInterC, pUpper ); + Aig_ManStop( pInterC ); + + if ( RetValue1 && RetValue2 ) + printf( "Im is correct.\n" ); + if ( !RetValue1 ) + printf( "Property A => Im fails.\n" ); + if ( !RetValue2 ) + printf( "Property Im => !B fails.\n" ); + + Aig_ManStop( pLower ); + Aig_ManStop( pUpper ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_VerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter ) +{ + extern Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ); + Aig_Man_t * pLower, * pUpper, * pInterC; + int RetValue1, RetValue2; + + pLower = Intb_ManDeriveClauses( pMan, pCnf, 1 ); + pUpper = Intb_ManDeriveClauses( pMan, pCnf, 0 ); + Aig_ManFlipFirstPo( pUpper ); + + pInterC = Aig_ManDupExpand( pInter, pLower ); +//Aig_ManPrintStats( pLower ); +//Aig_ManPrintStats( pUpper ); +//Aig_ManPrintStats( pInterC ); +//Aig_ManDumpBlif( pInterC, "inter_c.blif", NULL, NULL ); + RetValue1 = Saig_ManCheckContainment( pLower, pInterC ); + Aig_ManStop( pInterC ); + + pInterC = Aig_ManDupExpand( pInter, pUpper ); + RetValue2 = Saig_ManCheckContainment( pInterC, pUpper ); + Aig_ManStop( pInterC ); + + if ( RetValue1 && RetValue2 ) + printf( "Ip is correct.\n" ); + if ( !RetValue1 ) + printf( "Property A => Ip fails.\n" ); + if ( !RetValue2 ) + printf( "Property Ip => !B fails.\n" ); + + Aig_ManStop( pLower ); + Aig_ManStop( pUpper ); +} + +/**Function************************************************************* + + Synopsis [Performs one SAT run with interpolation.] + + Description [Returns 1 if proven. 0 if failed. -1 if undecided.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_PerformOneStep( Saig_IntMan_t * p, int fUseIp ) +{ + sat_solver * pSat; + void * pSatCnf = NULL; + Inta_Man_t * pManInterA; + Intb_Man_t * pManInterB; + int clk, status, RetValue; + assert( p->pInterNew == NULL ); + + // derive the SAT solver + pSat = Saig_DeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB ); +//Sat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 1 ); + // solve the problem +clk = clock(); + status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + p->nConfCur = pSat->stats.conflicts; +p->timeSat += clock() - clk; + if ( status == l_False ) { - pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); - RetValue = Fra_FraigMiterStatus( pAigTemp ); - Aig_ManStop( pAigTemp ); -// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); + pSatCnf = sat_solver_store_release( pSat ); + RetValue = 1; } - assert( RetValue != -1 ); - Aig_ManStop( pMiter ); + else if ( status == l_True ) + { + RetValue = 0; + } + else + { + RetValue = -1; + } + sat_solver_delete( pSat ); + if ( pSatCnf == NULL ) + return RetValue; + + // create the resulting manager +clk = clock(); + if ( !fUseIp ) + { + pManInterA = Inta_ManAlloc(); + p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); + Inta_ManFree( pManInterA ); + } + else + { + Aig_Man_t * pInterNew2; + int RetValue; + + pManInterA = Inta_ManAlloc(); + p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); +// Saig_VerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew ); + Inta_ManFree( pManInterA ); + + pManInterB = Intb_ManAlloc(); + pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 ); + Saig_VerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 ); + Intb_ManFree( pManInterB ); + + // check relationship + RetValue = Saig_ManCheckEquivalence( pInterNew2, p->pInterNew ); + if ( RetValue ) + printf( "Equivalence \"Ip == Im\" holds\n" ); + else + { +// printf( "Equivalence \"Ip == Im\" does not hold\n" ); + RetValue = Saig_ManCheckContainment( pInterNew2, p->pInterNew ); + if ( RetValue ) + printf( "Containment \"Ip -> Im\" holds\n" ); + else + printf( "Containment \"Ip -> Im\" does not hold\n" ); + + RetValue = Saig_ManCheckContainment( p->pInterNew, pInterNew2 ); + if ( RetValue ) + printf( "Containment \"Im -> Ip\" holds\n" ); + else + printf( "Containment \"Im -> Ip\" does not hold\n" ); + } + + Aig_ManStop( pInterNew2 ); + } +p->timeInt += clock() - clk; + Sto_ManFree( pSatCnf ); return RetValue; } @@ -497,7 +738,7 @@ void Saig_ManagerFree( Saig_IntMan_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth ) +int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUseIp, int fVerbose, int * pDepth ) { Saig_IntMan_t * p; Aig_Man_t * pAigTemp; @@ -578,7 +819,7 @@ p->timeCnf += clock() - clk; } // perform interplation clk = clock(); - RetValue = Saig_PerformOneStep( p ); + RetValue = Saig_PerformOneStep( p, fUseIp ); if ( fVerbose ) { printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ", diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index aa8d6b30..d1aa2c82 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -297,6 +297,7 @@ void Abc_FrameClearDesign() void Abc_Init( Abc_Frame_t * pAbc ) { // Abc_NtkBddImplicationTest(); +// Ply_LutPairTest(); Cmd_CommandAdd( pAbc, "Printing", "print_stats", Abc_CommandPrintStats, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_exdc", Abc_CommandPrintExdc, 0 ); @@ -7072,6 +7073,9 @@ int Abc_CommandEspresso( Abc_Frame_t * pAbc, int argc, char ** argv ) pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); + printf( "This command is currently disabled.\n" ); + return 0; + // set defaults fVerbose = 0; Extra_UtilGetoptReset(); @@ -7098,7 +7102,7 @@ int Abc_CommandEspresso( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "SOP minimization is possible for logic networks (run \"renode\").\n" ); return 1; } - Abc_NtkEspresso( pNtk, fVerbose ); +// Abc_NtkEspresso( pNtk, fVerbose ); return 0; usage: @@ -7764,6 +7768,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } */ + + /* // pNtkRes = Abc_NtkDar( pNtk ); // pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); @@ -7776,8 +7782,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; */ + // Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose ); /* if ( globalUtilOptind != 1 ) @@ -15337,9 +15345,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) int nBTLimit; int fRewrite; int fTransLoop; + int fUsePudlak; int fVerbose; - extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose ); + extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -15349,9 +15358,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) nBTLimit = 20000; fRewrite = 0; fTransLoop = 1; + fUsePudlak = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Crtvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Crtpvh" ) ) != EOF ) { switch ( c ) { @@ -15372,6 +15382,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': fTransLoop ^= 1; break; + case 'p': + fUsePudlak ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -15401,15 +15414,16 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" ); return 0; } - Abc_NtkDarBmcInter( pNtk, nBTLimit, fRewrite, fTransLoop, fVerbose ); + Abc_NtkDarBmcInter( pNtk, nBTLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose ); return 0; usage: - fprintf( pErr, "usage: int [-C num] [-rtvh]\n" ); + fprintf( pErr, "usage: int [-C num] [-rtpvh]\n" ); fprintf( pErr, "\t uses interpolation to prove the property\n" ); fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit ); fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" ); + fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 2a234b68..a691a205 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1270,7 +1270,7 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose ) +int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose ) { Aig_Man_t * pMan; int RetValue, Depth, clk = clock(); @@ -1282,7 +1282,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTra return -1; } assert( pMan->nRegs > 0 ); - RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fVerbose, &Depth ); + RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose, &Depth ); if ( RetValue == 1 ) printf( "Property proved. " ); else if ( RetValue == 0 ) @@ -2148,12 +2148,12 @@ Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanu ***********************************************************************/ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ) { - extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); + extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ); Aig_Man_t * pMan; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return; - Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); + Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 ); Aig_ManStop( pMan ); } diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 777da95b..e83785fe 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -14,7 +14,6 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcDelay.c \ src/base/abci/abcDress.c \ src/base/abci/abcDsd.c \ - src/base/abci/abcEspresso.c \ src/base/abci/abcExtract.c \ src/base/abci/abcFpga.c \ src/base/abci/abcFpgaFast.c \ diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 88028105..54beb8b6 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -275,10 +275,16 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho fprintf( pFile, " Level%d;\n", Level ); Vec_PtrForEachEntry( vNodes, pNode, i ) { + int SuppSize; + Vec_Ptr_t * vSupp; if ( (int)pNode->Level != Level ) continue; if ( Abc_ObjFaninNum(pNode) == 0 ) continue; + vSupp = Abc_NtkNodeSupport( pNtk, &pNode, 1 ); + SuppSize = Vec_PtrSize( vSupp ); + Vec_PtrFree( vSupp ); + // fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); if ( Abc_NtkIsStrash(pNtk) ) pSopString = ""; @@ -288,7 +294,10 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData)); else pSopString = Abc_NtkPrintSop(pNode->pData); - fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString ); +// fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString ); + fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, + SuppSize, + pSopString ); fprintf( pFile, ", shape = ellipse" ); if ( pNode->fMarkB ) diff --git a/src/base/main/main.c b/src/base/main/main.c index 1f1f19ba..6f2e1d11 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -56,8 +56,10 @@ int main( int argc, char * argv[] ) // added to detect memory leaks: #ifdef _DEBUG +#ifdef ABC_CHECK_LEAKS _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF ); #endif +#endif // Npn_Experiment(); // Npn_Generate(); @@ -255,8 +257,10 @@ void Abc_Start() Abc_Frame_t * pAbc; // added to detect memory leaks: #ifdef _DEBUG +#ifdef ABC_CHECK_LEAKS _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF ); #endif +#endif // start the glocal frame pAbc = Abc_FrameGetGlobalFrame(); // source the resource file diff --git a/src/base/main/main.h b/src/base/main/main.h index 852b8f25..62dc394a 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -40,10 +40,6 @@ typedef struct Abc_Frame_t_ Abc_Frame_t; /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -// this include should be the first one in the list -// it is used to catch memory leaks on Windows -#include "leaks.h" - // data structure packages #include "extra.h" #include "vec.h" diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index eae8b7a6..462b5a02 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -114,8 +114,8 @@ Abc_Frame_t * Abc_FrameAllocate() // networks to be used by choice p->vStore = Vec_PtrAlloc( 16 ); // initialize decomposition manager - define_cube_size(20); - set_espresso_flags(); +// define_cube_size(20); +// set_espresso_flags(); // initialize the trace manager // Abc_HManStart(); return p; @@ -139,7 +139,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) extern void undefine_cube_size(); // extern void Ivy_TruthManStop(); // Abc_HManStop(); - undefine_cube_size(); +// undefine_cube_size(); Rwt_ManGlobalStop(); // Ivy_TruthManStop(); if ( p->pLibVer ) Abc_LibFree( p->pLibVer, NULL ); diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h index a308cbb3..f4145e7f 100644 --- a/src/map/fpga/fpgaInt.h +++ b/src/map/fpga/fpgaInt.h @@ -23,7 +23,6 @@ /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -//#include "leaks.h" #include <stdio.h> #include <stdlib.h> #include <string.h> diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h index 541077d5..00550deb 100644 --- a/src/map/mapper/mapperInt.h +++ b/src/map/mapper/mapperInt.h @@ -23,7 +23,6 @@ /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -//#include "leaks.h" #include <stdio.h> #include <stdlib.h> #include <string.h> diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 6b840024..f45afcbe 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -43,7 +43,9 @@ extern "C" { // this include should be the first one in the list // it is used to catch memory leaks on Windows +#ifdef ABC_CHECK_LEAKS #include "leaks.h" +#endif #include <stdio.h> #include <stdlib.h> diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h index ee82fc3e..03de79f1 100644 --- a/src/misc/vec/vec.h +++ b/src/misc/vec/vec.h @@ -50,7 +50,9 @@ typedef long long sint64; // this include should be the first one in the list // it is used to catch memory leaks on Windows +#ifdef ABC_CHECK_LEAKS #include "leaks.h" +#endif //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make index f6805600..4bc6eca7 100644 --- a/src/sat/bsat/module.make +++ b/src/sat/bsat/module.make @@ -1,6 +1,7 @@ SRC += src/sat/bsat/satMem.c \ src/sat/bsat/satInter.c \ src/sat/bsat/satInterA.c \ + src/sat/bsat/satInterB.c \ src/sat/bsat/satInterP.c \ src/sat/bsat/satSolver.c \ src/sat/bsat/satStore.c \ diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index dd884b3c..cc780580 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -965,6 +965,51 @@ p->timeTotal += clock() - clkTotal; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ) +{ + Aig_Man_t * p; + Aig_Obj_t * pMiter, * pSum, * pLit; + Sto_Cls_t * pClause; + int Var, VarAB, v; + p = Aig_ManStart( 10000 ); + pMiter = Aig_ManConst1(p); + Sto_ManForEachClauseRoot( pCnf, pClause ) + { + if ( fClausesA ^ pClause->fA ) // clause of B + continue; + // clause of A + pSum = Aig_ManConst0(p); + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( pMan->pVarTypes[Var] < 0 ) // global var + { + VarAB = -pMan->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) ); + pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) ); + } + else + pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) ); + pSum = Aig_Or( p, pSum, pLit ); + } + pMiter = Aig_And( p, pMiter, pSum ); + } + Aig_ObjCreatePo( p, pMiter ); + return p; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c new file mode 100644 index 00000000..e0f4328d --- /dev/null +++ b/src/sat/bsat/satInterB.c @@ -0,0 +1,1055 @@ +/**CFile**************************************************************** + + FileName [satInter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sat_solver.] + + Synopsis [Interpolation package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> +#include "satStore.h" +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// variable assignments +static const lit LIT_UNDEF = 0xffffffff; + +// interpolation manager +struct Intb_Man_t_ +{ + // clauses of the problems + Sto_Man_t * pCnf; // the set of CNF clauses for A and B + Vec_Int_t * vVarsAB; // the array of global variables + // various parameters + int fVerbose; // verbosiness flag + int fProofVerif; // verifies the proof + int fProofWrite; // writes the proof file + int nVarsAlloc; // the allocated size of var arrays + int nClosAlloc; // the allocated size of clause arrays + // internal BCP + int nRootSize; // the number of root level assignments + int nTrailSize; // the number of assignments made + lit * pTrail; // chronological order of assignments (size nVars) + lit * pAssigns; // assignments by variable (size nVars) + char * pSeens; // temporary mark (size nVars) + Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars) + Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) + // interpolation data + Aig_Man_t * pAig; // the AIG manager for recording the interpolant + int * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] + Aig_Obj_t ** pInters; // storage for interpolants as truth tables (size nClauses) + int nIntersAlloc; // the allocated size of truth table array + // proof recording + int Counter; // counter of resolved clauses + int * pProofNums; // the proof numbers for each clause (size nClauses) + FILE * pFile; // the file for proof recording + // internal verification + lit * pResLits; // the literals of the resolvent + int nResLits; // the number of literals of the resolvent + int nResLitsAlloc;// the number of literals of the resolvent + // runtime stats + int timeBcp; // the runtime for BCP + int timeTrace; // the runtime of trace construction + int timeTotal; // the total runtime of interpolation +}; + +// procedure to get hold of the clauses' truth table +static inline Aig_Obj_t ** Intb_ManAigRead( Intb_Man_t * pMan, Sto_Cls_t * pCls ) { return pMan->pInters + pCls->Id; } +static inline void Intb_ManAigClear( Intb_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst0(pMan->pAig); } +static inline void Intb_ManAigFill( Intb_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst1(pMan->pAig); } +static inline void Intb_ManAigCopy( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = *q; } +static inline void Intb_ManAigAnd( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_And(pMan->pAig, *p, *q); } +static inline void Intb_ManAigOr( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, *q); } +static inline void Intb_ManAigOrNot( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); } +static inline void Intb_ManAigOrVar( Intb_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v)); } +static inline void Intb_ManAigOrNotVar( Intb_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); } +static inline void Intb_ManAigMux0( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *q, *p); } +static inline void Intb_ManAigMux1( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *p, *q); } + +// reading/writing the proof for a clause +static inline int Intb_ManProofGet( Intb_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; } +static inline void Intb_ManProofSet( Intb_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Intb_Man_t * Intb_ManAlloc() +{ + Intb_Man_t * p; + // allocate the manager + p = (Intb_Man_t *)malloc( sizeof(Intb_Man_t) ); + memset( p, 0, sizeof(Intb_Man_t) ); + // verification + p->nResLitsAlloc = (1<<16); + p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); + // parameters + p->fProofWrite = 0; + p->fProofVerif = 1; + return p; +} + +/**Function************************************************************* + + Synopsis [Count common variables in the clauses of A and B.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManGlobalVars( Intb_Man_t * p ) +{ + Sto_Cls_t * pClause; + int LargeNum = -100000000; + int Var, nVarsAB, v; + + // mark the variable encountered in the clauses of A + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( !pClause->fA ) + break; + for ( v = 0; v < (int)pClause->nLits; v++ ) + p->pVarTypes[lit_var(pClause->pLits[v])] = 1; + } + + // check variables that appear in clauses of B + nVarsAB = 0; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( pClause->fA ) + continue; + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] == 1 ) // var of A + { + // change it into a global variable + nVarsAB++; + p->pVarTypes[Var] = LargeNum; + } + } + } + assert( nVarsAB <= Vec_IntSize(p->vVarsAB) ); + + // order global variables + nVarsAB = 0; + Vec_IntForEachEntry( p->vVarsAB, Var, v ) + p->pVarTypes[Var] = -(1+nVarsAB++); + + // check that there is no extra global variables + for ( v = 0; v < p->pCnf->nVars; v++ ) + assert( p->pVarTypes[v] != LargeNum ); + return nVarsAB; +} + +/**Function************************************************************* + + Synopsis [Resize proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManResize( Intb_Man_t * p ) +{ + // check if resizing is needed + if ( p->nVarsAlloc < p->pCnf->nVars ) + { + // find the new size + if ( p->nVarsAlloc == 0 ) + p->nVarsAlloc = 1; + while ( p->nVarsAlloc < p->pCnf->nVars ) + p->nVarsAlloc *= 2; + // resize the arrays + p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); + p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); + p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); + p->pVarTypes = (int *) realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc ); + p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc ); + p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 ); + } + + // clean the free space + memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); + memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); + memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); + memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars ); + memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 ); + + // compute the number of common variables + Intb_ManGlobalVars( p ); + + // check if resizing of clauses is needed + if ( p->nClosAlloc < p->pCnf->nClauses ) + { + // find the new size + if ( p->nClosAlloc == 0 ) + p->nClosAlloc = 1; + while ( p->nClosAlloc < p->pCnf->nClauses ) + p->nClosAlloc *= 2; + // resize the arrays + p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc ); + } + memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); + + // check if resizing of truth tables is needed + if ( p->nIntersAlloc < p->pCnf->nClauses ) + { + p->nIntersAlloc = p->pCnf->nClauses; + p->pInters = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * p->nIntersAlloc ); + } + memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses ); +} + +/**Function************************************************************* + + Synopsis [Deallocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManFree( Intb_Man_t * p ) +{ +/* + printf( "Runtime stats:\n" ); +PRT( "BCP ", p->timeBcp ); +PRT( "Trace ", p->timeTrace ); +PRT( "TOTAL ", p->timeTotal ); +*/ + free( p->pInters ); + free( p->pProofNums ); + free( p->pTrail ); + free( p->pAssigns ); + free( p->pSeens ); + free( p->pVarTypes ); + free( p->pReasons ); + free( p->pWatches ); + free( p->pResLits ); + free( p ); +} + + + + +/**Function************************************************************* + + Synopsis [Prints the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrintClause( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + int i; + printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Intb_ManProofGet(p, pClause) ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + printf( " %d", pClause->pLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the resolvent.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrintResolvent( lit * pResLits, int nResLits ) +{ + int i; + printf( "Resolvent: {" ); + for ( i = 0; i < nResLits; i++ ) + printf( " %d", pResLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the interpolant for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrintInterOne( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + printf( "Clause %2d : ", pClause->Id ); +// Extra_PrintBinary___( stdout, Intb_ManAigRead(p, pClause), (1 << p->nVarsAB) ); + printf( "\n" ); +} + + + +/**Function************************************************************* + + Synopsis [Adds one clause to the watcher list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Intb_ManWatchClause( Intb_Man_t * p, Sto_Cls_t * pClause, lit Lit ) +{ + assert( lit_check(Lit, p->pCnf->nVars) ); + if ( pClause->pLits[0] == Lit ) + pClause->pNext0 = p->pWatches[lit_neg(Lit)]; + else + { + assert( pClause->pLits[1] == Lit ); + pClause->pNext1 = p->pWatches[lit_neg(Lit)]; + } + p->pWatches[lit_neg(Lit)] = pClause; +} + + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Intb_ManEnqueue( Intb_Man_t * p, lit Lit, Sto_Cls_t * pReason ) +{ + int Var = lit_var(Lit); + if ( p->pAssigns[Var] != LIT_UNDEF ) + return p->pAssigns[Var] == Lit; + p->pAssigns[Var] = Lit; + p->pReasons[Var] = pReason; + p->pTrail[p->nTrailSize++] = Lit; +//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Intb_ManCancelUntil( Intb_Man_t * p, int Level ) +{ + lit Lit; + int i, Var; + for ( i = p->nTrailSize - 1; i >= Level; i-- ) + { + Lit = p->pTrail[i]; + Var = lit_var( Lit ); + p->pReasons[Var] = NULL; + p->pAssigns[Var] = LIT_UNDEF; +//printf( "cancelling var %d\n", Var ); + } + p->nTrailSize = Level; +} + +/**Function************************************************************* + + Synopsis [Propagate one assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Sto_Cls_t * Intb_ManPropagateOne( Intb_Man_t * p, lit Lit ) +{ + Sto_Cls_t ** ppPrev, * pCur, * pTemp; + lit LitF = lit_neg(Lit); + int i; + // iterate through the literals + ppPrev = p->pWatches + Lit; + for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev ) + { + // make sure the false literal is in the second literal of the clause + if ( pCur->pLits[0] == LitF ) + { + pCur->pLits[0] = pCur->pLits[1]; + pCur->pLits[1] = LitF; + pTemp = pCur->pNext0; + pCur->pNext0 = pCur->pNext1; + pCur->pNext1 = pTemp; + } + assert( pCur->pLits[1] == LitF ); + + // if the first literal is true, the clause is satisfied + if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // look for a new literal to watch + for ( i = 2; i < (int)pCur->nLits; i++ ) + { + // skip the case when the literal is false + if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) + continue; + // the literal is either true or unassigned - watch it + pCur->pLits[1] = pCur->pLits[i]; + pCur->pLits[i] = LitF; + // remove this clause from the watch list of Lit + *ppPrev = pCur->pNext1; + // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1]) + Intb_ManWatchClause( p, pCur, pCur->pLits[1] ); + break; + } + if ( i < (int)pCur->nLits ) // found new watch + continue; + + // clause is unit - enqueue new implication + if ( Intb_ManEnqueue(p, pCur->pLits[0], pCur) ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // conflict detected - return the conflict clause + return pCur; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Propagate the current assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sto_Cls_t * Intb_ManPropagate( Intb_Man_t * p, int Start ) +{ + Sto_Cls_t * pClause; + int i; + int clk = clock(); + for ( i = Start; i < p->nTrailSize; i++ ) + { + pClause = Intb_ManPropagateOne( p, p->pTrail[i] ); + if ( pClause ) + { +p->timeBcp += clock() - clk; + return pClause; + } + } +p->timeBcp += clock() - clk; + return NULL; +} + + +/**Function************************************************************* + + Synopsis [Writes one root clause into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManProofWriteOne( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + Intb_ManProofSet( p, pClause, ++p->Counter ); + + if ( p->fProofWrite ) + { + int v; + fprintf( p->pFile, "%d", Intb_ManProofGet(p, pClause) ); + for ( v = 0; v < (int)pClause->nLits; v++ ) + fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) ); + fprintf( p->pFile, " 0 0\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Traces the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManGetGlobalVar( Intb_Man_t * p, int Var ) +{ + int VarAB; + if ( p->pVarTypes[Var] >= 0 ) // global var + return -1; + VarAB = -p->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) ); + return VarAB; +} + + +/**Function************************************************************* + + Synopsis [Traces the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal ) +{ + Sto_Cls_t * pReason; + int i, v, Var, PrevId; + int fPrint = 0; + int clk = clock(); + + // collect resolvent literals + if ( p->fProofVerif ) + { + assert( (int)pConflict->nLits <= p->nResLitsAlloc ); + memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits ); + p->nResLits = pConflict->nLits; + } + + // mark all the variables in the conflict as seen + for ( v = 0; v < (int)pConflict->nLits; v++ ) + p->pSeens[lit_var(pConflict->pLits[v])] = 1; + + // start the anticedents +// pFinal->pAntis = Vec_PtrAlloc( 32 ); +// Vec_PtrPush( pFinal->pAntis, pConflict ); + + if ( p->pCnf->nClausesA ) + Intb_ManAigCopy( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pConflict) ); + + // follow the trail backwards + PrevId = Intb_ManProofGet(p, pConflict); + for ( i = p->nTrailSize - 1; i >= 0; i-- ) + { + // skip literals that are not involved + Var = lit_var(p->pTrail[i]); + if ( !p->pSeens[Var] ) + continue; + p->pSeens[Var] = 0; + + // skip literals of the resulting clause + pReason = p->pReasons[Var]; + if ( pReason == NULL ) + continue; + assert( p->pTrail[i] == pReason->pLits[0] ); + + // add the variables to seen + for ( v = 1; v < (int)pReason->nLits; v++ ) + p->pSeens[lit_var(pReason->pLits[v])] = 1; + + + // record the reason clause + assert( Intb_ManProofGet(p, pReason) > 0 ); + p->Counter++; + if ( p->fProofWrite ) + fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Intb_ManProofGet(p, pReason) ); + PrevId = p->Counter; + + if ( p->pCnf->nClausesA ) + { + if ( p->pVarTypes[Var] == 1 )// || rand() % 10 == 0 ) // var of A + Intb_ManAigOr( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason) ); + else if ( p->pVarTypes[Var] == 0 ) // var of B + Intb_ManAigAnd( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason) ); + else + { + int VarAB = Intb_ManGetGlobalVar(p, Var); + // check that the var is present in the reason + for ( v = 0; v < (int)pReason->nLits; v++ ) + if ( lit_var(pReason->pLits[v]) == Var ) + break; + assert( v < (int)pReason->nLits ); + if ( lit_sign(pReason->pLits[v]) ) // negative polarity + Intb_ManAigMux0( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason), VarAB ); + else + Intb_ManAigMux1( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason), VarAB ); + } + } + + // resolve the temporary resolvent with the reason clause + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Intb_ManPrintResolvent( p->pResLits, p->nResLits ); + // check that the var is present in the resolvent + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == Var ) + break; + if ( v1 == p->nResLits ) + printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var ); + if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) ) + printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var ); + // remove this variable from the resolvent + assert( lit_var(p->pResLits[v1]) == Var ); + p->nResLits--; + for ( ; v1 < p->nResLits; v1++ ) + p->pResLits[v1] = p->pResLits[v1+1]; + // add variables of the reason clause + for ( v2 = 1; v2 < (int)pReason->nLits; v2++ ) + { + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) ) + break; + // if it is a new variable, add it to the resolvent + if ( v1 == p->nResLits ) + { + if ( p->nResLits == p->nResLitsAlloc ) + printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id ); + p->pResLits[ p->nResLits++ ] = pReason->pLits[v2]; + continue; + } + // if the variable is the same, the literal should be the same too + if ( p->pResLits[v1] == pReason->pLits[v2] ) + continue; + // the literal is different + printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); + } + } + +// Vec_PtrPush( pFinal->pAntis, pReason ); + } + + // unmark all seen variables +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// p->pSeens[lit_var(p->pTrail[i])] = 0; + // check that the literals are unmarked +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 ); + + // use the resulting clause to check the correctness of resolution + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Intb_ManPrintResolvent( p->pResLits, p->nResLits ); + for ( v1 = 0; v1 < p->nResLits; v1++ ) + { + for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ ) + if ( pFinal->pLits[v2] == p->pResLits[v1] ) + break; + if ( v2 < (int)pFinal->nLits ) + continue; + break; + } + if ( v1 < p->nResLits ) + { + printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id ); + Intb_ManPrintClause( p, pConflict ); + Intb_ManPrintResolvent( p->pResLits, p->nResLits ); + Intb_ManPrintClause( p, pFinal ); + } + } +p->timeTrace += clock() - clk; + + // return the proof pointer + if ( p->pCnf->nClausesA ) + { +// Intb_ManPrintInterOne( p, pFinal ); + } + Intb_ManProofSet( p, pFinal, p->Counter ); + return p->Counter; +} + +/**Function************************************************************* + + Synopsis [Records the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManProofRecordOne( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + Sto_Cls_t * pConflict; + int i; + + // empty clause never ends up there + assert( pClause->nLits > 0 ); + if ( pClause->nLits == 0 ) + printf( "Error: Empty clause is attempted.\n" ); + + // add assumptions to the trail + assert( !pClause->fRoot ); + assert( p->nTrailSize == p->nRootSize ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + if ( !Intb_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumptions + pConflict = Intb_ManPropagate( p, p->nRootSize ); + if ( pConflict == NULL ) + { + assert( 0 ); // cannot prove + return 0; + } + + // construct the proof + Intb_ManProofTraceOne( p, pConflict, pClause ); + + // undo to the root level + Intb_ManCancelUntil( p, p->nRootSize ); + + // add large clauses to the watched lists + if ( pClause->nLits > 1 ) + { + Intb_ManWatchClause( p, pClause, pClause->pLits[0] ); + Intb_ManWatchClause( p, pClause, pClause->pLits[1] ); + return 1; + } + assert( pClause->nLits == 1 ); + + // if the clause proved is unit, add it and propagate + if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumption + pConflict = Intb_ManPropagate( p, p->nRootSize ); + if ( pConflict ) + { + // construct the proof + Intb_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty ); +// if ( p->fVerbose ) +// printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); + return 0; + } + + // update the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Propagate the root clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManProcessRoots( Intb_Man_t * p ) +{ + Sto_Cls_t * pClause; + int Counter; + + // make sure the root clauses are preceeding the learnt clauses + Counter = 0; + Sto_ManForEachClause( p->pCnf, pClause ) + { + assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) ); + assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) ); + Counter++; + } + assert( p->pCnf->nClauses == Counter ); + + // make sure the last clause if empty + assert( p->pCnf->pTail->nLits == 0 ); + + // go through the root unit clauses + p->nTrailSize = 0; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + // create watcher lists for the root clauses + if ( pClause->nLits > 1 ) + { + Intb_ManWatchClause( p, pClause, pClause->pLits[0] ); + Intb_ManWatchClause( p, pClause, pClause->pLits[1] ); + } + // empty clause and large clauses + if ( pClause->nLits != 1 ) + continue; + // unit clause + assert( lit_check(pClause->pLits[0], p->pCnf->nVars) ); + if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + // detected root level conflict + printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" ); + assert( 0 ); + return 0; + } + } + + // propagate the root unit clauses + pClause = Intb_ManPropagate( p, 0 ); + if ( pClause ) + { + // detected root level conflict + Intb_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); + return 0; + } + + // set the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrepareInter( Intb_Man_t * p ) +{ + Sto_Cls_t * pClause; + int Var, VarAB, v; + + // set interpolants for root clauses + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( !pClause->fA ) // clause of B + { + Intb_ManAigFill( p, Intb_ManAigRead(p, pClause) ); +// Intb_ManPrintInterOne( p, pClause ); + continue; + } + // clause of A + Intb_ManAigClear( p, Intb_ManAigRead(p, pClause) ); + + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] < 0 ) // global var + { + VarAB = -p->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) ); + if ( lit_sign(pClause->pLits[v]) ) // negative var + Intb_ManAigOrNotVar( p, Intb_ManAigRead(p, pClause), VarAB ); + else + Intb_ManAigOrVar( p, Intb_ManAigRead(p, pClause), VarAB ); + } + } + +// Intb_ManPrintInterOne( p, pClause ); + } +} + +/**Function************************************************************* + + Synopsis [Computes interpolant for the given CNF.] + + Description [Takes the interpolation manager, the CNF deriving by the SAT + solver, which includes ClausesA, ClausesB, and learned clauses. Additional + arguments are the vector of variables common to AB and the verbosiness flag. + Returns the AIG manager with a single output, containing the interpolant.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose ) +{ + Aig_Man_t * pRes; + Aig_Obj_t * pObj; + Sto_Cls_t * pClause; + int RetValue = 1; + int clkTotal = clock(); + + // check that the CNF makes sense + assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); + p->pCnf = pCnf; + p->fVerbose = fVerbose; + p->vVarsAB = vVarsAB; + p->pAig = pRes = Aig_ManStart( 10000 ); + Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 ); + + // adjust the manager + Intb_ManResize( p ); + + // prepare the interpolant computation + Intb_ManPrepareInter( p ); + + // construct proof for each clause + // start the proof + if ( p->fProofWrite ) + { + p->pFile = fopen( "proof.cnf_", "w" ); + p->Counter = 0; + } + + // write the root clauses + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + Intb_ManProofWriteOne( p, pClause ); + + // propagate root level assignments + if ( Intb_ManProcessRoots( p ) ) + { + // if there is no conflict, consider learned clauses + Sto_ManForEachClause( p->pCnf, pClause ) + { + if ( pClause->fRoot ) + continue; + if ( !Intb_ManProofRecordOne( p, pClause ) ) + { + RetValue = 0; + break; + } + } + } + + // stop the proof + if ( p->fProofWrite ) + { + fclose( p->pFile ); + p->pFile = NULL; + } + + if ( fVerbose ) + { +// PRT( "Interpo", clock() - clkTotal ); + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", + p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, + 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), + 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); +p->timeTotal += clock() - clkTotal; + } + + pObj = *Intb_ManAigRead( p, p->pCnf->pTail ); + Aig_ObjCreatePo( pRes, pObj ); + Aig_ManCleanup( pRes ); + + p->pAig = NULL; + return pRes; + +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ) +{ + Aig_Man_t * p; + Aig_Obj_t * pMiter, * pSum, * pLit; + Sto_Cls_t * pClause; + int Var, VarAB, v; + p = Aig_ManStart( 10000 ); + pMiter = Aig_ManConst1(p); + Sto_ManForEachClauseRoot( pCnf, pClause ) + { + if ( fClausesA ^ pClause->fA ) // clause of B + continue; + // clause of A + pSum = Aig_ManConst0(p); + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( pMan->pVarTypes[Var] < 0 ) // global var + { + VarAB = -pMan->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) ); + pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) ); + } + else + pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) ); + pSum = Aig_Or( p, pSum, pLit ); + } + pMiter = Aig_And( p, pMiter, pSum ); + } + Aig_ObjCreatePo( p, pMiter ); + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/bsat/satMem.h b/src/sat/bsat/satMem.h index 22b7a87c..f60d7fdd 100644 --- a/src/sat/bsat/satMem.h +++ b/src/sat/bsat/satMem.h @@ -23,7 +23,6 @@ /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -//#include "leaks.h" #include <stdio.h> #include <stdlib.h> #include <string.h> diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h index 027afcb4..ef98ab93 100644 --- a/src/sat/bsat/satStore.h +++ b/src/sat/bsat/satStore.h @@ -135,6 +135,12 @@ extern Inta_Man_t * Inta_ManAlloc(); extern void Inta_ManFree( Inta_Man_t * p ); extern void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose ); +/*=== satInterB.c ==========================================================*/ +typedef struct Intb_Man_t_ Intb_Man_t; +extern Intb_Man_t * Intb_ManAlloc(); +extern void Intb_ManFree( Intb_Man_t * p ); +extern void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose ); + /*=== satInterP.c ==========================================================*/ typedef struct Intp_Man_t_ Intp_Man_t; extern Intp_Man_t * Intp_ManAlloc(); diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index c13d7083..0e8b1e31 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -23,7 +23,6 @@ /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -//#include "leaks.h" #include <stdio.h> #include <stdlib.h> #include <string.h> diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index 03903abe..2ff0e695 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -25,7 +25,6 @@ /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -//#include "leaks.h" #include <stdio.h> #include <stdlib.h> #include <string.h> |