diff options
Diffstat (limited to 'src/temp/xyz')
-rw-r--r-- | src/temp/xyz/module.make | 8 | ||||
-rw-r--r-- | src/temp/xyz/xyz.h | 110 | ||||
-rw-r--r-- | src/temp/xyz/xyzBuild.c | 379 | ||||
-rw-r--r-- | src/temp/xyz/xyzCore.c | 1025 | ||||
-rw-r--r-- | src/temp/xyz/xyzInt.h | 642 | ||||
-rw-r--r-- | src/temp/xyz/xyzMan.c | 144 | ||||
-rw-r--r-- | src/temp/xyz/xyzMinEsop.c | 299 | ||||
-rw-r--r-- | src/temp/xyz/xyzMinMan.c | 113 | ||||
-rw-r--r-- | src/temp/xyz/xyzMinSop.c | 615 | ||||
-rw-r--r-- | src/temp/xyz/xyzMinUtil.c | 277 | ||||
-rw-r--r-- | src/temp/xyz/xyzTest.c | 417 |
11 files changed, 0 insertions, 4029 deletions
diff --git a/src/temp/xyz/module.make b/src/temp/xyz/module.make deleted file mode 100644 index f84fa8cc..00000000 --- a/src/temp/xyz/module.make +++ /dev/null @@ -1,8 +0,0 @@ -SRC += src/temp/xyz/xyzBuild.c \ - src/temp/xyz/xyzCore.c \ - src/temp/xyz/xyzMan.c \ - src/temp/xyz/xyzMinEsop.c \ - src/temp/xyz/xyzMinMan.c \ - src/temp/xyz/xyzMinSop.c \ - src/temp/xyz/xyzMinUtil.c \ - src/temp/xyz/xyzTest.c diff --git a/src/temp/xyz/xyz.h b/src/temp/xyz/xyz.h deleted file mode 100644 index 4fec2150..00000000 --- a/src/temp/xyz/xyz.h +++ /dev/null @@ -1,110 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyz.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [External declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyz.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __XYZ_H__ -#define __XYZ_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -#include "abc.h" -#include "xyzInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Xyz_Man_t_ Xyz_Man_t; -typedef struct Xyz_Obj_t_ Xyz_Obj_t; - -// storage for node information -struct Xyz_Obj_t_ -{ - Min_Cube_t * pCover[3]; // pos/neg/esop - Vec_Int_t * vSupp; // computed support (all nodes except CIs) -}; - -// storage for additional information -struct Xyz_Man_t_ -{ - // general characteristics - int nFaninMax; // the number of vars - int nCubesMax; // the limit on the number of cubes in the intermediate covers - int nWords; // the number of words - Vec_Int_t * vFanCounts; // fanout counts - Vec_Ptr_t * vObjStrs; // object structures - void * pMemory; // memory for the internal data strctures - Min_Man_t * pManMin; // the cub manager - int fUseEsop; // enables ESOPs - int fUseSop; // enables SOPs - // arrays to map local variables - Vec_Int_t * vComTo0; // mapping of common variables into first fanin - Vec_Int_t * vComTo1; // mapping of common variables into second fanin - Vec_Int_t * vPairs0; // the first var in each pair of common vars - Vec_Int_t * vPairs1; // the second var in each pair of common vars - Vec_Int_t * vTriv0; // trival support of the first node - Vec_Int_t * vTriv1; // trival support of the second node - // statistics - int nSupps; // supports created - int nSuppsMax; // the maximum number of supports - int nBoundary; // the boundary size - int nNodes; // the number of nodes processed -}; - -static inline Xyz_Obj_t * Abc_ObjGetStr( Abc_Obj_t * pObj ) { return Vec_PtrEntry(((Xyz_Man_t *)pObj->pNtk->pManCut)->vObjStrs, pObj->Id); } - -static inline void Abc_ObjSetSupp( Abc_Obj_t * pObj, Vec_Int_t * vVec ) { Abc_ObjGetStr(pObj)->vSupp = vVec; } -static inline Vec_Int_t * Abc_ObjGetSupp( Abc_Obj_t * pObj ) { return Abc_ObjGetStr(pObj)->vSupp; } - -static inline void Abc_ObjSetCover2( Abc_Obj_t * pObj, Min_Cube_t * pCov ) { Abc_ObjGetStr(pObj)->pCover[2] = pCov; } -static inline Min_Cube_t * Abc_ObjGetCover2( Abc_Obj_t * pObj ) { return Abc_ObjGetStr(pObj)->pCover[2]; } - -static inline void Abc_ObjSetCover( Abc_Obj_t * pObj, Min_Cube_t * pCov, int Pol ) { Abc_ObjGetStr(pObj)->pCover[Pol] = pCov; } -static inline Min_Cube_t * Abc_ObjGetCover( Abc_Obj_t * pObj, int Pol ) { return Abc_ObjGetStr(pObj)->pCover[Pol]; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== xyzBuild.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk ); -/*=== xyzCore.c ===========================================================*/ -extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose ); -/*=== xyzMan.c ============================================================*/ -extern Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax ); -extern void Xyz_ManFree( Xyz_Man_t * p ); -extern void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj ); -/*=== xyzTest.c ===========================================================*/ -extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk ); - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - - diff --git a/src/temp/xyz/xyzBuild.c b/src/temp/xyz/xyzBuild.c deleted file mode 100644 index e32721e7..00000000 --- a/src/temp/xyz/xyzBuild.c +++ /dev/null @@ -1,379 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyzBuild.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [Network construction procedures.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyzBuild.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "xyz.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Derives the decomposed network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Abc_NtkXyzDeriveCube( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp ) -{ - Vec_Int_t * vLits; - Abc_Obj_t * pNodeNew, * pFanin; - int i, iFanin, Lit; - // create empty cube - if ( pCube->nLits == 0 ) - return Abc_NodeCreateConst1(pNtkNew); - // get the literals of this cube - vLits = Vec_IntAlloc( 10 ); - Min_CubeGetLits( pCube, vLits ); - assert( pCube->nLits == (unsigned)vLits->nSize ); - // create special case when there is only one literal - if ( pCube->nLits == 1 ) - { - iFanin = Vec_IntEntry(vLits,0); - pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); - Lit = Min_CubeGetVar(pCube, iFanin); - assert( Lit == 1 || Lit == 2 ); - Vec_IntFree( vLits ); - if ( Lit == 1 )// negative - return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy ); - return pFanin->pCopy; - } - assert( pCube->nLits > 1 ); - // create the AND cube - pNodeNew = Abc_NtkCreateNode( pNtkNew ); - for ( i = 0; i < vLits->nSize; i++ ) - { - iFanin = Vec_IntEntry(vLits,i); - pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); - Lit = Min_CubeGetVar(pCube, iFanin); - assert( Lit == 1 || Lit == 2 ); - Vec_IntWriteEntry( vLits, i, Lit==1 ); - Abc_ObjAddFanin( pNodeNew, pFanin->pCopy ); - } - pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray ); - Vec_IntFree( vLits ); - return pNodeNew; -} - -/**Function************************************************************* - - Synopsis [Derives the decomposed network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Abc_NtkXyzDeriveNode_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int Level ) -{ - Min_Cube_t * pCover, * pCube; - Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin; - Vec_Int_t * vSupp; - int Entry, nCubes, i; - - if ( Abc_ObjIsCi(pObj) ) - return pObj->pCopy; - assert( Abc_ObjIsNode(pObj) ); - // skip if already computed - if ( pObj->pCopy ) - return pObj->pCopy; - - // get the support and the cover - vSupp = Abc_ObjGetSupp( pObj ); - pCover = Abc_ObjGetCover2( pObj ); - assert( vSupp ); -/* - if ( pCover && pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) > 0 ) - { - printf( "%d\n ", pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) ); - Min_CoverWrite( stdout, pCover ); - } -*/ -/* - // print the support of this node - printf( "{ " ); - Vec_IntForEachEntry( vSupp, Entry, i ) - printf( "%d ", Entry ); - printf( "} cubes = %d\n", Min_CoverCountCubes( pCover ) ); -*/ - // process the fanins - Vec_IntForEachEntry( vSupp, Entry, i ) - { - pFanin = Abc_NtkObj(pObj->pNtk, Entry); - Abc_NtkXyzDeriveNode_rec( p, pNtkNew, pFanin, Level+1 ); - } - - // for each cube, construct the node - nCubes = Min_CoverCountCubes( pCover ); - if ( nCubes == 0 ) - pNodeNew = Abc_NodeCreateConst0(pNtkNew); - else if ( nCubes == 1 ) - pNodeNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCover, vSupp ); - else - { - pNodeNew = Abc_NtkCreateNode( pNtkNew ); - Min_CoverForEachCube( pCover, pCube ) - { - pFaninNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCube, vSupp ); - Abc_ObjAddFanin( pNodeNew, pFaninNew ); - } - pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes ); - } -/* - printf( "Created node %d(%d) at level %d: ", pNodeNew->Id, pObj->Id, Level ); - Vec_IntForEachEntry( vSupp, Entry, i ) - { - pFanin = Abc_NtkObj(pObj->pNtk, Entry); - printf( "%d(%d) ", pFanin->pCopy->Id, pFanin->Id ); - } - printf( "\n" ); - Min_CoverWrite( stdout, pCover ); -*/ - pObj->pCopy = pNodeNew; - return pNodeNew; -} - -/**Function************************************************************* - - Synopsis [Derives the decomposed network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj; - int i; - assert( Abc_NtkIsStrash(pNtk) ); - // perform strashing - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); - // reconstruct the network - Abc_NtkForEachCo( pNtk, pObj, i ) - { - Abc_NtkXyzDeriveNode_rec( p, pNtkNew, Abc_ObjFanin0(pObj), 0 ); -// printf( "*** CO %s : %d -> %d \n", Abc_ObjName(pObj), pObj->pCopy->Id, Abc_ObjFanin0(pObj)->pCopy->Id ); - } - // add the COs - Abc_NtkFinalize( pNtk, pNtkNew ); - Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); - // make sure everything is okay - if ( !Abc_NtkCheck( pNtkNew ) ) - { - printf( "Abc_NtkXyzDerive: The network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - return pNtkNew; -} - - - - -/**Function************************************************************* - - Synopsis [Derives the decomposed network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Abc_NtkXyzDeriveInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl ) -{ - assert( pObj->pCopy ); - if ( !fCompl ) - return pObj->pCopy; - if ( pObj->pCopy->pCopy == NULL ) - pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy ); - return pObj->pCopy->pCopy; - } - -/**Function************************************************************* - - Synopsis [Derives the decomposed network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Abc_NtkXyzDeriveCubeInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp ) -{ - Vec_Int_t * vLits; - Abc_Obj_t * pNodeNew, * pFanin; - int i, iFanin, Lit; - // create empty cube - if ( pCube->nLits == 0 ) - return Abc_NodeCreateConst1(pNtkNew); - // get the literals of this cube - vLits = Vec_IntAlloc( 10 ); - Min_CubeGetLits( pCube, vLits ); - assert( pCube->nLits == (unsigned)vLits->nSize ); - // create special case when there is only one literal - if ( pCube->nLits == 1 ) - { - iFanin = Vec_IntEntry(vLits,0); - pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); - Lit = Min_CubeGetVar(pCube, iFanin); - assert( Lit == 1 || Lit == 2 ); - Vec_IntFree( vLits ); -// if ( Lit == 1 )// negative -// return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy ); -// return pFanin->pCopy; - return Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 ); - } - assert( pCube->nLits > 1 ); - // create the AND cube - pNodeNew = Abc_NtkCreateNode( pNtkNew ); - for ( i = 0; i < vLits->nSize; i++ ) - { - iFanin = Vec_IntEntry(vLits,i); - pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); - Lit = Min_CubeGetVar(pCube, iFanin); - assert( Lit == 1 || Lit == 2 ); - Vec_IntWriteEntry( vLits, i, Lit==1 ); -// Abc_ObjAddFanin( pNodeNew, pFanin->pCopy ); - Abc_ObjAddFanin( pNodeNew, Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 ) ); - } -// pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray ); - pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, NULL ); - Vec_IntFree( vLits ); - return pNodeNew; -} - -/**Function************************************************************* - - Synopsis [Derives the decomposed network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Abc_NtkXyzDeriveNodeInv_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl ) -{ - Min_Cube_t * pCover, * pCube; - Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin; - Vec_Int_t * vSupp; - int Entry, nCubes, i; - - // skip if already computed - if ( pObj->pCopy ) - return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl ); - assert( Abc_ObjIsNode(pObj) ); - - // get the support and the cover - vSupp = Abc_ObjGetSupp( pObj ); - pCover = Abc_ObjGetCover2( pObj ); - assert( vSupp ); - - // process the fanins - Vec_IntForEachEntry( vSupp, Entry, i ) - { - pFanin = Abc_NtkObj(pObj->pNtk, Entry); - Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, pFanin, 0 ); - } - - // for each cube, construct the node - nCubes = Min_CoverCountCubes( pCover ); - if ( nCubes == 0 ) - pNodeNew = Abc_NodeCreateConst0(pNtkNew); - else if ( nCubes == 1 ) - pNodeNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCover, vSupp ); - else - { - pNodeNew = Abc_NtkCreateNode( pNtkNew ); - Min_CoverForEachCube( pCover, pCube ) - { - pFaninNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCube, vSupp ); - Abc_ObjAddFanin( pNodeNew, pFaninNew ); - } - pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes ); - } - - pObj->pCopy = pNodeNew; - return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl ); -} - -/**Function************************************************************* - - Synopsis [Derives the decomposed network.] - - Description [The resulting network contains only pure AND/OR/EXOR gates - and inverters. This procedure is usedful to generate Verilog.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pNodeNew; - int i; - assert( Abc_NtkIsStrash(pNtk) ); - // perform strashing - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); - // reconstruct the network - Abc_NtkForEachCo( pNtk, pObj, i ) - { - pNodeNew = Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) ); - Abc_ObjAddFanin( pObj->pCopy, pNodeNew ); - } - // add the COs - Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); - // make sure everything is okay - if ( !Abc_NtkCheck( pNtkNew ) ) - { - printf( "Abc_NtkXyzDeriveInv: The network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - return pNtkNew; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/xyz/xyzCore.c b/src/temp/xyz/xyzCore.c deleted file mode 100644 index e5089788..00000000 --- a/src/temp/xyz/xyzCore.c +++ /dev/null @@ -1,1025 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyzCore.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [Core procedures.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyzCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "xyz.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ); -static int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ); -static void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary ); -/* -static int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); -static int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); -static int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); -static int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); -static int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); -static int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); -*/ - -static int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj ); -static Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ); -static Min_Cube_t * Abc_NodeXyzSum( Xyz_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_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose ) -{ - Abc_Ntk_t * pNtkNew; - Xyz_Man_t * p; - - assert( Abc_NtkIsStrash(pNtk) ); - - // create the manager - p = Xyz_ManAlloc( pNtk, nFaninMax ); - p->fUseEsop = fUseEsop; - p->fUseSop = 1;//fUseSop; - pNtk->pManCut = p; - - // perform mapping - Abc_NtkXyzCovers( p, pNtk, fVerbose ); - - // derive the final network - if ( fUseInvs ) - pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk ); - else - pNtkNew = Abc_NtkXyzDerive( p, pNtk ); -// pNtkNew = NULL; - - - Xyz_ManFree( p ); - pNtk->pManCut = NULL; - - // make sure that everything is okay - if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) ) - { - printf( "Abc_NtkXyz: The network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Compute the supports.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ) -{ - Abc_Obj_t * pObj; - int i, clk = clock(); - - // start the manager - p->vFanCounts = Abc_NtkFanoutCounts(pNtk); - - // set trivial cuts for the constant and the CIs - pObj = Abc_NtkConst1(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_NtkXyzCoversOne(p, pNtk, fVerbose) ) - break; - } - - // clean the cut-point markers - Abc_NtkForEachObj( pNtk, pObj, i ) - pObj->fMarkA = 0; - -if ( fVerbose ) -{ -PRT( "Total", clock() - clk ); -} -} - -/**Function************************************************************* - - Synopsis [Compute the supports.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ) -{ - ProgressBar * pProgress; - Abc_Obj_t * pObj; - Vec_Ptr_t * vBoundary; - int i, clk = 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_NtkXyzCovers_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( 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 ); -PRT( "T", clock() - clk ); -} - return fStop; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkXyzCovers_rec( Xyz_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_NtkXyzCovers_rec( p, pObj0, vBoundary ); - Abc_NtkXyzCovers_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_NodeXyzPropagate( 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_NodeXyzDropData( p, pObj0 ); -// Abc_NodeXyzDropData( p, pObj1 ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NodeXyzSupport( Xyz_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_NodeXyzPropagate( Xyz_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_NodeXyzSupport( 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_NodeXyzProduct( 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_NodeXyzProduct( 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_NodeXyzSum( 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_MAX( p->nSuppsMax, p->nSupps ); - return 1; -} - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Min_Cube_t * Abc_NodeXyzProduct( Xyz_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_NodeXyzSum( Xyz_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_NodeXyzPropagateEsop( Xyz_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_NodeXyzSupport( 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_NodeXyzProductEsop( 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_MAX( 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_NodeXyzPropagateSop( Xyz_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_NodeXyzSupport( 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_NodeXyzProductSop( 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_NodeXyzUnionSop( 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_MAX( 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_NodeXyzProductEsop( Xyz_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_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) -{ - return 1; -} - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeXyzUnionEsop( Xyz_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_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) -{ - return 1; -} - - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/xyz/xyzInt.h b/src/temp/xyz/xyzInt.h deleted file mode 100644 index 656612aa..00000000 --- a/src/temp/xyz/xyzInt.h +++ /dev/null @@ -1,642 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyzInt.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [Internal declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyzInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Min_Man_t_ Min_Man_t; -typedef struct Min_Cube_t_ Min_Cube_t; - -struct Min_Man_t_ -{ - int nVars; // the number of vars - int nWords; // the number of words - Extra_MmFixed_t * pMemMan; // memory manager for cubes - // temporary cubes - Min_Cube_t * pOne0; // tautology cube - Min_Cube_t * pOne1; // tautology cube - Min_Cube_t * pTriv0[2]; // trivial cube - Min_Cube_t * pTriv1[2]; // trivial cube - Min_Cube_t * pTemp; // cube for computing the distance - Min_Cube_t * pBubble; // cube used as a separator - // temporary storage for the new cover - int nCubes; // the number of cubes - Min_Cube_t ** ppStore; // storage for cubes by number of literals -}; - -struct Min_Cube_t_ -{ - Min_Cube_t * pNext; // the pointer to the next cube in the cover - unsigned nVars : 10; // the number of variables - unsigned nWords : 12; // the number of machine words - unsigned nLits : 10; // the number of literals in the cube - unsigned uData[1]; // the bit-data for the cube -}; - - -// iterators through the entries in the linked lists of cubes -#define Min_CoverForEachCube( pCover, pCube ) \ - for ( pCube = pCover; \ - pCube; \ - pCube = pCube->pNext ) -#define Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) \ - for ( pCube = pCover, \ - pCube2 = pCube? pCube->pNext: NULL; \ - pCube; \ - pCube = pCube2, \ - pCube2 = pCube? pCube->pNext: NULL ) -#define Min_CoverForEachCubePrev( pCover, pCube, ppPrev ) \ - for ( pCube = pCover, \ - ppPrev = &(pCover); \ - pCube; \ - ppPrev = &pCube->pNext, \ - pCube = pCube->pNext ) - -// macros to get hold of bits and values in the cubes -static inline int Min_CubeHasBit( Min_Cube_t * p, int i ) { return (p->uData[(i)>>5] & (1<<((i) & 31))) > 0; } -static inline void Min_CubeSetBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] |= (1<<((i) & 31)); } -static inline void Min_CubeXorBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] ^= (1<<((i) & 31)); } -static inline int Min_CubeGetVar( Min_Cube_t * p, int Var ) { return 3 & (p->uData[(2*Var)>>5] >> ((2*Var) & 31)); } -static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uData[(2*Var)>>5] ^= (Value<<((2*Var) & 31)); } - -/*=== xyzMinEsop.c ==========================================================*/ -extern void Min_EsopMinimize( Min_Man_t * p ); -extern void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); -/*=== xyzMinSop.c ==========================================================*/ -extern void Min_SopMinimize( Min_Man_t * p ); -extern void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); -/*=== xyzMinMan.c ==========================================================*/ -extern Min_Man_t * Min_ManAlloc( int nVars ); -extern void Min_ManClean( Min_Man_t * p, int nSupp ); -extern void Min_ManFree( Min_Man_t * p ); -/*=== xyzMinUtil.c ==========================================================*/ -extern void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube ); -extern void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ); -extern void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p ); -extern void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ); -extern void Min_CoverCheck( Min_Man_t * p ); -extern int Min_CubeCheck( Min_Cube_t * pCube ); -extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ); -extern void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover ); -extern int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Creates the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubeAlloc( Min_Man_t * p ) -{ - Min_Cube_t * pCube; - pCube = (Min_Cube_t *)Extra_MmFixedEntryFetch( p->pMemMan ); - pCube->pNext = NULL; - pCube->nVars = p->nVars; - pCube->nWords = p->nWords; - pCube->nLits = 0; - memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords ); - return pCube; -} - -/**Function************************************************************* - - Synopsis [Creates the cube representing elementary var.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubeAllocVar( Min_Man_t * p, int iVar, int fCompl ) -{ - Min_Cube_t * pCube; - pCube = Min_CubeAlloc( p ); - Min_CubeXorBit( pCube, iVar*2+fCompl ); - pCube->nLits = 1; - return pCube; -} - -/**Function************************************************************* - - Synopsis [Creates the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy ) -{ - Min_Cube_t * pCube; - pCube = Min_CubeAlloc( p ); - memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords ); - pCube->nLits = pCopy->nLits; - return pCube; -} - -/**Function************************************************************* - - Synopsis [Recycles the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CubeRecycle( Min_Man_t * p, Min_Cube_t * pCube ) -{ - Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube ); -} - -/**Function************************************************************* - - Synopsis [Recycles the cube cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CoverRecycle( Min_Man_t * p, Min_Cube_t * pCover ) -{ - Min_Cube_t * pCube, * pCube2; - Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube ); -} - - -/**Function************************************************************* - - Synopsis [Counts the number of cubes in the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubeCountLits( Min_Cube_t * pCube ) -{ - unsigned uData; - int Count = 0, i, w; - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); - for ( i = 0; i < 32; i += 2 ) - if ( uData & (1 << i) ) - Count++; - } - return Count; -} - -/**Function************************************************************* - - Synopsis [Counts the number of cubes in the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CubeGetLits( Min_Cube_t * pCube, Vec_Int_t * vLits ) -{ - unsigned uData; - int i, w; - Vec_IntClear( vLits ); - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); - for ( i = 0; i < 32; i += 2 ) - if ( uData & (1 << i) ) - Vec_IntPush( vLits, w*16 + i/2 ); - } -} - -/**Function************************************************************* - - Synopsis [Counts the number of cubes in the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CoverCountCubes( Min_Cube_t * pCover ) -{ - Min_Cube_t * pCube; - int Count = 0; - Min_CoverForEachCube( pCover, pCube ) - Count++; - return Count; -} - - -/**Function************************************************************* - - Synopsis [Checks if two cubes are disjoint.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubesDisjoint( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) -{ - unsigned uData; - int i; - assert( pCube0->nVars == pCube1->nVars ); - for ( i = 0; i < (int)pCube0->nWords; i++ ) - { - uData = pCube0->uData[i] & pCube1->uData[i]; - uData = (uData | (uData >> 1)) & 0x55555555; - if ( uData != 0x55555555 ) - return 1; - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Collects the disjoint variables of the two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CoverGetDisjVars( Min_Cube_t * pThis, Min_Cube_t * pCube, Vec_Int_t * vVars ) -{ - unsigned uData; - int i, w; - Vec_IntClear( vVars ); - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - uData = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555; - uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1)); - if ( uData == 0 ) - continue; - for ( i = 0; i < 32; i += 2 ) - if ( uData & (1 << i) ) - Vec_IntPush( vVars, w*16 + i/2 ); - } -} - -/**Function************************************************************* - - Synopsis [Checks if two cubes are disjoint.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubesDistOne( Min_Cube_t * pCube0, Min_Cube_t * pCube1, Min_Cube_t * pTemp ) -{ - unsigned uData; - int i, fFound = 0; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - { - uData = pCube0->uData[i] ^ pCube1->uData[i]; - if ( uData == 0 ) - { - if ( pTemp ) pTemp->uData[i] = 0; - continue; - } - if ( fFound ) - return 0; - uData = (uData | (uData >> 1)) & 0x55555555; - if ( (uData & (uData-1)) > 0 ) // more than one 1 - return 0; - if ( pTemp ) pTemp->uData[i] = uData | (uData << 1); - fFound = 1; - } - if ( fFound == 0 ) - { - printf( "\n" ); - Min_CubeWrite( stdout, pCube0 ); - Min_CubeWrite( stdout, pCube1 ); - printf( "Error: Min_CubesDistOne() looks at two equal cubes!\n" ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Checks if two cubes are disjoint.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubesDistTwo( Min_Cube_t * pCube0, Min_Cube_t * pCube1, int * pVar0, int * pVar1 ) -{ - unsigned uData;//, uData2; - int i, k, Var0 = -1, Var1 = -1; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - { - uData = pCube0->uData[i] ^ pCube1->uData[i]; - if ( uData == 0 ) - continue; - if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s - return 0; - uData = (uData | (uData >> 1)) & 0x55555555; - if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 ) - return 0; - for ( k = 0; k < 32; k += 2 ) - if ( uData & (1 << k) ) - { - if ( Var0 == -1 ) - Var0 = 16 * i + k/2; - else if ( Var1 == -1 ) - Var1 = 16 * i + k/2; - else - return 0; - } - /* - if ( Var0 >= 0 ) - { - uData &= 0xFFFF; - uData2 = (uData >> 16); - if ( uData && uData2 ) - return 0; - if ( uData ) - { - } - uData }= uData2; - uData &= 0x - } - */ - } - if ( Var0 >= 0 && Var1 >= 0 ) - { - *pVar0 = Var0; - *pVar1 = Var1; - return 1; - } - if ( Var0 == -1 || Var1 == -1 ) - { - printf( "\n" ); - Min_CubeWrite( stdout, pCube0 ); - Min_CubeWrite( stdout, pCube1 ); - printf( "Error: Min_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" ); - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Makes the produce of two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubesProduct( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) -{ - Min_Cube_t * pCube; - int i; - assert( pCube0->nVars == pCube1->nVars ); - pCube = Min_CubeAlloc( p ); - for ( i = 0; i < p->nWords; i++ ) - pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i]; - pCube->nLits = Min_CubeCountLits( pCube ); - return pCube; -} - -/**Function************************************************************* - - Synopsis [Makes the produce of two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubesXor( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) -{ - Min_Cube_t * pCube; - int i; - assert( pCube0->nVars == pCube1->nVars ); - pCube = Min_CubeAlloc( p ); - for ( i = 0; i < p->nWords; i++ ) - pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i]; - pCube->nLits = Min_CubeCountLits( pCube ); - return pCube; -} - -/**Function************************************************************* - - Synopsis [Makes the produce of two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubesAreEqual( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) -{ - int i; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - if ( pCube0->uData[i] != pCube1->uData[i] ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if pCube1 is contained in pCube0, bitwise.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CubeIsContained( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) -{ - int i; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Transforms the cube into the result of merging.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, Min_Cube_t * pMask ) -{ - int w; - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - pCube->uData[w] = pCube->uData[w] ^ pDist->uData[w]; - pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]); - } -} - -/**Function************************************************************* - - Synopsis [Transforms the cube into the result of distance-1 merging.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist ) -{ - int w; - for ( w = 0; w < (int)pCube->nWords; w++ ) - pCube->uData[w] |= pDist->uData[w]; -} - - - -/**Function************************************************************* - - Synopsis [Sorts the cover in the increasing number of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCover ) -{ - Min_Cube_t * pCube, * pCube2, * pThis; - if ( pCover == NULL ) - { - Min_ManClean( p, p->nVars ); - return; - } - Min_ManClean( p, pCover->nVars ); - Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - { - // go through the linked list - Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) - if ( Min_CubesAreEqual( pCube, pThis ) ) - { - Min_CubeRecycle( p, pCube ); - break; - } - if ( pThis != NULL ) - continue; - pCube->pNext = p->ppStore[pCube->nLits]; - p->ppStore[pCube->nLits] = pCube; - p->nCubes++; - } -} - -/**Function************************************************************* - - Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube ) -{ - Min_Cube_t * pThis; - int i; -/* - // this cube cannot be equal to any cube - Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) - { - if ( Min_CubesAreEqual( pCube, pThis ) ) - { - Min_CubeWrite( stdout, pCube ); - assert( 0 ); - } - } -*/ - // try to find a containing cube - for ( i = 0; i <= (int)pCube->nLits; i++ ) - Min_CoverForEachCube( p->ppStore[i], pThis ) - { - // skip the bubble - if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) - return 1; - } - return 0; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/xyz/xyzMan.c b/src/temp/xyz/xyzMan.c deleted file mode 100644 index 844e8c13..00000000 --- a/src/temp/xyz/xyzMan.c +++ /dev/null @@ -1,144 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyzMan.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [Decomposition manager.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyzMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "xyz.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax ) -{ - Xyz_Man_t * pMan; - Xyz_Obj_t * pMem; - Abc_Obj_t * pObj; - int i; - assert( pNtk->pManCut == NULL ); - - // start the manager - pMan = ALLOC( Xyz_Man_t, 1 ); - memset( pMan, 0, sizeof(Xyz_Man_t) ); - pMan->nFaninMax = nFaninMax; - pMan->nCubesMax = 2 * pMan->nFaninMax; - pMan->nWords = Abc_BitWordNum( nFaninMax * 2 ); - - // get the cubes - pMan->vComTo0 = Vec_IntAlloc( 2*nFaninMax ); - pMan->vComTo1 = Vec_IntAlloc( 2*nFaninMax ); - pMan->vPairs0 = Vec_IntAlloc( nFaninMax ); - pMan->vPairs1 = Vec_IntAlloc( nFaninMax ); - pMan->vTriv0 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv0, -1 ); - pMan->vTriv1 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv1, -1 ); - - // allocate memory for object structures - pMan->pMemory = pMem = ALLOC( Xyz_Obj_t, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) ); - memset( pMem, 0, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) ); - // allocate storage for the pointers to the memory - pMan->vObjStrs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) ); - Vec_PtrFill( pMan->vObjStrs, Abc_NtkObjNumMax(pNtk), NULL ); - Abc_NtkForEachObj( pNtk, pObj, i ) - Vec_PtrWriteEntry( pMan->vObjStrs, i, pMem + i ); - // create the cube manager - pMan->pManMin = Min_ManAlloc( nFaninMax ); - return pMan; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Xyz_ManFree( Xyz_Man_t * p ) -{ - Vec_Int_t * vSupp; - int i; - for ( i = 0; i < p->vObjStrs->nSize; i++ ) - { - vSupp = ((Xyz_Obj_t *)p->vObjStrs->pArray[i])->vSupp; - if ( vSupp ) Vec_IntFree( vSupp ); - } - - Min_ManFree( p->pManMin ); - Vec_PtrFree( p->vObjStrs ); - Vec_IntFree( p->vFanCounts ); - Vec_IntFree( p->vTriv0 ); - Vec_IntFree( p->vTriv1 ); - Vec_IntFree( p->vComTo0 ); - Vec_IntFree( p->vComTo1 ); - Vec_IntFree( p->vPairs0 ); - Vec_IntFree( p->vPairs1 ); - free( p->pMemory ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Drop the covers at the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj ) -{ - int nFanouts; - assert( p->vFanCounts ); - nFanouts = Vec_IntEntry( p->vFanCounts, pObj->Id ); - assert( nFanouts > 0 ); - if ( --nFanouts == 0 ) - { - Vec_IntFree( Abc_ObjGetSupp(pObj) ); - Abc_ObjSetSupp( pObj, NULL ); - Min_CoverRecycle( p->pManMin, Abc_ObjGetCover2(pObj) ); - Abc_ObjSetCover2( pObj, NULL ); - p->nSupps--; - } - Vec_IntWriteEntry( p->vFanCounts, pObj->Id, nFanouts ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/xyz/xyzMinEsop.c b/src/temp/xyz/xyzMinEsop.c deleted file mode 100644 index 839e2410..00000000 --- a/src/temp/xyz/xyzMinEsop.c +++ /dev/null @@ -1,299 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyzMinEsop.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [ESOP manipulation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyzMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "xyzInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Min_EsopRewrite( Min_Man_t * p ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_EsopMinimize( Min_Man_t * p ) -{ - int nCubesInit, nCubesOld, nIter; - if ( p->nCubes < 3 ) - return; - nIter = 0; - nCubesInit = p->nCubes; - do { - nCubesOld = p->nCubes; - Min_EsopRewrite( p ); - nIter++; - } - while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); - -// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); -} - -/**Function************************************************************* - - Synopsis [Performs one round of rewriting using distance 2 cubes.] - - Description [The weakness of this procedure is that it tries each cube - with only one distance-2 cube. If this pair does not lead to improvement - the cube is inserted into the cover anyhow, and we try another pair. - A possible improvement would be to try this cube with all distance-2 - cubes, until an improvement is found, or until all such cubes are tried.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_EsopRewrite( Min_Man_t * p ) -{ - Min_Cube_t * pCube, ** ppPrev; - Min_Cube_t * pThis, ** ppPrevT; - int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld; - int nPairs = 0; - - // insert the bubble before the first cube - p->pBubble->pNext = p->ppStore[0]; - p->ppStore[0] = p->pBubble; - p->pBubble->nLits = 0; - - // go through the cubes - while ( 1 ) - { - // get the index of the bubble - Index = p->pBubble->nLits; - - // find the bubble - Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev ) - if ( pCube == p->pBubble ) - break; - assert( pCube == p->pBubble ); - - // remove the bubble, get the next cube after the bubble - *ppPrev = p->pBubble->pNext; - pCube = p->pBubble->pNext; - if ( pCube == NULL ) - for ( Index++; Index <= p->nVars; Index++ ) - if ( p->ppStore[Index] ) - { - ppPrev = &(p->ppStore[Index]); - pCube = p->ppStore[Index]; - break; - } - // stop if there is no more cubes - if ( pCube == NULL ) - break; - - // find the first dist2 cube - Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT ) - if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) - break; - if ( pThis == NULL && Index < p->nVars ) - Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT ) - if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) - break; - if ( pThis == NULL && Index < p->nVars - 1 ) - Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT ) - if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) - break; - // continue if there is no dist2 cube - if ( pThis == NULL ) - { - // insert the bubble after the cube - p->pBubble->pNext = pCube->pNext; - pCube->pNext = p->pBubble; - p->pBubble->nLits = pCube->nLits; - continue; - } - nPairs++; - - // remove the cubes, insert the bubble instead of pCube - *ppPrevT = pThis->pNext; - *ppPrev = p->pBubble; - p->pBubble->pNext = pCube->pNext; - p->pBubble->nLits = pCube->nLits; - p->nCubes -= 2; - - // Exorlink-2: - // A{v00} B{v01} + A{v10} B{v11} = - // A{v00+v10} B{v01} + A{v10} B{v01+v11} = - // A{v00} B{v01+v11} + A{v00+v10} B{v11} - - // save the dist2 parameters - v00 = Min_CubeGetVar( pCube, Var0 ); - v01 = Min_CubeGetVar( pCube, Var1 ); - v10 = Min_CubeGetVar( pThis, Var0 ); - v11 = Min_CubeGetVar( pThis, Var1 ); -//printf( "\n" ); -//Min_CubeWrite( stdout, pCube ); -//Min_CubeWrite( stdout, pThis ); - - // derive the first pair of resulting cubes - Min_CubeXorVar( pCube, Var0, v10 ); - pCube->nLits -= (v00 != 3); - pCube->nLits += ((v00 ^ v10) != 3); - Min_CubeXorVar( pThis, Var1, v01 ); - pThis->nLits -= (v11 != 3); - pThis->nLits += ((v01 ^ v11) != 3); - - // add the cubes - nCubesOld = p->nCubes; - Min_EsopAddCube( p, pCube ); - Min_EsopAddCube( p, pThis ); - // check if the cubes were absorbed - if ( p->nCubes < nCubesOld + 2 ) - continue; - - // pull out both cubes - assert( pThis == p->ppStore[pThis->nLits] ); - p->ppStore[pThis->nLits] = pThis->pNext; - assert( pCube == p->ppStore[pCube->nLits] ); - p->ppStore[pCube->nLits] = pCube->pNext; - p->nCubes -= 2; - - // derive the second pair of resulting cubes - Min_CubeXorVar( pCube, Var0, v10 ); - pCube->nLits -= ((v00 ^ v10) != 3); - pCube->nLits += (v00 != 3); - Min_CubeXorVar( pCube, Var1, v11 ); - pCube->nLits -= (v01 != 3); - pCube->nLits += ((v01 ^ v11) != 3); - - Min_CubeXorVar( pThis, Var0, v00 ); - pThis->nLits -= (v10 != 3); - pThis->nLits += ((v00 ^ v10) != 3); - Min_CubeXorVar( pThis, Var1, v01 ); - pThis->nLits -= ((v01 ^ v11) != 3); - pThis->nLits += (v11 != 3); - - // add them anyhow - Min_EsopAddCube( p, pCube ); - Min_EsopAddCube( p, pThis ); - } -// printf( "Pairs = %d ", nPairs ); -} - -/**Function************************************************************* - - Synopsis [Adds the cube to storage.] - - Description [Returns 0 if the cube is added or removed. Returns 1 - if the cube is glued with some other cube and has to be added again. - Do not forget to clean the storage!] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube ) -{ - Min_Cube_t * pThis, ** ppPrev; - // try to find the identical cube - Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) - { - if ( Min_CubesAreEqual( pCube, pThis ) ) - { - *ppPrev = pThis->pNext; - Min_CubeRecycle( p, pCube ); - Min_CubeRecycle( p, pThis ); - p->nCubes--; - return 0; - } - } - // find a distance-1 cube if it exists - if ( pCube->nLits < pCube->nVars ) - Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev ) - { - if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) ) - { - *ppPrev = pThis->pNext; - Min_CubesTransform( pCube, pThis, p->pTemp ); - pCube->nLits++; - Min_CubeRecycle( p, pThis ); - p->nCubes--; - return 1; - } - } - Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) - { - if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) ) - { - *ppPrev = pThis->pNext; - Min_CubesTransform( pCube, pThis, p->pTemp ); - pCube->nLits--; - Min_CubeRecycle( p, pThis ); - p->nCubes--; - return 1; - } - } - if ( pCube->nLits > 0 ) - Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev ) - { - if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) ) - { - *ppPrev = pThis->pNext; - Min_CubesTransform( pCube, pThis, p->pTemp ); - Min_CubeRecycle( p, pThis ); - p->nCubes--; - return 1; - } - } - // add the cube - pCube->pNext = p->ppStore[pCube->nLits]; - p->ppStore[pCube->nLits] = pCube; - p->nCubes++; - return 0; -} - -/**Function************************************************************* - - Synopsis [Adds the cube to storage.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) -{ - assert( pCube != p->pBubble ); - assert( (int)pCube->nLits == Min_CubeCountLits(pCube) ); - while ( Min_EsopAddCubeInt( p, pCube ) ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/xyz/xyzMinMan.c b/src/temp/xyz/xyzMinMan.c deleted file mode 100644 index 20314698..00000000 --- a/src/temp/xyz/xyzMinMan.c +++ /dev/null @@ -1,113 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyzMinMan.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [SOP manipulation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyzMinMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "xyzInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Starts the minimization manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Min_Man_t * Min_ManAlloc( int nVars ) -{ - Min_Man_t * pMan; - // start the manager - pMan = ALLOC( Min_Man_t, 1 ); - memset( pMan, 0, sizeof(Min_Man_t) ); - pMan->nVars = nVars; - pMan->nWords = Abc_BitWordNum( nVars * 2 ); - pMan->pMemMan = Extra_MmFixedStart( sizeof(Min_Cube_t) + sizeof(unsigned) * (pMan->nWords - 1) ); - // allocate storage for the temporary cover - pMan->ppStore = ALLOC( Min_Cube_t *, pMan->nVars + 1 ); - // create tautology cubes - Min_ManClean( pMan, nVars ); - pMan->pOne0 = Min_CubeAlloc( pMan ); - pMan->pOne1 = Min_CubeAlloc( pMan ); - pMan->pTemp = Min_CubeAlloc( pMan ); - pMan->pBubble = Min_CubeAlloc( pMan ); pMan->pBubble->uData[0] = 0; - // create trivial cubes - Min_ManClean( pMan, 1 ); - pMan->pTriv0[0] = Min_CubeAllocVar( pMan, 0, 0 ); - pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 ); - pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 ); - pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 ); - Min_ManClean( pMan, nVars ); - return pMan; -} - -/**Function************************************************************* - - Synopsis [Cleans the minimization manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_ManClean( Min_Man_t * p, int nSupp ) -{ - // set the size of the cube manager - p->nVars = nSupp; - p->nWords = Abc_BitWordNum(2*nSupp); - // clean the storage - memset( p->ppStore, 0, sizeof(Min_Cube_t *) * (nSupp + 1) ); - p->nCubes = 0; -} - -/**Function************************************************************* - - Synopsis [Stops the minimization manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_ManFree( Min_Man_t * p ) -{ - Extra_MmFixedStop ( p->pMemMan, 0 ); - free( p->ppStore ); - free( p ); -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/xyz/xyzMinSop.c b/src/temp/xyz/xyzMinSop.c deleted file mode 100644 index a5d57c66..00000000 --- a/src/temp/xyz/xyzMinSop.c +++ /dev/null @@ -1,615 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyzMinSop.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [SOP manipulation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyzMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "xyzInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Min_SopRewrite( Min_Man_t * p ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_SopMinimize( Min_Man_t * p ) -{ - int nCubesInit, nCubesOld, nIter; - if ( p->nCubes < 3 ) - return; - nIter = 0; - nCubesInit = p->nCubes; - do { - nCubesOld = p->nCubes; - Min_SopRewrite( p ); - nIter++; -// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); - } - while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); -// printf( "\n" ); - -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_SopRewrite( Min_Man_t * p ) -{ - Min_Cube_t * pCube, ** ppPrev; - Min_Cube_t * pThis, ** ppPrevT; - Min_Cube_t * pTemp; - int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld; - int nPairs = 0; -/* - { - Min_Cube_t * pCover; - pCover = Min_CoverCollect( p, p->nVars ); -printf( "\n\n" ); -Min_CoverWrite( stdout, pCover ); - Min_CoverExpand( p, pCover ); - } -*/ - - // insert the bubble before the first cube - p->pBubble->pNext = p->ppStore[0]; - p->ppStore[0] = p->pBubble; - p->pBubble->nLits = 0; - - // go through the cubes - while ( 1 ) - { - // get the index of the bubble - Index = p->pBubble->nLits; - - // find the bubble - Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev ) - if ( pCube == p->pBubble ) - break; - assert( pCube == p->pBubble ); - - // remove the bubble, get the next cube after the bubble - *ppPrev = p->pBubble->pNext; - pCube = p->pBubble->pNext; - if ( pCube == NULL ) - for ( Index++; Index <= p->nVars; Index++ ) - if ( p->ppStore[Index] ) - { - ppPrev = &(p->ppStore[Index]); - pCube = p->ppStore[Index]; - break; - } - // stop if there is no more cubes - if ( pCube == NULL ) - break; - - // find the first dist2 cube - Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT ) - if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) - break; - if ( pThis == NULL && Index < p->nVars ) - Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT ) - if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) - break; - // continue if there is no dist2 cube - if ( pThis == NULL ) - { - // insert the bubble after the cube - p->pBubble->pNext = pCube->pNext; - pCube->pNext = p->pBubble; - p->pBubble->nLits = pCube->nLits; - continue; - } - nPairs++; -/* -printf( "\n" ); -Min_CubeWrite( stdout, pCube ); -Min_CubeWrite( stdout, pThis ); -*/ - // remove the cubes, insert the bubble instead of pCube - *ppPrevT = pThis->pNext; - *ppPrev = p->pBubble; - p->pBubble->pNext = pCube->pNext; - p->pBubble->nLits = pCube->nLits; - p->nCubes -= 2; - - assert( pCube != p->pBubble && pThis != p->pBubble ); - - - // save the dist2 parameters - v00 = Min_CubeGetVar( pCube, Var0 ); - v01 = Min_CubeGetVar( pCube, Var1 ); - v10 = Min_CubeGetVar( pThis, Var0 ); - v11 = Min_CubeGetVar( pThis, Var1 ); - assert( v00 != v10 && v01 != v11 ); - assert( v00 != 3 || v01 != 3 ); - assert( v10 != 3 || v11 != 3 ); - -//printf( "\n" ); -//Min_CubeWrite( stdout, pCube ); -//Min_CubeWrite( stdout, pThis ); - -//printf( "\n" ); -//Min_CubeWrite( stdout, pCube ); -//Min_CubeWrite( stdout, pThis ); - - // consider the case when both cubes have non-empty literals - if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 ) - { - assert( v00 == (v10 ^ 3) ); - assert( v01 == (v11 ^ 3) ); - // create the temporary cube equal to the first corner - Min_CubeXorVar( pCube, Var0, 3 ); - // check if this cube is contained - fCont0 = Min_CoverContainsCube( p, pCube ); - // create the temporary cube equal to the first corner - Min_CubeXorVar( pCube, Var0, 3 ); - Min_CubeXorVar( pCube, Var1, 3 ); -//printf( "\n" ); -//Min_CubeWrite( stdout, pCube ); -//Min_CubeWrite( stdout, pThis ); - // check if this cube is contained - fCont1 = Min_CoverContainsCube( p, pCube ); - // undo the change - Min_CubeXorVar( pCube, Var1, 3 ); - - // check if the cubes can be overwritten - if ( fCont0 && fCont1 ) - { - // one of the cubes can be recycled, the other expanded and added - Min_CubeRecycle( p, pThis ); - // remove the literals - Min_CubeXorVar( pCube, Var0, v00 ^ 3 ); - Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); - pCube->nLits -= 2; - Min_SopAddCube( p, pCube ); - } - else if ( fCont0 ) - { - // expand both cubes and add them - Min_CubeXorVar( pCube, Var0, v00 ^ 3 ); - pCube->nLits--; - Min_SopAddCube( p, pCube ); - Min_CubeXorVar( pThis, Var1, v11 ^ 3 ); - pThis->nLits--; - Min_SopAddCube( p, pThis ); - } - else if ( fCont1 ) - { - // expand both cubes and add them - Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); - pCube->nLits--; - Min_SopAddCube( p, pCube ); - Min_CubeXorVar( pThis, Var0, v10 ^ 3 ); - pThis->nLits--; - Min_SopAddCube( p, pThis ); - } - else - { - Min_SopAddCube( p, pCube ); - Min_SopAddCube( p, pThis ); - } - // otherwise, no change is possible - continue; - } - - // if one of them does not have DC lit, move it - if ( v00 != 3 && v01 != 3 ) - { - assert( v10 == 3 || v11 == 3 ); - pTemp = pCube; pCube = pThis; pThis = pTemp; - Index = v00; v00 = v10; v10 = Index; - Index = v01; v01 = v11; v11 = Index; - } - - // make sure the first cube has first var DC - if ( v00 != 3 ) - { - assert( v01 == 3 ); - Index = Var0; Var0 = Var1; Var1 = Index; - Index = v00; v00 = v01; v01 = Index; - Index = v10; v10 = v11; v11 = Index; - } - - // consider both cases: both have DC lit - if ( v00 == 3 && v11 == 3 ) - { - assert( v01 != 3 && v10 != 3 ); - // try the remaining minterm - // create the temporary cube equal to the first corner - Min_CubeXorVar( pCube, Var0, v10 ); - Min_CubeXorVar( pCube, Var1, 3 ); - pCube->nLits++; - // check if this cube is contained - fCont0 = Min_CoverContainsCube( p, pCube ); - // undo the cube transformations - Min_CubeXorVar( pCube, Var0, v10 ); - Min_CubeXorVar( pCube, Var1, 3 ); - pCube->nLits--; - // check the case when both are covered - if ( fCont0 ) - { - // one of the cubes can be recycled, the other expanded and added - Min_CubeRecycle( p, pThis ); - // remove the literals - Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); - pCube->nLits--; - Min_SopAddCube( p, pCube ); - } - else - { - // try two reduced cubes - Min_CubeXorVar( pCube, Var0, v10 ); - pCube->nLits++; - // remember the cubes - nCubesOld = p->nCubes; - Min_SopAddCube( p, pCube ); - // check if the cube is absorbed - if ( p->nCubes < nCubesOld + 1 ) - { // absorbed - add the second cube - Min_SopAddCube( p, pThis ); - } - else - { // remove this cube, and try another one - assert( pCube == p->ppStore[pCube->nLits] ); - p->ppStore[pCube->nLits] = pCube->pNext; - p->nCubes--; - - // return the cube to the previous state - Min_CubeXorVar( pCube, Var0, v10 ); - pCube->nLits--; - - // generate another reduced cube - Min_CubeXorVar( pThis, Var1, v01 ); - pThis->nLits++; - - // add both cubes - Min_SopAddCube( p, pCube ); - Min_SopAddCube( p, pThis ); - } - } - } - else // the first cube has DC lit - { - assert( v01 != 3 && v10 != 3 && v11 != 3 ); - // try the remaining minterm - // create the temporary cube equal to the minterm - Min_CubeXorVar( pThis, Var0, 3 ); - // check if this cube is contained - fCont0 = Min_CoverContainsCube( p, pThis ); - // undo the cube transformations - Min_CubeXorVar( pThis, Var0, 3 ); - // check the case when both are covered - if ( fCont0 ) - { - // one of the cubes can be recycled, the other expanded and added - Min_CubeRecycle( p, pThis ); - // remove the literals - Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); - pCube->nLits--; - Min_SopAddCube( p, pCube ); - } - else - { - // try reshaping the cubes - // reduce the first cube - Min_CubeXorVar( pCube, Var0, v10 ); - pCube->nLits++; - // expand the second cube - Min_CubeXorVar( pThis, Var1, v11 ^ 3 ); - pThis->nLits--; - // add both cubes - Min_SopAddCube( p, pCube ); - Min_SopAddCube( p, pThis ); - } - } - } -// printf( "Pairs = %d ", nPairs ); -} - -/**Function************************************************************* - - Synopsis [Adds cube to the SOP cover stored in the manager.] - - Description [Returns 0 if the cube is added or removed. Returns 1 - if the cube is glued with some other cube and has to be added again.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube ) -{ - Min_Cube_t * pThis, * pThis2, ** ppPrev; - int i; - // try to find the identical cube - Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) - { - if ( Min_CubesAreEqual( pCube, pThis ) ) - { - Min_CubeRecycle( p, pCube ); - return 0; - } - } - // try to find a containing cube - for ( i = 0; i < (int)pCube->nLits; i++ ) - Min_CoverForEachCube( p->ppStore[i], pThis ) - { - if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) - { - Min_CubeRecycle( p, pCube ); - return 0; - } - } - // try to find distance one in the same bin - Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) - { - if ( Min_CubesDistOne( pCube, pThis, NULL ) ) - { - *ppPrev = pThis->pNext; - Min_CubesTransformOr( pCube, pThis ); - pCube->nLits--; - Min_CubeRecycle( p, pThis ); - p->nCubes--; - return 1; - } - } - - // clean the other cubes using this one - for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ ) - { - ppPrev = &p->ppStore[i]; - Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 ) - { - if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) ) - { - *ppPrev = pThis->pNext; - Min_CubeRecycle( p, pThis ); - p->nCubes--; - } - else - ppPrev = &pThis->pNext; - } - } - - // add the cube - pCube->pNext = p->ppStore[pCube->nLits]; - p->ppStore[pCube->nLits] = pCube; - p->nCubes++; - return 0; -} - -/**Function************************************************************* - - Synopsis [Adds the cube to storage.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) -{ - assert( Min_CubeCheck( pCube ) ); - assert( pCube != p->pBubble ); - assert( (int)pCube->nLits == Min_CubeCountLits(pCube) ); - while ( Min_SopAddCubeInt( p, pCube ) ); -} - - - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_SopContain( Min_Man_t * p ) -{ - Min_Cube_t * pCube, * pCube2, ** ppPrev; - int i, k; - for ( i = 0; i <= p->nVars; i++ ) - { - Min_CoverForEachCube( p->ppStore[i], pCube ) - Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev ) - { - if ( !Min_CubesAreEqual( pCube, pCube2 ) ) - continue; - *ppPrev = pCube2->pNext; - Min_CubeRecycle( p, pCube2 ); - p->nCubes--; - } - for ( k = i + 1; k <= p->nVars; k++ ) - Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev ) - { - if ( !Min_CubeIsContained( pCube, pCube2 ) ) - continue; - *ppPrev = pCube2->pNext; - Min_CubeRecycle( p, pCube2 ); - p->nCubes--; - } - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_SopDist1Merge( Min_Man_t * p ) -{ - Min_Cube_t * pCube, * pCube2, * pCubeNew; - int i; - for ( i = p->nVars; i >= 0; i-- ) - { - Min_CoverForEachCube( p->ppStore[i], pCube ) - Min_CoverForEachCube( pCube->pNext, pCube2 ) - { - assert( pCube->nLits == pCube2->nLits ); - if ( !Min_CubesDistOne( pCube, pCube2, NULL ) ) - continue; - pCubeNew = Min_CubesXor( p, pCube, pCube2 ); - assert( pCubeNew->nLits == pCube->nLits - 1 ); - pCubeNew->pNext = p->ppStore[pCubeNew->nLits]; - p->ppStore[pCubeNew->nLits] = pCubeNew; - p->nCubes++; - } - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp ) -{ - Vec_Int_t * vVars; - Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev; - int Num, Value, i; - - // get the variables - vVars = Vec_IntAlloc( 100 ); - // create the tautology cube - pCover = Min_CubeAlloc( p ); - // sharp it with all cubes - Min_CoverForEachCube( pSharp, pCube ) - Min_CoverForEachCubePrev( pCover, pThis, ppPrev ) - { - if ( Min_CubesDisjoint( pThis, pCube ) ) - continue; - // remember the next pointer - pNext = pThis->pNext; - // get the variables, in which pThis is '-' while pCube is fixed - Min_CoverGetDisjVars( pThis, pCube, vVars ); - // generate the disjoint cubes - pReady = pThis; - Vec_IntForEachEntryReverse( vVars, Num, i ) - { - // correct the literal - Min_CubeXorVar( pReady, vVars->pArray[i], 3 ); - if ( i == 0 ) - break; - // create the new cube and clean this value - Value = Min_CubeGetVar( pReady, vVars->pArray[i] ); - pReady = Min_CubeDup( p, pReady ); - Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value ); - // add to the cover - *ppPrev = pReady; - ppPrev = &pReady->pNext; - } - pThis = pReady; - pThis->pNext = pNext; - } - Vec_IntFree( vVars ); - - // perform dist-1 merge and contain - Min_CoverExpandRemoveEqual( p, pCover ); - Min_SopDist1Merge( p ); - Min_SopContain( p ); - return Min_CoverCollect( p, p->nVars ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Min_SopCheck( Min_Man_t * p ) -{ - Min_Cube_t * pCube, * pThis; - int i; - - pCube = Min_CubeAlloc( p ); - Min_CubeXorBit( pCube, 2*0+1 ); - Min_CubeXorBit( pCube, 2*1+1 ); - Min_CubeXorBit( pCube, 2*2+0 ); - Min_CubeXorBit( pCube, 2*3+0 ); - Min_CubeXorBit( pCube, 2*4+0 ); - Min_CubeXorBit( pCube, 2*5+1 ); - Min_CubeXorBit( pCube, 2*6+1 ); - pCube->nLits = 7; - -// Min_CubeWrite( stdout, pCube ); - - // check that the cubes contain it - for ( i = 0; i <= p->nVars; i++ ) - Min_CoverForEachCube( p->ppStore[i], pThis ) - if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) - { - Min_CubeRecycle( p, pCube ); - return 1; - } - Min_CubeRecycle( p, pCube ); - return 0; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/xyz/xyzMinUtil.c b/src/temp/xyz/xyzMinUtil.c deleted file mode 100644 index 9ec5f83f..00000000 --- a/src/temp/xyz/xyzMinUtil.c +++ /dev/null @@ -1,277 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyzMinUtil.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [Utilities.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyzMinUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "xyzInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube ) -{ - int i; - assert( (int)pCube->nLits == Min_CubeCountLits(pCube) ); - for ( i = 0; i < (int)pCube->nVars; i++ ) - if ( Min_CubeHasBit(pCube, i*2) ) - { - if ( Min_CubeHasBit(pCube, i*2+1) ) - fprintf( pFile, "-" ); - else - fprintf( pFile, "0" ); - } - else - { - if ( Min_CubeHasBit(pCube, i*2+1) ) - fprintf( pFile, "1" ); - else - fprintf( pFile, "?" ); - } - fprintf( pFile, " 1\n" ); -// fprintf( pFile, " %d\n", pCube->nLits ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ) -{ - Min_Cube_t * pCube; - Min_CoverForEachCube( pCover, pCube ) - Min_CubeWrite( pFile, pCube ); - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p ) -{ - Min_Cube_t * pCube; - int i; - for ( i = 0; i <= p->nVars; i++ ) - { - Min_CoverForEachCube( p->ppStore[i], pCube ) - { - printf( "%2d : ", i ); - if ( pCube == p->pBubble ) - { - printf( "Bubble\n" ); - continue; - } - Min_CubeWrite( pFile, pCube ); - } - } - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ) -{ - char Buffer[1000]; - Min_Cube_t * pCube; - FILE * pFile; - int i; - sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" ); - for ( i = strlen(Buffer) - 1; i >= 0; i-- ) - if ( Buffer[i] == '<' || Buffer[i] == '>' ) - Buffer[i] = '_'; - pFile = fopen( Buffer, "w" ); - fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() ); - fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 ); - fprintf( pFile, ".o %d\n", 1 ); - fprintf( pFile, ".p %d\n", Min_CoverCountCubes(pCover) ); - if ( fEsop ) fprintf( pFile, ".type esop\n" ); - Min_CoverForEachCube( pCover, pCube ) - Min_CubeWrite( pFile, pCube ); - fprintf( pFile, ".e\n" ); - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_CoverCheck( Min_Man_t * p ) -{ - Min_Cube_t * pCube; - int i; - for ( i = 0; i <= p->nVars; i++ ) - Min_CoverForEachCube( p->ppStore[i], pCube ) - assert( i == (int)pCube->nLits ); -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Min_CubeCheck( Min_Cube_t * pCube ) -{ - int i; - for ( i = 0; i < (int)pCube->nVars; i++ ) - if ( Min_CubeGetVar( pCube, i ) == 0 ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Converts the cover from the sorted structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ) -{ - Min_Cube_t * pCov = NULL, ** ppTail = &pCov; - Min_Cube_t * pCube, * pCube2; - int i; - for ( i = 0; i <= nSuppSize; i++ ) - { - Min_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 ) - { - assert( i == (int)pCube->nLits ); - *ppTail = pCube; - ppTail = &pCube->pNext; - assert( pCube->uData[0] ); // not a bubble - } - } - *ppTail = NULL; - return pCov; -} - -/**Function************************************************************* - - Synopsis [Sorts the cover in the increasing number of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover ) -{ - Min_Cube_t * pCube, * pCube2; - Min_ManClean( p, p->nVars ); - Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - { - pCube->pNext = p->ppStore[pCube->nLits]; - p->ppStore[pCube->nLits] = pCube; - p->nCubes++; - } -} - -/**Function************************************************************* - - Synopsis [Sorts the cover in the increasing number of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover ) -{ - Min_Cube_t * pCube; - int i, Counter; - if ( pCover == NULL ) - return 0; - // clean the cube - for ( i = 0; i < (int)pCover->nWords; i++ ) - p->pTemp->uData[i] = ~((unsigned)0); - // add the bit data - Min_CoverForEachCube( pCover, pCube ) - for ( i = 0; i < (int)pCover->nWords; i++ ) - p->pTemp->uData[i] &= pCube->uData[i]; - // count the vars - Counter = 0; - for ( i = 0; i < (int)pCover->nVars; i++ ) - Counter += ( Min_CubeGetVar(p->pTemp, i) != 3 ); - return Counter; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/xyz/xyzTest.c b/src/temp/xyz/xyzTest.c deleted file mode 100644 index 38580790..00000000 --- a/src/temp/xyz/xyzTest.c +++ /dev/null @@ -1,417 +0,0 @@ -/**CFile**************************************************************** - - FileName [xyzTest.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [Testing procedures.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: xyzTest.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "xyz.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Min_Cube_t * Abc_NodeDeriveCoverPro( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 ) -{ - Min_Cube_t * pCover; - Min_Cube_t * pCube0, * pCube1, * pCube; - if ( pCover0 == NULL || pCover1 == NULL ) - return NULL; - // clean storage - Min_ManClean( p, p->nVars ); - // go through the cube pairs - Min_CoverForEachCube( pCover0, pCube0 ) - Min_CoverForEachCube( pCover1, pCube1 ) - { - if ( Min_CubesDisjoint( pCube0, pCube1 ) ) - continue; - pCube = Min_CubesProduct( p, pCube0, pCube1 ); - // add the cube to storage - Min_SopAddCube( p, pCube ); - } - Min_SopMinimize( p ); - pCover = Min_CoverCollect( p, p->nVars ); - assert( p->nCubes == Min_CoverCountCubes(pCover) ); - return pCover; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Min_Cube_t * Abc_NodeDeriveCoverSum( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 ) -{ - Min_Cube_t * pCover; - Min_Cube_t * pThis, * pCube; - if ( pCover0 == NULL || pCover1 == NULL ) - return NULL; - // clean storage - Min_ManClean( p, p->nVars ); - // add the cubes to storage - Min_CoverForEachCube( pCover0, pThis ) - { - pCube = Min_CubeDup( p, pThis ); - Min_SopAddCube( p, pCube ); - } - Min_CoverForEachCube( pCover1, pThis ) - { - pCube = Min_CubeDup( p, pThis ); - Min_SopAddCube( p, pCube ); - } - Min_SopMinimize( p ); - pCover = Min_CoverCollect( p, p->nVars ); - assert( p->nCubes == Min_CoverCountCubes(pCover) ); - return pCover; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeDeriveSops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes ) -{ - Min_Cube_t * pCov0[2], * pCov1[2]; - Min_Cube_t * pCoverP, * pCoverN; - Abc_Obj_t * pObj; - int i, nCubes, fCompl0, fCompl1; - - // set elementary vars - Vec_PtrForEachEntry( vSupp, pObj, i ) - { - pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 ); - pObj->pNext = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 1 ); - } - - // get the cover for each node in the array - Vec_PtrForEachEntry( vNodes, pObj, i ) - { - // get the complements - fCompl0 = Abc_ObjFaninC0(pObj); - fCompl1 = Abc_ObjFaninC1(pObj); - // get the covers - pCov0[0] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy; - pCov0[1] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pNext; - pCov1[0] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy; - pCov1[1] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pNext; - // compute the covers - pCoverP = Abc_NodeDeriveCoverPro( p, pCov0[ fCompl0], pCov1[ fCompl1] ); - pCoverN = Abc_NodeDeriveCoverSum( p, pCov0[!fCompl0], pCov1[!fCompl1] ); - // set the covers - pObj->pCopy = (Abc_Obj_t *)pCoverP; - pObj->pNext = (Abc_Obj_t *)pCoverN; - } - - nCubes = ABC_MIN( Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverP) ); - -/* -printf( "\n\n" ); -Min_CoverWrite( stdout, pCoverP ); -printf( "\n\n" ); -Min_CoverWrite( stdout, pCoverN ); -*/ - -// printf( "\n" ); -// Min_CoverWrite( stdout, pCoverP ); - -// Min_CoverExpand( p, pCoverP ); -// Min_SopMinimize( p ); -// pCoverP = Min_CoverCollect( p, p->nVars ); - -// printf( "\n" ); -// Min_CoverWrite( stdout, pCoverP ); - -// nCubes = Min_CoverCountCubes(pCoverP); - - // clean the copy fields - Vec_PtrForEachEntry( vNodes, pObj, i ) - pObj->pCopy = pObj->pNext = NULL; - Vec_PtrForEachEntry( vSupp, pObj, i ) - pObj->pCopy = pObj->pNext = NULL; - -// Min_CoverWriteFile( pCoverP, Abc_ObjName(pRoot), 0 ); -// printf( "\n" ); -// Min_CoverWrite( stdout, pCoverP ); - -// printf( "\n" ); -// Min_CoverWrite( stdout, pCoverP ); -// printf( "\n" ); -// Min_CoverWrite( stdout, pCoverN ); - return nCubes; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkTestSop( Abc_Ntk_t * pNtk ) -{ - Min_Man_t * p; - Vec_Ptr_t * vSupp, * vNodes; - Abc_Obj_t * pObj; - int i, nCubes; - assert( Abc_NtkIsStrash(pNtk) ); - - Abc_NtkCleanCopy(pNtk); - Abc_NtkCleanNext(pNtk); - Abc_NtkForEachCo( pNtk, pObj, i ) - { - if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) ) - { - printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) ); - continue; - } - - vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 ); - vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 ); - - printf( "%20s : Cone = %5d. Supp = %5d. ", - Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize ); -// if ( vSupp->nSize <= 128 ) - { - p = Min_ManAlloc( vSupp->nSize ); - nCubes = Abc_NodeDeriveSops( p, pObj, vSupp, vNodes ); - printf( "Cubes = %5d. ", nCubes ); - Min_ManFree( p ); - } - printf( "\n" ); - - - Vec_PtrFree( vNodes ); - Vec_PtrFree( vSupp ); - } -} - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Min_Cube_t * Abc_NodeDeriveCover( Min_Man_t * p, Min_Cube_t * pCov0, Min_Cube_t * pCov1, int fComp0, int fComp1 ) -{ - Min_Cube_t * pCover0, * pCover1, * pCover; - Min_Cube_t * pCube0, * pCube1, * pCube; - - // complement the first if needed - if ( !fComp0 ) - pCover0 = pCov0; - else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube - pCover0 = pCov0->pNext; - else - pCover0 = p->pOne0, p->pOne0->pNext = pCov0; - - // complement the second if needed - if ( !fComp1 ) - pCover1 = pCov1; - else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube - pCover1 = pCov1->pNext; - else - pCover1 = p->pOne1, p->pOne1->pNext = pCov1; - - if ( pCover0 == NULL || pCover1 == NULL ) - return NULL; - - // clean storage - Min_ManClean( p, p->nVars ); - // go through the cube pairs - Min_CoverForEachCube( pCover0, pCube0 ) - Min_CoverForEachCube( pCover1, pCube1 ) - { - if ( Min_CubesDisjoint( pCube0, pCube1 ) ) - continue; - pCube = Min_CubesProduct( p, pCube0, pCube1 ); - // add the cube to storage - Min_EsopAddCube( p, pCube ); - } - - if ( p->nCubes > 10 ) - { -// printf( "(%d,", p->nCubes ); - Min_EsopMinimize( p ); -// printf( "%d) ", p->nCubes ); - } - - pCover = Min_CoverCollect( p, p->nVars ); - assert( p->nCubes == Min_CoverCountCubes(pCover) ); - -// if ( p->nCubes > 1000 ) -// printf( "%d ", p->nCubes ); - return pCover; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeDeriveEsops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes ) -{ - Min_Cube_t * pCover, * pCube; - Abc_Obj_t * pObj; - int i; - - // set elementary vars - Vec_PtrForEachEntry( vSupp, pObj, i ) - pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 ); - - // get the cover for each node in the array - Vec_PtrForEachEntry( vNodes, pObj, i ) - { - pCover = Abc_NodeDeriveCover( p, - (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy, - (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy, - Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); - pObj->pCopy = (Abc_Obj_t *)pCover; - if ( p->nCubes > 3000 ) - return -1; - } - - // add complement if needed - if ( Abc_ObjFaninC0(pRoot) ) - { - if ( pCover && pCover->nLits == 0 ) // topmost one is the tautology cube - { - pCube = pCover; - pCover = pCover->pNext; - Min_CubeRecycle( p, pCube ); - p->nCubes--; - } - else - { - pCube = Min_CubeAlloc( p ); - pCube->pNext = pCover; - p->nCubes++; - } - } -/* - Min_CoverExpand( p, pCover ); - Min_EsopMinimize( p ); - pCover = Min_CoverCollect( p, p->nVars ); -*/ - // clean the copy fields - Vec_PtrForEachEntry( vNodes, pObj, i ) - pObj->pCopy = NULL; - Vec_PtrForEachEntry( vSupp, pObj, i ) - pObj->pCopy = NULL; - -// Min_CoverWriteFile( pCover, Abc_ObjName(pRoot), 1 ); -// Min_CoverWrite( stdout, pCover ); - return p->nCubes; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkTestEsop( Abc_Ntk_t * pNtk ) -{ - Min_Man_t * p; - Vec_Ptr_t * vSupp, * vNodes; - Abc_Obj_t * pObj; - int i, nCubes; - assert( Abc_NtkIsStrash(pNtk) ); - - Abc_NtkCleanCopy(pNtk); - Abc_NtkForEachCo( pNtk, pObj, i ) - { - if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) ) - { - printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) ); - continue; - } - - vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 ); - vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 ); - - printf( "%20s : Cone = %5d. Supp = %5d. ", - Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize ); -// if ( vSupp->nSize <= 128 ) - { - p = Min_ManAlloc( vSupp->nSize ); - nCubes = Abc_NodeDeriveEsops( p, pObj, vSupp, vNodes ); - printf( "Cubes = %5d. ", nCubes ); - Min_ManFree( p ); - } - printf( "\n" ); - - - Vec_PtrFree( vNodes ); - Vec_PtrFree( vSupp ); - } -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |