Detecting properties of internal nodes.

4 files changed, 267 insertions, 0 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 79eaf3e0..971f29bb 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -213,6 +213,7 @@ struct Abc_Ntk_t_
     Vec_Int_t *       vTopo;
     Vec_Ptr_t *       vAttrs;        // managers of various node attributes (node functionality, global BDDs, etc)
     Vec_Int_t *       vNameIds;      // name IDs
+    Vec_Int_t *       vFins;         // obj/type info
 };
 
 struct Abc_Des_t_ 
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index a2f5e138..e95306c9 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -1398,6 +1398,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Vec_PtrFreeP( &pNtk->vLtlProperties );
     Vec_IntFreeP( &pNtk->vObjPerm );
     Vec_IntFreeP( &pNtk->vTopo );
+    Vec_IntFreeP( &pNtk->vFins );
     ABC_FREE( pNtk );
 }
 
diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c
index 31121516..91fa2d9f 100644
--- a/src/base/abci/abcDetect.c
+++ b/src/base/abci/abcDetect.c
@@ -20,6 +20,7 @@
 
 #include "base/abc/abc.h"
 #include "misc/vec/vecHsh.h"
+#include "misc/util/utilNam.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,12 +29,167 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef enum { 
+    ABC_FIN_NONE = 0,      //  0:  unknown
+    ABC_FIN_SA0,           //  1:
+    ABC_FIN_SA1,           //  2:
+    ABC_FIN_NEG,           //  3:
+    ABC_FIN_RDOB_AND,      //  4:
+    ABC_FIN_RDOB_NAND,     //  5:
+    ABC_FIN_RDOB_OR,       //  6:
+    ABC_FIN_RDOB_NOR,      //  7:
+    ABC_FIN_RDOB_XOR,      //  8:
+    ABC_FIN_RDOB_NXOR,     //  9:
+    ABC_FIN_RDOB_NOT,      // 10:
+    ABC_FIN_RDOB_BUFF,     // 11:
+    ABC_FIN_RDOB_LAST      // 12:
+} Abc_FinType_t;
+
+typedef struct Fin_Info_t_
+{
+    Vec_Int_t * vPairs;    // original info as a set of pairs (ObjId, TypeId)
+    Vec_Int_t * vObjs;     // all those objects that have some info 
+    Vec_Wec_t * vMap;      // for each object, the set of types
+    Vec_Wec_t * vClasses;  // classes of objects
+
+} Abc_FinInfo_t;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Recognize type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_ReadFinType( char * pThis )
+{
+    if ( !strcmp(pThis, "SA0") )        return ABC_FIN_SA0;
+    if ( !strcmp(pThis, "SA1") )        return ABC_FIN_SA1;
+    if ( !strcmp(pThis, "NEG") )        return ABC_FIN_NEG;
+    if ( !strcmp(pThis, "RDOB_AND") )   return ABC_FIN_RDOB_AND;
+    if ( !strcmp(pThis, "RDOB_NAND") )  return ABC_FIN_RDOB_NAND;
+    if ( !strcmp(pThis, "RDOB_OR") )    return ABC_FIN_RDOB_OR;
+    if ( !strcmp(pThis, "RDOB_NOR") )   return ABC_FIN_RDOB_NOR;
+    if ( !strcmp(pThis, "RDOB_XOR") )   return ABC_FIN_RDOB_XOR;
+    if ( !strcmp(pThis, "RDOB_NXOR") )  return ABC_FIN_RDOB_NXOR;
+    if ( !strcmp(pThis, "RDOB_NOT") )   return ABC_FIN_RDOB_NOT;
+    if ( !strcmp(pThis, "RDOB_BUFF") )  return ABC_FIN_RDOB_BUFF;
+    return ABC_FIN_NONE;
+}
+char * Io_WriteFinType( int Type )
+{
+    if ( Type == ABC_FIN_SA0 )          return "SA0";
+    if ( Type == ABC_FIN_SA1 )          return "SA1";
+    if ( Type == ABC_FIN_NEG )          return "NEG";
+    if ( Type == ABC_FIN_RDOB_AND  )    return "RDOB_AND" ;
+    if ( Type == ABC_FIN_RDOB_NAND )    return "RDOB_NAND";
+    if ( Type == ABC_FIN_RDOB_OR   )    return "RDOB_OR"  ;
+    if ( Type == ABC_FIN_RDOB_NOR  )    return "RDOB_NOR" ;
+    if ( Type == ABC_FIN_RDOB_XOR  )    return "RDOB_XOR" ;
+    if ( Type == ABC_FIN_RDOB_NXOR )    return "RDOB_NXOR";
+    if ( Type == ABC_FIN_RDOB_NOT  )    return "RDOB_NOT" ;
+    if ( Type == ABC_FIN_RDOB_BUFF )    return "RDOB_BUFF";
+    return "Unknown";
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read information from file.]
+
+  Description [Returns information as a set of pairs: (ObjId, TypeId).
+  Uses the current network to map ObjName given in the file into ObjId.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
+{
+    char Buffer[1000];
+    Abc_Obj_t * pObj;
+    Abc_Nam_t * pNam;
+    Vec_Int_t * vMap; 
+    Vec_Int_t * vPairs = NULL;
+    int i, Type, iObj, fFound, nLines = 1;
+    FILE * pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open input file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    // map CI/node names into their IDs
+    pNam = Abc_NamStart( 1000, 10 );
+    vMap = Vec_IntAlloc( 1000 );
+    Vec_IntPush( vMap, -1 );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( !Abc_ObjIsCi(pObj) && !Abc_ObjIsNode(pObj) )
+            continue;
+        Abc_NamStrFindOrAdd( pNam, Abc_ObjName(pObj), &fFound );
+        if ( fFound )
+        {
+            printf( "The same name \"%s\" appears twice among CIs and internal nodes.\n", Abc_ObjName(pObj) );
+            goto finish;
+        }
+        Vec_IntPush( vMap, Abc_ObjId(pObj) );
+    }
+    assert( Vec_IntSize(vMap) == Abc_NamObjNumMax(pNam) );
+    // read file lines
+    vPairs = Vec_IntAlloc( 1000 );
+    while ( fgets(Buffer, 1000, pFile) != NULL )
+    {
+        // read line number
+        char * pToken = strtok( Buffer, " \n\r\t" );
+        if ( nLines++ != atoi(pToken) )
+        {
+            printf( "Line numbers are not consecutive. Quitting.\n" );
+            Vec_IntFreeP( &vPairs );
+            goto finish;
+        }
+        // read object name and find its ID
+        pToken = strtok( NULL, " \n\r\t" );
+        iObj = Abc_NamStrFind( pNam, pToken );
+        if ( !iObj )
+        {
+            printf( "Cannot find object with name \"%s\".\n", pToken );
+            continue;
+        }
+        // read type
+        pToken = strtok( NULL, " \n\r\t" );
+        Type = Io_ReadFinType( pToken );
+        if ( Type == ABC_FIN_NONE )
+        {
+            printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(pObj) );
+            continue;
+        }
+        Vec_IntPushTwo( vPairs, Vec_IntEntry(vMap, iObj), Type );
+    }
+    printf( "Finished reading %d lines.\n", nLines - 1 );
+
+    // verify the reader by printing the results
+    if ( fVerbose )
+        Vec_IntForEachEntryDouble( vPairs, iObj, Type, i )
+            printf( "%-10d%-10s%-10s\n", i/2+1, Abc_ObjName(Abc_NtkObj(pNtk, iObj)), Io_WriteFinType(Type) );
+
+finish:
+    Vec_IntFree( vMap );
+    Abc_NamDeref( pNam );
+    fclose( pFile );
+    return vPairs;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Detect equivalence classes of nodes in terms of their TFO.]
 
   Description [Given is the logic network (pNtk) and the set of objects
@@ -163,6 +319,57 @@ void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk )
     Vec_WecFree( vRes );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Miter construction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkComputeObjects( Vec_Int_t * vPairs )
+{
+    int iObj, Type, i;
+    Vec_Int_t * vObjs = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntryDouble( vPairs, iObj, Type, i )
+        Vec_IntPush( vObjs, iObj );
+    Vec_IntUniqify( vObjs );
+    return vObjs;
+}
+Vec_Wec_t * Abc_NtkComputeObjInfo( Vec_Int_t * vPairs, int nObjs )
+{
+    int iObj, Type, i;
+    Vec_Wec_t * vInfo = Vec_WecStart( nObjs );
+    Vec_IntForEachEntryDouble( vPairs, iObj, Type, i )
+        Vec_WecPush( vInfo, iObj, Type );
+    return vInfo;
+}
+void Abc_NtkSolveClassesTest( Abc_Ntk_t * pNtk )
+{
+    Abc_FinInfo_t * p;
+    if ( pNtk->vFins == NULL )
+    {
+        printf( "Current network does not have the required info.\n" );
+        return;
+    }
+    // collect data
+    p = ABC_CALLOC( Abc_FinInfo_t, 1 );
+    p->vPairs   = pNtk->vFins;
+    p->vObjs    = Abc_NtkComputeObjects( p->vPairs );
+    p->vMap     = Abc_NtkComputeObjInfo( p->vPairs, Abc_NtkObjNumMax(pNtk) );
+    p->vClasses = Abc_NtkDetectClasses( pNtk, p->vObjs );
+
+
+    // cleanup
+    Vec_WecFree( p->vClasses );
+    Vec_WecFree( p->vMap );
+    Vec_IntFree( p->vObjs );
+    ABC_FREE( p );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.c b/src/base/io/io.c
index e0e524fd..a5a64db6 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -40,6 +40,7 @@ static int IoCommandReadBench   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadDsd     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEdif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEqn     ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadFins    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadInit    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadPla     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadTruth   ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -104,6 +105,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_dsd",      IoCommandReadDsd,      1 );
 //    Cmd_CommandAdd( pAbc, "I/O", "read_edif",     IoCommandReadEdif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_eqn",      IoCommandReadEqn,      1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_fins",     IoCommandReadFins,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "read_init",     IoCommandReadInit,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_truth",    IoCommandReadTruth,    1 );
@@ -831,6 +833,62 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandReadFins( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose );
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    char * pFileName;
+    int c, fVerbose = 0;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    // check current network
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    // compute information and save it in the network
+    Vec_IntFreeP( &pNtk->vFins );
+    pNtk->vFins = Io_ReadFins( pNtk, pFileName, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_fins [-vh] <file>\n" );
+    fprintf( pAbc->Err, "\t         reads the network in equation format\n" );
+    fprintf( pAbc->Err, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;