summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abc/abc.h2
-rw-r--r--src/base/abc/abcObj.c25
-rw-r--r--src/base/abc/abcUtil.c2
-rw-r--r--src/base/abci/abc.c325
-rw-r--r--src/base/abci/abcCut.c2
-rw-r--r--src/base/abci/abcIvy.c4
-rw-r--r--src/base/abci/abcLut.c786
-rw-r--r--src/base/abci/abcPrint.c6
-rw-r--r--src/base/abci/abcReconv.c19
-rw-r--r--src/base/abci/module.make2
-rw-r--r--src/map/fpga/fpga.c33
-rw-r--r--src/map/fpga/fpga.h2
-rw-r--r--src/map/fpga/fpgaInt.h1
-rw-r--r--src/misc/extra/extra.h40
-rw-r--r--src/misc/extra/extraUtilTruth.c8
-rw-r--r--src/opt/fxu/fxu.c1
-rw-r--r--src/temp/ivy/ivyCut.c475
-rw-r--r--src/temp/ivy/module.make1
-rw-r--r--src/temp/xyz/module.make8
-rw-r--r--src/temp/xyz/xyz.h110
-rw-r--r--src/temp/xyz/xyzBuild.c379
-rw-r--r--src/temp/xyz/xyzCore.c1025
-rw-r--r--src/temp/xyz/xyzInt.h642
-rw-r--r--src/temp/xyz/xyzMan.c144
-rw-r--r--src/temp/xyz/xyzMinEsop.c299
-rw-r--r--src/temp/xyz/xyzMinMan.c113
-rw-r--r--src/temp/xyz/xyzMinSop.c615
-rw-r--r--src/temp/xyz/xyzMinUtil.c277
-rw-r--r--src/temp/xyz/xyzTest.c417
29 files changed, 5651 insertions, 112 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 29a95e46..15d3aa06 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -515,6 +515,7 @@ extern Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fIni
/*=== abcObj.c ==========================================================*/
extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj );
+extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
@@ -598,6 +599,7 @@ extern int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams
extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
extern void Abc_NtkManCutStop( Abc_ManCut_t * p );
extern Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p );
+extern Vec_Ptr_t * Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p );
extern Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
extern Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain );
extern void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 53886161..d993ca65 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -264,8 +264,33 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
Abc_ObjRecycle( pObj );
}
+/**Function*************************************************************
+
+ Synopsis [Deletes the node and MFFC of the node.]
+ Description []
+
+ SideEffects []
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj )
+{
+ Abc_Ntk_t * pNtk = pObj->pNtk;
+ Vec_Ptr_t * vNodes;
+ int i;
+ assert( !Abc_ObjIsComplement(pObj) );
+ assert( Abc_ObjFanoutNum(pObj) == 0 );
+ // delete fanins and fanouts
+ vNodes = Vec_PtrAlloc( 100 );
+ Abc_NodeCollectFanins( pObj, vNodes );
+ Abc_NtkDeleteObj( pObj );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
+ Abc_NtkDeleteObj_rec( pObj );
+ Vec_PtrFree( vNodes );
+}
/**Function*************************************************************
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 175b17f7..afa91c45 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -915,7 +915,7 @@ void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
/**Function*************************************************************
- Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]
+ Synopsis [Procedure used for sorting the nodes in increasing order of levels.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 075c64ee..64ee4596 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -31,96 +31,97 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static int Abc_CommandPrintStats ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintExdc ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintIo ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintLatch ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintSymms ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintUnate ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintAuto ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowAig ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowNtk ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandDemiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOneOutput ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOneNode ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigStore ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandUnmap ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAttach ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSuperChoice ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPga ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintStats ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintExdc ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintIo ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintLatch ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSymms ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintUnate ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintAuto ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowAig ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowNtk ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDemiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneOutput ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneNode ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigStore ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnmap ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAttach ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSuperChoice ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPga ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -209,6 +210,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "SC mapping", "unmap", Abc_CommandUnmap, 1 );
Cmd_CommandAdd( pAbc, "SC mapping", "attach", Abc_CommandAttach, 1 );
Cmd_CommandAdd( pAbc, "SC mapping", "sc", Abc_CommandSuperChoice, 1 );
+ Cmd_CommandAdd( pAbc, "SC mapping", "scl", Abc_CommandSuperChoiceLut, 1 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga", Abc_CommandFpga, 1 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "pga", Abc_CommandPga, 1 );
@@ -5494,15 +5496,121 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandSuperChoiceLut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c;
+ int nLutSize;
+ int nCutSizeMax;
+ int fVerbose;
+ extern int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fVerbose = 1;
+ nLutSize = 4;
+ nCutSizeMax = 10;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KNh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nLutSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nLutSize < 0 )
+ goto usage;
+ break;
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nCutSizeMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nCutSizeMax < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Superchoicing works only for the AIG representation (run \"strash\").\n" );
+ return 1;
+ }
+
+ // convert the network into the SOP network
+ pNtkRes = Abc_NtkAigToLogicSop( pNtk );
+
+ // get the new network
+ if ( !Abc_NtkSuperChoiceLut( pNtkRes, nLutSize, nCutSizeMax, fVerbose ) )
+ {
+ Abc_NtkDelete( pNtkRes );
+ fprintf( pErr, "Superchoicing has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: scl [-K num] [-N num] [-vh]\n" );
+ fprintf( pErr, "\t performs superchoicing for K-LUTs\n" );
+ fprintf( pErr, "\t (accumulate: \"r file.blif; b; scl; f -ac; wb file_sc.blif\")\n" );
+ fprintf( pErr, "\t (FPGA map: \"r file_sc.blif; ft; read_lut lutlibK; fpga\")\n" );
+ fprintf( pErr, "\t-K num : the number of LUT inputs [default = %d]\n", nLutSize );
+ fprintf( pErr, "\t-N num : the max size of the cut [default = %d]\n", nCutSizeMax );
+ fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char Buffer[100];
+ char LutSize[100];
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int fRecovery;
int fSwitching;
int fVerbose;
+ int nLutSize;
float DelayTarget;
extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fVerbose );
@@ -5516,8 +5624,9 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
fSwitching = 0;
fVerbose = 0;
DelayTarget =-1;
+ nLutSize =-1;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "apvhD" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "apvhDK" ) ) != EOF )
{
switch ( c )
{
@@ -5543,6 +5652,17 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( DelayTarget <= 0.0 )
goto usage;
break;
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nLutSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nLutSize < 0 )
+ goto usage;
+ break;
default:
goto usage;
}
@@ -5560,6 +5680,10 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
+ // create the new LUT library
+ if ( nLutSize >= 3 && nLutSize <= 6 )
+ Fpga_SetSimpleLutLib( nLutSize );
+
if ( !Abc_NtkIsStrash(pNtk) )
{
// strash and balance the network
@@ -5606,13 +5730,18 @@ usage:
sprintf( Buffer, "not used" );
else
sprintf( Buffer, "%.2f", DelayTarget );
- fprintf( pErr, "usage: fpga [-D float] [-apvh]\n" );
- fprintf( pErr, "\t performs FPGA mapping of the current network\n" );
- fprintf( pErr, "\t-a : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
- fprintf( pErr, "\t-p : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" );
- fprintf( pErr, "\t-D : sets the required time for the mapping [default = %s]\n", Buffer );
- fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
- fprintf( pErr, "\t-h : prints the command usage\n");
+ if ( nLutSize == -1 )
+ sprintf( LutSize, "library" );
+ else
+ sprintf( LutSize, "%d", nLutSize );
+ fprintf( pErr, "usage: fpga [-D float] [-K num] [-apvh]\n" );
+ fprintf( pErr, "\t performs FPGA mapping of the current network\n" );
+ fprintf( pErr, "\t-a : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
+ fprintf( pErr, "\t-p : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" );
+ fprintf( pErr, "\t-D float : sets the required time for the mapping [default = %s]\n", Buffer );
+ fprintf( pErr, "\t-K num : the number of LUT inputs [default = %s]%s\n", LutSize, (nLutSize == -1 ? " (type \"print_lut\")" : "") );
+ fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : prints the command usage\n");
return 1;
}
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 2752dc69..f5fe2629 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -314,7 +314,7 @@ void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
{
Abc_Obj_t * pFanin;
int fDagNode, fTriv, TreeCode = 0;
- assert( Abc_NtkIsStrash(pObj->pNtk) );
+// assert( Abc_NtkIsStrash(pObj->pNtk) );
assert( Abc_ObjFaninNum(pObj) == 2 );
// check if the node is a DAG node
fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj));
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 0108b520..a04f3d9c 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -85,7 +85,9 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
// Ivy_MffcTest( pMan );
Ivy_ManPrintStats( pMan );
- Ivy_ManSeqRewrite( pMan, 0, 0 );
+// Ivy_ManSeqRewrite( pMan, 0, 0 );
+// Ivy_ManTestCutsAlg( pMan );
+ Ivy_ManTestCutsBool( pMan );
Ivy_ManPrintStats( pMan );
// convert from the AIG manager
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
new file mode 100644
index 00000000..165d84c5
--- /dev/null
+++ b/src/base/abci/abcLut.c
@@ -0,0 +1,786 @@
+/**CFile****************************************************************
+
+ FileName [abcLut.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Superchoicing for K-LUTs.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcLut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SCL_LUT_MAX 6 // the maximum LUT size
+#define SCL_VARS_MAX 15 // the maximum number of variables
+#define SCL_NODE_MAX 1000 // the maximum number of nodes
+
+typedef struct Abc_ManScl_t_ Abc_ManScl_t;
+struct Abc_ManScl_t_
+{
+ // paramers
+ int nLutSize; // the LUT size
+ int nCutSizeMax; // the max number of leaves of the cone
+ int nNodesMax; // the max number of divisors in the cone
+ int nWords; // the number of machine words in sim info
+ // structural representation of the cone
+ Vec_Ptr_t * vLeaves; // leaves of the cut
+ Vec_Ptr_t * vVolume; // volume of the cut
+ int pBSet[SCL_VARS_MAX]; // bound set
+ // functional representation of the cone
+ unsigned * uTruth; // truth table of the cone
+ // representation of truth tables
+ unsigned ** uVars; // elementary truth tables
+ unsigned ** uSims; // truth tables of the nodes
+ unsigned ** uCofs; // truth tables of the cofactors
+};
+
+static Vec_Ptr_t * s_pLeaves = NULL;
+
+static Cut_Man_t * Abc_NtkStartCutManForScl( Abc_Ntk_t * pNtk, int nLutSize );
+static Abc_ManScl_t * Abc_ManSclStart( int nLutSize, int nCutSizeMax, int nNodesMax );
+static void Abc_ManSclStop( Abc_ManScl_t * p );
+static void Abc_NodeLutMap( Cut_Man_t * pManCuts, Abc_Obj_t * pObj );
+
+static Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * pManScl, Abc_Obj_t * pObj );
+static int Abc_NodeDecomposeStep( Abc_ManScl_t * pManScl );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs superchoicing for K-LUTs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int fVerbose )
+{
+ ProgressBar * pProgress;
+ Abc_ManCut_t * pManCut;
+ Abc_ManScl_t * pManScl;
+ Cut_Man_t * pManCuts;
+ Abc_Obj_t * pObj, * pFanin, * pObjTop;
+ int i, LevelMax, nNodes;
+ int nNodesTried, nNodesDec, nNodesExist, nNodesUsed;
+
+ assert( Abc_NtkIsSopLogic(pNtk) );
+ if ( nLutSize < 3 || nLutSize > SCL_LUT_MAX )
+ {
+ printf( "LUT size (%d) does not belong to the interval: 3 <= LUT size <= %d\n", nLutSize, SCL_LUT_MAX );
+ return 0;
+ }
+ if ( nCutSizeMax <= nLutSize || nCutSizeMax > SCL_VARS_MAX )
+ {
+ printf( "Cut size (%d) does not belong to the interval: LUT size (%d) < Cut size <= %d\n", nCutSizeMax, nLutSize, SCL_VARS_MAX );
+ return 0;
+ }
+
+ assert( nLutSize <= SCL_LUT_MAX );
+ assert( nCutSizeMax <= SCL_VARS_MAX );
+ nNodesTried = nNodesDec = nNodesExist = nNodesUsed = 0;
+
+ // set the delays of the CIs
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ pObj->Level = 0;
+
+//Abc_NtkGetLevelNum( pNtk );
+
+ // start the managers
+ pManScl = Abc_ManSclStart( nLutSize, nCutSizeMax, 1000 );
+ pManCuts = Abc_NtkStartCutManForScl( pNtk, nLutSize );
+ pManCut = Abc_NtkManCutStart( nCutSizeMax, 100000, 100000, 100000 );
+ s_pLeaves = Abc_NtkManCutReadCutSmall( pManCut );
+ pManScl->vVolume = Abc_NtkManCutReadVisited( pManCut );
+
+ // process each internal node (assuming topological order of nodes!!!)
+ nNodes = Abc_NtkObjNumMax(pNtk);
+ pProgress = Extra_ProgressBarStart( stdout, nNodes );
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+// if ( i != nNodes-1 )
+// continue;
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ if ( i >= nNodes )
+ break;
+ if ( Abc_ObjFaninNum(pObj) != 2 )
+ continue;
+ nNodesTried++;
+
+ // map this node using regular cuts
+// pObj->Level = 0;
+ Abc_NodeLutMap( pManCuts, pObj );
+ // compute the cut
+ pManScl->vLeaves = Abc_NodeFindCut( pManCut, pObj, 0 );
+ if ( Vec_PtrSize(pManScl->vLeaves) <= nLutSize )
+ continue;
+ // get the volume of the cut
+ if ( Vec_PtrSize(pManScl->vVolume) > SCL_NODE_MAX )
+ continue;
+ nNodesDec++;
+
+ // decompose the cut
+ pObjTop = Abc_NodeSuperChoiceLut( pManScl, pObj );
+ if ( pObjTop == NULL )
+ continue;
+ nNodesExist++;
+
+ // if there is no delay improvement, skip; otherwise, update level
+ if ( pObjTop->Level >= pObj->Level )
+ {
+ Abc_NtkDeleteObj_rec( pObjTop );
+ continue;
+ }
+ pObj->Level = pObjTop->Level;
+ nNodesUsed++;
+ }
+ Extra_ProgressBarStop( pProgress );
+
+ // delete the managers
+ Abc_ManSclStop( pManScl );
+ Abc_NtkManCutStop( pManCut );
+ Cut_ManStop( pManCuts );
+
+ // get the largest arrival time
+ LevelMax = 0;
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ {
+ pFanin = Abc_ObjFanin0( pObj );
+ // skip inv/buf
+ if ( Abc_ObjFaninNum(pFanin) == 1 )
+ pFanin = Abc_ObjFanin0( pFanin );
+ // get the new level
+ LevelMax = ABC_MAX( LevelMax, (int)pFanin->Level );
+ }
+
+ if ( fVerbose )
+ printf( "Try = %d. Dec = %d. Exist = %d. Use = %d. SUPER = %d levels of %d-LUTs.\n",
+ nNodesTried, nNodesDec, nNodesExist, nNodesUsed, LevelMax, nLutSize );
+// if ( fVerbose )
+// printf( "The network is superchoiced for %d levels of %d-LUTs.\n", LevelMax, nLutSize );
+
+ // clean the data field
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ pObj->pNext = NULL;
+
+ // check
+ if ( !Abc_NtkCheck( pNtk ) )
+ {
+ printf( "Abc_NtkSuperChoiceLut: The network check has failed.\n" );
+ return 0;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs LUT mapping of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeLutMap( Cut_Man_t * pManCuts, Abc_Obj_t * pObj )
+{
+ Cut_Cut_t * pCut;
+ Abc_Obj_t * pFanin;
+ int i, DelayMax;
+ pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCuts, pObj, 0, 0 );
+ assert( pCut != NULL );
+ assert( pObj->Level == 0 );
+ // go through the cuts
+ pObj->Level = ABC_INFINITY;
+ for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
+ {
+ DelayMax = 0;
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ {
+ pFanin = Abc_NtkObj( pObj->pNtk, pCut->pLeaves[i] );
+// assert( Abc_ObjIsCi(pFanin) || pFanin->Level > 0 ); // should hold if node ordering is topological
+ if ( DelayMax < (int)pFanin->Level )
+ DelayMax = pFanin->Level;
+ }
+ if ( (int)pObj->Level > DelayMax )
+ pObj->Level = DelayMax;
+ }
+ assert( pObj->Level < ABC_INFINITY );
+ pObj->Level++;
+// printf( "%d(%d) ", pObj->Id, pObj->Level );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the cut manager for rewriting.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkStartCutManForScl( Abc_Ntk_t * pNtk, int nLutSize )
+{
+ static Cut_Params_t Params, * pParams = &Params;
+ Cut_Man_t * pManCut;
+ Abc_Obj_t * pObj;
+ int i;
+ // start the cut manager
+ memset( pParams, 0, sizeof(Cut_Params_t) );
+ pParams->nVarsMax = nLutSize; // the max cut size ("k" of the k-feasible cuts)
+ pParams->nKeepMax = 500; // the max number of cuts kept at a node
+ pParams->fTruth = 0; // compute truth tables
+ pParams->fFilter = 1; // filter dominated cuts
+ pParams->fSeq = 0; // compute sequential cuts
+ pParams->fDrop = 0; // drop cuts on the fly
+ pParams->fVerbose = 0; // the verbosiness flag
+ pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
+ pManCut = Cut_ManStart( pParams );
+ if ( pParams->fDrop )
+ Cut_ManSetFanoutCounts( pManCut, Abc_NtkFanoutCounts(pNtk) );
+ // set cuts for PIs
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ if ( Abc_ObjFanoutNum(pObj) > 0 )
+ Cut_NodeSetTriv( pManCut, pObj->Id );
+ return pManCut;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_ManScl_t * Abc_ManSclStart( int nLutSize, int nCutSizeMax, int nNodesMax )
+{
+ Abc_ManScl_t * p;
+ int i, k;
+ assert( sizeof(unsigned) == 4 );
+ p = ALLOC( Abc_ManScl_t, 1 );
+ memset( p, 0, sizeof(Abc_ManScl_t) );
+ p->nLutSize = nLutSize;
+ p->nCutSizeMax = nCutSizeMax;
+ p->nNodesMax = nNodesMax;
+ p->nWords = Extra_TruthWordNum(nCutSizeMax);
+ // allocate simulation info
+ p->uVars = (unsigned **)Extra_ArrayAlloc( nCutSizeMax, p->nWords, 4 );
+ p->uSims = (unsigned **)Extra_ArrayAlloc( nNodesMax, p->nWords, 4 );
+ p->uCofs = (unsigned **)Extra_ArrayAlloc( 2 << nLutSize, p->nWords, 4 );
+ memset( p->uVars[0], 0, nCutSizeMax * p->nWords * 4 );
+ // assign elementary truth tables
+ for ( k = 0; k < p->nCutSizeMax; k++ )
+ for ( i = 0; i < p->nWords * 32; i++ )
+ if ( i & (1 << k) )
+ p->uVars[k][i>>5] |= (1 << (i&31));
+ // other data structures
+// p->vBound = Vec_IntAlloc( nCutSizeMax );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_ManSclStop( Abc_ManScl_t * p )
+{
+// Vec_IntFree( p->vBound );
+ free( p->uVars );
+ free( p->uSims );
+ free( p->uCofs );
+ free( p );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs superchoicing for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Abc_NodeSuperChoiceTruth( Abc_ManScl_t * pManScl )
+{
+ Abc_Obj_t * pObj;
+ unsigned * puData0, * puData1, * puData;
+ char * pSop;
+ int i, k;
+ // set elementary truth tables
+ Vec_PtrForEachEntry( pManScl->vLeaves, pObj, i )
+ pObj->pNext = (Abc_Obj_t *)pManScl->uVars[i];
+ // compute truth tables for internal nodes
+ Vec_PtrForEachEntry( pManScl->vVolume, pObj, i )
+ {
+ // set storage for the node's simulation info
+ pObj->pNext = (Abc_Obj_t *)pManScl->uSims[i];
+ // get pointer to the simulation info
+ puData = (unsigned *)pObj->pNext;
+ puData0 = (unsigned *)Abc_ObjFanin0(pObj)->pNext;
+ puData1 = (unsigned *)Abc_ObjFanin1(pObj)->pNext;
+ // simulate
+ pSop = pObj->pData;
+ if ( pSop[0] == '0' && pSop[1] == '0' )
+ for ( k = 0; k < pManScl->nWords; k++ )
+ puData[k] = ~puData0[k] & ~puData1[k];
+ else if ( pSop[0] == '0' )
+ for ( k = 0; k < pManScl->nWords; k++ )
+ puData[k] = ~puData0[k] & puData1[k];
+ else if ( pSop[1] == '0' )
+ for ( k = 0; k < pManScl->nWords; k++ )
+ puData[k] = puData0[k] & ~puData1[k];
+ else
+ for ( k = 0; k < pManScl->nWords; k++ )
+ puData[k] = puData0[k] & puData1[k];
+ }
+ return puData;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs superchoicing for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect2_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vVolume )
+{
+ if ( pObj->fMarkC )
+ return;
+ pObj->fMarkC = 1;
+ assert( Abc_ObjFaninNum(pObj) == 2 );
+ Abc_NodeSuperChoiceCollect2_rec( Abc_ObjFanin0(pObj), vVolume );
+ Abc_NodeSuperChoiceCollect2_rec( Abc_ObjFanin1(pObj), vVolume );
+ Vec_PtrPush( vVolume, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs superchoicing for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect2( Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+ Abc_Obj_t * pObj;
+ int i;
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ pObj->fMarkC = 1;
+ Vec_PtrClear( vVolume );
+ Abc_NodeSuperChoiceCollect2_rec( pRoot, vVolume );
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ pObj->fMarkC = 0;
+ Vec_PtrForEachEntry( vVolume, pObj, i )
+ pObj->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs superchoicing for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+ if ( pObj->fMarkB )
+ {
+ Vec_PtrPush( vLeaves, pObj );
+ pObj->fMarkB = 0;
+ }
+ if ( pObj->fMarkC )
+ return;
+ pObj->fMarkC = 1;
+ assert( Abc_ObjFaninNum(pObj) == 2 );
+ Abc_NodeSuperChoiceCollect_rec( Abc_ObjFanin0(pObj), vLeaves, vVolume );
+ Abc_NodeSuperChoiceCollect_rec( Abc_ObjFanin1(pObj), vLeaves, vVolume );
+ Vec_PtrPush( vVolume, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs superchoicing for one node.]
+
+ Description [Orders the leaves topologically.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect( Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+ Abc_Obj_t * pObj;
+ int i, nLeaves;
+ nLeaves = Vec_PtrSize(vLeaves);
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ pObj->fMarkB = pObj->fMarkC = 1;
+ Vec_PtrClear( vVolume );
+ Vec_PtrClear( vLeaves );
+ Abc_NodeSuperChoiceCollect_rec( pRoot, vLeaves, vVolume );
+ assert( Vec_PtrSize(vLeaves) == nLeaves );
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ pObj->fMarkC = 0;
+ Vec_PtrForEachEntry( vVolume, pObj, i )
+ pObj->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs superchoicing for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeLeavesRemove( Vec_Ptr_t * vLeaves, unsigned uPhase, int nVars )
+{
+ int i;
+ for ( i = nVars - 1; i >= 0; i-- )
+ if ( uPhase & (1 << i) )
+ Vec_PtrRemove( vLeaves, Vec_PtrEntry(vLeaves, i) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs superchoicing for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NodeGetLevel( Abc_Obj_t * pObj )
+{
+ Abc_Obj_t * pFanin;
+ int i, Level;
+ Level = 0;
+ Abc_ObjForEachFanin( pObj, pFanin, i )
+ Level = ABC_MAX( Level, (int)pFanin->Level );
+ return Level + 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs superchoicing for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * p, Abc_Obj_t * pObj )
+{
+ Abc_Obj_t * pFanin, * pObjNew;
+ int i, nVars, uSupport, nSuppVars;
+ // collect the cone using DFS (excluding leaves)
+ Abc_NodeSuperChoiceCollect2( pObj, p->vLeaves, p->vVolume );
+ assert( Vec_PtrEntryLast(p->vVolume) == pObj );
+ // compute the truth table
+ p->uTruth = Abc_NodeSuperChoiceTruth( p );
+ // get the support of this truth table
+ nVars = Vec_PtrSize(p->vLeaves);
+ uSupport = Extra_TruthSupport(p->uTruth, nVars);
+ nSuppVars = Extra_WordCountOnes(uSupport);
+ assert( nSuppVars <= nVars );
+ if ( nSuppVars == 0 )
+ {
+ pObj->Level = 0;
+ return NULL;
+ }
+ if ( nSuppVars == 1 )
+ {
+ // find the variable
+ for ( i = 0; i < nVars; i++ )
+ if ( uSupport & (1 << i) )
+ break;
+ assert( i < nVars );
+ pFanin = Vec_PtrEntry( p->vLeaves, i );
+ pObj->Level = pFanin->Level;
+ return NULL;
+ }
+ // support-minimize the truth table
+ if ( nSuppVars != nVars )
+ {
+ Extra_TruthShrink( p->uCofs[0], p->uTruth, nSuppVars, nVars, uSupport );
+ Extra_TruthCopy( p->uTruth, p->uCofs[0], nVars );
+ Abc_NodeLeavesRemove( p->vLeaves, ((1 << nVars) - 1) & ~uSupport, nVars );
+ }
+// return NULL;
+ // decompose the truth table recursively
+ while ( Vec_PtrSize(p->vLeaves) > p->nLutSize )
+ if ( !Abc_NodeDecomposeStep( p ) )
+ {
+ Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
+ if ( Abc_ObjIsNode(pFanin) && Abc_ObjFanoutNum(pFanin) == 0 )
+ Abc_NtkDeleteObj_rec( pFanin );
+ return NULL;
+ }
+ // create the topmost node
+ pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+ Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
+ Abc_ObjAddFanin( pObjNew, pFanin );
+ // create the function
+ pObjNew->pData = Abc_SopCreateFromTruth( pObj->pNtk->pManFunc, Vec_PtrSize(p->vLeaves), p->uTruth ); // need ISOP
+ pObjNew->Level = Abc_NodeGetLevel( pObjNew );
+ return pObjNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Procedure used for sorting the nodes in increasing order of levels.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NodeCompareLevelsInc( int * pp1, int * pp2 )
+{
+ Abc_Obj_t * pNode1, * pNode2;
+ pNode1 = Vec_PtrEntry(s_pLeaves, *pp1);
+ pNode2 = Vec_PtrEntry(s_pLeaves, *pp2);
+ if ( pNode1->Level < pNode2->Level )
+ return -1;
+ if ( pNode1->Level > pNode2->Level )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Selects the earliest arriving nodes from the array.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeDecomposeSort( Abc_Obj_t ** pLeaves, int nVars, int * pBSet, int nLutSize )
+{
+ Abc_Obj_t * pTemp[SCL_VARS_MAX];
+ int i, k, kBest, LevelMin;
+ assert( nLutSize < nVars );
+ assert( nVars <= SCL_VARS_MAX );
+ // copy nodes into the internal storage
+// printf( "(" );
+ for ( i = 0; i < nVars; i++ )
+ {
+ pTemp[i] = pLeaves[i];
+// printf( " %d", pLeaves[i]->Level );
+ }
+// printf( " )\n" );
+ // choose one node at a time
+ for ( i = 0; i < nLutSize; i++ )
+ {
+ kBest = -1;
+ LevelMin = ABC_INFINITY;
+ for ( k = 0; k < nVars; k++ )
+ if ( pTemp[k] && LevelMin > (int)pTemp[k]->Level )
+ {
+ LevelMin = pTemp[k]->Level;
+ kBest = k;
+ }
+ pBSet[i] = kBest;
+ pTemp[kBest] = NULL;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs superchoicing for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NodeDecomposeStep( Abc_ManScl_t * p )
+{
+ static char pCofClasses[1<<SCL_LUT_MAX][1<<SCL_LUT_MAX];
+ static char nCofClasses[1<<SCL_LUT_MAX];
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pObjNew, * pFanin, * pNodesNew[SCL_LUT_MAX];
+ unsigned * pTruthCof, * pTruthClass, * pTruth, uPhase;
+ int i, k, c, v, w, nVars, nVarsNew, nClasses, nCofs;
+ // set the network
+ pNtk = ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, 0))->pNtk;
+ // find the earliest nodes
+ nVars = Vec_PtrSize(p->vLeaves);
+ assert( nVars > p->nLutSize );
+/*
+ for ( v = 0; v < nVars; v++ )
+ p->pBSet[v] = v;
+ qsort( (void *)p->pBSet, nVars, sizeof(int),
+ (int (*)(const void *, const void *)) Abc_NodeCompareLevelsInc );
+*/
+ Abc_NodeDecomposeSort( (Abc_Obj_t **)Vec_PtrArray(p->vLeaves), Vec_PtrSize(p->vLeaves), p->pBSet, p->nLutSize );
+ assert( ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, p->pBSet[0]))->Level <=
+ ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, p->pBSet[1]))->Level );
+ // cofactor w.r.t. the selected variables
+ Extra_TruthCopy( p->uCofs[1], p->uTruth, nVars );
+ c = 2;
+ for ( v = 0; v < p->nLutSize; v++ )
+ for ( k = 0; k < (1<<v); k++ )
+ {
+ Extra_TruthCopy( p->uCofs[c], p->uCofs[c/2], nVars );
+ Extra_TruthCopy( p->uCofs[c+1], p->uCofs[c/2], nVars );
+ Extra_TruthCofactor0( p->uCofs[c], nVars, p->pBSet[v] );
+ Extra_TruthCofactor1( p->uCofs[c+1], nVars, p->pBSet[v] );
+ c += 2;
+ }
+ assert( c == (2 << p->nLutSize) );
+ // count unique cofactors
+ nClasses = 0;
+ nCofs = (1 << p->nLutSize);
+ for ( i = 0; i < nCofs; i++ )
+ {
+ pTruthCof = p->uCofs[ nCofs + i ];
+ for ( k = 0; k < nClasses; k++ )
+ {
+ pTruthClass = p->uCofs[ nCofs + pCofClasses[k][0] ];
+ if ( Extra_TruthIsEqual( pTruthCof, pTruthClass, nVars ) )
+ {
+ pCofClasses[k][ nCofClasses[k]++ ] = i;
+ break;
+ }
+ }
+ if ( k != nClasses )
+ continue;
+ // not found
+ pCofClasses[nClasses][0] = i;
+ nCofClasses[nClasses] = 1;
+ nClasses++;
+ if ( nClasses > nCofs/2 )
+ return 0;
+ }
+ // the number of cofactors is acceptable
+ nVarsNew = Extra_Base2Log( nClasses );
+ assert( nVarsNew < p->nLutSize );
+ // create the remainder truth table
+ // for each class of cofactors, multiply cofactor truth table by its code
+ Extra_TruthClear( p->uTruth, nVars );
+ for ( k = 0; k < nClasses; k++ )
+ {
+ pTruthClass = p->uCofs[ nCofs + pCofClasses[k][0] ];
+ for ( v = 0; v < nVarsNew; v++ )
+ if ( k & (1 << v) )
+ Extra_TruthAnd( pTruthClass, pTruthClass, p->uVars[p->pBSet[v]], nVars );
+ else
+ Extra_TruthSharp( pTruthClass, pTruthClass, p->uVars[p->pBSet[v]], nVars );
+ Extra_TruthOr( p->uTruth, p->uTruth, pTruthClass, nVars );
+ }
+ // create nodes
+ pTruth = p->uCofs[0];
+ for ( v = 0; v < nVarsNew; v++ )
+ {
+ Extra_TruthClear( pTruth, p->nLutSize );
+ for ( k = 0; k < nClasses; k++ )
+ if ( k & (1 << v) )
+ for ( i = 0; i < nCofClasses[k]; i++ )
+ {
+ pTruthCof = p->uCofs[1];
+ Extra_TruthFill( pTruthCof, p->nLutSize );
+ for ( w = 0; w < p->nLutSize; w++ )
+ if ( pCofClasses[k][i] & (1 << (p->nLutSize-1-w)) )
+ Extra_TruthAnd( pTruthCof, pTruthCof, p->uVars[w], p->nLutSize );
+ else
+ Extra_TruthSharp( pTruthCof, pTruthCof, p->uVars[w], p->nLutSize );
+ Extra_TruthOr( pTruth, pTruth, pTruthCof, p->nLutSize );
+ }
+ // implement the node
+ pObjNew = Abc_NtkCreateNode( pNtk );
+ for ( i = 0; i < p->nLutSize; i++ )
+ {
+ pFanin = Vec_PtrEntry( p->vLeaves, p->pBSet[i] );
+ Abc_ObjAddFanin( pObjNew, pFanin );
+ }
+ // create the function
+ pObjNew->pData = Abc_SopCreateFromTruth( pNtk->pManFunc, p->nLutSize, pTruth ); // need ISOP
+ pObjNew->Level = Abc_NodeGetLevel( pObjNew );
+ pNodesNew[v] = pObjNew;
+ }
+ // put the new nodes back into the list
+ for ( v = 0; v < nVarsNew; v++ )
+ Vec_PtrWriteEntry( p->vLeaves, p->pBSet[v], pNodesNew[v] );
+ // compute the variables that should be removed
+ uPhase = 0;
+ for ( v = nVarsNew; v < p->nLutSize; v++ )
+ uPhase |= (1 << p->pBSet[v]);
+ // remove entries from the array
+ Abc_NodeLeavesRemove( p->vLeaves, uPhase, nVars );
+ // update truth table
+ Extra_TruthShrink( p->uCofs[0], p->uTruth, nVars - p->nLutSize + nVarsNew, nVars, ((1 << nVars) - 1) & ~uPhase );
+ Extra_TruthCopy( p->uTruth, p->uCofs[0], nVars );
+ assert( !Extra_TruthVarInSupport( p->uTruth, nVars, nVars - p->nLutSize + nVarsNew ) );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index f95591ab..48b9eeda 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -135,18 +135,18 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
}
*/
-/*
+
// print the statistic into a file
{
FILE * pTable;
- pTable = fopen( "stats.txt", "a+" );
+ pTable = fopen( "fpga_stats.txt", "a+" );
fprintf( pTable, "%s ", pNtk->pName );
fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
fprintf( pTable, "%d ", Abc_AigGetLevelNum(pNtk) );
fprintf( pTable, "\n" );
fclose( pTable );
}
-*/
+
/*
// print the statistic into a file
{
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index e5b9e024..10400129 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -321,7 +321,8 @@ int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int
{
CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit );
//printf( " Fanin %s has cost %d.\n", Abc_ObjName(pNode), CostCur );
- if ( CostBest > CostCur )
+ if ( CostBest > CostCur ||
+ (CostBest == CostCur && pNode->Level > pFaninBest->Level) )
{
CostBest = CostCur;
pFaninBest = pNode;
@@ -643,6 +644,22 @@ Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p )
SeeAlso []
***********************************************************************/
+Vec_Ptr_t * Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p )
+{
+ return p->vNodeLeaves;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the leaves of the cone.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p )
{
return p->vVisited;
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index c297180d..5d35678d 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -11,7 +11,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcFraig.c \
src/base/abci/abcFxu.c \
src/base/abci/abcGen.c \
- src/base/abci/abcIvy.c \
+ src/base/abci/abcLut.c \
src/base/abci/abcMap.c \
src/base/abci/abcMiter.c \
src/base/abci/abcNtbdd.c \
diff --git a/src/map/fpga/fpga.c b/src/map/fpga/fpga.c
index c663aa74..be817713 100644
--- a/src/map/fpga/fpga.c
+++ b/src/map/fpga/fpga.c
@@ -235,6 +235,39 @@ usage:
return 1; /* error exit */
}
+/**Function*************************************************************
+
+ Synopsis [Sets simple LUT library.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fpga_SetSimpleLutLib( int nLutSize )
+{
+ Fpga_LutLib_t s_LutLib6 = { "lutlib", 6, {0,1,1,1,1,1,1}, {0,1,1,1,1,1,1} };
+ Fpga_LutLib_t s_LutLib5 = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} };
+ Fpga_LutLib_t s_LutLib4 = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} };
+ Fpga_LutLib_t s_LutLib3 = { "lutlib", 3, {0,1,1,1}, {0,1,1,1} };
+ Fpga_LutLib_t * pLutLib;
+ assert( nLutSize >= 3 && nLutSize <= 6 );
+ switch ( nLutSize )
+ {
+ case 3: pLutLib = &s_LutLib3; break;
+ case 4: pLutLib = &s_LutLib4; break;
+ case 5: pLutLib = &s_LutLib5; break;
+ case 6: pLutLib = &s_LutLib6; break;
+ default: pLutLib = NULL; break;
+ }
+ if ( pLutLib == NULL )
+ return;
+ Fpga_LutLibFree( Abc_FrameReadLibLut() );
+ Abc_FrameSetLibLut( Fpga_LutLibDup(pLutLib) );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/map/fpga/fpga.h b/src/map/fpga/fpga.h
index bbb95984..ee65f7a8 100644
--- a/src/map/fpga/fpga.h
+++ b/src/map/fpga/fpga.h
@@ -156,6 +156,8 @@ extern int Fpga_CutVolume( Fpga_Cut_t * pCut );
extern int Fpga_ManCheckConsistency( Fpga_Man_t * p );
extern void Fpga_ManCleanData0( Fpga_Man_t * pMan );
extern Fpga_NodeVec_t * Fpga_CollectNodeTfo( Fpga_Man_t * pMan, Fpga_Node_t * pNode );
+/*=== fpga.c =============================================================*/
+extern void Fpga_SetSimpleLutLib( int nLutSize );
#ifdef __cplusplus
}
diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h
index 3a35d6dc..318def25 100644
--- a/src/map/fpga/fpgaInt.h
+++ b/src/map/fpga/fpgaInt.h
@@ -28,7 +28,6 @@
#include <stdlib.h>
#include <string.h>
#include "extra.h"
-#include "fraig.h"
#include "fpga.h"
////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index d404dbc6..9f3b4cc7 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -417,12 +417,40 @@ static inline int Extra_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVar
return 0;
return 1;
}
+static inline int Extra_TruthIsConst0( unsigned * pIn, int nVars )
+{
+ int w;
+ for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+ if ( pIn[w] )
+ return 0;
+ return 1;
+}
+static inline int Extra_TruthIsConst1( unsigned * pIn, int nVars )
+{
+ int w;
+ for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+ if ( pIn[w] != ~(unsigned)0 )
+ return 0;
+ return 1;
+}
static inline void Extra_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn[w];
}
+static inline void Extra_TruthClear( unsigned * pOut, int nVars )
+{
+ int w;
+ for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+ pOut[w] = 0;
+}
+static inline void Extra_TruthFill( unsigned * pOut, int nVars )
+{
+ int w;
+ for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+ pOut[w] = ~(unsigned)0;
+}
static inline void Extra_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
@@ -435,6 +463,18 @@ static inline void Extra_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned *
for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn0[w] & pIn1[w];
}
+static inline void Extra_TruthOr( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+ int w;
+ for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+ pOut[w] = pIn0[w] | pIn1[w];
+}
+static inline void Extra_TruthSharp( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+ int w;
+ for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+ pOut[w] = pIn0[w] & ~pIn1[w];
+}
static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
diff --git a/src/misc/extra/extraUtilTruth.c b/src/misc/extra/extraUtilTruth.c
index a0c58025..a80c0d3d 100644
--- a/src/misc/extra/extraUtilTruth.c
+++ b/src/misc/extra/extraUtilTruth.c
@@ -184,8 +184,8 @@ void Extra_TruthSwapAdjacentVars2( unsigned * pIn, unsigned * pOut, int nVars, i
Synopsis [Expands the truth table according to the phase.]
Description [The input and output truth tables are in pIn/pOut. The current number
- of variables is nVars. The total number of variables in nVarsAll. The last variable
- (Phase) contains shows how the variables should be moved.]
+ of variables is nVars. The total number of variables in nVarsAll. The last argument
+ (Phase) contains shows where the variables should go.]
SideEffects []
@@ -218,8 +218,8 @@ void Extra_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAl
Synopsis [Shrinks the truth table according to the phase.]
Description [The input and output truth tables are in pIn/pOut. The current number
- of variables is nVars. The total number of variables in nVarsAll. The last variable
- (Phase) contains shows how the variables should be moved.]
+ of variables is nVars. The total number of variables in nVarsAll. The last argument
+ (Phase) contains shows what variables should remain.]
SideEffects []
diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index 169fb218..a92ef934 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -17,7 +17,6 @@
***********************************************************************/
#include "fxuInt.h"
-//#include "mvc.h"
#include "fxu.h"
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
index a8fd148b..57720e17 100644
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@@ -198,6 +198,481 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi
assert( Vec_IntSize(vFront) <= nSize );
}
+
+
+/**Function*************************************************************
+
+ Synopsis [Comparison for node pointers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManFindAlgCutCompare( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
+{
+ if ( *pp1 < *pp2 )
+ return -1;
+ if ( *pp1 > *pp2 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computing one algebraic cut.]
+
+ Description [Returns 1 if the tree-leaves of this node where traversed
+ and found to have no external references (and have not been collected).
+ Returns 0 if the tree-leaves have external references and are collected.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pRoot, Ivy_Type_t Type, Vec_Ptr_t * vFront )
+{
+ int RetValue0, RetValue1;
+ Ivy_Obj_t * pRootR = Ivy_Regular(pRoot);
+ assert( Type != IVY_EXOR || !Ivy_IsComplement(pRoot) );
+ // if the node is a buffer skip through it
+ if ( Ivy_ObjIsBuf(pRootR) )
+ return Ivy_ManFindAlgCut_rec( Ivy_NotCond(Ivy_ObjChild0(pRootR), Ivy_IsComplement(pRoot)), Type, vFront );
+ // if the node is the end of the tree, return
+ if ( Ivy_IsComplement(pRoot) || Ivy_ObjIsCi(pRoot) || Ivy_ObjType(pRoot) != Type )
+ {
+ if ( Ivy_ObjRefs(pRootR) == 1 )
+ return 1;
+ assert( Ivy_ObjRefs(pRootR) > 1 );
+ Vec_PtrPush( vFront, pRoot );
+ return 0;
+ }
+ // branch on the node
+ assert( Ivy_ObjIsNode(pRoot) );
+ RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjChild0(pRoot), Type, vFront );
+ RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjChild1(pRoot), Type, vFront );
+ // the case when both have no external referenced
+ if ( RetValue0 && RetValue1 )
+ {
+ if ( Ivy_ObjRefs(pRoot) == 1 )
+ return 1;
+ assert( Ivy_ObjRefs(pRoot) > 1 );
+ Vec_PtrPush( vFront, pRoot );
+ return 0;
+ }
+ // the case when one of them has external references
+ if ( RetValue0 )
+ Vec_PtrPush( vFront, Ivy_ObjChild0(pRoot) );
+ if ( RetValue1 )
+ Vec_PtrPush( vFront, Ivy_ObjChild1(pRoot) );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computing one algebraic cut.]
+
+ Description [Algebraic cut stops when we hit (a) CI, (b) complemented edge,
+ (c) boundary of different gates. Returns 1 if this is a pure tree.
+ Returns -1 if the contant 0 is detected. Return 0 if the array can be used.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront )
+{
+ Ivy_Obj_t * pObj, * pPrev;
+ int RetValue, i, k;
+ assert( !Ivy_IsComplement(pRoot) );
+ // clear the frontier and collect the nodes
+ Vec_PtrClear( vFront );
+ RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront );
+ // return if the node is the root of a tree
+ if ( RetValue == 1 )
+ return 1;
+ // sort the entries to in increasing order
+ Vec_PtrSort( vFront, Ivy_ManFindAlgCutCompare );
+ // remove duplicated
+ k = 1;
+ Vec_PtrForEachEntryStart( vFront, pObj, i, 1 )
+ {
+ pPrev = (k == 0 ? NULL : Vec_PtrEntry(vFront, k-1));
+ if ( pObj == pPrev )
+ {
+ if ( Ivy_ObjIsExor(pRoot) )
+ k--;
+ continue;
+ }
+ if ( pObj == Ivy_Not(pPrev) )
+ return -1;
+ Vec_PtrWriteEntry( vFront, k++, pObj );
+ }
+ if ( k == 0 )
+ return -1;
+ Vec_PtrShrink( vFront, k );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_ManTestCutsAlg( Ivy_Man_t * p )
+{
+ Vec_Ptr_t * vFront;
+ Ivy_Obj_t * pObj, * pTemp;
+ int i, k, RetValue;
+ vFront = Vec_PtrAlloc( 100 );
+ Ivy_ManForEachObj( p, pObj, i )
+ {
+ if ( !Ivy_ObjIsNode(pObj) )
+ continue;
+ if ( Ivy_ObjIsMuxType(pObj) )
+ {
+ printf( "m " );
+ continue;
+ }
+ if ( pObj->Id == 509 )
+ {
+ int y = 0;
+ }
+
+ RetValue = Ivy_ManFindAlgCut( pObj, vFront );
+ if ( Ivy_ObjIsExor(pObj) )
+ printf( "x" );
+ if ( RetValue == -1 )
+ printf( "Const0 " );
+ else if ( RetValue == 1 || Vec_PtrSize(vFront) <= 2 )
+ printf( ". " );
+ else
+ printf( "%d ", Vec_PtrSize(vFront) );
+
+ printf( "( " );
+ Vec_PtrForEachEntry( vFront, pTemp, k )
+ printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
+ printf( ")\n" );
+
+ if ( Vec_PtrSize(vFront) == 5 )
+ {
+ int x = 0;
+ }
+ }
+ printf( "\n" );
+ Vec_PtrFree( vFront );
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Computing Boolean cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManFindBoolCut_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume, Ivy_Obj_t * pPivot )
+{
+ int RetValue0, RetValue1;
+ if ( pObj == pPivot )
+ {
+ Vec_PtrPushUnique( vLeaves, pObj );
+ Vec_PtrPushUnique( vVolume, pObj );
+ return 1;
+ }
+ if ( pObj->fMarkA )
+ return 0;
+
+// assert( !Ivy_ObjIsCi(pObj) );
+ if ( Ivy_ObjIsCi(pObj) )
+ return 0;
+
+ if ( Ivy_ObjIsBuf(pObj) )
+ {
+ RetValue0 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
+ if ( !RetValue0 )
+ return 0;
+ Vec_PtrPushUnique( vVolume, pObj );
+ return 1;
+ }
+ assert( Ivy_ObjIsNode(pObj) );
+ RetValue0 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
+ RetValue1 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin1(pObj), vLeaves, vVolume, pPivot );
+ if ( !RetValue0 && !RetValue1 )
+ return 0;
+ // add new leaves
+ if ( !RetValue0 )
+ {
+ Vec_PtrPushUnique( vLeaves, Ivy_ObjFanin0(pObj) );
+ Vec_PtrPushUnique( vVolume, Ivy_ObjFanin0(pObj) );
+ }
+ if ( !RetValue1 )
+ {
+ Vec_PtrPushUnique( vLeaves, Ivy_ObjFanin1(pObj) );
+ Vec_PtrPushUnique( vVolume, Ivy_ObjFanin1(pObj) );
+ }
+ Vec_PtrPushUnique( vVolume, pObj );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the cost of one node (how many new nodes are added.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManFindBoolCutCost( Ivy_Obj_t * pObj )
+{
+ int Cost;
+ // make sure the node is in the construction zone
+ assert( pObj->fMarkA == 1 );
+ // cannot expand over the PI node
+ if ( Ivy_ObjIsCi(pObj) )
+ return 999;
+ // always expand over the buffer
+ if ( Ivy_ObjIsBuf(pObj) )
+ return !Ivy_ObjFanin0(pObj)->fMarkA;
+ // get the cost of the cone
+ Cost = (!Ivy_ObjFanin0(pObj)->fMarkA) + (!Ivy_ObjFanin1(pObj)->fMarkA);
+ // return the number of nodes to be added to the leaves if this node is removed
+ return Cost;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computing Boolean cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolume, Vec_Ptr_t * vLeaves )
+{
+ Ivy_Obj_t * pObj, * pFaninC, * pFanin0, * pFanin1, * pPivot;
+ int RetValue, LevelLimit, Lev, k;
+ assert( !Ivy_IsComplement(pRoot) );
+ // clear the frontier and collect the nodes
+ Vec_PtrClear( vFront );
+ Vec_PtrClear( vVolume );
+ if ( Ivy_ObjIsMuxType(pRoot) )
+ pFaninC = Ivy_ObjRecognizeMux( pRoot, &pFanin0, &pFanin1 );
+ else
+ {
+ pFaninC = NULL;
+ pFanin0 = Ivy_ObjFanin0(pRoot);
+ pFanin1 = Ivy_ObjFanin1(pRoot);
+ }
+ // start cone A
+ pFanin0->fMarkA = 1;
+ Vec_PtrPush( vFront, pFanin0 );
+ Vec_PtrPush( vVolume, pFanin0 );
+ // start cone B
+ pFanin1->fMarkB = 1;
+ Vec_PtrPush( vFront, pFanin1 );
+ Vec_PtrPush( vVolume, pFanin1 );
+ // iteratively expand until the common node (pPivot) is found or limit is reached
+ assert( Ivy_ObjLevel(pRoot) == Ivy_ObjLevelNew(pRoot) );
+ pPivot = NULL;
+ LevelLimit = IVY_MAX( Ivy_ObjLevel(pRoot) - 10, 1 );
+ for ( Lev = Ivy_ObjLevel(pRoot) - 1; Lev >= LevelLimit; Lev-- )
+ {
+ while ( 1 )
+ {
+ // find the next node to expand on this level
+ Vec_PtrForEachEntry( vFront, pObj, k )
+ if ( (int)pObj->Level == Lev )
+ break;
+ if ( k == Vec_PtrSize(vFront) )
+ break;
+ assert( (int)pObj->Level <= Lev );
+ assert( pObj->fMarkA ^ pObj->fMarkB );
+ // remove the old node
+ Vec_PtrRemove( vFront, pObj );
+
+ // expand this node
+ pFanin0 = Ivy_ObjFanin0(pObj);
+ if ( !pFanin0->fMarkA && !pFanin0->fMarkB )
+ {
+ Vec_PtrPush( vFront, pFanin0 );
+ Vec_PtrPush( vVolume, pFanin0 );
+ }
+ // mark the new nodes
+ if ( pObj->fMarkA )
+ pFanin0->fMarkA = 1;
+ if ( pObj->fMarkB )
+ pFanin0->fMarkB = 1;
+
+ if ( Ivy_ObjIsBuf(pObj) )
+ {
+ if ( pFanin0->fMarkA && pFanin0->fMarkB )
+ {
+ pPivot = pFanin0;
+ break;
+ }
+ continue;
+ }
+
+ // expand this node
+ pFanin1 = Ivy_ObjFanin1(pObj);
+ if ( !pFanin1->fMarkA && !pFanin1->fMarkB )
+ {
+ Vec_PtrPush( vFront, pFanin1 );
+ Vec_PtrPush( vVolume, pFanin1 );
+ }
+ // mark the new nodes
+ if ( pObj->fMarkA )
+ pFanin1->fMarkA = 1;
+ if ( pObj->fMarkB )
+ pFanin1->fMarkB = 1;
+
+ // consider if it is time to quit
+ if ( pFanin0->fMarkA && pFanin0->fMarkB )
+ {
+ pPivot = pFanin0;
+ break;
+ }
+ if ( pFanin1->fMarkA && pFanin1->fMarkB )
+ {
+ pPivot = pFanin1;
+ break;
+ }
+ }
+ if ( pPivot != NULL )
+ break;
+ }
+ if ( pPivot == NULL )
+ return 0;
+ // if the MUX control is defined, it should not be
+ if ( pFaninC && !pFaninC->fMarkA && !pFaninC->fMarkB )
+ Vec_PtrPush( vFront, pFaninC );
+ // clean the markings
+ Vec_PtrForEachEntry( vVolume, pObj, k )
+ pObj->fMarkA = pObj->fMarkB = 0;
+
+ // mark the nodes on the frontier (including the pivot)
+ Vec_PtrForEachEntry( vFront, pObj, k )
+ pObj->fMarkA = 1;
+ // cut exists, collect all the nodes on the shortest path to the pivot
+ Vec_PtrClear( vLeaves );
+ Vec_PtrClear( vVolume );
+ RetValue = Ivy_ManFindBoolCut_rec( pRoot, vLeaves, vVolume, pPivot );
+ assert( RetValue == 1 );
+ // unmark the nodes on the frontier (including the pivot)
+ Vec_PtrForEachEntry( vFront, pObj, k )
+ pObj->fMarkA = 0;
+
+ // mark the nodes in the volume
+ Vec_PtrForEachEntry( vVolume, pObj, k )
+ pObj->fMarkA = 1;
+ // expand the cut without increasing its size
+ while ( 1 )
+ {
+ Vec_PtrForEachEntry( vLeaves, pObj, k )
+ if ( Ivy_ManFindBoolCutCost(pObj) < 2 )
+ break;
+ if ( k == Vec_PtrSize(vLeaves) )
+ break;
+ // the node can be expanded
+ // remove the old node
+ Vec_PtrRemove( vLeaves, pObj );
+ // expand this node
+ pFanin0 = Ivy_ObjFanin0(pObj);
+ if ( !pFanin0->fMarkA )
+ {
+ pFanin0->fMarkA = 1;
+ Vec_PtrPush( vVolume, pFanin0 );
+ Vec_PtrPush( vLeaves, pFanin0 );
+ }
+ if ( Ivy_ObjIsBuf(pObj) )
+ continue;
+ // expand this node
+ pFanin1 = Ivy_ObjFanin1(pObj);
+ if ( !pFanin1->fMarkA )
+ {
+ pFanin1->fMarkA = 1;
+ Vec_PtrPush( vVolume, pFanin1 );
+ Vec_PtrPush( vLeaves, pFanin1 );
+ }
+ }
+ // unmark the nodes in the volume
+ Vec_PtrForEachEntry( vVolume, pObj, k )
+ pObj->fMarkA = 0;
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_ManTestCutsBool( Ivy_Man_t * p )
+{
+ Vec_Ptr_t * vFront, * vVolume, * vLeaves;
+ Ivy_Obj_t * pObj, * pTemp;
+ int i, k, RetValue;
+ vFront = Vec_PtrAlloc( 100 );
+ vVolume = Vec_PtrAlloc( 100 );
+ vLeaves = Vec_PtrAlloc( 100 );
+ Ivy_ManForEachObj( p, pObj, i )
+ {
+ if ( !Ivy_ObjIsNode(pObj) )
+ continue;
+ if ( Ivy_ObjIsMuxType(pObj) )
+ {
+ printf( "m" );
+ continue;
+ }
+ if ( Ivy_ObjIsExor(pObj) )
+ printf( "x" );
+ RetValue = Ivy_ManFindBoolCut( pObj, vFront, vVolume, vLeaves );
+ if ( RetValue == 0 )
+ printf( "- " );
+ else
+ printf( "%d ", Vec_PtrSize(vLeaves) );
+/*
+ printf( "( " );
+ Vec_PtrForEachEntry( vFront, pTemp, k )
+ printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
+ printf( ")\n" );
+*/
+ }
+ printf( "\n" );
+ Vec_PtrFree( vFront );
+ Vec_PtrFree( vVolume );
+ Vec_PtrFree( vLeaves );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make
index d59a3fa3..beadb8b9 100644
--- a/src/temp/ivy/module.make
+++ b/src/temp/ivy/module.make
@@ -5,6 +5,7 @@ SRC += src/temp/ivy/ivyBalance.c \
src/temp/ivy/ivyDfs.c \
src/temp/ivy/ivyDsd.c \
src/temp/ivy/ivyMan.c \
+ src/temp/ivy/ivyMulti.c \
src/temp/ivy/ivyObj.c \
src/temp/ivy/ivyOper.c \
src/temp/ivy/ivyRewrite.c \
diff --git a/src/temp/xyz/module.make b/src/temp/xyz/module.make
new file mode 100644
index 00000000..ae7dab0f
--- /dev/null
+++ b/src/temp/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/temp/xyz/xyz.h b/src/temp/xyz/xyz.h
new file mode 100644
index 00000000..4fec2150
--- /dev/null
+++ b/src/temp/xyz/xyz.h
@@ -0,0 +1,110 @@
+/**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
new file mode 100644
index 00000000..e32721e7
--- /dev/null
+++ b/src/temp/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/temp/xyz/xyzCore.c b/src/temp/xyz/xyzCore.c
new file mode 100644
index 00000000..e5089788
--- /dev/null
+++ b/src/temp/xyz/xyzCore.c
@@ -0,0 +1,1025 @@
+/**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
new file mode 100644
index 00000000..656612aa
--- /dev/null
+++ b/src/temp/xyz/xyzInt.h
@@ -0,0 +1,642 @@
+/**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
new file mode 100644
index 00000000..844e8c13
--- /dev/null
+++ b/src/temp/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/temp/xyz/xyzMinEsop.c b/src/temp/xyz/xyzMinEsop.c
new file mode 100644
index 00000000..839e2410
--- /dev/null
+++ b/src/temp/xyz/xyzMinEsop.c
@@ -0,0 +1,299 @@
+/**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
new file mode 100644
index 00000000..20314698
--- /dev/null
+++ b/src/temp/xyz/xyzMinMan.c
@@ -0,0 +1,113 @@
+/**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
new file mode 100644
index 00000000..a5d57c66
--- /dev/null
+++ b/src/temp/xyz/xyzMinSop.c
@@ -0,0 +1,615 @@
+/**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
new file mode 100644
index 00000000..9ec5f83f
--- /dev/null
+++ b/src/temp/xyz/xyzMinUtil.c
@@ -0,0 +1,277 @@
+/**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
new file mode 100644
index 00000000..38580790
--- /dev/null
+++ b/src/temp/xyz/xyzTest.c
@@ -0,0 +1,417 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
+