Detecting properties of internal nodes.

3 files changed, 15 insertions, 186 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a5b96c24..5ac2cd09 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7216,7 +7216,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fVerbose );
     Abc_Ntk_t * pNtk;
     int c, fVerbose = 0;
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -7244,7 +7244,7 @@ int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Only applicable to a logic network.\n" );
         return 1;
     }
-    Abc_NtkDetectClassesTest( pNtk );
+    Abc_NtkDetectClassesTest( pNtk, fVerbose );
     return 0;
 
 usage:
diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c
index 91fa2d9f..8fa395e8 100644
--- a/src/base/abci/abcDetect.c
+++ b/src/base/abci/abcDetect.c
@@ -8,7 +8,7 @@
 
   Synopsis    [Detect conditions.]
 
-  Author      [Alan Mishchenko]
+  Author      [Alan Mishchenko, Dao Ai Quoc]
   
   Affiliation [UC Berkeley]
 
@@ -21,10 +21,11 @@
 #include "base/abc/abc.h"
 #include "misc/vec/vecHsh.h"
 #include "misc/util/utilNam.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -45,15 +46,6 @@ typedef enum {
     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                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -145,6 +137,7 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
     assert( Vec_IntSize(vMap) == Abc_NamObjNumMax(pNam) );
     // read file lines
     vPairs = Vec_IntAlloc( 1000 );
+    Vec_IntPushTwo( vPairs, -1, -1 );
     while ( fgets(Buffer, 1000, pFile) != NULL )
     {
         // read line number
@@ -168,17 +161,18 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
         Type = Io_ReadFinType( pToken );
         if ( Type == ABC_FIN_NONE )
         {
-            printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(pObj) );
+            printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(Abc_NtkObj(pNtk, iObj)) );
             continue;
         }
         Vec_IntPushTwo( vPairs, Vec_IntEntry(vMap, iObj), Type );
     }
+    assert( Vec_IntSize(vPairs) == 2 * nLines );
     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) );
+        Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 )
+            printf( "%-10d%-10s%-10s\n", i/2, Abc_ObjName(Abc_NtkObj(pNtk, iObj)), Io_WriteFinType(Type) );
 
 finish:
     Vec_IntFree( vMap );
@@ -190,138 +184,7 @@ finish:
 
 /**Function*************************************************************
 
-  Synopsis    [Detect equivalence classes of nodes in terms of their TFO.]
-
-  Description [Given is the logic network (pNtk) and the set of objects
-  (primary inputs or internal nodes) to be considered (vObjs), this function
-  returns a set of equivalence classes of these objects in terms of their 
-  transitive fanout (TFO). Two objects belong to the same class if the set 
-  of COs they feed into are the same.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkDetectClasses_rec( Abc_Obj_t * pObj, Vec_Int_t * vMap, Hsh_VecMan_t * pHash, Vec_Int_t * vTemp )
-{
-    Vec_Int_t * vArray, * vSet;
-    Abc_Obj_t * pNext; int i;
-    // get the CO set for this object
-    int Entry = Vec_IntEntry(vMap, Abc_ObjId(pObj));
-    if ( Entry != -1 ) // the set is already computed
-        return Entry;
-    // compute a new CO set
-    assert( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) );
-    // if there is no fanouts, the set of COs is empty
-    if ( Abc_ObjFanoutNum(pObj) == 0 )
-    {
-        Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), 0 );
-        return 0;
-    }
-    // compute the set for the first fanout
-    Entry = Abc_NtkDetectClasses_rec( Abc_ObjFanout0(pObj), vMap, pHash, vTemp );
-    if ( Abc_ObjFanoutNum(pObj) == 1 )
-        return Entry;
-    vSet = Vec_IntAlloc( 16 );
-    // initialize the set with that of first fanout
-    vArray = Hsh_VecReadEntry( pHash, Entry );
-    Vec_IntClear( vSet );
-    Vec_IntAppend( vSet, vArray );
-    // iteratively add sets of other fanouts
-    Abc_ObjForEachFanout( pObj, pNext, i )
-    {
-        if ( i == 0 ) 
-            continue;
-        Entry = Abc_NtkDetectClasses_rec( pNext, vMap, pHash, vTemp );
-        vArray = Hsh_VecReadEntry( pHash, Entry );
-        Vec_IntTwoMerge2( vSet, vArray, vTemp );
-        ABC_SWAP( Vec_Int_t, *vSet, *vTemp );
-    }
-    // create or find new set and map the object into it
-    Entry = Hsh_VecManAdd( pHash, vSet );
-    Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), Entry );
-    Vec_IntFree( vSet );
-    return Entry;
-}
-Vec_Wec_t * Abc_NtkDetectClasses( Abc_Ntk_t * pNtk, Vec_Int_t * vObjs )
-{
-    Vec_Wec_t * vClasses;   // classes of equivalence objects from vObjs
-    Vec_Int_t * vClassMap;  // mapping of each CO set into its class in vClasses
-    Vec_Int_t * vClass;     // one equivalence class     
-    Abc_Obj_t * pObj; 
-    int i, iObj, SetId, ClassId;
-    // create hash table to hash sets of CO indexes
-    Hsh_VecMan_t * pHash = Hsh_VecManStart( 1000 );
-    // create elementary sets (each composed of one CO) and map COs into them
-    Vec_Int_t * vMap = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) );
-    Vec_Int_t * vSet = Vec_IntAlloc( 16 );
-    assert( Abc_NtkIsLogic(pNtk) );
-    // compute empty set
-    SetId = Hsh_VecManAdd( pHash, vSet );
-    assert( SetId == 0 );
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        Vec_IntFill( vSet, 1, i );
-        SetId = Hsh_VecManAdd( pHash, vSet );
-        Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), SetId );
-    }
-    // make sure the array of objects is sorted
-    Vec_IntSort( vObjs, 0 );
-    // begin from the objects and map their IDs into sets of COs
-    Abc_NtkForEachObjVec( vObjs, pNtk, pObj, i )
-        Abc_NtkDetectClasses_rec( pObj, vMap, pHash, vSet );
-    Vec_IntFree( vSet );
-    // create map for mapping CO set its their classes
-    vClassMap = Vec_IntStartFull( Hsh_VecSize(pHash) + 1 );
-    // collect classes of objects
-    vClasses = Vec_WecAlloc( 1000 );
-    Vec_IntForEachEntry( vObjs, iObj, i )
-    {
-        // for a given object (iObj), find the ID of its COs set
-        SetId = Vec_IntEntry( vMap, iObj );
-        assert( SetId >= 0 );
-        // for the given CO set, finds its equivalence class
-        ClassId = Vec_IntEntry( vClassMap, SetId );
-        if ( ClassId == -1 )  // there is no equivalence class
-        {
-            // map this CO set into a new equivalence class
-            Vec_IntWriteEntry( vClassMap, SetId, Vec_WecSize(vClasses) );
-            vClass = Vec_WecPushLevel( vClasses );
-        }
-        else // get hold of the equivalence class
-            vClass = Vec_WecEntry( vClasses, ClassId );
-        // add objects to the class
-        Vec_IntPush( vClass, iObj );
-        // print the set for this object
-        //printf( "Object %5d : ", iObj );
-        //Vec_IntPrint( Hsh_VecReadEntry(pHash, SetId) );
-    }
-    Hsh_VecManStop( pHash );
-    Vec_IntFree( vClassMap );
-    Vec_IntFree( vMap );
-    return vClasses;
-}
-void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk )
-{
-    Vec_Int_t * vObjs;
-    Vec_Wec_t * vRes;
-    // for testing, create the set of object IDs for all combinational inputs (CIs)
-    Abc_Obj_t * pObj; int i;
-    vObjs = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
-    Abc_NtkForEachCi( pNtk, pObj, i )
-        Vec_IntPush( vObjs, Abc_ObjId(pObj) );
-    // compute equivalence classes of CIs and print them
-    vRes = Abc_NtkDetectClasses( pNtk, vObjs );
-    Vec_WecPrint( vRes, 0 );
-    // clean up
-    Vec_IntFree( vObjs );
-    Vec_WecFree( vRes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Miter construction.]
+  Synopsis    [Top-level procedure.]
 
   Description []
                
@@ -330,46 +193,12 @@ void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Abc_NtkComputeObjects( Vec_Int_t * vPairs )
+void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    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 );
+    printf( "This procedure is currently not used.\n" );
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index 0d3868b3..ce23ce96 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -556,7 +556,7 @@ int Cba_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameUpdateGia( pAbc, pNew );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%blast [-svh]\n" );
+    Abc_Print( -2, "usage: @blast [-svh]\n" );
     Abc_Print( -2, "\t         performs bit-blasting of the word-level design\n" );
     Abc_Print( -2, "\t-s     : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );