abc/src/proof/ssw/sswFilter.c
/**Function*************************************************************

  Synopsis    [Filter equivalence classes of nodes.]

  Description [Unrolls at most nFramesMax frames. Works with nConfMax
  conflicts until the first undefined SAT call. Verbose prints the message.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Filter equivalence classes of nodes.]

Description [Unrolls at most nFramesMax frames. Works with nConfMax
conflicts until the first undefined SAT call. Verbose prints the message.]




Function Synopsis [ Filter equivalence classes of nodes . ] Description [ Unrolls at most nFramesMax frames . Works with nConfMax conflicts until the first undefined SAT call . Verbose prints the message . ]
void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{
    Ssw_Pars_t Pars, * pPars = &Pars;
    Ssw_Man_t * p;
    int r, TimeLimitPart;
    abctime nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
    assert( Aig_ManRegNum(pAig) > 0 );
    assert( Aig_ManConstrNum(pAig) == 0 );
    if ( Aig_ManNodeNum(pAig) == 0 )
        return;
    Aig_ManRandom( 1 );
    Ssw_ManSetDefaultParams( pPars = &Pars );
    pPars->nFramesK  = 3; 
    pPars->nBTLimit  = nConfMax;
    pPars->TimeLimit = TimeLimit;
    pPars->fVerbose  = fVerbose;
    p = Ssw_ManCreate( pAig, pPars );
    pPars->nFramesK  = nFramesMax;
    if ( pAig->pReprs == NULL )
        p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 );
    else
        p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
    Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
    assert( p->vInits == NULL );
    if ( pCex )
        Ssw_ManFindStartingState( p, pCex );
    for ( r = 0; r < nRounds; r++ )
    {
        if ( p->pPars->fVerbose )
            Abc_Print( 1, "Round %3d:\n", r );
        Ssw_ManRefineByFilterSim( p, p->pPars->nFramesK );
        if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
        {
            Abc_Print( 1, "All equivalences are refined away.\n" );
            break;
        }
        if ( p->pPars->fVerbose )
        {
            Abc_Print( 1, "Initial    : " );
            Ssw_ClassesPrint( p->ppClasses, 0 );
        }
        p->pMSat = Ssw_SatStart( 0 );
        TimeLimitPart = TimeLimit ? (nTimeToStop - Abc_Clock()) / CLOCKS_PER_SEC : 0;
        if ( TimeLimit2 )
        {
            if ( TimeLimitPart )
                TimeLimitPart = Abc_MinInt( TimeLimitPart, TimeLimit2 );
            else
                TimeLimitPart = TimeLimit2;
        }
        Ssw_ManSweepBmcFilter( p, TimeLimitPart );
        Ssw_SatStop( p->pMSat );
        p->pMSat = NULL;
        Ssw_ManCleanup( p );
        Ssw_ManRollForward( p, p->pPars->nFramesK );
        if ( TimeLimit && Abc_Clock() > nTimeToStop )
        {
            Abc_Print( 1, "Reached timeout (%d seconds).\n",  TimeLimit );
            break;
        }
    }
    Aig_ManSetPhase( p->pAig );
    Aig_ManCleanMarkB( p->pAig );
    pPars->fVerbose = 0;
    Ssw_ManStop( p );
}
void Ssw_SignalFilter ( Aig_Man_t * pAig , int nFramesMax , int nConfMax , int nRounds , int TimeLimit , int TimeLimit2 , Abc_Cex_t * pCex , int fLatchOnly , int fVerbose ) { Ssw_Pars_t Pars , * pPars = & Pars ; Ssw_Man_t * p ; int r , TimeLimitPart ; abctime nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock ( ) : 0 ; assert ( Aig_ManRegNum ( pAig ) > 0 ) ; assert ( Aig_ManConstrNum ( pAig ) == 0 ) ; if ( Aig_ManNodeNum ( pAig ) == 0 ) return ; Aig_ManRandom ( 1 ) ; Ssw_ManSetDefaultParams ( pPars = & Pars ) ; pPars -> nFramesK = 3 ; pPars -> nBTLimit = nConfMax ; pPars -> TimeLimit = TimeLimit ; pPars -> fVerbose = fVerbose ; p = Ssw_ManCreate ( pAig , pPars ) ; pPars -> nFramesK = nFramesMax ; if ( pAig -> pReprs == NULL ) p -> ppClasses = Ssw_ClassesPrepareSimple ( pAig , fLatchOnly , 0 ) ; else p -> ppClasses = Ssw_ClassesPrepareFromReprs ( pAig ) ; Ssw_ClassesSetData ( p -> ppClasses , NULL , NULL , Ssw_SmlObjIsConstBit , Ssw_SmlObjsAreEqualBit ) ; assert ( p -> vInits == NULL ) ; if ( pCex ) Ssw_ManFindStartingState ( p , pCex ) ; for ( r = 0 ; r < nRounds ; r ++ ) { if ( p -> pPars -> fVerbose ) Abc_Print ( 1 , " \n " , r ) ; Ssw_ManRefineByFilterSim ( p , p -> pPars -> nFramesK ) ; if ( Ssw_ClassesCand1Num ( p -> ppClasses ) == 0 && Ssw_ClassesClassNum ( p -> ppClasses ) == 0 ) { Abc_Print ( 1 , " \n " ) ; break ; } if ( p -> pPars -> fVerbose ) { Abc_Print ( 1 , " " ) ; Ssw_ClassesPrint ( p -> ppClasses , 0 ) ; } p -> pMSat = Ssw_SatStart ( 0 ) ; TimeLimitPart = TimeLimit ? ( nTimeToStop - Abc_Clock ( ) ) / CLOCKS_PER_SEC : 0 ; if ( TimeLimit2 ) { if ( TimeLimitPart ) TimeLimitPart = Abc_MinInt ( TimeLimitPart , TimeLimit2 ) ; else TimeLimitPart = TimeLimit2 ; } Ssw_ManSweepBmcFilter ( p , TimeLimitPart ) ; Ssw_SatStop ( p -> pMSat ) ; p -> pMSat = NULL ; Ssw_ManCleanup ( p ) ; Ssw_ManRollForward ( p , p -> pPars -> nFramesK ) ; if ( TimeLimit && Abc_Clock ( ) > nTimeToStop ) { Abc_Print ( 1 , " \n " , TimeLimit ) ; break ; } } Aig_ManSetPhase ( p -> pAig ) ; Aig_ManCleanMarkB ( p -> pAig ) ; pPars -> fVerbose = 0 ; Ssw_ManStop ( p ) ; }
Function
Synopsis    [Filter equivalence classes of nodes.]
Function Synopsis [ Filter equivalence classes of nodes . ]
//, clkTotal = Abc_Clock(); // consider the case of empty AIG // reset random numbers // if parameters are not given, create them //nFramesMax; // start the induction manager // create trivial equivalence classes with all nodes being candidates for constant 1 // compute starting state if needed // refine classes using BMC // start filtering equivalence classes // printout // simulate pattern forward // check timeout // cleanup // cleanup