abc/src/aig/saig/saigGlaCba.c
/**Function*************************************************************

  Synopsis    [Performs gate-level localization abstraction.]

  Description [Returns array of objects included in the abstraction. This array
  may contain only const1, flop outputs, and internal nodes, that is, objects
  that should have clauses added to the SAT solver.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Performs gate-level localization abstraction.]

Description [Returns array of objects included in the abstraction. This array
may contain only const1, flop outputs, and internal nodes, that is, objects
that should have clauses added to the SAT solver.]




Function Synopsis [ Performs gate - level localization abstraction . ] Description [ Returns array of objects included in the abstraction . This array may contain only const1 flop outputs and internal nodes that is objects that should have clauses added to the SAT solver . ]
Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose, int * piFrame )
{
    Vec_Int_t * vResult = NULL;
    Aig_Gla1Man_t * p;
    Aig_Man_t * pAbs;
    Aig_Obj_t * pObj;
    Abc_Cex_t * pCex;
    Vec_Int_t * vPPiRefine;
    int f, g, r, i, iSatVar, Lit, Entry, RetValue;
    int nConfBef, nConfAft;
    clock_t clk, clkTotal = clock();
    clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
    assert( Saig_ManPoNum(pAig) == 1 );
    if ( nFramesMax == 0 )
        nFramesMax = ABC_INFINITY;
    if ( fVerbose )
    {
        if ( TimeLimit )
            printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit );
        else
            printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax );
    }
    p = Aig_Gla1ManStart( pAig, vGateClassesOld, fNaiveCnf );
    p->nFramesMax = nFramesMax;
    p->nConfLimit = nConfLimit;
    p->fVerbose   = fVerbose;
    Vec_IntWriteEntry( p->vIncluded, 0, 1 );
    Aig_Gla1FetchVecId( p, Aig_ManConst1(pAig) );
    if ( TimeLimit )
        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
    for ( f = 0; f < nFramesMax; f++ )
    {
        Aig_ManForEachObjVec( p->vAssigned, pAig, pObj, i )
            if ( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) )
                if ( !Aig_Gla1ObjAddToSolver( p, pObj, f ) )
                    printf( "Error!  SAT solver became UNSAT.\n" );
        if ( f < nStart )
            continue;
        pObj    = Aig_ManCo( pAig, 0 );
        iSatVar = Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObj), f );
        Lit     = toLitCond( iSatVar, Aig_ObjFaninC0(pObj) );
        Aig_Gla1CollectAbstr( p );
        for ( r = 0; r < ABC_INFINITY; r++ )
        {
            clk = clock();
            nConfBef = p->pSat->stats.conflicts;
            RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, 
                (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
            nConfAft = p->pSat->stats.conflicts;
            p->timeSat += clock() - clk;
            if ( RetValue != l_True )
            {
                if ( fVerbose )
                {
                    if ( r == 0 )
                        printf( "== %3d ==", f );
                    else
                        printf( "         " );
                    if ( TimeLimit && clock() > nTimeToStop )
                        printf( "       SAT solver timed out after %d seconds.\n", TimeLimit );
                    else if ( RetValue != l_False )
                        printf( "       SAT solver returned UNDECIDED after %5d conflicts.\n", nConfAft - nConfBef );
                    else
                    {
                        printf( "       SAT solver returned UNSAT after %5d conflicts.  ", nConfAft - nConfBef );
                        Abc_PrintTime( 1, "Total time", clock() - clkTotal );
                    }
                }
                break;
            }
            clk = clock();
            pAbs = Aig_Gla1DeriveAbs( p );
            pCex = Aig_Gla1DeriveCex( p, f );
            RetValue = Saig_ManVerifyCex( pAbs, pCex );
            if ( RetValue == 0 )
                printf( "Error!  CEX is invalid.\n" );
            vPPiRefine = Saig_ManCbaFilterInputs( pAbs, Vec_IntSize(p->vPis), pCex, 0 );
            Vec_IntForEachEntry( vPPiRefine, Entry, i )
            {
                pObj = Aig_ManObj( pAig, Vec_IntEntry(p->vPPis, Entry) );
                assert( Aig_ObjIsNode(pObj) || Saig_ObjIsLo(p->pAig, pObj) );
                assert( Vec_IntEntry( p->vIncluded, Aig_ObjId(pObj) ) == 0 );
                Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 );
                for ( g = 0; g <= f; g++ )
                    if ( !Aig_Gla1ObjAddToSolver( p, pObj, g ) )
                        printf( "Error!  SAT solver became UNSAT.\n" );
            }
            if ( Vec_IntSize(vPPiRefine) == 0 )
            {
                Vec_IntFreeP( &p->vIncluded );
                Vec_IntFree( vPPiRefine );
                Aig_ManStop( pAbs );
                Abc_CexFree( pCex );
                break;
            }
            Vec_IntFree( vPPiRefine );
            Aig_ManStop( pAbs );
            Abc_CexFree( pCex );
            p->timeRef += clock() - clk;
            Aig_Gla1CollectAbstr( p );
            if ( fVerbose )
                Aig_Gla1PrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef );
        }
        if ( RetValue != l_False )
            break;
    }
    p->timeTotal = clock() - clkTotal;
    if ( f == nFramesMax )
        printf( "Finished %d frames without exceeding conflict limit (%d).\n", f, nConfLimit );
    else if ( p->vIncluded == NULL )
        printf( "The problem is SAT in frame %d. The CEX is currently not produced.\n", f );
    else
        printf( "Ran out of conflict limit (%d) at frame %d.\n", nConfLimit, f );
    *piFrame = f;
    if ( fVerbose )
    {
        ABC_PRTP( "Sat   ", p->timeSat,   p->timeTotal );
        ABC_PRTP( "Ref   ", p->timeRef,   p->timeTotal );
        ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
    }
    if ( !fNaiveCnf && p->vIncluded )
        Aig_Gla1ExtendIncluded( p );
    vResult = p->vIncluded;  p->vIncluded = NULL;
    Aig_Gla1ManStop( p );
    return vResult;
}
Vec_Int_t * Aig_Gla1ManPerform ( Aig_Man_t * pAig , Vec_Int_t * vGateClassesOld , int nStart , int nFramesMax , int nConfLimit , int TimeLimit , int fNaiveCnf , int fVerbose , int * piFrame ) { Vec_Int_t * vResult = NULL ; Aig_Gla1Man_t * p ; Aig_Man_t * pAbs ; Aig_Obj_t * pObj ; Abc_Cex_t * pCex ; Vec_Int_t * vPPiRefine ; int f , g , r , i , iSatVar , Lit , Entry , RetValue ; int nConfBef , nConfAft ; clock_t clk , clkTotal = clock ( ) ; clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock ( ) : 0 ; assert ( Saig_ManPoNum ( pAig ) == 1 ) ; if ( nFramesMax == 0 ) nFramesMax = ABC_INFINITY ; if ( fVerbose ) { if ( TimeLimit ) printf ( " \n " , nStart , nFramesMax , TimeLimit ) ; else printf ( " \n " , nStart , nFramesMax ) ; } p = Aig_Gla1ManStart ( pAig , vGateClassesOld , fNaiveCnf ) ; p -> nFramesMax = nFramesMax ; p -> nConfLimit = nConfLimit ; p -> fVerbose = fVerbose ; Vec_IntWriteEntry ( p -> vIncluded , 0 , 1 ) ; Aig_Gla1FetchVecId ( p , Aig_ManConst1 ( pAig ) ) ; if ( TimeLimit ) sat_solver_set_runtime_limit ( p -> pSat , nTimeToStop ) ; for ( f = 0 ; f < nFramesMax ; f ++ ) { Aig_ManForEachObjVec ( p -> vAssigned , pAig , pObj , i ) if ( Vec_IntEntry ( p -> vIncluded , Aig_ObjId ( pObj ) ) ) if ( ! Aig_Gla1ObjAddToSolver ( p , pObj , f ) ) printf ( " \n " ) ; if ( f < nStart ) continue ; pObj = Aig_ManCo ( pAig , 0 ) ; iSatVar = Aig_Gla1FetchVar ( p , Aig_ObjFanin0 ( pObj ) , f ) ; Lit = toLitCond ( iSatVar , Aig_ObjFaninC0 ( pObj ) ) ; Aig_Gla1CollectAbstr ( p ) ; for ( r = 0 ; r < ABC_INFINITY ; r ++ ) { clk = clock ( ) ; nConfBef = p -> pSat -> stats . conflicts ; RetValue = sat_solver_solve ( p -> pSat , & Lit , & Lit + 1 , ( ABC_INT64_T ) nConfLimit , ( ABC_INT64_T ) 0 , ( ABC_INT64_T ) 0 , ( ABC_INT64_T ) 0 ) ; nConfAft = p -> pSat -> stats . conflicts ; p -> timeSat += clock ( ) - clk ; if ( RetValue != l_True ) { if ( fVerbose ) { if ( r == 0 ) printf ( " " , f ) ; else printf ( " " ) ; if ( TimeLimit && clock ( ) > nTimeToStop ) printf ( " \n " , TimeLimit ) ; else if ( RetValue != l_False ) printf ( " \n " , nConfAft - nConfBef ) ; else { printf ( " " , nConfAft - nConfBef ) ; Abc_PrintTime ( 1 , " " , clock ( ) - clkTotal ) ; } } break ; } clk = clock ( ) ; pAbs = Aig_Gla1DeriveAbs ( p ) ; pCex = Aig_Gla1DeriveCex ( p , f ) ; RetValue = Saig_ManVerifyCex ( pAbs , pCex ) ; if ( RetValue == 0 ) printf ( " \n " ) ; vPPiRefine = Saig_ManCbaFilterInputs ( pAbs , Vec_IntSize ( p -> vPis ) , pCex , 0 ) ; Vec_IntForEachEntry ( vPPiRefine , Entry , i ) { pObj = Aig_ManObj ( pAig , Vec_IntEntry ( p -> vPPis , Entry ) ) ; assert ( Aig_ObjIsNode ( pObj ) || Saig_ObjIsLo ( p -> pAig , pObj ) ) ; assert ( Vec_IntEntry ( p -> vIncluded , Aig_ObjId ( pObj ) ) == 0 ) ; Vec_IntWriteEntry ( p -> vIncluded , Aig_ObjId ( pObj ) , 1 ) ; for ( g = 0 ; g <= f ; g ++ ) if ( ! Aig_Gla1ObjAddToSolver ( p , pObj , g ) ) printf ( " \n " ) ; } if ( Vec_IntSize ( vPPiRefine ) == 0 ) { Vec_IntFreeP ( & p -> vIncluded ) ; Vec_IntFree ( vPPiRefine ) ; Aig_ManStop ( pAbs ) ; Abc_CexFree ( pCex ) ; break ; } Vec_IntFree ( vPPiRefine ) ; Aig_ManStop ( pAbs ) ; Abc_CexFree ( pCex ) ; p -> timeRef += clock ( ) - clk ; Aig_Gla1CollectAbstr ( p ) ; if ( fVerbose ) Aig_Gla1PrintAbstr ( p , f , r , p -> pSat -> size , nConfAft - nConfBef ) ; } if ( RetValue != l_False ) break ; } p -> timeTotal = clock ( ) - clkTotal ; if ( f == nFramesMax ) printf ( " \n " , f , nConfLimit ) ; else if ( p -> vIncluded == NULL ) printf ( " \n " , f ) ; else printf ( " \n " , nConfLimit , f ) ; * piFrame = f ; if ( fVerbose ) { ABC_PRTP ( " " , p -> timeSat , p -> timeTotal ) ; ABC_PRTP ( " " , p -> timeRef , p -> timeTotal ) ; ABC_PRTP ( " " , p -> timeTotal , p -> timeTotal ) ; } if ( ! fNaiveCnf && p -> vIncluded ) Aig_Gla1ExtendIncluded ( p ) ; vResult = p -> vIncluded ; p -> vIncluded = NULL ; Aig_Gla1ManStop ( p ) ; return vResult ; }
Function
Synopsis    [Performs gate-level localization abstraction.]
Function Synopsis [ Performs gate - level localization abstraction . ]
// start the solver // include constant node // set runtime limit // iterate over the timeframes // initialize abstraction in this timeframe // skip checking if we are not supposed to // create output literal to represent property failure // try solving the abstraction // try to find a counter-example // derive abstraction // derive counter-example // verify the counter-example // perform refinement // prepare abstraction // print stats // prepare return value