/**CFile**************************************************************** FileName [covCore.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Mapping into network of SOPs/ESOPs.] Synopsis [Core procedures.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: covCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "cov.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// static void Abc_NtkCovCovers( Cov_Man_t * p, Abc_Ntk_t * pNtk, int fVerbose ); static int Abc_NtkCovCoversOne( Cov_Man_t * p, Abc_Ntk_t * pNtk, int fVerbose ); static void Abc_NtkCovCovers_rec( Cov_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary ); /* static int Abc_NodeCovPropagateEsop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); static int Abc_NodeCovPropagateSop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); static int Abc_NodeCovUnionEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); static int Abc_NodeCovUnionSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); static int Abc_NodeCovProductEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); static int Abc_NodeCovProductSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); */ static int Abc_NodeCovPropagate( Cov_Man_t * p, Abc_Obj_t * pObj ); static Min_Cube_t * Abc_NodeCovProduct( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ); static Min_Cube_t * Abc_NodeCovSum( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Performs decomposition.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Ntk_t * Abc_NtkSopEsopCover( Abc_Ntk_t * pNtk, int nFaninMax, int fUseEsop, int fUseSop, int fUseInvs, int fVerbose ) { Abc_Ntk_t * pNtkNew; Cov_Man_t * p; assert( Abc_NtkIsStrash(pNtk) ); // create the manager p = Cov_ManAlloc( pNtk, nFaninMax ); p->fUseEsop = fUseEsop; p->fUseSop = fUseSop; pNtk->pManCut = p; // perform mapping Abc_NtkCovCovers( p, pNtk, fVerbose ); // derive the final network // if ( fUseInvs ) // pNtkNew = Abc_NtkCovDeriveClean( p, pNtk ); // else // pNtkNew = Abc_NtkCovDerive( p, pNtk ); // pNtkNew = NULL; pNtkNew = Abc_NtkCovDeriveRegular( p, pNtk ); Cov_ManFree( p ); pNtk->pManCut = NULL; // make sure that everything is okay if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkCov: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); return NULL; } return pNtkNew; } /**Function************************************************************* Synopsis [Compute the supports.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkCovCovers( Cov_Man_t * p, Abc_Ntk_t * pNtk, int fVerbose ) { Abc_Obj_t * pObj; int i; abctime clk = Abc_Clock(); // start the manager p->vFanCounts = Abc_NtkFanoutCounts(pNtk); // set trivial cuts for the constant and the CIs pObj = Abc_AigConst1(pNtk); pObj->fMarkA = 1; Abc_NtkForEachCi( pNtk, pObj, i ) pObj->fMarkA = 1; // perform iterative decomposition for ( i = 0; ; i++ ) { if ( fVerbose ) printf( "Iter %d : ", i+1 ); if ( Abc_NtkCovCoversOne(p, pNtk, fVerbose) ) break; } // clean the cut-point markers Abc_NtkForEachObj( pNtk, pObj, i ) pObj->fMarkA = 0; if ( fVerbose ) { ABC_PRT( "Total", Abc_Clock() - clk ); } } /**Function************************************************************* Synopsis [Compute the supports.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NtkCovCoversOne( Cov_Man_t * p, Abc_Ntk_t * pNtk, int fVerbose ) { ProgressBar * pProgress; Abc_Obj_t * pObj; Vec_Ptr_t * vBoundary; int i; abctime clk = Abc_Clock(); int Counter = 0; int fStop = 1; // array to collect the nodes in the new boundary vBoundary = Vec_PtrAlloc( 100 ); // start from the COs and mark visited nodes using pObj->fMarkB pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pObj, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); // skip the solved nodes (including the CIs) pObj = Abc_ObjFanin0(pObj); if ( pObj->fMarkA ) { Counter++; continue; } // traverse the cone starting from this node if ( Abc_ObjGetSupp(pObj) == NULL ) Abc_NtkCovCovers_rec( p, pObj, vBoundary ); // count the number of solved cones if ( Abc_ObjGetSupp(pObj) == NULL ) fStop = 0; else Counter++; /* printf( "%-15s : ", Abc_ObjName(pObj) ); printf( "lev = %5d ", pObj->Level ); if ( Abc_ObjGetSupp(pObj) == NULL ) { printf( "\n" ); continue; } printf( "supp = %3d ", Abc_ObjGetSupp(pObj)->nSize ); printf( "esop = %3d ", Min_CoverCountCubes( Abc_ObjGetCover2(pObj) ) ); printf( "\n" ); */ } Extra_ProgressBarStop( pProgress ); // clean visited nodes Abc_NtkForEachObj( pNtk, pObj, i ) pObj->fMarkB = 0; // create the new boundary p->nBoundary = 0; Vec_PtrForEachEntry( Abc_Obj_t *, vBoundary, pObj, i ) { if ( !pObj->fMarkA ) { pObj->fMarkA = 1; p->nBoundary++; } } Vec_PtrFree( vBoundary ); if ( fVerbose ) { printf( "Outs = %4d (%4d) Node = %6d (%6d) Max = %6d Bound = %4d ", Counter, Abc_NtkCoNum(pNtk), p->nSupps, Abc_NtkNodeNum(pNtk), p->nSuppsMax, p->nBoundary ); ABC_PRT( "T", Abc_Clock() - clk ); } return fStop; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkCovCovers_rec( Cov_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary ) { Abc_Obj_t * pObj0, * pObj1; // return if the support is already computed if ( pObj->fMarkB || pObj->fMarkA )//|| Abc_ObjGetSupp(pObj) ) // why do we need Supp check here??? return; // mark as visited pObj->fMarkB = 1; // get the fanins pObj0 = Abc_ObjFanin0(pObj); pObj1 = Abc_ObjFanin1(pObj); // solve for the fanins Abc_NtkCovCovers_rec( p, pObj0, vBoundary ); Abc_NtkCovCovers_rec( p, pObj1, vBoundary ); // skip the node that spaced out if ( (!pObj0->fMarkA && !Abc_ObjGetSupp(pObj0)) || // fanin is not ready (!pObj1->fMarkA && !Abc_ObjGetSupp(pObj1)) || // fanin is not ready !Abc_NodeCovPropagate( p, pObj ) ) // node's support or covers cannot be computed { // save the nodes of the future boundary if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) ) Vec_PtrPush( vBoundary, pObj0 ); if ( !pObj1->fMarkA && Abc_ObjGetSupp(pObj1) ) Vec_PtrPush( vBoundary, pObj1 ); return; } // consider dropping the fanin supports // Abc_NodeCovDropData( p, pObj0 ); // Abc_NodeCovDropData( p, pObj1 ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Abc_NodeCovSupport( Cov_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1 ) { Vec_Int_t * vSupp; int k0, k1; assert( vSupp0 && vSupp1 ); Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 ); Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 ); Vec_IntClear( p->vPairs0 ); Vec_IntClear( p->vPairs1 ); vSupp = Vec_IntAlloc( vSupp0->nSize + vSupp1->nSize ); for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; ) { if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] ) { Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); Vec_IntPush( p->vPairs0, k0 ); Vec_IntPush( p->vPairs1, k1 ); Vec_IntPush( vSupp, vSupp0->pArray[k0] ); k0++; k1++; } else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] ) { Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); Vec_IntPush( vSupp, vSupp0->pArray[k0] ); k0++; } else { Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); Vec_IntPush( vSupp, vSupp1->pArray[k1] ); k1++; } } for ( ; k0 < vSupp0->nSize; k0++ ) { Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); Vec_IntPush( vSupp, vSupp0->pArray[k0] ); } for ( ; k1 < vSupp1->nSize; k1++ ) { Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); Vec_IntPush( vSupp, vSupp1->pArray[k1] ); } /* printf( "Zero : " ); for ( k0 = 0; k0 < vSupp0->nSize; k0++ ) printf( "%d ", vSupp0->pArray[k0] ); printf( "\n" ); printf( "One : " ); for ( k1 = 0; k1 < vSupp1->nSize; k1++ ) printf( "%d ", vSupp1->pArray[k1] ); printf( "\n" ); printf( "Sum : " ); for ( k0 = 0; k0 < vSupp->nSize; k0++ ) printf( "%d ", vSupp->pArray[k0] ); printf( "\n" ); printf( "\n" ); */ return vSupp; } /**Function************************************************************* Synopsis [Propagates all types of covers.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NodeCovPropagate( Cov_Man_t * p, Abc_Obj_t * pObj ) { Min_Cube_t * pCoverP = NULL, * pCoverN = NULL, * pCoverX = NULL; Min_Cube_t * pCov0, * pCov1, * pCover0, * pCover1; Vec_Int_t * vSupp, * vSupp0, * vSupp1; Abc_Obj_t * pObj0, * pObj1; int fCompl0, fCompl1; pObj0 = Abc_ObjFanin0( pObj ); pObj1 = Abc_ObjFanin1( pObj ); if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); // get the resulting support vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); vSupp = Abc_NodeCovSupport( p, vSupp0, vSupp1 ); // quit if support if too large if ( vSupp->nSize > p->nFaninMax ) { Vec_IntFree( vSupp ); return 0; } // get the complemented attributes fCompl0 = Abc_ObjFaninC0( pObj ); fCompl1 = Abc_ObjFaninC1( pObj ); // propagate ESOP if ( p->fUseEsop ) { // get the covers pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0); pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1); if ( pCov0 && pCov1 ) { // complement the first if needed if ( !fCompl0 ) pCover0 = pCov0; else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube pCover0 = pCov0->pNext; else pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0; // complement the second if needed if ( !fCompl1 ) pCover1 = pCov1; else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube pCover1 = pCov1->pNext; else pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1; // derive the new cover pCoverX = Abc_NodeCovProduct( p, pCover0, pCover1, 1, vSupp->nSize ); } } // propagate SOPs if ( p->fUseSop ) { // get the covers for the direct polarity pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0); pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1); // derive the new cover if ( pCover0 && pCover1 ) pCoverP = Abc_NodeCovProduct( p, pCover0, pCover1, 0, vSupp->nSize ); // get the covers for the inverse polarity pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0); pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1); // derive the new cover if ( pCover0 && pCover1 ) pCoverN = Abc_NodeCovSum( p, pCover0, pCover1, 0, vSupp->nSize ); } // if none of the covers can be computed quit if ( !pCoverX && !pCoverP && !pCoverN ) { Vec_IntFree( vSupp ); return 0; } // set the covers assert( Abc_ObjGetSupp(pObj) == NULL ); Abc_ObjSetSupp( pObj, vSupp ); Abc_ObjSetCover( pObj, pCoverP, 0 ); Abc_ObjSetCover( pObj, pCoverN, 1 ); Abc_ObjSetCover2( pObj, pCoverX ); //printf( "%3d : %4d %4d %4d\n", pObj->Id, Min_CoverCountCubes(pCoverP), Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverX) ); // count statistics p->nSupps++; p->nSuppsMax = Abc_MaxInt( p->nSuppsMax, p->nSupps ); return 1; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Min_Cube_t * Abc_NodeCovProduct( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ) { Min_Cube_t * pCube, * pCube0, * pCube1; Min_Cube_t * pCover; int i, Val0, Val1; assert( pCover0 && pCover1 ); // clean storage Min_ManClean( p->pManMin, nSupp ); // go through the cube pairs Min_CoverForEachCube( pCover0, pCube0 ) Min_CoverForEachCube( pCover1, pCube1 ) { // go through the support variables of the cubes for ( i = 0; i < p->vPairs0->nSize; i++ ) { Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] ); Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] ); if ( (Val0 & Val1) == 0 ) break; } // check disjointness if ( i < p->vPairs0->nSize ) continue; if ( p->pManMin->nCubes > p->nCubesMax ) { pCover = Min_CoverCollect( p->pManMin, nSupp ); //Min_CoverWriteFile( pCover, "large", 1 ); Min_CoverRecycle( p->pManMin, pCover ); return NULL; } // create the product cube pCube = Min_CubeAlloc( p->pManMin ); // add the literals pCube->nLits = 0; for ( i = 0; i < nSupp; i++ ) { if ( p->vComTo0->pArray[i] == -1 ) Val0 = 3; else Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); if ( p->vComTo1->pArray[i] == -1 ) Val1 = 3; else Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); if ( (Val0 & Val1) == 3 ) continue; Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 ); pCube->nLits++; } // add the cube to storage if ( fEsop ) Min_EsopAddCube( p->pManMin, pCube ); else Min_SopAddCube( p->pManMin, pCube ); } // minimize the cover if ( fEsop ) Min_EsopMinimize( p->pManMin ); else Min_SopMinimize( p->pManMin ); pCover = Min_CoverCollect( p->pManMin, nSupp ); // quit if the cover is too large if ( Min_CoverCountCubes(pCover) > p->nFaninMax ) { /* Min_CoverWriteFile( pCover, "large", 1 ); Min_CoverExpand( p->pManMin, pCover ); Min_EsopMinimize( p->pManMin ); Min_EsopMinimize( p->pManMin ); Min_EsopMinimize( p->pManMin ); Min_EsopMinimize( p->pManMin ); Min_EsopMinimize( p->pManMin ); Min_EsopMinimize( p->pManMin ); Min_EsopMinimize( p->pManMin ); Min_EsopMinimize( p->pManMin ); Min_EsopMinimize( p->pManMin ); pCover = Min_CoverCollect( p->pManMin, nSupp ); */ Min_CoverRecycle( p->pManMin, pCover ); return NULL; } return pCover; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Min_Cube_t * Abc_NodeCovSum( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ) { Min_Cube_t * pCube, * pCube0, * pCube1; Min_Cube_t * pCover; int i, Val0, Val1; assert( pCover0 && pCover1 ); // clean storage Min_ManClean( p->pManMin, nSupp ); Min_CoverForEachCube( pCover0, pCube0 ) { // create the cube pCube = Min_CubeAlloc( p->pManMin ); pCube->nLits = 0; for ( i = 0; i < p->vComTo0->nSize; i++ ) { if ( p->vComTo0->pArray[i] == -1 ) continue; Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); if ( Val0 == 3 ) continue; Min_CubeXorVar( pCube, i, Val0 ^ 3 ); pCube->nLits++; } if ( p->pManMin->nCubes > p->nCubesMax ) { pCover = Min_CoverCollect( p->pManMin, nSupp ); Min_CoverRecycle( p->pManMin, pCover ); return NULL; } // add the cube to storage if ( fEsop ) Min_EsopAddCube( p->pManMin, pCube ); else Min_SopAddCube( p->pManMin, pCube ); } Min_CoverForEachCube( pCover1, pCube1 ) { // create the cube pCube = Min_CubeAlloc( p->pManMin ); pCube->nLits = 0; for ( i = 0; i < p->vComTo1->nSize; i++ ) { if ( p->vComTo1->pArray[i] == -1 ) continue; Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); if ( Val1 == 3 ) continue; Min_CubeXorVar( pCube, i, Val1 ^ 3 ); pCube->nLits++; } if ( p->pManMin->nCubes > p->nCubesMax ) { pCover = Min_CoverCollect( p->pManMin, nSupp ); Min_CoverRecycle( p->pManMin, pCover ); return NULL; } // add the cube to storage if ( fEsop ) Min_EsopAddCube( p->pManMin, pCube ); else Min_SopAddCube( p->pManMin, pCube ); } // minimize the cover if ( fEsop ) Min_EsopMinimize( p->pManMin ); else Min_SopMinimize( p->pManMin ); pCover = Min_CoverCollect( p->pManMin, nSupp ); // quit if the cover is too large if ( Min_CoverCountCubes(pCover) > p->nFaninMax ) { Min_CoverRecycle( p->pManMin, pCover ); return NULL; } return pCover; } #if 0 /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NodeCovPropagateEsop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ) { Min_Cube_t * pCover, * pCover0, * pCover1, * pCov0, * pCov1; Vec_Int_t * vSupp, * vSupp0, * vSupp1; if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); // get the resulting support vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); vSupp = Abc_NodeCovSupport( p, vSupp0, vSupp1 ); // quit if support if too large if ( vSupp->nSize > p->nFaninMax ) { Vec_IntFree( vSupp ); return 0; } // get the covers pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0); pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1); // complement the first if needed if ( !Abc_ObjFaninC0(pObj) ) pCover0 = pCov0; else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube pCover0 = pCov0->pNext; else pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0; // complement the second if needed if ( !Abc_ObjFaninC1(pObj) ) pCover1 = pCov1; else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube pCover1 = pCov1->pNext; else pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1; // derive and minimize the cover (quit if too large) if ( !Abc_NodeCovProductEsop( p, pCover0, pCover1, vSupp->nSize ) ) { pCover = Min_CoverCollect( p->pManMin, vSupp->nSize ); Min_CoverRecycle( p->pManMin, pCover ); Vec_IntFree( vSupp ); return 0; } // minimize the cover Min_EsopMinimize( p->pManMin ); pCover = Min_CoverCollect( p->pManMin, vSupp->nSize ); // quit if the cover is too large if ( Min_CoverCountCubes(pCover) > p->nFaninMax ) { Min_CoverRecycle( p->pManMin, pCover ); Vec_IntFree( vSupp ); return 0; } // count statistics p->nSupps++; p->nSuppsMax = Abc_MaxInt( p->nSuppsMax, p->nSupps ); // set the covers assert( Abc_ObjGetSupp(pObj) == NULL ); Abc_ObjSetSupp( pObj, vSupp ); Abc_ObjSetCover2( pObj, pCover ); return 1; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NodeCovPropagateSop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ) { Min_Cube_t * pCoverP, * pCoverN, * pCover0, * pCover1; Vec_Int_t * vSupp, * vSupp0, * vSupp1; int fCompl0, fCompl1; if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); // get the resulting support vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); vSupp = Abc_NodeCovSupport( p, vSupp0, vSupp1 ); // quit if support if too large if ( vSupp->nSize > p->nFaninMax ) { Vec_IntFree( vSupp ); return 0; } // get the complemented attributes fCompl0 = Abc_ObjFaninC0(pObj); fCompl1 = Abc_ObjFaninC1(pObj); // prepare the positive cover pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0); pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1); // derive and minimize the cover (quit if too large) if ( !pCover0 || !pCover1 ) pCoverP = NULL; else if ( !Abc_NodeCovProductSop( p, pCover0, pCover1, vSupp->nSize ) ) { pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize ); Min_CoverRecycle( p->pManMin, pCoverP ); pCoverP = NULL; } else { Min_SopMinimize( p->pManMin ); pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize ); // quit if the cover is too large if ( Min_CoverCountCubes(pCoverP) > p->nFaninMax ) { Min_CoverRecycle( p->pManMin, pCoverP ); pCoverP = NULL; } } // prepare the negative cover pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0); pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1); // derive and minimize the cover (quit if too large) if ( !pCover0 || !pCover1 ) pCoverN = NULL; else if ( !Abc_NodeCovUnionSop( p, pCover0, pCover1, vSupp->nSize ) ) { pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize ); Min_CoverRecycle( p->pManMin, pCoverN ); pCoverN = NULL; } else { Min_SopMinimize( p->pManMin ); pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize ); // quit if the cover is too large if ( Min_CoverCountCubes(pCoverN) > p->nFaninMax ) { Min_CoverRecycle( p->pManMin, pCoverN ); pCoverN = NULL; } } if ( pCoverP == NULL && pCoverN == NULL ) { Vec_IntFree( vSupp ); return 0; } // count statistics p->nSupps++; p->nSuppsMax = Abc_MaxInt( p->nSuppsMax, p->nSupps ); // set the covers assert( Abc_ObjGetSupp(pObj) == NULL ); Abc_ObjSetSupp( pObj, vSupp ); Abc_ObjSetCover( pObj, pCoverP, 0 ); Abc_ObjSetCover( pObj, pCoverN, 1 ); return 1; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NodeCovProductEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) { Min_Cube_t * pCube, * pCube0, * pCube1; int i, Val0, Val1; // clean storage Min_ManClean( p->pManMin, nSupp ); if ( pCover0 == NULL || pCover1 == NULL ) return 1; // go through the cube pairs Min_CoverForEachCube( pCover0, pCube0 ) Min_CoverForEachCube( pCover1, pCube1 ) { // go through the support variables of the cubes for ( i = 0; i < p->vPairs0->nSize; i++ ) { Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] ); Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] ); if ( (Val0 & Val1) == 0 ) break; } // check disjointness if ( i < p->vPairs0->nSize ) continue; if ( p->pManMin->nCubes >= p->nCubesMax ) return 0; // create the product cube pCube = Min_CubeAlloc( p->pManMin ); // add the literals pCube->nLits = 0; for ( i = 0; i < nSupp; i++ ) { if ( p->vComTo0->pArray[i] == -1 ) Val0 = 3; else Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); if ( p->vComTo1->pArray[i] == -1 ) Val1 = 3; else Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); if ( (Val0 & Val1) == 3 ) continue; Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 ); pCube->nLits++; } // add the cube to storage Min_EsopAddCube( p->pManMin, pCube ); } return 1; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NodeCovProductSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) { return 1; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NodeCovUnionEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) { Min_Cube_t * pCube, * pCube0, * pCube1; int i, Val0, Val1; // clean storage Min_ManClean( p->pManMin, nSupp ); if ( pCover0 ) { Min_CoverForEachCube( pCover0, pCube0 ) { // create the cube pCube = Min_CubeAlloc( p->pManMin ); pCube->nLits = 0; for ( i = 0; i < p->vComTo0->nSize; i++ ) { if ( p->vComTo0->pArray[i] == -1 ) continue; Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); if ( Val0 == 3 ) continue; Min_CubeXorVar( pCube, i, Val0 ^ 3 ); pCube->nLits++; } if ( p->pManMin->nCubes >= p->nCubesMax ) return 0; // add the cube to storage Min_EsopAddCube( p->pManMin, pCube ); } } if ( pCover1 ) { Min_CoverForEachCube( pCover1, pCube1 ) { // create the cube pCube = Min_CubeAlloc( p->pManMin ); pCube->nLits = 0; for ( i = 0; i < p->vComTo1->nSize; i++ ) { if ( p->vComTo1->pArray[i] == -1 ) continue; Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); if ( Val1 == 3 ) continue; Min_CubeXorVar( pCube, i, Val1 ^ 3 ); pCube->nLits++; } if ( p->pManMin->nCubes >= p->nCubesMax ) return 0; // add the cube to storage Min_EsopAddCube( p->pManMin, pCube ); } } return 1; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NodeCovUnionSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) { return 1; } #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END