Adding features for invariant minimization.

1 files changed, 120 insertions, 31 deletions

diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
index 0bf27f7b..1a98fb71 100644
--- a/src/base/wlc/wlcAbc.c
+++ b/src/base/wlc/wlcAbc.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
+void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
 {
     Wlc_Obj_t * pObj;
     int i, k, nNum, nRange, nBits = 0;
@@ -53,7 +53,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
         nRange = Wlc_ObjRange(pObj);
         for ( k = 0; k < nRange; k++ )
         {
-            nNum = Vec_IntEntry(vInv, nBits + k);
+            nNum = Vec_IntEntry(vCounts, nBits + k);
             if ( nNum )
                 break;
         }
@@ -65,7 +65,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
         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 );
+            nNum = Vec_IntEntry( vCounts, nBits + k );
             if ( nNum == 0 )
                 continue;
             printf( "  [%d] -> %d", k, nNum );
@@ -73,8 +73,8 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
         printf( "\n");
         nBits += nRange;
     }
-    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
-    assert( Vec_IntSize(vInv) == nBits );
+    //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+    assert( Vec_IntSize(vCounts) == nBits );
 }
 
 /**Function*************************************************************
@@ -88,8 +88,14 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose )
+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;
@@ -98,46 +104,69 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
     // 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);
+    pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv");
     // create primary inputs
-    Wlc_NtkForEachCi( pNtk, pObj, i )
+    if ( pNtk == NULL )
     {
-        if ( pObj->Type != WLC_OBJ_FO )
-            continue;
-        nRange = Wlc_ObjRange(pObj);
-        for ( k = 0; k < nRange; k++ )
+        int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) );
+        Vec_IntForEachEntry( vCounts, Entry, i )
         {
-            nNum = Vec_IntEntry(vInv, nBits + k);
-            if ( nNum )
-                break;
+            if ( Entry == 0 )
+                continue;
+            pMainObj = Abc_NtkCreatePi( pMainNtk );
+            sprintf( Buffer, "pi%d", i );
+            Abc_ObjAssignName( pMainObj, Buffer, NULL );
         }
-        if ( k == nRange )
+        if ( Abc_NtkPiNum(pMainNtk) != nInputs )
         {
-            nBits += nRange;
-            continue;
+            printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" );
+            Abc_NtkDelete( pMainNtk );
+            return NULL;
         }
-        //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
-        for ( k = 0; k < nRange; k++ )
+    }
+    else
+    {
+        Wlc_NtkForEachCi( pNtk, pObj, i )
         {
-            nNum = Vec_IntEntry( vInv, nBits + k );
-            if ( nNum == 0 )
+            if ( pObj->Type != WLC_OBJ_FO )
                 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 );
-
+            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( "\n");
-        nBits += nRange;
     }
-    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
-    assert( Vec_IntSize(vInv) == nBits );
+    //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 );
@@ -145,6 +174,66 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
     return pMainNtk;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Translate current network into an interpolant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs )
+{
+    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_Obj_t * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
+        char * pName, * pCube, * pSop = (char *)pNode->pData;
+        Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) );
+        Abc_Obj_t * pFanin; int i, k, Value, nLits;
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            assert( Abc_ObjIsCi(pFanin) );
+            pName = Abc_ObjName(pFanin);
+            for ( k = (int)strlen(pName)-1; k >= 0; k-- )
+                if ( pName[k] < '0' || pName[k] > '9' )
+                    break;
+            if ( k == (int)strlen(pName)-1 )
+            {
+                printf( "Cannot read input name of fanin %d.\n", i );
+                Value = i;
+            }
+            else 
+                Value = atoi(pName + k + 1);
+            Vec_IntPush( vFanins, Value );
+        }
+        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                                ///
 ////////////////////////////////////////////////////////////////////////