Experiments with the mapper.

7 files changed, 117 insertions, 1 deletions

diff --git a/src/bool/kit/kitDsd.c b/src/bool/kit/kitDsd.c
index 7d85214b..cd02db67 100644
--- a/src/bool/kit/kitDsd.c
+++ b/src/bool/kit/kitDsd.c
@@ -2497,7 +2497,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
     p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 );
     pTruthC = Kit_DsdTruthCompute( p, pNtk );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
-        printf( "Verification failed.\n" );
+        printf( "Verification failed for gate with %d inputs.\n", nVars );
     Kit_DsdManFree( p );
 }
 
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 3c2ba703..13fa4108 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -275,6 +275,8 @@ struct If_Man_t_
     void *             pUserMan;
     Vec_Int_t *        vDump;
     int                pDumpIns[16];
+    Vec_Str_t *        vMarks;
+    Vec_Int_t *        vVisited2;
 
     // timing manager
     Tim_Man_t *        pManTim;
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index 0c9287a1..c03061af 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -106,6 +106,8 @@ int If_ManPerformMappingComb( If_Man_t * p )
     If_Obj_t * pObj;
     abctime clkTotal = Abc_Clock();
     int i;
+    //p->vVisited2 = Vec_IntAlloc( 100 );
+    //p->vMarks = Vec_StrStart( If_ManObjNum(p) );
 
     // set arrival times and fanout estimates
     If_ManForEachCi( p, pObj, i )
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 2d6889c0..079781e0 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -1494,6 +1494,68 @@ int If_CutCountTotalFanins( If_Man_t * p )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutFilter2_rec( If_Man_t * p, If_Obj_t * pObj, int LevelMin )
+{
+    char * pVisited = Vec_StrEntryP(p->vMarks, pObj->Id);
+    if ( *pVisited )
+        return *pVisited;
+    Vec_IntPush( p->vVisited2, pObj->Id );
+    if ( (int)pObj->Level <= LevelMin )
+        return (*pVisited = 1);
+    if ( If_CutFilter2_rec( p, pObj->pFanin0, LevelMin ) == 1 )
+        return (*pVisited = 1);
+    if ( If_CutFilter2_rec( p, pObj->pFanin1, LevelMin ) == 1 )
+        return (*pVisited = 1);
+    return (*pVisited = 2);
+}
+int If_CutFilter2( If_Man_t * p, If_Obj_t * pNode, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf, * pTemp;  int i, Count = 0; 
+//    printf( "Considering node %d and cut {", pNode->Id );
+//    If_CutForEachLeaf( p, pCut, pLeaf, i )
+//        printf( " %d", pLeaf->Id );
+//    printf( " }\n" );
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        int k, iObj, RetValue, nLevelMin = ABC_INFINITY;
+        Vec_IntClear( p->vVisited2 );
+        If_CutForEachLeaf( p, pCut, pTemp, k )
+        {
+            if ( pTemp == pLeaf )
+                continue;
+            nLevelMin = Abc_MinInt( nLevelMin, (int)pTemp->Level );
+            assert( Vec_StrEntry(p->vMarks, pTemp->Id) == 0 );
+            Vec_StrWriteEntry( p->vMarks, pTemp->Id, 2 );
+            Vec_IntPush( p->vVisited2, pTemp->Id );
+        }
+        RetValue = If_CutFilter2_rec( p, pLeaf, nLevelMin );
+        Vec_IntForEachEntry( p->vVisited2, iObj, k )
+            Vec_StrWriteEntry( p->vMarks, iObj, 0 );
+        if ( RetValue == 2 )
+        {
+            Count++;
+            pCut->nLeaves--;
+            for ( k = i; k < (int)pCut->nLeaves; k++ )
+                pCut->pLeaves[k] = pCut->pLeaves[k+1];
+            i--;
+        }
+    }
+    //if ( Count )
+    //    printf( "%d", Count );
+    return 0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 4027b780..6ecd0eb8 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -273,6 +273,8 @@ void If_ManStop( If_Man_t * p )
     Vec_IntFreeP( &p->vPairRes );
     Vec_StrFreeP( &p->vPairPerms );
     Vec_PtrFreeP( &p->vVisited );
+    Vec_StrFreeP( &p->vMarks );
+    Vec_IntFreeP( &p->vVisited2 );
     if ( p->vPairHash )
         Hash_IntManStop( p->vPairHash );
     for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c
index c7180e1c..06e880c2 100644
--- a/src/map/mio/mioUtils.c
+++ b/src/map/mio/mioUtils.c
@@ -224,6 +224,7 @@ void Mio_WritePin( FILE * pFile, Mio_Pin_t * pPin, int NameLen, int fAllPins )
 ***********************************************************************/
 void Mio_WriteGate( FILE * pFile, Mio_Gate_t * pGate, int GateLen, int NameLen, int FormLen, int fPrintSops, int fAllPins )
 {
+    //Vec_Int_t * vCover = Vec_IntAlloc( 1 << 10 );  int nLits;
     char Buffer[5000];
     Mio_Pin_t * pPin;
     assert( NameLen+FormLen+2 < 5000 );
@@ -239,7 +240,11 @@ void Mio_WriteGate( FILE * pFile, Mio_Gate_t * pGate, int GateLen, int NameLen,
     else // different pins
         Mio_GateForEachPin( pGate, pPin )
             Mio_WritePin( pFile, pPin, NameLen, 0 );
+    //nLits = 2*Kit_TruthLitNum((unsigned*)&pGate->uTruth, Mio_GateReadPinNum(pGate), vCover);
+    //if ( nLits != Mio_GateReadArea(pGate) )
+    //    printf( " # %d ", nLits );
     fprintf( pFile, "\n" );
+    //Vec_IntFree( vCover );
 }
 
 /**Function*************************************************************
diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c
index 71e0b7b3..963ea15b 100644
--- a/src/proof/acec/acecXor.c
+++ b/src/proof/acec/acecXor.c
@@ -21,6 +21,7 @@
 #include "acecInt.h"
 #include "misc/vec/vecWec.h"
 #include "misc/extra/extra.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -425,6 +426,48 @@ Acec_Box_t * Acec_ProduceBox( Gia_Man_t * p, int fVerbose )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManTestXor( Gia_Man_t * p )
+{
+    Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
+    Vec_Wrd_t * vSims   = Gia_ManSimPatSimOut( p, vSimsPi, 1 );
+    int n, i, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p);
+    Gia_Obj_t * pObj; Vec_Wrd_t * vSims2;
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        Gia_Obj_t Obj = *pObj;
+        for ( n = 0; n < 2; n++ )
+        {
+            if ( n ) 
+            {
+                pObj->iDiff1 = pObj->iDiff0;
+                pObj->fCompl1 = pObj->fCompl0;
+            }
+            else
+            {
+                pObj->iDiff0 = pObj->iDiff1;
+                pObj->fCompl0 = pObj->fCompl1;
+            }
+            vSims2 = Gia_ManSimPatSimOut( p, vSimsPi, 1 );
+            printf( "%2d %2d : %5d\n", i, n, Abc_TtCountOnesVecXor(Vec_WrdArray(vSims), Vec_WrdArray(vSims2), Vec_WrdSize(vSims2)) );
+            Vec_WrdFree( vSims2 );
+            *pObj = Obj;
+        }
+    }
+    Vec_WrdFree( vSimsPi );
+    Vec_WrdFree( vSims );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////