| /**CFile**************************************************************** |
| |
| FileName [pdrInv.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Property driven reachability.] |
| |
| Synopsis [Invariant computation, printing, verification.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - November 20, 2010.] |
| |
| Revision [$Id: pdrInv.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "pdrInt.h" |
| #include "base/abc/abc.h" // for Abc_NtkCollectCioNames() |
| #include "base/main/main.h" // for Abc_FrameReadGlobalFrame() |
| #include "aig/ioa/ioa.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) |
| { |
| Vec_Ptr_t * vVec; |
| int i, ThisSize, Length, LengthStart; |
| if ( Vec_PtrSize(p->vSolvers) < 2 ) |
| { |
| Abc_Print(1, "Frame " ); |
| Abc_Print(1, "Clauses " ); |
| Abc_Print(1, "Max Queue " ); |
| Abc_Print(1, "Flops " ); |
| Abc_Print(1, "Cex " ); |
| Abc_Print(1, "Time" ); |
| Abc_Print(1, "\n" ); |
| return; |
| } |
| if ( Abc_FrameIsBatchMode() && !fClose ) |
| return; |
| // count the total length of the printout |
| Length = 0; |
| Vec_VecForEachLevel( p->vClauses, vVec, i ) |
| Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); |
| // determine the starting point |
| LengthStart = Abc_MaxInt( 0, Length - 60 ); |
| Abc_Print( 1, "%3d :", Vec_PtrSize(p->vSolvers)-1 ); |
| ThisSize = 5; |
| if ( LengthStart > 0 ) |
| { |
| Abc_Print( 1, " ..." ); |
| ThisSize += 4; |
| } |
| Length = 0; |
| Vec_VecForEachLevel( p->vClauses, vVec, i ) |
| { |
| if ( Length < LengthStart ) |
| { |
| Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); |
| continue; |
| } |
| Abc_Print( 1, " %d", Vec_PtrSize(vVec) ); |
| Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); |
| ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); |
| } |
| for ( i = ThisSize; i < 70; i++ ) |
| Abc_Print( 1, " " ); |
| Abc_Print( 1, "%5d", p->nQueMax ); |
| Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops ); |
| if ( p->pPars->fUseAbs ) |
| Abc_Print( 1, "%4d", p->nCexes ); |
| Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC ); |
| if ( p->pPars->fSolveAll ) |
| Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts ); |
| if ( p->pPars->nTimeOutOne ) |
| Abc_Print( 1, " T/O =%3d", p->pPars->nDropOuts ); |
| Abc_Print( 1, "%s", fClose ? "\n":"\r" ); |
| if ( fClose ) |
| p->nQueMax = 0, p->nCexes = 0; |
| fflush( stdout ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Counts how many times each flop appears in the set of cubes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) |
| { |
| Vec_Int_t * vFlopCount; |
| Pdr_Set_t * pCube; |
| int i, n; |
| vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) ); |
| Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) |
| { |
| if ( pCube->nRefs == -1 ) |
| continue; |
| for ( n = 0; n < pCube->nLits; n++ ) |
| { |
| assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) ); |
| Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 ); |
| } |
| } |
| return vFlopCount; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Pdr_ManFindInvariantStart( Pdr_Man_t * p ) |
| { |
| Vec_Ptr_t * vArrayK; |
| int k, kMax = Vec_PtrSize(p->vSolvers)-1; |
| Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax+1 ) |
| if ( Vec_PtrSize(vArrayK) == 0 ) |
| return k; |
| // return -1; |
| // if there is no starting point (as in case of SAT or undecided), return the last frame |
| // Abc_Print( 1, "The last timeframe contains %d clauses.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, kMax)) ); |
| return kMax; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Counts the number of variables used in the clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Pdr_ManCollectCubes( Pdr_Man_t * p, int kStart ) |
| { |
| Vec_Ptr_t * vResult; |
| Vec_Ptr_t * vArrayK; |
| Pdr_Set_t * pSet; |
| int i, j; |
| vResult = Vec_PtrAlloc( 100 ); |
| Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, kStart ) |
| Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pSet, j ) |
| Vec_PtrPush( vResult, pSet ); |
| return vResult; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Pdr_ManCountFlopsInv( Pdr_Man_t * p ) |
| { |
| int kStart = Pdr_ManFindInvariantStart(p); |
| Vec_Ptr_t *vCubes = Pdr_ManCollectCubes(p, kStart); |
| Vec_Int_t * vInv = Pdr_ManCountFlops( p, vCubes ); |
| Vec_PtrFree(vCubes); |
| return vInv; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Counts the number of variables used in the clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart ) |
| { |
| Vec_Int_t * vFlopCounts; |
| Vec_Ptr_t * vCubes; |
| int i, Entry, Counter = 0; |
| if ( p->vInfCubes == NULL ) |
| vCubes = Pdr_ManCollectCubes( p, kStart ); |
| else |
| vCubes = Vec_PtrDup( p->vInfCubes ); |
| vFlopCounts = Pdr_ManCountFlops( p, vCubes ); |
| Vec_IntForEachEntry( vFlopCounts, Entry, i ) |
| Counter += (Entry > 0); |
| Vec_IntFreeP( &vFlopCounts ); |
| Vec_PtrFree( vCubes ); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart ) |
| { |
| Vec_Ptr_t * vArrayK; |
| Pdr_Set_t * pCube; |
| int i, k, Counter = 0; |
| Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart ) |
| { |
| Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare ); |
| Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i ) |
| { |
| Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k ); |
| Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL ); |
| Abc_Print( 1, "\n" ); |
| } |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Pdr_SetPrintOne( Pdr_Set_t * p ) |
| { |
| int i; |
| Abc_Print(1, "Clause: {" ); |
| for ( i = 0; i < p->nLits; i++ ) |
| Abc_Print(1, " %s%d", Abc_LitIsCompl(p->Lits[i])? "!":"", Abc_Lit2Var(p->Lits[i]) ); |
| Abc_Print(1, " }\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Pdr_ManDupAigWithClauses( Aig_Man_t * p, Vec_Ptr_t * vCubes ) |
| { |
| Aig_Man_t * pNew; |
| Aig_Obj_t * pObj, * pObjNew, * pLit; |
| Pdr_Set_t * pCube; |
| int i, n; |
| // create the new manager |
| pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| // create the PIs |
| Aig_ManCleanData( p ); |
| Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); |
| Aig_ManForEachCi( p, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pNew ); |
| // create outputs for each cube |
| Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) |
| { |
| // Pdr_SetPrintOne( pCube ); |
| pObjNew = Aig_ManConst1(pNew); |
| for ( n = 0; n < pCube->nLits; n++ ) |
| { |
| assert( Abc_Lit2Var(pCube->Lits[n]) < Saig_ManRegNum(p) ); |
| pLit = Aig_NotCond( Aig_ManCi(pNew, Saig_ManPiNum(p) + Abc_Lit2Var(pCube->Lits[n])), Abc_LitIsCompl(pCube->Lits[n]) ); |
| pObjNew = Aig_And( pNew, pObjNew, pLit ); |
| } |
| Aig_ObjCreateCo( pNew, pObjNew ); |
| } |
| // duplicate internal nodes |
| Aig_ManForEachNode( p, pObj, i ) |
| pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| // add the POs |
| Saig_ManForEachLi( p, pObj, i ) |
| Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| Aig_ManCleanup( pNew ); |
| Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) ); |
| // check the resulting network |
| if ( !Aig_ManCheck(pNew) ) |
| Abc_Print(1, "Aig_ManDupSimple(): The check has failed.\n" ); |
| return pNew; |
| } |
| void Pdr_ManDumpAig( Aig_Man_t * p, Vec_Ptr_t * vCubes ) |
| { |
| Aig_Man_t * pNew = Pdr_ManDupAigWithClauses( p, vCubes ); |
| Ioa_WriteAiger( pNew, "aig_with_clauses.aig", 0, 0 ); |
| Aig_ManStop( pNew ); |
| Abc_Print(1, "Dumped modified AIG into file \"aig_with_clauses.aig\".\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) |
| { |
| FILE * pFile; |
| Vec_Int_t * vFlopCounts; |
| Vec_Ptr_t * vCubes; |
| Pdr_Set_t * pCube; |
| char ** pNamesCi; |
| int i, kStart, Count = 0; |
| // create file |
| pFile = fopen( pFileName, "w" ); |
| if ( pFile == NULL ) |
| { |
| Abc_Print( 1, "Cannot open file \"%s\" for writing invariant.\n", pFileName ); |
| return; |
| } |
| // collect cubes |
| kStart = Pdr_ManFindInvariantStart( p ); |
| if ( fProved ) |
| vCubes = Pdr_ManCollectCubes( p, kStart ); |
| else |
| vCubes = Vec_PtrDup( p->vInfCubes ); |
| Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare ); |
| // Pdr_ManDumpAig( p->pAig, vCubes ); |
| // count cubes |
| Count = 0; |
| Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) |
| { |
| if ( pCube->nRefs == -1 ) |
| continue; |
| Count++; |
| } |
| // collect variable appearances |
| vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; |
| // output the header |
| if ( fProved ) |
| fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName ); |
| else |
| fprintf( pFile, "# Clauses of the last timeframe for \"%s\"\n", p->pAig->pName ); |
| fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() ); |
| fprintf( pFile, ".i %d\n", p->pPars->fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) ); |
| fprintf( pFile, ".o 1\n" ); |
| fprintf( pFile, ".p %d\n", Count ); |
| // output flop names |
| pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 ); |
| if ( pNamesCi ) |
| { |
| fprintf( pFile, ".ilb" ); |
| for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) |
| if ( !p->pPars->fUseSupp || Vec_IntEntry( vFlopCounts, i ) ) |
| fprintf( pFile, " %s", pNamesCi[Saig_ManPiNum(p->pAig) + i] ); |
| fprintf( pFile, "\n" ); |
| ABC_FREE( pNamesCi ); |
| fprintf( pFile, ".ob inv\n" ); |
| } |
| // output cubes |
| Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) |
| { |
| if ( pCube->nRefs == -1 ) |
| continue; |
| Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); |
| fprintf( pFile, " 1\n" ); |
| } |
| fprintf( pFile, ".e\n\n" ); |
| fclose( pFile ); |
| Vec_IntFreeP( &vFlopCounts ); |
| Vec_PtrFree( vCubes ); |
| if ( fProved ) |
| Abc_Print( 1, "Inductive invariant was written into file \"%s\".\n", pFileName ); |
| else |
| Abc_Print( 1, "Clauses of the last timeframe were written into file \"%s\".\n", pFileName ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p ) |
| { |
| Vec_Str_t * vStr; |
| Vec_Int_t * vFlopCounts; |
| Vec_Ptr_t * vCubes; |
| Pdr_Set_t * pCube; |
| int i, kStart; |
| vStr = Vec_StrAlloc( 1000 ); |
| // collect cubes |
| kStart = Pdr_ManFindInvariantStart( p ); |
| if ( p->vInfCubes == NULL ) |
| vCubes = Pdr_ManCollectCubes( p, kStart ); |
| else |
| vCubes = Vec_PtrDup( p->vInfCubes ); |
| Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare ); |
| // collect variable appearances |
| vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; |
| // output cubes |
| Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) |
| { |
| if ( pCube->nRefs == -1 ) |
| continue; |
| Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); |
| } |
| Vec_IntFreeP( &vFlopCounts ); |
| Vec_PtrFree( vCubes ); |
| Vec_StrPush( vStr, '\0' ); |
| return vStr; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Pdr_ManReportInvariant( Pdr_Man_t * p ) |
| { |
| Vec_Ptr_t * vCubes; |
| int kStart = Pdr_ManFindInvariantStart( p ); |
| vCubes = Pdr_ManCollectCubes( p, kStart ); |
| Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (cex = %d, ave = %.2f)\n", |
| kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), p->nCexesTotal, 1.0*p->nXsimLits/p->nXsimRuns ); |
| // Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", |
| // kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) ); |
| Vec_PtrFree( vCubes ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Pdr_ManVerifyInvariant( Pdr_Man_t * p ) |
| { |
| sat_solver * pSat; |
| Vec_Int_t * vLits; |
| Vec_Ptr_t * vCubes; |
| Pdr_Set_t * pCube; |
| int i, kStart, kThis, RetValue, Counter = 0; |
| abctime clk = Abc_Clock(); |
| // collect cubes used in the inductive invariant |
| kStart = Pdr_ManFindInvariantStart( p ); |
| vCubes = Pdr_ManCollectCubes( p, kStart ); |
| // create solver with the cubes |
| kThis = Vec_PtrSize(p->vSolvers); |
| pSat = Pdr_ManCreateSolver( p, kThis ); |
| // add the property output |
| // Pdr_ManSetPropertyOutput( p, kThis ); |
| // add the clauses |
| Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) |
| { |
| vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); |
| assert( RetValue ); |
| sat_solver_compress( pSat ); |
| } |
| // check each clause |
| Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) |
| { |
| vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 ); |
| RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); |
| if ( RetValue != l_False ) |
| { |
| Abc_Print( 1, "Verification of clause %d failed.\n", i ); |
| Counter++; |
| } |
| } |
| if ( Counter ) |
| Abc_Print( 1, "Verification of %d clauses has failed.\n", Counter ); |
| else |
| { |
| Abc_Print( 1, "Verification of invariant with %d clauses was successful. ", Vec_PtrSize(vCubes) ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| } |
| // sat_solver_delete( pSat ); |
| Vec_PtrFree( vCubes ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) |
| { |
| sat_solver * pSat; |
| Vec_Int_t * vLits; |
| Pdr_Set_t * pCube; |
| int i, kThis, RetValue, fChanges = 0, Counter = 0; |
| // create solver with the cubes |
| kThis = Vec_PtrSize(p->vSolvers); |
| pSat = Pdr_ManCreateSolver( p, kThis ); |
| // add the clauses |
| Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) |
| { |
| if ( pCube->nRefs == -1 ) // skip non-inductive |
| continue; |
| vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); |
| assert( RetValue ); |
| sat_solver_compress( pSat ); |
| } |
| // check each clause |
| Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) |
| { |
| if ( pCube->nRefs == -1 ) // skip non-inductive |
| continue; |
| vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 ); |
| RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); |
| if ( RetValue != l_False ) // mark as non-inductive |
| { |
| pCube->nRefs = -1; |
| fChanges = 1; |
| } |
| else |
| Counter++; |
| } |
| //Abc_Print(1, "Clauses = %d.\n", Counter ); |
| //sat_solver_delete( pSat ); |
| return fChanges; |
| } |
| Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ) |
| { |
| Vec_Int_t * vResult; |
| Vec_Ptr_t * vCubes; |
| Pdr_Set_t * pCube; |
| int i, v, kStart; |
| // collect cubes used in the inductive invariant |
| kStart = Pdr_ManFindInvariantStart( p ); |
| vCubes = Pdr_ManCollectCubes( p, kStart ); |
| // refine as long as there are changes |
| if ( fReduce ) |
| while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) ); |
| // collect remaining clauses |
| vResult = Vec_IntAlloc( 1000 ); |
| Vec_IntPush( vResult, 0 ); |
| Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) |
| { |
| if ( pCube->nRefs == -1 ) // skip non-inductive |
| continue; |
| Vec_IntAddToEntry( vResult, 0, 1 ); |
| Vec_IntPush( vResult, pCube->nLits ); |
| for ( v = 0; v < pCube->nLits; v++ ) |
| Vec_IntPush( vResult, pCube->Lits[v] ); |
| } |
| //Vec_PtrFree( vCubes ); |
| Vec_PtrFreeP( &p->vInfCubes ); |
| p->vInfCubes = vCubes; |
| Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) ); |
| return vResult; |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Remove clauses while maintaining the invariant.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| #define Pdr_ForEachCube( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 ) |
| |
| Vec_Int_t * Pdr_InvMap( Vec_Int_t * vCounts ) |
| { |
| int i, k = 0, Count; |
| Vec_Int_t * vMap = Vec_IntStart( Vec_IntSize(vCounts) ); |
| Vec_IntForEachEntry( vCounts, Count, i ) |
| if ( Count ) |
| Vec_IntWriteEntry( vMap, i, k++ ); |
| return vMap; |
| } |
| Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv ) |
| { |
| int i, k, * pCube, * pList = Vec_IntArray(vInv); |
| Vec_Int_t * vCounts = Vec_IntStart( Vec_IntEntryLast(vInv) ); |
| Pdr_ForEachCube( pList, pCube, i ) |
| for ( k = 0; k < pCube[0]; k++ ) |
| Vec_IntAddToEntry( vCounts, Abc_Lit2Var(pCube[k+1]), 1 ); |
| return vCounts; |
| } |
| int Pdr_InvUsedFlopNum( Vec_Int_t * vInv ) |
| { |
| Vec_Int_t * vCounts = Pdr_InvCounts( vInv ); |
| int nZeros = Vec_IntCountZero( vCounts ); |
| Vec_IntFree( vCounts ); |
| return Vec_IntEntryLast(vInv) - nZeros; |
| } |
| |
| Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts ) |
| { |
| Vec_Str_t * vStr = Vec_StrAlloc( 1000 ); |
| Vec_Int_t * vMap = Pdr_InvMap( vCounts ); |
| int nVars = Vec_IntSize(vCounts) - Vec_IntCountZero(vCounts); |
| int i, k, * pCube, * pList = Vec_IntArray(vInv); |
| char * pBuffer = ABC_ALLOC( char, nVars ); |
| for ( i = 0; i < nVars; i++ ) |
| pBuffer[i] = '-'; |
| Pdr_ForEachCube( pList, pCube, i ) |
| { |
| for ( k = 0; k < pCube[0]; k++ ) |
| pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '0' + !Abc_LitIsCompl(pCube[k+1]); |
| for ( k = 0; k < nVars; k++ ) |
| Vec_StrPush( vStr, pBuffer[k] ); |
| Vec_StrPush( vStr, ' ' ); |
| Vec_StrPush( vStr, '1' ); |
| Vec_StrPush( vStr, '\n' ); |
| for ( k = 0; k < pCube[0]; k++ ) |
| pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '-'; |
| } |
| Vec_StrPush( vStr, '\0' ); |
| ABC_FREE( pBuffer ); |
| Vec_IntFree( vMap ); |
| return vStr; |
| } |
| void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose ) |
| { |
| Abc_Print(1, "Invariant contains %d clauses with %d literals and %d flops (out of %d).\n", Vec_IntEntry(vInv, 0), Vec_IntSize(vInv)-Vec_IntEntry(vInv, 0)-2, Pdr_InvUsedFlopNum(vInv), Vec_IntEntryLast(vInv) ); |
| if ( fVerbose ) |
| { |
| Vec_Int_t * vCounts = Pdr_InvCounts( vInv ); |
| Vec_Str_t * vStr = Pdr_InvPrintStr( vInv, vCounts ); |
| Abc_Print(1, "%s", Vec_StrArray( vStr ) ); |
| Vec_IntFree( vCounts ); |
| Vec_StrFree( vStr ); |
| } |
| } |
| |
| int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver * pSat, int fSkip ) |
| { |
| int nBTLimit = 0; |
| int fCheckProperty = 1; |
| int i, k, status, nFailed = 0, nFailedOuts = 0; |
| // collect cubes |
| int * pCube, * pList = Vec_IntArray(vInv); |
| // create variables |
| Vec_Int_t * vLits = Vec_IntAlloc(100); |
| int iFoVarBeg = sat_solver_nvars(pSat) - Gia_ManRegNum(p); |
| int iFiVarBeg = 1 + Gia_ManPoNum(p); |
| // add cubes |
| Pdr_ForEachCube( pList, pCube, i ) |
| { |
| // collect literals |
| Vec_IntClear( vLits ); |
| for ( k = 0; k < pCube[0]; k++ ) |
| if ( pCube[k+1] != -1 ) |
| Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) ); |
| if ( Vec_IntSize(vLits) == 0 ) |
| { |
| Vec_IntFree( vLits ); |
| return 1; |
| } |
| // add it to the solver |
| status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) ); |
| assert( status == 1 ); |
| } |
| // verify property output |
| if ( fCheckProperty ) |
| { |
| for ( i = 0; i < Gia_ManPoNum(p); i++ ) |
| { |
| Vec_IntFill( vLits, 1, Abc_Var2Lit(1+i, 0) ); |
| status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); |
| if ( status == l_Undef ) // timeout |
| break; |
| if ( status == l_True ) // sat - property fails |
| { |
| if ( fVerbose ) |
| Abc_Print(1, "Coverage check failed for output %d.\n", i ); |
| nFailedOuts++; |
| if ( fSkip ) |
| { |
| Vec_IntFree( vLits ); |
| return 1; |
| } |
| continue; |
| } |
| assert( status == l_False ); // unsat - property holds |
| } |
| } |
| // iterate through cubes in the direct order |
| Pdr_ForEachCube( pList, pCube, i ) |
| { |
| // collect cube |
| Vec_IntClear( vLits ); |
| for ( k = 0; k < pCube[0]; k++ ) |
| if ( pCube[k+1] != -1 ) |
| Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) ); |
| // check if this cube intersects with the complement of other cubes in the solver |
| // if it does not intersect, then it is redundant and can be skipped |
| status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); |
| if ( status != l_True && fVerbose ) |
| Abc_Print(1, "Finished checking clause %d (out of %d)...\r", i, pList[0] ); |
| if ( status == l_Undef ) // timeout |
| break; |
| if ( status == l_False ) // unsat -- correct |
| continue; |
| assert( status == l_True ); |
| if ( fVerbose ) |
| Abc_Print(1, "Inductiveness check failed for clause %d.\n", i ); |
| nFailed++; |
| if ( fSkip ) |
| { |
| Vec_IntFree( vLits ); |
| return 1; |
| } |
| } |
| Vec_IntFree( vLits ); |
| return nFailed + nFailedOuts; |
| } |
| |
| int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) |
| { |
| int RetValue; |
| Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); |
| sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| assert( sat_solver_nvars(pSat) == pCnf->nVars ); |
| Cnf_DataFree( pCnf ); |
| RetValue = Pdr_InvCheck_int( p, vInv, fVerbose, pSat, 0 ); |
| sat_solver_delete( pSat ); |
| return RetValue; |
| } |
| |
| Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) |
| { |
| int nBTLimit = 0; |
| int fCheckProperty = 1; |
| abctime clk = Abc_Clock(); |
| int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0; |
| Vec_Int_t * vRes = NULL; |
| // create SAT solver |
| Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); |
| sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0]; |
| // create variables |
| Vec_Int_t * vLits = Vec_IntAlloc(100); |
| Vec_Bit_t * vRemoved = Vec_BitStart( nCubes ); |
| int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p); |
| int iFiVarBeg = 1 + Gia_ManPoNum(p); |
| int iAuxVarBeg = sat_solver_nvars(pSat); |
| // allocate auxiliary variables |
| assert( sat_solver_nvars(pSat) == pCnf->nVars ); |
| sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + nCubes ); |
| // add clauses |
| Pdr_ForEachCube( pList, pCube, i ) |
| { |
| // collect literals |
| Vec_IntFill( vLits, 1, Abc_Var2Lit(iAuxVarBeg + i, 1) ); // neg aux literal |
| for ( k = 0; k < pCube[0]; k++ ) |
| Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) ); |
| // add it to the solver |
| status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) ); |
| assert( status == 1 ); |
| } |
| // iterate through clauses |
| Pdr_ForEachCube( pList, pCube, i ) |
| { |
| if ( Vec_BitEntry(vRemoved, i) ) |
| continue; |
| // collect aux literals for remaining clauses |
| Vec_IntClear( vLits ); |
| for ( k = 0; k < nCubes; k++ ) |
| if ( k != i && !Vec_BitEntry(vRemoved, k) ) // skip this cube and already removed cubes |
| Vec_IntPush( vLits, Abc_Var2Lit(iAuxVarBeg + k, 0) ); // pos aux literal |
| nLits = Vec_IntSize( vLits ); |
| // check if the property still holds |
| if ( fCheckProperty ) |
| { |
| for ( k = 0; k < Gia_ManPoNum(p); k++ ) |
| { |
| Vec_IntShrink( vLits, nLits ); |
| Vec_IntPush( vLits, Abc_Var2Lit(1+k, 0) ); |
| status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); |
| if ( status == l_Undef ) // timeout |
| { |
| fFailed = 1; |
| break; |
| } |
| if ( status == l_True ) // sat - property fails |
| break; |
| assert( status == l_False ); // unsat - property holds |
| } |
| if ( fFailed ) |
| break; |
| if ( k < Gia_ManPoNum(p) ) |
| continue; |
| } |
| // check other clauses |
| fCannot = 0; |
| Pdr_ForEachCube( pList, pCube, n ) |
| { |
| if ( Vec_BitEntry(vRemoved, n) || n == i ) |
| continue; |
| // collect cube |
| Vec_IntShrink( vLits, nLits ); |
| for ( k = 0; k < pCube[0]; k++ ) |
| Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) ); |
| // check if this cube intersects with the complement of other cubes in the solver |
| // if it does not intersect, then it is redundant and can be skipped |
| status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); |
| if ( status == l_Undef ) // timeout |
| { |
| fFailed = 1; |
| break; |
| } |
| if ( status == l_False ) // unsat -- correct |
| continue; |
| assert( status == l_True ); |
| // cannot remove |
| fCannot = 1; |
| break; |
| } |
| if ( fFailed ) |
| break; |
| if ( fCannot ) |
| continue; |
| if ( fVerbose ) |
| Abc_Print(1, "Removing clause %d.\n", i ); |
| Vec_BitWriteEntry( vRemoved, i, 1 ); |
| nRemoved++; |
| } |
| if ( nRemoved ) |
| Abc_Print(1, "Invariant minimization reduced %d clauses (out of %d). ", nRemoved, nCubes ); |
| else |
| Abc_Print(1, "Invariant minimization did not change the invariant. " ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| // cleanup cover |
| if ( !fFailed && nRemoved > 0 ) // finished without timeout and removed some cubes |
| { |
| vRes = Vec_IntAlloc( 1000 ); |
| Vec_IntPush( vRes, nCubes-nRemoved ); |
| Pdr_ForEachCube( pList, pCube, i ) |
| if ( !Vec_BitEntry(vRemoved, i) ) |
| for ( k = 0; k <= pCube[0]; k++ ) |
| Vec_IntPush( vRes, pCube[k] ); |
| Vec_IntPush( vRes, Vec_IntEntryLast(vInv) ); |
| } |
| Cnf_DataFree( pCnf ); |
| sat_solver_delete( pSat ); |
| Vec_BitFree( vRemoved ); |
| Vec_IntFree( vLits ); |
| return vRes; |
| } |
| |
| Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) |
| { |
| Vec_Int_t * vRes = NULL; |
| abctime clk = Abc_Clock(); |
| int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 0; |
| Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); |
| sat_solver * pSat; |
| // sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| Pdr_ForEachCube( pList, pCube, i ) |
| { |
| nLits += pCube[0]; |
| for ( k = 0; k < pCube[0]; k++ ) |
| { |
| int Save = pCube[k+1]; |
| pCube[k+1] = -1; |
| //sat_solver_bookmark( pSat ); |
| pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| if ( Pdr_InvCheck_int(p, vInv, 0, pSat, 1) ) |
| pCube[k+1] = Save; |
| else |
| { |
| if ( fVerbose ) |
| Abc_Print(1, "Removing lit %d from clause %d.\n", k, i ); |
| nRemoved++; |
| } |
| sat_solver_delete( pSat ); |
| //sat_solver_rollback( pSat ); |
| //sat_solver_bookmark( pSat ); |
| } |
| } |
| Cnf_DataFree( pCnf ); |
| //sat_solver_delete( pSat ); |
| if ( nRemoved ) |
| Abc_Print(1, "Invariant minimization reduced %d literals (out of %d). ", nRemoved, nLits ); |
| else |
| Abc_Print(1, "Invariant minimization did not change the invariant. " ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| if ( nRemoved > 0 ) // finished without timeout and removed some lits |
| { |
| vRes = Vec_IntAlloc( 1000 ); |
| Vec_IntPush( vRes, pList[0] ); |
| Pdr_ForEachCube( pList, pCube, i ) |
| { |
| int nLits = 0; |
| for ( k = 0; k < pCube[0]; k++ ) |
| if ( pCube[k+1] != -1 ) |
| nLits++; |
| Vec_IntPush( vRes, nLits ); |
| for ( k = 0; k < pCube[0]; k++ ) |
| if ( pCube[k+1] != -1 ) |
| Vec_IntPush( vRes, pCube[k+1] ); |
| } |
| Vec_IntPush( vRes, Vec_IntEntryLast(vInv) ); |
| } |
| return vRes; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
