diff options
Diffstat (limited to 'src/aig/fra')
-rw-r--r-- | src/aig/fra/fra.h | 42 | ||||
-rw-r--r-- | src/aig/fra/fraBmc.c | 11 | ||||
-rw-r--r-- | src/aig/fra/fraCec.c | 16 | ||||
-rw-r--r-- | src/aig/fra/fraClass.c | 45 | ||||
-rw-r--r-- | src/aig/fra/fraClau.c | 11 | ||||
-rw-r--r-- | src/aig/fra/fraClaus.c | 21 | ||||
-rw-r--r-- | src/aig/fra/fraCnf.c | 15 | ||||
-rw-r--r-- | src/aig/fra/fraCore.c | 9 | ||||
-rw-r--r-- | src/aig/fra/fraHot.c | 23 | ||||
-rw-r--r-- | src/aig/fra/fraImp.c | 25 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 19 | ||||
-rw-r--r-- | src/aig/fra/fraIndVer.c | 9 | ||||
-rw-r--r-- | src/aig/fra/fraLcr.c | 51 | ||||
-rw-r--r-- | src/aig/fra/fraMan.c | 5 | ||||
-rw-r--r-- | src/aig/fra/fraPart.c | 23 | ||||
-rw-r--r-- | src/aig/fra/fraSat.c | 7 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 35 | ||||
-rw-r--r-- | src/aig/fra/fraSim.c | 69 | ||||
-rw-r--r-- | src/aig/fra/fra_.c | 5 |
19 files changed, 284 insertions, 157 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index f661d2e5..b046cc47 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -21,6 +21,7 @@ #ifndef __FRA_H__ #define __FRA_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -41,9 +42,10 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif + + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -55,7 +57,6 @@ typedef struct Fra_Sec_t_ Fra_Sec_t; typedef struct Fra_Man_t_ Fra_Man_t; typedef struct Fra_Cla_t_ Fra_Cla_t; typedef struct Fra_Sml_t_ Fra_Sml_t; -typedef struct Fra_Cex_t_ Fra_Cex_t; typedef struct Fra_Bmc_t_ Fra_Bmc_t; // FRAIG parameters @@ -180,17 +181,6 @@ struct Fra_Sml_t_ unsigned pData[0]; // simulation data for the nodes }; -// simulation manager -struct Fra_Cex_t_ -{ - int iPo; // the zero-based number of PO, for which verification failed - int iFrame; // the zero-based number of the time-frame, for which verificaiton failed - int nRegs; // the number of registers in the miter - int nPis; // the number of primary inputs in the miter - int nBits; // the number of words of bit data used - unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis) -}; - // FRAIG manager struct Fra_Man_t_ { @@ -382,16 +372,18 @@ extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrame extern void Fra_SmlStop( Fra_Sml_t * p ); extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter ); extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); -extern Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ); -extern Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); -extern void Fra_SmlFreeCounterExample( Fra_Cex_t * p ); -extern Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ); -extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p ); -extern int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p ); - -#ifdef __cplusplus -} -#endif +extern Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ); +extern Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); +extern void Fra_SmlFreeCounterExample( Abc_Cex_t * p ); +extern Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ); +extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ); +extern int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p ); +extern Abc_Cex_t * Fra_SmlSimpleCounterExample( Aig_Man_t * pAig, int * pModel, int iFrame, int iPo ); + + +ABC_NAMESPACE_HEADER_END + + #endif diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c index 7b08d74d..ae9e4bc5 100644 --- a/src/aig/fra/fraBmc.c +++ b/src/aig/fra/fraBmc.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -68,7 +71,7 @@ static inline Aig_Obj_t * Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { asse ***********************************************************************/ int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) { - Fra_Man_t * p = pObj0->pData; + Fra_Man_t * p = (Fra_Man_t *)pObj0->pData; Aig_Obj_t * pObjFrames0, * pObjFrames1; Aig_Obj_t * pObjFraig0, * pObjFraig1; int i; @@ -99,7 +102,7 @@ int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) ***********************************************************************/ int Fra_BmcNodeIsConst( Aig_Obj_t * pObj ) { - Fra_Man_t * p = pObj->pData; + Fra_Man_t * p = (Fra_Man_t *)pObj->pData; return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) ); } @@ -421,7 +424,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFraig ); if ( pBmc->pAigFraig->pData ) { - pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, pBmc->pAigFraig->pData ); + pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, (int *)pBmc->pAigFraig->pData ); ABC_FREE( pBmc->pAigFraig->pData ); } else if ( iOutput >= 0 ) @@ -444,3 +447,5 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index b7a78050..037e6c70 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -21,6 +21,9 @@ #include "fra.h" #include "cnf.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -58,7 +61,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi Cnf_DataTranformPolarity( pCnf, 0 ); // convert into SAT solver - pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); if ( pSat == NULL ) { Cnf_DataFree( pCnf ); @@ -128,8 +131,9 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi } else assert( 0 ); -// ABC_PRT( "SAT sat_solver time", clock() - clk ); -// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts ); + +// Abc_Print( 1, "The number of conflicts = %6d. ", (int)pSat->stats.conflicts ); +// Abc_PrintTime( 1, "Solving time", clock() - clk ); // if the problem is SAT, get the counterexample if ( status == l_True ) @@ -283,7 +287,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart ); // solve the partitions nOutputs = -1; - Vec_PtrForEachEntry( vParts, pAig, i ) + Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i ) { nOutputs++; if ( fVerbose ) @@ -319,7 +323,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi fflush( stdout ); } // free intermediate results - Vec_PtrForEachEntry( vParts, pAig, i ) + Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i ) Aig_ManStop( pAig ); Vec_PtrFree( vParts ); return RetValue; @@ -395,3 +399,5 @@ ABC_PRT( "Time", clock() - clkTotal ); //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 94cac80a..9b1ad3f2 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + /* The candidate equivalence classes are stored as a vector of pointers to the array of pointers to the nodes in each class. @@ -124,7 +127,7 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ) } } if ( vFailed ) - Vec_PtrForEachEntry( vFailed, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vFailed, pObj, i ) p->pAig->pReprs[pObj->Id] = NULL; } @@ -163,7 +166,7 @@ int Fra_ClassesCountLits( Fra_Cla_t * p ) Aig_Obj_t ** pClass; int i, nNodes, nLits = 0; nLits = Vec_PtrSize( p->vClasses1 ); - Vec_PtrForEachEntry( p->vClasses, pClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i ) { nNodes = Fra_ClassCount( pClass ); assert( nNodes > 1 ); @@ -187,7 +190,7 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p ) { Aig_Obj_t ** pClass; int i, nNodes, nPairs = 0; - Vec_PtrForEachEntry( p->vClasses, pClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i ) { nNodes = Fra_ClassCount( pClass ); assert( nNodes > 1 ); @@ -244,13 +247,13 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ) if ( fVeryVerbose ) { - Vec_PtrForEachEntry( p->vClasses1, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i ) assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) ); printf( "Constants { " ); - Vec_PtrForEachEntry( p->vClasses1, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i ) printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) ); printf( "}\n" ); - Vec_PtrForEachEntry( p->vClasses, pClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i ) { printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) ); Fra_PrintClass( p, pClass ); @@ -415,15 +418,15 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass ) Vec_PtrPush( p->vClassNew, pObj ); /* printf( "Refining class (" ); - Vec_PtrForEachEntry( p->vClassOld, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i ) printf( "%d,", pObj->Id ); printf( ") + (" ); - Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) printf( "%d,", pObj->Id ); printf( ")\n" ); */ // put the nodes back into the class memory - Vec_PtrForEachEntry( p->vClassOld, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i ) { ppClass[i] = pObj; ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL; @@ -431,7 +434,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass ) } ppClass += 2*Vec_PtrSize(p->vClassOld); // put the new nodes into the class memory - Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) { ppClass[i] = pObj; ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; @@ -455,7 +458,7 @@ int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses ) { Aig_Obj_t ** pClass, ** pClass2; int nRefis; - pClass = Vec_PtrEntryLast( vClasses ); + pClass = (Aig_Obj_t **)Vec_PtrEntryLast( vClasses ); for ( nRefis = 0; (pClass2 = Fra_RefineClassOne( p, pClass )); nRefis++ ) { // if the original class is trivial, remove it @@ -495,7 +498,7 @@ int Fra_ClassesRefine( Fra_Cla_t * p ) // refine the classes nRefis = 0; Vec_PtrClear( p->vClassesTemp ); - Vec_PtrForEachEntry( p->vClasses, pClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i ) { // add the class to the new array assert( pClass[0] != NULL ); @@ -533,7 +536,7 @@ int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped ) // collect all the nodes to be refined k = 0; Vec_PtrClear( p->vClassNew ); - Vec_PtrForEachEntry( p->vClasses1, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i ) { if ( p->pFuncNodeIsConst( pObj ) ) Vec_PtrWriteEntry( p->vClasses1, k++, pObj ); @@ -545,19 +548,19 @@ int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped ) return 0; /* printf( "Refined const-1 class: {" ); - Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) printf( " %d", pObj->Id ); printf( " }\n" ); */ if ( Vec_PtrSize(p->vClassNew) == 1 ) { - Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL ); + Fra_ClassObjSetRepr( (Aig_Obj_t *)Vec_PtrEntry(p->vClassNew,0), NULL ); return 1; } // create a new class composed of these nodes ppClass = p->pMemClassesFree; p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew); - Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i ) { ppClass[i] = pObj; ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; @@ -658,7 +661,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) printf( "Before: Const = %6d. Class = %6d. ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) ); // remove nodes from classes whose weight is less than WeightMax/Ratio k = 0; - Vec_PtrForEachEntry( p->vClasses1, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i ) { if ( pWeights[pObj->Id] >= WeightMax/Ratio ) Vec_PtrWriteEntry( p->vClasses1, k++, pObj ); @@ -667,7 +670,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) } Vec_PtrShrink( p->vClasses1, k ); // in each class, compact the nodes - Vec_PtrForEachEntry( p->vClasses, ppClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i ) { k = 1; for ( c = 1; ppClass[c]; c++ ) @@ -681,7 +684,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) } // remove classes with only repr k = 0; - Vec_PtrForEachEntry( p->vClasses, ppClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i ) if ( ppClass[1] != NULL ) Vec_PtrWriteEntry( p->vClasses, k++, ppClass ); Vec_PtrShrink( p->vClasses, k ); @@ -705,7 +708,7 @@ void Fra_ClassesSelectRepr( Fra_Cla_t * p ) Aig_Obj_t ** pClass, * pNodeMin; int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur; // reassign representatives in each class - Vec_PtrForEachEntry( p->vClasses, pClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i ) { // collect support sizes and find the min-support node cMinSupp = -1; @@ -855,3 +858,5 @@ printf( "Assert miters = %6d. Output miters = %6d.\n", //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraClau.c b/src/aig/fra/fraClau.c index 96d06380..490c73ff 100644 --- a/src/aig/fra/fraClau.c +++ b/src/aig/fra/fraClau.c @@ -22,6 +22,9 @@ #include "cnf.h" #include "satSolver.h" +ABC_NAMESPACE_IMPL_START + + /* This code is inspired by the paper: Aaron Bradley and Zohar Manna, "Checking safety by inductive generalization of counterexamples to @@ -233,7 +236,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 ); //Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 ); - p->pSatMain = Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 ); + p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 ); /* { int i; @@ -248,7 +251,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL ); assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) ); pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) ); - p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 ); + p->pSatTest = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 ); p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest ); // derive one timeframe to be checked for BMC @@ -256,7 +259,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) //Aig_ManShow( pFramesBmc, 0, NULL ); assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) ); pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) ); - p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 ); + p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 ); // create variable sets p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) ); @@ -756,3 +759,5 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c index e5fe3f40..90659333 100644 --- a/src/aig/fra/fraClaus.c +++ b/src/aig/fra/fraClaus.c @@ -22,6 +22,9 @@ #include "cnf.h" #include "satSolver.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -818,7 +821,7 @@ clk = clock(); int * pStart; // reset the solver if ( p->pSatMain ) sat_solver_delete( p->pSatMain ); - p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); + p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); if ( p->pSatMain == NULL ) { printf( "Error: Main solver is unsat.\n" ); @@ -1030,8 +1033,8 @@ void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel ) { if ( pModel[i] == l_True ) { - assert( Aig_InfoHasBit( Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 ); - Aig_InfoSetBit( Vec_PtrEntry(p->vCexes, i), p->nCexes ); + assert( Aig_InfoHasBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 ); + Aig_InfoSetBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes ); } } p->nCexes++; @@ -1056,7 +1059,7 @@ int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits ) { iVar = lit_var(pLits[i]) - p->nFrames * p->pCnf->nVars; assert( iVar > 0 && iVar < p->pCnf->nVars ); - pSims[i] = Vec_PtrEntry( p->vCexes, iVar ); + pSims[i] = (unsigned *)Vec_PtrEntry( p->vCexes, iVar ); } nWords = p->nCexes / 32; for ( w = 0; w < nWords; w++ ) @@ -1098,7 +1101,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p ) // reset the solver if ( p->pSatMain ) sat_solver_delete( p->pSatMain ); - p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 ); + p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 ); if ( p->pSatMain == NULL ) { printf( "Error: Main solver is unsat.\n" ); @@ -1516,7 +1519,7 @@ Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit ) Aig_Obj_t * pLiteral; int NodeId = pVar2Id[ lit_var(Lit) ]; assert( NodeId >= 0 ); - pLiteral = Aig_ManObj( p->pAig, NodeId )->pData; + pLiteral = (Aig_Obj_t *)Aig_ManObj( p->pAig, NodeId )->pData; return Aig_NotCond( pLiteral, lit_sign(Lit) ); } @@ -1705,7 +1708,7 @@ if ( fVerbose ) // check BMC clk = clock(); - p->pSatBmc = Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 ); + p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 ); if ( p->pSatBmc == NULL ) { printf( "Error: BMC solver is unsat.\n" ); @@ -1725,7 +1728,7 @@ if ( fVerbose ) // start the SAT solver clk = clock(); - p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 ); + p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 ); if ( p->pSatMain == NULL ) { printf( "Error: Main solver is unsat.\n" ); @@ -1867,3 +1870,5 @@ clk = clock(); //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c index 27da3fc5..5021e750 100644 --- a/src/aig/fra/fraCnf.c +++ b/src/aig/fra/fraCnf.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -134,7 +137,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) pLits = ABC_ALLOC( int, nLits ); // suppose AND-gate is A & B = C // add !A => !C or A + !C - Vec_PtrForEachEntry( vSuper, pFanin, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) { pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1); @@ -142,7 +145,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) assert( RetValue ); } // add A & B => C or !A + !B + C - Vec_PtrForEachEntry( vSuper, pFanin, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); @@ -246,7 +249,7 @@ void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier ); if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier ); // explore nodes in the frontier - Vec_PtrForEachEntry( vFrontier, pNode, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i ) { // create the supergate assert( Fra_ObjSatNum(pNode) ); @@ -258,14 +261,14 @@ void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) ); Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) ); Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) ); - Vec_PtrForEachEntry( vFanins, pFanin, k ) + Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k ) Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); Fra_AddClausesMux( p, pNode ); } else { vFanins = Fra_CollectSuper( pNode, fUseMuxes ); - Vec_PtrForEachEntry( vFanins, pFanin, k ) + Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k ) Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); Fra_AddClausesSuper( p, pNode, vFanins ); } @@ -282,3 +285,5 @@ void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index fad8c7bf..93c16e1e 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -198,12 +201,12 @@ void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex ) Aig_ManForEachPo( p->pManAig, pObj, i ) pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); // check if the classes hold - Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i ) { if ( pObj->fPhase != pObj->fMarkB ) printf( "The node %d is not constant under cex!\n", pObj->Id ); } - Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i ) { for ( c = 1; ppClass[c]; c++ ) if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) ) @@ -483,3 +486,5 @@ Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c index c4472121..29c9c33d 100644 --- a/src/aig/fra/fraHot.c +++ b/src/aig/fra/fraHot.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -143,8 +146,8 @@ Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim ) continue; assert( i-nTruePis >= 0 ); // Aig_ManForEachLoSeq( pSim->pAig, pObj2, k ) -// Vec_PtrForEachEntryStart( pSim->pAig->vPis, pObj2, k, Aig_ManPiNum(p)-Aig_ManRegNum(p) ) - Vec_PtrForEachEntryStart( pSim->pAig->vPis, pObj2, k, i+1 ) +// Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManPiNum(p)-Aig_ManRegNum(p) ) + Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, i+1 ) { if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) ) continue; @@ -201,7 +204,7 @@ void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots ) pObj2 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out2) ); pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) ); pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) ); - // add contraint to solver + // add constraint to solver if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) ) { printf( "Fra_OneHotAssume(): Adding clause makes SAT solver unsat.\n" ); @@ -337,11 +340,11 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots ) Aig_ManRandom(1); for ( i = 0; i < nRegs; i++ ) { - pSim1 = Vec_PtrEntry( vSimInfo, i ); + pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, i ); for ( w = 0; w < nSimWords; w++ ) pSim1[w] = Fra_ObjRandomSim(); } - pSimTot = Vec_PtrEntry( vSimInfo, nRegs ); + pSimTot = (unsigned *)Vec_PtrEntry( vSimInfo, nRegs ); // collect simulation info memset( pSimTot, 0, sizeof(unsigned) * nSimWords ); @@ -355,8 +358,8 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots ) //Fra_LitSign(Out1)? '-': '+', Fra_LitReg(Out1), //Fra_LitSign(Out2)? '-': '+', Fra_LitReg(Out2) ); Counter++; - pSim1 = Vec_PtrEntry( vSimInfo, Fra_LitReg(Out1) ); - pSim2 = Vec_PtrEntry( vSimInfo, Fra_LitReg(Out2) ); + pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out1) ); + pSim2 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out2) ); if ( Fra_LitSign(Out1) && Fra_LitSign(Out2) ) for ( w = 0; w < nSimWords; w++ ) pSimTot[w] |= pSim1[w] & pSim2[w]; @@ -442,7 +445,7 @@ void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots ) // these constrants should be added to different timeframes! // (also note that PIs follow first - then registers) // - Vec_PtrForEachEntry( vOnehots, vGroup, k ) + Vec_PtrForEachEntry( Vec_Int_t *, vOnehots, vGroup, k ) { Vec_IntForEachEntry( vGroup, Out1, i ) Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 ) @@ -451,7 +454,7 @@ void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots ) pObj2 = Aig_ManPi( p->pManFraig, Out2 ); pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 ); pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 ); - // add contraint to solver + // add constraint to solver if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) ) { printf( "Fra_OneHotAddKnownConstraint(): Adding clause makes SAT solver unsat.\n" ); @@ -469,3 +472,5 @@ void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c index 716e83d5..34fa87e5 100644 --- a/src/aig/fra/fraImp.c +++ b/src/aig/fra/fraImp.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -211,12 +214,12 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr ) // skip nodes participating in the classes // if ( Fra_ClassObjRepr(pObj) ) // continue; - pMemory = Vec_PtrEntry( vNodes, pnBits[i] ); + pMemory = (int *)Vec_PtrEntry( vNodes, pnBits[i] ); pMemory[ pnNodes[pnBits[i]]++ ] = i; } // add 0s in the end nTotal = 0; - Vec_PtrForEachEntry( vNodes, pMemory, i ) + Vec_PtrForEachEntry( int *, vNodes, pMemory, i ) { pMemory[ pnNodes[i]++ ] = 0; nTotal += pnNodes[i]; @@ -335,8 +338,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in // count the total number of implications for ( k = nSimWords * 32; k > 0; k-- ) for ( i = k - 1; i > 0; i-- ) - for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ ) - for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ ) + for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ ) + for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ ) nImpsTotal++; // compute implications and their costs @@ -347,8 +350,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in { // HERE WE ARE MISSING SOME POTENTIAL IMPLICATIONS (with complement!) - for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ ) - for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ ) + for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ ) + for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ ) { nImpsTried++; if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) ) @@ -444,7 +447,7 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums ) Vec_IntWriteEntry( vImps, i, 0 ); break; } - } + } if ( f < p->pPars->nFramesK ) continue; // add constraints in each timeframe @@ -465,7 +468,7 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums ) // L => R L' v R (complement = L & R') pLits[0] = 2 * Left + !fComplL; pLits[1] = 2 * Right + fComplR; - // add contraint to solver + // add constraint to solver if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) ) { sat_solver_delete( pSat ); @@ -712,8 +715,8 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ) pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) ); // record the implication: L' + R pMiter = Aig_Or( pNew, - Aig_NotCond(pLeft->pData, !pLeft->fPhase), - Aig_NotCond(pRight->pData, pRight->fPhase) ); + Aig_NotCond((Aig_Obj_t *)pLeft->pData, !pLeft->fPhase), + Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); Aig_ObjCreatePo( pNew, pMiter ); } pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld; @@ -724,3 +727,5 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 84b739a4..2f2d8f2d 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -21,6 +21,10 @@ #include "fra.h" #include "cnf.h" #include "dar.h" +#include "saig.h" + +ABC_NAMESPACE_IMPL_START + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -265,7 +269,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) { // divide large clock domains into separate partitions vResult = Vec_PtrAlloc( 100 ); - Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i ) + Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i ) { if ( nPartSize && Vec_IntSize(vPart) > nPartSize ) Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize ); @@ -281,7 +285,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) { // print partitions printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) ); - Vec_PtrForEachEntry( vResult, vPart, i ) + Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i ) { sprintf( Buffer, "part%03d.aig", i ); pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL ); @@ -294,7 +298,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) // perform SSW with partitions Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); - Vec_PtrForEachEntry( vResult, vPart, i ) + Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i ) { pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack ); // create the projection of 1-hot registers @@ -498,7 +502,7 @@ p->timeTrav += clock() - clk2; // Cnf_DataTranformPolarity( pCnf, 0 ); //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); - p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); p->nSatVars = pCnf->nVars; assert( p->pSat != NULL ); if ( p->pSat == NULL ) @@ -523,7 +527,7 @@ p->timeTrav += clock() - clk2; if ( pCnf->pVarNums[pObj->Id] == -1 ) continue; Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); - Fra_ObjSetFaninVec( pObj, (void *)1 ); + Fra_ObjSetFaninVec( pObj, (Vec_Ptr_t *)1 ); } Cnf_DataFree( pCnf ); @@ -653,7 +657,6 @@ finish: ***********************************************************************/ int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams ) { - extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); FILE * pFile; char * pFilePairs; Aig_Man_t * pMan, * pNew; @@ -678,7 +681,7 @@ int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams ) Aig_ManPrintStats( pNew ); } Aig_ManStop( pNew ); - pNum2Id = pMan->pData; + pNum2Id = (int *)pMan->pData; // write the output file pFilePairs = Aig_FileNameGenericAppend( pFileName, ".pairs" ); pFile = fopen( pFilePairs, "w" ); @@ -702,3 +705,5 @@ int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraIndVer.c b/src/aig/fra/fraIndVer.c index 71faa346..32069cfb 100644 --- a/src/aig/fra/fraIndVer.c +++ b/src/aig/fra/fraIndVer.c @@ -21,6 +21,9 @@ #include "fra.h" #include "cnf.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -72,7 +75,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve } */ // derive initialized frames for the base case - pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 1 ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 1 ); // check clauses in the base case Beg = 0; pStart = Vec_IntArray( vLits ); @@ -93,7 +96,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve sat_solver_delete( pSat ); // derive initialized frames for the base case - pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames + 1, 0 ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames + 1, 0 ); assert( pSat->size == 2 * pCnf->nVars ); // add clauses to the first frame Beg = 0; @@ -159,3 +162,5 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index 16912f46..b18a8fcd 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -197,7 +200,7 @@ void Fra_LcrAigPrepareTwo( Aig_Man_t * pAig, Fra_Man_t * p ) ***********************************************************************/ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) { - Fra_Man_t * pTemp = pObj0->pData; + Fra_Man_t * pTemp = (Fra_Man_t *)pObj0->pData; Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc; Aig_Man_t * pFraig; Aig_Obj_t * pOut0, * pOut1; @@ -215,7 +218,7 @@ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) return 1; } assert( nPart0 == nPart1 ); - pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart0 ); + pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart0 ); // get the fraig outputs pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj0->pNext] ); pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj1->pNext] ); @@ -235,7 +238,7 @@ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) ***********************************************************************/ int Fra_LcrNodeIsConst( Aig_Obj_t * pObj ) { - Fra_Man_t * pTemp = pObj->pData; + Fra_Man_t * pTemp = (Fra_Man_t *)pObj->pData; Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc; Aig_Man_t * pFraig; Aig_Obj_t * pOut; @@ -243,7 +246,7 @@ int Fra_LcrNodeIsConst( Aig_Obj_t * pObj ) assert( Aig_ObjIsPi(pObj) ); // find the partition to which these nodes belong nPart = pLcr->pInToOutPart[(long)pObj->pNext]; - pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart ); + pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart ); // get the fraig outputs pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj->pNext] ); return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig); @@ -264,14 +267,14 @@ Aig_Obj_t * Fra_LcrManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj { Aig_Obj_t * pObjNew; if ( pObj->pData ) - return pObj->pData; + return (Aig_Obj_t *)pObj->pData; Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin0(pObj) ); if ( Aig_ObjIsBuf(pObj) ) - return pObj->pData = Aig_ObjChild0Copy(pObj); + return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj)); Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin1(pObj) ); pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) ); Aig_Regular(pObjNew)->pHaig = pObj->pHaig; - return pObj->pData = pObjNew; + return (Aig_Obj_t *)(pObj->pData = pObjNew); } /**Function************************************************************* @@ -308,7 +311,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr ) Aig_ManCleanData( pLcr->pAig ); pNew = Aig_ManStartFrom( pLcr->pAig ); // go over the equivalence classes - Vec_PtrForEachEntry( pLcr->pCla->vClasses, ppClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, pLcr->pCla->vClasses, ppClass, i ) { pMiter = Aig_ManConst0(pNew); for ( c = 0; ppClass[c]; c++ ) @@ -321,7 +324,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr ) Aig_ObjCreatePo( pNew, pMiter ); } // go over the constant candidates - Vec_PtrForEachEntry( pLcr->pCla->vClasses1, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, pLcr->pCla->vClasses1, pObj, i ) { assert( Aig_ObjIsPi(pObj) ); pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)pObj->pNext ); @@ -349,14 +352,14 @@ void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOu int Out, Offset, i, k, c; // compute the LO/LI offset Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig); - Vec_PtrForEachEntry( vParts, vOne, i ) + Vec_PtrForEachEntry( Vec_Int_t *, vParts, vOne, i ) { vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) ); Vec_IntForEachEntry( vOne, Out, k ) { if ( Out < Vec_PtrSize(pCla->vClasses) ) { - ppClass = Vec_PtrEntry( pCla->vClasses, Out ); + ppClass = (Aig_Obj_t **)Vec_PtrEntry( pCla->vClasses, Out ); for ( c = 0; ppClass[c]; c++ ) { pInToOutPart[(long)ppClass[c]->pNext] = i; @@ -366,7 +369,7 @@ void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOu } else { - pObjPi = Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) ); + pObjPi = (Aig_Obj_t *)Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) ); pInToOutPart[(long)pObjPi->pNext] = i; pInToOutNum[(long)pObjPi->pNext] = Vec_IntSize(vOneNew); Vec_IntPush( vOneNew, Offset+(long)pObjPi->pNext ); @@ -393,7 +396,7 @@ Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t { assert( !Aig_IsComplement(pObj) ); if ( Aig_ObjIsTravIdCurrent(p, pObj) ) - return pObj->pData; + return (Aig_Obj_t *)pObj->pData; Aig_ObjSetTravIdCurrent(p, pObj); if ( Aig_ObjIsPi(pObj) ) { @@ -404,13 +407,13 @@ Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t else { pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr ); - pObj->pData = Aig_NotCond( pObj->pData, pRepr->fPhase ^ pObj->fPhase ); + pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, pRepr->fPhase ^ pObj->fPhase ); } - return pObj->pData; + return (Aig_Obj_t *)pObj->pData; } Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin0(pObj) ); Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin1(pObj) ); - return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) )); } /**Function************************************************************* @@ -467,12 +470,12 @@ void Fra_ClassNodesMark( Fra_Lcr_t * p ) // compute the LO/LI offset Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig); // mark the nodes remaining in the classes - Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i ) { pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)pObj->pNext ); pObj->fMarkA = 1; } - Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i ) { for ( c = 0; ppClass[c]; c++ ) { @@ -500,12 +503,12 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p ) // compute the LO/LI offset Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig); // mark the nodes remaining in the classes - Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i ) { pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)pObj->pNext ); pObj->fMarkA = 0; } - Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i ) + Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i ) { for ( c = 0; ppClass[c]; c++ ) { @@ -610,12 +613,12 @@ p->timePart += clock() - clk2; // derive AIGs for each partition Fra_ClassNodesMark( p ); Vec_PtrClear( p->vFraigs ); - Vec_PtrForEachEntry( p->vParts, vPart, i ) + Vec_PtrForEachEntry( Vec_Int_t *, p->vParts, vPart, i ) { int clk3 = clock(); if ( TimeLimit != 0.0 && clock() > TimeToStop ) { - Vec_PtrForEachEntry( p->vFraigs, pAigPart, i ) + Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i ) Aig_ManStop( pAigPart ); Aig_ManCleanMarkA( pAig ); Aig_ManCleanMarkB( pAig ); @@ -657,7 +660,7 @@ ABC_PRT( "Time", clock() - clk3 ); if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) ) p->fRefining = 1; // clean the fraigs - Vec_PtrForEachEntry( p->vFraigs, pAigPart, i ) + Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i ) Aig_ManStop( pAigPart ); // repartition if needed @@ -702,3 +705,5 @@ finish: //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 8bdd147d..7e427e72 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -307,3 +310,5 @@ void Fra_ManPrint( Fra_Man_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c index 6dfbd2e9..9556bb51 100644 --- a/src/aig/fra/fraPart.c +++ b/src/aig/fra/fraPart.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -63,7 +66,7 @@ ABC_PRT( "Supports", clock() - clk ); // remove last entry Aig_ManForEachPo( p, pObj, i ) { - vSup = Vec_VecEntry( vSupps, i ); + vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i ); Vec_IntPop( vSup ); // remember support // pObj->pNext = (Aig_Obj_t *)vSup; @@ -74,7 +77,7 @@ clk = clock(); vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) ); Aig_ManForEachPo( p, pObj, i ) { - vSup = Vec_VecEntry( vSupps, i ); + vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i ); Vec_IntForEachEntry( vSup, Entry, k ) Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i ); } @@ -91,7 +94,7 @@ clk = clock(); { // Bar_ProgressUpdate( pProgress, i, NULL ); // get old supports - vSup = Vec_VecEntry( vSupps, i ); + vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i ); if ( Vec_IntSize(vSup) < 2 ) continue; // compute new supports @@ -106,7 +109,7 @@ clk = clock(); // pObj = Aig_ManObj( p, Entry ); // get support of this output // vSup2 = (Vec_Int_t *)pObj->pNext; - vSup2 = Vec_VecEntry( vSupps, k ); + vSup2 = (Vec_Int_t *)Vec_VecEntry( vSupps, k ); // count the number of common vars nCommon = Vec_IntTwoCountCommon(vSup, vSup2); if ( nCommon < 2 ) @@ -197,7 +200,7 @@ ABC_PRT( "Supports", clock() - clk ); // remove last entry Aig_ManForEachPo( p, pObj, i ) { - vSup = Vec_VecEntry( vSupps, i ); + vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i ); Vec_IntPop( vSup ); // remember support // pObj->pNext = (Aig_Obj_t *)vSup; @@ -210,7 +213,7 @@ clk = clock(); { if ( i == p->nAsserts ) break; - vSup = Vec_VecEntry( vSupps, i ); + vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i ); Vec_IntForEachEntry( vSup, Entry, k ) Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i ); } @@ -223,17 +226,17 @@ clk = clock(); { if ( i % 50 != 0 ) continue; - vSup = Vec_VecEntry( vSupps, i ); + vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i ); memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) ); // go through each input of this output Vec_IntForEachEntry( vSup, Entry, k ) { pSupp[Entry] = 1; - vSup2 = Vec_VecEntry( vSuppsIn, Entry ); + vSup2 = (Vec_Int_t *)Vec_VecEntry( vSuppsIn, Entry ); // go though each assert of this input Vec_IntForEachEntry( vSup2, Entry2, m ) { - vSup3 = Vec_VecEntry( vSupps, Entry2 ); + vSup3 = (Vec_Int_t *)Vec_VecEntry( vSupps, Entry2 ); // go through each input of this assert Vec_IntForEachEntry( vSup3, Entry3, n ) { @@ -261,3 +264,5 @@ ABC_PRT( "Extension ", clock() - clk ); //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index 039a660f..50503670 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -21,6 +21,9 @@ #include <math.h> #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -512,7 +515,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i veci_push(&p->pSat->act_vars, Fra_ObjSatNum(pObj)); // explore the fanins vFanins = Fra_ObjFaninVec( pObj ); - Vec_PtrForEachEntry( vFanins, pFanin, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, i ) Counter += Fra_SetActivityFactors_rec( p, Aig_Regular(pFanin), LevelMin, LevelMax ); return 1 + Counter; } @@ -557,3 +560,5 @@ p->timeTrav += clock() - clk; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index ccb3e7b1..1576a70a 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -23,6 +23,10 @@ #include "int.h" #include "ssw.h" #include "saig.h" +#include "bbr.h" + +ABC_NAMESPACE_IMPL_START + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -63,7 +67,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p ) p->fInterpolation = 1; // enables interpolation p->fInterSeparate = 0; // enables interpolation for each outputs separately p->fReachability = 1; // enables BDD based reachability - p->fReorderImage = 0; // 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->fUseNewProver = 0; // enables new prover p->fSilent = 0; // disables all output @@ -292,7 +296,7 @@ ABC_PRT( "Time", clock() - clk ); // perform min-area retiming if ( pParSec->fRetimeRegs && pNew->nRegs ) { - extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); +// extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); clk = clock(); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); @@ -353,9 +357,9 @@ clk = clock(); Aig_ManSetRegNum( pNew, pNew->nRegs ); // pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 ); if ( Aig_ManRegNum(pNew) > 0 ) - pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 ); + pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 ); else - pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); + pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); if ( pNew == NULL ) { @@ -382,7 +386,7 @@ ABC_PRT( "Time", clock() - clk ); // if ( pParSec->fRetimeFirst && pNew->nRegs ) if ( pNew->nRegs ) { - extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); +// extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); clk = clock(); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); @@ -480,7 +484,7 @@ clk = clock(); } else if ( pParSec->fInterSeparate ) { - Ssw_Cex_t * pCex = NULL; + Abc_Cex_t * pCex = NULL; Aig_Man_t * pTemp, * pAux; Aig_Obj_t * pObjPo; int i, Counter = 0; @@ -488,6 +492,8 @@ clk = clock(); { if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pNew) ) continue; + if ( pPars->fVerbose ) + printf( "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pNew) ); pTemp = Aig_ManDupOneOutput( pNew, i, 1 ); pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 ); Aig_ManStop( pAux ); @@ -537,7 +543,7 @@ clk = clock(); RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth ); if ( pNewOrpos->pSeqModel ) { - Ssw_Cex_t * pCex; + Abc_Cex_t * pCex; pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL; pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel ); } @@ -561,10 +567,19 @@ ABC_PRT( "Time", clock() - clk ); // try reachability analysis if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax ) { - extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ); + Saig_ParBbr_t Pars, * pPars = &Pars; + Bbr_ManSetDefaultParams( pPars ); + pPars->TimeLimit = 0; + pPars->nBddMax = pParSec->nBddMax; + pPars->nIterMax = pParSec->nBddIterMax; + pPars->fPartition = 1; + pPars->fReorder = 1; + pPars->fReorderImage = 1; + pPars->fVerbose = 0; + pPars->fSilent = pParSec->fSilent; pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); - RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, pParSec->fReorderImage, 0, pParSec->fSilent ); + RetValue = Aig_ManVerifyUsingBdds( pNew, pPars ); } finish: @@ -645,3 +660,5 @@ ABC_PRT( "Time", clock() - clkTotal ); //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 4f164e5c..25c30989 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -41,7 +44,7 @@ ***********************************************************************/ int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ) { - Fra_Man_t * p = pObj->pData; + Fra_Man_t * p = (Fra_Man_t *)pObj->pData; static int s_FPrimes[128] = { 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, @@ -81,7 +84,7 @@ int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ) ***********************************************************************/ int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ) { - Fra_Man_t * p = pObj->pData; + Fra_Man_t * p = (Fra_Man_t *)pObj->pData; unsigned * pSims; int i; pSims = Fra_ObjSim(p->pSml, pObj->Id); @@ -104,7 +107,7 @@ int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ) ***********************************************************************/ int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) { - Fra_Man_t * p = pObj0->pData; + Fra_Man_t * p = (Fra_Man_t *)pObj0->pData; unsigned * pSims0, * pSims1; int i; pSims0 = Fra_ObjSim(p->pSml, pObj0->Id); @@ -885,12 +888,12 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW SeeAlso [] ***********************************************************************/ -Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) +Abc_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) { - Fra_Cex_t * pCex; + Abc_Cex_t * pCex; int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); - pCex = (Fra_Cex_t *)ABC_ALLOC( char, sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords ); - memset( pCex, 0, sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords ); + pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); + memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); pCex->nRegs = nRegs; pCex->nPis = nRealPis; pCex->nBits = nRegs + nRealPis * nFrames; @@ -908,7 +911,7 @@ Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) SeeAlso [] ***********************************************************************/ -void Fra_SmlFreeCounterExample( Fra_Cex_t * pCex ) +void Fra_SmlFreeCounterExample( Abc_Cex_t * pCex ) { ABC_FREE( pCex ); } @@ -924,9 +927,9 @@ void Fra_SmlFreeCounterExample( Fra_Cex_t * pCex ) SeeAlso [] ***********************************************************************/ -Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ) +Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ) { - Fra_Cex_t * pCex; + Abc_Cex_t * pCex; Aig_Obj_t * pObj; unsigned * pSims; int iPo, iFrame, iBit, i, k; @@ -998,9 +1001,9 @@ Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ) SeeAlso [] ***********************************************************************/ -Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ) +Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ) { - Fra_Cex_t * pCex; + Abc_Cex_t * pCex; Aig_Obj_t * pObj; int i, nFrames, nTruePis, nTruePos, iPo, iFrame; // get the number of frames @@ -1058,9 +1061,9 @@ Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in SeeAlso [] ***********************************************************************/ -Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) +Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) { - Fra_Cex_t * pCex; + Abc_Cex_t * pCex; int nTruePis, nTruePos, iPo, iFrame; assert( Aig_ManRegNum(pAig) > 0 ); nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); @@ -1085,7 +1088,7 @@ Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) SeeAlso [] ***********************************************************************/ -int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p ) +int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) { Fra_Sml_t * pSml; Aig_Obj_t * pObj; @@ -1113,6 +1116,38 @@ int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p ) /**Function************************************************************* + Synopsis [Make the trivial counter-example for the trivially asserted output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Fra_SmlSimpleCounterExample( Aig_Man_t * pAig, int * pModel, int iFrame, int iPo ) +{ + Abc_Cex_t * pCex; + int iBit; + pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), iFrame + 1 ); + pCex->iPo = iPo; + pCex->iFrame = iFrame; + for ( iBit = Aig_ManRegNum(pAig); iBit < pCex->nBits; iBit++ ) + if ( pModel[iBit-Aig_ManRegNum(pAig)] ) + Aig_InfoSetBit( pCex->pData, iBit ); +/* + if ( !Fra_SmlRunCounterExample( pAig, pCex ) ) + { + printf( "Fra_SmlSimpleCounterExample(): Counter-example is invalid.\n" ); +// Fra_SmlFreeCounterExample( pCex ); +// pCex = NULL; + } +*/ + return pCex; +} + +/**Function************************************************************* + Synopsis [Resimulates the counter-example.] Description [] @@ -1122,7 +1157,7 @@ int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p ) SeeAlso [] ***********************************************************************/ -int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p ) +int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p ) { Fra_Sml_t * pSml; Aig_Obj_t * pObj; @@ -1191,3 +1226,5 @@ int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/fra/fra_.c b/src/aig/fra/fra_.c index 2b601587..8e5785ec 100644 --- a/src/aig/fra/fra_.c +++ b/src/aig/fra/fra_.c @@ -20,6 +20,9 @@ #include "fra.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -46,3 +49,5 @@ //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + |