From 6b44b18e69f4e26249140e10c459615a77b32fc5 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 4 Aug 2006 08:01:00 -0700
Subject: Version abc60804
---
src/base/abci/abc.c | 34 ++-
src/base/abci/abcIvy.c | 6 +-
src/base/abci/abcSat.c | 2 +-
src/base/abci/abcTiming.c | 5 +-
src/base/main/mainFrame.c | 4 +-
src/misc/nm/nmApi.c | 7 +-
src/misc/nm/nmInt.h | 2 +
src/misc/nm/nmTable.c | 106 +++++++--
src/misc/vec/vecInt.h | 22 ++
src/opt/cut/abcCut.c | 491 ++++++++++++++++++++++++++++++++++++++++++
src/opt/cut/cut60720.zip | Bin 0 -> 31142 bytes
src/opt/cut/cut60721.zip | Bin 0 -> 42872 bytes
src/opt/cut/cutNode.c | 4 +-
src/sat/msat/msatActivity.c | 2 +-
src/sat/msat/msatInt.h | 2 +-
src/sat/msat/msatSolverApi.c | 8 +-
src/temp/ivy/ivy.h | 15 +-
src/temp/ivy/ivyCheck.c | 90 +++++++-
src/temp/ivy/ivyCut.c | 27 ++-
src/temp/ivy/ivyDfs.c | 4 +-
src/temp/ivy/ivyFanout.c | 293 ++++++++++++-------------
src/temp/ivy/ivyIsop.c | 223 +++++++++----------
src/temp/ivy/ivyMan.c | 14 +-
src/temp/ivy/ivyMem.c | 6 +-
src/temp/ivy/ivyObj.c | 51 +++--
src/temp/ivy/ivyResyn.c | 41 ++++
src/temp/ivy/ivyRwrPre.c | 2 +-
src/temp/ivy/ivySeq.c | 2 +-
src/temp/ivy/ivyUtil.c | 4 +-
src/temp/player/player.h | 3 +-
src/temp/player/playerMan.c | 2 +-
src/temp/player/playerToAbc.c | 67 ++++--
src/temp/vec/vecInt.h | 44 ++--
src/temp/vec/vecPtr.h | 30 ++-
34 files changed, 1230 insertions(+), 383 deletions(-)
create mode 100644 src/opt/cut/abcCut.c
create mode 100644 src/opt/cut/cut60720.zip
create mode 100644 src/opt/cut/cut60721.zip
(limited to 'src')
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7bee7f40..bb8f5658 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4487,22 +4487,26 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
int nPlaMax;
int RankCost;
int fFastMode;
+ int fRewriting;
+ int fSynthesis;
int fVerbose;
-// extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
- extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose );
+// extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fEsop, bool fSop, bool fInvs, bool fVerbose );
+ extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nLutMax = 8;
- nPlaMax = 128;
- RankCost = 96000;
- fFastMode = 0;
- fVerbose = 0;
+ nLutMax = 8;
+ nPlaMax = 128;
+ RankCost = 96000;
+ fFastMode = 1;
+ fRewriting = 1;
+ fSynthesis = 0;
+ fVerbose = 1;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfrsvh" ) ) != EOF )
{
switch ( c )
{
@@ -4542,6 +4546,12 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
fFastMode ^= 1;
break;
+ case 'r':
+ fRewriting ^= 1;
+ break;
+ case 's':
+ fSynthesis ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -4570,8 +4580,8 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// run the command
-// pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fUseInvs, fVerbose );
- pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fVerbose );
+// pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
+ pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -4582,12 +4592,14 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: xyz [-L num] [-P num] [-R num] [-fvh]\n" );
+ fprintf( pErr, "usage: xyz [-L num] [-P num] [-R num] [-frsvh]\n" );
fprintf( pErr, "\t specilized LUT/PLA decomposition\n" );
fprintf( pErr, "\t-L num : maximum number of LUT inputs (2<=num<=8) [default = %d]\n", nLutMax );
fprintf( pErr, "\t-P num : maximum number of PLA inputs/cubes (8<=num<=128) [default = %d]\n", nPlaMax );
fprintf( pErr, "\t-R num : maximum are of one decomposition rank [default = %d]\n", RankCost );
fprintf( pErr, "\t-f : toggle using fast LUT mapping mode [default = %s]\n", fFastMode? "yes": "no" );
+ fprintf( pErr, "\t-r : toggle using one pass of AIG rewriting [default = %s]\n", fRewriting? "yes": "no" );
+ fprintf( pErr, "\t-s : toggle using synthesis by AIG rewriting [default = %s]\n", fSynthesis? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index a3ffcf4e..380b3f8b 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -343,9 +343,11 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
// Ivy_ManRequiredLevels( pMan );
- Pla_ManFastLutMap( pMan, 8 );
- Ivy_ManStop( pMan );
+// Pla_ManFastLutMap( pMan, 8 );
+// Ivy_ManStop( pMan );
return NULL;
+
+
/*
// convert from the AIG manager
pNtkAig = Abc_NtkFromAig( pNtk, pMan );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index f447516f..b8491d06 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -408,7 +408,7 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo
int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax )
{
// nLevelMax = ((nLevelMax)/2)*3;
- assert( pObj->Level <= nLevelMax );
+ assert( (int)pObj->Level <= nLevelMax );
// return (int)(100000000.0 * pow(0.999, nLevelMax - pObj->Level));
return (int)(100000000.0 * (1 + 0.01 * pObj->Level));
// return (int)(100000000.0 / ((nLevelMax)/2)*3 - pObj->Level);
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index a40954bd..d2d731d9 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -647,9 +647,10 @@ void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk )
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj, * pFanout;
int i, k, nLevelsCur;
- assert( Abc_NtkIsStrash(pNtk) );
+// assert( Abc_NtkIsStrash(pNtk) );
// remember the maximum number of direct levels
- pNtk->LevelMax = Abc_AigGetLevelNum(pNtk);
+// pNtk->LevelMax = Abc_AigGetLevelNum(pNtk);
+ pNtk->LevelMax = Abc_NtkGetLevelNum(pNtk);
// start the reverse levels
pNtk->vLevelsR = Vec_IntAlloc( 0 );
Vec_IntFill( pNtk->vLevelsR, Abc_NtkObjNumMax(pNtk), 0 );
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index ecf77f70..5c4a0675 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -136,11 +136,11 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
{
extern void Rwt_ManGlobalStop();
extern void undefine_cube_size();
- extern void Ivy_TruthManStop();
+// extern void Ivy_TruthManStop();
// Abc_HManStop();
undefine_cube_size();
Rwt_ManGlobalStop();
- Ivy_TruthManStop();
+// Ivy_TruthManStop();
if ( p->pManDec ) Dec_ManStop( p->pManDec );
if ( p->dd ) Extra_StopManager( p->dd );
Abc_FrameDeleteAllNetworks( p );
diff --git a/src/misc/nm/nmApi.c b/src/misc/nm/nmApi.c
index e44d1ef9..120dbe91 100644
--- a/src/misc/nm/nmApi.c
+++ b/src/misc/nm/nmApi.c
@@ -46,10 +46,10 @@ Nm_Man_t * Nm_ManCreate( int nSize )
p = ALLOC( Nm_Man_t, 1 );
memset( p, 0, sizeof(Nm_Man_t) );
// set the parameters
- p->nSizeFactor = 4; // determined how much larger the table should be compared to data in it
- p->nGrowthFactor = 4; // determined how much the table grows after resizing
+ p->nSizeFactor = 2; // determined how much larger the table should be compared to data in it
+ p->nGrowthFactor = 3; // determined how much the table grows after resizing
// allocate and clean the bins
- p->nBins = Cudd_PrimeNm(p->nSizeFactor*nSize);
+ p->nBins = Cudd_PrimeNm(nSize);
p->pBinsI2N = ALLOC( Nm_Entry_t *, p->nBins );
p->pBinsN2I = ALLOC( Nm_Entry_t *, p->nBins );
memset( p->pBinsI2N, 0, sizeof(Nm_Entry_t *) * p->nBins );
@@ -127,6 +127,7 @@ char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, char * pName, char * pSuffix
nEntrySize = sizeof(Nm_Entry_t) + strlen(pName) + (pSuffix?strlen(pSuffix):0) + 1;
nEntrySize = (nEntrySize / 4 + ((nEntrySize % 4) > 0)) * 4;
pEntry = (Nm_Entry_t *)Extra_MmFlexEntryFetch( p->pMem, nEntrySize );
+ pEntry->pNextI2N = pEntry->pNextN2I = NULL;
pEntry->ObjId = ObjId;
sprintf( pEntry->Name, "%s%s", pName, pSuffix? pSuffix : "" );
// add the entry to the hash table
diff --git a/src/misc/nm/nmInt.h b/src/misc/nm/nmInt.h
index 43901993..8356a4cb 100644
--- a/src/misc/nm/nmInt.h
+++ b/src/misc/nm/nmInt.h
@@ -45,6 +45,8 @@ typedef struct Nm_Entry_t_ Nm_Entry_t;
struct Nm_Entry_t_
{
int ObjId; // object ID
+ Nm_Entry_t * pNextI2N; // the next entry in the ID hash table
+ Nm_Entry_t * pNextN2I; // the next entry in the name hash table
char Name[0]; // name of the object
};
diff --git a/src/misc/nm/nmTable.c b/src/misc/nm/nmTable.c
index 4243244d..4eeaf610 100644
--- a/src/misc/nm/nmTable.c
+++ b/src/misc/nm/nmTable.c
@@ -44,7 +44,7 @@ static unsigned Nm_HashString( char * pName, int TableSize )
};
unsigned i, Key = 0;
for ( i = 0; pName[i] != '\0'; i++ )
- Key ^= s_Primes[i%10]*pName[i]*pName[i]*pName[i];
+ Key ^= s_Primes[i%10]*pName[i]*pName[i];
return Key % TableSize;
}
@@ -67,13 +67,16 @@ static void Nm_ManResize( Nm_Man_t * p );
***********************************************************************/
int Nm_ManTableAdd( Nm_Man_t * p, Nm_Entry_t * pEntry )
{
- int i;
+ Nm_Entry_t ** ppSpot;
+// int i;
// resize the tables if needed
- if ( p->nEntries * p->nSizeFactor > p->nBins )
+// if ( p->nEntries * p->nSizeFactor > p->nBins )
+ if ( p->nEntries > p->nBins * p->nSizeFactor )
{
// Nm_ManPrintTables( p );
Nm_ManResize( p );
}
+/*
// hash it by ID
for ( i = Nm_HashNumber(pEntry->ObjId, p->nBins); p->pBinsI2N[i]; i = (i+1) % p->nBins )
if ( p->pBinsI2N[i] == pEntry )
@@ -86,6 +89,15 @@ int Nm_ManTableAdd( Nm_Man_t * p, Nm_Entry_t * pEntry )
return 0;
assert( p->pBinsN2I[i] == NULL );
p->pBinsN2I[i] = pEntry;
+*/
+ ppSpot = p->pBinsI2N + Nm_HashNumber(pEntry->ObjId, p->nBins);
+ pEntry->pNextI2N = *ppSpot;
+ *ppSpot = pEntry;
+
+ ppSpot = p->pBinsN2I + Nm_HashString(pEntry->Name, p->nBins);
+ pEntry->pNextN2I = *ppSpot;
+ *ppSpot = pEntry;
+
// report successfully added entry
p->nEntries++;
return 1;
@@ -121,10 +133,16 @@ int Nm_ManTableDelete( Nm_Man_t * p, Nm_Entry_t * pEntry )
***********************************************************************/
Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId )
{
- int i;
+ Nm_Entry_t * pEntry;
+// int i;
+/*
for ( i = Nm_HashNumber(ObjId, p->nBins); p->pBinsI2N[i]; i = (i+1) % p->nBins )
if ( p->pBinsI2N[i]->ObjId == ObjId )
return p->pBinsI2N[i];
+*/
+ for ( pEntry = p->pBinsI2N[ Nm_HashNumber(ObjId, p->nBins) ]; pEntry; pEntry = pEntry->pNextI2N )
+ if ( pEntry->ObjId == ObjId )
+ return pEntry;
return NULL;
}
@@ -141,9 +159,10 @@ Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId )
***********************************************************************/
Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** ppSecond )
{
- Nm_Entry_t * pFirst, * pSecond;
- int i, Counter = 0;
+ Nm_Entry_t * pFirst, * pSecond, * pEntry;
+ int Counter = 0;
pFirst = pSecond = NULL;
+/*
for ( i = Nm_HashString(pName, p->nBins); p->pBinsN2I[i]; i = (i+1) % p->nBins )
if ( strcmp(p->pBinsN2I[i]->Name, pName) == 0 )
{
@@ -158,12 +177,60 @@ Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** pp
Counter++;
if ( Counter > 100 )
printf( "%d ", Counter );
+*/
+ for ( pEntry = p->pBinsN2I[ Nm_HashString(pName, p->nBins) ]; pEntry; pEntry = pEntry->pNextN2I )
+ if ( strcmp(pEntry->Name, pName) == 0 )
+ {
+ if ( pFirst == NULL )
+ pFirst = pEntry;
+ else if ( pSecond == NULL )
+ pSecond = pEntry;
+ else
+ assert( 0 ); // name appears more than 2 times
+ }
+
// save the names
if ( ppSecond )
*ppSecond = pSecond;
return pFirst;
}
+/**Function*************************************************************
+
+ Synopsis [Profiles hash tables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nm_ManProfile( Nm_Man_t * p )
+{
+ Nm_Entry_t * pEntry;
+ int Counter, e;
+ printf( "I2N table: " );
+ for ( e = 0; e < p->nBins; e++ )
+ {
+ Counter = 0;
+ for ( pEntry = p->pBinsI2N[e]; pEntry; pEntry = pEntry->pNextI2N )
+ Counter++;
+ printf( "%d ", Counter );
+ }
+ printf( "\n" );
+ printf( "N2I table: " );
+ for ( e = 0; e < p->nBins; e++ )
+ {
+ Counter = 0;
+ for ( pEntry = p->pBinsN2I[e]; pEntry; pEntry = pEntry->pNextN2I )
+ Counter++;
+ printf( "%d ", Counter );
+ }
+ printf( "\n" );
+}
+
+
/**Function*************************************************************
@@ -178,8 +245,8 @@ Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** pp
***********************************************************************/
void Nm_ManResize( Nm_Man_t * p )
{
- Nm_Entry_t ** pBinsNewI2N, ** pBinsNewN2I, * pEntry;
- int nBinsNew, Counter, e, i, clk;
+ Nm_Entry_t ** pBinsNewI2N, ** pBinsNewN2I, * pEntry, * pEntry2, ** ppSpot;
+ int nBinsNew, Counter, e, clk;
clk = clock();
// get the new table size
@@ -192,12 +259,13 @@ clk = clock();
// rehash the entries from the old table
Counter = 0;
for ( e = 0; e < p->nBins; e++ )
+ for ( pEntry = p->pBinsI2N[e], pEntry2 = pEntry? pEntry->pNextI2N : NULL;
+ pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNextI2N : NULL )
{
- pEntry = p->pBinsI2N[e];
- if ( pEntry == NULL )
- continue;
- Counter++;
-
+// pEntry = p->pBinsI2N[e];
+// if ( pEntry == NULL )
+// continue;
+/*
// hash it by ID
for ( i = Nm_HashNumber(pEntry->ObjId, nBinsNew); pBinsNewI2N[i]; i = (i+1) % nBinsNew )
if ( pBinsNewI2N[i] == pEntry )
@@ -210,6 +278,16 @@ clk = clock();
assert( 0 );
assert( pBinsNewN2I[i] == NULL );
pBinsNewN2I[i] = pEntry;
+*/
+ ppSpot = pBinsNewI2N + Nm_HashNumber(pEntry->ObjId, nBinsNew);
+ pEntry->pNextI2N = *ppSpot;
+ *ppSpot = pEntry;
+
+ ppSpot = pBinsNewN2I + Nm_HashString(pEntry->Name, nBinsNew);
+ pEntry->pNextN2I = *ppSpot;
+ *ppSpot = pEntry;
+
+ Counter++;
}
assert( Counter == p->nEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", p->nBins, nBinsNew );
@@ -220,10 +298,10 @@ clk = clock();
p->pBinsI2N = pBinsNewI2N;
p->pBinsN2I = pBinsNewN2I;
p->nBins = nBinsNew;
+// Nm_ManProfile( p );
}
-
/**Function*************************************************************
Synopsis [Returns the smallest prime larger than the number.]
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 4f193cf2..4a97fc91 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -581,6 +581,28 @@ static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry )
return 0;
}
+/**Function*************************************************************
+
+ Synopsis [Returns the pointer to the next nWords entries in the vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned * Vec_IntFetch( Vec_Int_t * p, int nWords )
+{
+ p->nSize += nWords;
+ if ( p->nSize > p->nCap )
+ {
+// Vec_IntGrow( p, 2 * p->nSize );
+ return NULL;
+ }
+ return ((unsigned *)p->pArray) + p->nSize - nWords;
+}
+
/**Function*************************************************************
Synopsis [Returns the last entry and removes it from the list.]
diff --git a/src/opt/cut/abcCut.c b/src/opt/cut/abcCut.c
new file mode 100644
index 00000000..b4b879a3
--- /dev/null
+++ b/src/opt/cut/abcCut.c
@@ -0,0 +1,491 @@
+/**CFile****************************************************************
+
+ FileName [abcCut.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Interface to cut computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "cut.h"
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq );
+static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq );
+
+
+extern int nTotal, nGood, nEqual;
+
+// temporary
+//Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) { return NULL; }
+Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk )
+{
+ Vec_Int_t * vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 );
+ int i;
+ Abc_Obj_t * pObj;
+
+// Abc_NtkForEachCi( pNtk, pObj, i )
+// Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+// if ( Abc_ObjIsNode(pObj) && (rand() % 4 == 0) )
+ if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj) && (rand() % 3 == 0) )
+ Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+ }
+ return vAttrs;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts for the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
+{
+ ProgressBar * pProgress;
+ Cut_Man_t * p;
+ Abc_Obj_t * pObj, * pNode;
+ Vec_Ptr_t * vNodes;
+ Vec_Int_t * vChoices;
+ int i;
+ int clk = clock();
+
+ extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk );
+ extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
+
+ nTotal = nGood = nEqual = 0;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ // start the manager
+ pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
+ p = Cut_ManStart( pParams );
+ // compute node attributes if local or global cuts are requested
+ if ( pParams->fGlobal || pParams->fLocal )
+ {
+ extern Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk );
+ Cut_ManSetNodeAttrs( p, Abc_NtkGetNodeAttributes(pNtk) );
+ }
+ // prepare for cut dropping
+ if ( pParams->fDrop )
+ Cut_ManSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) );
+ // set cuts for PIs
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ if ( Abc_ObjFanoutNum(pObj) > 0 )
+ Cut_NodeSetTriv( p, pObj->Id );
+ // compute cuts for internal nodes
+ vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs
+ vChoices = Vec_IntAlloc( 100 );
+ pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ // when we reached a CO, it is time to deallocate the cuts
+ if ( Abc_ObjIsCo(pObj) )
+ {
+ if ( pParams->fDrop )
+ Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+ continue;
+ }
+ // skip constant node, it has no cuts
+ if ( Abc_NodeIsConst(pObj) )
+ continue;
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ // compute the cuts to the internal node
+ Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree );
+ // consider dropping the fanins cuts
+ if ( pParams->fDrop )
+ {
+ Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+ Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId1(pObj) );
+ }
+ // add cuts due to choices
+ if ( Abc_NodeIsAigChoice(pObj) )
+ {
+ Vec_IntClear( vChoices );
+ for ( pNode = pObj; pNode; pNode = pNode->pData )
+ Vec_IntPush( vChoices, pNode->Id );
+ Cut_NodeUnionCuts( p, vChoices );
+ }
+ }
+ Extra_ProgressBarStop( pProgress );
+ Vec_PtrFree( vNodes );
+ Vec_IntFree( vChoices );
+PRT( "Total", clock() - clk );
+//Abc_NtkPrintCuts( p, pNtk, 0 );
+// Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
+
+ // temporary printout of stats
+ if ( nTotal )
+ printf( "Total cuts = %d. Good cuts = %d. Ratio = %5.2f\n", nTotal, nGood, ((double)nGood)/nTotal );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Cut computation using the oracle.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
+{
+ Abc_Obj_t * pObj;
+ Vec_Ptr_t * vNodes;
+ int i, clk = clock();
+ int fDrop = Cut_OracleReadDrop(p);
+
+ assert( Abc_NtkIsStrash(pNtk) );
+
+ // prepare cut droppping
+ if ( fDrop )
+ Cut_OracleSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) );
+
+ // set cuts for PIs
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ if ( Abc_ObjFanoutNum(pObj) > 0 )
+ Cut_OracleNodeSetTriv( p, pObj->Id );
+
+ // compute cuts for internal nodes
+ vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ // when we reached a CO, it is time to deallocate the cuts
+ if ( Abc_ObjIsCo(pObj) )
+ {
+ if ( fDrop )
+ Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+ continue;
+ }
+ // skip constant node, it has no cuts
+ if ( Abc_NodeIsConst(pObj) )
+ continue;
+ // compute the cuts to the internal node
+ Cut_OracleComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),
+ Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+ // consider dropping the fanins cuts
+ if ( fDrop )
+ {
+ Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+ Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId1(pObj) );
+ }
+ }
+ Vec_PtrFree( vNodes );
+//PRT( "Total", clock() - clk );
+//Abc_NtkPrintCuts_( p, pNtk, 0 );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts for the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
+{
+ Cut_Man_t * p;
+ Abc_Obj_t * pObj, * pNode;
+ int i, nIters, fStatus;
+ Vec_Int_t * vChoices;
+ int clk = clock();
+
+ assert( Abc_NtkIsSeq(pNtk) );
+ assert( pParams->fSeq );
+// assert( Abc_NtkIsDfsOrdered(pNtk) );
+
+ // start the manager
+ pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
+ pParams->nCutSet = Abc_NtkCutSetNodeNum( pNtk );
+ p = Cut_ManStart( pParams );
+
+ // set cuts for the constant node and the PIs
+ pObj = Abc_NtkConst1(pNtk);
+ if ( Abc_ObjFanoutNum(pObj) > 0 )
+ Cut_NodeSetTriv( p, pObj->Id );
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ {
+//printf( "Setting trivial cut %d.\n", pObj->Id );
+ Cut_NodeSetTriv( p, pObj->Id );
+ }
+ // label the cutset nodes and set their number in the array
+ // assign the elementary cuts to the cutset nodes
+ Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+ {
+ assert( pObj->fMarkC == 0 );
+ pObj->fMarkC = 1;
+ pObj->pCopy = (Abc_Obj_t *)i;
+ Cut_NodeSetTriv( p, pObj->Id );
+//printf( "Setting trivial cut %d.\n", pObj->Id );
+ }
+
+ // process the nodes
+ vChoices = Vec_IntAlloc( 100 );
+ for ( nIters = 0; nIters < 10; nIters++ )
+ {
+//printf( "ITERATION %d:\n", nIters );
+ // compute the cuts for the internal nodes
+ Abc_AigForEachAnd( pNtk, pObj, i )
+ {
+ Abc_NodeGetCutsSeq( p, pObj, nIters==0 );
+ // add cuts due to choices
+ if ( Abc_NodeIsAigChoice(pObj) )
+ {
+ Vec_IntClear( vChoices );
+ for ( pNode = pObj; pNode; pNode = pNode->pData )
+ Vec_IntPush( vChoices, pNode->Id );
+ Cut_NodeUnionCutsSeq( p, vChoices, (pObj->fMarkC ? (int)pObj->pCopy : -1), nIters==0 );
+ }
+ }
+ // merge the new cuts with the old cuts
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ Cut_NodeNewMergeWithOld( p, pObj->Id );
+ Abc_AigForEachAnd( pNtk, pObj, i )
+ Cut_NodeNewMergeWithOld( p, pObj->Id );
+ // for the cutset, transfer temp cuts to new cuts
+ fStatus = 0;
+ Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+ fStatus |= Cut_NodeTempTransferToNew( p, pObj->Id, i );
+ if ( fStatus == 0 )
+ break;
+ }
+ Vec_IntFree( vChoices );
+
+ // if the status is not finished, transfer new to old for the cutset
+ Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+ Cut_NodeNewMergeWithOld( p, pObj->Id );
+
+ // transfer the old cuts to the new positions
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ Cut_NodeOldTransferToNew( p, pObj->Id );
+
+ // unlabel the cutset nodes
+ Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+ pObj->fMarkC = 0;
+if ( pParams->fVerbose )
+{
+PRT( "Total", clock() - clk );
+printf( "Converged after %d iterations.\n", nIters );
+}
+//Abc_NtkPrintCuts( p, pNtk, 1 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts for the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
+{
+ void * pList;
+ if ( pList = Abc_NodeReadCuts( p, pObj ) )
+ return pList;
+ Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fDag, fTree );
+ Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fDag, fTree );
+ return Abc_NodeGetCuts( p, pObj, fDag, fTree );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts for the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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_ObjFaninNum(pObj) == 2 );
+
+
+ // check if the node is a DAG node
+ fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj));
+ // increment the counter of DAG nodes
+ if ( fDagNode ) Cut_ManIncrementDagNodes( p );
+ // add the trivial cut if the node is a DAG node, or if we compute all cuts
+ fTriv = fDagNode || !fDag;
+ // check if fanins are DAG nodes
+ if ( fTree )
+ {
+ pFanin = Abc_ObjFanin0(pObj);
+ TreeCode |= (Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin));
+ pFanin = Abc_ObjFanin1(pObj);
+ TreeCode |= ((Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin)) << 1);
+ }
+
+
+ // changes due to the global/local cut computation
+ {
+ Cut_Params_t * pParams = Cut_ManReadParams(p);
+ if ( pParams->fLocal )
+ {
+ Vec_Int_t * vNodeAttrs = Cut_ManReadNodeAttrs(p);
+ fDagNode = Vec_IntEntry( vNodeAttrs, pObj->Id );
+ if ( fDagNode ) Cut_ManIncrementDagNodes( p );
+// fTriv = fDagNode || !pParams->fGlobal;
+ fTriv = !Vec_IntEntry( vNodeAttrs, pObj->Id );
+ TreeCode = 0;
+ pFanin = Abc_ObjFanin0(pObj);
+ TreeCode |= Vec_IntEntry( vNodeAttrs, pFanin->Id );
+ pFanin = Abc_ObjFanin1(pObj);
+ TreeCode |= (Vec_IntEntry( vNodeAttrs, pFanin->Id ) << 1);
+ }
+ }
+ return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),
+ Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv, TreeCode );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts for the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv )
+{
+ int CutSetNum;
+ assert( Abc_NtkIsSeq(pObj->pNtk) );
+ assert( Abc_ObjFaninNum(pObj) == 2 );
+ fTriv = pObj->fMarkC ? 0 : fTriv;
+ CutSetNum = pObj->fMarkC ? (int)pObj->pCopy : -1;
+ Cut_NodeComputeCutsSeq( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),
+ Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj), fTriv, CutSetNum );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts for the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj )
+{
+ return Cut_NodeReadCutsNew( p, pObj->Id );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts for the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj )
+{
+ Cut_NodeFreeCuts( p, pObj->Id );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts for the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq )
+{
+ Cut_Man_t * pMan = p;
+ Cut_Cut_t * pList;
+ Abc_Obj_t * pObj;
+ int i;
+ printf( "Cuts of the network:\n" );
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ pList = Abc_NodeReadCuts( p, pObj );
+ printf( "Node %s:\n", Abc_ObjName(pObj) );
+ Cut_CutPrintList( pList, fSeq );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts for the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq )
+{
+ Cut_Man_t * pMan = p;
+ Cut_Cut_t * pList;
+ Abc_Obj_t * pObj;
+ pObj = Abc_NtkObj( pNtk, 2 * Abc_NtkObjNum(pNtk) / 3 );
+ pList = Abc_NodeReadCuts( p, pObj );
+ printf( "Node %s:\n", Abc_ObjName(pObj) );
+ Cut_CutPrintList( pList, fSeq );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cut60720.zip b/src/opt/cut/cut60720.zip
new file mode 100644
index 00000000..86ad6726
Binary files /dev/null and b/src/opt/cut/cut60720.zip differ
diff --git a/src/opt/cut/cut60721.zip b/src/opt/cut/cut60721.zip
new file mode 100644
index 00000000..d55ccfd0
Binary files /dev/null and b/src/opt/cut/cut60721.zip differ
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index adff525f..1f93b14b 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -399,11 +399,9 @@ p->timeMerge += clock() - clk;
// set the list at the node
Vec_PtrFillExtra( p->vCutsNew, Node + 1, NULL );
assert( Cut_NodeReadCutsNew(p, Node) == NULL );
-
/////
- pList->pNext = NULL;
+// pList->pNext = NULL;
/////
-
Cut_NodeWriteCutsNew( p, Node, pList );
// filter the cuts
//clk = clock();
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
index f808d9bc..23925669 100644
--- a/src/sat/msat/msatActivity.c
+++ b/src/sat/msat/msatActivity.c
@@ -46,7 +46,7 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
return;
Var = MSAT_LIT2VAR(Lit);
if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 )
-// if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pLevel[Var])) > 1e100 )
+// if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pActLevels[Var])) > 1e100 )
Msat_SolverVarRescaleActivity( p );
Msat_OrderUpdate( p->pOrder, Var );
}
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index 15932c67..7845ec0b 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -119,7 +119,7 @@ struct Msat_Solver_t_
double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay.
double * pdActivity; // A heuristic measurement of the activity of a variable.
- int * pLevels; // the levels of the variables
+ int * pActLevels; // the levels of the variables
double dVarInc; // Amount to bump next variable with.
double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
Msat_Order_t * pOrder; // Keeps track of the decision variable order.
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index 8c1542df..9317dcac 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -174,11 +174,11 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
p->dVarDecay = dVarDecay;
p->pdActivity = ALLOC( double, p->nVarsAlloc );
- p->pLevels = ALLOC( int, p->nVarsAlloc );
+ p->pActLevels = ALLOC( int, p->nVarsAlloc );
for ( i = 0; i < p->nVarsAlloc; i++ )
{
p->pdActivity[i] = 0;
- p->pLevels = 0;
+ p->pActLevels[i] = 0;
}
p->pAssigns = ALLOC( int, p->nVarsAlloc );
@@ -243,7 +243,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
p->nVarsAlloc = nVarsAlloc;
p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
- p->pLevels = REALLOC( int, p->pLevels, p->nVarsAlloc );
+ p->pActLevels = REALLOC( int, p->pActLevels, p->nVarsAlloc );
for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
p->pdActivity[i] = 0;
@@ -399,7 +399,7 @@ void Msat_SolverFree( Msat_Solver_t * p )
Msat_ClauseVecFree( p->vLearned );
FREE( p->pdActivity );
- FREE( p->pLevels );
+ FREE( p->pActLevels );
Msat_OrderFree( p->pOrder );
for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 7fb054f7..a36c795b 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -66,7 +66,7 @@ typedef enum {
} Ivy_Init_t;
// the AIG node
-struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit)
+struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) // 10 words - 16 words
{
int Id; // integer ID
int TravId; // traversal ID
@@ -81,6 +81,10 @@ struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit)
Ivy_Obj_t * pFanin0; // fanin
Ivy_Obj_t * pFanin1; // fanin
Ivy_Obj_t * pFanout; // fanout
+ Ivy_Obj_t * pNextFan0; // next fanout of the first fanin
+ Ivy_Obj_t * pNextFan1; // next fanout of the second fanin
+ Ivy_Obj_t * pPrevFan0; // prev fanout of the first fanin
+ Ivy_Obj_t * pPrevFan1; // prev fanout of the second fanin
Ivy_Obj_t * pEquiv; // equivalent node
};
@@ -106,7 +110,8 @@ struct Ivy_Man_t_
int nTravIds; // the traversal ID
int nLevelMax; // the maximum level
Vec_Int_t * vRequired; // required times
- Vec_Ptr_t * vFanouts; // representation of the fanouts
+// Vec_Ptr_t * vFanouts; // representation of the fanouts
+ int fFanout; // fanout is allocated
void * pData; // the temporary data
void * pCopy; // the temporary data
// memory management
@@ -384,6 +389,7 @@ extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t *
extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
/*=== ivyCheck.c ========================================================*/
extern int Ivy_ManCheck( Ivy_Man_t * p );
+extern int Ivy_ManCheckFanouts( Ivy_Man_t * p );
/*=== ivyCut.c ==========================================================*/
extern void Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize );
extern Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves );
@@ -407,12 +413,10 @@ extern void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Ob
extern void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout );
extern void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew );
extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray );
-extern Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
/*=== ivyIsop.c ==========================================================*/
-extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover );
-extern void Ivy_TruthManStop();
+extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth );
/*=== ivyMan.c ==========================================================*/
extern Ivy_Man_t * Ivy_ManStart();
extern void Ivy_ManStop( Ivy_Man_t * p );
@@ -450,6 +454,7 @@ extern Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, I
extern Ivy_Obj_t * Ivy_Miter( Ivy_Man_t * p, Vec_Ptr_t * vPairs );
extern Ivy_Obj_t * Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
/*=== ivyResyn.c =========================================================*/
+extern Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
/*=== ivyRewrite.c =========================================================*/
extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c
index 36222f72..ebae64ff 100644
--- a/src/temp/ivy/ivyCheck.c
+++ b/src/temp/ivy/ivyCheck.c
@@ -115,7 +115,7 @@ int Ivy_ManCheck( Ivy_Man_t * p )
if ( Ivy_ObjRefs(pObj) == 0 )
printf( "Ivy_ManCheck: Node with ID \"%d\" has no fanouts.\n", pObj->Id );
// check fanouts
- if ( p->vFanouts && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) )
+ if ( p->fFanout && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) )
printf( "Ivy_ManCheck: Node with ID \"%d\" has mismatch between the number of fanouts and refs.\n", pObj->Id );
}
// count the number of nodes in the table
@@ -124,9 +124,95 @@ int Ivy_ManCheck( Ivy_Man_t * p )
printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
return 0;
}
+// if ( !Ivy_ManCheckFanouts(p) )
+// return 0;
if ( !Ivy_ManIsAcyclic(p) )
return 0;
- return 1;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verifies the fanouts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManCheckFanouts( Ivy_Man_t * p )
+{
+ Vec_Ptr_t * vFanouts;
+ Ivy_Obj_t * pObj, * pFanout, * pFanin;
+ int i, k, RetValue = 1;
+ if ( !p->fFanout )
+ return 1;
+ vFanouts = Vec_PtrAlloc( 100 );
+ // make sure every fanin is a fanout
+ Ivy_ManForEachObj( p, pObj, i )
+ {
+ pFanin = Ivy_ObjFanin0(pObj);
+ if ( pFanin == NULL )
+ continue;
+ Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
+ if ( pFanout == pObj )
+ break;
+ if ( k == Vec_PtrSize(vFanouts) )
+ {
+ printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
+ RetValue = 0;
+ }
+
+ pFanin = Ivy_ObjFanin1(pObj);
+ if ( pFanin == NULL )
+ continue;
+ Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
+ if ( pFanout == pObj )
+ break;
+ if ( k == Vec_PtrSize(vFanouts) )
+ {
+ printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
+ RetValue = 0;
+ }
+ // check that the previous fanout has the same fanin
+ if ( pObj->pPrevFan0 )
+ {
+ if ( Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) &&
+ Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) &&
+ Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) &&
+ Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) )
+ {
+ printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan0->Id );
+ RetValue = 0;
+ }
+ }
+ // check that the previous fanout has the same fanin
+ if ( pObj->pPrevFan1 )
+ {
+ if ( Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) &&
+ Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) &&
+ Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) &&
+ Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) )
+ {
+ printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan1->Id );
+ RetValue = 0;
+ }
+ }
+ }
+ // make sure every fanout is a fanin
+ Ivy_ManForEachObj( p, pObj, i )
+ {
+ Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, k )
+ if ( Ivy_ObjFanin0(pFanout) != pObj && Ivy_ObjFanin1(pFanout) != pObj )
+ {
+ printf( "Node %d is a fanout of node %d but the fanin is not there.\n", pFanout->Id, pObj->Id );
+ RetValue = 0;
+ }
+ }
+ Vec_PtrFree( vFanouts );
+ return RetValue;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
index 56f872e9..65ba4aac 100644
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@@ -856,6 +856,24 @@ void Ivy_NodePrintCuts( Ivy_Store_t * pCutStore )
Ivy_NodePrintCut( pCutStore->pCuts + i );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Ivy_Obj_t * Ivy_ObjRealFanin( Ivy_Obj_t * pObj )
+{
+ if ( !Ivy_ObjIsBuf(pObj) )
+ return pObj;
+ return Ivy_ObjRealFanin( Ivy_ObjFanin0(pObj) );
+}
+
/**Function*************************************************************
Synopsis []
@@ -911,11 +929,14 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
continue;
Ivy_NodeCutHash( pCutNew );
*/
- iLeaf0 = Ivy_ObjFaninId0(pLeaf);
- iLeaf1 = Ivy_ObjFaninId1(pLeaf);
+ iLeaf0 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin0(pLeaf)) );
+ iLeaf1 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin1(pLeaf)) );
if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) )
continue;
- Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 );
+ if ( iLeaf0 > iLeaf1 )
+ Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf1, iLeaf0 );
+ else
+ Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 );
Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew );
if ( pCutStore->nCuts == IVY_CUT_LIMIT )
break;
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index 30671baf..7246ec25 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -265,7 +265,7 @@ int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
{
if ( Ivy_ObjIsCi(pNode) || Ivy_ObjIsConst1(pNode) )
return 1;
- assert( Ivy_ObjIsNode( pNode ) );
+ assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) );
// make sure the node is not visited
assert( !Ivy_ObjIsTravIdPrevious(p, pNode) );
// check if the node is part of the combinational loop
@@ -290,7 +290,7 @@ int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
}
}
// check if the fanin is visited
- if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) )
+ if ( Ivy_ObjIsNode(pNode) && !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) )
{
// traverse the fanin's cone searching for the loop
if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pNode)) )
diff --git a/src/temp/ivy/ivyFanout.c b/src/temp/ivy/ivyFanout.c
index 2295516d..3930186a 100644
--- a/src/temp/ivy/ivyFanout.c
+++ b/src/temp/ivy/ivyFanout.c
@@ -24,9 +24,96 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static inline int Ivy_FanoutIsArray( void * p ) { return (int )(((unsigned)p) & 01); }
-static inline Vec_Ptr_t * Ivy_FanoutGetArray( void * p ) { assert( Ivy_FanoutIsArray(p) ); return (Vec_Ptr_t *)((unsigned)(p) & ~01); }
-static inline Vec_Ptr_t * Ivy_FanoutSetArray( void * p ) { assert( !Ivy_FanoutIsArray(p) ); return (Vec_Ptr_t *)((unsigned)(p) ^ 01); }
+// getting hold of the next fanout of the node
+static inline Ivy_Obj_t * Ivy_ObjNextFanout( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+ assert( !Ivy_IsComplement(pObj) );
+ assert( !Ivy_IsComplement(pFanout) );
+ if ( pFanout == NULL )
+ return NULL;
+ if ( Ivy_ObjFanin0(pFanout) == pObj )
+ return pFanout->pNextFan0;
+ assert( Ivy_ObjFanin1(pFanout) == pObj );
+ return pFanout->pNextFan1;
+}
+
+// getting hold of the previous fanout of the node
+static inline Ivy_Obj_t * Ivy_ObjPrevFanout( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+ assert( !Ivy_IsComplement(pObj) );
+ assert( !Ivy_IsComplement(pFanout) );
+ if ( pFanout == NULL )
+ return NULL;
+ if ( Ivy_ObjFanin0(pFanout) == pObj )
+ return pFanout->pPrevFan0;
+ assert( Ivy_ObjFanin1(pFanout) == pObj );
+ return pFanout->pPrevFan1;
+}
+
+// getting hold of the place where the next fanout will be attached
+static inline Ivy_Obj_t ** Ivy_ObjNextFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+ assert( !Ivy_IsComplement(pObj) );
+ assert( !Ivy_IsComplement(pFanout) );
+ if ( Ivy_ObjFanin0(pFanout) == pObj )
+ return &pFanout->pNextFan0;
+ assert( Ivy_ObjFanin1(pFanout) == pObj );
+ return &pFanout->pNextFan1;
+}
+
+// getting hold of the place where the next fanout will be attached
+static inline Ivy_Obj_t ** Ivy_ObjPrevFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+ assert( !Ivy_IsComplement(pObj) );
+ assert( !Ivy_IsComplement(pFanout) );
+ if ( Ivy_ObjFanin0(pFanout) == pObj )
+ return &pFanout->pPrevFan0;
+ assert( Ivy_ObjFanin1(pFanout) == pObj );
+ return &pFanout->pPrevFan1;
+}
+
+// getting hold of the place where the next fanout will be attached
+static inline Ivy_Obj_t ** Ivy_ObjPrevNextFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+ Ivy_Obj_t * pTemp;
+ assert( !Ivy_IsComplement(pObj) );
+ assert( !Ivy_IsComplement(pFanout) );
+ pTemp = Ivy_ObjPrevFanout(pObj, pFanout);
+ if ( pTemp == NULL )
+ return &pObj->pFanout;
+ if ( Ivy_ObjFanin0(pTemp) == pObj )
+ return &pTemp->pNextFan0;
+ assert( Ivy_ObjFanin1(pTemp) == pObj );
+ return &pTemp->pNextFan1;
+}
+
+// getting hold of the place where the next fanout will be attached
+static inline Ivy_Obj_t ** Ivy_ObjNextPrevFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+ Ivy_Obj_t * pTemp;
+ assert( !Ivy_IsComplement(pObj) );
+ assert( !Ivy_IsComplement(pFanout) );
+ pTemp = Ivy_ObjNextFanout(pObj, pFanout);
+ if ( pTemp == NULL )
+ return NULL;
+ if ( Ivy_ObjFanin0(pTemp) == pObj )
+ return &pTemp->pPrevFan0;
+ assert( Ivy_ObjFanin1(pTemp) == pObj );
+ return &pTemp->pPrevFan1;
+}
+
+// iterator through the fanouts of the node
+#define Ivy_ObjForEachFanoutInt( pObj, pFanout ) \
+ for ( pFanout = (pObj)->pFanout; pFanout; \
+ pFanout = Ivy_ObjNextFanout(pObj, pFanout) )
+
+// safe iterator through the fanouts of the node
+#define Ivy_ObjForEachFanoutIntSafe( pObj, pFanout, pFanout2 ) \
+ for ( pFanout = (pObj)->pFanout, \
+ pFanout2 = Ivy_ObjNextFanout(pObj, pFanout); \
+ pFanout; \
+ pFanout = pFanout2, \
+ pFanout2 = Ivy_ObjNextFanout(pObj, pFanout) )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -47,8 +134,8 @@ void Ivy_ManStartFanout( Ivy_Man_t * p )
{
Ivy_Obj_t * pObj;
int i;
- assert( p->vFanouts == NULL );
- p->vFanouts = Vec_PtrStart( Ivy_ManObjIdMax(p) + 1000 );
+ assert( !p->fFanout );
+ p->fFanout = 1;
Ivy_ManForEachObj( p, pObj, i )
{
if ( Ivy_ObjFanin0(pObj) )
@@ -71,14 +158,12 @@ void Ivy_ManStartFanout( Ivy_Man_t * p )
***********************************************************************/
void Ivy_ManStopFanout( Ivy_Man_t * p )
{
- void * pTemp;
+ Ivy_Obj_t * pObj;
int i;
- assert( p->vFanouts != NULL );
- Vec_PtrForEachEntry( p->vFanouts, pTemp, i )
- if ( Ivy_FanoutIsArray(pTemp) )
- Vec_PtrFree( Ivy_FanoutGetArray(pTemp) );
- Vec_PtrFree( p->vFanouts );
- p->vFanouts = NULL;
+ assert( p->fFanout );
+ p->fFanout = 0;
+ Ivy_ManForEachObj( p, pObj, i )
+ pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
}
/**Function*************************************************************
@@ -92,31 +177,15 @@ void Ivy_ManStopFanout( Ivy_Man_t * p )
SeeAlso []
***********************************************************************/
-void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pFanin, Ivy_Obj_t * pFanout )
{
- Vec_Ptr_t * vNodes;
- void ** ppSpot;
- assert( p->vFanouts != NULL );
- assert( !Ivy_IsComplement(pObj) );
- // extend the fanout array if needed
- Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
- // get the pointer to the place where fanouts are stored
- ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id );
- // consider several cases
- if ( *ppSpot == NULL ) // no fanout - add one fanout
- *ppSpot = pFanout;
- else if ( Ivy_FanoutIsArray(*ppSpot) ) // array of fanouts - add one fanout
+ assert( p->fFanout );
+ if ( pFanin->pFanout )
{
- vNodes = Ivy_FanoutGetArray(*ppSpot);
- Vec_PtrPush( vNodes, pFanout );
- }
- else // only one fanout - create array and put both fanouts into the array
- {
- vNodes = Vec_PtrAlloc( 4 );
- Vec_PtrPush( vNodes, *ppSpot );
- Vec_PtrPush( vNodes, pFanout );
- *ppSpot = Ivy_FanoutSetArray( vNodes );
+ *Ivy_ObjNextFanoutPlace(pFanin, pFanout) = pFanin->pFanout;
+ *Ivy_ObjPrevFanoutPlace(pFanin, pFanin->pFanout) = pFanout;
}
+ pFanin->pFanout = pFanout;
}
/**Function*************************************************************
@@ -130,30 +199,25 @@ void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
SeeAlso []
***********************************************************************/
-void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pFanin, Ivy_Obj_t * pFanout )
{
- Vec_Ptr_t * vNodes;
- void ** ppSpot;
- assert( p->vFanouts != NULL );
- assert( !Ivy_IsComplement(pObj) );
- // extend the fanout array if needed
- Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
- ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id );
- if ( *ppSpot == NULL ) // no fanout - should not happen
- {
- assert( 0 );
- }
- else if ( Ivy_FanoutIsArray(*ppSpot) ) // the array of fanouts - delete the fanout
- {
- vNodes = Ivy_FanoutGetArray(*ppSpot);
- Vec_PtrRemove( vNodes, pFanout );
- }
- else // only one fanout - delete the fanout
- {
- assert( *ppSpot == pFanout );
- *ppSpot = NULL;
- }
-// printf( " %d", Ivy_ObjFanoutNum(p, pObj) );
+ Ivy_Obj_t ** ppPlace1, ** ppPlace2, ** ppPlaceN;
+ assert( pFanin->pFanout != NULL );
+
+ ppPlace1 = Ivy_ObjNextFanoutPlace(pFanin, pFanout);
+ ppPlaceN = Ivy_ObjPrevNextFanoutPlace(pFanin, pFanout);
+ assert( *ppPlaceN == pFanout );
+ if ( ppPlaceN )
+ *ppPlaceN = *ppPlace1;
+
+ ppPlace2 = Ivy_ObjPrevFanoutPlace(pFanin, pFanout);
+ ppPlaceN = Ivy_ObjNextPrevFanoutPlace(pFanin, pFanout);
+ assert( ppPlaceN == NULL || *ppPlaceN == pFanout );
+ if ( ppPlaceN )
+ *ppPlaceN = *ppPlace2;
+
+ *ppPlace1 = NULL;
+ *ppPlace2 = NULL;
}
/**Function*************************************************************
@@ -167,32 +231,18 @@ void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
SeeAlso []
***********************************************************************/
-void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew )
+void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pFanin, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew )
{
- Vec_Ptr_t * vNodes;
- void ** ppSpot;
- int Index;
- assert( p->vFanouts != NULL );
- assert( !Ivy_IsComplement(pObj) );
- // extend the fanout array if needed
- Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
- ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id );
- if ( *ppSpot == NULL ) // no fanout - should not happen
- {
- assert( 0 );
- }
- else if ( Ivy_FanoutIsArray(*ppSpot) ) // the array of fanouts - find and replace the fanout
- {
- vNodes = Ivy_FanoutGetArray(*ppSpot);
- Index = Vec_PtrFind( vNodes, pFanoutOld );
- assert( Index >= 0 );
- Vec_PtrWriteEntry( vNodes, Index, pFanoutNew );
- }
- else // only one fanout - delete the fanout
- {
- assert( *ppSpot == pFanoutOld );
- *ppSpot = pFanoutNew;
- }
+ Ivy_Obj_t ** ppPlace;
+ ppPlace = Ivy_ObjPrevNextFanoutPlace(pFanin, pFanoutOld);
+ assert( *ppPlace == pFanoutOld );
+ if ( ppPlace )
+ *ppPlace = pFanoutNew;
+ ppPlace = Ivy_ObjNextPrevFanoutPlace(pFanin, pFanoutOld);
+ assert( ppPlace == NULL || *ppPlace == pFanoutOld );
+ if ( ppPlace )
+ *ppPlace = pFanoutNew;
+ // assuming that pFanoutNew already points to the next fanout
}
/**Function*************************************************************
@@ -208,52 +258,12 @@ void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld
***********************************************************************/
void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray )
{
- Vec_Ptr_t * vNodes;
- Ivy_Obj_t * pTemp;
- int i;
- assert( p->vFanouts != NULL );
+ Ivy_Obj_t * pFanout;
+ assert( p->fFanout );
assert( !Ivy_IsComplement(pObj) );
- // extend the fanout array if needed
- Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
- vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id );
- // clean the resulting array
Vec_PtrClear( vArray );
- if ( vNodes == NULL ) // no fanout - nothing to do
- {
- }
- else if ( Ivy_FanoutIsArray(vNodes) ) // the array of fanouts - copy fanouts
- {
- vNodes = Ivy_FanoutGetArray(vNodes);
- Vec_PtrForEachEntry( vNodes, pTemp, i )
- Vec_PtrPush( vArray, pTemp );
- }
- else // only one fanout - add the fanout
- Vec_PtrPush( vArray, vNodes );
-}
-
-/**Function*************************************************************
-
- Synopsis [Reads one fanout.]
-
- Description [Returns fanout if there is only one fanout.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj )
-{
- Vec_Ptr_t * vNodes;
- assert( p->vFanouts != NULL );
- assert( !Ivy_IsComplement(pObj) );
- // extend the fanout array if needed
- Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
- vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id );
- // clean the resulting array
- if ( vNodes && !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return
- return (Ivy_Obj_t *)vNodes;
- return NULL;
+ Ivy_ObjForEachFanoutInt( pObj, pFanout )
+ Vec_PtrPush( vArray, pFanout );
}
/**Function*************************************************************
@@ -269,18 +279,7 @@ Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj )
***********************************************************************/
Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj )
{
- Vec_Ptr_t * vNodes;
- assert( p->vFanouts != NULL );
- assert( !Ivy_IsComplement(pObj) );
- // extend the fanout array if needed
- Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
- vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id );
- // clean the resulting array
- if ( vNodes == NULL )
- return NULL;
- if ( !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return
- return (Ivy_Obj_t *)vNodes;
- return Vec_PtrEntry( Ivy_FanoutGetArray(vNodes), 0 );
+ return pObj->pFanout;
}
/**Function*************************************************************
@@ -296,21 +295,13 @@ Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj )
***********************************************************************/
int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj )
{
- Vec_Ptr_t * vNodes;
- assert( p->vFanouts != NULL );
- assert( !Ivy_IsComplement(pObj) );
- // extend the fanout array if needed
- Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
- vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id );
- // clean the resulting array
- if ( vNodes == NULL )
- return 0;
- if ( !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return
- return 1;
- return Vec_PtrSize( Ivy_FanoutGetArray(vNodes) );
+ Ivy_Obj_t * pFanout;
+ int Counter = 0;
+ Ivy_ObjForEachFanoutInt( pObj, pFanout )
+ Counter++;
+ return Counter;
}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyIsop.c b/src/temp/ivy/ivyIsop.c
index 2d0101a7..1a4fce25 100644
--- a/src/temp/ivy/ivyIsop.c
+++ b/src/temp/ivy/ivyIsop.c
@@ -25,6 +25,10 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+// ISOP computation fails if intermediate memory usage exceed this limit
+#define IVY_ISOP_MEM_LIMIT 4096
+
+// intermediate ISOP representation
typedef struct Ivy_Sop_t_ Ivy_Sop_t;
struct Ivy_Sop_t_
{
@@ -32,122 +36,70 @@ struct Ivy_Sop_t_
int nCubes;
};
-static Mem_Flex_t * s_Man = NULL;
-
-static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes );
-static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes );
+// static procedures to compute ISOP
+static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore );
+static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-/**Function*************************************************************
-
- Synopsis [Deallocates memory used for computing ISOPs from TTs.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ivy_TruthManStop()
-{
- Mem_FlexStop( s_Man, 0 );
- s_Man = NULL;
-}
-
/**Function*************************************************************
Synopsis [Computes ISOP from TT.]
- Description []
+ Description [Returns the cover in vCover. Uses the rest of array in vCover
+ as an intermediate memory storage. Returns the cover with -1 cubes, if the
+ the computation exceeded the memory limit (IVY_ISOP_MEM_LIMIT words of
+ intermediate data).]
SideEffects []
SeeAlso []
***********************************************************************/
-int Ivy_TruthIsopOne( unsigned * puTruth, int nVars, Vec_Int_t * vCover )
+int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth )
{
Ivy_Sop_t cRes, * pcRes = &cRes;
+ Ivy_Sop_t cRes2, * pcRes2 = &cRes2;
unsigned * pResult;
- int i;
+ int RetValue = 0;
assert( nVars >= 0 && nVars < 16 );
// if nVars < 5, make sure it does not depend on those vars
- for ( i = nVars; i < 5; i++ )
- assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
+// for ( i = nVars; i < 5; i++ )
+// assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
// prepare memory manager
- if ( s_Man == NULL )
- s_Man = Mem_FlexStart();
- else
- Mem_FlexRestart( s_Man );
- // compute ISOP
- pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
-// Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" );
-// Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" );
- assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
-//printf( "%d ", Mem_FlexReadMemUsage(s_Man) );
-//printf( "%d ", pcRes->nCubes );
- // copy the truth table
Vec_IntClear( vCover );
- for ( i = 0; i < pcRes->nCubes; i++ )
- Vec_IntPush( vCover, pcRes->pCubes[i] );
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes ISOP from TT.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover )
-{
- Ivy_Sop_t cRes, * pcRes = &cRes;
- unsigned * pResult;
- int i;
- assert( nVars >= 0 && nVars < 16 );
- // if nVars < 5, make sure it does not depend on those vars
- for ( i = nVars; i < 5; i++ )
- assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
- // prepare memory manager
- if ( s_Man == NULL )
- s_Man = Mem_FlexStart();
- else
- Mem_FlexRestart( s_Man );
- // compute ISOP
- pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
-// Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" );
-// Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" );
- assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
-//printf( "%d ", Mem_FlexReadMemUsage(s_Man) );
-//printf( "%d ", pcRes->nCubes );
- // copy the truth table
- Vec_IntClear( vCover );
- for ( i = 0; i < pcRes->nCubes; i++ )
- Vec_IntPush( vCover, pcRes->pCubes[i] );
-
- // try other polarity
- Mem_FlexRestart( s_Man );
- Extra_TruthNot( puTruth, puTruth, nVars );
- pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
- assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
- Extra_TruthNot( puTruth, puTruth, nVars );
- if ( Vec_IntSize(vCover) < pcRes->nCubes )
+ Vec_IntGrow( vCover, IVY_ISOP_MEM_LIMIT );
+ // compute ISOP for the direct polarity
+ pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vCover );
+ if ( pcRes->nCubes == -1 )
+ {
+ vCover->nSize = -1;
return 0;
-
- // copy the truth table
- Vec_IntClear( vCover );
- for ( i = 0; i < pcRes->nCubes; i++ )
- Vec_IntPush( vCover, pcRes->pCubes[i] );
- return 1;
+ }
+ assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+ if ( fTryBoth )
+ {
+ // compute ISOP for the complemented polarity
+ Extra_TruthNot( puTruth, puTruth, nVars );
+ pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vCover );
+ if ( pcRes2->nCubes >= 0 )
+ {
+ assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+ if ( pcRes->nCubes > pcRes2->nCubes )
+ {
+ RetValue = 1;
+ pcRes = pcRes2;
+ }
+ }
+ Extra_TruthNot( puTruth, puTruth, nVars );
+ }
+// printf( "%d ", vCover->nSize );
+ // move the cover representation to the beginning of the memory buffer
+ memmove( vCover->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
+ Vec_IntShrink( vCover, pcRes->nCubes );
+ return RetValue;
}
/**Function*************************************************************
@@ -161,17 +113,22 @@ int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover )
SeeAlso []
***********************************************************************/
-unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes )
+unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore )
{
Ivy_Sop_t cRes0, cRes1, cRes2;
Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
unsigned * puRes0, * puRes1, * puRes2;
unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
int i, k, Var, nWords, nWordsAll;
- assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
+// assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
// allocate room for the resulting truth table
nWordsAll = Extra_TruthWordNum( nVars );
- pTemp = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWordsAll );
+ pTemp = Vec_IntFetch( vStore, nWordsAll );
+ if ( pTemp == NULL )
+ {
+ pcRes->nCubes = -1;
+ return NULL;
+ }
// check for constants
if ( Extra_TruthIsConst0( puOn, nVars ) )
{
@@ -183,7 +140,12 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
if ( Extra_TruthIsConst1( puOnDc, nVars ) )
{
pcRes->nCubes = 1;
- pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
+ pcRes->pCubes = Vec_IntFetch( vStore, 1 );
+ if ( pcRes->pCubes == NULL )
+ {
+ pcRes->nCubes = -1;
+ return NULL;
+ }
pcRes->pCubes[0] = 0;
Extra_TruthFill( pTemp, nVars );
return pTemp;
@@ -198,7 +160,7 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
// consider a simple case when one-word computation can be used
if ( Var < 5 )
{
- unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes );
+ unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore );
for ( i = 0; i < nWordsAll; i++ )
pTemp[i] = uRes;
return pTemp;
@@ -211,17 +173,37 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
pTemp0 = pTemp; pTemp1 = pTemp + nWords;
// solve for cofactors
Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
- puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0 );
+ puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
+ if ( pcRes0->nCubes == -1 )
+ {
+ pcRes->nCubes = -1;
+ return NULL;
+ }
Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
- puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1 );
+ puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
+ if ( pcRes1->nCubes == -1 )
+ {
+ pcRes->nCubes = -1;
+ return NULL;
+ }
Extra_TruthSharp( pTemp0, puOn0, puRes0, Var );
Extra_TruthSharp( pTemp1, puOn1, puRes1, Var );
Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var );
Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
- puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2 );
+ puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
+ if ( pcRes2->nCubes == -1 )
+ {
+ pcRes->nCubes = -1;
+ return NULL;
+ }
// create the resulting cover
pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
- pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
+ pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
+ if ( pcRes->pCubes == NULL )
+ {
+ pcRes->nCubes = -1;
+ return NULL;
+ }
k = 0;
for ( i = 0; i < pcRes0->nCubes; i++ )
pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
@@ -255,7 +237,7 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
SeeAlso []
***********************************************************************/
-unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes )
+unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore )
{
unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
Ivy_Sop_t cRes0, cRes1, cRes2;
@@ -273,7 +255,12 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
if ( uOnDc == 0xFFFFFFFF )
{
pcRes->nCubes = 1;
- pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
+ pcRes->pCubes = Vec_IntFetch( vStore, 1 );
+ if ( pcRes->pCubes == NULL )
+ {
+ pcRes->nCubes = -1;
+ return 0;
+ }
pcRes->pCubes[0] = 0;
return 0xFFFFFFFF;
}
@@ -292,12 +279,32 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
Extra_TruthCofactor0( &uOnDc0, Var + 1, Var );
Extra_TruthCofactor1( &uOnDc1, Var + 1, Var );
// solve for cofactors
- uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0 );
- uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1 );
- uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2 );
+ uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
+ if ( pcRes0->nCubes == -1 )
+ {
+ pcRes->nCubes = -1;
+ return 0;
+ }
+ uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore );
+ if ( pcRes1->nCubes == -1 )
+ {
+ pcRes->nCubes = -1;
+ return 0;
+ }
+ uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore );
+ if ( pcRes2->nCubes == -1 )
+ {
+ pcRes->nCubes = -1;
+ return 0;
+ }
// create the resulting cover
pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
- pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
+ pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
+ if ( pcRes->pCubes == NULL )
+ {
+ pcRes->nCubes = -1;
+ return 0;
+ }
k = 0;
for ( i = 0; i < pcRes0->nCubes; i++ )
pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index c5b66ad0..9839567f 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -82,7 +82,7 @@ Ivy_Man_t * Ivy_ManStart()
void Ivy_ManStop( Ivy_Man_t * p )
{
// Ivy_TableProfile( p );
- if ( p->vFanouts ) Ivy_ManStopFanout( p );
+// if ( p->vFanouts ) Ivy_ManStopFanout( p );
if ( p->vChunks ) Ivy_ManStopMemory( p );
if ( p->vRequired ) Vec_IntFree( p->vRequired );
if ( p->vPis ) Vec_PtrFree( p->vPis );
@@ -156,14 +156,14 @@ int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
void Ivy_ManPrintStats( Ivy_Man_t * p )
{
printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) );
- printf( "A = %d. ", Ivy_ManAndNum(p) );
- printf( "L = %d. ", Ivy_ManLatchNum(p) );
+ printf( "A = %7d. ", Ivy_ManAndNum(p) );
+ printf( "L = %5d. ", Ivy_ManLatchNum(p) );
// printf( "X = %d. ", Ivy_ManExorNum(p) );
- printf( "B = %d. ", Ivy_ManBufNum(p) );
- printf( "MaxID = %d. ", Ivy_ManObjIdMax(p) );
+// printf( "B = %3d. ", Ivy_ManBufNum(p) );
+ printf( "MaxID = %7d. ", Ivy_ManObjIdMax(p) );
// printf( "Cre = %d. ", p->nCreated );
// printf( "Del = %d. ", p->nDeleted );
- printf( "Lev = %d. ", Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) );
+ printf( "Lev = %3d. ", Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) );
printf( "\n" );
}
@@ -190,7 +190,7 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
assert( Ivy_ManPoNum(p) == Vec_PtrSize(p->vPos) );
assert( Vec_PtrSize( p->vBufs ) == 0 );
// create fanouts
- if ( p->vFanouts == NULL )
+ if ( p->fFanout == 0 )
Ivy_ManStartFanout( p );
// collect the POs to be converted into latches
for ( i = 0; i < nLatches; i++ )
diff --git a/src/temp/ivy/ivyMem.c b/src/temp/ivy/ivyMem.c
index 01833f03..6ca33541 100644
--- a/src/temp/ivy/ivyMem.c
+++ b/src/temp/ivy/ivyMem.c
@@ -87,15 +87,15 @@ void Ivy_ManAddMemory( Ivy_Man_t * p )
{
char * pMemory;
int i, nBytes;
- assert( sizeof(Ivy_Obj_t) <= 32 );
+ assert( sizeof(Ivy_Obj_t) <= 64 );
assert( p->pListFree == NULL );
assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
// allocate new memory page
- nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 32;
+ nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 64;
pMemory = ALLOC( char, nBytes );
Vec_PtrPush( p->vChunks, pMemory );
// align memory at the 32-byte boundary
- pMemory = pMemory + 32 - (((int)pMemory) & 31);
+ pMemory = pMemory + 64 - (((int)pMemory) & 63);
// remember the manager in the first entry
Vec_PtrPush( p->vPages, pMemory );
// break the memory down into nodes
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index 735d79c3..3122c8c8 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -79,6 +79,7 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
assert( Ivy_TableLookup(p, pGhost) == NULL );
// get memory for the new object
pObj = Ivy_ManFetchMemory( p );
+//printf( "Reusing %p.\n", pObj );
assert( Ivy_ObjIsNone(pObj) );
pObj->Id = Vec_PtrSize(p->vObjs);
Vec_PtrPush( p->vObjs, pObj );
@@ -139,13 +140,13 @@ void Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj
if ( Ivy_ObjFanin0(pObj) != NULL )
{
Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) );
- if ( p->vFanouts )
+ if ( p->fFanout )
Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj );
}
if ( Ivy_ObjFanin1(pObj) != NULL )
{
Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) );
- if ( p->vFanouts )
+ if ( p->fFanout )
Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj );
}
// add the node to the structural hash table
@@ -168,23 +169,29 @@ void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj )
assert( !Ivy_IsComplement(pObj) );
assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || Ivy_ObjFanin1(pObj) != NULL );
// remove connections
- if ( Ivy_ObjFanin0(pObj) != NULL )
+ if ( pObj->pFanin0 != NULL )
{
Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj));
- if ( p->vFanouts )
+ if ( p->fFanout )
Ivy_ObjDeleteFanout( p, Ivy_ObjFanin0(pObj), pObj );
}
- if ( Ivy_ObjFanin1(pObj) != NULL )
+ if ( pObj->pFanin1 != NULL )
{
Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj));
- if ( p->vFanouts )
+ if ( p->fFanout )
Ivy_ObjDeleteFanout( p, Ivy_ObjFanin1(pObj), pObj );
}
+ assert( pObj->pNextFan0 == NULL );
+ assert( pObj->pNextFan1 == NULL );
+ assert( pObj->pPrevFan0 == NULL );
+ assert( pObj->pPrevFan1 == NULL );
// remove the node from the structural hash table
Ivy_TableDelete( p, pObj );
// add the first fanin
pObj->pFanin0 = NULL;
pObj->pFanin1 = NULL;
+
+// Ivy_ManCheckFanouts( p );
}
/**Function*************************************************************
@@ -205,14 +212,14 @@ void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew
pFaninOld = Ivy_ObjFanin0(pObj);
// decrement ref and remove fanout
Ivy_ObjRefsDec( pFaninOld );
- if ( p->vFanouts )
+ if ( p->fFanout )
Ivy_ObjDeleteFanout( p, pFaninOld, pObj );
+ // update the fanin
+ pObj->pFanin0 = pFaninNew;
// increment ref and add fanout
Ivy_ObjRefsInc( Ivy_Regular(pFaninNew) );
- if ( p->vFanouts )
+ if ( p->fFanout )
Ivy_ObjAddFanout( p, Ivy_Regular(pFaninNew), pObj );
- // update the fanin
- pObj->pFanin0 = pFaninNew;
// get rid of old fanin
if ( !Ivy_ObjIsPi(pFaninOld) && Ivy_ObjRefs(pFaninOld) == 0 )
Ivy_ObjDelete_rec( p, pFaninOld, 1 );
@@ -243,7 +250,7 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
Vec_PtrRemove( p->vPis, pObj );
else if ( Ivy_ObjIsPo(pObj) )
Vec_PtrRemove( p->vPos, pObj );
- else if ( p->vFanouts && Ivy_ObjIsBuf(pObj) )
+ else if ( p->fFanout && Ivy_ObjIsBuf(pObj) )
Vec_PtrRemove( p->vBufs, pObj );
// clean and recycle the entry
if ( fFreeTop )
@@ -251,11 +258,14 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
// free the node
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
Ivy_ManRecycleMemory( p, pObj );
+//printf( "Recycling after delete %p.\n", pObj );
}
else
{
int nRefsOld = pObj->nRefs;
+ Ivy_Obj_t * pFanout = pObj->pFanout;
Ivy_ObjClean( pObj );
+ pObj->pFanout = pFanout;
pObj->nRefs = nRefsOld;
}
}
@@ -318,7 +328,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
if ( fUpdateLevel )
{
// if the new node's arrival time is different, recursively update arrival time of the fanouts
- if ( p->vFanouts && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
+ if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
{
assert( Ivy_ObjIsNode(pObjOld) );
pObjOld->Level = pObjNew->Level;
@@ -338,16 +348,23 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
// delete the old object
if ( fDeleteOld )
Ivy_ObjDelete_rec( p, pObjOld, fFreeTop );
- // make sure object is pointing to itself
+ // make sure object is not pointing to itself
assert( Ivy_ObjFanin0(pObjNew) == NULL || pObjOld != Ivy_ObjFanin0(pObjNew) );
assert( Ivy_ObjFanin1(pObjNew) == NULL || pObjOld != Ivy_ObjFanin1(pObjNew) );
+ // make sure the old node has no fanin fanout pointers
+ if ( p->fFanout )
+ {
+ assert( pObjOld->pFanout != NULL );
+ assert( pObjNew->pFanout == NULL );
+ pObjNew->pFanout = pObjOld->pFanout;
+ }
// transfer the old object
assert( Ivy_ObjRefs(pObjNew) == 0 );
nRefsOld = pObjOld->nRefs;
Ivy_ObjOverwrite( pObjOld, pObjNew );
pObjOld->nRefs = nRefsOld;
// patch the fanout of the fanins
- if ( p->vFanouts )
+ if ( p->fFanout )
{
Ivy_ObjPatchFanout( p, Ivy_ObjFanin0(pObjOld), pObjNew, pObjOld );
if ( Ivy_ObjFanin1(pObjOld) )
@@ -358,9 +375,12 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
// recycle the object that was taken over by pObjOld
Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL );
Ivy_ManRecycleMemory( p, pObjNew );
+//printf( "Recycling after patch %p.\n", pObjNew );
// if the new node is the buffer propagate it
- if ( p->vFanouts && Ivy_ObjIsBuf(pObjOld) )
+ if ( p->fFanout && Ivy_ObjIsBuf(pObjOld) )
Vec_PtrPush( p->vBufs, pObjOld );
+// Ivy_ManCheckFanouts( p );
+// printf( "\n" );
}
/**Function*************************************************************
@@ -385,6 +405,7 @@ void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel
return;
pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) );
Ivy_ObjPatchFanin0( p, pNode, pFanReal0 );
+// Ivy_ManCheckFanouts( p );
return;
}
if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) )
diff --git a/src/temp/ivy/ivyResyn.c b/src/temp/ivy/ivyResyn.c
index 804bdfb4..b2e4a4dd 100644
--- a/src/temp/ivy/ivyResyn.c
+++ b/src/temp/ivy/ivyResyn.c
@@ -28,6 +28,47 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+/**Function*************************************************************
+
+ Synopsis [Performs several passes of rewriting on the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
+{
+ int clk;
+ Ivy_Man_t * pTemp;
+
+if ( fVerbose ) { printf( "Original:\n" ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+ pMan = Ivy_ManBalance( pMan, fUpdateLevel );
+if ( fVerbose ) { printf( "\n" ); }
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
+clk = clock();
+ Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
+if ( fVerbose ) { printf( "\n" ); }
+if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+ pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
+ Ivy_ManStop( pTemp );
+if ( fVerbose ) { printf( "\n" ); }
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+ return pMan;
+}
+
/**Function*************************************************************
Synopsis [Performs several passes of rewriting on the AIG.]
diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c
index 537b64ff..64331579 100644
--- a/src/temp/ivy/ivyRwrPre.c
+++ b/src/temp/ivy/ivyRwrPre.c
@@ -61,7 +61,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
if ( pManRwt == NULL )
return 0;
// create fanouts
- if ( fUpdateLevel && p->vFanouts == NULL )
+ if ( fUpdateLevel && p->fFanout == 0 )
Ivy_ManStartFanout( p );
// compute the reverse levels if level update is requested
if ( fUpdateLevel )
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
index 8fd1b63b..7cf55b69 100644
--- a/src/temp/ivy/ivySeq.c
+++ b/src/temp/ivy/ivySeq.c
@@ -64,7 +64,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
if ( pManRwt == NULL )
return 0;
// create fanouts
- if ( p->vFanouts == NULL )
+ if ( p->fFanout == 0 )
Ivy_ManStartFanout( p );
// resynthesize each node once
nNodes = Ivy_ManObjIdMax(p);
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index 77a55a39..a23e76c9 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -381,7 +381,7 @@ void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj )
Ivy_Obj_t * pFanout;
Vec_Ptr_t * vFanouts;
int i, LevelNew;
- assert( p->vFanouts );
+ assert( p->fFanout );
assert( Ivy_ObjIsNode(pObj) );
vFanouts = Vec_PtrAlloc( 10 );
Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
@@ -416,7 +416,7 @@ int Ivy_ObjLevelRNew( Ivy_Man_t * p, Ivy_Obj_t * pObj )
Ivy_Obj_t * pFanout;
Vec_Ptr_t * vFanouts;
int i, Required, LevelNew = 1000000;
- assert( p->vFanouts && p->vRequired );
+ assert( p->fFanout && p->vRequired );
vFanouts = Vec_PtrAlloc( 10 );
Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
{
diff --git a/src/temp/player/player.h b/src/temp/player/player.h
index b0bb0ec4..0213683f 100644
--- a/src/temp/player/player.h
+++ b/src/temp/player/player.h
@@ -86,13 +86,14 @@ static inline Pla_Obj_t * Ivy_ObjPlaStr( Ivy_Man_t * p, Ivy_Obj_t * pObj ) {
////////////////////////////////////////////////////////////////////////
/*=== playerToAbc.c ==============================================================*/
-extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose );
+extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose );
/*=== playerCore.c =============================================================*/
extern Pla_Man_t * Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose );
/*=== playerFast.c =============================================================*/
extern void Pla_ManFastLutMap( Ivy_Man_t * pAig, int nLimit );
extern void Pla_ManFastLutMapStop( Ivy_Man_t * pAig );
extern void Pla_ManFastLutMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves );
+extern void Pla_ManFastLutMapReverseLevel( Ivy_Man_t * pAig );
/*=== playerMan.c ==============================================================*/
extern Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * p, int nLutMax, int nPlaMax );
extern void Pla_ManFree( Pla_Man_t * p );
diff --git a/src/temp/player/playerMan.c b/src/temp/player/playerMan.c
index 1196d242..78b20718 100644
--- a/src/temp/player/playerMan.c
+++ b/src/temp/player/playerMan.c
@@ -40,7 +40,7 @@
***********************************************************************/
Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * pAig, int nLutMax, int nPlaMax )
-{
+{
Pla_Man_t * pMan;
assert( !(nLutMax < 2 || nLutMax > 8 || nPlaMax < 8 || nPlaMax > 128) );
// start the manager
diff --git a/src/temp/player/playerToAbc.c b/src/temp/player/playerToAbc.c
index fc5e01ea..91994ca6 100644
--- a/src/temp/player/playerToAbc.c
+++ b/src/temp/player/playerToAbc.c
@@ -50,9 +50,8 @@ static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId )
SeeAlso []
***********************************************************************/
-void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose )
+void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose )
{
- int fUseRewriting = 0;
Pla_Man_t * p;
Ivy_Man_t * pMan, * pManExt;
Abc_Ntk_t * pNtkNew;
@@ -69,7 +68,15 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int f
}
if ( fVerbose )
Ivy_ManPrintStats( pMan );
- if ( fUseRewriting )
+ if ( fRewriting )
+ {
+ // simplify
+ pMan = Ivy_ManResyn0( pManExt = pMan, 1, 0 );
+ Ivy_ManStop( pManExt );
+ if ( fVerbose )
+ Ivy_ManPrintStats( pMan );
+ }
+ if ( fSynthesis )
{
// simplify
pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 );
@@ -261,9 +268,16 @@ Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t *
pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
pObjAbc = Abc_NodeCreateConst0( pNtkNew );
}
+ else if ( Extra_TruthIsConst1(puTruth, 8) )
+ {
+ pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
+ pObjAbc = Abc_NodeCreateConst1( pNtkNew );
+ }
else
{
- int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes );
+ int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes, 1 );
+ if ( vNodes->nSize == -1 )
+ printf( "Ivy_ManToAbc_rec(): Internal error.\n" );
pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes );
if ( fCompl ) Abc_SopComplement(pObjAbc->pData);
// printf( "Cover contains %d cubes.\n", Vec_IntSize(vNodes) );
@@ -372,9 +386,16 @@ Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj
pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
pObjAbc = Abc_NodeCreateConst0( pNtkNew );
}
+ else if ( Extra_TruthIsConst1(puTruth, 8) )
+ {
+ pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
+ pObjAbc = Abc_NodeCreateConst1( pNtkNew );
+ }
else
{
- int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes );
+ int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes, 1 );
+ if ( vNodes->nSize == -1 )
+ printf( "Ivy_ManToAbcFast_rec(): Internal error.\n" );
pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes );
if ( fCompl ) Abc_SopComplement(pObjAbc->pData);
}
@@ -444,32 +465,48 @@ static inline int Abc_NtkPlayerCostOne( int nCost, int RankCost )
int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose )
{
Abc_Obj_t * pObj;
- int nFanins, nLevels, * pLevelCosts, CostTotal, nRanksTotal, i;
+ int * pLevelCosts, * pLevelCostsR;
+ int nFanins, nLevels, LevelR, Cost, CostTotal, CostTotalR, nRanksTotal, nRanksTotalR, i;
+ // compute the reverse levels
+ Abc_NtkStartReverseLevels( pNtk );
// compute the costs for each level
nLevels = Abc_NtkGetLevelNum( pNtk );
- pLevelCosts = ALLOC( int, nLevels + 1 );
- memset( pLevelCosts, 0, sizeof(int) * (nLevels + 1) );
+ pLevelCosts = ALLOC( int, nLevels + 1 );
+ pLevelCostsR = ALLOC( int, nLevels + 1 );
+ memset( pLevelCosts, 0, sizeof(int) * (nLevels + 1) );
+ memset( pLevelCostsR, 0, sizeof(int) * (nLevels + 1) );
Abc_NtkForEachNode( pNtk, pObj, i )
{
nFanins = Abc_ObjFaninNum(pObj);
if ( nFanins == 0 )
continue;
- pLevelCosts[ pObj->Level ] += Abc_NodePlayerCost( nFanins );
+ Cost = Abc_NodePlayerCost( nFanins );
+ LevelR = Vec_IntEntry( pNtk->vLevelsR, pObj->Id );
+ pLevelCosts[ pObj->Level ] += Cost;
+ pLevelCostsR[ LevelR ] += Cost;
}
// compute the total cost
- CostTotal = nRanksTotal = 0;
- for ( i = 1; i <= nLevels; i++ )
+ CostTotal = CostTotalR = nRanksTotal = nRanksTotalR = 0;
+ for ( i = 0; i <= nLevels; i++ )
{
- CostTotal += pLevelCosts[i];
- nRanksTotal += Abc_NtkPlayerCostOne( pLevelCosts[i], RankCost );
+ CostTotal += pLevelCosts[i];
+ CostTotalR += pLevelCostsR[i];
+ nRanksTotal += Abc_NtkPlayerCostOne( pLevelCosts[i], RankCost );
+ nRanksTotalR += Abc_NtkPlayerCostOne( pLevelCostsR[i], RankCost );
}
+ assert( CostTotal == CostTotalR );
// print out statistics
if ( fVerbose )
{
for ( i = 1; i <= nLevels; i++ )
- printf( "Level %2d : Cost = %6d. Ranks = %6.3f.\n", i, pLevelCosts[i], ((double)pLevelCosts[i])/RankCost );
- printf( "TOTAL : Cost = %6d. Ranks = %3d.\n", CostTotal, nRanksTotal );
+ printf( "Level %2d : Cost = %7d. Ranks = %6.3f. Cost = %7d. Ranks = %6.3f.\n", i,
+ pLevelCosts[i], ((double)pLevelCosts[i])/RankCost,
+ pLevelCostsR[nLevels+1-i], ((double)pLevelCostsR[nLevels+1-i])/RankCost );
+ printf( "TOTAL : Cost = %7d. Ranks = %6d. RanksR = %5d. RanksBest = %5d.\n",
+ CostTotal, nRanksTotal, nRanksTotalR, nLevels );
}
+ free( pLevelCosts );
+ free( pLevelCostsR );
return nRanksTotal;
}
diff --git a/src/temp/vec/vecInt.h b/src/temp/vec/vecInt.h
index 9db30af7..4a97fc91 100644
--- a/src/temp/vec/vecInt.h
+++ b/src/temp/vec/vecInt.h
@@ -278,23 +278,6 @@ static inline int Vec_IntEntry( Vec_Int_t * p, int i )
return p->pArray[i];
}
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int * Vec_IntEntryP( Vec_Int_t * p, int i )
-{
- assert( i >= 0 && i < p->nSize );
- return p->pArray + i;
-}
-
/**Function*************************************************************
Synopsis []
@@ -402,10 +385,7 @@ static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry )
int i;
if ( p->nSize >= nSize )
return;
- if ( p->nSize < 2 * nSize )
- Vec_IntGrow( p, 2 * nSize );
- else
- Vec_IntGrow( p, p->nSize );
+ Vec_IntGrow( p, nSize );
for ( i = p->nSize; i < nSize; i++ )
p->pArray[i] = Entry;
p->nSize = nSize;
@@ -601,6 +581,28 @@ static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry )
return 0;
}
+/**Function*************************************************************
+
+ Synopsis [Returns the pointer to the next nWords entries in the vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned * Vec_IntFetch( Vec_Int_t * p, int nWords )
+{
+ p->nSize += nWords;
+ if ( p->nSize > p->nCap )
+ {
+// Vec_IntGrow( p, 2 * p->nSize );
+ return NULL;
+ }
+ return ((unsigned *)p->pArray) + p->nSize - nWords;
+}
+
/**Function*************************************************************
Synopsis [Returns the last entry and removes it from the list.]
diff --git a/src/temp/vec/vecPtr.h b/src/temp/vec/vecPtr.h
index 96975ff0..07ac0f17 100644
--- a/src/temp/vec/vecPtr.h
+++ b/src/temp/vec/vecPtr.h
@@ -282,6 +282,23 @@ static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
return p->pArray[i];
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void ** Vec_PtrEntryP( Vec_Ptr_t * p, int i )
+{
+ assert( i >= 0 && i < p->nSize );
+ return p->pArray + i;
+}
+
/**Function*************************************************************
Synopsis []
@@ -371,7 +388,10 @@ static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
int i;
if ( p->nSize >= nSize )
return;
- Vec_PtrGrow( p, nSize );
+ if ( p->nSize < 2 * nSize )
+ Vec_PtrGrow( p, 2 * nSize );
+ else
+ Vec_PtrGrow( p, p->nSize );
for ( i = p->nSize; i < nSize; i++ )
p->pArray[i] = Entry;
p->nSize = nSize;
@@ -505,10 +525,18 @@ static inline int Vec_PtrFind( Vec_Ptr_t * p, void * Entry )
static inline void Vec_PtrRemove( Vec_Ptr_t * p, void * Entry )
{
int i;
+ // delete assuming that it is closer to the end
+ for ( i = p->nSize - 1; i >= 0; i-- )
+ if ( p->pArray[i] == Entry )
+ break;
+ assert( i >= 0 );
+/*
+ // delete assuming that it is closer to the beginning
for ( i = 0; i < p->nSize; i++ )
if ( p->pArray[i] == Entry )
break;
assert( i < p->nSize );
+*/
for ( i++; i < p->nSize; i++ )
p->pArray[i-1] = p->pArray[i];
p->nSize--;
--
cgit v1.2.3