mirror of https://github.com/YosysHQ/abc.git
Version abc80718
This commit is contained in:
Alan Mishchenko
parent
d63a0cbbfd
commit
13f52980da
1
Makefile
1
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 \
|
||||
|
|
|
|||
24
abc.dsp
24
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"
|
||||
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -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>
|
||||
{{{
|
||||
}}}
|
||||
|
||||
###############################################################################
|
||||
|
||||
|
|
@ -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
|
||||
|
|
@ -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>
|
||||
{{{
|
||||
}}}
|
||||
|
||||
###############################################################################
|
||||
|
||||
4
readme
4
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:
|
||||
|
|
|
|||
|
|
@ -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)); }
|
||||
|
|
|
|||
|
|
@ -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" );
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 ==========================================================*/
|
||||
|
|
|
|||
|
|
@ -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 <num> (var of C),
|
||||
where <num> 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 ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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 )
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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 <DIR> .
|
||||
07/02/2008 03:51 PM <DIR> ..
|
||||
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
|
||||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -0,0 +1 @@
|
|||
SRC +=
|
||||
Loading…
Reference in New Issue