abc/src/proof/pdr/pdrTsim2.c
/**Function*************************************************************

  Synopsis    [Shrinks values using ternary simulation.]

  Description [The cube contains the set of flop index literals which,
  when converted into a clause and applied to the combinational outputs, 
  led to a satisfiable SAT run in frame k (values stored in the SAT solver).
  If the cube is NULL, it is assumed that the first property output was
  asserted and failed.
  The resulting array is a set of flop index literals that asserts the COs.
  Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Shrinks values using ternary simulation.]

Description [The cube contains the set of flop index literals which,
when converted into a clause and applied to the combinational outputs,
led to a satisfiable SAT run in frame k (values stored in the SAT solver).
If the cube is NULL, it is assumed that the first property output was
asserted and failed.
The resulting array is a set of flop index literals that asserts the COs.
Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]




Function Synopsis [ Shrinks values using ternary simulation . ] Description [ The cube contains the set of flop index literals which when converted into a clause and applied to the combinational outputs led to a satisfiable SAT run in frame k ( values stored in the SAT solver ) . If the cube is NULL it is assumed that the first property output was asserted and failed . The resulting array is a set of flop index literals that asserts the COs . Priority contains 0 for i - th entry if the i - th FF is desirable to remove . ]
Pdr_Set_t * Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube )
{
    int fTryNew = 1;
    Pdr_Set_t * pRes;
    Gia_Obj_t * pObj;
    Vec_IntClear( p->vCoObjs );
    if ( pCube == NULL ) 
    {
        pObj = Gia_ManCo(p->pGia, p->pMan->iOutCur);
        Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
    }
    else 
    {
        int i;
        for ( i = 0; i < pCube->nLits; i++ )
        {
            if ( pCube->Lits[i] == -1 )
                continue;
            pObj = Gia_ManCo(p->pGia, Gia_ManPoNum(p->pGia) + Abc_Lit2Var(pCube->Lits[i]));
            Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
        }
    }
if ( 0 )
{
Abc_Print( 1, "Trying to justify cube " );
if ( pCube )
    Pdr_SetPrint( stdout, pCube, Gia_ManRegNum(p->pGia), NULL );
else
    Abc_Print( 1, "<prop=fail>" );
Abc_Print( 1, " in frame %d.\n", k );
}
    Txs_ManCollectCone( p->pGia, p->vCoObjs, p->vCiObjs, p->vNodes );
    Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
    Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
    Txs_ManForwardPass( p->pGia, p->vPrio, p->vCiObjs, p->vCiVals, p->vNodes, p->vCoObjs, p->vCoVals );
    if ( fTryNew )
        Txs_ManFindCiReduction( p->pGia, p->vPrio, p->vCiObjs, p->vNodes, p->vCoObjs, p->vPiLits, p->vFfLits, p->vTemp );
    else
        Txs_ManBackwardPass( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits );
    Txs_ManVerify( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits, p->vCoObjs, p->vCoVals );
    pRes = Pdr_SetCreate( p->vFfLits, p->vPiLits );
    return pRes;
}
Pdr_Set_t * Txs_ManTernarySim ( Txs_Man_t * p , int k , Pdr_Set_t * pCube ) { int fTryNew = 1 ; Pdr_Set_t * pRes ; Gia_Obj_t * pObj ; Vec_IntClear ( p -> vCoObjs ) ; if ( pCube == NULL ) { pObj = Gia_ManCo ( p -> pGia , p -> pMan -> iOutCur ) ; Vec_IntPush ( p -> vCoObjs , Gia_ObjId ( p -> pGia , pObj ) ) ; } else { int i ; for ( i = 0 ; i < pCube -> nLits ; i ++ ) { if ( pCube -> Lits [ i ] == -1 ) continue ; pObj = Gia_ManCo ( p -> pGia , Gia_ManPoNum ( p -> pGia ) + Abc_Lit2Var ( pCube -> Lits [ i ] ) ) ; Vec_IntPush ( p -> vCoObjs , Gia_ObjId ( p -> pGia , pObj ) ) ; } } if ( 0 ) { Abc_Print ( 1 , " " ) ; if ( pCube ) Pdr_SetPrint ( stdout , pCube , Gia_ManRegNum ( p -> pGia ) , NULL ) ; else Abc_Print ( 1 , " " ) ; Abc_Print ( 1 , " \n " , k ) ; } Txs_ManCollectCone ( p -> pGia , p -> vCoObjs , p -> vCiObjs , p -> vNodes ) ; Pdr_ManCollectValues ( p -> pMan , k , p -> vCiObjs , p -> vCiVals ) ; Pdr_ManCollectValues ( p -> pMan , k , p -> vCoObjs , p -> vCoVals ) ; Txs_ManForwardPass ( p -> pGia , p -> vPrio , p -> vCiObjs , p -> vCiVals , p -> vNodes , p -> vCoObjs , p -> vCoVals ) ; if ( fTryNew ) Txs_ManFindCiReduction ( p -> pGia , p -> vPrio , p -> vCiObjs , p -> vNodes , p -> vCoObjs , p -> vPiLits , p -> vFfLits , p -> vTemp ) ; else Txs_ManBackwardPass ( p -> pGia , p -> vCiObjs , p -> vNodes , p -> vPiLits , p -> vFfLits ) ; Txs_ManVerify ( p -> pGia , p -> vCiObjs , p -> vNodes , p -> vPiLits , p -> vFfLits , p -> vCoObjs , p -> vCoVals ) ; pRes = Pdr_SetCreate ( p -> vFfLits , p -> vPiLits ) ; return pRes ; }
Function
Synopsis    [Shrinks values using ternary simulation.]
Function Synopsis [ Shrinks values using ternary simulation . ]
// collect CO objects // the target is the property output // the target is the cube // collect CI objects // collect values // perform two passes // derive the final set //ZH: Disabled assertion because this invariant doesn't hold with down //because of the join operation which can bring in initial states //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );