initial commit of public abc

1 files changed, 241 insertions, 8 deletions

diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c
index 22d5d6b8..9828d17e 100644
--- a/src/aig/saig/saigSimExt.c
+++ b/src/aig/saig/saigSimExt.c
@@ -21,6 +21,9 @@
 #include "saig.h"
 #include "ssw.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -49,13 +52,13 @@ static inline int Saig_ManSimInfoAnd( int Value0, int Value1 )
 
 static inline int Saig_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
 {
-    unsigned * pInfo = Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
+    unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
     return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1));
 }
 
 static inline void Saig_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
 {
-    unsigned * pInfo = Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
+    unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
     assert( Value >= SAIG_ZER && Value <= SAIG_UND );
     Value ^= Saig_ManSimInfoGet( vSimInfo, pObj, iFrame );
     pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1));
@@ -107,7 +110,7 @@ int Saig_ManExtendOneEval( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManSimDataInit( Aig_Man_t * p, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes )
+int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int i, f, Entry, iBit = 0;
@@ -146,7 +149,7 @@ int Saig_ManSimDataInit( Aig_Man_t * p, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo,
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManExtendOne( Aig_Man_t * p, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, 
+int Saig_ManExtendOne( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, 
     int iPi, int iFrame, Vec_Int_t * vUndo, Vec_Int_t * vVis, Vec_Int_t * vVis2 )
 {
     Aig_Obj_t * pFanout, * pObj = Aig_ManPi(p, iPi);
@@ -247,7 +250,7 @@ void Saig_ManExtendUndo( Aig_Man_t * p, Vec_Ptr_t * vSimInfo, Vec_Int_t * vUndo
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
+Vec_Int_t * Saig_ManExtendCounterExample0( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
 {
     Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
     int i, f, Value;
@@ -297,14 +300,244 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Ssw_C
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Ssw_Cex_t * pCex, int fVerbose )
+Vec_Int_t * Saig_ManExtendCounterExample1( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
+{
+    Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
+    int i, f, Value;
+//    assert( Aig_ManRegNum(p) > 0 );
+    assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) );
+    // start simulation data
+    Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );
+    assert( Value == SAIG_ONE );
+    // select the result
+    vRes = Vec_IntAlloc( 1000 );
+    vResInv = Vec_IntAlloc( 1000 );
+    vVis = Vec_IntAlloc( 1000 );
+    vVis2 = Vec_IntAlloc( 1000 );
+    vUndo = Vec_IntAlloc( 1000 );
+    for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- )
+    {
+        Vec_IntClear( vUndo );
+        for ( f = pCex->iFrame; f >= 0; f-- )
+            if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
+            {
+                Saig_ManExtendUndo( p, vSimInfo, vUndo );
+                break;
+            }
+        if ( f >= 0 )
+            Vec_IntPush( vRes, i );
+        else
+            Vec_IntPush( vResInv, i );
+    }
+    Vec_IntFree( vVis );
+    Vec_IntFree( vVis2 );
+    Vec_IntFree( vUndo );
+    // resimulate to make sure it is valid
+    Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
+    assert( Value == SAIG_ONE );
+    Vec_IntFree( vResInv );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of PIs for flops that should not be absracted.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManExtendCounterExample2( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
+{
+    Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
+    int i, f, Value;
+//    assert( Aig_ManRegNum(p) > 0 );
+    assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) );
+    // start simulation data
+    Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );
+    assert( Value == SAIG_ONE );
+    // select the result
+    vRes = Vec_IntAlloc( 1000 );
+    vResInv = Vec_IntAlloc( 1000 );
+    vVis = Vec_IntAlloc( 1000 );
+    vVis2 = Vec_IntAlloc( 1000 );
+    vUndo = Vec_IntAlloc( 1000 );
+    for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
+    {
+        if ( i % 2 == 0 )
+            continue;
+        Vec_IntClear( vUndo );
+        for ( f = pCex->iFrame; f >= 0; f-- )
+            if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
+            {
+                Saig_ManExtendUndo( p, vSimInfo, vUndo );
+                break;
+            }
+        if ( f >= 0 )
+            Vec_IntPush( vRes, i );
+        else
+            Vec_IntPush( vResInv, i );
+    }
+    for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
+    {
+        if ( i % 2 == 1 )
+            continue;
+        Vec_IntClear( vUndo );
+        for ( f = pCex->iFrame; f >= 0; f-- )
+            if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
+            {
+                Saig_ManExtendUndo( p, vSimInfo, vUndo );
+                break;
+            }
+        if ( f >= 0 )
+            Vec_IntPush( vRes, i );
+        else
+            Vec_IntPush( vResInv, i );
+    }
+    Vec_IntFree( vVis );
+    Vec_IntFree( vVis2 );
+    Vec_IntFree( vUndo );
+    // resimulate to make sure it is valid
+    Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
+    assert( Value == SAIG_ONE );
+    Vec_IntFree( vResInv );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of PIs for flops that should not be absracted.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManExtendCounterExample3( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
+{
+    Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
+    int i, f, Value;
+//    assert( Aig_ManRegNum(p) > 0 );
+    assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) );
+    // start simulation data
+    Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );
+    assert( Value == SAIG_ONE );
+    // select the result
+    vRes = Vec_IntAlloc( 1000 );
+    vResInv = Vec_IntAlloc( 1000 );
+    vVis = Vec_IntAlloc( 1000 );
+    vVis2 = Vec_IntAlloc( 1000 );
+    vUndo = Vec_IntAlloc( 1000 );
+    for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- )
+    {
+        if ( i % 2 == 0 )
+            continue;
+        Vec_IntClear( vUndo );
+        for ( f = pCex->iFrame; f >= 0; f-- )
+            if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
+            {
+                Saig_ManExtendUndo( p, vSimInfo, vUndo );
+                break;
+            }
+        if ( f >= 0 )
+            Vec_IntPush( vRes, i );
+        else
+            Vec_IntPush( vResInv, i );
+    }
+    for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- )
+    {
+        if ( i % 2 == 1 )
+            continue;
+        Vec_IntClear( vUndo );
+        for ( f = pCex->iFrame; f >= 0; f-- )
+            if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
+            {
+                Saig_ManExtendUndo( p, vSimInfo, vUndo );
+                break;
+            }
+        if ( f >= 0 )
+            Vec_IntPush( vRes, i );
+        else
+            Vec_IntPush( vResInv, i );
+    }
+    Vec_IntFree( vVis );
+    Vec_IntFree( vVis2 );
+    Vec_IntFree( vUndo );
+    // resimulate to make sure it is valid
+    Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
+    assert( Value == SAIG_ONE );
+    Vec_IntFree( vResInv );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of PIs for flops that should not be absracted.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
+{
+    Vec_Int_t * vRes0 = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
+    Vec_Int_t * vRes1 = Saig_ManExtendCounterExample1( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
+    Vec_Int_t * vRes2 = Saig_ManExtendCounterExample2( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
+    Vec_Int_t * vRes3 = Saig_ManExtendCounterExample3( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
+    Vec_Int_t * vRes  = vRes0;
+//    if ( fVerbose ) 
+        printf( "Removable flops: Order0 =%3d. Order1 =%3d. Order2 =%3d. Order3 =%3d.\n",
+            Vec_IntSize(vRes0), Vec_IntSize(vRes1), Vec_IntSize(vRes2), Vec_IntSize(vRes3) );
+    if ( Vec_IntSize(vRes1) <  Vec_IntSize(vRes) )
+        vRes = vRes1;
+    if ( Vec_IntSize(vRes2) <  Vec_IntSize(vRes) )
+        vRes = vRes2;
+    if ( Vec_IntSize(vRes3) <  Vec_IntSize(vRes) )
+        vRes = vRes3;
+    vRes = Vec_IntDup( vRes );
+    Vec_IntFree( vRes0 );
+    Vec_IntFree( vRes1 );
+    Vec_IntFree( vRes2 );
+    Vec_IntFree( vRes3 );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of PIs for flops that should not be absracted.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose )
 {
     Vec_Int_t * vRes;
     Vec_Ptr_t * vSimInfo;
     int clk;
+    if ( Saig_ManPiNum(p) != pCex->nPis )
+    {
+        printf( "Saig_ManExtendCounterExampleTest(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
+            Aig_ManPiNum(p), pCex->nPis );
+        return NULL;
+    }
     Aig_ManFanoutStart( p );
     vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) );
+    Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) );
+
 clk = clock();
+//    vRes = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
     vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
     if ( fVerbose )
     {
@@ -314,8 +547,6 @@ ABC_PRT( "Time", clock() - clk );
     Vec_PtrFree( vSimInfo );
     Aig_ManFanoutStop( p );
     return vRes;
-//    Vec_IntFree( vRes );
-//    return NULL;
 }
 
 ////////////////////////////////////////////////////////////////////////
@@ -323,3 +554,5 @@ ABC_PRT( "Time", clock() - clk );
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+