summaryrefslogtreecommitdiffstats
path: root/src/opt/dar/darScript.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/dar/darScript.c')
-rw-r--r--src/opt/dar/darScript.c927
1 files changed, 927 insertions, 0 deletions
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
new file mode 100644
index 00000000..79d6dfc4
--- /dev/null
+++ b/src/opt/dar/darScript.c
@@ -0,0 +1,927 @@
+/**CFile****************************************************************
+
+ FileName [darScript.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting.]
+
+ Synopsis [Rewriting scripts.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: darScript.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "darInt.h"
+#include "src/proof/dch/dch.h"
+#include "src/aig/gia/gia.h"
+#include "src/aig/gia/giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs one iteration of AIG rewriting.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
+{
+ Aig_Man_t * pTemp;
+ Dar_RwrPar_t Pars, * pPars = &Pars;
+ Dar_ManDefaultRwrParams( pPars );
+ pAig = Aig_ManDupDfs( pAig );
+ Dar_ManRewrite( pAig, pPars );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "rwsat".]
+
+ Description []
+
+ SideEffects [This procedure does not tighten level during restructuring.]
+
+ 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 * pTemp;
+
+ Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+ Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+
+ Dar_ManDefaultRwrParams( pParsRwr );
+ Dar_ManDefaultRefParams( pParsRef );
+
+ pParsRwr->fUpdateLevel = 0;
+ pParsRef->fUpdateLevel = 0;
+
+ pParsRwr->fVerbose = fVerbose;
+ pParsRef->fVerbose = fVerbose;
+//printf( "1" );
+ pAig = Aig_ManDupDfs( pAig );
+ if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
+
+//printf( "2" );
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+
+//Aig_ManDumpBlif( pAig, "inter.blif", NULL, NULL );
+//printf( "3" );
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
+
+//printf( "4" );
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
+
+//printf( "5" );
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+
+//printf( "6" );
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
+
+//printf( "7" );
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs one iteration of AIG rewriting.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_ManHaigPrintStats( Aig_Man_t * pAig )
+{
+ Aig_Obj_t * pObj;
+ int Counter, i;
+ Counter = 0;
+ Aig_ManForEachNode( pAig, pObj, i )
+ Counter += (pObj->pHaig != NULL);
+ printf( "Total nodes = %6d. Equiv nodes = %6d.\n", Aig_ManNodeNum(pAig), Counter );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, 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->fPower = fPower;
+
+ pParsRwr->fVerbose = 0;//fVerbose;
+ pParsRef->fVerbose = 0;//fVerbose;
+
+ pAig = Aig_ManDupDfs( pAig );
+ if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
+/*
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+*/
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
+
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+
+ pParsRwr->fUseZeros = 1;
+ pParsRef->fUseZeros = 1;
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
+
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, 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;
+
+ 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->fFanout = fFanout;
+ pParsRwr->fPower = fPower;
+
+ pParsRwr->fVerbose = 0;//fVerbose;
+ pParsRef->fVerbose = 0;//fVerbose;
+
+ pAig = Aig_ManDupDfs( pAig );
+ if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
+/*
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+*/
+ // rewrite
+// Dar_ManRewrite( pAig, pParsRwr );
+ pParsRwr->fUpdateLevel = 0; // disable level update
+ Dar_ManRewrite( pAig, pParsRwr );
+ pParsRwr->fUpdateLevel = fUpdateLevel; // reenable level update if needed
+
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
+
+ // balance
+// if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
+
+ pParsRwr->fUseZeros = 1;
+ pParsRef->fUseZeros = 1;
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
+
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "RefactorZ: " ), Aig_ManPrintStats( pAig );
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
+
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, 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;
+ Aig_Obj_t * pObj;
+ int i;
+
+ vAigs = Vec_PtrAlloc( 3 );
+ pAig = Aig_ManDupDfs(pAig);
+ Vec_PtrPush( vAigs, pAig );
+
+ Aig_ManForEachObj( pAig, pObj, i )
+ pObj->pHaig = pObj;
+
+ pAig = Dar_ManCompress(pAig, fBalance, fUpdateLevel, fPower, fVerbose);
+ Vec_PtrPush( vAigs, pAig );
+//Aig_ManPrintStats( pAig );
+
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ pObj->pNext = pObj->pHaig;
+ pObj->pHaig = pObj;
+ }
+
+ pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose);
+ Vec_PtrPush( vAigs, pAig );
+//Aig_ManPrintStats( pAig );
+
+ pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 1 );
+ Aig_ManForEachObj( pAig, pObj, i )
+ pObj->pHaig = pObj->pNext;
+
+ return vAigs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, 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, 0, fVerbose );
+
+ // swap the first and last network
+ // this should lead to the primary choice being "better" because of synthesis
+ // (it is also important when constructing choices)
+ if ( !fConstruct )
+ {
+ pMan = (Aig_Man_t *)Vec_PtrPop( vAigs );
+ Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
+ Vec_PtrWriteEntry( vAigs, 0, pMan );
+ }
+
+if ( fVerbose )
+{
+ABC_PRT( "Synthesis time", clock() - clk );
+}
+clk = clock();
+ if ( fConstruct )
+ pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
+ else
+ pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
+ Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
+ Aig_ManStop( pTemp );
+ Vec_PtrFree( vAigs );
+if ( fVerbose )
+{
+ABC_PRT( "Choicing time ", clock() - clk );
+}
+ return pMan;
+// return NULL;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_NewCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, 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->fPower = fPower;
+
+ pParsRwr->fVerbose = 0;//fVerbose;
+ pParsRef->fVerbose = 0;//fVerbose;
+
+// pAig = Aig_ManDupDfs( pAig );
+ if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
+
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+
+ pParsRwr->fUseZeros = 1;
+ pParsRef->fUseZeros = 1;
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
+
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_NewCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fLightSynth, 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;
+
+ 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->fFanout = fFanout;
+ pParsRwr->fPower = fPower;
+
+ pParsRwr->fVerbose = 0;//fVerbose;
+ pParsRef->fVerbose = 0;//fVerbose;
+
+// pAig = Aig_ManDupDfs( pAig );
+ if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
+
+ // skip if lighter synthesis is requested
+ if ( !fLightSynth )
+ {
+ // rewrite
+ //Dar_ManRewrite( pAig, pParsRwr );
+// pParsRwr->fUpdateLevel = 0; // disable level update // this change was requested in July and later disabled
+ Dar_ManRewrite( pAig, pParsRwr );
+// pParsRwr->fUpdateLevel = fUpdateLevel; // reenable level update if needed
+
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
+ }
+
+ // balance
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+
+ // skip if lighter synthesis is requested
+ if ( !fLightSynth )
+ {
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
+ }
+
+ pParsRwr->fUseZeros = 1;
+ pParsRef->fUseZeros = 1;
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
+
+ // skip if lighter synthesis is requested
+ if ( !fLightSynth )
+ {
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+ }
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "RefactorZ: " ), Aig_ManPrintStats( pAig );
+
+ // skip if lighter synthesis is requested
+ if ( !fLightSynth )
+ {
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
+ }
+
+ // balance
+ if ( fBalance )
+ {
+ pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+ Aig_ManStop( pTemp );
+ if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
+ }
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count the number of nodes with very high fanout count.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_NewChoiceSynthesisGuard( Aig_Man_t * pAig )
+{
+ Aig_Obj_t * pObj;
+ int i, Count = 0;
+ Aig_ManForEachNode( pAig, pObj, i )
+ if ( Aig_ObjRefs(pObj) > 1000 )
+ Count += Aig_ObjRefs(pObj) / 1000;
+ return (int)(Count > 10);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description [Takes AIG manager, consumes it, and produces GIA manager.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, 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 * vGias;
+ Gia_Man_t * pGia, * pTemp;
+ int i;
+
+ if ( fUpdateLevel && Dar_NewChoiceSynthesisGuard(pAig) )
+ {
+ if ( fVerbose )
+ printf( "Warning: Due to high fanout count of some nodes, level updating is disabled.\n" );
+ fUpdateLevel = 0;
+ }
+
+ vGias = Vec_PtrAlloc( 3 );
+ pGia = Gia_ManFromAig(pAig);
+ Vec_PtrPush( vGias, pGia );
+
+ pAig = Dar_NewCompress( pAig, fBalance, fUpdateLevel, fPower, fVerbose );
+ pGia = Gia_ManFromAig(pAig);
+ Vec_PtrPush( vGias, pGia );
+//Aig_ManPrintStats( pAig );
+
+ pAig = Dar_NewCompress2( pAig, fBalance, fUpdateLevel, 1, fPower, fLightSynth, fVerbose );
+ pGia = Gia_ManFromAig(pAig);
+ Vec_PtrPush( vGias, pGia );
+//Aig_ManPrintStats( pAig );
+
+ Aig_ManStop( pAig );
+
+ // swap around the first and the last
+ pTemp = (Gia_Man_t *)Vec_PtrPop( vGias );
+ Vec_PtrPush( vGias, Vec_PtrEntry(vGias,0) );
+ Vec_PtrWriteEntry( vGias, 0, pTemp );
+
+// Aig_Man_t * pAig;
+// int i;
+// printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
+// Vec_PtrForEachEntry( Aig_Man_t *, p->vAigs, pAig, i )
+// Aig_ManPrintStats( pAig );
+
+ // derive the miter
+ pGia = Gia_ManChoiceMiter( vGias );
+
+ // cleanup
+ Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i )
+ Gia_ManStop( pTemp );
+ Vec_PtrFree( vGias );
+ return pGia;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+/*
+Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+ extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+ extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+
+ int fVerbose = pPars->fVerbose;
+ int fConstruct = 0;
+ Aig_Man_t * pMan, * pTemp;
+ Vec_Ptr_t * vAigs;
+ int i, clk;
+
+clk = clock();
+// vAigs = Dar_ManChoiceSynthesisExt();
+// vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
+ vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, 0 );
+
+ // swap the first and last network
+ // this should lead to the primary choice being "better" because of synthesis
+ // (it is also important when constructing choices)
+ if ( !fConstruct )
+ {
+ pMan = Vec_PtrPop( vAigs );
+ Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
+ Vec_PtrWriteEntry( vAigs, 0, pMan );
+ }
+
+if ( fVerbose )
+{
+//ABC_PRT( "Synthesis time", clock() - clk );
+}
+ pPars->timeSynth = clock() - clk;
+
+clk = clock();
+ // perform choice computation
+ if ( pPars->fUseGia )
+ pMan = Cec_ComputeChoices( vAigs, pPars );
+ else
+ pMan = Dch_ComputeChoices( vAigs, pPars );
+
+ // reconstruct the network
+ pMan = Aig_ManDupDfsGuided( pTemp = pMan, Vec_PtrEntry(vAigs,0) );
+ Aig_ManStop( pTemp );
+ // duplicate the timing manager
+ pTemp = Vec_PtrEntry( vAigs, 0 );
+ if ( pTemp->pManTime )
+ {
+ extern void * Tim_ManDup( void * p, int fDiscrete );
+ pMan->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
+ }
+ // reset levels
+ Aig_ManChoiceLevel( pMan );
+ ABC_FREE( pMan->pName );
+ ABC_FREE( pMan->pSpec );
+ pMan->pName = Abc_UtilStrsav( pTemp->pName );
+ pMan->pSpec = Abc_UtilStrsav( pTemp->pSpec );
+
+ // cleanup
+ Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
+ Aig_ManStop( pTemp );
+ Vec_PtrFree( vAigs );
+
+if ( fVerbose )
+{
+//ABC_PRT( "Choicing time ", clock() - clk );
+}
+ return pMan;
+// return NULL;
+}
+*/
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description [Consumes the input AIG to reduce memory usage.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManChoiceNewAig( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+// extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
+ extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+ int fVerbose = pPars->fVerbose;
+ Aig_Man_t * pMan, * pTemp;
+ Vec_Ptr_t * vAigs;
+ Vec_Ptr_t * vPios;
+ void * pManTime;
+ char * pName, * pSpec;
+ int i, clk;
+
+clk = clock();
+ vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
+pPars->timeSynth = clock() - clk;
+ // swap the first and last network
+ // this should lead to the primary choice being "better" because of synthesis
+ // (it is also important when constructing choices)
+ pMan = (Aig_Man_t *)Vec_PtrPop( vAigs );
+ Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
+ Vec_PtrWriteEntry( vAigs, 0, pMan );
+
+ // derive the total AIG
+ pMan = Dch_DeriveTotalAig( vAigs );
+ // cleanup
+ Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
+ Aig_ManStop( pTemp );
+ Vec_PtrFree( vAigs );
+
+ // compute choices
+ pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
+ Aig_ManStop( pTemp );
+
+ // save useful things
+ pManTime = pAig->pManTime; pAig->pManTime = NULL;
+ pName = Abc_UtilStrsav( pAig->pName );
+ pSpec = Abc_UtilStrsav( pAig->pSpec );
+
+ // create guidence
+ vPios = Aig_ManOrderPios( pMan, pAig );
+ Aig_ManStop( pAig );
+
+ // reconstruct the network
+ pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
+ Aig_ManStop( pTemp );
+ Vec_PtrFree( vPios );
+
+ // reset levels
+ pMan->pManTime = pManTime;
+ Aig_ManChoiceLevel( pMan );
+
+ // copy names
+ ABC_FREE( pMan->pName );
+ ABC_FREE( pMan->pSpec );
+ pMan->pName = pName;
+ pMan->pSpec = pSpec;
+ return pMan;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description [Consumes the input AIG to reduce memory usage.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+ extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
+// extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
+ extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+ int fVerbose = pPars->fVerbose;
+ Aig_Man_t * pMan, * pTemp;
+ Gia_Man_t * pGia;
+ Vec_Ptr_t * vPios;
+ void * pManTime;
+ char * pName, * pSpec;
+ int clk;
+
+ // save useful things
+ pManTime = pAig->pManTime; pAig->pManTime = NULL;
+ pName = Abc_UtilStrsav( pAig->pName );
+ pSpec = Abc_UtilStrsav( pAig->pSpec );
+
+ // perform synthesis
+clk = clock();
+ pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
+pPars->timeSynth = clock() - clk;
+
+ // perform choice computation
+ if ( pPars->fUseGia )
+ pMan = Cec_ComputeChoices( pGia, pPars );
+ else
+ {
+ pMan = Gia_ManToAigSkip( pGia, 3 );
+ Gia_ManStop( pGia );
+ pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
+ Aig_ManStop( pTemp );
+ }
+
+ // create guidence
+ vPios = Aig_ManOrderPios( pMan, pAig );
+ Aig_ManStop( pAig );
+
+ // reconstruct the network
+ pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
+ Aig_ManStop( pTemp );
+ Vec_PtrFree( vPios );
+
+ // reset levels
+ pMan->pManTime = pManTime;
+ Aig_ManChoiceLevel( pMan );
+
+ // copy names
+ ABC_FREE( pMan->pName );
+ ABC_FREE( pMan->pSpec );
+ pMan->pName = pName;
+ pMan->pSpec = pSpec;
+ return pMan;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+