summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/rwr/rwr.h1
-rw-r--r--src/opt/rwr/rwrMan.c23
-rw-r--r--src/opt/xyz/module.make8
-rw-r--r--src/opt/xyz/xyz.h94
-rw-r--r--src/opt/xyz/xyzBuild.c379
-rw-r--r--src/opt/xyz/xyzCore.c697
-rw-r--r--src/opt/xyz/xyzInt.h631
-rw-r--r--src/opt/xyz/xyzMan.c144
-rw-r--r--src/opt/xyz/xyzMinEsop.c277
-rw-r--r--src/opt/xyz/xyzMinMan.c112
-rw-r--r--src/opt/xyz/xyzMinSop.c341
-rw-r--r--src/opt/xyz/xyzMinUtil.c225
-rw-r--r--src/opt/xyz/xyzTest.c51
13 files changed, 2983 insertions, 0 deletions
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 3856c04e..70e1070b 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -129,6 +129,7 @@ extern void Rwr_ManIncTravId( Rwr_Man_t * p );
extern Rwr_Man_t * Rwr_ManStart( bool fPrecompute );
extern void Rwr_ManStop( Rwr_Man_t * p );
extern void Rwr_ManPrintStats( Rwr_Man_t * p );
+extern void Rwr_ManPrintStatsFile( Rwr_Man_t * p );
extern void * Rwr_ManReadDecs( Rwr_Man_t * p );
extern int Rwr_ManReadCompl( Rwr_Man_t * p );
extern void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 1d306e7e..115065f5 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -179,6 +179,29 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
SeeAlso []
***********************************************************************/
+void Rwr_ManPrintStatsFile( Rwr_Man_t * p )
+{
+ FILE * pTable;
+ pTable = fopen( "stats.txt", "a+" );
+ fprintf( pTable, "%d ", p->nCutsGood );
+ fprintf( pTable, "%d ", p->nSubgraphs );
+ fprintf( pTable, "%d ", p->nNodesRewritten );
+ fprintf( pTable, "%d", p->nNodesGained );
+ fprintf( pTable, "\n" );
+ fclose( pTable );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void * Rwr_ManReadDecs( Rwr_Man_t * p )
{
return p->pGraph;
diff --git a/src/opt/xyz/module.make b/src/opt/xyz/module.make
new file mode 100644
index 00000000..ae7dab0f
--- /dev/null
+++ b/src/opt/xyz/module.make
@@ -0,0 +1,8 @@
+SRC += src/opt/xyz/xyzBuild.c \
+ src/opt/xyz/xyzCore.c \
+ src/opt/xyz/xyzMan.c \
+ src/opt/xyz/xyzMinEsop.c \
+ src/opt/xyz/xyzMinMan.c \
+ src/opt/xyz/xyzMinSop.c \
+ src/opt/xyz/xyzMinUtil.c \
+ src/opt/xyz/xyzTest.c
diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h
new file mode 100644
index 00000000..f18686ff
--- /dev/null
+++ b/src/opt/xyz/xyz.h
@@ -0,0 +1,94 @@
+/**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 $]
+
+***********************************************************************/
+
+#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
+ // 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 );
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzBuild.c b/src/opt/xyz/xyzBuild.c
new file mode 100644
index 00000000..e32721e7
--- /dev/null
+++ b/src/opt/xyz/xyzBuild.c
@@ -0,0 +1,379 @@
+/**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/opt/xyz/xyzCore.c b/src/opt/xyz/xyzCore.c
new file mode 100644
index 00000000..a48f749e
--- /dev/null
+++ b/src/opt/xyz/xyzCore.c
@@ -0,0 +1,697 @@
+/**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 );
+
+////////////////////////////////////////////////////////////////////////
+/// 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 );
+ 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 );
+
+ 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
+ Abc_NtkXyzCovers_rec( p, pObj, vBoundary );
+ 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) )
+ 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_NodeXyzPropagateEsop(p, pObj, pObj0, pObj1) ) // 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 []
+
+ 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
+ while ( 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
+ while ( 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
+ while ( 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;
+}
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h
new file mode 100644
index 00000000..22950bfd
--- /dev/null
+++ b/src/opt/xyz/xyzInt.h
@@ -0,0 +1,631 @@
+/**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 int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+/*=== xyzMinSop.c ==========================================================*/
+extern void Min_SopMinimize( Min_Man_t * p );
+extern int 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_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop );
+extern void Min_CoverCheck( Min_Man_t * p );
+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 );
+ 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 [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 [Check if the cube is equal or dist1 or contained.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew )
+{
+ Min_Cube_t * pCube;
+ int i;
+ // check identity
+ Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
+ if ( Min_CubesAreEqual( pCube, pNew ) )
+ return 1;
+ // check containment
+ for ( i = 0; i < (int)pNew->nLits; i++ )
+ Min_CoverForEachCube( p->ppStore[i], pCube )
+ if ( Min_CubeIsContained( pCube, pNew ) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check if the cube is equal or dist1 or contained.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew )
+{
+ Min_Cube_t * pCube;
+ Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
+ if ( Min_CubesDistOne( pCube, pNew, NULL ) )
+ return pCube;
+ return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzMan.c b/src/opt/xyz/xyzMan.c
new file mode 100644
index 00000000..844e8c13
--- /dev/null
+++ b/src/opt/xyz/xyzMan.c
@@ -0,0 +1,144 @@
+/**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/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c
new file mode 100644
index 00000000..114e28a6
--- /dev/null
+++ b/src/opt/xyz/xyzMinEsop.c
@@ -0,0 +1,277 @@
+/**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 []
+
+ 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;
+ while ( Min_EsopAddCube( p, pCube ) );
+ while ( 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
+ while ( Min_EsopAddCube( p, pCube ) );
+ while ( Min_EsopAddCube( p, pThis ) );
+ }
+// printf( "Pairs = %d ", nPairs );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds the cube to storage.]
+
+ Description [If the distance one cube is found, returns the transformed
+ cube. If there is no distance one, adds the given cube to storage.
+ Do not forget to clean the storage!]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Min_EsopAddCube( 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;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzMinMan.c b/src/opt/xyz/xyzMinMan.c
new file mode 100644
index 00000000..423564c1
--- /dev/null
+++ b/src/opt/xyz/xyzMinMan.c
@@ -0,0 +1,112 @@
+/**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 );
+ 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/opt/xyz/xyzMinSop.c b/src/opt/xyz/xyzMinSop.c
new file mode 100644
index 00000000..1c5951fe
--- /dev/null
+++ b/src/opt/xyz/xyzMinSop.c
@@ -0,0 +1,341 @@
+/**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++;
+ }
+ while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+
+// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
+}
+
+/**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;
+ 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;
+ // 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;
+
+
+ // 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 );
+
+ // skip the case when rewriting is impossible
+ if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 )
+ continue;
+
+ // if one of them does not have DC lit, move it
+ if ( v00 != 3 && v01 != 3 )
+ {
+ pTemp = pCube; pCube = pThis; pThis = pTemp;
+ Index = v00; v00 = v10; v10 = Index;
+ Index = v01; v01 = v11; v11 = Index;
+ }
+
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+ // 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 two reduced cubes
+
+ }
+ else // the first cube has DC lit
+ {
+ assert( v01 != 3 && v10 != 3 && v11 != 3 );
+ // try reduced and expanded cube
+ }
+ }
+// printf( "Pairs = %d ", nPairs );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+ return 1;
+}
+
+
+
+
+/**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 []
+
+***********************************************************************/
+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 []
+
+***********************************************************************/
+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 );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzMinUtil.c b/src/opt/xyz/xyzMinUtil.c
new file mode 100644
index 00000000..0aebb815
--- /dev/null
+++ b/src/opt/xyz/xyzMinUtil.c
@@ -0,0 +1,225 @@
+/**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_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
+{
+ char Buffer[1000];
+ Min_Cube_t * pCube;
+ FILE * pFile;
+ int i;
+ sprintf( Buffer, "%s.esop", pName );
+ 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 [Performs one round of rewriting using distance 2 cubes.]
+
+ 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 [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;
+ }
+ }
+ *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/opt/xyz/xyzTest.c b/src/opt/xyz/xyzTest.c
new file mode 100644
index 00000000..6c0a63f3
--- /dev/null
+++ b/src/opt/xyz/xyzTest.c
@@ -0,0 +1,51 @@
+/**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 []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk )
+{
+ return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+