Skip to content

A
abc
Commit ae4b5135 by Alan Mishchenko
Options

Cumulative changes in the last few weeks.

parent f4066b5b
Showing with 841 additions and 293 deletions
Makefile
...@@ -20,7 +20,7 @@ MODULES := \ ...@@ -20,7 +20,7 @@ MODULES := \
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/mfs \ 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/sim src/opt/ret src/opt/res src/opt/lpk \
src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \ src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \
src/sat/psat \ src/sat/psat src/sat/pdr \
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \ 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/mem src/aig/dar src/aig/fra src/aig/cnf \
src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \ src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
......
abcexe.dsp
...@@ -50,7 +50,7 @@ BSC32=bscmake.exe ...@@ -50,7 +50,7 @@ BSC32=bscmake.exe
# ADD BSC32 /nologo # ADD BSC32 /nologo
LINK32=link.exe 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 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 lib\abcr.lib lib\abcextr.lib /nologo /subsystem:console /incremental:yes /debug /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 lib\abcr.lib /nologo /subsystem:console /incremental:yes /debug /machine:I386 /out:"_TEST/abc.exe"
!ELSEIF "$(CFG)" == "abcexe - Win32 Debug" !ELSEIF "$(CFG)" == "abcexe - Win32 Debug"
...@@ -74,7 +74,7 @@ BSC32=bscmake.exe ...@@ -74,7 +74,7 @@ BSC32=bscmake.exe
# ADD BSC32 /nologo # ADD BSC32 /nologo
LINK32=link.exe 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 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 lib\abcd.lib lib\abcextd.lib /nologo /subsystem:console /debug /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 lib\abcd.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe"
!ENDIF !ENDIF
......
abclib.dsp
...@@ -41,7 +41,7 @@ RSC=rc.exe ...@@ -41,7 +41,7 @@ RSC=rc.exe
# PROP Intermediate_Dir "ReleaseLib" # PROP Intermediate_Dir "ReleaseLib"
# PROP Target_Dir "" # PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "src/ext/ext" /I "src/misc/ext" /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/cov" /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" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/llb" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c # ADD CPP /nologo /MD /W3 /GX /O2 /I "src/sat/pdr" /I "src/ext/ext" /I "src/misc/ext" /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/cov" /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" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/llb" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe BSC32=bscmake.exe
...@@ -64,7 +64,7 @@ LIB32=link.exe -lib ...@@ -64,7 +64,7 @@ LIB32=link.exe -lib
# PROP Intermediate_Dir "DebugLib" # PROP Intermediate_Dir "DebugLib"
# PROP Target_Dir "" # 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 BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src/ext/ext" /I "src/misc/ext" /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/cov" /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" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/llb" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c # ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src/sat/pdr" /I "src/ext/ext" /I "src/misc/ext" /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/cov" /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" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/llb" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
# ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG"
BSC32=bscmake.exe BSC32=bscmake.exe
...@@ -1306,16 +1306,56 @@ SOURCE=.\src\sat\psat\m114p.h ...@@ -1306,16 +1306,56 @@ SOURCE=.\src\sat\psat\m114p.h
SOURCE=.\src\sat\psat\m114p_types.h SOURCE=.\src\sat\psat\m114p_types.h
# End Source File # End Source File
# End Group # End Group
# Begin Group "nsat" # Begin Group "lsat"
# PROP Default_Filter "" # PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\sat\lsat\solver.h
# End Source File
# End Group # End Group
# Begin Group "lsat" # Begin Group "pdr"
# PROP Default_Filter "" # PROP Default_Filter ""
# Begin Source File # Begin Source File
SOURCE=.\src\sat\lsat\solver.h SOURCE=.\src\sat\pdr\pdr.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\pdr\pdrClass.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\pdr\pdrCnf.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\pdr\pdrCore.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\pdr\pdrInt.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\pdr\pdrInv.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\pdr\pdrMan.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\pdr\pdrSat.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\pdr\pdrTsim.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\pdr\pdrUtil.c
# End Source File # End Source File
# End Group # End Group
# End Group # End Group
...@@ -3483,6 +3523,10 @@ SOURCE=.\src\aig\saig\saigSynch.c ...@@ -3483,6 +3523,10 @@ SOURCE=.\src\aig\saig\saigSynch.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\saig\saigTempor.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigTrans.c SOURCE=.\src\aig\saig\saigTrans.c
# End Source File # End Source File
# Begin Source File # Begin Source File
...@@ -3927,6 +3971,10 @@ SOURCE=.\src\aig\gia\giaSim.c ...@@ -3927,6 +3971,10 @@ SOURCE=.\src\aig\gia\giaSim.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\gia\giaSim2.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaSort.c SOURCE=.\src\aig\gia\giaSort.c
# End Source File # End Source File
# Begin Source File # Begin Source File
...@@ -4038,50 +4086,6 @@ SOURCE=.\src\aig\llb\llbReach.c ...@@ -4038,50 +4086,6 @@ SOURCE=.\src\aig\llb\llbReach.c
SOURCE=.\src\aig\llb\llbSched.c SOURCE=.\src\aig\llb\llbSched.c
# End Source File # End Source File
# End Group # End Group
# Begin Group "sky"
# PROP Default_Filter ""
# End Group
# Begin Group "pdr"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\xxx\pdr\pdr.c
# End Source File
# Begin Source File
SOURCE=.\src\xxx\pdr\pdr.h
# End Source File
# Begin Source File
SOURCE=.\src\xxx\pdr\pdrClass.c
# End Source File
# Begin Source File
SOURCE=.\src\xxx\pdr\pdrCore.c
# End Source File
# Begin Source File
SOURCE=.\src\xxx\pdr\pdrInt.h
# End Source File
# Begin Source File
SOURCE=.\src\xxx\pdr\pdrMan.c
# End Source File
# Begin Source File
SOURCE=.\src\xxx\pdr\pdrSat.c
# End Source File
# Begin Source File
SOURCE=.\src\xxx\pdr\pdrTsim.c
# End Source File
# Begin Source File
SOURCE=.\src\xxx\pdr\pdrUtil.c
# End Source File
# End Group
# End Group # End Group
# End Group # End Group
# Begin Group "Header Files" # Begin Group "Header Files"
......
src/aig/cnf/cnf.h
...@@ -62,6 +62,8 @@ struct Cnf_Dat_t_ ...@@ -62,6 +62,8 @@ struct Cnf_Dat_t_
int nClauses; // the number of CNF clauses int nClauses; // the number of CNF clauses
int ** pClauses; // the CNF clauses int ** pClauses; // the CNF clauses
int * pVarNums; // the number of CNF variable for each node ID (-1 if unused) int * pVarNums; // the number of CNF variable for each node ID (-1 if unused)
int * pObj2Clause; // the mapping of objects into clauses
int * pObj2Count; // the mapping of objects into clause number
}; };
// the cut used to represent node in the AIG // the cut used to represent node in the AIG
...@@ -125,6 +127,7 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut ...@@ -125,6 +127,7 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut
/*=== cnfCore.c ========================================================*/ /*=== cnfCore.c ========================================================*/
extern Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig ); extern Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig );
extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs ); extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs );
extern Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig );
extern Cnf_Man_t * Cnf_ManRead(); extern Cnf_Man_t * Cnf_ManRead();
extern void Cnf_ClearMemory(); extern void Cnf_ClearMemory();
/*=== cnfCut.c ========================================================*/ /*=== cnfCut.c ========================================================*/
...@@ -167,6 +170,7 @@ extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ...@@ -167,6 +170,7 @@ extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p
extern Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped ); extern Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ); extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ); extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
extern Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ); extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs );
extern Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p ); extern Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p );
......
src/aig/cnf/cnfCore.c
...@@ -138,6 +138,59 @@ p->timeSave = clock() - clk; ...@@ -138,6 +138,59 @@ p->timeSave = clock() - clk;
//ABC_PRT( "Saving ", p->timeSave ); //ABC_PRT( "Saving ", p->timeSave );
return pCnf; return pCnf;
} }
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig )
{
Cnf_Man_t * p;
Cnf_Dat_t * pCnf;
Vec_Ptr_t * vMapped;
Aig_MmFixed_t * pMemCuts;
int clk;
// allocate the CNF manager
if ( s_pManCnf == NULL )
s_pManCnf = Cnf_ManStart();
// connect the managers
p = s_pManCnf;
p->pManAig = pAig;
// generate cuts for all nodes, assign cost, and find best cuts
clk = clock();
pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 );
p->timeCuts = clock() - clk;
// find the mapping
clk = clock();
Cnf_DeriveMapping( p );
p->timeMap = clock() - clk;
// Aig_ManScanMapping( p, 1 );
// convert it into CNF
clk = clock();
Cnf_ManTransferCuts( p );
vMapped = Cnf_ManScanMapping( p, 1, 1 );
pCnf = Cnf_ManWriteCnfOther( p, vMapped );
Vec_PtrFree( vMapped );
Aig_MmFixedStop( pMemCuts, 0 );
p->timeSave = clock() - clk;
// reset reference counters
Aig_ManResetRefs( pAig );
//ABC_PRT( "Cuts ", p->timeCuts );
//ABC_PRT( "Map ", p->timeMap );
//ABC_PRT( "Saving ", p->timeSave );
return pCnf;
}
/**Function************************************************************* /**Function*************************************************************
......
src/aig/cnf/cnfMan.c
...@@ -180,6 +180,8 @@ void Cnf_DataFree( Cnf_Dat_t * p ) ...@@ -180,6 +180,8 @@ void Cnf_DataFree( Cnf_Dat_t * p )
{ {
if ( p == NULL ) if ( p == NULL )
return; return;
ABC_FREE( p->pObj2Clause );
ABC_FREE( p->pObj2Count );
ABC_FREE( p->pClauses[0] ); ABC_FREE( p->pClauses[0] );
ABC_FREE( p->pClauses ); ABC_FREE( p->pClauses );
ABC_FREE( p->pVarNums ); ABC_FREE( p->pVarNums );
......
src/aig/cnf/cnfWrite.c
...@@ -245,8 +245,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) ...@@ -245,8 +245,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
//printf( "\n" ); //printf( "\n" );
// allocate CNF // allocate CNF
pCnf = ABC_ALLOC( Cnf_Dat_t, 1 ); pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
pCnf->pMan = p->pManAig; pCnf->pMan = p->pManAig;
pCnf->nLiterals = nLiterals; pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses; pCnf->nClauses = nClauses;
...@@ -367,6 +366,174 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) ...@@ -367,6 +366,174 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
// verify that the correct number of literals and clauses was written // verify that the correct number of literals and clauses was written
assert( pLits - pCnf->pClauses[0] == nLiterals ); assert( pLits - pCnf->pClauses[0] == nLiterals );
assert( pClas - pCnf->pClauses == nClauses ); assert( pClas - pCnf->pClauses == nClauses );
//Cnf_DataPrint( pCnf, 1 );
return pCnf;
}
/**Function*************************************************************
Synopsis [Derives CNF for the mapping.]
Description [Derives CNF with obj IDs as SAT vars and mapping of
objects into clauses (pObj2Clause and pObj2Count).]
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
{
Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
Cnf_Cut_t * pCut;
Vec_Int_t * vCover, * vSopTemp;
int OutVar, PoVar, pVars[32], * pLits, ** pClas;
unsigned uTruth;
int i, k, nLiterals, nClauses, Cube;
// count the number of literals and clauses
nLiterals = 1 + 4 * Aig_ManPoNum( p->pManAig );
nClauses = 1 + 2 * Aig_ManPoNum( p->pManAig );
Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
{
assert( Aig_ObjIsNode(pObj) );
pCut = Cnf_ObjBestCut( pObj );
// positive polarity of the cut
if ( pCut->nFanins < 5 )
{
uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
assert( p->pSopSizes[uTruth] >= 0 );
nClauses += p->pSopSizes[uTruth];
}
else
{
nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
nClauses += Vec_IntSize(pCut->vIsop[1]);
}
// negative polarity of the cut
if ( pCut->nFanins < 5 )
{
uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
assert( p->pSopSizes[uTruth] >= 0 );
nClauses += p->pSopSizes[uTruth];
}
else
{
nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
nClauses += Vec_IntSize(pCut->vIsop[0]);
}
}
// allocate CNF
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->pMan = p->pManAig;
pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses;
pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
// create room for variable numbers
pCnf->pObj2Clause = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
pCnf->pObj2Count = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
pCnf->pObj2Clause[i] = pCnf->pObj2Count[i] = -1;
pCnf->nVars = Aig_ManObjNumMax(p->pManAig);
// clear the PI counters
Aig_ManForEachPi( p->pManAig, pObj, i )
pCnf->pObj2Count[pObj->Id] = 0;
// assign the clauses
vSopTemp = Vec_IntAlloc( 1 << 16 );
pLits = pCnf->pClauses[0];
pClas = pCnf->pClauses;
Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
{
// remember the starting clause
pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
pCnf->pObj2Count[pObj->Id] = 0;
// get the best cut
pCut = Cnf_ObjBestCut( pObj );
// save variables of this cut
OutVar = pObj->Id;
for ( k = 0; k < (int)pCut->nFanins; k++ )
{
pVars[k] = pCut->pFanins[k];
assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
}
// positive polarity of the cut
if ( pCut->nFanins < 5 )
{
uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
vCover = vSopTemp;
}
else
vCover = pCut->vIsop[1];
Vec_IntForEachEntry( vCover, Cube, k )
{
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
}
pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
// negative polarity of the cut
if ( pCut->nFanins < 5 )
{
uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
vCover = vSopTemp;
}
else
vCover = pCut->vIsop[0];
Vec_IntForEachEntry( vCover, Cube, k )
{
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
}
pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
}
Vec_IntFree( vSopTemp );
// write the output literals
Aig_ManForEachPo( p->pManAig, pObj, i )
{
// remember the starting clause
pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
pCnf->pObj2Count[pObj->Id] = 2;
// get variables
OutVar = Aig_ObjFanin0(pObj)->Id;
PoVar = pObj->Id;
// first clause
*pClas++ = pLits;
*pLits++ = 2 * PoVar;
*pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
// second clause
*pClas++ = pLits;
*pLits++ = 2 * PoVar + 1;
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
}
// remember the starting clause
pCnf->pObj2Clause[Aig_ManConst1(p->pManAig)->Id] = pClas - pCnf->pClauses;
pCnf->pObj2Count[Aig_ManConst1(p->pManAig)->Id] = 1;
// write the constant literal
OutVar = Aig_ManConst1(p->pManAig)->Id;
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
// verify that the correct number of literals and clauses was written
assert( pLits - pCnf->pClauses[0] == nLiterals );
assert( pClas - pCnf->pClauses == nClauses );
//Cnf_DataPrint( pCnf, 1 );
return pCnf; return pCnf;
} }
......
src/aig/fra/fra.h
...@@ -123,6 +123,7 @@ struct Fra_Sec_t_ ...@@ -123,6 +123,7 @@ struct Fra_Sec_t_
int nBddVarsMax; // the state space limit for BDD reachability int nBddVarsMax; // the state space limit for BDD reachability
int nBddMax; // the max number of BDD nodes int nBddMax; // the max number of BDD nodes
int nBddIterMax; // the limit on the number of BDD iterations int nBddIterMax; // the limit on the number of BDD iterations
int nPdrTimeout; // the timeout for PDR in the end
int fPhaseAbstract; // enables phase abstraction int fPhaseAbstract; // enables phase abstraction
int fRetimeFirst; // enables most-forward retiming at the beginning int fRetimeFirst; // enables most-forward retiming at the beginning
int fRetimeRegs; // enables min-register retiming at the beginning int fRetimeRegs; // enables min-register retiming at the beginning
...@@ -134,6 +135,7 @@ struct Fra_Sec_t_ ...@@ -134,6 +135,7 @@ struct Fra_Sec_t_
int fReorderImage; // enables BDD reordering during image computation int fReorderImage; // enables BDD reordering during image computation
int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove
int fUseNewProver; // the new prover int fUseNewProver; // the new prover
int fUsePdr; // the PDR
int fSilent; // disables all output int fSilent; // disables all output
int fVerbose; // enables verbose reporting of statistics int fVerbose; // enables verbose reporting of statistics
int fVeryVerbose; // enables very verbose reporting int fVeryVerbose; // enables very verbose reporting
......
src/aig/fra/fraSec.c
...@@ -24,6 +24,7 @@ ...@@ -24,6 +24,7 @@
#include "ssw.h" #include "ssw.h"
#include "saig.h" #include "saig.h"
#include "bbr.h" #include "bbr.h"
#include "pdr.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
...@@ -70,6 +71,8 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p ) ...@@ -70,6 +71,8 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
p->fReorderImage = 1; // enables variable reordering during image computation p->fReorderImage = 1; // enables variable reordering during image computation
p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove
p->fUseNewProver = 0; // enables new prover p->fUseNewProver = 0; // enables new prover
p->fUsePdr = 1; // enables PDR
p->nPdrTimeout = 60; // enabled PDR timeout
p->fSilent = 0; // disables all output p->fSilent = 0; // disables all output
p->fVerbose = 0; // enables verbose reporting of statistics p->fVerbose = 0; // enables verbose reporting of statistics
p->fVeryVerbose = 0; // enables very verbose reporting p->fVeryVerbose = 0; // enables very verbose reporting
...@@ -539,7 +542,7 @@ clk = clock(); ...@@ -539,7 +542,7 @@ clk = clock();
} }
else else
{ {
Aig_Man_t * pNewOrpos = Said_ManDupOrpos( pNew ); Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew );
RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth ); RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth );
if ( pNewOrpos->pSeqModel ) if ( pNewOrpos->pSeqModel )
{ {
...@@ -582,6 +585,24 @@ ABC_PRT( "Time", clock() - clk ); ...@@ -582,6 +585,24 @@ ABC_PRT( "Time", clock() - clk );
RetValue = Aig_ManVerifyUsingBdds( pNew, pPars ); RetValue = Aig_ManVerifyUsingBdds( pNew, pPars );
} }
// try PDR
if ( pParSec->fUsePdr && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
{
Abc_Cex_t * pCex = NULL;
Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew );
Pdr_Par_t Pars, * pPars = &Pars;
Pdr_ManSetDefaultParams( pPars );
pPars->nTimeOut = pParSec->nPdrTimeout;
pPars->fVerbose = pParSec->fVerbose;
if ( pParSec->fVerbose )
printf( "Running property directed reachability...\n" );
RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex );
if ( pCex )
pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pCex );
Aig_ManStop( pNewOrpos );
pNew->pSeqModel = pCex;
}
finish: finish:
// report the miter // report the miter
if ( RetValue == 1 ) if ( RetValue == 1 )
......
src/aig/gia/gia.h
...@@ -179,6 +179,7 @@ struct Gia_ParSim_t_ ...@@ -179,6 +179,7 @@ struct Gia_ParSim_t_
// user-controlled parameters // user-controlled parameters
int nWords; // the number of machine words int nWords; // the number of machine words
int nIters; // the number of timeframes int nIters; // the number of timeframes
int RandSeed; // seed to generate random numbers
int TimeLimit; // time limit in seconds int TimeLimit; // time limit in seconds
int fCheckMiter; // check if miter outputs are non-zero int fCheckMiter; // check if miter outputs are non-zero
int fVerbose; // enables verbose output int fVerbose; // enables verbose output
......
src/aig/gia/giaEquiv.c
...@@ -1049,6 +1049,11 @@ Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int n ...@@ -1049,6 +1049,11 @@ Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int n
break; break;
if ( f == nFramesMax ) if ( f == nFramesMax )
break; break;
if ( Gia_ManAndNum(pFrames) > 500000 )
{
Gia_ManStop( pFrames );
return NULL;
}
Gia_ManStop( pFrames ); Gia_ManStop( pFrames );
pFrames = NULL; pFrames = NULL;
} }
......
src/aig/gia/giaSim.c
...@@ -65,6 +65,7 @@ void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p ) ...@@ -65,6 +65,7 @@ void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p )
// user-controlled parameters // user-controlled parameters
p->nWords = 8; // the number of machine words p->nWords = 8; // the number of machine words
p->nIters = 32; // the number of timeframes p->nIters = 32; // the number of timeframes
p->RandSeed = 0; // the seed to generate random numbers
p->TimeLimit = 60; // time limit in seconds p->TimeLimit = 60; // time limit in seconds
p->fCheckMiter = 0; // check if miter outputs are non-zero p->fCheckMiter = 0; // check if miter outputs are non-zero
p->fVerbose = 0; // enables verbose output p->fVerbose = 0; // enables verbose output
...@@ -437,9 +438,8 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int ...@@ -437,9 +438,8 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
int f, i, w, iPioId, Counter; int f, i, w, iPioId, Counter;
p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
p->iFrame = iFrame; p->iFrame = iFrame;
p->iPo = iOut; p->iPo = iOut;
// fill in the binary data // fill in the binary data
Gia_ManRandom( 1 );
Counter = p->nRegs; Counter = p->nRegs;
pData = ABC_ALLOC( unsigned, nWords ); pData = ABC_ALLOC( unsigned, nWords );
for ( f = 0; f <= iFrame; f++, Counter += p->nPis ) for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
...@@ -468,14 +468,36 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int ...@@ -468,14 +468,36 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Gia_ManResetRandom( Gia_ParSim_t * pPars )
{
int i;
Gia_ManRandom( 1 );
for ( i = 0; i < pPars->RandSeed; i++ )
Gia_ManRandom( 0 );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
{ {
extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
Gia_ManSim_t * p; Gia_ManSim_t * p;
int i, clkTotal = clock(); int i, clkTotal = clock();
int iOut, iPat, RetValue = 0; int iOut, iPat, RetValue = 0;
if ( pAig->pReprs && pAig->pNexts )
return Gia_ManSimSimulateEquiv( pAig, pPars );
ABC_FREE( pAig->pCexSeq ); ABC_FREE( pAig->pCexSeq );
p = Gia_ManSimCreate( pAig, pPars ); p = Gia_ManSimCreate( pAig, pPars );
Gia_ManRandom( 1 ); Gia_ManResetRandom( pPars );
Gia_ManSimInfoInit( p ); Gia_ManSimInfoInit( p );
for ( i = 0; i < pPars->nIters; i++ ) for ( i = 0; i < pPars->nIters; i++ )
{ {
...@@ -487,6 +509,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) ...@@ -487,6 +509,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
} }
if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) ) if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
{ {
Gia_ManResetRandom( pPars );
pPars->iOutFail = iOut; pPars->iOutFail = iOut;
pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids ); pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i ); Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i );
......
src/aig/gia/giaUtil.c
...@@ -952,8 +952,12 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) ...@@ -952,8 +952,12 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pAig, pObj, k ) Gia_ManForEachCo( pAig, pObj, k )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
if ( i == p->iFrame )
break;
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
{
pObjRo->fMark0 = pObjRi->fMark0; pObjRo->fMark0 = pObjRi->fMark0;
}
} }
assert( iBit == p->nBits ); assert( iBit == p->nBits );
if ( fDualOut ) if ( fDualOut )
......
src/aig/gia/module.make
...@@ -29,6 +29,7 @@ SRC += src/aig/gia/gia.c \ ...@@ -29,6 +29,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaScl.c \ src/aig/gia/giaScl.c \
src/aig/gia/giaShrink.c \ src/aig/gia/giaShrink.c \
src/aig/gia/giaSim.c \ src/aig/gia/giaSim.c \
src/aig/gia/giaSim2.c \
src/aig/gia/giaSort.c \ src/aig/gia/giaSort.c \
src/aig/gia/giaSpeedup.c \ src/aig/gia/giaSpeedup.c \
src/aig/gia/giaSupMin.c \ src/aig/gia/giaSupMin.c \
......
src/aig/live/liveness.c
...@@ -2230,7 +2230,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A ...@@ -2230,7 +2230,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
#ifdef ALLOW_SAFETY_PROPERTIES #ifdef ALLOW_SAFETY_PROPERTIES
printf("liveness output is conjoined with safety assertions\n"); printf("liveness output is conjoined with safety assertions\n");
pObjSafetyAndLiveToSafety = Aig_Or( pNew, pObjSafetyGate, pNegatedSafetyConjunction ); pObjSafetyAndLiveToSafety = Aig_Or( pNew, pObjSafetyGate, pNegatedSafetyConjunction );
pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii ); pObjSafetyPropertyOutput = (Aig_Obj_t *)Vec_PtrEntry( vPoForLtlProps, iii );
Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyAndLiveToSafety ); Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyAndLiveToSafety );
#else #else
pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii ); pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii );
......
src/aig/live/ltl_parser.c
...@@ -78,6 +78,7 @@ void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk ) ...@@ -78,6 +78,7 @@ void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk )
if( pAbc->vLTLProperties_global != NULL ) if( pAbc->vLTLProperties_global != NULL )
{ {
// printf("Deleting exisitng LTL database from the frame\n"); // printf("Deleting exisitng LTL database from the frame\n");
Vec_PtrFree( pAbc->vLTLProperties_global );
pAbc->vLTLProperties_global = NULL; pAbc->vLTLProperties_global = NULL;
} }
pAbc->vLTLProperties_global = Vec_PtrAlloc(Vec_PtrSize(pNtk->vLtlProperties)); pAbc->vLTLProperties_global = Vec_PtrAlloc(Vec_PtrSize(pNtk->vLtlProperties));
......
src/aig/llb/llbCore.c
...@@ -48,7 +48,7 @@ void Llb_ManSetDefaultParams( Gia_ParLlb_t * p ) ...@@ -48,7 +48,7 @@ void Llb_ManSetDefaultParams( Gia_ParLlb_t * p )
{ {
memset( p, 0, sizeof(Gia_ParLlb_t) ); memset( p, 0, sizeof(Gia_ParLlb_t) );
p->nBddMax = 1000000; p->nBddMax = 1000000;
p->nIterMax = 1000; p->nIterMax = 10000000;
p->nClusterMax = 20; p->nClusterMax = 20;
p->nHintDepth = 0; p->nHintDepth = 0;
p->HintFirst = 0; p->HintFirst = 0;
......
src/aig/llb/llbReach.c
...@@ -575,7 +575,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo ...@@ -575,7 +575,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
if ( bReached == NULL ) if ( bReached == NULL )
return 0; // reachable return 0; // reachable
assert( bCurrent == NULL ); // assert( bCurrent == NULL );
if ( bCurrent ) if ( bCurrent )
Cudd_RecursiveDeref( p->dd, bCurrent ); Cudd_RecursiveDeref( p->dd, bCurrent );
// report the stats // report the stats
......
src/aig/mfx/mfxInt.h
...@@ -60,7 +60,8 @@ struct Mfx_Man_t_ ...@@ -60,7 +60,8 @@ struct Mfx_Man_t_
Vec_Ptr_t * vNodes; // the internal nodes of the window Vec_Ptr_t * vNodes; // the internal nodes of the window
Vec_Ptr_t * vDivs; // the divisors of the node Vec_Ptr_t * vDivs; // the divisors of the node
Vec_Int_t * vDivLits; // the SAT literals of divisor nodes Vec_Int_t * vDivLits; // the SAT literals of divisor nodes
Vec_Int_t * vProjVars; // the projection variables Vec_Int_t * vProjVarsCnf; // the projection variables
Vec_Int_t * vProjVarsSat; // the projection variables
// intermediate simulation data // intermediate simulation data
Vec_Ptr_t * vDivCexes; // the counter-example for dividors Vec_Ptr_t * vDivCexes; // the counter-example for dividors
int nDivWords; // the number of words int nDivWords; // the number of words
......
src/aig/mfx/mfxInter.c
...@@ -96,13 +96,13 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int ...@@ -96,13 +96,13 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int
Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert ); Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert );
// collect the outputs of the divisors // collect the outputs of the divisors
Vec_IntClear( p->vProjVars ); Vec_IntClear( p->vProjVarsCnf );
Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) ) Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
{ {
assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); Vec_IntPush( p->vProjVarsCnf, p->pCnf->pVarNums[pObjPo->Id] );
} }
assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) ); assert( Vec_IntSize(p->vProjVarsCnf) == Vec_PtrSize(p->vDivs) );
// start the solver // start the solver
pSat = sat_solver_new(); pSat = sat_solver_new();
...@@ -161,7 +161,7 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int ...@@ -161,7 +161,7 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int
// get the variable number of this divisor // get the variable number of this divisor
i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
// get the corresponding SAT variable // get the corresponding SAT variable
iVar = Vec_IntEntry( p->vProjVars, i ); iVar = Vec_IntEntry( p->vProjVarsCnf, i );
// add the corresponding EXOR gate // add the corresponding EXOR gate
if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
{ {
...@@ -181,15 +181,17 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int ...@@ -181,15 +181,17 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int
else else
{ {
// add the clauses for the EXOR gates - and remember their outputs // add the clauses for the EXOR gates - and remember their outputs
Vec_IntForEachEntry( p->vProjVars, iVar, i ) Vec_IntClear( p->vProjVarsSat );
Vec_IntForEachEntry( p->vProjVarsCnf, iVar, i )
{ {
if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
{ {
sat_solver_delete( pSat ); sat_solver_delete( pSat );
return NULL; return NULL;
} }
Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i ); Vec_IntPush( p->vProjVarsSat, 2 * p->pCnf->nVars + i );
} }
assert( Vec_IntSize(p->vProjVarsCnf) == Vec_IntSize(p->vProjVarsSat) );
// simplify the solver // simplify the solver
status = sat_solver_simplify(pSat); status = sat_solver_simplify(pSat);
if ( status == 0 ) if ( status == 0 )
...@@ -242,7 +244,7 @@ unsigned * Mfx_InterplateTruth( Mfx_Man_t * p, int * pCands, int nCands, int fIn ...@@ -242,7 +244,7 @@ unsigned * Mfx_InterplateTruth( Mfx_Man_t * p, int * pCands, int nCands, int fIn
// get the variable number of this divisor // get the variable number of this divisor
i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
// get the corresponding SAT variable // get the corresponding SAT variable
pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
} }
// derive the interpolant // derive the interpolant
...@@ -342,7 +344,7 @@ Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands ) ...@@ -342,7 +344,7 @@ Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands )
// get the variable number of this divisor // get the variable number of this divisor
i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
// get the corresponding SAT variable // get the corresponding SAT variable
pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
} }
// derive the interpolant // derive the interpolant
......
src/aig/mfx/mfxMan.c
...@@ -49,7 +49,8 @@ Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars ) ...@@ -49,7 +49,8 @@ Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars )
p = ABC_ALLOC( Mfx_Man_t, 1 ); p = ABC_ALLOC( Mfx_Man_t, 1 );
memset( p, 0, sizeof(Mfx_Man_t) ); memset( p, 0, sizeof(Mfx_Man_t) );
p->pPars = pPars; p->pPars = pPars;
p->vProjVars = Vec_IntAlloc( 100 ); p->vProjVarsCnf = Vec_IntAlloc( 100 );
p->vProjVarsSat = Vec_IntAlloc( 100 );
p->vDivLits = Vec_IntAlloc( 100 ); p->vDivLits = Vec_IntAlloc( 100 );
p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFX_FANIN_MAX); p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFX_FANIN_MAX);
p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFX_FANIN_MAX+1, p->nDivWords ); p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFX_FANIN_MAX+1, p->nDivWords );
...@@ -178,7 +179,8 @@ void Mfx_ManStop( Mfx_Man_t * p ) ...@@ -178,7 +179,8 @@ void Mfx_ManStop( Mfx_Man_t * p )
Vec_IntFree( p->vMem ); Vec_IntFree( p->vMem );
Vec_VecFree( p->vLevels ); Vec_VecFree( p->vLevels );
Vec_PtrFree( p->vFanins ); Vec_PtrFree( p->vFanins );
Vec_IntFree( p->vProjVars ); Vec_IntFree( p->vProjVarsCnf );
Vec_IntFree( p->vProjVarsSat );
Vec_IntFree( p->vDivLits ); Vec_IntFree( p->vDivLits );
Vec_PtrFree( p->vDivCexes ); Vec_PtrFree( p->vDivCexes );
ABC_FREE( p ); ABC_FREE( p );
......
src/aig/mfx/mfxResub.c
...@@ -111,7 +111,7 @@ int Mfx_TryResubOnce( Mfx_Man_t * p, int * pCands, int nCands ) ...@@ -111,7 +111,7 @@ int Mfx_TryResubOnce( Mfx_Man_t * p, int * pCands, int nCands )
} }
p->nSatCexes++; p->nSatCexes++;
// store the counter-example // store the counter-example
Vec_IntForEachEntry( p->vProjVars, iVar, i ) Vec_IntForEachEntry( p->vProjVarsSat, iVar, i )
{ {
pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
...@@ -166,7 +166,7 @@ int Mfx_SolveSatResub( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int fOnlyRe ...@@ -166,7 +166,7 @@ int Mfx_SolveSatResub( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int fOnlyRe
continue; continue;
Vec_PtrPush( p->vFanins, pFanin ); Vec_PtrPush( p->vFanins, pFanin );
iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i; iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i;
pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
} }
RetValue = Mfx_TryResubOnce( p, pCands, nCands ); RetValue = Mfx_TryResubOnce( p, pCands, nCands );
if ( RetValue == -1 ) if ( RetValue == -1 )
...@@ -244,7 +244,7 @@ p->timeInt += clock() - clk; ...@@ -244,7 +244,7 @@ p->timeInt += clock() - clk;
if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) ) if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) )
return 0; return 0;
pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
RetValue = Mfx_TryResubOnce( p, pCands, nCands+1 ); RetValue = Mfx_TryResubOnce( p, pCands, nCands+1 );
if ( RetValue == -1 ) if ( RetValue == -1 )
return 0; return 0;
...@@ -316,7 +316,7 @@ int Mfx_SolveSatResub2( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int iFanin ...@@ -316,7 +316,7 @@ int Mfx_SolveSatResub2( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int iFanin
continue; continue;
Vec_PtrPush( p->vFanins, pFanin ); Vec_PtrPush( p->vFanins, pFanin );
iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i; iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i;
pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
} }
RetValue = Mfx_TryResubOnce( p, pCands, nCands ); RetValue = Mfx_TryResubOnce( p, pCands, nCands );
if ( RetValue == -1 ) if ( RetValue == -1 )
...@@ -390,8 +390,8 @@ p->timeInt += clock() - clk; ...@@ -390,8 +390,8 @@ p->timeInt += clock() - clk;
if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) ) if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) )
return 0; return 0;
pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 );
pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
RetValue = Mfx_TryResubOnce( p, pCands, nCands+2 ); RetValue = Mfx_TryResubOnce( p, pCands, nCands+2 );
if ( RetValue == -1 ) if ( RetValue == -1 )
return 0; return 0;
......
src/aig/mfx/mfxSat.c
...@@ -58,7 +58,7 @@ int Mfx_SolveSat_iter( Mfx_Man_t * p ) ...@@ -58,7 +58,7 @@ int Mfx_SolveSat_iter( Mfx_Man_t * p )
p->nCares++; p->nCares++;
// add SAT assignment to the solver // add SAT assignment to the solver
Mint = 0; Mint = 0;
Vec_IntForEachEntry( p->vProjVars, iVar, b ) Vec_IntForEachEntry( p->vProjVarsSat, iVar, b )
{ {
Lits[b] = toLit( iVar ); Lits[b] = toLit( iVar );
if ( sat_solver_var_value( p->pSat, iVar ) ) if ( sat_solver_var_value( p->pSat, iVar ) )
...@@ -70,7 +70,7 @@ int Mfx_SolveSat_iter( Mfx_Man_t * p ) ...@@ -70,7 +70,7 @@ int Mfx_SolveSat_iter( Mfx_Man_t * p )
assert( !Aig_InfoHasBit(p->uCare, Mint) ); assert( !Aig_InfoHasBit(p->uCare, Mint) );
Aig_InfoSetBit( p->uCare, Mint ); Aig_InfoSetBit( p->uCare, Mint );
// add the blocking clause // add the blocking clause
RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) ); RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVarsSat) );
if ( RetValue == 0 ) if ( RetValue == 0 )
return 0; return 0;
return 1; return 1;
...@@ -92,15 +92,15 @@ int Mfx_SolveSat( Mfx_Man_t * p, Nwk_Obj_t * pNode ) ...@@ -92,15 +92,15 @@ int Mfx_SolveSat( Mfx_Man_t * p, Nwk_Obj_t * pNode )
Aig_Obj_t * pObjPo; Aig_Obj_t * pObjPo;
int RetValue, i; int RetValue, i;
// collect projection variables // collect projection variables
Vec_IntClear( p->vProjVars ); Vec_IntClear( p->vProjVarsSat );
Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Nwk_ObjFaninNum(pNode) ) Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Nwk_ObjFaninNum(pNode) )
{ {
assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); Vec_IntPush( p->vProjVarsSat, p->pCnf->pVarNums[pObjPo->Id] );
} }
// prepare the truth table of care set // prepare the truth table of care set
p->nFanins = Vec_IntSize( p->vProjVars ); p->nFanins = Vec_IntSize( p->vProjVarsSat );
p->nWords = Aig_TruthWordNum( p->nFanins ); p->nWords = Aig_TruthWordNum( p->nFanins );
memset( p->uCare, 0, sizeof(unsigned) * p->nWords ); memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
......
src/aig/saig/module.make
...@@ -24,5 +24,6 @@ SRC += src/aig/saig/saigAbs.c \ ...@@ -24,5 +24,6 @@ SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigStrSim.c \ src/aig/saig/saigStrSim.c \
src/aig/saig/saigSwitch.c \ src/aig/saig/saigSwitch.c \
src/aig/saig/saigSynch.c \ src/aig/saig/saigSynch.c \
src/aig/saig/saigTempor.c \
src/aig/saig/saigTrans.c \ src/aig/saig/saigTrans.c \
src/aig/saig/saigWnd.c src/aig/saig/saigWnd.c
src/aig/saig/saig.h
...@@ -146,7 +146,8 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame ...@@ -146,7 +146,8 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose ); extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose ); extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
/*=== saigDup.c ==========================================================*/ /*=== saigDup.c ==========================================================*/
extern Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
/*=== saigHaig.c ==========================================================*/ /*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose ); extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
......
src/aig/saig/saigBmc2.c
...@@ -820,7 +820,12 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax ...@@ -820,7 +820,12 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
{ {
printf( "No output was asserted in %d frames. ", p->iFramePrev-1 ); printf( "No output was asserted in %d frames. ", p->iFramePrev-1 );
if ( piFrames ) if ( piFrames )
*piFrames = p->iFramePrev-1; {
if ( p->iOutputLast > 0 )
*piFrames = p->iFramePrev - 1;
else
*piFrames = p->iFramePrev;
}
} }
if ( fVerbOverwrite ) if ( fVerbOverwrite )
{ {
...@@ -834,7 +839,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax ...@@ -834,7 +839,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
{ {
if ( p->iFrameLast >= p->nFramesMax ) if ( p->iFrameLast >= p->nFramesMax )
printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
else if ( p->pSat->stats.conflicts > p->nConfMaxAll ) else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
else else
printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
......
src/aig/saig/saigDup.c
...@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START ...@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig ) Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * pAig )
{ {
Aig_Man_t * pAigNew; Aig_Man_t * pAigNew;
Aig_Obj_t * pObj, * pMiter; Aig_Obj_t * pObj, * pMiter;
...@@ -79,6 +79,56 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig ) ...@@ -79,6 +79,56 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Duplicates while ORing the POs of sequential circuit.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pObj, * pObj2, * pMiter;
int i;
if ( pAig->nConstrs > 0 )
{
printf( "The AIG manager should have no constraints.\n" );
return NULL;
}
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
pAigNew->pName = Aig_UtilStrsav( pAig->pName );
pAigNew->nConstrs = pAig->nConstrs;
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
// create variables for PIs
Aig_ManForEachPi( pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi( pAigNew );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create POs
assert( Vec_IntSize(vPairs) % 2 == 0 );
Aig_ManForEachNodeVec( pAig, vPairs, pObj, i )
{
pObj2 = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
pMiter = Aig_Exor( pAigNew, pObj->pData, pObj2->pData );
pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase );
Aig_ObjCreatePo( pAigNew, pMiter );
}
// transfer to register outputs
Saig_ManForEachLi( pAig, pObj, i )
Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
Aig_ManCleanup( pAigNew );
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
return pAigNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.] Synopsis [Duplicates the AIG manager recursively.]
Description [] Description []
......
src/aig/saig/saigPhase.c
...@@ -255,15 +255,22 @@ int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords, int nPref ) ...@@ -255,15 +255,22 @@ int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords, int nPref )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix ) void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix, int nLoop )
{ {
unsigned * pState; unsigned * pState;
int nRegs = p->pAig->nRegs; int nRegs = p->pAig->nRegs;
int Value, i, k, Counter = 0; int Value, i, k, Counter = 0;
if ( Vec_PtrSize(p->vStates) > 80 ) printf( "Ternary traces for each flop:\n" );
return; printf( " : " );
for ( i = 0; i < Vec_PtrSize(p->vStates) - nLoop - 1; i++ )
printf( "%d", i%10 );
printf( " " );
for ( i = 0; i < nLoop; i++ )
printf( "%d", i%10 );
printf( "\n" );
for ( i = 0; i < nRegs; i++ ) for ( i = 0; i < nRegs; i++ )
{ {
/*
Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k ) Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k )
{ {
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
...@@ -274,8 +281,11 @@ void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix ) ...@@ -274,8 +281,11 @@ void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix )
Counter++; Counter++;
else else
continue; continue;
*/
// print trace // print trace
printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id ); // printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id );
printf( "%5d : ", Counter++ );
Vec_PtrForEachEntryStop( unsigned *, p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 ) Vec_PtrForEachEntryStop( unsigned *, p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 )
{ {
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
...@@ -488,7 +498,7 @@ Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits, int f ...@@ -488,7 +498,7 @@ Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits, int f
Saig_ManForEachLo( p, pObj, i ) Saig_ManForEachLo( p, pObj, i )
Saig_ObjSetXsim( pObj, Saig_XsimConvertValue(Vec_IntEntry(vInits, i)) ); Saig_ObjSetXsim( pObj, Saig_XsimConvertValue(Vec_IntEntry(vInits, i)) );
} }
else else
{ {
Saig_ManForEachLo( p, pObj, i ) Saig_ManForEachLo( p, pObj, i )
Saig_ObjSetXsim( pObj, SAIG_XVS0 ); Saig_ObjSetXsim( pObj, SAIG_XVS0 );
...@@ -811,6 +821,42 @@ int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits ) ...@@ -811,6 +821,42 @@ int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
{
Saig_Tsim_t * pTsi;
int nFrames, nPrefix, nNonXRegs;
assert( Saig_ManRegNum(p) );
assert( Saig_ManPiNum(p) );
assert( Saig_ManPoNum(p) );
// perform terminary simulation
pTsi = Saig_ManReachableTernary( p, NULL, 0 );
if ( pTsi == NULL )
return 0;
// derive information
nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix;
nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, pTsi->nWords, nPrefix );
// print statistics
if ( fVerbose )
printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", nPrefix, nFrames, p->nRegs, nNonXRegs );
if ( fVeryVerbose )
Saig_TsiPrintTraces( pTsi, pTsi->nWords, nPrefix, nFrames );
Saig_TsiStop( pTsi );
// potentially, may need to reduce nFrames if nPrefix is less than nFrames
return nPrefix;
}
/**Function*************************************************************
Synopsis [Performs automated phase abstraction.]
Description [Takes the AIG manager and the array of initial states.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose ) Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose )
{ {
Aig_Man_t * pNew = NULL; Aig_Man_t * pNew = NULL;
...@@ -829,10 +875,10 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame ...@@ -829,10 +875,10 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
// print statistics // print statistics
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n", printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs ); pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
if ( pTsi->nNonXRegs < 100 ) if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix ); Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
} }
if ( fPrint ) if ( fPrint )
printf( "Print-out finished. Phase assignment is not performed.\n" ); printf( "Print-out finished. Phase assignment is not performed.\n" );
...@@ -885,10 +931,10 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ) ...@@ -885,10 +931,10 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
// print statistics // print statistics
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n", printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs ); pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
if ( pTsi->nNonXRegs < 100 ) if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix ); Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
} }
nFrames = pTsi->nCycle; nFrames = pTsi->nCycle;
if ( fPrint ) if ( fPrint )
......
src/aig/ssw/ssw.h
...@@ -68,6 +68,7 @@ struct Ssw_Pars_t_ ...@@ -68,6 +68,7 @@ struct Ssw_Pars_t_
int fUseCSat; // new SAT solver using when fScorrGia is selected int fUseCSat; // new SAT solver using when fScorrGia is selected
int fVerbose; // verbose stats int fVerbose; // verbose stats
int fFlopVerbose; // verbose printout of redundant flops int fFlopVerbose; // verbose printout of redundant flops
int fEquivDump; // enables dumping equivalences
// optimized latch correspondence // optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized) int fLatchCorrOpt; // perform register correspondence (optimized)
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only) int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
......
src/aig/ssw/sswConstr.c
...@@ -83,8 +83,8 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames ) ...@@ -83,8 +83,8 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
} }
// remove dangling nodes // remove dangling nodes
Aig_ManCleanup( pFrames ); Aig_ManCleanup( pFrames );
return pFrames; return pFrames;
} }
/**Function************************************************************* /**Function*************************************************************
......
src/aig/ssw/sswCore.c
...@@ -64,6 +64,8 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) ...@@ -64,6 +64,8 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->fDynamic = 0; // dynamic partitioning p->fDynamic = 0; // dynamic partitioning
p->fLocalSim = 0; // local simulation p->fLocalSim = 0; // local simulation
p->fVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats
p->fEquivDump = 0; // enables dumping equivalences
// latch correspondence // latch correspondence
p->fLatchCorrOpt = 0; // performs optimized register correspondence p->fLatchCorrOpt = 0; // performs optimized register correspondence
p->nSatVarMax = 1000; // the max number of SAT variables p->nSatVarMax = 1000; // the max number of SAT variables
......
src/aig/ssw/sswDyn.c
...@@ -409,12 +409,12 @@ p->timeReduce += clock() - clk; ...@@ -409,12 +409,12 @@ p->timeReduce += clock() - clk;
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL ); Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) ) if ( Saig_ObjIsLo(p->pAig, pObj) )
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 ); p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
else if ( Aig_ObjIsNode(pObj) ) else if ( Aig_ObjIsNode(pObj) )
{ {
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew ); Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 ); p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
} }
// check if it is time to recycle the solver // check if it is time to recycle the solver
if ( p->pMSat->pSat == NULL || if ( p->pMSat->pSat == NULL ||
......
src/aig/ssw/sswInt.h
...@@ -277,7 +277,7 @@ extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Ai ...@@ -277,7 +277,7 @@ extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Ai
/*=== sswSweep.c ===================================================*/ /*=== sswSweep.c ===================================================*/
extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ); extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
extern void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f ); extern void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f );
extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ); extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs );
extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p );
/*=== sswUnique.c ===================================================*/ /*=== sswUnique.c ===================================================*/
......
src/aig/ssw/sswSemi.c
...@@ -204,7 +204,7 @@ clk = clock(); ...@@ -204,7 +204,7 @@ clk = clock();
{ {
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew ); Ssw_ObjSetFrame( p, pObj, f, pObjNew );
if ( Ssw_ManSweepNode( p, pObj, f, 1 ) ) if ( Ssw_ManSweepNode( p, pObj, f, 1, NULL ) )
{ {
Ssw_ManFilterBmcSavePattern( pBmc ); Ssw_ManFilterBmcSavePattern( pBmc );
if ( fFirst == 0 ) if ( fFirst == 0 )
......
src/aig/ssw/sswSim.c
...@@ -304,6 +304,23 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj ) ...@@ -304,6 +304,23 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_SmlNodeIsZeroFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f )
{
unsigned * pSims = Ssw_ObjSim(p, pObj->Id);
return pSims[f] == 0;
}
/**Function*************************************************************
Synopsis [Counts the number of one's in the patten the object.] Synopsis [Counts the number of one's in the patten the object.]
Description [] Description []
...@@ -1308,7 +1325,7 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) ...@@ -1308,7 +1325,7 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
// run random simulation // run random simulation
Ssw_SmlSimulateOne( pSml ); Ssw_SmlSimulateOne( pSml );
// check if the given output has failed // check if the given output has failed
RetValue = !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); RetValue = !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, p->iPo), p->iFrame );
Ssw_SmlStop( pSml ); Ssw_SmlStop( pSml );
return RetValue; return RetValue;
} }
...@@ -1347,7 +1364,7 @@ int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) ...@@ -1347,7 +1364,7 @@ int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
// check if the given output has failed // check if the given output has failed
iOut = -1; iOut = -1;
Saig_ManForEachPo( pAig, pObj, k ) Saig_ManForEachPo( pAig, pObj, k )
if ( !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, k) ) ) if ( !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, k), p->iFrame ) )
{ {
iOut = k; iOut = k;
break; break;
...@@ -1541,81 +1558,6 @@ Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew ) ...@@ -1541,81 +1558,6 @@ Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew )
return pCex; return pCex;
} }
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p )
{
Ssw_Sml_t * pSml;
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
unsigned * pSims;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
iBit = 0;
Saig_ManForEachLo( pAig, pObj, i )
// Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
Ssw_SmlObjAssignConst( pSml, pObj, 0, 0 );
// assign simulation info for the primary inputs
iBit = p->nRegs;
for ( i = 0; i <= p->iFrame; i++ )
Saig_ManForEachPi( pAig, pObj, k )
Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Ssw_SmlSimulateOne( pSml );
// check if the given output has failed
RetValue = !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
// write the output file
for ( i = 0; i <= p->iFrame; i++ )
{
/*
Saig_ManForEachLo( pAig, pObj, k )
{
pSims = Ssw_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
fprintf( pFile, " " );
*/
Saig_ManForEachPi( pAig, pObj, k )
{
pSims = Ssw_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
/*
fprintf( pFile, " " );
Saig_ManForEachPo( pAig, pObj, k )
{
pSims = Ssw_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
fprintf( pFile, " " );
Saig_ManForEachLi( pAig, pObj, k )
{
pSims = Ssw_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
*/
fprintf( pFile, "\n" );
}
Ssw_SmlStop( pSml );
return RetValue;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
src/aig/ssw/sswSweep.c
...@@ -184,7 +184,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p ) ...@@ -184,7 +184,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs )
{ {
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue, clk; int RetValue, clk;
...@@ -221,6 +221,11 @@ p->timeMarkCones += clock() - clk; ...@@ -221,6 +221,11 @@ p->timeMarkCones += clock() - clk;
Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 ); Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
return 0; return 0;
} }
if ( vPairs )
{
Vec_IntPush( vPairs, pObjRepr->Id );
Vec_IntPush( vPairs, pObj->Id );
}
if ( RetValue == -1 ) // timed out if ( RetValue == -1 ) // timed out
{ {
Ssw_ClassesRemoveNode( p->ppClasses, pObj ); Ssw_ClassesRemoveNode( p->ppClasses, pObj );
...@@ -287,7 +292,7 @@ clk = clock(); ...@@ -287,7 +292,7 @@ clk = clock();
Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL ); Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew ); Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1 ); p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL );
} }
// quit if this is the last timeframe // quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 ) if ( f == p->pPars->nFramesK - 1 )
...@@ -312,6 +317,39 @@ p->timeBmc += clock() - clk; ...@@ -312,6 +317,39 @@ p->timeBmc += clock() - clk;
return p->fRefined; return p->fRefined;
} }
/**Function*************************************************************
Synopsis [Generates AIG with the following nodes put into seq miters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
{
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
FILE * pFile;
char pBuffer[16];
Aig_Man_t * pNew;
sprintf( pBuffer, "equiv%03d.aig", Num );
pFile = fopen( pBuffer, "w" );
if ( pFile == NULL )
{
printf( "Cannot open file %s for writing.\n", pBuffer );
return;
}
fclose( pFile );
pNew = Saig_ManCreateEquivMiter( p, vPairs );
Ioa_WriteAiger( pNew, pBuffer, 0, 0 );
Aig_ManStop( pNew );
printf( "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs fraiging for the internal nodes.] Synopsis [Performs fraiging for the internal nodes.]
...@@ -325,9 +363,11 @@ p->timeBmc += clock() - clk; ...@@ -325,9 +363,11 @@ p->timeBmc += clock() - clk;
***********************************************************************/ ***********************************************************************/
int Ssw_ManSweep( Ssw_Man_t * p ) int Ssw_ManSweep( Ssw_Man_t * p )
{ {
static int Counter;
Bar_Progress_t * pProgress = NULL; Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew; Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, clk, i, f; int nConstrPairs, clk, i, f;
Vec_Int_t * vDisproved;
// perform speculative reduction // perform speculative reduction
clk = clock(); clk = clock();
...@@ -362,17 +402,18 @@ p->timeReduce += clock() - clk; ...@@ -362,17 +402,18 @@ p->timeReduce += clock() - clk;
Ssw_ClassesClearRefined( p->ppClasses ); Ssw_ClassesClearRefined( p->ppClasses );
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
vDisproved = p->pPars->fEquivDump? Vec_IntAlloc(1000) : NULL;
Aig_ManForEachObj( p->pAig, pObj, i ) Aig_ManForEachObj( p->pAig, pObj, i )
{ {
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL ); Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) ) if ( Saig_ObjIsLo(p->pAig, pObj) )
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 ); p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
else if ( Aig_ObjIsNode(pObj) ) else if ( Aig_ObjIsNode(pObj) )
{ {
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew ); Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 ); p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
} }
} }
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
...@@ -380,6 +421,9 @@ p->timeReduce += clock() - clk; ...@@ -380,6 +421,9 @@ p->timeReduce += clock() - clk;
// cleanup // cleanup
// Ssw_ClassesCheck( p->ppClasses ); // Ssw_ClassesCheck( p->ppClasses );
if ( p->pPars->fEquivDump )
Ssw_ManDumpEquivMiter( p->pAig, vDisproved, Counter++ );
Vec_IntFreeP( &vDisproved );
return p->fRefined; return p->fRefined;
} }
......
src/base/abci/abcBalance.c
...@@ -68,7 +68,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, int fDuplicate, int fSelective, in ...@@ -68,7 +68,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, int fDuplicate, int fSelective, in
// perform balancing // perform balancing
Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective, fUpdateLevel ); Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective, fUpdateLevel );
Abc_NtkFinalize( pNtk, pNtkAig ); Abc_NtkFinalize( pNtk, pNtkAig );
Abc_AigCleanup( pNtkAig->pManFunc ); Abc_AigCleanup( (Abc_Aig_t *)pNtkAig->pManFunc );
// undo the required times // undo the required times
if ( fSelective ) if ( fSelective )
{ {
......
src/base/abci/abcCut.c
...@@ -173,7 +173,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) ...@@ -173,7 +173,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
// continue; // continue;
Extra_ProgressBarUpdate( pProgress, i, NULL ); Extra_ProgressBarUpdate( pProgress, i, NULL );
// compute the cuts to the internal node // compute the cuts to the internal node
pList = Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree ); pList = (Cut_Cut_t *)Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree );
if ( pParams->fNpnSave && pList ) if ( pParams->fNpnSave && pList )
{ {
extern void Npn_ManSaveOne( unsigned * puTruth, int nVars ); extern void Npn_ManSaveOne( unsigned * puTruth, int nVars );
......
src/base/abci/abcDar.c
...@@ -35,6 +35,7 @@ ...@@ -35,6 +35,7 @@
#include "cec.h" #include "cec.h"
#include "csw.h" #include "csw.h"
#include "giaAbs.h" #include "giaAbs.h"
#include "pdr.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
...@@ -2245,14 +2246,6 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar ) ...@@ -2245,14 +2246,6 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
return RetValue; return RetValue;
} }
typedef struct Pdr_Par_t_ Pdr_Par_t;
struct Pdr_Par_t_
{
int fAbstract; // perform abstraction
int fVerbose; // enable verbose output
int fVeryVerbose; // enable verbose output
};
/**Function************************************************************* /**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.] Synopsis [Gives the current ABC network to AIG manager for processing.]
...@@ -2264,14 +2257,10 @@ struct Pdr_Par_t_ ...@@ -2264,14 +2257,10 @@ struct Pdr_Par_t_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex ) int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
{ {
// extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
// extern int Pdr_ManSolve( Aig_Man_t * pAig, Abc_Cex_t ** ppCex, Pdr_Par_t * pPars );
int RetValue = -1, clk = clock(); int RetValue = -1, clk = clock();
Pdr_Par_t Pars, * pPars = &Pars;
Aig_Man_t * pMan; Aig_Man_t * pMan;
// Pdr_ManSetDefaultParams( pPars );
*ppCex = NULL; *ppCex = NULL;
pMan = Abc_NtkToDar( pNtk, 0, 1 ); pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL ) if ( pMan == NULL )
...@@ -2279,7 +2268,18 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex ) ...@@ -2279,7 +2268,18 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex )
printf( "Converting network into AIG has failed.\n" ); printf( "Converting network into AIG has failed.\n" );
return -1; return -1;
} }
// RetValue = Pdr_ManSolve( pMan, ppCex, pPars ); // perform ORing the primary outputs
if ( pPars->iOutput == -1 )
{
Aig_Man_t * pTemp = Saig_ManDupOrpos( pMan );
RetValue = Pdr_ManSolve( pTemp, pPars, ppCex );
if ( RetValue == 0 )
(*ppCex)->iPo = Ssw_SmlFindOutputCounterExample( pMan, *ppCex );
Aig_ManStop( pTemp );
}
else
RetValue = Pdr_ManSolve( pMan, pPars, ppCex );
// output the result
if ( RetValue == 1 ) if ( RetValue == 1 )
printf( "Property proved. " ); printf( "Property proved. " );
else if ( RetValue == 0 ) else if ( RetValue == 0 )
...@@ -2931,6 +2931,34 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ) ...@@ -2931,6 +2931,34 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs targe enlargement.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose )
{
extern Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose );
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
pTemp = Saig_ManTempor( pMan, nFrames, TimeOut, nConfLimit, fUseBmc, fVerbose, fVeryVerbose );
Aig_ManStop( pMan );
if ( pTemp == NULL )
return Abc_NtkDup( pNtk );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pTemp );
Aig_ManStop( pTemp );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Performs induction for property only.] Synopsis [Performs induction for property only.]
Description [] Description []
......
src/base/abci/abcIvy.c
...@@ -508,7 +508,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars ) ...@@ -508,7 +508,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
// pParams->fUseBdds = 1; // pParams->fUseBdds = 1;
// pParams->fBddReorder = 1; // pParams->fBddReorder = 1;
// pParams->nTotalBacktrackLimit = 10000; // pParams->nTotalBacktrackLimit = 10000;
// strash the network if it is not strashed already // strash the network if it is not strashed already
if ( !Abc_NtkIsStrash(pNtk) ) if ( !Abc_NtkIsStrash(pNtk) )
{ {
......
src/base/cmd/cmdPlugin.c
...@@ -136,7 +136,7 @@ char * Abc_GetBinaryName( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -136,7 +136,7 @@ char * Abc_GetBinaryName( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
i++; i++;
if ( strcmp( pTemp, argv[0] ) == 0 ) if ( strcmp( pTemp, argv[0] ) == 0 )
return Vec_PtrEntry( pAbc->vPlugInComBinPairs, i ); return (char *)Vec_PtrEntry( pAbc->vPlugInComBinPairs, i );
} }
assert( 0 ); assert( 0 );
return NULL; return NULL;
......
src/base/io/ioReadBlifMv.c
...@@ -232,6 +232,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) ...@@ -232,6 +232,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
Vec_PtrForEachEntry( char *, vGlobalLtlArray, pLtlProp, i ) Vec_PtrForEachEntry( char *, vGlobalLtlArray, pLtlProp, i )
Vec_PtrPush( pNtk->vLtlProperties, pLtlProp ); Vec_PtrPush( pNtk->vLtlProperties, pLtlProp );
Vec_PtrFreeP( &vGlobalLtlArray );
return pNtk; return pNtk;
} }
......
src/base/io/ioReadPla.c
...@@ -51,6 +51,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fCheck ) ...@@ -51,6 +51,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fCheck )
// start the file // start the file
p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t|" ); p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t|" );
// p = Extra_FileReaderAlloc( pFileName, "", "\n\r", " \t|" );
if ( p == NULL ) if ( p == NULL )
return NULL; return NULL;
...@@ -91,7 +92,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros ) ...@@ -91,7 +92,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
int nInputs = -1, nOutputs = -1, nProducts = -1; int nInputs = -1, nOutputs = -1, nProducts = -1;
char * pCubeIn, * pCubeOut; char * pCubeIn, * pCubeOut;
int i, k, iLine, nDigits, nCubes; int i, k, iLine, nDigits, nCubes;
// allocate the empty network // allocate the empty network
pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) ); pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) );
...@@ -103,9 +104,17 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros ) ...@@ -103,9 +104,17 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL ); Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
// if it is the end of file, quit the loop // if it is the end of file, quit the loop
if ( strcmp( (char *)vTokens->pArray[0], ".e" ) == 0 ) if ( strncmp( (char *)vTokens->pArray[0], ".e", 2 ) == 0 )
break; break;
// if it is the model name, get the name
if ( strcmp( (char *)vTokens->pArray[0], ".model" ) == 0 )
{
ABC_FREE( pNtk->pName );
pNtk->pName = Extra_UtilStrsav( (char *)vTokens->pArray[1] );
continue;
}
if ( vTokens->nSize == 1 ) if ( vTokens->nSize == 1 )
{ {
printf( "%s (line %d): Wrong number of token.\n", printf( "%s (line %d): Wrong number of token.\n",
......
src/misc/util/utilFile.c
...@@ -98,6 +98,7 @@ int tmpFile(const char* prefix, const char* suffix, char** out_name) ...@@ -98,6 +98,7 @@ int tmpFile(const char* prefix, const char* suffix, char** out_name)
free(*out_name); free(*out_name);
*out_name = NULL; *out_name = NULL;
}else{ }else{
// Kludge: // Kludge:
close(fd); close(fd);
unlink(*out_name); unlink(*out_name);
...@@ -107,6 +108,11 @@ int tmpFile(const char* prefix, const char* suffix, char** out_name) ...@@ -107,6 +108,11 @@ int tmpFile(const char* prefix, const char* suffix, char** out_name)
free(*out_name); free(*out_name);
*out_name = NULL; *out_name = NULL;
} }
// assert( 0 );
// commented out because had problem with g++ saying that
// close() and unlink() are not defined in the namespace
} }
return fd; return fd;
......
src/opt/mfs/mfsCore.c
...@@ -268,10 +268,10 @@ clk = clock(); ...@@ -268,10 +268,10 @@ clk = clock();
p->nNodesBad++; p->nNodesBad++;
return 1; return 1;
} }
clk = clock(); //clk = clock();
if ( p->pPars->fGiaSat ) // if ( p->pPars->fGiaSat )
Abc_NtkMfsConstructGia( p ); // Abc_NtkMfsConstructGia( p );
p->timeGia += clock() - clk; //p->timeGia += clock() - clk;
// solve the SAT problem // solve the SAT problem
if ( p->pPars->fPower ) if ( p->pPars->fPower )
Abc_NtkMfsEdgePower( p, pNode ); Abc_NtkMfsEdgePower( p, pNode );
...@@ -284,8 +284,8 @@ p->timeGia += clock() - clk; ...@@ -284,8 +284,8 @@ p->timeGia += clock() - clk;
Abc_NtkMfsResubNode2( p, pNode ); Abc_NtkMfsResubNode2( p, pNode );
} }
p->timeSat += clock() - clk; p->timeSat += clock() - clk;
if ( p->pPars->fGiaSat ) // if ( p->pPars->fGiaSat )
Abc_NtkMfsDeconstructGia( p ); // Abc_NtkMfsDeconstructGia( p );
return 1; return 1;
} }
......
src/opt/mfs/mfsGia.c
...@@ -271,7 +271,7 @@ int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands ) ...@@ -271,7 +271,7 @@ int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands )
assert( Val3 == 1 ); assert( Val3 == 1 );
*/ */
// store the counter-example // store the counter-example
Vec_IntForEachEntry( p->vProjVars, iVar, i ) Vec_IntForEachEntry( p->vProjVarsSat, iVar, i )
{ {
pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
iOut = iVar - 2 * p->pCnf->nVars; iOut = iVar - 2 * p->pCnf->nVars;
......
src/opt/mfs/mfsInt.h
...@@ -61,19 +61,22 @@ struct Mfs_Man_t_ ...@@ -61,19 +61,22 @@ struct Mfs_Man_t_
Vec_Ptr_t * vNodes; // the internal nodes of the window Vec_Ptr_t * vNodes; // the internal nodes of the window
Vec_Ptr_t * vDivs; // the divisors of the node Vec_Ptr_t * vDivs; // the divisors of the node
Vec_Int_t * vDivLits; // the SAT literals of divisor nodes Vec_Int_t * vDivLits; // the SAT literals of divisor nodes
Vec_Int_t * vProjVars; // the projection variables Vec_Int_t * vProjVarsCnf; // the projection variables
Vec_Int_t * vProjVarsSat; // the projection variables
// intermediate simulation data // intermediate simulation data
Vec_Ptr_t * vDivCexes; // the counter-example for dividors Vec_Ptr_t * vDivCexes; // the counter-example for dividors
int nDivWords; // the number of words int nDivWords; // the number of words
int nCexes; // the numbe rof current counter-examples int nCexes; // the numbe rof current counter-examples
int nSatCalls; int nSatCalls;
int nSatCexes; int nSatCexes;
/*
// intermediate AIG data // intermediate AIG data
Gia_Man_t * pGia; // replica of the AIG in the new package Gia_Man_t * pGia; // replica of the AIG in the new package
// Gia_Obj_t ** pSat2Gia; // mapping of PO SAT var into internal GIA nodes // Gia_Obj_t ** pSat2Gia; // mapping of PO SAT var into internal GIA nodes
Tas_Man_t * pTas; // the SAT solver Tas_Man_t * pTas; // the SAT solver
Vec_Int_t * vCex; // the counter-example Vec_Int_t * vCex; // the counter-example
Vec_Ptr_t * vGiaLits; // literals given as assumptions Vec_Ptr_t * vGiaLits; // literals given as assumptions
*/
// used for bidecomposition // used for bidecomposition
Vec_Int_t * vTruth; Vec_Int_t * vTruth;
Bdc_Man_t * pManDec; Bdc_Man_t * pManDec;
...@@ -87,7 +90,7 @@ struct Mfs_Man_t_ ...@@ -87,7 +90,7 @@ struct Mfs_Man_t_
Int_Man_t * pMan; // interpolation manager; Int_Man_t * pMan; // interpolation manager;
Vec_Int_t * vMem; // memory for intermediate SOPs Vec_Int_t * vMem; // memory for intermediate SOPs
Vec_Vec_t * vLevels; // levelized structure for updating Vec_Vec_t * vLevels; // levelized structure for updating
Vec_Ptr_t * vFanins; // the new set of fanins Vec_Ptr_t * vMfsFanins; // the new set of fanins
int nTotConfLim; // total conflict limit int nTotConfLim; // total conflict limit
int nTotConfLevel; // total conflicts on this level int nTotConfLevel; // total conflicts on this level
// switching activity // switching activity
......
src/opt/mfs/mfsInter.c
...@@ -96,13 +96,13 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, ...@@ -96,13 +96,13 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert ); Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert );
// collect the outputs of the divisors // collect the outputs of the divisors
Vec_IntClear( p->vProjVars ); Vec_IntClear( p->vProjVarsCnf );
Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) ) Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
{ {
assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); Vec_IntPush( p->vProjVarsCnf, p->pCnf->pVarNums[pObjPo->Id] );
} }
assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) ); assert( Vec_IntSize(p->vProjVarsCnf) == Vec_PtrSize(p->vDivs) );
// start the solver // start the solver
pSat = sat_solver_new(); pSat = sat_solver_new();
...@@ -178,7 +178,7 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, ...@@ -178,7 +178,7 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
// get the variable number of this divisor // get the variable number of this divisor
i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
// get the corresponding SAT variable // get the corresponding SAT variable
iVar = Vec_IntEntry( p->vProjVars, i ); iVar = Vec_IntEntry( p->vProjVarsCnf, i );
// add the corresponding EXOR gate // add the corresponding EXOR gate
if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
{ {
...@@ -198,15 +198,17 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, ...@@ -198,15 +198,17 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
else else
{ {
// add the clauses for the EXOR gates - and remember their outputs // add the clauses for the EXOR gates - and remember their outputs
Vec_IntForEachEntry( p->vProjVars, iVar, i ) Vec_IntClear( p->vProjVarsSat );
Vec_IntForEachEntry( p->vProjVarsCnf, iVar, i )
{ {
if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
{ {
sat_solver_delete( pSat ); sat_solver_delete( pSat );
return NULL; return NULL;
} }
Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i ); Vec_IntPush( p->vProjVarsSat, 2 * p->pCnf->nVars + i );
} }
assert( Vec_IntSize(p->vProjVarsCnf) == Vec_IntSize(p->vProjVarsSat) );
// simplify the solver // simplify the solver
status = sat_solver_simplify(pSat); status = sat_solver_simplify(pSat);
if ( status == 0 ) if ( status == 0 )
...@@ -259,7 +261,7 @@ unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, i ...@@ -259,7 +261,7 @@ unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, i
// get the variable number of this divisor // get the variable number of this divisor
i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
// get the corresponding SAT variable // get the corresponding SAT variable
pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
} }
// derive the interpolant // derive the interpolant
...@@ -362,7 +364,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) ...@@ -362,7 +364,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
// get the variable number of this divisor // get the variable number of this divisor
i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
// get the corresponding SAT variable // get the corresponding SAT variable
pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
} }
// derive the interpolant // derive the interpolant
......
src/opt/mfs/mfsMan.c
...@@ -49,14 +49,15 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ) ...@@ -49,14 +49,15 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
p = ABC_ALLOC( Mfs_Man_t, 1 ); p = ABC_ALLOC( Mfs_Man_t, 1 );
memset( p, 0, sizeof(Mfs_Man_t) ); memset( p, 0, sizeof(Mfs_Man_t) );
p->pPars = pPars; p->pPars = pPars;
p->vProjVars = Vec_IntAlloc( 100 ); p->vProjVarsCnf = Vec_IntAlloc( 100 );
p->vProjVarsSat = Vec_IntAlloc( 100 );
p->vDivLits = Vec_IntAlloc( 100 ); p->vDivLits = Vec_IntAlloc( 100 );
p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX); p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX);
p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords ); p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords );
p->pMan = Int_ManAlloc(); p->pMan = Int_ManAlloc();
p->vMem = Vec_IntAlloc( 0 ); p->vMem = Vec_IntAlloc( 0 );
p->vLevels = Vec_VecStart( 32 ); p->vLevels = Vec_VecStart( 32 );
p->vFanins = Vec_PtrAlloc( 32 ); p->vMfsFanins= Vec_PtrAlloc( 32 );
return p; return p;
} }
...@@ -201,8 +202,9 @@ void Mfs_ManStop( Mfs_Man_t * p ) ...@@ -201,8 +202,9 @@ void Mfs_ManStop( Mfs_Man_t * p )
Int_ManFree( p->pMan ); Int_ManFree( p->pMan );
Vec_IntFree( p->vMem ); Vec_IntFree( p->vMem );
Vec_VecFree( p->vLevels ); Vec_VecFree( p->vLevels );
Vec_PtrFree( p->vFanins ); Vec_PtrFree( p->vMfsFanins );
Vec_IntFree( p->vProjVars ); Vec_IntFree( p->vProjVarsCnf );
Vec_IntFree( p->vProjVarsSat );
Vec_IntFree( p->vDivLits ); Vec_IntFree( p->vDivLits );
Vec_PtrFree( p->vDivCexes ); Vec_PtrFree( p->vDivCexes );
ABC_FREE( p ); ABC_FREE( p );
......
src/opt/mfs/mfsResub.c
...@@ -42,14 +42,14 @@ ABC_NAMESPACE_IMPL_START ...@@ -42,14 +42,14 @@ ABC_NAMESPACE_IMPL_START
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc ) void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vMfsFanins, Hop_Obj_t * pFunc )
{ {
Abc_Obj_t * pObjNew, * pFanin; Abc_Obj_t * pObjNew, * pFanin;
int k; int k;
// create the new node // create the new node
pObjNew = Abc_NtkCreateNode( pObj->pNtk ); pObjNew = Abc_NtkCreateNode( pObj->pNtk );
pObjNew->pData = pFunc; pObjNew->pData = pFunc;
Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pFanin, k ) Vec_PtrForEachEntry( Abc_Obj_t *, vMfsFanins, pFanin, k )
Abc_ObjAddFanin( pObjNew, pFanin ); Abc_ObjAddFanin( pObjNew, pFanin );
// replace the old node by the new node // replace the old node by the new node
//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj ); //printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
...@@ -103,14 +103,14 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) ...@@ -103,14 +103,14 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
int fVeryVerbose = 0; int fVeryVerbose = 0;
unsigned * pData; unsigned * pData;
int RetValue, RetValue2 = -1, iVar, i, clk = clock(); int RetValue, RetValue2 = -1, iVar, i, clk = clock();
/*
if ( p->pPars->fGiaSat ) if ( p->pPars->fGiaSat )
{ {
RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands ); RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
p->timeGia += clock() - clk; p->timeGia += clock() - clk;
return RetValue2; return RetValue2;
} }
*/
p->nSatCalls++; p->nSatCalls++;
RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
// assert( RetValue == l_False || RetValue == l_True ); // assert( RetValue == l_False || RetValue == l_True );
...@@ -137,7 +137,7 @@ p->timeGia += clock() - clk; ...@@ -137,7 +137,7 @@ p->timeGia += clock() - clk;
printf( "S " ); printf( "S " );
p->nSatCexes++; p->nSatCexes++;
// store the counter-example // store the counter-example
Vec_IntForEachEntry( p->vProjVars, iVar, i ) Vec_IntForEachEntry( p->vProjVarsSat, iVar, i )
{ {
pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
...@@ -186,14 +186,14 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f ...@@ -186,14 +186,14 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
// try fanins without the critical fanin // try fanins without the critical fanin
nCands = 0; nCands = 0;
Vec_PtrClear( p->vFanins ); Vec_PtrClear( p->vMfsFanins );
Abc_ObjForEachFanin( pNode, pFanin, i ) Abc_ObjForEachFanin( pNode, pFanin, i )
{ {
if ( i == iFanin ) if ( i == iFanin )
continue; continue;
Vec_PtrPush( p->vFanins, pFanin ); Vec_PtrPush( p->vMfsFanins, pFanin );
iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
} }
RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands ); RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
if ( RetValue == -1 ) if ( RetValue == -1 )
...@@ -212,7 +212,7 @@ clk = clock(); ...@@ -212,7 +212,7 @@ clk = clock();
if ( pFunc == NULL ) if ( pFunc == NULL )
return 0; return 0;
// update the network // update the network
Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
p->timeInt += clock() - clk; p->timeInt += clock() - clk;
return 1; return 1;
} }
...@@ -269,7 +269,7 @@ p->timeInt += clock() - clk; ...@@ -269,7 +269,7 @@ p->timeInt += clock() - clk;
if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
return 0; return 0;
pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ); RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 );
if ( RetValue == -1 ) if ( RetValue == -1 )
return 0; return 0;
...@@ -287,8 +287,8 @@ clk = clock(); ...@@ -287,8 +287,8 @@ clk = clock();
if ( pFunc == NULL ) if ( pFunc == NULL )
return 0; return 0;
// update the network // update the network
Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
p->timeInt += clock() - clk; p->timeInt += clock() - clk;
return 1; return 1;
} }
...@@ -334,14 +334,14 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int ...@@ -334,14 +334,14 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
// try fanins without the critical fanin // try fanins without the critical fanin
nCands = 0; nCands = 0;
Vec_PtrClear( p->vFanins ); Vec_PtrClear( p->vMfsFanins );
Abc_ObjForEachFanin( pNode, pFanin, i ) Abc_ObjForEachFanin( pNode, pFanin, i )
{ {
if ( i == iFanin || i == iFanin2 ) if ( i == iFanin || i == iFanin2 )
continue; continue;
Vec_PtrPush( p->vFanins, pFanin ); Vec_PtrPush( p->vMfsFanins, pFanin );
iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
} }
RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands ); RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
if ( RetValue == -1 ) if ( RetValue == -1 )
...@@ -358,7 +358,7 @@ clk = clock(); ...@@ -358,7 +358,7 @@ clk = clock();
if ( pFunc == NULL ) if ( pFunc == NULL )
return 0; return 0;
// update the network // update the network
Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
p->timeInt += clock() - clk; p->timeInt += clock() - clk;
return 1; return 1;
} }
...@@ -435,8 +435,8 @@ p->timeInt += clock() - clk; ...@@ -435,8 +435,8 @@ p->timeInt += clock() - clk;
if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
return 0; return 0;
pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 );
pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ); RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 );
if ( RetValue == -1 ) if ( RetValue == -1 )
return 0; return 0;
...@@ -452,10 +452,10 @@ clk = clock(); ...@@ -452,10 +452,10 @@ clk = clock();
if ( pFunc == NULL ) if ( pFunc == NULL )
return 0; return 0;
// update the network // update the network
Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) ); Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar2) );
Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
assert( Vec_PtrSize(p->vFanins) == nCands + 2 ); assert( Vec_PtrSize(p->vMfsFanins) == nCands + 2 );
Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
p->timeInt += clock() - clk; p->timeInt += clock() - clk;
return 1; return 1;
} }
......
src/opt/mfs/mfsSat.c
...@@ -63,7 +63,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) ...@@ -63,7 +63,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
p->nCares++; p->nCares++;
// add SAT assignment to the solver // add SAT assignment to the solver
Mint = 0; Mint = 0;
Vec_IntForEachEntry( p->vProjVars, iVar, b ) Vec_IntForEachEntry( p->vProjVarsSat, iVar, b )
{ {
Lits[b] = toLit( iVar ); Lits[b] = toLit( iVar );
if ( sat_solver_var_value( p->pSat, iVar ) ) if ( sat_solver_var_value( p->pSat, iVar ) )
...@@ -75,7 +75,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) ...@@ -75,7 +75,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
assert( !Aig_InfoHasBit(p->uCare, Mint) ); assert( !Aig_InfoHasBit(p->uCare, Mint) );
Aig_InfoSetBit( p->uCare, Mint ); Aig_InfoSetBit( p->uCare, Mint );
// add the blocking clause // add the blocking clause
RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) ); RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVarsSat) );
if ( RetValue == 0 ) if ( RetValue == 0 )
return 0; return 0;
return 1; return 1;
...@@ -97,15 +97,15 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) ...@@ -97,15 +97,15 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
Aig_Obj_t * pObjPo; Aig_Obj_t * pObjPo;
int RetValue, i; int RetValue, i;
// collect projection variables // collect projection variables
Vec_IntClear( p->vProjVars ); Vec_IntClear( p->vProjVarsSat );
Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) ) Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) )
{ {
assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); Vec_IntPush( p->vProjVarsSat, p->pCnf->pVarNums[pObjPo->Id] );
} }
// prepare the truth table of care set // prepare the truth table of care set
p->nFanins = Vec_IntSize( p->vProjVars ); p->nFanins = Vec_IntSize( p->vProjVarsSat );
p->nWords = Aig_TruthWordNum( p->nFanins ); p->nWords = Aig_TruthWordNum( p->nFanins );
memset( p->uCare, 0, sizeof(unsigned) * p->nWords ); memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
......
src/opt/mfs/module.make
SRC += src/opt/mfs/mfsCore.c \ SRC += src/opt/mfs/mfsCore.c \
src/opt/mfs/mfsDiv.c \ src/opt/mfs/mfsDiv.c \
src/opt/mfs/mfsGia.c \
src/opt/mfs/mfsInter.c \ src/opt/mfs/mfsInter.c \
src/opt/mfs/mfsMan.c \ src/opt/mfs/mfsMan.c \
src/opt/mfs/mfsResub.c \ src/opt/mfs/mfsResub.c \
......
src/sat/bsat/satSolver.c
...@@ -28,6 +28,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ...@@ -28,6 +28,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "satStore.h" #include "satStore.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
#define SAT_USE_ANALYZE_FINAL
/* /*
extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
...@@ -40,8 +43,10 @@ extern int Sto_ManChangeLastClause( void * p ); ...@@ -40,8 +43,10 @@ extern int Sto_ManChangeLastClause( void * p );
extern void Sto_ManMarkRoots( void * p ); extern void Sto_ManMarkRoots( void * p );
extern void Sto_ManMarkClausesA( void * p ); extern void Sto_ManMarkClausesA( void * p );
*/ */
//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
//================================================================================================= //=================================================================================================
// Debug: // Debug:
...@@ -457,14 +462,14 @@ static inline int enqueue(sat_solver* s, lit l, clause* from) ...@@ -457,14 +462,14 @@ static inline int enqueue(sat_solver* s, lit l, clause* from)
} }
static inline void assume(sat_solver* s, lit l){ static inline int assume(sat_solver* s, lit l){
assert(s->qtail == s->qhead); assert(s->qtail == s->qhead);
assert(s->assigns[lit_var(l)] == l_Undef); assert(s->assigns[lit_var(l)] == l_Undef);
#ifdef VERBOSEDEBUG #ifdef VERBOSEDEBUG
printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l)); printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
#endif #endif
veci_push(&s->trail_lim,s->qtail); veci_push(&s->trail_lim,s->qtail);
enqueue(s,l,(clause*)0); return enqueue(s,l,(clause*)0);
} }
...@@ -624,52 +629,73 @@ static int sat_solver_lit_removable(sat_solver* s, lit l, int minl) ...@@ -624,52 +629,73 @@ static int sat_solver_lit_removable(sat_solver* s, lit l, int minl)
| stores the result in 'out_conflict'. | stores the result in 'out_conflict'.
|________________________________________________________________________________________________@*/ |________________________________________________________________________________________________@*/
/* /*
void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) void Solver::analyzeFinal(Clause* confl, bool skip_first)
{ {
out_conflict.clear(); // -- NOTE! This code is relatively untested. Please report bugs!
out_conflict.push(p); conflict.clear();
if (root_level == 0) return;
if (decisionLevel() == 0)
return; vec<char>& seen = analyze_seen;
for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
seen[var(p)] = 1; Var x = var((*confl)[i]);
if (level[x] > 0)
seen[x] = 1;
}
for (int i = trail.size()-1; i >= trail_lim[0]; i--){ int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level];
Var x = var(trail[i]); for (int i = start; i >= trail_lim[0]; i--){
Var x = var(trail[i]);
if (seen[x]){ if (seen[x]){
if (reason(x) == GClause_NULL){ GClause r = reason[x];
assert(level(x) > 0); if (r == GClause_NULL){
out_conflict.push(~trail[i]); assert(level[x] > 0);
conflict.push(~trail[i]);
}else{ }else{
Clause& c = ca.deref(smartReason(x)); if (r.isLit()){
for (int j = 1; j < c.size(); j++) Lit p = r.lit();
if (level(var(c[j])) > 0) if (level[var(p)] > 0)
seen[var(c[j])] = 1; seen[var(p)] = 1;
}else{
Clause& c = *r.clause();
for (int j = 1; j < c.size(); j++)
if (level[var(c[j])] > 0)
seen[var(c[j])] = 1;
}
} }
seen[x] = 0; seen[x] = 0;
} }
} }
seen[var(p)] = 0;
} }
*/ */
static void sat_solver_analyze_final(sat_solver* s, lit p, veci* out_conflict) #ifdef SAT_USE_ANALYZE_FINAL
static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first)
{ {
int i, j; int i, j, start;
veci_resize(out_conflict,0); veci_resize(&s->conf_final,0);
// veci_push(out_conflict,p); // do not write conflict literal if ( s->root_level == 0 )
if ( sat_solver_dlevel(s) == 0 )
return; return;
assert( veci_size(&s->tagged) == 0 ); assert( veci_size(&s->tagged) == 0 );
assert( s->tags[lit_var(p)] == l_Undef ); // assert( s->tags[lit_var(p)] == l_Undef );
s->tags[lit_var(p)] = l_True; // s->tags[lit_var(p)] = l_True;
for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){ for (i = skip_first ? 1 : 0; i < clause_size(conf); i++)
{
int x = lit_var(clause_begin(conf)[i]);
if (s->levels[x] > 0)
{
s->tags[x] = l_True;
veci_push(&s->tagged,x);
}
}
start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
int x = lit_var(s->trail[i]); int x = lit_var(s->trail[i]);
if (s->tags[x] == l_True){ if (s->tags[x] == l_True){
if (s->reasons[x] == NULL){ if (s->reasons[x] == NULL){
assert(s->levels[x] > 0); assert(s->levels[x] > 0);
veci_push(out_conflict,lit_neg(s->trail[i])); veci_push(&s->conf_final,lit_neg(s->trail[i]));
}else{ }else{
clause* c = s->reasons[x]; clause* c = s->reasons[x];
if (clause_is_lit(c)){ if (clause_is_lit(c)){
...@@ -698,6 +724,8 @@ static void sat_solver_analyze_final(sat_solver* s, lit p, veci* out_conflict) ...@@ -698,6 +724,8 @@ static void sat_solver_analyze_final(sat_solver* s, lit p, veci* out_conflict)
veci_resize(&s->tagged,0); veci_resize(&s->tagged,0);
} }
#endif
static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
{ {
...@@ -976,8 +1004,9 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT ...@@ -976,8 +1004,9 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
#endif #endif
s->stats.conflicts++; conflictC++; s->stats.conflicts++; conflictC++;
if (sat_solver_dlevel(s) == s->root_level){ if (sat_solver_dlevel(s) == s->root_level){
lit p = clause_is_lit(confl)? clause_read_lit(confl) : clause_begin(confl)[0]; #ifdef SAT_USE_ANALYZE_FINAL
// sat_solver_analyze_final(s, lit_neg(p), &s->conf_final); sat_solver_analyze_final(s, confl, 0);
#endif
veci_delete(&learnt_clause); veci_delete(&learnt_clause);
return l_False; return l_False;
} }
...@@ -988,6 +1017,10 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT ...@@ -988,6 +1017,10 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
blevel = s->root_level > blevel ? s->root_level : blevel; blevel = s->root_level > blevel ? s->root_level : blevel;
sat_solver_canceluntil(s,blevel); sat_solver_canceluntil(s,blevel);
sat_solver_record(s,&learnt_clause); sat_solver_record(s,&learnt_clause);
#ifdef SAT_USE_ANALYZE_FINAL
// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0;
#endif
act_var_decay(s); act_var_decay(s);
act_clause_decay(s); act_clause_decay(s);
...@@ -1340,25 +1373,107 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit ...@@ -1340,25 +1373,107 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) ) if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
s->nInsLimit = nInsLimitGlobal; s->nInsLimit = nInsLimitGlobal;
#ifndef SAT_USE_ANALYZE_FINAL
//printf("solve: "); printlits(begin, end); printf("\n"); //printf("solve: "); printlits(begin, end); printf("\n");
for (i = begin; i < end; i++){ for (i = begin; i < end; i++){
switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){ switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
case 1: /* l_True: */ case 1: // l_True:
break; break;
case 0: /* l_Undef */ case 0: // l_Undef
assume(s, *i); assume(s, *i);
if (sat_solver_propagate(s) == NULL) if (sat_solver_propagate(s) == NULL)
break; break;
// fallthrough // fallthrough
case -1: /* l_False */ case -1: // l_False
sat_solver_canceluntil(s, 0); sat_solver_canceluntil(s, 0);
return l_False; return l_False;
} }
} }
s->nCalls2++;
s->root_level = sat_solver_dlevel(s); s->root_level = sat_solver_dlevel(s);
#endif
/*
// Perform assumptions:
root_level = assumps.size();
for (int i = 0; i < assumps.size(); i++){
Lit p = assumps[i];
assert(var(p) < nVars());
if (!assume(p)){
GClause r = reason[var(p)];
if (r != GClause_NULL){
Clause* confl;
if (r.isLit()){
confl = propagate_tmpbin;
(*confl)[1] = ~p;
(*confl)[0] = r.lit();
}else
confl = r.clause();
analyzeFinal(confl, true);
conflict.push(~p);
}else
conflict.clear(),
conflict.push(~p);
cancelUntil(0);
return false; }
Clause* confl = propagate();
if (confl != NULL){
analyzeFinal(confl), assert(conflict.size() > 0);
cancelUntil(0);
return false; }
}
assert(root_level == decisionLevel());
*/
#ifdef SAT_USE_ANALYZE_FINAL
// Perform assumptions:
s->root_level = end - begin;
for ( i = begin; i < end; i++ )
{
lit p = *i;
assert(lit_var(p) < s->size);
veci_push(&s->trail_lim,s->qtail);
if (!enqueue(s,p,(clause*)0))
{
clause * r = s->reasons[lit_var(p)];
if (r != NULL)
{
clause* confl;
if (clause_is_lit(r))
{
confl = s->binary;
(clause_begin(confl))[1] = lit_neg(p);
(clause_begin(confl))[0] = clause_read_lit(r);
}
else
confl = r;
sat_solver_analyze_final(s, confl, 1);
veci_push(&s->conf_final, lit_neg(p));
}
else
{
veci_resize(&s->conf_final,0);
veci_push(&s->conf_final, lit_neg(p));
}
sat_solver_canceluntil(s, 0);
return l_False;
}
else
{
clause* confl = sat_solver_propagate(s);
if (confl != NULL){
sat_solver_analyze_final(s, confl, 0);
assert(s->conf_final.size > 0);
sat_solver_canceluntil(s, 0);
return l_False; }
}
}
assert(s->root_level == sat_solver_dlevel(s));
#endif
s->nCalls2++;
if (s->verbosity >= 1){ if (s->verbosity >= 1){
printf("==================================[MINISAT]===================================\n"); printf("==================================[MINISAT]===================================\n");
printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
......
src/sat/bsat/satSolver.h
...@@ -85,8 +85,6 @@ extern int sat_solver_nconflicts(sat_solver* s); ...@@ -85,8 +85,6 @@ extern int sat_solver_nconflicts(sat_solver* s);
extern void sat_solver_setnvars(sat_solver* s,int n); extern void sat_solver_setnvars(sat_solver* s,int n);
extern int sat_solver_final(sat_solver* s, int ** ppArray);
struct stats_t struct stats_t
{ {
ABC_INT64_T starts, decisions, propagations, inspects, conflicts; ABC_INT64_T starts, decisions, propagations, inspects, conflicts;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment