Reading/writing MiniAIG and several minor changes.

abclib.dsp

@@ -3575,6 +3575,10 @@ SOURCE=.\src\aig\gia\giaMem.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaMini.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaPat.c
 # End Source File
 # Begin Source File

src/aig/gia/gia.h

@@ -876,6 +876,7 @@ extern Gia_Man_t *         Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t *
 extern Gia_Man_t *         Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
 extern Gia_Man_t *         Gia_ManDupOneHot( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupLevelized( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
 /*=== giaEnable.c ==========================================================*/
 extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
 extern Gia_Man_t *         Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
@@ -984,6 +985,9 @@ extern void                Gia_MmStepStop( Gia_MmStep_t * p, int fVerbose );
 extern char *              Gia_MmStepEntryFetch( Gia_MmStep_t * p, int nBytes );
 extern void                Gia_MmStepEntryRecycle( Gia_MmStep_t * p, char * pEntry, int nBytes );
 extern int                 Gia_MmStepReadMemUsage( Gia_MmStep_t * p );
+/*=== giaMini.c ===========================================================*/
+extern Gia_Man_t *         Gia_ManReadMiniAig( char * pFileName );
+extern void                Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
 /*=== giaPat.c ===========================================================*/
 extern void                Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
 /*=== giaRetime.c ===========================================================*/
@@ -1100,6 +1104,9 @@ extern void                Gia_ManInvertPos( Gia_Man_t * pAig );
 extern int                 Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
 extern void                Gia_ManMarkFanoutDrivers( Gia_Man_t * p );
 extern void                Gia_ManSwapPos( Gia_Man_t * p, int i );
+extern Vec_Int_t *         Gia_ManSaveValue( Gia_Man_t * p );
+extern void                Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues );
+
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;

src/aig/gia/giaDup.c

@@ -2317,6 +2317,41 @@ Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    // start the new manager
+    pNew = Gia_ManStart( 5000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    // create constant
+    Gia_ManConst0(p)->Value = 0;
+    // create PIs
+    Gia_ManForEachObjVec( vCis, p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // create internal nodes
+    Gia_ManForEachObjVec( vAnds, p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // create ROs
+    Gia_ManForEachObjVec( vCos, p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, nRegs );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaIso.c

@@ -955,41 +955,6 @@ void Gia_ManFindCaninicalOrder( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAn
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs )
-{
-    Gia_Man_t * pNew;
-    Gia_Obj_t * pObj;
-    int i;
-    // start the new manager
-    pNew = Gia_ManStart( 5000 );
-    pNew->pName = Abc_UtilStrsav( p->pName );
-    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
-    // create constant
-    Gia_ManConst0(p)->Value = 0;
-    // create PIs
-    Gia_ManForEachObjVec( vCis, p, pObj, i )
-        pObj->Value = Gia_ManAppendCi( pNew );
-    // create internal nodes
-    Gia_ManForEachObjVec( vAnds, p, pObj, i )
-        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    // create ROs
-    Gia_ManForEachObjVec( vCos, p, pObj, i )
-        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-    Gia_ManSetRegNum( pNew, nRegs );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose )
 {
     Gia_Man_t * pRes = NULL;

src/aig/gia/giaMini.c

+/**CFile****************************************************************
+
+  FileName    [giaMini.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Reader/writer for MiniAIG.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaMini.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "base/main/main.h"
+#include "aig/miniaig/miniaig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Converts MiniAIG into GIA.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjFromMiniFanin0Copy( Gia_Man_t * pGia, Vec_Int_t * vCopies, Mini_Aig_t * p, int Id )
+{
+    int Lit = Mini_AigNodeFanin0( p, Id );
+    return Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) );
+}
+int Gia_ObjFromMiniFanin1Copy( Gia_Man_t * pGia, Vec_Int_t * vCopies, Mini_Aig_t * p, int Id )
+{
+    int Lit = Mini_AigNodeFanin1( p, Id );
+    return Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) );
+}
+Gia_Man_t * Gia_ManFromMiniAig( Mini_Aig_t * p )
+{
+    Gia_Man_t * pGia, * pTemp;
+    Vec_Int_t * vCopies;
+    int i, iGiaLit, nNodes;
+    // get the number of nodes
+    nNodes = Mini_AigNodeNum(p);
+    // create ABC network
+    pGia = Gia_ManStart( nNodes );
+    pGia->pName = Abc_UtilStrsav( "MiniAig" );
+    // create mapping from MiniAIG objects into ABC objects
+    vCopies = Vec_IntAlloc( nNodes );
+    Vec_IntPush( vCopies, 0 );
+    // iterate through the objects
+    Gia_ManHashAlloc( pGia );
+    for ( i = 1; i < nNodes; i++ )
+    {
+        if ( Mini_AigNodeIsPi( p, i ) )
+            iGiaLit = Gia_ManAppendCi(pGia);
+        else if ( Mini_AigNodeIsPo( p, i ) )
+            iGiaLit = Gia_ManAppendCo(pGia, Gia_ObjFromMiniFanin0Copy(pGia, vCopies, p, i));
+        else if ( Mini_AigNodeIsAnd( p, i ) )
+            iGiaLit = Gia_ManHashAnd(pGia, Gia_ObjFromMiniFanin0Copy(pGia, vCopies, p, i), Gia_ObjFromMiniFanin1Copy(pGia, vCopies, p, i));
+        else assert( 0 );
+        Vec_IntPush( vCopies, iGiaLit );
+    }
+    Gia_ManHashStop( pGia );
+    assert( Vec_IntSize(vCopies) == nNodes );
+    Vec_IntFree( vCopies );
+    Gia_ManSetRegNum( pGia, Mini_AigRegNum(p) );
+    pGia = Gia_ManCleanup( pTemp = pGia );
+    Gia_ManStop( pTemp );
+    return pGia;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts GIA into MiniAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mini_Aig_t * Gia_ManToMiniAig( Gia_Man_t * pGia )
+{
+    Mini_Aig_t * p;
+    Gia_Obj_t * pObj;
+    int i;
+    // create the manager
+    p = Mini_AigStart();
+    Gia_ManConst0(pGia)->Value = Mini_AigLitConst0();
+    // create primary inputs
+    Gia_ManForEachCi( pGia, pObj, i )
+        pObj->Value = Mini_AigCreatePi(p);
+    // create internal nodes
+    Gia_ManForEachAnd( pGia, pObj, i )
+        pObj->Value = Mini_AigAnd( p, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // create primary outputs
+    Gia_ManForEachCo( pGia, pObj, i )
+        pObj->Value = Mini_AigCreatePo( p, Gia_ObjFanin0Copy(pObj) );
+    // set registers
+    Mini_AigSetRegNum( p, Gia_ManRegNum(pGia) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedures to input/output MiniAIG into/from internal GIA.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FrameGiaInputMiniAig( Abc_Frame_t * pAbc, void * p )
+{
+    Gia_Man_t * pGia;
+    if ( pAbc == NULL )
+        printf( "ABC framework is not initialized by calling Abc_Start()\n" );
+    pGia = Gia_ManFromMiniAig( (Mini_Aig_t *)p );
+    Abc_FrameUpdateGia( pAbc, pGia );
+//    Gia_ManDelete( pGia );
+}
+void * Abc_FrameGiaOutputMiniAig( Abc_Frame_t * pAbc )
+{
+    Gia_Man_t * pGia;
+    if ( pAbc == NULL )
+        printf( "ABC framework is not initialized by calling Abc_Start()\n" );
+    pGia = Abc_FrameReadGia( pAbc );
+    if ( pGia == NULL )
+        printf( "Current network in ABC framework is not defined.\n" );
+    return Gia_ManToMiniAig( pGia );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedures to read/write GIA to/from MiniAIG file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManReadMiniAig( char * pFileName )
+{
+    Mini_Aig_t * p = Mini_AigLoad( pFileName );
+    Gia_Man_t * pGia = Gia_ManFromMiniAig( p );
+    Mini_AigStop( p );
+    return pGia;
+}
+void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName )
+{
+    Mini_Aig_t * p = Gia_ManToMiniAig( pGia );
+    Mini_AigDump( p, pFileName );
+    Mini_AigStop( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/aig/gia/giaUtil.c

@@ -1363,6 +1363,35 @@ void Gia_ManSwapPos( Gia_Man_t * p, int i )
     Gia_ManPatchCoDriver( p, i, Lit0 );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Save/load value from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManSaveValue( Gia_Man_t * p )
+{
+    Vec_Int_t * vValues;
+    Gia_Obj_t * pObj;
+    int i;
+    vValues = Vec_IntAlloc( Gia_ManObjNum(p) );
+    Gia_ManForEachObj( p, pObj, i )
+        Vec_IntPush( vValues, pObj->Value );
+    return vValues;
+}
+void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->Value = Vec_IntEntry(vValues, i);
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/module.make

@@ -28,6 +28,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaIso2.c \
     src/aig/gia/giaMan.c \
     src/aig/gia/giaMem.c \
+    src/aig/gia/giaMini.c \
     src/aig/gia/giaPat.c \
     src/aig/gia/giaRetime.c \
     src/aig/gia/giaScl.c \

src/base/abci/abc.c

@@ -23716,17 +23716,21 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pFile;
     char ** pArgvNew;
     char * FileName, * pTemp;
-    int nArgcNew;
-    int c, fVerbose = 0;
+    int c, nArgcNew;
+    int fUseMini = 0;
+    int fVerbose = 0;
     int fSkipStrash = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "smvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 's':
             fSkipStrash ^= 1;
             break;
+        case 'm':
+            fUseMini ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -23758,14 +23762,18 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     fclose( pFile );
 
-    pAig = Gia_AigerRead( FileName, fSkipStrash, 0 );
+    if ( fUseMini )
+        pAig = Gia_ManReadMiniAig( FileName );
+    else
+        pAig = Gia_AigerRead( FileName, fSkipStrash, 0 );
     Abc_FrameUpdateGia( pAbc, pAig );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &r [-svh] <file>\n" );
+    Abc_Print( -2, "usage: &r [-smvh] <file>\n" );
     Abc_Print( -2, "\t         reads the current AIG from the AIGER file\n" );
     Abc_Print( -2, "\t-s     : toggles structural hashing while reading [default = %s]\n", !fSkipStrash? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fUseMini? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : the file name\n");
@@ -24192,15 +24200,19 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     char ** pArgvNew;
     int c, nArgcNew;
     int fUnique = 0;
+    int fMiniAig = 0;
     int fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "uvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "umvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'u':
             fUnique ^= 1;
             break;
+        case 'm':
+            fMiniAig ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -24229,14 +24241,17 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         Gia_AigerWriteSimple( pGia, pFileName );
         Gia_ManStop( pGia );
     }
+    else if ( fMiniAig )
+        Gia_ManWriteMiniAig( pAbc->pGia, pFileName );
     else
         Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0 );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &w [-uvh] <file>\n" );
+    Abc_Print( -2, "usage: &w [-umvh] <file>\n" );
     Abc_Print( -2, "\t         writes the current AIG into the AIGER file\n" );
     Abc_Print( -2, "\t-u     : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
+    Abc_Print( -2, "\t-m     : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : the file name\n");

src/misc/vec/vecInt.h

@@ -1298,6 +1298,25 @@ static inline int Vec_IntTwoCountCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
     }
     return Counter;
 }
+static inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr )
+{
+    int * pBeg1 = vArr1->pArray;
+    int * pBeg2 = vArr2->pArray;
+    int * pEnd1 = vArr1->pArray + vArr1->nSize;
+    int * pEnd2 = vArr2->pArray + vArr2->nSize;
+    int Counter = 0;
+    Vec_IntClear( vArr );
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            Vec_IntPush( vArr, *pBeg1 ), pBeg1++, pBeg2++;
+        else if ( *pBeg1 < *pBeg2 )
+            pBeg1++;
+        else 
+            pBeg2++;
+    }
+    return Vec_IntSize(vArr);
+}
 
 /**Function*************************************************************