diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/proof/pdr/pdrTsim.c | 46 | ||||
-rw-r--r-- | src/proof/ssw/sswAig.c | 17 | ||||
-rw-r--r-- | src/proof/ssw/sswBmc.c | 17 | ||||
-rw-r--r-- | src/proof/ssw/sswCnf.c | 27 | ||||
-rw-r--r-- | src/proof/ssw/sswConstr.c | 69 | ||||
-rw-r--r-- | src/proof/ssw/sswDyn.c | 33 | ||||
-rw-r--r-- | src/proof/ssw/sswFilter.c | 47 | ||||
-rw-r--r-- | src/proof/ssw/sswIslands.c | 43 | ||||
-rw-r--r-- | src/proof/ssw/sswLcorr.c | 25 | ||||
-rw-r--r-- | src/proof/ssw/sswMan.c | 37 | ||||
-rw-r--r-- | src/proof/ssw/sswPairs.c | 65 | ||||
-rw-r--r-- | src/proof/ssw/sswPart.c | 9 | ||||
-rw-r--r-- | src/proof/ssw/sswRarity.c | 183 | ||||
-rw-r--r-- | src/proof/ssw/sswRarity2.c | 63 | ||||
-rw-r--r-- | src/proof/ssw/sswSemi.c | 45 | ||||
-rw-r--r-- | src/proof/ssw/sswSim.c | 139 | ||||
-rw-r--r-- | src/proof/ssw/sswSimSat.c | 11 | ||||
-rw-r--r-- | src/proof/ssw/sswSweep.c | 23 | ||||
-rw-r--r-- | src/proof/ssw/sswUnique.c | 15 |
19 files changed, 464 insertions, 450 deletions
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 59127461..fa65edea 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -152,14 +152,14 @@ int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj ) Synopsis [Performs ternary simulation for one design.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -int Pdr_ManSimDataInit( Aig_Man_t * pAig, - Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes, +int Pdr_ManSimDataInit( Aig_Man_t * pAig, + Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes, Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals, Vec_Int_t * vCi2Rem ) { Aig_Obj_t * pObj; @@ -190,7 +190,7 @@ int Pdr_ManSimDataInit( Aig_Man_t * pAig, Synopsis [Tries to assign ternary value to one of the CIs.] Description [] - + SideEffects [] SeeAlso [] @@ -368,7 +368,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) // collect CO objects Vec_IntClear( vCoObjs ); if ( pCube == NULL ) // the target is the property output - Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); + Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); else // the target is the cube { for ( i = 0; i < pCube->nLits; i++ ) @@ -400,6 +400,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL ); assert( RetValue ); +#if 1 // try removing high-priority flops Vec_IntClear( vCi2Rem ); Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) @@ -429,10 +430,42 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); else Pdr_ManExtendUndo( p->pAig, vUndo ); } +#else + // try removing low-priority flops + Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + { + if ( !Saig_ObjIsLo( p->pAig, pObj ) ) + continue; + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); + if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) + continue; + Vec_IntClear( vUndo ); + if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) + Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); + else + Pdr_ManExtendUndo( p->pAig, vUndo ); + } + // try removing high-priority flops + Vec_IntClear( vCi2Rem ); + Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + { + if ( !Saig_ObjIsLo( p->pAig, pObj ) ) + continue; + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); + if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) + continue; + Vec_IntClear( vUndo ); + if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) + Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); + else + Pdr_ManExtendUndo( p->pAig, vUndo ); + } +#endif + if ( p->pPars->fVeryVerbose ) Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem ); - assert( RetValue ); + assert( RetValue ); // derive the set of resulting registers Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits ); @@ -447,4 +480,3 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswAig.c b/src/proof/ssw/sswAig.c index cd0f0c7a..acd8f919 100644 --- a/src/proof/ssw/sswAig.c +++ b/src/proof/ssw/sswAig.c @@ -45,7 +45,7 @@ ABC_NAMESPACE_IMPL_START Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig ) { Ssw_Frm_t * p; - p = ABC_ALLOC( Ssw_Frm_t, 1 ); + p = ABC_ALLOC( Ssw_Frm_t, 1 ); memset( p, 0, sizeof(Ssw_Frm_t) ); p->pAig = pAig; p->nObjs = Aig_ManObjNumMax( pAig ); @@ -80,7 +80,7 @@ void Ssw_FrmStop( Ssw_Frm_t * p ) Synopsis [Performs speculative reduction for one node.] Description [] - + SideEffects [] SeeAlso [] @@ -95,7 +95,7 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, return; p->nConstrTotal++; assert( pObjRepr->Id < pObj->Id ); - // get the new node + // get the new node pObjNew = Ssw_ObjFrame( p, pObj, iFrame ); // get the new node of the representative pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame ); @@ -135,7 +135,7 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Synopsis [Prepares the inductive case with speculative reduction.] Description [] - + SideEffects [] SeeAlso [] @@ -181,7 +181,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) // transfer to the primary outputs Aig_ManForEachCo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) ); - // transfer latch input to the latch outputs + // transfer latch input to the latch outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjFrame(p, pObjLi,f) ); } @@ -203,7 +203,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) Synopsis [Prepares the inductive case with speculative reduction.] Description [] - + SideEffects [] SeeAlso [] @@ -218,7 +218,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) assert( Aig_ManRegNum(p->pAig) > 0 ); assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) ); p->nConstrTotal = p->nConstrReduced = 0; - + // start the fraig package pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames ); pFrames->pName = Abc_UtilStrsav( p->pAig->pName ); @@ -245,7 +245,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) // remove dangling nodes Aig_ManCleanup( pFrames ); Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) ); -// printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n", +// Abc_Print( 1, "SpecRed: Total constraints = %d. Reduced constraints = %d.\n", // p->nConstrTotal, p->nConstrReduced ); return pFrames; } @@ -256,4 +256,3 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c index 4fa9c07a..c88b2dcc 100644 --- a/src/proof/ssw/sswBmc.c +++ b/src/proof/ssw/sswBmc.c @@ -60,10 +60,10 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f ) { if ( f == 0 ) pRes = Aig_ManConst0( pFrm->pFrames ); - else + else pRes = Ssw_BmcUnroll_rec( pFrm, Saig_ObjLoToLi(pFrm->pAig, pObj), f-1 ); } - else + else { assert( Aig_ObjIsNode(pObj) ); Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f ); @@ -81,7 +81,7 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f ) Synopsis [Derives counter-example.] Description [] - + SideEffects [] SeeAlso [] @@ -140,7 +140,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo // report statistics if ( fVerbose ) { - printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", + Abc_Print( 1, "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); fflush( stdout ); @@ -162,7 +162,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo Lit = toLitCond( Ssw_ObjSatNum(pSat,pObjFrame), Aig_IsComplement(pObjFrame) ); if ( fVerbose ) { - printf( "Solving output %2d of frame %3d ... \r", + Abc_Print( 1, "Solving output %2d of frame %3d ... \r", i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); } status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); @@ -199,9 +199,9 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo } if ( fVerbose ) { - printf( "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), f ); - printf( "Conf =%8.0f. Var =%8d. AIG=%9d. ", - (double)pSat->pSat->stats.conflicts, + Abc_Print( 1, "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), f ); + Abc_Print( 1, "Conf =%8.0f. Var =%8d. AIG=%9d. ", + (double)pSat->pSat->stats.conflicts, pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) ); ABC_PRT( "T", clock() - clkPart ); clkPart = clock(); @@ -222,4 +222,3 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswCnf.c b/src/proof/ssw/sswCnf.c index e3b422d5..dce61489 100644 --- a/src/proof/ssw/sswCnf.c +++ b/src/proof/ssw/sswCnf.c @@ -46,7 +46,7 @@ Ssw_Sat_t * Ssw_SatStart( int fPolarFlip ) { Ssw_Sat_t * p; int Lit; - p = ABC_ALLOC( Ssw_Sat_t, 1 ); + p = ABC_ALLOC( Ssw_Sat_t, 1 ); memset( p, 0, sizeof(Ssw_Sat_t) ); p->pAig = NULL; p->fPolarFlip = fPolarFlip; @@ -80,7 +80,7 @@ Ssw_Sat_t * Ssw_SatStart( int fPolarFlip ) ***********************************************************************/ void Ssw_SatStop( Ssw_Sat_t * p ) { -// printf( "Recycling SAT solver with %d vars and %d restarts.\n", +// Abc_Print( 1, "Recycling SAT solver with %d vars and %d restarts.\n", // p->pSat->size, p->pSat->stats.starts ); if ( p->pSat ) sat_solver_delete( p->pSat ); @@ -174,10 +174,10 @@ void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode ) // two additional clauses // t' & e' -> f' - // t & e -> f + // t & e -> f // t + e + f' - // t' + e' + f + // t' + e' + f if ( VarT == VarE ) { @@ -214,7 +214,7 @@ void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode ) Synopsis [Addes clauses to the solver.] Description [] - + SideEffects [] SeeAlso [] @@ -267,7 +267,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) Synopsis [Collects the supergate.] Description [] - + SideEffects [] SeeAlso [] @@ -276,8 +276,8 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) { // if the new node is complemented or a PI, another gate begins - if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || - (!fFirst && Aig_ObjRefs(pObj) > 1) || + if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || + (!fFirst && Aig_ObjRefs(pObj) > 1) || (fUseMuxes && Aig_ObjIsMuxType(pObj)) ) { Vec_PtrPushUnique( vSuper, pObj ); @@ -294,7 +294,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int Synopsis [Collects the supergate.] Description [] - + SideEffects [] SeeAlso [] @@ -313,7 +313,7 @@ void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) Synopsis [Updates the solver clause database.] Description [] - + SideEffects [] SeeAlso [] @@ -342,14 +342,14 @@ void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie Synopsis [Updates the solver clause database.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj ) -{ +{ Vec_Ptr_t * vFrontier; Aig_Obj_t * pNode, * pFanin; int i, k, fUseMuxes = 1; @@ -393,7 +393,7 @@ void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj ) Synopsis [Copy pattern from the solver into the internal storage.] Description [] - + SideEffects [] SeeAlso [] @@ -425,4 +425,3 @@ int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c index 2612191d..475ed70c 100644 --- a/src/proof/ssw/sswConstr.c +++ b/src/proof/ssw/sswConstr.c @@ -77,32 +77,32 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames ) continue; Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) ); } - // transfer latch inputs to the latch outputs + // transfer latch inputs to the latch outputs Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) Aig_ObjSetCopy( pObjLo, Aig_ObjCopy(pObjLi) ); } // remove dangling nodes Aig_ManCleanup( pFrames ); - return pFrames; -} + return pFrames; +} /**Function************************************************************* Synopsis [Finds one satisfiable assignment of the timeframes.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) -{ +{ Aig_Man_t * pFrames; sat_solver * pSat; Cnf_Dat_t * pCnf; - Aig_Obj_t * pObj; + Aig_Obj_t * pObj; int i, RetValue; if ( pvInits ) *pvInits = NULL; @@ -110,7 +110,7 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) // derive the timeframes pFrames = Ssw_FramesWithConstraints( p, nFrames ); // create CNF - pCnf = Cnf_Derive( pFrames, 0 ); + pCnf = Cnf_Derive( pFrames, 0 ); // create SAT solver pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); if ( pSat == NULL ) @@ -120,7 +120,7 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) return 1; } // solve - RetValue = sat_solver_solve( pSat, NULL, NULL, + RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue == l_True && pvInits ) { @@ -129,8 +129,8 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) Vec_IntPush( *pvInits, sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) ); // Aig_ManForEachCi( pFrames, pObj, i ) -// printf( "%d", Vec_IntEntry(*pvInits, i) ); -// printf( "\n" ); +// Abc_Print( 1, "%d", Vec_IntEntry(*pvInits, i) ); +// Abc_Print( 1, "\n" ); } sat_solver_delete( pSat ); Cnf_DataFree( pCnf ); @@ -154,19 +154,19 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) ***********************************************************************/ int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) -{ +{ Vec_Int_t * vLits; sat_solver * pSat; Cnf_Dat_t * pCnf; - Aig_Obj_t * pObj; + Aig_Obj_t * pObj; int i, f, iVar, RetValue, nRegs; if ( pvInits ) *pvInits = NULL; assert( p->nConstrs > 0 ); // create CNF nRegs = p->nRegs; p->nRegs = 0; - pCnf = Cnf_Derive( p, Aig_ManCoNum(p) ); - p->nRegs = nRegs; + pCnf = Cnf_Derive( p, Aig_ManCoNum(p) ); + p->nRegs = nRegs; // create SAT solver pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 ); assert( pSat->size == nFrames * pCnf->nVars ); @@ -188,8 +188,8 @@ int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) Vec_IntPush( vLits, toLitCond(iVar, 1) ); } } - RetValue = sat_solver_solve( pSat, (int *)Vec_IntArray(vLits), - (int *)Vec_IntArray(vLits) + Vec_IntSize(vLits), + RetValue = sat_solver_solve( pSat, (int *)Vec_IntArray(vLits), + (int *)Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue == l_True && pvInits ) { @@ -225,12 +225,12 @@ int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) ***********************************************************************/ void Ssw_ManPrintPolarity( Aig_Man_t * p ) -{ +{ Aig_Obj_t * pObj; int i; Aig_ManForEachObj( p, pObj, i ) - printf( "%d", pObj->fPhase ); - printf( "\n" ); + Abc_Print( 1, "%d", pObj->fPhase ); + Abc_Print( 1, "\n" ); } /**Function************************************************************* @@ -245,7 +245,7 @@ void Ssw_ManPrintPolarity( Aig_Man_t * p ) ***********************************************************************/ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p ) -{ +{ Aig_Obj_t * pObj, * pObjLi; int f, i, iLits, RetValue1, RetValue2; int nFrames = Vec_IntSize(p->vInits) / Saig_ManPiNum(p->pAig); @@ -276,12 +276,12 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p ) if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) ) { if ( pObj->fMarkB ) - printf( "output %d failed in frame %d.\n", i, f ); + Abc_Print( 1, "output %d failed in frame %d.\n", i, f ); } else { if ( pObj->fMarkB ) - printf( "constraint %d failed in frame %d.\n", i, f ); + Abc_Print( 1, "constraint %d failed in frame %d.\n", i, f ); } } // transfer @@ -312,7 +312,7 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p ) ***********************************************************************/ int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) -{ +{ Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; int RetValue; // get representative of this class @@ -328,7 +328,7 @@ int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ); // if the fraiged nodes are the same, return if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) - return 0; + return 0; // call equivalence checking if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) ) RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); @@ -351,7 +351,7 @@ int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr ) { - printf( "Ssw_ManSweepNodeConstr(): Failed to refine representative.\n" ); + Abc_Print( 1, "Ssw_ManSweepNodeConstr(): Failed to refine representative.\n" ); } return 1; } @@ -398,7 +398,7 @@ Aig_Obj_t * Ssw_ManSweepBmcConstr_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) Synopsis [Performs fraiging for the internal nodes.] Description [] - + SideEffects [] SeeAlso [] @@ -464,7 +464,7 @@ clk = clock(); // quit if this is the last timeframe if ( f == p->pPars->nFramesK - 1 ) break; - // transfer latch input to the latch outputs + // transfer latch input to the latch outputs Aig_ManForEachCo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) ); // build logic cones for register outputs @@ -489,7 +489,7 @@ p->timeBmc += clock() - clk; Synopsis [Performs fraiging for the internal nodes.] Description [] - + SideEffects [] SeeAlso [] @@ -545,7 +545,7 @@ clk = clock(); // quit if this is the last timeframe if ( f == p->pPars->nFramesK - 1 ) break; - // transfer latch input to the latch outputs + // transfer latch input to the latch outputs Aig_ManForEachCo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) ); // build logic cones for register outputs @@ -572,7 +572,7 @@ p->timeBmc += clock() - clk; Synopsis [Performs fraiging for the internal nodes.] Description [] - + SideEffects [] SeeAlso [] @@ -610,14 +610,14 @@ Aig_Obj_t * Ssw_FramesWithClasses_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) Synopsis [Performs fraiging for the internal nodes.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ int Ssw_ManSweepConstr( Ssw_Man_t * p ) -{ +{ Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObj2, * pObjNew; int nConstrPairs, i, f, iLits; @@ -672,7 +672,7 @@ p->timeReduce += clock() - clk; assert( Ssw_ObjChild0Fra(p,pObj,f) != Aig_ManConst1(p->pFrames) ); if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst1(p->pFrames) ) { - printf( "Polarity violation.\n" ); + Abc_Print( 1, "Polarity violation.\n" ); continue; } Ssw_NodesAreConstrained( p, Ssw_ObjChild0Fra(p,pObj,f), Aig_ManConst0(p->pFrames) ); @@ -695,7 +695,7 @@ p->timeReduce += clock() - clk; if ( Saig_ObjIsLo(p->pAig, pObj) ) p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 ); else if ( Aig_ObjIsNode(pObj) ) - { + { pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 ); @@ -714,4 +714,3 @@ p->timeReduce += clock() - clk; ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c index 96f1315b..5fc22fdf 100644 --- a/src/proof/ssw/sswDyn.c +++ b/src/proof/ssw/sswDyn.c @@ -94,7 +94,7 @@ void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis ) Synopsis [Collects new POs in p->vNewPos.] Description [] - + SideEffects [] SeeAlso [] @@ -129,11 +129,11 @@ void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos Synopsis [Loads logic cones and relevant constraints.] - Description [Both pRepr and pObj are objects of the AIG. + Description [Both pRepr and pObj are objects of the AIG. The result is the current SAT solver loaded with the logic cones - for pRepr and pObj corresponding to them in the frames, + for pRepr and pObj corresponding to them in the frames, as well as all the relevant constraints.] - + SideEffects [] SeeAlso [] @@ -151,7 +151,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) pObjFrames = Aig_Regular( Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) ); assert( pReprFrames != pObjFrames ); /* - // compute the AIG support + // compute the AIG support Vec_PtrClear( p->vNewLos ); Ssw_ManCollectPis_rec( pRepr, p->vNewLos ); Ssw_ManCollectPis_rec( pObj, p->vNewLos ); @@ -166,7 +166,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames ); Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames ); - // compute the frames support + // compute the frames support Vec_PtrClear( p->vNewLos ); Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos ); Ssw_ManCollectPis_rec( pObjFrames, p->vNewLos ); @@ -202,7 +202,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) Synopsis [Tranfers simulation information from FRAIG to AIG.] Description [] - + SideEffects [] SeeAlso [] @@ -254,7 +254,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) Synopsis [Performs one round of simulation with counter-examples.] Description [] - + SideEffects [] SeeAlso [] @@ -286,7 +286,7 @@ p->timeSimSat += clock() - clk; Synopsis [Performs one round of simulation with counter-examples.] Description [] - + SideEffects [] SeeAlso [] @@ -364,14 +364,14 @@ p->timeSimSat += clock() - clk; Synopsis [Performs fraiging for the internal nodes.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ int Ssw_ManSweepDyn( Ssw_Man_t * p ) -{ +{ Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObjNew; int i, f; @@ -414,15 +414,15 @@ p->timeReduce += clock() - clk; if ( Saig_ObjIsLo(p->pAig, pObj) ) p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL ); else if ( Aig_ObjIsNode(pObj) ) - { + { pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL ); } // check if it is time to recycle the solver - if ( p->pMSat->pSat == NULL || - (p->pPars->nSatVarMax2 && - p->pMSat->nSatVars > p->pPars->nSatVarMax2 && + if ( p->pMSat->pSat == NULL || + (p->pPars->nSatVarMax2 && + p->pMSat->nSatVars > p->pPars->nSatVarMax2 && p->nRecycleCalls > p->pPars->nRecycleCalls2) ) { // resimulate @@ -435,7 +435,7 @@ p->timeReduce += clock() - clk; Ssw_ManSweepResimulateDyn( p, f ); p->iNodeStart = i+1; } -// printf( "Recycling SAT solver with %d vars and %d calls.\n", +// Abc_Print( 1, "Recycling SAT solver with %d vars and %d calls.\n", // p->pMSat->nSatVars, p->nRecycleCalls ); // Aig_ManCleanMarkAB( p->pAig ); Aig_ManCleanMarkAB( p->pFrames ); @@ -489,4 +489,3 @@ p->timeReduce += clock() - clk; ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c index 047e2201..534fc275 100644 --- a/src/proof/ssw/sswFilter.c +++ b/src/proof/ssw/sswFilter.c @@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames ) -{ +{ Aig_Obj_t * pObj, * pObjLi; int f, i, RetValue1, RetValue2; assert( nFrames > 0 ); @@ -87,14 +87,14 @@ void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames ) Synopsis [Performs fraiging for one node.] Description [Returns the fraiged node.] - + SideEffects [] SeeAlso [] ***********************************************************************/ void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames ) -{ +{ Aig_Obj_t * pObj, * pObjLi; int f, i; assert( nFrames > 0 ); @@ -129,14 +129,14 @@ void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames ) Synopsis [Performs fraiging for one node.] Description [Returns the fraiged node.] - + SideEffects [] SeeAlso [] ***********************************************************************/ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex ) -{ +{ Aig_Obj_t * pObj, * pObjLi; int f, i, iBit; // assign register outputs @@ -164,7 +164,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex ) // check that the output failed as expected -- cannot check because it is not an SRM! // pObj = Aig_ManCo( p->pAig, pCex->iPo ); // if ( pObj->fMarkB != 1 ) -// printf( "The counter-example does not refine the output.\n" ); +// Abc_Print( 1, "The counter-example does not refine the output.\n" ); // record the new pattern Saig_ManForEachLo( p->pAig, pObj, i ) if ( pObj->fMarkB ^ Abc_InfoHasBit(p->pPatWords, Saig_ManPiNum(p->pAig) + i) ) @@ -183,7 +183,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex ) ***********************************************************************/ int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) -{ +{ Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; int RetValue; // get representative of this class @@ -199,7 +199,7 @@ int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ); // if the fraiged nodes are the same, return if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) - return 0; + return 0; // call equivalence checking if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) ) RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); @@ -222,7 +222,7 @@ int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr ) { - printf( "Ssw_ManSweepNodeFilter(): Failed to refine representative.\n" ); + Abc_Print( 1, "Ssw_ManSweepNodeFilter(): Failed to refine representative.\n" ); } return 0; } @@ -287,15 +287,15 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit ) if ( Abc_InfoHasBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i ) ) { Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst1(p->pFrames) ); -//printf( "1" ); +//Abc_Print( 1, "1" ); } else { Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) ); -//printf( "0" ); +//Abc_Print( 1, "0" ); } } -//printf( "\n" ); +//Abc_Print( 1, "\n" ); // sweep internal nodes for ( f = 0; f < p->pPars->nFramesK; f++ ) @@ -332,20 +332,20 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit ) // printout if ( p->pPars->fVerbose ) { - printf( "Frame %4d : ", f ); + Abc_Print( 1, "Frame %4d : ", f ); Ssw_ClassesPrint( p->ppClasses, 0 ); } if ( i < Vec_PtrSize(p->pAig->vObjs) ) { if ( p->pPars->fVerbose ) - printf( "Exceeded the resource limits (%d conflicts). Quitting...\n", p->pPars->nBTLimit ); + Abc_Print( 1, "Exceeded the resource limits (%d conflicts). Quitting...\n", p->pPars->nBTLimit ); break; - } + } // quit if this is the last timeframe if ( f == p->pPars->nFramesK - 1 ) { if ( p->pPars->fVerbose ) - printf( "Exceeded the time frame limit (%d time frames). Quitting...\n", p->pPars->nFramesK ); + Abc_Print( 1, "Exceeded the time frame limit (%d time frames). Quitting...\n", p->pPars->nFramesK ); break; } // check timeout @@ -371,9 +371,9 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit ) Synopsis [Filter equivalence classes of nodes.] - Description [Unrolls at most nFramesMax frames. Works with nConfMax + Description [Unrolls at most nFramesMax frames. Works with nConfMax conflicts until the first undefined SAT call. Verbose prints the message.] - + SideEffects [] SeeAlso [] @@ -415,18 +415,18 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun for ( r = 0; r < nRounds; r++ ) { if ( p->pPars->fVerbose ) - printf( "Round %3d:\n", r ); + Abc_Print( 1, "Round %3d:\n", r ); // start filtering equivalence classes Ssw_ManRefineByFilterSim( p, p->pPars->nFramesK ); if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 ) { - printf( "All equivalences are refined away.\n" ); + Abc_Print( 1, "All equivalences are refined away.\n" ); break; } // printout if ( p->pPars->fVerbose ) { - printf( "Initial : " ); + Abc_Print( 1, "Initial : " ); Ssw_ClassesPrint( p->ppClasses, 0 ); } p->pMSat = Ssw_SatStart( 0 ); @@ -447,7 +447,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun // check timeout if ( TimeLimit && clock() > nTimeToStop ) { - printf( "Reached timeout (%d seconds).\n", TimeLimit ); + Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeLimit ); break; } } @@ -471,7 +471,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun ***********************************************************************/ void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) -{ +{ Aig_Man_t * pAig; pAig = Gia_ManToAigSimple( p ); if ( p->pReprs != NULL ) @@ -491,4 +491,3 @@ void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRoun ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c index 97e9cf54..d1758b75 100644 --- a/src/proof/ssw/sswIslands.c +++ b/src/proof/ssw/sswIslands.c @@ -104,7 +104,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs ) continue; pObj1 = (Aig_Obj_t *)pObj0->pData; if ( !Saig_ObjIsLo(p1, pObj1) ) - printf( "Mismatch between LO pairs.\n" ); + Abc_Print( 1, "Mismatch between LO pairs.\n" ); } Saig_ManForEachLo( p1, pObj1, i ) { @@ -112,7 +112,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs ) continue; pObj0 = (Aig_Obj_t *)pObj1->pData; if ( !Saig_ObjIsLo(p0, pObj0) ) - printf( "Mismatch between LO pairs.\n" ); + Abc_Print( 1, "Mismatch between LO pairs.\n" ); } } @@ -164,7 +164,7 @@ void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes ) Vec_PtrPush( vNodes, pNext ); } } - Aig_ObjForEachFanout( p, pObj, pNext, iFan, k ) + Aig_ObjForEachFanout( p, pObj, pNext, iFan, k ) { if ( Saig_ObjIsPo(p, pNext) ) continue; @@ -184,7 +184,7 @@ void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes ) Synopsis [Establishes relationship between nodes using pairing.] Description [] - + SideEffects [] SeeAlso [] @@ -228,9 +228,9 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose if ( fVerbose ) { int nUnmached = Ssw_MatchingCountUnmached(p0); - printf( "Extending islands by %d steps:\n", nDist ); - printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n", - 0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), + Abc_Print( 1, "Extending islands by %d steps:\n", nDist ); + Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n", + 0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) ); } for ( d = 0; d < nDist; d++ ) @@ -262,8 +262,8 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose if ( fVerbose ) { int nUnmached = Ssw_MatchingCountUnmached(p0); - printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n", - d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), + Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n", + d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) ); } } @@ -323,7 +323,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 ) Synopsis [Derives matching for all pairs.] Description [Modifies both AIGs.] - + SideEffects [] SeeAlso [] @@ -361,7 +361,7 @@ Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 ) Synopsis [Transfers the result of matching to miter.] Description [The array of pairs should be complete.] - + SideEffects [] SeeAlso [] @@ -410,7 +410,7 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p Synopsis [Solves SEC using structural similarity.] Description [Modifies both p0 and p1 by adding extra logic.] - + SideEffects [] SeeAlso [] @@ -418,7 +418,7 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p ***********************************************************************/ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars ) { - Ssw_Man_t * p; + Ssw_Man_t * p; Vec_Int_t * vPairsAll, * vPairsMiter; Aig_Man_t * pMiter, * pAigNew; // derive full matching @@ -446,10 +446,10 @@ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_ Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); Aig_ManDumpBlif( pSRed, "srm_part.blif", NULL, NULL ); Aig_ManStop( pSRed ); - printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" ); + Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" ); } else - printf( "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" ); + Abc_Print( 1, "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" ); } p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 ); Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord ); @@ -489,11 +489,11 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai // report the result of verification RetValue = Ssw_MiterStatus( pAigRes, 1 ); if ( RetValue == 1 ) - printf( "Verification successful. " ); + Abc_Print( 1, "Verification successful. " ); else if ( RetValue == 0 ) - printf( "Verification failed with a counter-example. " ); + Abc_Print( 1, "Verification failed with a counter-example. " ); else - printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", + Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) ); ABC_PRT( "Time", clock() - clk ); Aig_ManStop( pAigRes ); @@ -545,7 +545,7 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars ) Aig_Man_t * pPart0, * pPart1; int RetValue; if ( pPars->fVerbose ) - printf( "Performing sequential verification using structural similarity.\n" ); + Abc_Print( 1, "Performing sequential verification using structural similarity.\n" ); // consider the case when a miter is given if ( p1 == NULL ) { @@ -556,7 +556,7 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars ) // demiter the miter if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) ) { - printf( "Demitering has failed.\n" ); + Abc_Print( 1, "Demitering has failed.\n" ); return -1; } } @@ -573,7 +573,7 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars ) { // Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL ); // Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL ); -// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); +// Abc_Print( 1, "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); } } assert( Aig_ManRegNum(pPart0) > 0 ); @@ -596,4 +596,3 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c index e58e9b50..cd212e0b 100644 --- a/src/proof/ssw/sswLcorr.c +++ b/src/proof/ssw/sswLcorr.c @@ -69,7 +69,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p ) Synopsis [Performs one round of simulation with counter-examples.] Description [] - + SideEffects [] SeeAlso [] @@ -99,7 +99,7 @@ p->timeSimSat += clock() - clk; Synopsis [Saves one counter-example into internal storage.] Description [] - + SideEffects [] SeeAlso [] @@ -127,7 +127,7 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand ) Synopsis [Builds fraiged logic cone of the node.] Description [] - + SideEffects [] SeeAlso [] @@ -151,7 +151,7 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj ) Synopsis [Recycles the SAT solver.] Description [] - + SideEffects [] SeeAlso [] @@ -173,17 +173,17 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj p->nCallsDelta = 0; clk = clock(); // get the fraiged node - pObjLi = Saig_ObjLoToLi( p->pAig, pObj ); + pObjLi = Saig_ObjLoToLi( p->pAig, pObj ); Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) ); pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 ); // get the fraiged representative if ( Aig_ObjIsCi(pObjRepr) ) { - pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr ); + pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr ); Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) ); pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 ); } - else + else pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, 0 ); p->timeReduce += clock() - clk; // if the fraiged nodes are the same, return @@ -200,7 +200,7 @@ p->timeReduce += clock() - clk; p->fRefined = 1; } else - { + { RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); if ( RetValue == 1 ) // proved equivalence { @@ -215,7 +215,7 @@ p->timeReduce += clock() - clk; return; } else // disproved equivalence - { + { Ssw_SmlAddPattern( p, pObjRepr, pObj ); p->nPatterns++; p->nCallsSat++; @@ -229,7 +229,7 @@ p->timeReduce += clock() - clk; Synopsis [Performs one iteration of sweeping latches.] Description [] - + SideEffects [] SeeAlso [] @@ -301,7 +301,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) if ( p->nPatterns == 32 ) Ssw_ManSweepResimulate( p ); // attempt recycling the SAT solver - if ( p->pPars->nSatVarMax && + if ( p->pPars->nSatVarMax && p->pMSat->nSatVars > p->pPars->nSatVarMax && p->nRecycleCalls > p->pPars->nRecycleCalls ) { @@ -315,7 +315,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) } // ABC_PRT( "reduce", p->timeReduce ); // Aig_TableProfile( p->pFrames ); -// printf( "And gates = %d\n", Aig_ManNodeNum(p->pFrames) ); +// Abc_Print( 1, "And gates = %d\n", Aig_ManNodeNum(p->pFrames) ); // resimulate if ( p->nPatterns > 0 ) Ssw_ManSweepResimulate( p ); @@ -335,4 +335,3 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswMan.c b/src/proof/ssw/sswMan.c index a982c0c5..45f08d89 100644 --- a/src/proof/ssw/sswMan.c +++ b/src/proof/ssw/sswMan.c @@ -50,7 +50,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) Aig_ManFanoutStart( pAig ); Aig_ManSetCioIds( pAig ); // create interpolation manager - p = ABC_ALLOC( Ssw_Man_t, 1 ); + p = ABC_ALLOC( Ssw_Man_t, 1 ); memset( p, 0, sizeof(Ssw_Man_t) ); p->pPars = pPars; p->pAig = pAig; @@ -60,7 +60,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) p->iOutputLit = -1; // allocate storage for sim pattern p->nPatWords = Abc_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) ); - p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords ); + p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords ); // other p->vNewLos = Vec_PtrAlloc( 100 ); p->vNewPos = Vec_IntAlloc( 100 ); @@ -75,7 +75,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) Synopsis [Prints stats of the manager.] Description [] - + SideEffects [] SeeAlso [] @@ -105,17 +105,17 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) { double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20); - printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f MB.\n", + Abc_Print( 1, "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f MB.\n", p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, Saig_ManConstrNum(p->pAig), p->pPars->nMaxLevs, nMemory ); - printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n", - Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), + Abc_Print( 1, "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n", + Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), 0/(p->pPars->nIters+1) ); - printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n", + Abc_Print( 1, "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n", p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p) ); - printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n", + Abc_Print( 1, "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n", p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds ); - printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", - p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), + Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat; @@ -133,13 +133,13 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) // report the reductions if ( p->pAig->nConstrs ) { - printf( "Statistics reflecting the use of constraints:\n" ); - printf( "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n", + Abc_Print( 1, "Statistics reflecting the use of constraints:\n" ); + Abc_Print( 1, "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n", p->nConesTotal, p->nConesConstr, 100.0*p->nConesConstr/p->nConesTotal ); - printf( "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n", + Abc_Print( 1, "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n", p->nEquivsTotal, p->nEquivsConstr, 100.0*p->nEquivsConstr/p->nEquivsTotal ); - printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", - p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1), + Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1), p->nRegsBegC, p->nRegsEndC, 100.0*(p->nRegsBegC-p->nRegsEndC)/(p->nRegsBegC?p->nRegsBegC:1) ); } } @@ -166,7 +166,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) p->pFrames = NULL; memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); } - if ( p->vSimInfo ) + if ( p->vSimInfo ) { Vec_PtrFree( p->vSimInfo ); p->vSimInfo = NULL; @@ -180,7 +180,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) Synopsis [Frees the manager.] Description [] - + SideEffects [] SeeAlso [] @@ -193,7 +193,7 @@ void Ssw_ManStop( Ssw_Man_t * p ) Ssw_ManPrintStats( p ); if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); - if ( p->pSml ) + if ( p->pSml ) Ssw_SmlStop( p->pSml ); if ( p->vDiffPairs ) Vec_IntFree( p->vDiffPairs ); @@ -215,4 +215,3 @@ void Ssw_ManStop( Ssw_Man_t * p ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswPairs.c b/src/proof/ssw/sswPairs.c index e4228685..3068adc4 100644 --- a/src/proof/ssw/sswPairs.c +++ b/src/proof/ssw/sswPairs.c @@ -80,11 +80,11 @@ int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose ) if ( fVerbose ) { - printf( "Miter has %d outputs. ", Saig_ManPoNum(p) ); - printf( "Const0 = %d. ", CountConst0 ); - printf( "NonConst0 = %d. ", CountNonConst0 ); - printf( "Undecided = %d. ", CountUndecided ); - printf( "\n" ); + Abc_Print( 1, "Miter has %d outputs. ", Saig_ManPoNum(p) ); + Abc_Print( 1, "Const0 = %d. ", CountConst0 ); + Abc_Print( 1, "NonConst0 = %d. ", CountNonConst0 ); + Abc_Print( 1, "Undecided = %d. ", CountUndecided ); + Abc_Print( 1, "\n" ); } if ( CountNonConst0 ) @@ -140,7 +140,7 @@ Vec_Int_t * Ssw_TransferSignalPairs( Aig_Man_t * pMiter, Aig_Man_t * pAig1, Aig_ Synopsis [Transform pairs into class representation.] Description [] - + SideEffects [] SeeAlso [] @@ -187,12 +187,12 @@ Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumM else if ( idReprRepr == -1 && idReprObj >= 0 ) { // object has a class assert( idReprObj != idRepr ); - if ( idReprObj < idRepr ) + if ( idReprObj < idRepr ) { // add idRepr to the same class Vec_IntPushUniqueOrder( pvClasses[idReprObj], idRepr ); pReprs[ idRepr ] = idReprObj; } - else // if ( idReprObj > idRepr ) + else // if ( idReprObj > idRepr ) { // make idRepr new representative Vec_IntPushFirst( pvClasses[idReprObj], idRepr ); pvClasses[idRepr] = pvClasses[idReprObj]; @@ -243,7 +243,7 @@ Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumM Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -253,7 +253,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax ) { int i; for ( i = 0; i < nObjNumMax; i++ ) - if ( pvClasses[i] ) + if ( pvClasses[i] ) Vec_IntFree( pvClasses[i] ); ABC_FREE( pvClasses ); } @@ -263,7 +263,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax ) Synopsis [Performs signal correspondence for the miter of two AIGs with node pairs defined.] Description [] - + SideEffects [] SeeAlso [] @@ -271,7 +271,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax ) ***********************************************************************/ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ) { - Ssw_Man_t * p; + Ssw_Man_t * p; Aig_Man_t * pAigNew, * pMiter; Ssw_Pars_t Pars; Vec_Int_t * vPairs; @@ -308,7 +308,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA Synopsis [Runs inductive SEC for the miter of two AIGs with node pairs defined.] Description [] - + SideEffects [] SeeAlso [] @@ -337,16 +337,16 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ) continue; /* if ( Aig_ObjIsNode(pObj) ) - printf( "n " ); + Abc_Print( 1, "n " ); else if ( Saig_ObjIsPi(pAig, pObj) ) - printf( "pi " ); + Abc_Print( 1, "pi " ); else if ( Saig_ObjIsLo(pAig, pObj) ) - printf( "lo " ); + Abc_Print( 1, "lo " ); */ Vec_IntPush( vIds1, Aig_ObjId(pObj) ); Vec_IntPush( vIds2, Aig_ObjId(pRepr) ); } - printf( "Recorded %d pairs (before: %d after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) ); + Abc_Print( 1, "Recorded %d pairs (before: %d after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) ); // try the new AIGs pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig, pAigNew, vIds1, vIds2, pPars ); Vec_IntFree( vIds1 ); @@ -354,11 +354,11 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ) // report the results RetValue = Ssw_MiterStatus( pAigRes, 1 ); if ( RetValue == 1 ) - printf( "Verification successful. " ); + Abc_Print( 1, "Verification successful. " ); else if ( RetValue == 0 ) - printf( "Verification failed with the counter-example. " ); + Abc_Print( 1, "Verification failed with the counter-example. " ); else - printf( "Verification UNDECIDED. Remaining registers %d (total %d). ", + Abc_Print( 1, "Verification UNDECIDED. Remaining registers %d (total %d). ", Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) ); ABC_PRT( "Time", clock() - clk ); // cleanup @@ -384,16 +384,16 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V clock_t clk = clock(); assert( vIds1 != NULL && vIds2 != NULL ); // try the new AIGs - printf( "Performing specialized verification with node pairs.\n" ); + Abc_Print( 1, "Performing specialized verification with node pairs.\n" ); pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig1, pAig2, vIds1, vIds2, pPars ); // report the results RetValue = Ssw_MiterStatus( pAigRes, 1 ); if ( RetValue == 1 ) - printf( "Verification successful. " ); + Abc_Print( 1, "Verification successful. " ); else if ( RetValue == 0 ) - printf( "Verification failed with a counter-example. " ); + Abc_Print( 1, "Verification failed with a counter-example. " ); else - printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", + Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) ); ABC_PRT( "Time", clock() - clk ); // cleanup @@ -418,7 +418,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ) int RetValue; clock_t clk = clock(); // try the new AIGs - printf( "Performing general verification without node pairs.\n" ); + Abc_Print( 1, "Performing general verification without node pairs.\n" ); pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 ); Aig_ManCleanup( pMiter ); pAigRes = Ssw_SignalCorrespondence( pMiter, pPars ); @@ -426,11 +426,11 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ) // report the results RetValue = Ssw_MiterStatus( pAigRes, 1 ); if ( RetValue == 1 ) - printf( "Verification successful. " ); + Abc_Print( 1, "Verification successful. " ); else if ( RetValue == 0 ) - printf( "Verification failed with a counter-example. " ); + Abc_Print( 1, "Verification failed with a counter-example. " ); else - printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", + Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) ); ABC_PRT( "Time", clock() - clk ); // cleanup @@ -455,16 +455,16 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ) int RetValue; clock_t clk = clock(); // try the new AIGs -// printf( "Performing general verification without node pairs.\n" ); +// Abc_Print( 1, "Performing general verification without node pairs.\n" ); pAigRes = Ssw_SignalCorrespondence( pMiter, pPars ); // report the results RetValue = Ssw_MiterStatus( pAigRes, 1 ); if ( RetValue == 1 ) - printf( "Verification successful. " ); + Abc_Print( 1, "Verification successful. " ); else if ( RetValue == 0 ) - printf( "Verification failed with a counter-example. " ); + Abc_Print( 1, "Verification failed with a counter-example. " ); else - printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", + Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) ); ABC_PRT( "Time", clock() - clk ); // cleanup @@ -478,4 +478,3 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c index 78ddbc5c..dbe8a877 100644 --- a/src/proof/ssw/sswPart.c +++ b/src/proof/ssw/sswPart.c @@ -56,7 +56,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) clock_t clk = clock(); if ( pPars->fConstrs ) { - printf( "Cannot use partitioned computation with constraints.\n" ); + Abc_Print( 1, "Cannot use partitioned computation with constraints.\n" ); return NULL; } // save parameters @@ -82,14 +82,14 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) if ( fPrintParts ) { // print partitions - printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) ); + Abc_Print( 1, "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) ); Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i ) { // extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); sprintf( Buffer, "part%03d.aig", i ); pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL ); Ioa_WriteAiger( pTemp, Buffer, 0, 0 ); - printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", + Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) ); Aig_ManStop( pTemp ); } @@ -109,7 +109,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) pNew = Ssw_SignalCorrespondence( pTemp, pPars ); nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack ); if ( fVerbose ) - printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", + Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses ); Aig_ManStop( pNew ); } @@ -138,4 +138,3 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 9536bed1..8df54822 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -17,7 +17,7 @@ Revision [$Id: sswRarity.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] ***********************************************************************/ - + #include "sswInt.h" #include "aig/gia/giaAig.h" #include "base/main/main.h" @@ -59,19 +59,19 @@ struct Ssw_RarMan_t_ }; -static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) +static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) { assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); return p->pRarity[iBin * (1 << p->nBinSize) + iPat]; } -static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value ) +static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value ) { assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value; } -static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) +static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) { assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); @@ -93,7 +93,7 @@ static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 6 Synopsis [Prepares random number generator.] Description [] - + SideEffects [] SeeAlso [] @@ -112,7 +112,7 @@ void Ssw_RarManPrepareRandom( int nRandSeed ) Synopsis [Initializes random primary inputs.] Description [] - + SideEffects [] SeeAlso [] @@ -139,7 +139,7 @@ void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p ) Synopsis [Derives the counter-example.] Description [] - + SideEffects [] SeeAlso [] @@ -184,13 +184,13 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin // verify the counter example if ( !Saig_ManVerifyCex( p->pAig, pCex ) ) { - printf( "Ssw_RarDeriveCex(): Counter-example is invalid.\n" ); + Abc_Print( 1, "Ssw_RarDeriveCex(): Counter-example is invalid.\n" ); // Abc_CexFree( pCex ); // pCex = NULL; } else { -// printf( "Counter-example verification is successful.\n" ); +// Abc_Print( 1, "Counter-example verification is successful.\n" ); } return pCex; } @@ -209,9 +209,9 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin ***********************************************************************/ void transpose32( unsigned A[32] ) { - int j, k; - unsigned t, m = 0x0000FFFF; - for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) ) + int j, k; + unsigned t, m = 0x0000FFFF; + for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) ) { for ( k = 0; k < 32; k = (k + j + 1) & ~j ) { @@ -220,7 +220,7 @@ void transpose32( unsigned A[32] ) A[k+j] = A[k+j] ^ (t << j); } } -} +} /**Function************************************************************* @@ -235,9 +235,9 @@ void transpose32( unsigned A[32] ) ***********************************************************************/ void transpose64( word A[64] ) { - int j, k; - word t, m = 0x00000000FFFFFFFF; - for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) ) + int j, k; + word t, m = 0x00000000FFFFFFFF; + for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) ) { for ( k = 0; k < 64; k = (k + j + 1) & ~j ) { @@ -246,14 +246,14 @@ void transpose64( word A[64] ) A[k+j] = A[k+j] ^ (t << j); } } -} +} /**Function************************************************************* Synopsis [Transposing 64-bit matrix.] Description [] - + SideEffects [] SeeAlso [] @@ -261,10 +261,10 @@ void transpose64( word A[64] ) ***********************************************************************/ void transpose64Simple( word A[64], word B[64] ) { - int i, k; + int i, k; for ( i = 0; i < 64; i++ ) B[i] = 0; - for ( i = 0; i < 64; i++ ) + for ( i = 0; i < 64; i++ ) for ( k = 0; k < 64; k++ ) if ( (A[i] >> k) & 1 ) B[k] |= ((word)1 << (63-i)); @@ -292,7 +292,7 @@ void TransposeTest() for ( i = 0; i < 64; i++ ) M[i] = i? (word)0 : ~(word)0; // for ( i = 0; i < 64; i++ ) -// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" ); +// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" ); clk = clock(); for ( i = 0; i < 100001; i++ ) @@ -306,14 +306,14 @@ void TransposeTest() for ( i = 0; i < 64; i++ ) if ( M[i] != N[i] ) - printf( "Mismatch\n" ); + Abc_Print( 1, "Mismatch\n" ); /* - printf( "\n" ); + Abc_Print( 1, "\n" ); for ( i = 0; i < 64; i++ ) - Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" ); - printf( "\n" ); + Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" ); + Abc_Print( 1, "\n" ); for ( i = 0; i < 64; i++ ) - Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), printf( "\n" ); + Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), Abc_Print( 1, "\n" ); */ } @@ -357,15 +357,15 @@ void Ssw_RarTranspose( Ssw_RarMan_t * p ) Saig_ManForEachLi( p->pAig, pObj, i ) { word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); printf( "\n" ); + Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); Abc_Print( 1, "\n" ); } - printf( "\n" ); + Abc_Print( 1, "\n" ); for ( i = 0; i < p->nWords*64; i++ ) { word * pBitData = Ssw_RarPatSim( p, i ); - Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); printf( "\n" ); + Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); Abc_Print( 1, "\n" ); } - printf( "\n" ); + Abc_Print( 1, "\n" ); */ } @@ -423,7 +423,7 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit ) Synopsis [Returns 1 if simulation info is composed of all zeros.] Description [] - + SideEffects [] SeeAlso [] @@ -446,7 +446,7 @@ int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj ) Synopsis [Returns 1 if simulation infos are equal.] Description [] - + SideEffects [] SeeAlso [] @@ -470,7 +470,7 @@ int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) Synopsis [Computes hash value of the node using its simulation info.] Description [] - + SideEffects [] SeeAlso [] @@ -479,19 +479,19 @@ int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj ) { Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan; - static int s_SPrimes[128] = { - 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, - 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, - 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, - 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, - 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, - 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, - 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, - 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, - 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, - 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, - 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, - 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, + static int s_SPrimes[128] = { + 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, + 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, + 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, + 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, + 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, + 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, + 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, + 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, + 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, + 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, + 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, + 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 }; unsigned * pSims; @@ -509,7 +509,7 @@ unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj ) Synopsis [Returns 1 if simulation info is composed of all zeros.] Description [] - + SideEffects [] SeeAlso [] @@ -537,7 +537,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) Synopsis [Check if any of the POs becomes non-constant.] Description [] - + SideEffects [] SeeAlso [] @@ -568,7 +568,7 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p ) Synopsis [Performs one round of simulation.] Description [] - + SideEffects [] SeeAlso [] @@ -580,7 +580,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f word * pSim, * pSim0, * pSim1; word Flip, Flip0, Flip1; int w, i; - // initialize + // initialize Ssw_RarManInitialize( p, vInit ); Vec_PtrClear( p->vUpdConst ); Vec_PtrClear( p->vUpdClass ); @@ -603,7 +603,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f Aig_ObjSetTravIdCurrent( p->pAig, pRepr ); } } - // simulate + // simulate Aig_ManForEachNode( p->pAig, pObj, i ) { pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); @@ -657,7 +657,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 ); Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 ); } - } + } } @@ -666,7 +666,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -700,7 +700,7 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -725,7 +725,7 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p ) Synopsis [Select best patterns.] Description [] - + SideEffects [] SeeAlso [] @@ -762,7 +762,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) p->pPatCosts[k] += 1.0/(Value*Value); } // print the result -//printf( "%3d : %9.6f\n", k, p->pPatCosts[k] ); +//Abc_Print( 1, "%3d : %9.6f\n", k, p->pPatCosts[k] ); } // choose as many as there are words @@ -785,7 +785,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest ); for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ ) Vec_IntPush( vInits, Abc_InfoHasBit(pPattern, k) ); -//printf( "Best pattern %5d\n", iPatBest ); +//Abc_Print( 1, "Best pattern %5d\n", iPatBest ); Vec_IntPush( p->vPatBests, iPatBest ); } assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords ); @@ -804,7 +804,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) ***********************************************************************/ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex ) -{ +{ Vec_Int_t * vInit; Aig_Obj_t * pObj, * pObjLi; int f, i, iBit; @@ -833,15 +833,15 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex // check that the output failed as expected -- cannot check because it is not an SRM! // pObj = Aig_ManCo( pAig, pCex->iPo ); // if ( pObj->fMarkB != 1 ) -// printf( "The counter-example does not refine the output.\n" ); +// Abc_Print( 1, "The counter-example does not refine the output.\n" ); // record the new pattern vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) ); Saig_ManForEachLo( pAig, pObj, i ) { -//printf( "%d", pObj->fMarkB ); +//Abc_Print( 1, "%d", pObj->fMarkB ); Vec_IntPush( vInit, pObj->fMarkB ); } -//printf( "\n" ); +//Abc_Print( 1, "\n" ); Aig_ManCleanMarkB( pAig ); return vInit; } @@ -872,7 +872,7 @@ int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose ) pAig->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), 1 ); pAig->pSeqModel->iPo = i; if ( fVerbose ) - printf( "Output %d is trivally SAT in frame 0. \n", i ); + Abc_Print( 1, "Output %d is trivally SAT in frame 0. \n", i ); return 1; } } @@ -911,7 +911,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) ) return 0; if ( fVerbose ) - printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", + Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", nWords, nFrames, nRounds, nRandSeed, TimeOut ); // reset random numbers Ssw_RarManPrepareRandom( nSavedSeed ); @@ -929,7 +929,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits ); Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0 ); // if ( pNewAig->pSeqModel != NULL ) -// printf( "BMC has found a counter-example in frame %d.\n", iFrameFail ); +// Abc_Print( 1, "BMC has found a counter-example in frame %d.\n", iFrameFail ); Aig_ManStop( pNewAig ); } // simulate @@ -938,12 +938,12 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 ); if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) { - if ( fVerbose ) printf( "\n" ); -// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + if ( fVerbose ) Abc_Print( 1, "\n" ); +// Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); Ssw_RarManPrepareRandom( nSavedSeed ); ABC_FREE( pAig->pSeqModel ); if ( fVerbose ) - printf( "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart ); + Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, fVerbose ); // print final report Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); @@ -954,9 +954,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in // check timeout if ( TimeOut && clock() > nTimeToStop ) { - if ( fVerbose ) printf( "\n" ); - printf( "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); - printf( "Reached timeout (%d sec).\n", TimeOut ); + if ( fVerbose ) Abc_Print( 1, "\n" ); + Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); + Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut ); goto finish; } } @@ -977,16 +977,16 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in // printout if ( fVerbose ) { -// printf( "Round %3d: ", r ); +// Abc_Print( 1, "Round %3d: ", r ); // Abc_PrintTime( 1, "Time", clock() - clk ); - printf( "." ); + Abc_Print( 1, "." ); } } finish: if ( r == nRounds && f == nFrames ) { - if ( fVerbose ) printf( "\n" ); - printf( "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); + if ( fVerbose ) Abc_Print( 1, "\n" ); + Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } // cleanup @@ -1048,7 +1048,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize if ( fMiter && Ssw_RarCheckTrivial( pAig, 1 ) ) return 0; if ( fVerbose ) - printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", + Abc_Print( 1, "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", nWords, nFrames, nRounds, nRandSeed, TimeOut ); // reset random numbers Ssw_RarManPrepareRandom( nSavedSeed ); @@ -1060,7 +1060,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize if ( pCex ) { p->vInits = Ssw_RarFindStartingState( pAig, pCex ); - printf( "Beginning simulation from the state derived using the counter-example.\n" ); + Abc_Print( 1, "Beginning simulation from the state derived using the counter-example.\n" ); } else p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) ); @@ -1079,7 +1079,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize // print the stats if ( fVerbose ) { - printf( "Initial : " ); + Abc_Print( 1, "Initial : " ); Ssw_ClassesPrint( p->ppClasses, 0 ); } // refine classes using BMC @@ -1088,7 +1088,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize // start filtering equivalence classes if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 ) { - printf( "All equivalences are refined away.\n" ); + Abc_Print( 1, "All equivalences are refined away.\n" ); break; } // simulate @@ -1097,11 +1097,11 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f ); if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) { - if ( !fVerbose ) - printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" ); -// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + if ( !fVerbose ) + Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" ); +// Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); if ( fVerbose ) - printf( "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart ); + Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart ); Ssw_RarManPrepareRandom( nSavedSeed ); Abc_CexFree( pAig->pSeqModel ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, 1 ); @@ -1114,9 +1114,9 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize // check timeout if ( TimeOut && clock() > nTimeToStop ) { - if ( fVerbose ) printf( "\n" ); - printf( "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); - printf( "Reached timeout (%d sec).\n", TimeOut ); + if ( fVerbose ) Abc_Print( 1, "\n" ); + Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); + Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut ); goto finish; } } @@ -1137,21 +1137,21 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize // printout if ( fVerbose ) { - printf( "Round %3d: ", r ); + Abc_Print( 1, "Round %3d: ", r ); Ssw_ClassesPrint( p->ppClasses, 0 ); } else { - printf( "." ); + Abc_Print( 1, "." ); } } finish: // report if ( r == nRounds && f == nFrames ) { - if ( !fVerbose ) - printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" ); - printf( "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); + if ( !fVerbose ) + Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" ); + Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } // cleanup @@ -1171,7 +1171,7 @@ finish: ***********************************************************************/ int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) -{ +{ Aig_Man_t * pAig; int RetValue; pAig = Gia_ManToAigSimple( p ); @@ -1197,4 +1197,3 @@ int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c index 6a67dea6..f6b2c319 100644 --- a/src/proof/ssw/sswRarity2.c +++ b/src/proof/ssw/sswRarity2.c @@ -50,19 +50,19 @@ struct Ssw_RarMan_t_ }; -static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) +static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) { assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); return p->pRarity[iBin * (1 << p->nBinSize) + iPat]; } -static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value ) +static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value ) { assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value; } -static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) +static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) { assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); @@ -78,7 +78,7 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -109,7 +109,7 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -148,7 +148,7 @@ static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) Saig_ManForEachLi( p->pAig, pObj, i ) { pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); - Extra_PrintBinary( stdout, pData, 32 ); printf( "\n" ); + Extra_PrintBinary( stdout, pData, 32 ); Abc_Print( 1, "\n" ); } */ for ( k = 0; k < p->nWords * 32; k++ ) @@ -168,8 +168,8 @@ static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) for ( i = 0; i < p->nGroups; i++ ) { for ( k = 0; k < (1 << p->nBinSize); k++ ) - printf( "%d ", Ssw_RarGetBinPat(p, i, k) ); - printf( "\n" ); + Abc_Print( 1, "%d ", Ssw_RarGetBinPat(p, i, k) ); + Abc_Print( 1, "\n" ); } */ } @@ -212,7 +212,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) p->pPatCosts[k] += 1.0/(Value*Value); } // print the result -// printf( "%3d : %9.6f\n", k, p->pPatCosts[k] ); +// Abc_Print( 1, "%3d : %9.6f\n", k, p->pPatCosts[k] ); } // choose as many as there are words @@ -237,7 +237,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); Vec_IntPush( vInits, Abc_InfoHasBit(pData, iPatBest) ); } -//printf( "Best pattern %5d\n", iPatBest ); +//Abc_Print( 1, "Best pattern %5d\n", iPatBest ); } assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords ); } @@ -255,7 +255,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) ***********************************************************************/ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex ) -{ +{ Vec_Int_t * vInit; Aig_Obj_t * pObj, * pObjLi; int f, i, iBit; @@ -284,7 +284,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex // check that the output failed as expected -- cannot check because it is not an SRM! // pObj = Aig_ManCo( pAig, pCex->iPo ); // if ( pObj->fMarkB != 1 ) -// printf( "The counter-example does not refine the output.\n" ); +// Abc_Print( 1, "The counter-example does not refine the output.\n" ); // record the new pattern vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) ); Saig_ManForEachLo( pAig, pObj, i ) @@ -318,7 +318,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i if ( Aig_ManNodeNum(pAig) == 0 ) return -1; if ( fVerbose ) - printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", + Abc_Print( 1, "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", nWords, nFrames, nBinSize, nRounds, TimeOut ); // reset random numbers Aig_ManRandom( 1 ); @@ -336,8 +336,8 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i Ssw_SmlSimulateOne( p->pSml ); if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) { - if ( fVerbose ) printf( "\n" ); - printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + if ( fVerbose ) Abc_Print( 1, "\n" ); + Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); RetValue = 0; break; } @@ -348,22 +348,22 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i // printout if ( fVerbose ) { -// printf( "Round %3d: ", r ); +// Abc_Print( 1, "Round %3d: ", r ); // Abc_PrintTime( 1, "Time", clock() - clk ); - printf( "." ); + Abc_Print( 1, "." ); } // check timeout if ( TimeOut && clock() > nTimeToStop ) { - if ( fVerbose ) printf( "\n" ); - printf( "Reached timeout (%d seconds).\n", TimeOut ); + if ( fVerbose ) Abc_Print( 1, "\n" ); + Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeOut ); break; } } if ( r == nRounds ) { - if ( fVerbose ) printf( "\n" ); - printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); + if ( fVerbose ) Abc_Print( 1, "\n" ); + Abc_Print( 1, "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } // cleanup @@ -397,7 +397,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz if ( Aig_ManNodeNum(pAig) == 0 ) return -1; if ( fVerbose ) - printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", + Abc_Print( 1, "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", nWords, nFrames, nBinSize, nRounds, TimeOut ); // reset random numbers Aig_ManRandom( 1 ); @@ -427,7 +427,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz // print the stats if ( fVerbose ) { - printf( "Initial : " ); + Abc_Print( 1, "Initial : " ); Ssw_ClassesPrint( p->ppClasses, 0 ); } // refine classes using BMC @@ -436,15 +436,15 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz // start filtering equivalence classes if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 ) { - printf( "All equivalences are refined away.\n" ); + Abc_Print( 1, "All equivalences are refined away.\n" ); break; } // simulate Ssw_SmlSimulateOne( p->pSml ); if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) { - if ( fVerbose ) printf( "\n" ); - printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + if ( fVerbose ) Abc_Print( 1, "\n" ); + Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); RetValue = 0; break; } @@ -454,7 +454,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz // printout if ( fVerbose ) { - printf( "Round %3d: ", r ); + Abc_Print( 1, "Round %3d: ", r ); Ssw_ClassesPrint( p->ppClasses, 0 ); } // get initialization patterns @@ -464,14 +464,14 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz // check timeout if ( TimeOut && clock() > nTimeToStop ) { - if ( fVerbose ) printf( "\n" ); - printf( "Reached timeout (%d seconds).\n", TimeOut ); + if ( fVerbose ) Abc_Print( 1, "\n" ); + Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeOut ); break; } } if ( r == nRounds ) { - printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); + Abc_Print( 1, "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } // cleanup @@ -491,7 +491,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz ***********************************************************************/ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) -{ +{ Aig_Man_t * pAig; int RetValue; pAig = Gia_ManToAigSimple( p ); @@ -516,4 +516,3 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c index e58ba848..822f63f5 100644 --- a/src/proof/ssw/sswSemi.c +++ b/src/proof/ssw/sswSemi.c @@ -67,7 +67,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) Aig_Obj_t * pObj; int i; // create interpolation manager - p = ABC_ALLOC( Ssw_Sem_t, 1 ); + p = ABC_ALLOC( Ssw_Sem_t, 1 ); memset( p, 0, sizeof(Ssw_Sem_t) ); p->nConfMaxStart = nConfMax; p->nConfMax = nConfMax; @@ -101,7 +101,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -120,7 +120,7 @@ void Ssw_SemManStop( Ssw_Sem_t * p ) Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -141,7 +141,7 @@ int Ssw_SemCheckTargets( Ssw_Sem_t * p ) Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -168,7 +168,7 @@ void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p ) Synopsis [Performs fraiging for the internal nodes.] Description [] - + SideEffects [] SeeAlso [] @@ -212,7 +212,7 @@ clk = clock(); { fFirst = 1; pBmc->nConfMax *= 10; - } + } } if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax ) { @@ -236,7 +236,7 @@ clk = clock(); Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew ); Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) ); } -//printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts ); +//Abc_Print( 1, "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts ); } if ( fFirst ) pBmc->nConfMax /= 10; @@ -272,10 +272,10 @@ int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int } if ( fVerbose ) { - printf( "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n", - Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), + Abc_Print( 1, "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n", + Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep ); - } + } RetValue = 0; for ( Iter = 0; Iter < p->nPatterns; Iter++ ) { @@ -284,16 +284,16 @@ clk = clock(); Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets ); if ( fVerbose ) { - printf( "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ", - Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), - Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns, + Abc_Print( 1, "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ", + Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), + Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns, p->pMan->nSatFailsReal? "f" : " " ); ABC_PRT( "T", clock() - clk ); - } + } Ssw_ManCleanup( p->pMan ); if ( fCheckTargets && Ssw_SemCheckTargets( p ) ) { - printf( "Target is hit!!!\n" ); + Abc_Print( 1, "Target is hit!!!\n" ); RetValue = 1; } if ( p->nPatterns >= p->nPatternsAlloc ) @@ -304,14 +304,14 @@ clk = clock(); pMan->nStrangers = 0; pMan->nSatCalls = 0; pMan->nSatProof = 0; - pMan->nSatFailsReal = 0; + pMan->nSatFailsReal = 0; pMan->nSatCallsUnsat = 0; - pMan->nSatCallsSat = 0; - pMan->timeSimSat = 0; - pMan->timeSat = 0; - pMan->timeSatSat = 0; - pMan->timeSatUnsat = 0; - pMan->timeSatUndec = 0; + pMan->nSatCallsSat = 0; + pMan->timeSimSat = 0; + pMan->timeSat = 0; + pMan->timeSatSat = 0; + pMan->timeSatUnsat = 0; + pMan->timeSatUndec = 0; return RetValue; } @@ -321,4 +321,3 @@ clk = clock(); ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c index bb4a55d2..469af654 100644 --- a/src/proof/ssw/sswSim.c +++ b/src/proof/ssw/sswSim.c @@ -62,19 +62,19 @@ static inline unsigned Ssw_ObjRandomSim() { return Aig_ManRa ***********************************************************************/ unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj ) { - static int s_SPrimes[128] = { - 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, - 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, - 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, - 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, - 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, - 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, - 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, - 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, - 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, - 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, - 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, - 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, + static int s_SPrimes[128] = { + 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, + 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, + 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, + 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, + 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, + 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, + 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, + 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, + 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, + 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, + 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, + 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 }; unsigned * pSims; @@ -93,7 +93,7 @@ unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj ) Synopsis [Returns 1 if simulation info is composed of all zeros.] Description [] - + SideEffects [] SeeAlso [] @@ -115,7 +115,7 @@ int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj ) Synopsis [Returns 1 if simulation infos are equal.] Description [] - + SideEffects [] SeeAlso [] @@ -138,7 +138,7 @@ int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 Synopsis [Returns 1 if the node appears to be constant 1 candidate.] Description [] - + SideEffects [] SeeAlso [] @@ -154,7 +154,7 @@ int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj ) Synopsis [Returns 1 if the nodes appear equal.] Description [] - + SideEffects [] SeeAlso [] @@ -171,7 +171,7 @@ int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) Synopsis [Counts the number of 1s in the XOR of simulation data.] Description [] - + SideEffects [] SeeAlso [] @@ -193,7 +193,7 @@ int Ssw_SmlNodeNotEquWeight( Ssw_Sml_t * p, int Left, int Right ) Synopsis [Checks implication.] Description [] - + SideEffects [] SeeAlso [] @@ -228,7 +228,7 @@ int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * p Synopsis [Counts the number of 1s in the implication.] Description [] - + SideEffects [] SeeAlso [] @@ -261,7 +261,7 @@ int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * p Synopsis [Counts the number of 1s in the implication.] Description [] - + SideEffects [] SeeAlso [] @@ -285,7 +285,7 @@ int Ssw_SmlCountEqual( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo ) Synopsis [Returns 1 if simulation info is composed of all zeros.] Description [] - + SideEffects [] SeeAlso [] @@ -307,7 +307,7 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj ) Synopsis [Returns 1 if simulation info is composed of all zeros.] Description [] - + SideEffects [] SeeAlso [] @@ -324,7 +324,7 @@ int Ssw_SmlNodeIsZeroFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f ) Synopsis [Counts the number of one's in the patten the object.] Description [] - + SideEffects [] SeeAlso [] @@ -353,7 +353,7 @@ int Ssw_SmlNodeCountOnesReal( Ssw_Sml_t * p, Aig_Obj_t * pObj ) Synopsis [Counts the number of one's in the patten the object.] Description [] - + SideEffects [] SeeAlso [] @@ -389,7 +389,7 @@ int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs ) Synopsis [Generated const 0 pattern.] Description [] - + SideEffects [] SeeAlso [] @@ -405,7 +405,7 @@ void Ssw_SmlSavePattern0( Ssw_Man_t * p, int fInit ) Synopsis [[Generated const 1 pattern.] Description [] - + SideEffects [] SeeAlso [] @@ -431,14 +431,14 @@ void Ssw_SmlSavePattern1( Ssw_Man_t * p, int fInit ) Synopsis [Creates the counter-example from the successful pattern.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo ) -{ +{ Aig_Obj_t * pFanin, * pObjPi; unsigned * pSims; int i, k, BestPat, * pModel; @@ -461,10 +461,10 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo ) Aig_ManForEachCi( p->pAig, pObjPi, i ) { pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat); -// printf( "%d", pModel[i] ); +// Abc_Print( 1, "%d", pModel[i] ); } pModel[Aig_ManCiNum(p->pAig)] = pObjPo->Id; -// printf( "\n" ); +// Abc_Print( 1, "\n" ); return pModel; } @@ -485,7 +485,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p ) int i; // make sure the reference simulation pattern does not detect the bug pObj = Aig_ManCo( p->pAig, 0 ); - assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); + assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); Aig_ManForEachCo( p->pAig, pObj, i ) { if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) ) @@ -504,7 +504,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p ) Synopsis [Assigns random patterns to the PI node.] Description [] - + SideEffects [] SeeAlso [] @@ -529,7 +529,7 @@ void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj ) Synopsis [Assigns random patterns to the PI node.] Description [] - + SideEffects [] SeeAlso [] @@ -551,7 +551,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) Synopsis [Assigns constant patterns to the PI node.] Description [] - + SideEffects [] SeeAlso [] @@ -566,14 +566,14 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; for ( i = 0; i < p->nWordsFrame; i++ ) pSims[i] = fConst1? ~(unsigned)0 : 0; -} +} /**Function************************************************************* Synopsis [Assigns constant patterns to the PI node.] Description [] - + SideEffects [] SeeAlso [] @@ -587,14 +587,14 @@ void Ssw_SmlObjAssignConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, in assert( Aig_ObjIsCi(pObj) ); pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; pSims[iWord] = fConst1? ~(unsigned)0 : 0; -} +} /**Function************************************************************* Synopsis [Assigns constant patterns to the PI node.] Description [] - + SideEffects [] SeeAlso [] @@ -607,14 +607,14 @@ void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWor assert( Aig_ObjIsCi(pObj) ); pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; pSims[iWord] = Word; -} +} /**Function************************************************************* Synopsis [Assings distance-1 simulation info for the PIs.] Description [] - + SideEffects [] SeeAlso [] @@ -627,7 +627,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) assert( p->nFrames > 0 ); if ( p->nFrames == 1 ) { - // copy the PI info + // copy the PI info Aig_ManForEachCi( p->pAig, pObj, i ) Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 ); // flip one bit @@ -644,7 +644,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) for ( f = 0; f < p->nFrames; f++ ) Saig_ManForEachPi( p->pAig, pObj, i ) Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f ); - // copy the latch info + // copy the latch info k = 0; Saig_ManForEachLo( p->pAig, pObj, i ) Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 ); @@ -665,7 +665,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) Synopsis [Assings distance-1 simulation info for the PIs.] Description [] - + SideEffects [] SeeAlso [] @@ -697,7 +697,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat ) Synopsis [Simulates one node.] Description [] - + SideEffects [] SeeAlso [] @@ -763,7 +763,7 @@ void Ssw_SmlNodeSimulate( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) Synopsis [Simulates one node.] Description [] - + SideEffects [] SeeAlso [] @@ -794,7 +794,7 @@ int Ssw_SmlNodesCompareInFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pO Synopsis [Simulates one node.] Description [] - + SideEffects [] SeeAlso [] @@ -828,7 +828,7 @@ void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) Synopsis [Simulates one node.] Description [] - + SideEffects [] SeeAlso [] @@ -857,7 +857,7 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, Synopsis [Simulates one node.] Description [] - + SideEffects [] SeeAlso [] @@ -886,7 +886,7 @@ void Ssw_SmlNodeTransferFirst( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn Synopsis [Assings random simulation info for the PIs.] Description [] - + SideEffects [] SeeAlso [] @@ -919,7 +919,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit ) Synopsis [Assings random simulation info for the PIs.] Description [] - + SideEffects [] SeeAlso [] @@ -946,7 +946,7 @@ void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit ) Synopsis [Assings random simulation info for the PIs.] Description [] - + SideEffects [] SeeAlso [] @@ -971,7 +971,7 @@ void Ssw_SmlReinitialize( Ssw_Sml_t * p ) Synopsis [Check if any of the POs becomes non-constant.] Description [] - + SideEffects [] SeeAlso [] @@ -996,7 +996,7 @@ int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p ) Synopsis [Simulates AIG manager.] Description [Assumes that the PI simulation info is attached.] - + SideEffects [] SeeAlso [] @@ -1035,7 +1035,7 @@ p->nSimRounds++; Synopsis [Converts simulation information to be not normallized.] Description [] - + SideEffects [] SeeAlso [] @@ -1067,7 +1067,7 @@ void Ssw_SmlUnnormalize( Ssw_Sml_t * p ) Synopsis [Simulates AIG manager.] Description [Assumes that the PI simulation info is attached.] - + SideEffects [] SeeAlso [] @@ -1108,7 +1108,7 @@ void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pV Synopsis [Simulates AIG manager.] Description [Assumes that the PI simulation info is attached.] - + SideEffects [] SeeAlso [] @@ -1139,7 +1139,7 @@ p->nSimRounds++; Synopsis [Allocates simulation manager.] Description [] - + SideEffects [] SeeAlso [] @@ -1164,7 +1164,7 @@ Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFr Synopsis [Allocates simulation manager.] Description [] - + SideEffects [] SeeAlso [] @@ -1180,7 +1180,7 @@ void Ssw_SmlClean( Ssw_Sml_t * p ) Synopsis [Get simulation data.] Description [] - + SideEffects [] SeeAlso [] @@ -1202,7 +1202,7 @@ Vec_Ptr_t * Ssw_SmlSimDataPointers( Ssw_Sml_t * p ) Synopsis [Deallocates simulation manager.] Description [] - + SideEffects [] SeeAlso [] @@ -1219,7 +1219,7 @@ void Ssw_SmlStop( Ssw_Sml_t * p ) Synopsis [Performs simulation of the uninitialized circuit.] Description [] - + SideEffects [] SeeAlso [] @@ -1239,7 +1239,7 @@ Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords ) Synopsis [Performs simulation of the initialized circuit.] Description [] - + SideEffects [] SeeAlso [] @@ -1260,7 +1260,7 @@ Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW Synopsis [Performs next round of sequential simulation.] Description [] - + SideEffects [] SeeAlso [] @@ -1279,7 +1279,7 @@ void Ssw_SmlResimulateSeq( Ssw_Sml_t * p ) Synopsis [Returns the number of frames simulated in the manager.] Description [] - + SideEffects [] SeeAlso [] @@ -1295,7 +1295,7 @@ int Ssw_SmlNumFrames( Ssw_Sml_t * p ) Synopsis [Returns the total number of simulation words.] Description [] - + SideEffects [] SeeAlso [] @@ -1312,7 +1312,7 @@ int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p ) Description [The simulation info is normalized unless procedure Ssw_SmlUnnormalize() is called in advance.] - + SideEffects [] SeeAlso [] @@ -1329,7 +1329,7 @@ unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj ) Synopsis [Creates sequential counter-example from the simulation info.] Description [] - + SideEffects [] SeeAlso [] @@ -1391,7 +1391,7 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p ) // verify the counter example if ( !Saig_ManVerifyCex( p->pAig, pCex ) ) { - printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" ); + Abc_Print( 1, "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" ); Abc_CexFree( pCex ); pCex = NULL; } @@ -1404,4 +1404,3 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswSimSat.c b/src/proof/ssw/sswSimSat.c index 4d1b3ba2..6e5944d1 100644 --- a/src/proof/ssw/sswSimSat.c +++ b/src/proof/ssw/sswSimSat.c @@ -62,17 +62,17 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr ) RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 ); RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 ); // make sure refinement happened - if ( Aig_ObjIsConst1(pRepr) ) + if ( Aig_ObjIsConst1(pRepr) ) { assert( RetValue1 ); if ( RetValue1 == 0 ) - printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" ); + Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" ); } else { assert( RetValue2 ); if ( RetValue2 == 0 ) - printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" ); + Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" ); } } p->timeSimSat += clock() - clk; @@ -105,13 +105,13 @@ void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, { assert( RetValue1 ); if ( RetValue1 == 0 ) - printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" ); + Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" ); } else { assert( RetValue2 ); if ( RetValue2 == 0 ) - printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" ); + Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" ); } p->timeSimSat += clock() - clk; } @@ -122,4 +122,3 @@ p->timeSimSat += clock() - clk; ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c index b4ff44c2..bccc6aa4 100644 --- a/src/proof/ssw/sswSweep.c +++ b/src/proof/ssw/sswSweep.c @@ -98,7 +98,7 @@ void Ssw_CheckConstraints( Ssw_Man_t * p ) Counter++; } } - printf( "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter ); + Abc_Print( 1, "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter ); } /**Function************************************************************* @@ -148,7 +148,7 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f ) Synopsis [Saves one counter-example into internal storage.] Description [] - + SideEffects [] SeeAlso [] @@ -178,14 +178,14 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p ) Synopsis [Performs fraiging for one node.] Description [Returns the fraiged node.] - + SideEffects [] SeeAlso [] ***********************************************************************/ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs ) -{ +{ Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; int RetValue; clock_t clk; @@ -202,7 +202,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_ assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ); // if the fraiged nodes are the same, return if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) - return 0; + return 0; // add constraints on demand if ( !fBmc && p->pPars->fDynamic ) { @@ -248,7 +248,7 @@ p->timeMarkCones += clock() - clk; assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr ) { - printf( "Ssw_ManSweepNode(): Failed to refine representative.\n" ); + Abc_Print( 1, "Ssw_ManSweepNode(): Failed to refine representative.\n" ); } return 1; } @@ -299,7 +299,7 @@ clk = clock(); // quit if this is the last timeframe if ( f == p->pPars->nFramesK - 1 ) break; - // transfer latch input to the latch outputs + // transfer latch input to the latch outputs Aig_ManForEachCo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) ); // build logic cones for register outputs @@ -340,14 +340,14 @@ void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num ) pFile = fopen( pBuffer, "w" ); if ( pFile == NULL ) { - printf( "Cannot open file %s for writing.\n", pBuffer ); + Abc_Print( 1, "Cannot open file %s for writing.\n", pBuffer ); return; } fclose( pFile ); pNew = Saig_ManCreateEquivMiter( p, vPairs ); Ioa_WriteAiger( pNew, pBuffer, 0, 0 ); Aig_ManStop( pNew ); - printf( "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer ); + Abc_Print( 1, "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer ); } @@ -363,7 +363,7 @@ void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num ) ***********************************************************************/ int Ssw_ManSweep( Ssw_Man_t * p ) -{ +{ static int Counter; Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObj2, * pObjNew; @@ -412,7 +412,7 @@ p->timeReduce += clock() - clk; if ( Saig_ObjIsLo(p->pAig, pObj) ) p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved ); else if ( Aig_ObjIsNode(pObj) ) - { + { pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved ); @@ -435,4 +435,3 @@ p->timeReduce += clock() - clk; ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswUnique.c b/src/proof/ssw/sswUnique.c index 1bd44a03..9fad9060 100644 --- a/src/proof/ssw/sswUnique.c +++ b/src/proof/ssw/sswUnique.c @@ -61,7 +61,7 @@ void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p ) // Vec_IntPush( p->vDiffPairs, 1 ); else if ( Aig_ObjPhaseReal(pObj0) != Aig_ObjPhaseReal(pObj1) ) Vec_IntPush( p->vDiffPairs, 1 ); - else + else { RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObj0), Aig_Regular(pObj1) ); Vec_IntPush( p->vDiffPairs, RetValue!=1 ); @@ -72,7 +72,7 @@ void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p ) Counter = 0; Vec_IntForEachEntry( p->vDiffPairs, RetValue, i ) Counter += RetValue; -// printf( "The number of different register pairs = %d.\n", Counter ); +// Abc_Print( 1, "The number of different register pairs = %d.\n", Counter ); } @@ -96,7 +96,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV assert( p->vDiffPairs && Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) ); // compute the first support in terms of LOs - ppObjs[0] = pRepr; + ppObjs[0] = pRepr; ppObjs[1] = pObj; Aig_SupportNodes( p->pAig, ppObjs, 2, p->vCommon ); // keep only LOs @@ -116,7 +116,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV Vec_PtrShrink( p->vCommon, k ); if ( fVerbose ) - printf( "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ", + Abc_Print( 1, "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ", Aig_ObjId(pObj), RetValue, Vec_PtrSize(p->vCommon), fFeasible? "yes": "no " ); @@ -129,10 +129,10 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV if ( Value0 != Value1 ) RetValue = 0; if ( fVerbose ) - printf( "%d", Value0 ^ Value1 ); + Abc_Print( 1, "%d", Value0 ^ Value1 ); } if ( fVerbose ) - printf( "\n" ); + Abc_Print( 1, "\n" ); return RetValue && fFeasible; } @@ -166,7 +166,7 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int } if ( Aig_ObjIsConst1(Aig_Regular(pTotal)) ) { -// printf( "Skipped\n" ); +// Abc_Print( 1, "Skipped\n" ); return 0; } // create CNF @@ -194,4 +194,3 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int ABC_NAMESPACE_IMPL_END - |