From 13f52980dae9821b3d7bec9ff6a0fa4e544607d7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 18 Jul 2008 08:01:00 -0700 Subject: Version abc80718 --- Makefile | 1 + abc.dsp | 24 +- abclib.dsp | 2844 ++++++++++++++++++++++++++++++++++++++++++++ abclib.dsw | 29 + abctestlib.dsp | 102 ++ abctestlib.dsw | 29 + readme | 4 + src/aig/ntl/ntl.h | 3 +- src/aig/ntl/ntlMan.c | 47 +- src/aig/ntl/ntlReadBlif.c | 4 +- src/aig/ntl/ntlWriteBlif.c | 2 + src/aig/saig/saig.h | 2 +- src/aig/saig/saigInter.c | 342 +++++- src/base/abci/abc.c | 28 +- src/base/abci/abcDar.c | 4 +- src/base/main/main.c | 8 +- src/map/pcm/module.make | 0 src/map/ply/module.make | 0 src/misc/extra/extra.h | 2 +- src/misc/vec/vec.h | 2 +- src/misc/zlib/1.c | 35 - src/sat/bsat/satInterA.c | 2 +- src/sat/psat/m114p.h | 39 + src/sat/psat/m114p_types.h | 9 + src/sat/psat/module.make | 1 + 25 files changed, 3481 insertions(+), 82 deletions(-) create mode 100644 abclib.dsp create mode 100644 abclib.dsw create mode 100644 abctestlib.dsp create mode 100644 abctestlib.dsw create mode 100644 src/map/pcm/module.make create mode 100644 src/map/ply/module.make delete mode 100644 src/misc/zlib/1.c create mode 100644 src/sat/psat/m114p.h create mode 100644 src/sat/psat/m114p_types.h create mode 100644 src/sat/psat/module.make diff --git a/Makefile b/Makefile index 93749444..99dadb06 100644 --- a/Makefile +++ b/Makefile @@ -19,6 +19,7 @@ MODULES := \ 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 \ src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \ + src/sat/psat \ src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \ src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \ src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \ diff --git a/abc.dsp b/abc.dsp index cfd72ed8..a8f63e61 100644 --- a/abc.dsp +++ b/abc.dsp @@ -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 /D "_CRT_SECURE_NO_DEPRECATE" /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/sat/nsat" /I "src/sat/psat" /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 @@ -50,7 +50,7 @@ BSC32=bscmake.exe # 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 /nologo /subsystem:console /profile /machine:I386 /out:"_TEST/abc.exe" +# 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 m114pr.lib /nologo /subsystem:console /profile /machine:I386 /out:"_TEST/abc.exe" /libpath:"lib" !ELSEIF "$(CFG)" == "abc - Win32 Debug" @@ -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 /D "_CRT_SECURE_NO_DEPRECATE" /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/sat/nsat" /I "src/sat/psat" /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" @@ -75,7 +75,7 @@ BSC32=bscmake.exe # 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 /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe" /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 m114pd.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept /libpath:"lib" !ENDIF @@ -1245,6 +1245,22 @@ SOURCE=.\src\sat\proof\pr.c SOURCE=.\src\sat\proof\pr.h # End Source File # End Group +# Begin Group "psat" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\sat\psat\m114p.h +# End Source File +# Begin Source File + +SOURCE=.\src\sat\psat\m114p_types.h +# End Source File +# End Group +# Begin Group "nsat" + +# PROP Default_Filter "" +# End Group # End Group # Begin Group "opt" diff --git a/abclib.dsp b/abclib.dsp new file mode 100644 index 00000000..df244f0f --- /dev/null +++ b/abclib.dsp @@ -0,0 +1,2844 @@ +# 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 new file mode 100644 index 00000000..260ade17 --- /dev/null +++ b/abclib.dsw @@ -0,0 +1,29 @@ +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 new file mode 100644 index 00000000..e901cbda --- /dev/null +++ b/abctestlib.dsp @@ -0,0 +1,102 @@ +# 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 new file mode 100644 index 00000000..7ae6cac9 --- /dev/null +++ b/abctestlib.dsw @@ -0,0 +1,29 @@ +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/readme b/readme index 13bb8e15..93e6f89d 100644 --- a/readme +++ b/readme @@ -11,6 +11,10 @@ Modify Makefile to have -DLIN (for 32-bits) or -DLIN64 (for 64-bits) If compiling as a static library, it is necessary to uncomment #define _LIB in "src/abc/main/main.c" +To compile with Microsoft Visual Studio higher than 6.0, +remove ABC_CHECK_LEAKS from the preprocessor definitions +for the debug version (Project->Settings->C/C++->Preprocessor Definitions) + Several things to try if it does not compile on your platform: - Try running all code (not only Makefile and depends.sh) through dos2unix - Try the following actions: diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index b0f3b1fb..5f1f724f 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -66,7 +66,7 @@ struct Ntl_Man_t_ char * pName; // the name of this design char * pSpec; // the name of input file Vec_Ptr_t * vModels; // the array of all models used to represent boxes - int BoxTypes[15]; // the array of box types among the models + int BoxTypes[32]; // the array of box types among the models // memory managers Aig_MmFlex_t * pMemObjs; // memory for objects Aig_MmFlex_t * pMemSops; // memory for SOPs @@ -225,6 +225,7 @@ static inline int Ntl_BoxIsWhite( Ntl_Obj_t * p ) { assert( Ntl_ static inline int Ntl_BoxIsBlack( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrWhite; } static inline int Ntl_BoxIsComb( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrComb; } static inline int Ntl_BoxIsSeq( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrComb; } +static inline int Ntl_BoxIsNoMerge( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrNoMerge; } static inline int Ntl_ObjIsMapLeaf( Ntl_Obj_t * p ) { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p)); } static inline int Ntl_ObjIsMapRoot( Ntl_Obj_t * p ) { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p)); } diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c index 06a1a51c..dd481537 100644 --- a/src/aig/ntl/ntlMan.c +++ b/src/aig/ntl/ntlMan.c @@ -222,7 +222,7 @@ void Ntl_ManPrintStats( Ntl_Man_t * p ) printf( "inv/buf = %5d ", Ntl_ModelLut1Num(pRoot) ); printf( "box = %4d ", Ntl_ModelBoxNum(pRoot) ); printf( "mod = %3d ", Vec_PtrSize(p->vModels) ); - printf( "net = %d", Ntl_ModelCountNets(pRoot) ); + printf( "net = %d", Ntl_ModelCountNets(pRoot) ); printf( "\n" ); fflush( stdout ); assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) ); @@ -262,10 +262,11 @@ void Ntl_ManSaveBoxType( Ntl_Obj_t * pObj ) Ntl_Mod_t * pModel = pObj->pImplem; int Number = 0; assert( Ntl_ObjIsBox(pObj) ); - Number |= (pModel->attrWhite << 0); - Number |= (pModel->attrBox << 1); - Number |= (pModel->attrComb << 2); - Number |= (pModel->attrKeep << 3); + Number |= (pModel->attrWhite << 0); + Number |= (pModel->attrBox << 1); + Number |= (pModel->attrComb << 2); + Number |= (pModel->attrKeep << 3); + Number |= (pModel->attrNoMerge << 4); pModel->pMan->BoxTypes[Number]++; } @@ -291,19 +292,20 @@ void Ntl_ManPrintTypes( Ntl_Man_t * p ) printf( "BOX STATISTICS:\n" ); Ntl_ModelForEachBox( pModel, pObj, i ) Ntl_ManSaveBoxType( pObj ); - for ( i = 0; i < 15; i++ ) + for ( i = 0; i < 32; i++ ) { if ( !p->BoxTypes[i] ) continue; printf( "%5d :", p->BoxTypes[i] ); - printf( " %s", ((i & 1) > 0)? "white": "black" ); - printf( " %s", ((i & 2) > 0)? "box ": "logic" ); - printf( " %s", ((i & 4) > 0)? "comb ": "seq " ); - printf( " %s", ((i & 8) > 0)? "keep ": "sweep" ); + printf( " %s", ((i & 1) > 0)? "white ": "black " ); + printf( " %s", ((i & 2) > 0)? "box ": "logic " ); + printf( " %s", ((i & 4) > 0)? "comb ": "seq " ); + printf( " %s", ((i & 8) > 0)? "keep ": "sweep " ); + printf( " %s", ((i & 16) > 0)? "no_merge": "merge " ); printf( "\n" ); } printf( "Total box instances = %6d.\n\n", Ntl_ModelBoxNum(pModel) ); - for ( i = 0; i < 15; i++ ) + for ( i = 0; i < 32; i++ ) p->BoxTypes[i] = 0; } @@ -366,6 +368,11 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) Ntl_Obj_t * pObj; int i, k; pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName ); + pModelNew->attrWhite = pModelOld->attrWhite; + pModelNew->attrBox = pModelOld->attrBox; + pModelNew->attrComb = pModelOld->attrComb; + pModelNew->attrKeep = pModelOld->attrKeep; + pModelNew->attrNoMerge = pModelOld->attrNoMerge; Ntl_ModelForEachObj( pModelOld, pObj, i ) { if ( Ntl_ObjIsNode(pObj) ) @@ -423,10 +430,11 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) Ntl_Obj_t * pObj; int i, k; pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName ); - pModelNew->attrWhite = pModelOld->attrWhite; - pModelNew->attrBox = pModelOld->attrBox; - pModelNew->attrComb = pModelOld->attrComb; - pModelNew->attrKeep = pModelOld->attrKeep; + pModelNew->attrWhite = pModelOld->attrWhite; + pModelNew->attrBox = pModelOld->attrBox; + pModelNew->attrComb = pModelOld->attrComb; + pModelNew->attrKeep = pModelOld->attrKeep; + pModelNew->attrNoMerge = pModelOld->attrNoMerge; Ntl_ModelForEachObj( pModelOld, pObj, i ) pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj ); Ntl_ModelForEachNet( pModelOld, pNet, i ) @@ -504,10 +512,11 @@ Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init ) // create model sprintf( Name, "%s%d", "latch", Init ); pModel = Ntl_ModelAlloc( pMan, Name ); - pModel->attrWhite = 1; - pModel->attrBox = 1; - pModel->attrComb = 0; - pModel->attrKeep = 0; + pModel->attrWhite = 1; + pModel->attrBox = 1; + pModel->attrComb = 0; + pModel->attrKeep = 0; + pModel->attrNoMerge = 0; // create primary input pObj = Ntl_ModelCreatePi( pModel ); pNetLi = Ntl_ModelFindOrCreateNet( pModel, "li" ); diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index 6eb2cc95..30f972c8 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -878,14 +878,14 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine ) 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 ) p->pNtk->attrComb = 1; else if ( strcmp( pToken, "seq" ) == 0 ) p->pNtk->attrComb = 0; else if ( strcmp( pToken, "keep" ) == 0 ) p->pNtk->attrKeep = 1; + else if ( strcmp( pToken, "sweep" ) == 0 ) + p->pNtk->attrKeep = 0; else { sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), pToken, p->pNtk->pName ); diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c index 623fa3a6..9c8d55ae 100644 --- a/src/aig/ntl/ntlWriteBlif.c +++ b/src/aig/ntl/ntlWriteBlif.c @@ -66,6 +66,8 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel, int fMain ) // fprintf( pFile, " %s", pModel->attrKeep? "keep" : "sweep" ); fprintf( pFile, "\n" ); } + if ( pModel->attrNoMerge ) + fprintf( pFile, ".no_merge\n" ); fprintf( pFile, ".inputs" ); Ntl_ModelForEachPi( pModel, pObj, i ) fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName ); diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 08275ff3..4ae07063 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 fUsePudlak, int fVerbose, int * pDepth ); +extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, 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 527f372d..37eb3349 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -65,6 +65,8 @@ struct Saig_IntMan_t_ int timeTotal; }; +static int Saig_M144pPerformOneStep( Saig_IntMan_t * p ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -331,6 +333,7 @@ sat_solver * Saig_DeriveSatSolver( sat_solver_store_mark_roots( pSat ); // return clauses to the original state Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); return pSat; } @@ -727,6 +730,103 @@ void Saig_ManagerFree( Saig_IntMan_t * p ) free( p ); } + +/**Function************************************************************* + + Synopsis [Check inductive containment.] + + Description [Given interpolant I and transition relation T, here we + check that I(x) * T(x,y) => T(y). ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p ) +{ + sat_solver * pSat; + Aig_Man_t * pInterOld = p->pInter; + Aig_Man_t * pInterNew = p->pInterNew; + Aig_Man_t * pTrans = p->pAigTrans; + Cnf_Dat_t * pCnfOld = p->pCnfInter; + Cnf_Dat_t * pCnfNew = Cnf_Derive( p->pInterNew, 0 ); + Cnf_Dat_t * pCnfTrans = p->pCnfAig; + Aig_Obj_t * pObj, * pObj2; + int status, i, Lits[2]; + + // start the solver + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars ); + + // interpolant + for ( i = 0; i < pCnfNew->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) ) + assert( 0 ); + } + + // connector clauses + Cnf_DataLift( pCnfTrans, pCnfNew->nVars ); + Aig_ManForEachPi( pInterNew, pObj, i ) + { + pObj2 = Saig_ManLo( pTrans, i ); + Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + // one timeframe + for ( i = 0; i < pCnfTrans->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfTrans->pClauses[i], pCnfTrans->pClauses[i+1] ) ) + assert( 0 ); + } + + // connector clauses + Cnf_DataLift( pCnfNew, pCnfNew->nVars + pCnfTrans->nVars ); + Aig_ManForEachPi( pInterNew, pObj, i ) + { + pObj2 = Saig_ManLi( pTrans, i ); + Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + + // complement the last literal + Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1]; + pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]); + // add clauses of B + for ( i = 0; i < pCnfNew->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) ) + assert( 0 ); + } + // complement the last literal + Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1]; + pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]); + + // return clauses to the original state + Cnf_DataLift( pCnfTrans, -pCnfNew->nVars ); + Cnf_DataLift( pCnfNew, -pCnfNew->nVars -pCnfTrans->nVars ); + Cnf_DataFree( pCnfNew ); + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); + sat_solver_delete( pSat ); + return status == l_False; +} + + /**Function************************************************************* Synopsis [Interplates while the number of conflicts is not exceeded.] @@ -738,7 +838,7 @@ void Saig_ManagerFree( Saig_IntMan_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUseIp, int fVerbose, int * pDepth ) +int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fVerbose, int * pDepth ) { Saig_IntMan_t * p; Aig_Man_t * pAigTemp; @@ -809,17 +909,20 @@ p->timeCnf += clock() - clk; // iterate the interpolation procedure for ( i = 0; ; i++ ) { - if ( p->nFrames + i >= 75 ) + if ( p->nFrames + i >= nFramesMax ) { if ( fVerbose ) - printf( "Reached limit (%d) on the number of timeframes.\n", 75 ); + printf( "Reached limit (%d) on the number of timeframes.\n", nFramesMax ); p->timeTotal = clock() - clkTotal; Saig_ManagerFree( p ); return -1; } // perform interplation clk = clock(); - RetValue = Saig_PerformOneStep( p, fUseIp ); + if ( fUseIp ) + RetValue = Saig_M144pPerformOneStep( p ); + else + RetValue = Saig_PerformOneStep( p, 0 ); if ( fVerbose ) { printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ", @@ -859,7 +962,10 @@ clk = clock(); p->timeRwr += clock() - clk; // check containment of interpolants clk = clock(); - Status = Saig_ManCheckContainment( p->pInterNew, p->pInter ); + if ( fCheckInd ) + Status = Saig_ManCheckInductiveContainment( p ); + else + Status = Saig_ManCheckContainment( p->pInterNew, p->pInter ); p->timeEqu += clock() - clk; if ( Status ) // contained { @@ -897,6 +1003,232 @@ p->timeCnf += clock() - clk; return RetValue; } + +#include "m114p.h" + +/**Function************************************************************* + + Synopsis [Returns the SAT solver for one interpolation run.] + + Description [pInter is the previous interpolant. pAig is one time frame. + pFrames is the unrolled time frames.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +M114p_Solver_t Saig_M144pDeriveSatSolver( + Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, + Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, + Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, + Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars ) +{ + M114p_Solver_t pSat; + Aig_Obj_t * pObj, * pObj2; + int i, Lits[2]; + + // sanity checks + assert( Aig_ManRegNum(pInter) == 0 ); + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pFrames) == 0 ); + assert( Aig_ManPoNum(pInter) == 1 ); + assert( Aig_ManPoNum(pFrames) == 1 ); + assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) ); +// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); + + // prepare CNFs + Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars ); + + *pvMapRoots = Vec_IntAlloc( 10000 ); + *pvMapVars = Vec_IntAlloc( 0 ); + Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 ); + for ( i = 0; i < pCnfFrames->nVars; i++ ) + Vec_IntWriteEntry( *pvMapVars, i, -2 ); + + // start the solver + pSat = M114p_SolverNew( 1 ); + M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars ); + + // add clauses of A + // interpolant + for ( i = 0; i < pCnfInter->nClauses; i++ ) + { + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) ) + assert( 0 ); + } + // connector clauses + Aig_ManForEachPi( pInter, pObj, i ) + { + pObj2 = Saig_ManLo( pAig, i ); + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + // one timeframe + for ( i = 0; i < pCnfAig->nClauses; i++ ) + { + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) ) + assert( 0 ); + } + // connector clauses + Aig_ManForEachPi( pFrames, pObj, i ) + { + if ( i == Aig_ManRegNum(pAig) ) + break; +// Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); + Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i ); + + pObj2 = Saig_ManLi( pAig, i ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + // add clauses of B + for ( i = 0; i < pCnfFrames->nClauses; i++ ) + { + Vec_IntPush( *pvMapRoots, 1 ); + if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) + assert( 0 ); + } + // return clauses to the original state + Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [Computes interpolant using MiniSat-1.14p.] + + Description [Assumes that the solver returned UNSAT and proof + logging was enabled. Array vMapRoots maps number of each root clause + into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT + solver variable into -1 (var of A), -2 (var of B), and (var of C), + where is the var's 0-based number in the ordering of C variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) +{ + Aig_Man_t * p; + Aig_Obj_t * pInter, * pInter2, * pVar; + Vec_Ptr_t * vInters; + int * pLits, * pClauses, * pVars; + int nLits, nVars, i, k, iVar; + assert( M114p_SolverProofIsReady(s) ); + vInters = Vec_PtrAlloc( 1000 ); + // process root clauses + p = Aig_ManStart( 10000 ); + M114p_SolverForEachRoot( s, &pLits, nLits, i ) + { + if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B + pInter = Aig_ManConst1(p); + else // clause of A + { + pInter = Aig_ManConst0(p); + for ( k = 0; k < nLits; k++ ) + { + iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) ); + if ( iVar < 0 ) // var of A or B + continue; + pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) ); + pInter = Aig_Or( p, pInter, pVar ); + } + } + Vec_PtrPush( vInters, pInter ); + } + assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); + + // process learned clauses + M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) + { + pInter = Vec_PtrEntry( vInters, pClauses[0] ); + for ( k = 0; k < nVars; k++ ) + { + iVar = Vec_IntEntry( vMapVars, pVars[k] ); + pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); + if ( iVar == -1 ) // var of A + pInter = Aig_Or( p, pInter, pInter2 ); + else // var of B or C + pInter = Aig_And( p, pInter, pInter2 ); + } + Vec_PtrPush( vInters, pInter ); + } + assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); + Vec_PtrFree( vInters ); + Aig_ObjCreatePo( p, pInter ); + Aig_ManCleanup( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Performs one SAT run with interpolation.] + + Description [Returns 1 if proven. 0 if failed. -1 if undecided.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_M144pPerformOneStep( Saig_IntMan_t * p ) +{ + M114p_Solver_t pSat; + Vec_Int_t * vMapRoots, * vMapVars; + int clk, status, RetValue; + assert( p->pInterNew == NULL ); + // derive the SAT solver + pSat = Saig_M144pDeriveSatSolver( p->pInter, p->pCnfInter, + p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, + &vMapRoots, &vMapVars ); + // solve the problem +clk = clock(); + status = M114p_SolverSolve( pSat, NULL, NULL, 0 ); + p->nConfCur = M114p_SolverGetConflictNum( pSat ); +p->timeSat += clock() - clk; + if ( status == 0 ) + { + RetValue = 1; +clk = clock(); + p->pInterNew = Saig_M144pInterpolate( pSat, vMapRoots, vMapVars ); +p->timeInt += clock() - clk; + } + else if ( status == 1 ) + { + RetValue = 0; + } + else + { + RetValue = -1; + } + M114p_SolverDelete( pSat ); + Vec_IntFree( vMapRoots ); + Vec_IntFree( vMapVars ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d1aa2c82..cb3d2d86 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -15343,12 +15343,14 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; int nBTLimit; + int nFramesMax; int fRewrite; int fTransLoop; int fUsePudlak; + int fCheckInd; int fVerbose; - extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose ); + extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -15356,12 +15358,14 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nBTLimit = 20000; + nFramesMax = 40; fRewrite = 0; fTransLoop = 1; fUsePudlak = 0; + fCheckInd = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Crtpvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpivh" ) ) != EOF ) { switch ( c ) { @@ -15376,6 +15380,17 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nBTLimit < 0 ) goto usage; break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFramesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFramesMax < 0 ) + goto usage; + break; case 'r': fRewrite ^= 1; break; @@ -15385,6 +15400,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': fUsePudlak ^= 1; break; + case 'i': + fCheckInd ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -15414,16 +15432,18 @@ 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, fUsePudlak, fVerbose ); + Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose ); return 0; usage: - fprintf( pErr, "usage: int [-C num] [-rtpvh]\n" ); + fprintf( pErr, "usage: int [-CF num] [-rtpivh]\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-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax ); 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-i : toggle inductive containment checking [default = %s]\n", fCheckInd? "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 a691a205..e47582e9 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 fUsePudlak, int fVerbose ) +int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, 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, fUsePudlak, fVerbose, &Depth ); + RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose, &Depth ); if ( RetValue == 1 ) printf( "Property proved. " ); else if ( RetValue == 0 ) diff --git a/src/base/main/main.c b/src/base/main/main.c index 6f2e1d11..bfa91ddc 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -55,11 +55,9 @@ int main( int argc, char * argv[] ) bool fBatch, fInitSource, fInitRead, fFinalWrite; // added to detect memory leaks: -#ifdef _DEBUG -#ifdef ABC_CHECK_LEAKS +#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0 _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF ); #endif -#endif // Npn_Experiment(); // Npn_Generate(); @@ -256,10 +254,8 @@ void Abc_Start() { Abc_Frame_t * pAbc; // added to detect memory leaks: -#ifdef _DEBUG -#ifdef ABC_CHECK_LEAKS +#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0 _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF ); -#endif #endif // start the glocal frame pAbc = Abc_FrameGetGlobalFrame(); diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make new file mode 100644 index 00000000..e69de29b diff --git a/src/map/ply/module.make b/src/map/ply/module.make new file mode 100644 index 00000000..e69de29b diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index f45afcbe..d63ed5d3 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -43,7 +43,7 @@ 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 +#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0 #include "leaks.h" #endif diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h index 03de79f1..4c19b5ee 100644 --- a/src/misc/vec/vec.h +++ b/src/misc/vec/vec.h @@ -50,7 +50,7 @@ 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 +#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0 #include "leaks.h" #endif diff --git a/src/misc/zlib/1.c b/src/misc/zlib/1.c deleted file mode 100644 index 8a06a346..00000000 --- a/src/misc/zlib/1.c +++ /dev/null @@ -1,35 +0,0 @@ - Volume in drive C is IBM_PRELOAD - Volume Serial Number is 20EA-F780 - - Directory of C:\_projects\abc\src\misc\zlib - -07/02/2008 03:51 PM . -07/02/2008 03:51 PM .. -07/02/2008 03:51 PM 0 1.c -12/21/2004 04:52 PM 4,708 adler32.c -06/02/2003 06:16 AM 9,545 algorithm.txt -07/07/2003 07:37 AM 2,568 compress_.c -06/13/2005 01:56 AM 13,616 crc32.c -01/05/2003 04:53 PM 31,009 crc32.h -07/18/2005 04:27 AM 65,899 deflate.c -05/29/2005 05:55 PM 12,445 deflate.h -07/11/2005 10:31 PM 32,129 gzio.c -05/31/2005 12:58 AM 22,787 infback.c -11/13/2004 06:05 AM 12,886 inffast.c -01/01/2003 05:46 PM 418 inffast.h -11/24/2002 11:44 PM 6,437 inffixed.h -06/14/2005 11:50 PM 50,345 inflate.c -11/13/2004 05:38 AM 6,031 inflate.h -07/18/2005 04:27 AM 14,085 inftrees.c -07/11/2005 08:50 AM 2,428 inftrees.h -07/02/2008 02:52 PM 34 link.txt -07/18/2005 04:25 AM 5,821 README -06/13/2005 02:34 AM 45,246 trees.c -02/24/1998 12:14 PM 8,572 trees.h -07/07/2003 07:36 AM 2,148 uncompr.c -05/28/2005 08:40 AM 9,876 zconf.h -07/18/2005 04:26 AM 67,545 zlib.h -06/13/2005 02:37 AM 7,454 zutil.c -07/11/2005 10:35 PM 7,128 zutil.h - 26 File(s) 441,160 bytes - 2 Dir(s) 1,641,279,488 bytes free diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index cc780580..5837e68f 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -941,7 +941,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in // stop the proof if ( p->fProofWrite ) - { + { fclose( p->pFile ); p->pFile = NULL; } diff --git a/src/sat/psat/m114p.h b/src/sat/psat/m114p.h new file mode 100644 index 00000000..5050cb4b --- /dev/null +++ b/src/sat/psat/m114p.h @@ -0,0 +1,39 @@ +// C-language header for MiniSat 1.14p + +#ifndef m114p_h +#define m114p_h + +#include "m114p_types.h" + +// SAT solver APIs +extern M114p_Solver_t M114p_SolverNew( int fRecordProof ); +extern void M114p_SolverDelete( M114p_Solver_t s ); +extern void M114p_SolverPrintStats( M114p_Solver_t s, double Time ); +extern void M114p_SolverSetVarNum( M114p_Solver_t s, int nVars ); +extern int M114p_SolverAddClause( M114p_Solver_t s, lit* begin, lit* end ); +extern int M114p_SolverSimplify( M114p_Solver_t s ); +extern int M114p_SolverSolve( M114p_Solver_t s, lit* begin, lit* end, int nConfLimit ); +extern int M114p_SolverGetConflictNum( M114p_Solver_t s ); + +// proof status APIs +extern int M114p_SolverProofIsReady( M114p_Solver_t s ); +extern void M114p_SolverProofSave( M114p_Solver_t s, char * pFileName ); +extern int M114p_SolverProofClauseNum( M114p_Solver_t s ); + +// proof traversal APIs +extern int M114p_SolverGetFirstRoot( M114p_Solver_t s, int ** ppLits ); +extern int M114p_SolverGetNextRoot( M114p_Solver_t s, int ** ppLits ); +extern int M114p_SolverGetFirstChain( M114p_Solver_t s, int ** ppClauses, int ** ppVars ); +extern int M114p_SolverGetNextChain( M114p_Solver_t s, int ** ppClauses, int ** ppVars ); + +// iterator over the root clauses (should be called first) +#define M114p_SolverForEachRoot( s, ppLits, nLits, i ) \ + for ( i = 0, nLits = M114p_SolverGetFirstRoot(s, ppLits); nLits; \ + i++, nLits = M114p_SolverGetNextRoot(s, ppLits) ) + +// iterator over the learned clauses (should be called after iterating over roots) +#define M114p_SolverForEachChain( s, ppClauses, ppVars, nVars, i ) \ + for ( i = 0, nVars = M114p_SolverGetFirstChain(s, ppClauses, ppVars); nVars; \ + i++, nVars = M114p_SolverGetNextChain(s, ppClauses, ppVars) ) + +#endif \ No newline at end of file diff --git a/src/sat/psat/m114p_types.h b/src/sat/psat/m114p_types.h new file mode 100644 index 00000000..54a20c5c --- /dev/null +++ b/src/sat/psat/m114p_types.h @@ -0,0 +1,9 @@ +// C-language header for MiniSat 1.14p + +#ifndef m114p_types_h +#define m114p_types_h + +typedef int M114p_Solver_t; +typedef int lit; + +#endif \ No newline at end of file diff --git a/src/sat/psat/module.make b/src/sat/psat/module.make new file mode 100644 index 00000000..d6d908e7 --- /dev/null +++ b/src/sat/psat/module.make @@ -0,0 +1 @@ +SRC += -- cgit v1.2.3