From 8ad1729aa9f3f9da65c36f89a57a8272ece196d9 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 23 Oct 2013 10:44:11 -0700
Subject: Adding new synthesis scripts.

---
 src/aig/gia/gia.h        |  5 ++++
 src/aig/gia/giaBalance.c | 70 ++++++++++++++++++++++++++++++++++++++++++++++--
 src/aig/gia/giaUtil.c    |  1 +
 3 files changed, 74 insertions(+), 2 deletions(-)

(limited to 'src/aig/gia')

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 4d1e2f26..122e5025 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -937,6 +937,9 @@ extern void                Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFile
 /*=== giaBalance.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fVerbose );
 extern Gia_Man_t *         Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t *         Gia_ManAigSyn2( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t *         Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t *         Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
 /*=== giaBidec.c ===========================================================*/
 extern unsigned *          Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
 extern Gia_Man_t *         Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
@@ -1062,6 +1065,8 @@ extern Gia_Man_t *         Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFram
 /*=== giaFront.c ==========================================================*/
 extern Gia_Man_t *         Gia_ManFront( Gia_Man_t * p );
 extern void                Gia_ManFrontTest( Gia_Man_t * p );
+/*=== giaFx.c ==========================================================*/
+extern Gia_Man_t *         Gia_ManPerformFx( Gia_Man_t * p, int nNewNodesMax, int LitCountMax, int fReverse, int fVerbose, int fVeryVerbose );
 /*=== giaHash.c ===========================================================*/
 extern void                Gia_ManHashAlloc( Gia_Man_t * p ); 
 extern void                Gia_ManHashStart( Gia_Man_t * p ); 
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index d3bb8407..cae652e9 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -965,7 +965,7 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
     pNew1 = Dam_ManAreaBalanceInt( pNew, vCiLevels, nNewNodesMax, fVerbose, fVeryVerbose );
     if ( fVerbose )     Gia_ManPrintStats( pNew1, NULL );
     Gia_ManStop( pNew );
-    Vec_IntFree( vCiLevels );
+    Vec_IntFreeP( &vCiLevels );
     // derive the final result
     pNew2 = Gia_ManDupNoMuxes( pNew1 );
     if ( fVerbose )     Gia_ManPrintStats( pNew2, NULL );
@@ -984,7 +984,7 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
+Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
     Jf_Par_t Pars, * pPars = &Pars;
@@ -1003,6 +1003,72 @@ Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
     Gia_ManStop( pTemp );
     return pNew;
 }
+Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Jf_Par_t Pars, * pPars = &Pars;
+    Jf_ManSetDefaultPars( pPars );
+    if ( fVerbose )     Gia_ManPrintStats( p, NULL );
+    // perform balancing
+    pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    // perform mapping
+    pPars->nLutSize = 6;
+    pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+//    Gia_ManStop( pTemp );
+    // perform balancing
+    pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    Gia_ManStop( pTemp );
+    // perform mapping
+    pPars->nLutSize = 4;
+    pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+//    Gia_ManStop( pTemp );
+    // perform balancing
+    pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Jf_Par_t Pars, * pPars = &Pars;
+    Jf_ManSetDefaultPars( pPars );
+    if ( fVerbose )     Gia_ManPrintStats( p, NULL );
+    // perform balancing
+    pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    // perform mapping
+    pPars->nLutSize = 7;
+    pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+//    Gia_ManStop( pTemp );
+    // perform extraction
+    pNew = Gia_ManPerformFx( pTemp = pNew, ABC_INFINITY, 0, 0, fVeryVerbose, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    Gia_ManStop( pTemp );
+    // perform balancing
+    pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    Gia_ManStop( pTemp );
+    // perform mapping
+    pPars->nLutSize = 5;
+    pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+//    Gia_ManStop( pTemp );
+    // perform extraction
+    pNew = Gia_ManPerformFx( pTemp = pNew, ABC_INFINITY, 0, 0, fVeryVerbose, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    Gia_ManStop( pTemp );
+    // perform balancing
+    pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 353edb86..08136e7d 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -535,6 +535,7 @@ int Gia_ManSetLevels( Gia_Man_t * p, Vec_Int_t * vCiLevels )
     int i;
     if ( vCiLevels == NULL )
         return Gia_ManLevelNum( p );
+    assert( Vec_IntSize(vCiLevels) == Gia_ManCiNum(p) );
     Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
     p->nLevels = 0;
     Gia_ManForEachCi( p, pObj, i )
-- 
cgit v1.2.3