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

  Synopsis    [Returns the result of support minimization.]

  Description [Returns internal AIG node that is equal to pFunc under 
  assignment pCond == 1, or NULL if there is no such node. status is 
  -1 if condition is not OR; 
  -2 if cone is too large or no cone; 
  -3 if no support reduction is possible.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Returns the result of support minimization.]

Description [Returns internal AIG node that is equal to pFunc under
assignment pCond == 1, or NULL if there is no such node. status is
1 if condition is not OR;
2 if cone is too large or no cone;
3 if no support reduction is possible.]




Function Synopsis [ Returns the result of support minimization . ] Description [ Returns internal AIG node that is equal to pFunc under assignment pCond == 1 or NULL if there is no such node . status is 1 if condition is not OR ; 2 if cone is too large or no cone ; 3 if no support reduction is possible . ]
Aig_Obj_t * Aig_ManSupportMinimization( Aig_Man_t * p, Aig_Obj_t * pCond, Aig_Obj_t * pFunc, int * pStatus )
{
    int nSuppMax = 16;
    Vec_Ptr_t * vOrGate, * vNodes, * vSupp, * vCofs;
    Aig_Obj_t * pResult;
    int RetValue;
    *pStatus = 0;
    if ( !Aig_IsComplement(pCond) || Aig_ObjIsCi(Aig_Regular(pCond)) || Aig_ObjIsConst1(Aig_Regular(pCond)) )
    {
        *pStatus = -1;
        return NULL;
    }
    if ( !Aig_ObjIsNode(Aig_Regular(pFunc)) )
    {
        *pStatus = -2;
        return NULL;
    }
    vOrGate = Aig_SuppMinCollectSuper( Aig_Regular(pCond) );
    if ( Vec_PtrSize(vOrGate) > nSuppMax )
    {
        Vec_PtrFree( vOrGate );
        *pStatus = -2;
        return NULL;
    }
    RetValue = Aig_SuppMinHighlightCone( p, Aig_Regular(pFunc), vOrGate );
    if ( RetValue == 0 ) 
    {
        Vec_PtrFree( vOrGate );
        *pStatus = -2;
        return NULL;
    }
    vNodes = Aig_SuppMinCollectCone( p, Aig_Regular(pFunc) );
    vSupp = Aig_SuppMinCollectSupport( p, vNodes );
    if ( Vec_PtrSize(vSupp) > nSuppMax )
    {
        Vec_PtrFree( vOrGate );
        Vec_PtrFree( vNodes );
        Vec_PtrFree( vSupp );
        *pStatus = -2;
        return NULL;
    }
    if ( !Aig_SuppMinGateIsInSupport( p, vOrGate, vSupp ) )
    {
        Vec_PtrFree( vOrGate );
        Vec_PtrFree( vNodes );
        Vec_PtrFree( vSupp );
        *pStatus = -3;
        return NULL;
    }
    vCofs = Aig_SuppMinPerform( p, vOrGate, vNodes, vSupp );
    if ( Vec_PtrSize(vCofs) == 0 )
    {
        Vec_PtrFree( vCofs );
        Vec_PtrFree( vOrGate );
        Vec_PtrFree( vNodes );
        Vec_PtrFree( vSupp );
        *pStatus = -3;
        return NULL;
    }
    pResult = Aig_SuppMinReconstruct( p, vCofs, vNodes, vSupp );
    pResult = Aig_NotCond( pResult, Aig_IsComplement(pFunc) );
    Vec_PtrFree( vCofs );
    Vec_PtrFree( vOrGate );
    Vec_PtrFree( vNodes );
    Vec_PtrFree( vSupp );
    return pResult;
}
Aig_Obj_t * Aig_ManSupportMinimization ( Aig_Man_t * p , Aig_Obj_t * pCond , Aig_Obj_t * pFunc , int * pStatus ) { int nSuppMax = 16 ; Vec_Ptr_t * vOrGate , * vNodes , * vSupp , * vCofs ; Aig_Obj_t * pResult ; int RetValue ; * pStatus = 0 ; if ( ! Aig_IsComplement ( pCond ) || Aig_ObjIsCi ( Aig_Regular ( pCond ) ) || Aig_ObjIsConst1 ( Aig_Regular ( pCond ) ) ) { * pStatus = -1 ; return NULL ; } if ( ! Aig_ObjIsNode ( Aig_Regular ( pFunc ) ) ) { * pStatus = -2 ; return NULL ; } vOrGate = Aig_SuppMinCollectSuper ( Aig_Regular ( pCond ) ) ; if ( Vec_PtrSize ( vOrGate ) > nSuppMax ) { Vec_PtrFree ( vOrGate ) ; * pStatus = -2 ; return NULL ; } RetValue = Aig_SuppMinHighlightCone ( p , Aig_Regular ( pFunc ) , vOrGate ) ; if ( RetValue == 0 ) { Vec_PtrFree ( vOrGate ) ; * pStatus = -2 ; return NULL ; } vNodes = Aig_SuppMinCollectCone ( p , Aig_Regular ( pFunc ) ) ; vSupp = Aig_SuppMinCollectSupport ( p , vNodes ) ; if ( Vec_PtrSize ( vSupp ) > nSuppMax ) { Vec_PtrFree ( vOrGate ) ; Vec_PtrFree ( vNodes ) ; Vec_PtrFree ( vSupp ) ; * pStatus = -2 ; return NULL ; } if ( ! Aig_SuppMinGateIsInSupport ( p , vOrGate , vSupp ) ) { Vec_PtrFree ( vOrGate ) ; Vec_PtrFree ( vNodes ) ; Vec_PtrFree ( vSupp ) ; * pStatus = -3 ; return NULL ; } vCofs = Aig_SuppMinPerform ( p , vOrGate , vNodes , vSupp ) ; if ( Vec_PtrSize ( vCofs ) == 0 ) { Vec_PtrFree ( vCofs ) ; Vec_PtrFree ( vOrGate ) ; Vec_PtrFree ( vNodes ) ; Vec_PtrFree ( vSupp ) ; * pStatus = -3 ; return NULL ; } pResult = Aig_SuppMinReconstruct ( p , vCofs , vNodes , vSupp ) ; pResult = Aig_NotCond ( pResult , Aig_IsComplement ( pFunc ) ) ; Vec_PtrFree ( vCofs ) ; Vec_PtrFree ( vOrGate ) ; Vec_PtrFree ( vNodes ) ; Vec_PtrFree ( vSupp ) ; return pResult ; }
Function
Synopsis    [Returns the result of support minimization.]
Function Synopsis [ Returns the result of support minimization . ]
// if pCond is not OR // if pFunc is not a node // collect the multi-input OR gate rooted in the condition // highlight the cone limited by these gates // no overlap // collect the cone rooted in pFunc limited by vOrGate // collect the support nodes reachable from the cone // check if all nodes belonging to OR gate are included in the support // (if this is not the case, don't-care minimization is not possible) // create truth tables of all nodes and find the maximal number // of support varialbles that can be replaced by constants // reconstruct the cone