From de978ced7b754706efaf18ae588e18eb05624faf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 19 Jul 2008 08:01:00 -0700 Subject: Version abc80719 --- abc.dsp | 8 ++- src/aig/cnf/cnf.h | 1 + src/aig/cnf/cnfMan.c | 16 +++++ src/aig/fra/fraSec.c | 4 +- src/aig/saig/module.make | 3 +- src/aig/saig/saig.h | 2 +- src/aig/saig/saigInter.c | 131 +++++++++++++++++++++++++++++++---- src/aig/saig/saigUnique.c | 170 ++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abc.c | 17 +++-- src/base/abci/abcDar.c | 4 +- src/map/pcm/module.make | 0 src/map/ply/module.make | 0 src/sat/bsat/satInterA.c | 8 ++- src/sat/bsat/satSolver.c | 36 +++++++--- src/sat/bsat/satSolver.h | 1 + 15 files changed, 360 insertions(+), 41 deletions(-) create mode 100644 src/aig/saig/saigUnique.c delete mode 100644 src/map/pcm/module.make delete mode 100644 src/map/ply/module.make diff --git a/abc.dsp b/abc.dsp index a8f63e61..4469f3b3 100644 --- a/abc.dsp +++ b/abc.dsp @@ -42,7 +42,7 @@ RSC=rc.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c +# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -66,7 +66,7 @@ LINK32=link.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c -# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c +# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /GZ /c # SUBTRACT CPP /X # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" @@ -3224,6 +3224,10 @@ SOURCE=.\src\aig\saig\saigScl.c SOURCE=.\src\aig\saig\saigTrans.c # End Source File +# Begin Source File + +SOURCE=.\src\aig\saig\saigUnique.c +# End Source File # End Group # End Group # End Group diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index 5c742f5d..f4f782df 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -136,6 +136,7 @@ extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p ); extern void Cnf_DataFree( Cnf_Dat_t * p ); extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ); +extern void Cnf_DataFlipLastLiteral( Cnf_Dat_t * p ); extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index f1c446fe..1e650a05 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -202,6 +202,22 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ) p->pClauses[0][v] += 2*nVarsPlus; } +/**Function************************************************************* + + Synopsis [Writes CNF into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_DataFlipLastLiteral( Cnf_Dat_t * p ) +{ + p->pClauses[0][p->nLiterals-1] = lit_neg( p->pClauses[0][p->nLiterals-1] ); +} + /**Function************************************************************* Synopsis [Writes CNF into a file.] diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 3365ac9a..3aafeb18 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -389,11 +389,11 @@ PRT( "Time", clock() - clkTotal ); clk = clock(); if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 ) { - extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose, int * pDepth ); + extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ); int Depth; pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); - RetValue = Saig_Interpolate( pNew, 5000, 0, 1, 0, pParSec->fVeryVerbose, &Depth ); + RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 1, 1, pParSec->fVeryVerbose, &Depth ); if ( pParSec->fVerbose ) { if ( RetValue == 1 ) diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 6639db21..b9a18ce2 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -9,4 +9,5 @@ SRC += src/aig/saig/saigBmc.c \ src/aig/saig/saigRetMin.c \ src/aig/saig/saigRetStep.c \ src/aig/saig/saigScl.c \ - src/aig/saig/saigTrans.c + src/aig/saig/saigTrans.c \ + src/aig/saig/saigUnique.c diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 4ae07063..5a7beeec 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -85,7 +85,7 @@ extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); /*=== saigInter.c ==========================================================*/ -extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose, int * pDepth ); +extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ); /*=== saigMiter.c ==========================================================*/ extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); /*=== saigPhase.c ==========================================================*/ diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index 37eb3349..86982d46 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -50,6 +50,7 @@ struct Saig_IntMan_t_ Vec_Int_t * vVarsAB; // the variables participating in // temporary place for the new interpolant Aig_Man_t * pInterNew; + Vec_Ptr_t * vInters; // parameters int nFrames; // the number of timeframes int nConfCur; // the current number of conflicts @@ -65,7 +66,9 @@ struct Saig_IntMan_t_ int timeTotal; }; +#ifdef ABC_USE_LIBRARIES static int Saig_M144pPerformOneStep( Saig_IntMan_t * p ); +#endif //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -328,7 +331,10 @@ sat_solver * Saig_DeriveSatSolver( for ( i = 0; i < pCnfFrames->nClauses; i++ ) { if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) - assert( 0 ); + { + pSat->fSolved = 1; + break; + } } sat_solver_store_mark_roots( pSat ); // return clauses to the original state @@ -604,7 +610,7 @@ p->timeSat += clock() - clk; else if ( status == l_True ) { RetValue = 0; - } + } else { RetValue = -1; @@ -686,6 +692,26 @@ void Saig_ManagerClean( Saig_IntMan_t * p ) Aig_ManStop( p->pFrames ); } +/**Function************************************************************* + + Synopsis [Frees the interpolation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManagerFreeInters( Saig_IntMan_t * p ) +{ + Aig_Man_t * pTemp; + int i; + Vec_PtrForEachEntry( p->vInters, pTemp, i ) + Aig_ManStop( pTemp ); + Vec_PtrClear( p->vInters ); +} + /**Function************************************************************* Synopsis [Frees the interpolation manager.] @@ -727,6 +753,8 @@ void Saig_ManagerFree( Saig_IntMan_t * p ) Aig_ManStop( p->pInter ); if ( p->pInterNew ) Aig_ManStop( p->pInterNew ); + Saig_ManagerFreeInters( p ); + Vec_PtrFree( p->vInters ); free( p ); } @@ -743,7 +771,7 @@ void Saig_ManagerFree( Saig_IntMan_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p ) +int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p, int fSubtractOld ) { sat_solver * pSat; Aig_Man_t * pInterOld = p->pInter; @@ -757,7 +785,10 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p ) // start the solver pSat = sat_solver_new(); - sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars ); + if ( fSubtractOld ) + sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars + pCnfOld->nVars ); + else + sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars ); // interpolant for ( i = 0; i < pCnfNew->nClauses; i++ ) @@ -803,21 +834,48 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p ) } // complement the last literal - Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1]; - pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]); // add clauses of B + Cnf_DataFlipLastLiteral( pCnfNew ); for ( i = 0; i < pCnfNew->nClauses; i++ ) { if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) ) - assert( 0 ); + { +// assert( 0 ); + Cnf_DataFree( pCnfNew ); + return 1; + } } - // complement the last literal - Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1]; - pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]); + Cnf_DataFlipLastLiteral( pCnfNew ); // return clauses to the original state Cnf_DataLift( pCnfTrans, -pCnfNew->nVars ); Cnf_DataLift( pCnfNew, -pCnfNew->nVars -pCnfTrans->nVars ); + if ( fSubtractOld ) + { + Cnf_DataLift( pCnfOld, 2 * pCnfNew->nVars + pCnfTrans->nVars ); + // old interpolant clauses + Cnf_DataFlipLastLiteral( pCnfOld ); + for ( i = 0; i < pCnfOld->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfOld->pClauses[i], pCnfOld->pClauses[i+1] ) ) + assert( 0 ); + } + Cnf_DataFlipLastLiteral( pCnfOld ); + // connector clauses + Aig_ManForEachPi( pInterOld, pObj, i ) + { + pObj2 = Aig_ManPi( pInterNew, i ); + Lits[0] = toLitCond( pCnfOld->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfNew->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfOld->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfNew->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + Cnf_DataLift( pCnfOld, - 2 * pCnfNew->nVars - pCnfTrans->nVars ); + } Cnf_DataFree( pCnfNew ); // solve the problem @@ -838,8 +896,9 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fVerbose, int * pDepth ) +int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ) { + extern int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters ); Saig_IntMan_t * p; Aig_Man_t * pAigTemp; int s, i, RetValue, Status, clk, clk2, clkTotal = clock(); @@ -856,6 +915,7 @@ int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRew p->nFrames = 1; p->nConfLimit = nConfLimit; p->fVerbose = fVerbose; + p->vInters = Vec_PtrAlloc( 10 ); // can perform SAT sweeping and/or rewriting of this AIG... p->pAig = pAig; if ( fTransLoop ) @@ -878,9 +938,11 @@ p->timeCnf += clock() - clk; *pDepth = -1; for ( s = 0; ; s++ ) { + Saig_ManagerFreeInters( p ); clk2 = clock(); // initial state p->pInter = Saig_ManInit( Aig_ManRegNum(pAig) ); + Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInter) ); clk = clock(); p->pCnfInter = Cnf_Derive( p->pInter, 0 ); p->timeCnf += clock() - clk; @@ -919,10 +981,13 @@ p->timeCnf += clock() - clk; } // perform interplation clk = clock(); +#ifdef ABC_USE_LIBRARIES if ( fUseIp ) RetValue = Saig_M144pPerformOneStep( p ); else +#endif RetValue = Saig_PerformOneStep( p, 0 ); + if ( fVerbose ) { printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ", @@ -960,11 +1025,15 @@ clk = clock(); p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 ); Aig_ManStop( pAigTemp ); p->timeRwr += clock() - clk; + // save the new interpolant + Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInterNew) ); // check containment of interpolants clk = clock(); - if ( fCheckInd ) - Status = Saig_ManCheckInductiveContainment( p ); - else + if ( fCheckKstep ) // k-step unique-state induction + Status = Saig_ManUniqueState( p->pAigTrans, p->vInters ); + else if ( fCheckInd ) // simple induction + Status = Saig_ManCheckInductiveContainment( p, 1 ); + else // combinational containment Status = Saig_ManCheckContainment( p->pInterNew, p->pInter ); p->timeEqu += clock() - clk; if ( Status ) // contained @@ -1004,6 +1073,8 @@ p->timeCnf += clock() - clk; } +#ifdef ABC_USE_LIBRARIES + #include "m114p.h" /**Function************************************************************* @@ -1134,10 +1205,14 @@ Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_ Aig_Man_t * p; Aig_Obj_t * pInter, * pInter2, * pVar; Vec_Ptr_t * vInters; + Vec_Int_t * vASteps; int * pLits, * pClauses, * pVars; - int nLits, nVars, i, k, iVar; + int nLits, nVars, i, k, iVar, haveASteps; + int CountA, CountB, CountC, CountCsaved; + assert( M114p_SolverProofIsReady(s) ); vInters = Vec_PtrAlloc( 1000 ); + vASteps = Vec_IntAlloc( 1000 ); // process root clauses p = Aig_ManStart( 10000 ); M114p_SolverForEachRoot( s, &pLits, nLits, i ) @@ -1157,26 +1232,50 @@ Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_ } } Vec_PtrPush( vInters, pInter ); + Vec_IntPush( vASteps, 0 ); } assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); // process learned clauses + CountA = CountB = CountC = CountCsaved = 0; M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) { pInter = Vec_PtrEntry( vInters, pClauses[0] ); + haveASteps = Vec_IntEntry( vASteps, pClauses[0] ); for ( k = 0; k < nVars; k++ ) { iVar = Vec_IntEntry( vMapVars, pVars[k] ); pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); + haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] ); if ( iVar == -1 ) // var of A + { + haveASteps = 1; pInter = Aig_Or( p, pInter, pInter2 ); + } else // var of B or C pInter = Aig_And( p, pInter, pInter2 ); + + if ( iVar == -1 ) + CountA++; + else if ( iVar == -2 ) + CountB++; + else + { + if ( haveASteps == 0 ) + CountCsaved++; + CountC++; + } } Vec_PtrPush( vInters, pInter ); + Vec_IntPush( vASteps, haveASteps ); } +// printf( "ResSteps: A = %6d. B = %6d. C = %6d. C_saved = %6d. (%6.2f %%)\n", +// CountA, CountB, CountC, CountCsaved, 100.0 * CountCsaved/CountC ); + assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); Vec_PtrFree( vInters ); + Vec_IntFree( vASteps ); + Aig_ObjCreatePo( p, pInter ); Aig_ManCleanup( p ); return p; @@ -1229,6 +1328,8 @@ p->timeInt += clock() - clk; return RetValue; } +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigUnique.c b/src/aig/saig/saigUnique.c new file mode 100644 index 00000000..8b4d80e7 --- /dev/null +++ b/src/aig/saig/saigUnique.c @@ -0,0 +1,170 @@ +/**CFile**************************************************************** + + FileName [saigUnique.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Containment checking with unique state constraints.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigUnique.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" +#include "cnf.h" +#include "satSolver.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for interpolation.] + + Description [The resulting manager is combinational. The primary inputs + corresponding to register outputs are ordered first.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f; + assert( Saig_ManRegNum(pAig) > 0 ); + pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) ); + Saig_ManForEachLo( pAig, pObj, i ) + { + pObj->pData = Aig_ObjCreatePi( pFrames ); + Vec_PtrPush( *pvMapReg, pObj->pData ); + } + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + { + pObjLo->pData = pObjLi->pData; + Vec_PtrPush( *pvMapReg, pObjLo->pData ); + } + } + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while mapping PIs into the given array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl ) +{ + Aig_Obj_t * pObj; + int i; + assert( Aig_ManPoNum(pOld) == 1 ); + // create the PIs + Aig_ManCleanData( pOld ); + Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( pOld, pObj, i ) + pObj->pData = ppNewPis[i]; + // duplicate internal nodes + Aig_ManForEachNode( pOld, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // add one PO to new + pObj = Aig_ManPo( pOld, 0 ); + Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters ) +{ + Aig_Man_t * pFrames, * pInterNext, * pInterThis; + Aig_Obj_t ** ppNodes; + Vec_Ptr_t * vMapRegs; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + int f, nRegs, status; + nRegs = Saig_ManRegNum(pTrans); + assert( nRegs > 0 ); + assert( Vec_PtrSize(vInters) > 1 ); + // generate the timeframes + pFrames = Saig_ManFramesLatches( pTrans, Vec_PtrSize(vInters)-1, &vMapRegs ); + assert( Vec_PtrSize(vMapRegs) == Vec_PtrSize(vInters) * nRegs ); + // add main constraints to the timeframes + ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs); + Vec_PtrForEachEntryStop( vInters, pInterThis, f, Vec_PtrSize(vInters)-1 ) + { + assert( nRegs == Aig_ManPiNum(pInterThis) ); + pInterNext = Vec_PtrEntry( vInters, f+1 ); + Saig_ManAppendCone( pInterNext, pFrames, ppNodes + f * nRegs, 0 ); + Saig_ManAppendCone( pInterThis, pFrames, ppNodes + f * nRegs, 1 ); + } + Saig_ManAppendCone( Vec_PtrEntryLast(vInters), pFrames, ppNodes + f * nRegs, 1 ); + Aig_ManCleanup( pFrames ); + Vec_PtrFree( vMapRegs ); + + // convert to CNF + pCnf = Cnf_Derive( pFrames, 0 ); + pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + + if ( pSat == NULL ) + return 1; + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); + sat_solver_delete( pSat ); + return status == l_False; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index cb3d2d86..264b1df4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -15348,9 +15348,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) int fTransLoop; int fUsePudlak; int fCheckInd; + int fCheckKstep; int fVerbose; - extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose ); + extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -15363,9 +15364,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fTransLoop = 1; fUsePudlak = 0; fCheckInd = 0; + fCheckKstep= 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpikvh" ) ) != EOF ) { switch ( c ) { @@ -15403,6 +15405,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'i': fCheckInd ^= 1; break; + case 'k': + fCheckKstep ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -15432,18 +15437,20 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" ); return 0; } - Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose ); + Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose ); return 0; usage: - fprintf( pErr, "usage: int [-CF num] [-rtpivh]\n" ); + fprintf( pErr, "usage: int [-CF num] [-rtpikvh]\n" ); fprintf( pErr, "\t uses interpolation to prove the property\n" ); fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit ); fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax ); fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" ); - fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" ); +// fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" ); + fprintf( pErr, "\t-p : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUsePudlak? "yes": "no" ); fprintf( pErr, "\t-i : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" ); + fprintf( pErr, "\t-k : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index e47582e9..e32dbce0 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1270,7 +1270,7 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose ) +int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose ) { Aig_Man_t * pMan; int RetValue, Depth, clk = clock(); @@ -1282,7 +1282,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fR return -1; } assert( pMan->nRegs > 0 ); - RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose, &Depth ); + RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose, &Depth ); if ( RetValue == 1 ) printf( "Property proved. " ); else if ( RetValue == 0 ) diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make deleted file mode 100644 index e69de29b..00000000 diff --git a/src/map/ply/module.make b/src/map/ply/module.make deleted file mode 100644 index e69de29b..00000000 diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index 5837e68f..82f4e034 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -809,8 +809,12 @@ int Inta_ManProcessRoots( Inta_Man_t * p ) if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) ) { // detected root level conflict - printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" ); - assert( 0 ); +// printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" ); +// assert( 0 ); + // detected root level conflict + Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); return 0; } } diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 0179796c..12529ca7 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1061,7 +1061,8 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) begin = veci_begin( &s->temp_clause ); end = begin + veci_size( &s->temp_clause ); - if (begin == end) return false; + if (begin == end) + return false; //printlits(begin,end); printf("\n"); // insertion sort @@ -1076,6 +1077,16 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) sat_solver_setnvars(s,maxvar+1); // sat_solver_setnvars(s, lit_var(*(end-1))+1 ); + /////////////////////////////////// + // add clause to internal storage + if ( s->pStore ) + { + extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); + int RetValue = Sto_ManAddClause( s->pStore, begin, end ); + assert( RetValue ); + } + /////////////////////////////////// + //printlits(begin,end); printf("\n"); values = s->assigns; @@ -1095,16 +1106,6 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) if (j == begin) // empty clause return false; - /////////////////////////////////// - // add clause to internal storage - if ( s->pStore ) - { - extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); - int RetValue = Sto_ManAddClause( s->pStore, begin, j ); - assert( RetValue ); - } - /////////////////////////////////// - if (j - begin == 1) // unit clause return enqueue(s,*begin,(clause*)0); @@ -1164,6 +1165,19 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin lbool* values = s->assigns; lit* i; + //////////////////////////////////////////////// + if ( s->fSolved ) + { + if ( s->pStore ) + { + extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); + int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL ); + assert( RetValue ); + } + return l_False; + } + //////////////////////////////////////////////// + // set the external limits s->nCalls++; s->nRestarts = 0; diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 9ffc2b75..86e7a966 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -182,6 +182,7 @@ struct sat_solver_t // clause store void * pStore; + int fSolved; // trace recording FILE * pFile; -- cgit v1.2.3