summaryrefslogtreecommitdiffstats
path: root/src/aig/dar
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/dar')
-rw-r--r--src/aig/dar/dar.h4
-rw-r--r--src/aig/dar/darBalance.c3
-rw-r--r--src/aig/dar/darCore.c12
-rw-r--r--src/aig/dar/darInt.h4
-rw-r--r--src/aig/dar/darLib.c8
-rw-r--r--src/aig/dar/darPrec.c388
-rw-r--r--src/aig/dar/darRefact.c2
-rw-r--r--src/aig/dar/darScript.c227
-rw-r--r--src/aig/dar/module.make1
9 files changed, 605 insertions, 44 deletions
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 923ffc12..1f25e767 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -86,8 +86,10 @@ extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
/*=== darScript.c ========================================================*/
extern Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig );
-extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
+extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
#ifdef __cplusplus
}
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 9c0997b8..d4266103 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -53,7 +53,8 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
Vec_Vec_t * vStore;
int i;
// create the new manager
- pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
// map the PI nodes
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index dec9bff7..5e1c0fad 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -65,7 +65,7 @@ void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars )
int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
{
Dar_Man_t * p;
- ProgressBar * pProgress;
+ Bar_Progress_t * pProgress;
Dar_Cut_t * pCut;
Aig_Obj_t * pObj, * pObjNew;
int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
@@ -88,15 +88,15 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
p->nNodesInit = Aig_ManNodeNum(pAig);
nNodesOld = Vec_PtrSize( pAig->vObjs );
- pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
+ pProgress = Bar_ProgressStart( stdout, nNodesOld );
Aig_ManForEachObj( pAig, pObj, i )
-// pProgress = Extra_ProgressBarStart( stdout, 100 );
+// pProgress = Bar_ProgressStart( stdout, 100 );
// Aig_ManOrderStart( pAig );
// Aig_ManForEachNodeInOrder( pAig, pObj )
{
-// Extra_ProgressBarUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
+// Bar_ProgressUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
- Extra_ProgressBarUpdate( pProgress, i, NULL );
+ Bar_ProgressUpdate( pProgress, i, NULL );
if ( !Aig_ObjIsNode(pObj) )
continue;
if ( i > nNodesOld )
@@ -167,7 +167,7 @@ p->timeCuts += clock() - clk;
p->timeTotal = clock() - clkStart;
p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
- Extra_ProgressBarStop( pProgress );
+ Bar_ProgressStop( pProgress );
p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
Dar_ManCutsFree( p );
// put the nodes into the DFS order and reassign their IDs
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index b14d5c30..97331416 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -38,6 +38,7 @@ extern "C" {
#include "vec.h"
#include "aig.h"
#include "dar.h"
+#include "bar.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -148,6 +149,9 @@ extern Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p );
extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
extern void Dar_ManStop( Dar_Man_t * p );
extern void Dar_ManPrintStats( Dar_Man_t * p );
+/*=== darPrec.c ============================================================*/
+extern char ** Dar_Permutations( int n );
+extern void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap );
#ifdef __cplusplus
}
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index e159f35a..14a47cee 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -129,8 +129,8 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs )
p->pObjs = ALLOC( Dar_LibObj_t, nObjs );
memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs );
// allocate canonical data
- p->pPerms4 = Extra_Permutations( 4 );
- Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
+ p->pPerms4 = Dar_Permutations( 4 );
+ Dar_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
// start the elementary objects
p->iObj = 4;
for ( i = 0; i < 4; i++ )
@@ -570,8 +570,8 @@ void Dar_LibStart()
int clk = clock();
assert( s_DarLib == NULL );
s_DarLib = Dar_LibRead();
- printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
- PRT( "Time", clock() - clk );
+// printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
+// PRT( "Time", clock() - clk );
}
/**Function*************************************************************
diff --git a/src/aig/dar/darPrec.c b/src/aig/dar/darPrec.c
new file mode 100644
index 00000000..c3e62389
--- /dev/null
+++ b/src/aig/dar/darPrec.c
@@ -0,0 +1,388 @@
+/**CFile****************************************************************
+
+ FileName [darPrec.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting.]
+
+ Synopsis [Truth table precomputation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: darPrec.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+ Synopsis [Allocated one-memory-chunk array.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void ** Dar_ArrayAlloc( int nCols, int nRows, int Size )
+{
+ char ** pRes;
+ char * pBuffer;
+ int i;
+ assert( nCols > 0 && nRows > 0 && Size > 0 );
+ pBuffer = ALLOC( char, nCols * (sizeof(void *) + nRows * Size) );
+ pRes = (char **)pBuffer;
+ pRes[0] = pBuffer + nCols * sizeof(void *);
+ for ( i = 1; i < nCols; i++ )
+ pRes[i] = pRes[0] + i * nRows * Size;
+ return pRes;
+}
+
+/**Function********************************************************************
+
+ Synopsis [Computes the factorial.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Dar_Factorial( int n )
+{
+ int i, Res = 1;
+ for ( i = 1; i <= n; i++ )
+ Res *= i;
+ return Res;
+}
+
+/**Function********************************************************************
+
+ Synopsis [Fills in the array of permutations.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+void Dar_Permutations_rec( char ** pRes, int nFact, int n, char Array[] )
+{
+ char ** pNext;
+ int nFactNext;
+ int iTemp, iCur, iLast, k;
+
+ if ( n == 1 )
+ {
+ pRes[0][0] = Array[0];
+ return;
+ }
+
+ // get the next factorial
+ nFactNext = nFact / n;
+ // get the last entry
+ iLast = n - 1;
+
+ for ( iCur = 0; iCur < n; iCur++ )
+ {
+ // swap Cur and Last
+ iTemp = Array[iCur];
+ Array[iCur] = Array[iLast];
+ Array[iLast] = iTemp;
+
+ // get the pointer to the current section
+ pNext = pRes + (n - 1 - iCur) * nFactNext;
+
+ // set the last entry
+ for ( k = 0; k < nFactNext; k++ )
+ pNext[k][iLast] = Array[iLast];
+
+ // call recursively for this part
+ Dar_Permutations_rec( pNext, nFactNext, n - 1, Array );
+
+ // swap them back
+ iTemp = Array[iCur];
+ Array[iCur] = Array[iLast];
+ Array[iLast] = iTemp;
+ }
+}
+
+/**Function********************************************************************
+
+ Synopsis [Computes the set of all permutations.]
+
+ Description [The number of permutations in the array is n!. The number of
+ entries in each permutation is n. Therefore, the resulting array is a
+ two-dimentional array of the size: n! x n. To free the resulting array,
+ call free() on the pointer returned by this procedure.]
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+char ** Dar_Permutations( int n )
+{
+ char Array[50];
+ char ** pRes;
+ int nFact, i;
+ // allocate memory
+ nFact = Dar_Factorial( n );
+ pRes = (char **)Dar_ArrayAlloc( nFact, n, sizeof(char) );
+ // fill in the permutations
+ for ( i = 0; i < n; i++ )
+ Array[i] = i;
+ Dar_Permutations_rec( pRes, nFact, n, Array );
+ // print the permutations
+/*
+ {
+ int i, k;
+ for ( i = 0; i < nFact; i++ )
+ {
+ printf( "{" );
+ for ( k = 0; k < n; k++ )
+ printf( " %d", pRes[i][k] );
+ printf( " }\n" );
+ }
+ }
+*/
+ return pRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Permutes the given vector of minterms.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_TruthPermute_int( int * pMints, int nMints, char * pPerm, int nVars, int * pMintsP )
+{
+ int m, v;
+ // clean the storage for minterms
+ memset( pMintsP, 0, sizeof(int) * nMints );
+ // go through minterms and add the variables
+ for ( m = 0; m < nMints; m++ )
+ for ( v = 0; v < nVars; v++ )
+ if ( pMints[m] & (1 << v) )
+ pMintsP[m] |= (1 << pPerm[v]);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Permutes the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Dar_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReverse )
+{
+ unsigned Result;
+ int * pMints;
+ int * pMintsP;
+ int nMints;
+ int i, m;
+
+ assert( nVars < 6 );
+ nMints = (1 << nVars);
+ pMints = ALLOC( int, nMints );
+ pMintsP = ALLOC( int, nMints );
+ for ( i = 0; i < nMints; i++ )
+ pMints[i] = i;
+
+ Dar_TruthPermute_int( pMints, nMints, pPerms, nVars, pMintsP );
+
+ Result = 0;
+ if ( fReverse )
+ {
+ for ( m = 0; m < nMints; m++ )
+ if ( Truth & (1 << pMintsP[m]) )
+ Result |= (1 << m);
+ }
+ else
+ {
+ for ( m = 0; m < nMints; m++ )
+ if ( Truth & (1 << m) )
+ Result |= (1 << pMintsP[m]);
+ }
+
+ free( pMints );
+ free( pMintsP );
+
+ return Result;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Changes the phase of the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Dar_TruthPolarize( unsigned uTruth, int Polarity, int nVars )
+{
+ // elementary truth tables
+ static unsigned Signs[5] = {
+ 0xAAAAAAAA, // 1010 1010 1010 1010 1010 1010 1010 1010
+ 0xCCCCCCCC, // 1010 1010 1010 1010 1010 1010 1010 1010
+ 0xF0F0F0F0, // 1111 0000 1111 0000 1111 0000 1111 0000
+ 0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000
+ 0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000
+ };
+ unsigned uTruthRes, uCof0, uCof1;
+ int nMints, Shift, v;
+ assert( nVars < 6 );
+ nMints = (1 << nVars);
+ uTruthRes = uTruth;
+ for ( v = 0; v < nVars; v++ )
+ if ( Polarity & (1 << v) )
+ {
+ uCof0 = uTruth & ~Signs[v];
+ uCof1 = uTruth & Signs[v];
+ Shift = (1 << v);
+ uCof0 <<= Shift;
+ uCof1 >>= Shift;
+ uTruth = uCof0 | uCof1;
+ }
+ return uTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes NPN canonical forms for 4-variable functions.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap )
+{
+ unsigned short * uCanons;
+ unsigned char * uMap;
+ unsigned uTruth, uPhase, uPerm;
+ char ** pPerms4, * uPhases, * uPerms;
+ int nFuncs, nClasses;
+ int i, k;
+
+ nFuncs = (1 << 16);
+ uCanons = ALLOC( unsigned short, nFuncs );
+ uPhases = ALLOC( char, nFuncs );
+ uPerms = ALLOC( char, nFuncs );
+ uMap = ALLOC( unsigned char, nFuncs );
+ memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
+ memset( uPhases, 0, sizeof(char) * nFuncs );
+ memset( uPerms, 0, sizeof(char) * nFuncs );
+ memset( uMap, 0, sizeof(unsigned char) * nFuncs );
+ pPerms4 = Dar_Permutations( 4 );
+
+ nClasses = 1;
+ nFuncs = (1 << 15);
+ for ( uTruth = 1; uTruth < (unsigned)nFuncs; uTruth++ )
+ {
+ // skip already assigned
+ if ( uCanons[uTruth] )
+ {
+ assert( uTruth > uCanons[uTruth] );
+ uMap[~uTruth & 0xFFFF] = uMap[uTruth] = uMap[uCanons[uTruth]];
+ continue;
+ }
+ uMap[uTruth] = nClasses++;
+ for ( i = 0; i < 16; i++ )
+ {
+ uPhase = Dar_TruthPolarize( uTruth, i, 4 );
+ for ( k = 0; k < 24; k++ )
+ {
+ uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 );
+ if ( uCanons[uPerm] == 0 )
+ {
+ uCanons[uPerm] = uTruth;
+ uPhases[uPerm] = i;
+ uPerms[uPerm] = k;
+
+ uPerm = ~uPerm & 0xFFFF;
+ uCanons[uPerm] = uTruth;
+ uPhases[uPerm] = i | 16;
+ uPerms[uPerm] = k;
+ }
+ else
+ assert( uCanons[uPerm] == uTruth );
+ }
+ uPhase = Dar_TruthPolarize( ~uTruth & 0xFFFF, i, 4 );
+ for ( k = 0; k < 24; k++ )
+ {
+ uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 );
+ if ( uCanons[uPerm] == 0 )
+ {
+ uCanons[uPerm] = uTruth;
+ uPhases[uPerm] = i;
+ uPerms[uPerm] = k;
+
+ uPerm = ~uPerm & 0xFFFF;
+ uCanons[uPerm] = uTruth;
+ uPhases[uPerm] = i | 16;
+ uPerms[uPerm] = k;
+ }
+ else
+ assert( uCanons[uPerm] == uTruth );
+ }
+ }
+ }
+ uPhases[(1<<16)-1] = 16;
+ assert( nClasses == 222 );
+ free( pPerms4 );
+ if ( puCanons )
+ *puCanons = uCanons;
+ else
+ free( uCanons );
+ if ( puPhases )
+ *puPhases = uPhases;
+ else
+ free( uPhases );
+ if ( puPerms )
+ *puPerms = uPerms;
+ else
+ free( uPerms );
+ if ( puMap )
+ *puMap = uMap;
+ else
+ free( uMap );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index b304fe34..a5435862 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -309,7 +309,7 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_
if ( Kit_GraphIsVar(pGraph) )
return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
// build the AIG nodes corresponding to the AND gates of the graph
-//printf( "Building (current number %d):\n", Aig_ManObjIdMax(pAig) );
+//printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) );
Kit_GraphForEachNode( pGraph, pNode, i )
{
pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 2fe39860..9eb5e280 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "darInt.h"
+#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -63,8 +64,8 @@ Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
-//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
+//alias rwsat "st; rw -l; b -l; rw -l; rf -l"
{
Aig_Man_t * pTemp;
@@ -74,18 +75,14 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
Dar_ManDefaultRwrParams( pParsRwr );
Dar_ManDefaultRefParams( pParsRef );
- pParsRwr->fUpdateLevel = fUpdateLevel;
- pParsRef->fUpdateLevel = fUpdateLevel;
+ pParsRwr->fUpdateLevel = 0;
+ pParsRef->fUpdateLevel = 0;
pParsRwr->fVerbose = fVerbose;
pParsRef->fVerbose = fVerbose;
- // balance
- if ( fBalance )
- {
-// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
-// Aig_ManStop( pTemp );
- }
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
@@ -98,9 +95,9 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
Aig_ManStop( pTemp );
// balance
-// if ( fBalance )
+ if ( fBalance )
{
- pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ pAig = Dar_ManBalance( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
}
@@ -109,28 +106,54 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
- pParsRwr->fUseZeros = 1;
- pParsRef->fUseZeros = 1;
-
- // rewrite
- Dar_ManRewrite( pAig, pParsRwr );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
- Aig_ManStop( pTemp );
+ return pAig;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
+//alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
+{
+ Aig_Man_t * pTemp;
+
+ Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+ Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+
+ Dar_ManDefaultRwrParams( pParsRwr );
+ Dar_ManDefaultRefParams( pParsRef );
+
+ pParsRwr->fUpdateLevel = fUpdateLevel;
+ pParsRef->fUpdateLevel = fUpdateLevel;
+
+ pParsRwr->fVerbose = fVerbose;
+ pParsRef->fVerbose = fVerbose;
+
+ pAig = Aig_ManDup( pAig, 0 );
// balance
if ( fBalance )
{
- pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
- Aig_ManStop( pTemp );
+// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+// Aig_ManStop( pTemp );
}
- // refactor
- Dar_ManRefactor( pAig, pParsRef );
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
- // rewrite
- Dar_ManRewrite( pAig, pParsRwr );
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
@@ -140,6 +163,15 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
}
+
+ pParsRwr->fUseZeros = 1;
+ pParsRef->fUseZeros = 1;
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
return pAig;
}
@@ -149,13 +181,13 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
Description []
- SideEffects [This procedure does not tighten level during restructuring.]
+ SideEffects []
SeeAlso []
***********************************************************************/
-Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
-//alias rwsat "st; rw -l; b -l; rw -l; rf -l"
+Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
+//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
{
Aig_Man_t * pTemp;
@@ -165,11 +197,20 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
Dar_ManDefaultRwrParams( pParsRwr );
Dar_ManDefaultRefParams( pParsRef );
- pParsRwr->fUpdateLevel = 0;
- pParsRef->fUpdateLevel = 0;
+ pParsRwr->fUpdateLevel = fUpdateLevel;
+ pParsRef->fUpdateLevel = fUpdateLevel;
pParsRwr->fVerbose = fVerbose;
pParsRef->fVerbose = fVerbose;
+
+ pAig = Aig_ManDup( pAig, 0 );
+
+ // balance
+ if ( fBalance )
+ {
+// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+// Aig_ManStop( pTemp );
+ }
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
@@ -182,20 +223,144 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
Aig_ManStop( pTemp );
// balance
+// if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ }
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ pParsRwr->fUseZeros = 1;
+ pParsRef->fUseZeros = 1;
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // balance
if ( fBalance )
{
- pAig = Dar_ManBalance( pTemp = pAig, 0 );
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
}
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ }
return pAig;
}
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
+//alias resyn "b; rw; rwz; b; rwz; b"
+//alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
+{
+ Vec_Ptr_t * vAigs;
+ vAigs = Vec_PtrAlloc( 3 );
+ pAig = Aig_ManDup(pAig, 0);
+ Vec_PtrPush( vAigs, pAig );
+ pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
+ Vec_PtrPush( vAigs, pAig );
+ pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, fVerbose);
+ Vec_PtrPush( vAigs, pAig );
+ return vAigs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
+{
+ Vec_Ptr_t * vAigs;
+ Aig_Man_t * pMan;
+ vAigs = Vec_PtrAlloc( 3 );
+ pMan = Ioa_ReadAiger( "i10_1.aig", 1 );
+ Vec_PtrPush( vAigs, pMan );
+ pMan = Ioa_ReadAiger( "i10_2.aig", 1 );
+ Vec_PtrPush( vAigs, pMan );
+ pMan = Ioa_ReadAiger( "i10_3.aig", 1 );
+ Vec_PtrPush( vAigs, pMan );
+ return vAigs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
+{
+ Aig_Man_t * pMan, * pTemp;
+ Vec_Ptr_t * vAigs;
+ int i, clk;
+
+clk = clock();
+// vAigs = Dar_ManChoiceSynthesisExt();
+ vAigs = Dar_ManChoiceSynthesis( pAig, fBalance, fUpdateLevel, fVerbose );
+
+ // swap the first and last network
+ // this should lead to the primary choice being "better" because of synthesis
+ pMan = Vec_PtrPop( vAigs );
+ Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
+ Vec_PtrWriteEntry( vAigs, 0, pMan );
+
+if ( fVerbose )
+{
+PRT( "Synthesis time", clock() - clk );
+}
+clk = clock();
+ pMan = Aig_ManChoicePartitioned( vAigs, 300 );
+ Vec_PtrForEachEntry( vAigs, pTemp, i )
+ Aig_ManStop( pTemp );
+ Vec_PtrFree( vAigs );
+if ( fVerbose )
+{
+PRT( "Choicing time ", clock() - clk );
+}
+ return pMan;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/dar/module.make b/src/aig/dar/module.make
index 09b45171..0a1f7687 100644
--- a/src/aig/dar/module.make
+++ b/src/aig/dar/module.make
@@ -4,6 +4,7 @@ SRC += src/aig/dar/darBalance.c \
src/aig/dar/darData.c \
src/aig/dar/darLib.c \
src/aig/dar/darMan.c \
+ src/aig/dar/darPrec.c \
src/aig/dar/darRefact.c \
src/aig/dar/darResub.c \
src/aig/dar/darScript.c \
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-28 16:50:24 +0000