abc/src/aig/aig/aigUtil.c
/**Function*************************************************************

  Synopsis    [Starts the process of retuning values for internal nodes.]

  Description [Should be called when pCex is available, before probing 
  any object for its value using Aig_ManCounterExampleValueLookup().]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Starts the process of retuning values for internal nodes.]

Description [Should be called when pCex is available, before probing
any object for its value using Aig_ManCounterExampleValueLookup().]




Function Synopsis [ Starts the process of retuning values for internal nodes . ] Description [ Should be called when pCex is available before probing any object for its value using Aig_ManCounterExampleValueLookup () . ]
void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex )
{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int Val0, Val1, nObjs, i, k, iBit = 0;
    assert( Aig_ManRegNum(pAig) > 0 ); 
    assert( pAig->pData2 == NULL );    
    pAig->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNumMax(pAig) ) );
    Saig_ManForEachLo( pAig, pObj, k )
        assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 );
    nObjs = Aig_ManObjNumMax(pAig);
    for ( i = 0; i <= pCex->iFrame; i++ )
    {
        Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + 0 );
        Saig_ManForEachPi( pAig, pObj, k )
            if ( Abc_InfoHasBit(pCex->pData, iBit++) )
                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
        Aig_ManForEachNode( pAig, pObj, k )
        {
            Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
            Val1 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
            if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) )
                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
        }
        Aig_ManForEachCo( pAig, pObj, k )
        {
            Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
            if ( Val0 ^ Aig_ObjFaninC0(pObj) )
                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
        }
        if ( i == pCex->iFrame )
            continue;
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            if ( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
    }
    assert( iBit == pCex->nBits );
    assert( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManCo(pAig, pCex->iPo)) ) );
}
void Aig_ManCounterExampleValueStart ( Aig_Man_t * pAig , Abc_Cex_t * pCex ) { Aig_Obj_t * pObj , * pObjRi , * pObjRo ; int Val0 , Val1 , nObjs , i , k , iBit = 0 ; assert ( Aig_ManRegNum ( pAig ) > 0 ) ; assert ( pAig -> pData2 == NULL ) ; pAig -> pData2 = ABC_CALLOC ( unsigned , Abc_BitWordNum ( ( pCex -> iFrame + 1 ) * Aig_ManObjNumMax ( pAig ) ) ) ; Saig_ManForEachLo ( pAig , pObj , k ) assert ( Abc_InfoHasBit ( pCex -> pData , iBit ++ ) == 0 ) ; nObjs = Aig_ManObjNumMax ( pAig ) ; for ( i = 0 ; i <= pCex -> iFrame ; i ++ ) { Abc_InfoSetBit ( ( unsigned * ) pAig -> pData2 , nObjs * i + 0 ) ; Saig_ManForEachPi ( pAig , pObj , k ) if ( Abc_InfoHasBit ( pCex -> pData , iBit ++ ) ) Abc_InfoSetBit ( ( unsigned * ) pAig -> pData2 , nObjs * i + Aig_ObjId ( pObj ) ) ; Aig_ManForEachNode ( pAig , pObj , k ) { Val0 = Abc_InfoHasBit ( ( unsigned * ) pAig -> pData2 , nObjs * i + Aig_ObjFaninId0 ( pObj ) ) ; Val1 = Abc_InfoHasBit ( ( unsigned * ) pAig -> pData2 , nObjs * i + Aig_ObjFaninId1 ( pObj ) ) ; if ( ( Val0 ^ Aig_ObjFaninC0 ( pObj ) ) & ( Val1 ^ Aig_ObjFaninC1 ( pObj ) ) ) Abc_InfoSetBit ( ( unsigned * ) pAig -> pData2 , nObjs * i + Aig_ObjId ( pObj ) ) ; } Aig_ManForEachCo ( pAig , pObj , k ) { Val0 = Abc_InfoHasBit ( ( unsigned * ) pAig -> pData2 , nObjs * i + Aig_ObjFaninId0 ( pObj ) ) ; if ( Val0 ^ Aig_ObjFaninC0 ( pObj ) ) Abc_InfoSetBit ( ( unsigned * ) pAig -> pData2 , nObjs * i + Aig_ObjId ( pObj ) ) ; } if ( i == pCex -> iFrame ) continue ; Saig_ManForEachLiLo ( pAig , pObjRi , pObjRo , k ) if ( Abc_InfoHasBit ( ( unsigned * ) pAig -> pData2 , nObjs * i + Aig_ObjId ( pObjRi ) ) ) Abc_InfoSetBit ( ( unsigned * ) pAig -> pData2 , nObjs * ( i + 1 ) + Aig_ObjId ( pObjRo ) ) ; } assert ( iBit == pCex -> nBits ) ; assert ( Abc_InfoHasBit ( ( unsigned * ) pAig -> pData2 , nObjs * pCex -> iFrame + Aig_ObjId ( Aig_ManCo ( pAig , pCex -> iPo ) ) ) ) ; }
Function
Synopsis    [Starts the process of retuning values for internal nodes.]
Function Synopsis [ Starts the process of retuning values for internal nodes . ]
// makes sense only for sequential AIGs // if this fail, there may be a memory leak // allocate memory to store simulation bits for internal nodes // the register values in the counter-example should be zero // iterate through the timeframes // set constant 1 node // set primary inputs according to the counter-example // compute values for each node // derive values for combinational outputs // transfer values to the register output of the next frame // check that the counter-example is correct, that is, the corresponding output is asserted