New upstream version 1.01+20180801git3fb3c6b+dfsg

1 files changed, 237 insertions, 116 deletions

diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
index 12425b0..1836f4e 100644
--- a/src/base/wlc/wlcAbc.c
+++ b/src/base/wlc/wlcAbc.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "wlc.h"

-#include "base/abc/abc.h"

+#include "wlc.h"
+#include "base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -30,120 +30,241 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
-

-/**Function*************************************************************

-

-  Synopsis    []

-

-  Description []

-

-  SideEffects []

-

-  SeeAlso     []

-

-***********************************************************************/

-void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )

-{

-    Wlc_Obj_t * pObj;

-    int i, k, nNum, nRange, nBits = 0;

-    Wlc_NtkForEachCi( pNtk, pObj, i )

-    {

-        if ( pObj->Type != WLC_OBJ_FO )

-            continue;

-        nRange = Wlc_ObjRange(pObj);

-        for ( k = 0; k < nRange; k++ )

-        {

-            nNum = Vec_IntEntry(vInv, nBits + k);

-            if ( nNum )

-                break;

-        }

-        if ( k == nRange )

-        {

-            nBits += nRange;

-            continue;

-        }

-        printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );

-        for ( k = 0; k < nRange; k++ )

-        {

-            nNum = Vec_IntEntry( vInv, nBits + k );

-            if ( nNum == 0 )

-                continue;

-            printf( "  [%d] -> %d", k, nNum );

-        }

-        printf( "\n");

-        nBits += nRange;

-    }

-    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );

-    assert( Vec_IntSize(vInv) == nBits );

-}

-

-/**Function*************************************************************

-

-  Synopsis    []

-

-  Description []

-               

-  SideEffects []

-

-  SeeAlso     []

-

-***********************************************************************/

-Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose )

-{

-    Wlc_Obj_t * pObj;

-    int i, k, nNum, nRange, nBits = 0;

-    Abc_Ntk_t * pMainNtk = NULL;

-    Abc_Obj_t * pMainObj, * pMainTemp;

-    char Buffer[5000];

-    // start the network

-    pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );

-    // duplicate the name and the spec

-    pMainNtk->pName = Extra_UtilStrsav(pNtk->pName);

-    // create primary inputs

-    Wlc_NtkForEachCi( pNtk, pObj, i )

-    {

-        if ( pObj->Type != WLC_OBJ_FO )

-            continue;

-        nRange = Wlc_ObjRange(pObj);

-        for ( k = 0; k < nRange; k++ )

-        {

-            nNum = Vec_IntEntry(vInv, nBits + k);

-            if ( nNum )

-                break;

-        }

-        if ( k == nRange )

-        {

-            nBits += nRange;

-            continue;

-        }

-        //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );

-        for ( k = 0; k < nRange; k++ )

-        {

-            nNum = Vec_IntEntry( vInv, nBits + k );

-            if ( nNum == 0 )

-                continue;

-            //printf( "  [%d] -> %d", k, nNum );

-            pMainObj = Abc_NtkCreatePi( pMainNtk );

-            sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );

-            Abc_ObjAssignName( pMainObj, Buffer, NULL );

-

-        }

-        //printf( "\n");

-        nBits += nRange;

-    }

-    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );

-    assert( Vec_IntSize(vInv) == nBits );

-    // create node

-    pMainObj = Abc_NtkCreateNode( pMainNtk );

-    Abc_NtkForEachPi( pMainNtk, pMainTemp, i )

-        Abc_ObjAddFanin( pMainObj, pMainTemp );

-    pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );

-    // create PO

-    pMainTemp = Abc_NtkCreatePo( pMainNtk );

-    Abc_ObjAddFanin( pMainTemp, pMainObj );

-    Abc_ObjAssignName( pMainTemp, "inv", NULL );

-    return pMainNtk;

-}

+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
+{
+    Wlc_Obj_t * pObj;
+    int i, k, nNum, nRange, nBits = 0;
+    Wlc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( pObj->Type != WLC_OBJ_FO )
+            continue;
+        nRange = Wlc_ObjRange(pObj);
+        for ( k = 0; k < nRange; k++ )
+        {
+            nNum = Vec_IntEntry(vCounts, nBits + k);
+            if ( nNum )
+                break;
+        }
+        if ( k == nRange )
+        {
+            nBits += nRange;
+            continue;
+        }
+        printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
+        for ( k = 0; k < nRange; k++ )
+        {
+            nNum = Vec_IntEntry( vCounts, nBits + k );
+            if ( nNum == 0 )
+                continue;
+            printf( "  [%d] -> %d", k, nNum );
+        }
+        printf( "\n");
+        nBits += nRange;
+    }
+    //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+    assert( Vec_IntSize(vCounts) == nBits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
+{
+    extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
+    extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );
+
+    Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+    Vec_Str_t * vSop = Pdr_InvPrintStr( vInv, vCounts );
+
+    Wlc_Obj_t * pObj;
+    int i, k, nNum, nRange, nBits = 0;
+    Abc_Ntk_t * pMainNtk = NULL;
+    Abc_Obj_t * pMainObj, * pMainTemp;
+    char Buffer[5000];
+    // start the network
+    pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+    // duplicate the name and the spec
+    pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv");
+    // create primary inputs
+    if ( pNtk == NULL )
+    {
+        int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) );
+        Vec_IntForEachEntry( vCounts, Entry, i )
+        {
+            if ( Entry == 0 )
+                continue;
+            pMainObj = Abc_NtkCreatePi( pMainNtk );
+            sprintf( Buffer, "pi%d", i );
+            Abc_ObjAssignName( pMainObj, Buffer, NULL );
+        }
+        if ( Abc_NtkPiNum(pMainNtk) != nInputs )
+        {
+            printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" );
+            Abc_NtkDelete( pMainNtk );
+            return NULL;
+        }
+    }
+    else
+    {
+        Wlc_NtkForEachCi( pNtk, pObj, i )
+        {
+            if ( pObj->Type != WLC_OBJ_FO )
+                continue;
+            nRange = Wlc_ObjRange(pObj);
+            for ( k = 0; k < nRange; k++ )
+            {
+                nNum = Vec_IntEntry(vCounts, nBits + k);
+                if ( nNum )
+                    break;
+            }
+            if ( k == nRange )
+            {
+                nBits += nRange;
+                continue;
+            }
+            //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
+            for ( k = 0; k < nRange; k++ )
+            {
+                nNum = Vec_IntEntry( vCounts, nBits + k );
+                if ( nNum == 0 )
+                    continue;
+                //printf( "  [%d] -> %d", k, nNum );
+                pMainObj = Abc_NtkCreatePi( pMainNtk );
+                sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
+                Abc_ObjAssignName( pMainObj, Buffer, NULL );
+
+            }
+            //printf( "\n");
+            nBits += nRange;
+        }
+    }
+    //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+    assert( pNtk == NULL || Vec_IntSize(vCounts) == nBits );
+    // create node
+    pMainObj = Abc_NtkCreateNode( pMainNtk );
+    Abc_NtkForEachPi( pMainNtk, pMainTemp, i )
+        Abc_ObjAddFanin( pMainObj, pMainTemp );
+    pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );
+    Vec_IntFree( vCounts );
+    Vec_StrFree( vSop );
+    // create PO
+    pMainTemp = Abc_NtkCreatePo( pMainNtk );
+    Abc_ObjAddFanin( pMainTemp, pMainObj );
+    Abc_ObjAssignName( pMainTemp, "inv", NULL );
+    return pMainNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Translate current network into an invariant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia )
+{
+    int nRegs = Gia_ManRegNum(pGia);
+    Vec_Int_t * vRes = NULL;
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+        printf( "The number of outputs is other than 1.\n" );
+    else if ( Abc_NtkNodeNum(pNtk) != 1 )
+        printf( "The number of internal nodes is other than 1.\n" );
+    else
+    {
+        Abc_Nam_t * pNames = NULL;
+        Abc_Obj_t * pFanin, * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
+        char * pName, * pCube, * pSop = (char *)pNode->pData;
+        Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) );
+        int i, k, Value, nLits, Counter = 0;
+        if ( pGia->vNamesIn )
+        {
+            // hash the names
+            pNames = Abc_NamStart( 100, 16 );
+            Vec_PtrForEachEntry( char *, pGia->vNamesIn, pName, i )
+            {
+                Value = Abc_NamStrFindOrAdd( pNames, pName, NULL );
+                assert( Value == i+1 );
+                //printf( "%s(%d) ", pName, i );
+            }
+            //printf( "\n" );
+        }
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            assert( Abc_ObjIsCi(pFanin) );
+            pName = Abc_ObjName(pFanin);
+            if ( pNames )
+            {
+                Value = Abc_NamStrFind(pNames, pName) - 1 - Gia_ManPiNum(pGia);
+                if ( Value < 0 )
+                {
+                    if ( Counter++ == 0 )
+                        printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i );
+                    Value = i;
+                }
+            }
+            else
+            {
+                for ( k = (int)strlen(pName)-1; k >= 0; k-- )
+                    if ( pName[k] < '0' || pName[k] > '9' )
+                        break;
+                if ( k == (int)strlen(pName)-1 )
+                {
+                    if ( Counter++ == 0 )
+                        printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i );
+                    Value = i;
+                }
+                else 
+                    Value = atoi(pName + k + 1);
+            }
+            Vec_IntPush( vFanins, Value );
+        }
+        if ( Counter )
+            printf( "Cannot read names for %d inputs of the invariant.\n", Counter );
+        if ( pNames )
+            Abc_NamStop( pNames );
+        assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) );
+        vRes = Vec_IntAlloc( 1000 );
+        Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) );
+        Abc_SopForEachCube( pSop, Abc_ObjFaninNum(pNode), pCube )
+        {
+            nLits = 0;
+            Abc_CubeForEachVar( pCube, Value, k )
+                if ( Value != '-' )
+                    nLits++;
+            Vec_IntPush( vRes, nLits );
+            Abc_CubeForEachVar( pCube, Value, k )
+                if ( Value != '-' )
+                    Vec_IntPush( vRes, Abc_Var2Lit(Vec_IntEntry(vFanins, k), (int)Value == '0') );
+        }
+        Vec_IntPush( vRes, nRegs );
+        Vec_IntFree( vFanins );
+    }
+    return vRes;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///