Various changes.

abclib.dsp

@@ -4915,6 +4915,10 @@ SOURCE=.\src\aig\gia\giaCut.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaDecs.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaDeep.c
 # End Source File
 # Begin Source File
@@ -5211,6 +5215,10 @@ SOURCE=.\src\aig\gia\giaSupp.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaSupps.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaSweep.c
 # End Source File
 # Begin Source File

src/aig/gia/gia.h

@@ -216,6 +216,7 @@ struct Gia_Man_t_
     Vec_Wrd_t *    vSimsPo;
     Vec_Int_t *    vClassOld;
     Vec_Int_t *    vClassNew;
+    Vec_Int_t *    vPats;
     // incremental simulation
     int            fIncrSim;
     int            iNextPi;
@@ -1275,6 +1276,11 @@ extern void                Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
 extern Gia_Man_t *         Gia_ManDupCof( Gia_Man_t * p, int iVar );
 extern Gia_Man_t *         Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose );
 extern Gia_Man_t *         Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose );
+/*=== giaDecs.c ============================================================*/
+extern int                 Gia_ResubVarNum( Vec_Int_t * vResub );
+extern word                Gia_ResubToTruth6( Vec_Int_t * vResub );
+extern int                 Gia_ManEvalSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int fVerbose );
+extern Vec_Int_t *         Gia_ManDeriveSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int Type );
 /*=== giaDfs.c ============================================================*/
 extern void                Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp );
 extern void                Gia_ManCollectAnds_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes );

src/aig/gia/giaMan.c

@@ -94,6 +94,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vStore );
     Vec_IntFreeP( &p->vClassNew );
     Vec_IntFreeP( &p->vClassOld );
+    Vec_IntFreeP( &p->vPats );
     Vec_WrdFreeP( &p->vSims );
     Vec_WrdFreeP( &p->vSimsT );
     Vec_WrdFreeP( &p->vSimsPi );

src/aig/gia/giaResub.c

@@ -651,6 +651,37 @@ Gia_Man_t * Gia_ManConstructFromGates2( Vec_Wec_t * vFuncs, Vec_Wec_t * vDivs, i
         Vec_IntFree( vSupp );
     return pNew;
 }
+Vec_Int_t * Gia_ManToGates( Gia_Man_t * p )
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 2*Gia_ManAndNum(p) + 1 );
+    Gia_Obj_t * pRoot = Gia_ManCo( p, 0 );
+    int iRoot = Gia_ObjFaninId0p(p, pRoot) - 1;
+    int nVars = Gia_ManCiNum(p);
+    assert( Gia_ManCoNum(p) == 1 );
+    if ( iRoot == -1 )
+        Vec_IntPush( vRes, Gia_ObjFaninC0(pRoot) );
+    else if ( iRoot < nVars )
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Gia_ObjFaninC0(pRoot)) );
+    else
+    {
+        Gia_Obj_t * pObj, * pLast = NULL; int i;
+        Gia_ManForEachCi( p, pObj, i )
+            assert( Gia_ObjId(p, pObj) == i+1 );
+        Gia_ManForEachAnd( p, pObj, i )
+        {
+            int iLit0 = Abc_Var2Lit( Gia_ObjFaninId0(pObj, i) - 1, Gia_ObjFaninC0(pObj) );
+            int iLit1 = Abc_Var2Lit( Gia_ObjFaninId1(pObj, i) - 1, Gia_ObjFaninC1(pObj) );
+            if ( iLit0 > iLit1 )
+                iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
+            Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 );
+            pLast = pObj;
+        }
+        assert( pLast == Gia_ObjFanin0(pRoot) );
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Gia_ObjFaninC0(pRoot)) );
+    }
+    assert( Vec_IntSize(vRes) == 2*Gia_ManAndNum(p) + 1 );
+    return vRes;
+}
 
 /**Function*************************************************************
 
@@ -1378,7 +1409,10 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit, int Depth )
             if ( iResLit >= 0 ) 
             {
                 int iNode = nVars + Vec_IntSize(p->vGates)/2;
+                if ( iDiv < iResLit )
                     Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) );
+                else
+                    Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_LitNot(iDiv) );
                 return Abc_Var2Lit( iNode, fUseOr );
             }
         }

src/aig/gia/module.make

@@ -16,6 +16,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaCSat2.c \
     src/aig/gia/giaCTas.c \
     src/aig/gia/giaCut.c \
+    src/aig/gia/giaDecs.c \
     src/aig/gia/giaDeep.c \
     src/aig/gia/giaDfs.c \
     src/aig/gia/giaDup.c \
@@ -89,6 +90,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaStr.c \
     src/aig/gia/giaSupMin.c \
     src/aig/gia/giaSupp.c \
+    src/aig/gia/giaSupps.c \
     src/aig/gia/giaSweep.c \
     src/aig/gia/giaSweeper.c \
     src/aig/gia/giaSwitch.c \

src/bool/bdc/bdc.h

@@ -79,6 +79,8 @@ extern void *      Bdc_FuncCopy( Bdc_Fun_t * p );
 extern int         Bdc_FuncCopyInt( Bdc_Fun_t * p );
 extern void        Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy );
 extern void        Bdc_FuncSetCopyInt( Bdc_Fun_t * p, int iCopy );
+extern int         Bdc_ManBidecNodeNum( word * pFunc, word * pCare, int nVars, int fVerbose );
+extern Vec_Int_t * Bdc_ManBidecResub( word * pFunc, word * pCare, int nVars );
 
 /*=== working with saved copies ==========================================*/
 static inline int  Bdc_FunObjCopy( Bdc_Fun_t * pObj )     { return Abc_LitNotCond( Bdc_FuncCopyInt(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }

src/bool/bdc/bdcCore.c

@@ -364,6 +364,85 @@ void Bdc_ManDecomposeTest( unsigned uTruth, int nVars )
     Bdc_ManFree( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_ManBidecNodeNum( word * pFunc, word * pCare, int nVars, int fVerbose )
+{
+    int nNodes, nTtWords = Abc_Truth6WordNum(nVars);
+    Bdc_Man_t * pManDec;
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    pPars->nVarsMax = nVars;
+    pManDec = Bdc_ManAlloc( pPars );
+    Bdc_ManDecompose( pManDec, (unsigned *)pFunc, (unsigned *)pCare, nVars, NULL, 1000 );
+    nNodes = Bdc_ManAndNum( pManDec );
+    if ( fVerbose )
+        Bdc_ManDecPrint( pManDec );
+    Bdc_ManFree( pManDec );
+    return nNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManBidecResubInt( Bdc_Man_t * p, Vec_Int_t * vRes )
+{
+    int i, iRoot = Bdc_FunId(p,Bdc_Regular(p->pRoot)) - 1;
+    if ( iRoot == -1 )
+        Vec_IntPush( vRes, !Bdc_IsComplement(p->pRoot) );
+    else if ( iRoot < p->nVars )
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Bdc_IsComplement(p->pRoot)) );
+    else
+    {
+        for ( i = p->nVars+1; i < p->nNodes; i++ )
+        {
+            Bdc_Fun_t * pNode = p->pNodes + i;
+            int iLit0 = Abc_Var2Lit( Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) - 1, Bdc_IsComplement(pNode->pFan0) );
+            int iLit1 = Abc_Var2Lit( Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) - 1, Bdc_IsComplement(pNode->pFan1) );
+            if ( iLit0 > iLit1 )
+                iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
+            Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 );
+        }
+        assert( 2 + iRoot == p->nNodes );
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Bdc_IsComplement(p->pRoot)) );
+    }
+}
+Vec_Int_t * Bdc_ManBidecResub( word * pFunc, word * pCare, int nVars )
+{
+    Vec_Int_t * vRes = NULL;
+    int nNodes, nTtWords = Abc_Truth6WordNum(nVars);
+    Bdc_Man_t * pManDec; 
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    pPars->nVarsMax = nVars;
+    pManDec = Bdc_ManAlloc( pPars );
+    Bdc_ManDecompose( pManDec, (unsigned *)pFunc, (unsigned *)pCare, nVars, NULL, 1000 );
+    if ( pManDec->pRoot != NULL )
+    {
+        //Bdc_ManDecPrint( pManDec );
+        nNodes = Bdc_ManAndNum( pManDec );
+        vRes = Vec_IntAlloc( 2*nNodes + 1 );
+        Bdc_ManBidecResubInt( pManDec, vRes );
+        assert( Vec_IntSize(vRes) == 2*nNodes + 1 );
+    }
+    Bdc_ManFree( pManDec );
+    return vRes;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/bool/kit/kit.h

@@ -574,6 +574,8 @@ extern int             Kit_TruthLitNum( unsigned * pTruth, int nVars, Vec_Int_t
 //extern Hop_Obj_t *     Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
 //extern Hop_Obj_t *     Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
 //extern Hop_Obj_t *     Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory );
+extern int             Kit_IsopNodeNum( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory );
+extern Vec_Int_t *     Kit_IsopResub( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory );
 /*=== kitIsop.c ==========================================================*/
 extern int             Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
 extern int             Kit_TruthIsop2( unsigned * puTruth0, unsigned * puTruth1, int nVars, Vec_Int_t * vMemory, int fTryBoth, int fReturnTt );

src/bool/kit/kitHop.c

@@ -136,6 +136,107 @@ int Kit_TruthToGia2( Gia_Man_t * pMan, unsigned * pTruth0, unsigned * pTruth1, i
   SeeAlso     []
 
 ***********************************************************************/
+int Kit_IsopNodeNum( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory )
+{
+    Kit_Graph_t * pGraph;
+    int nNodes;
+    // transform truth table into the decomposition tree
+    if ( vMemory == NULL )
+    {
+        vMemory = Vec_IntAlloc( 0 );
+        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
+        Vec_IntFree( vMemory );
+    }
+    else
+        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
+    if ( pGraph == NULL )
+    {
+        printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" );
+        Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" );
+        Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" );
+    }
+    // derive the AIG for the decomposition tree
+    nNodes = Kit_GraphNodeNum( pGraph );
+    Kit_GraphFree( pGraph );
+    return nNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_IsopResubInt( Kit_Graph_t * pGraph, Vec_Int_t * vRes )
+{
+    int nVars = Kit_GraphLeaveNum(pGraph);
+    assert( nVars >= 0 && nVars <= pGraph->nSize );
+    if ( Kit_GraphIsConst(pGraph) )
+        Vec_IntPush( vRes, Kit_GraphIsConst1(pGraph) );
+    else if ( Kit_GraphIsVar(pGraph) )
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(Kit_GraphVarInt(pGraph), Kit_GraphIsComplement(pGraph)) );
+    else
+    {
+        Kit_Node_t * pNode; int i;
+        Kit_GraphForEachNode( pGraph, pNode, i )
+        {
+            Kit_Node_t * pFan0 = Kit_GraphNodeFanin0( pGraph, pNode );
+            Kit_Node_t * pFan1 = Kit_GraphNodeFanin1( pGraph, pNode );
+            int iLit0 = Abc_Var2Lit( Kit_GraphNodeInt(pGraph, pFan0), pNode->eEdge0.fCompl );
+            int iLit1 = Abc_Var2Lit( Kit_GraphNodeInt(pGraph, pFan1), pNode->eEdge1.fCompl );
+            if ( iLit0 > iLit1 )
+                iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
+            Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 );
+        }
+        assert( pNode == Kit_GraphNode(pGraph, pGraph->eRoot.Node) );
+        Vec_IntPush( vRes, 4 + Abc_Var2Lit(Kit_GraphNodeInt(pGraph, pNode), Kit_GraphIsComplement(pGraph)) );
+    }
+}
+Vec_Int_t * Kit_IsopResub( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory )
+{
+    Vec_Int_t * vRes = NULL;
+    Kit_Graph_t * pGraph;
+    int nNodes;
+    // transform truth table into the decomposition tree
+    if ( vMemory == NULL )
+    {
+        vMemory = Vec_IntAlloc( 0 );
+        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
+        Vec_IntFree( vMemory );
+    }
+    else
+        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
+    if ( pGraph == NULL )
+    {
+        printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" );
+        Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" );
+        Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" );
+    }
+    // derive the AIG for the decomposition tree
+    nNodes = Kit_GraphNodeNum( pGraph );
+    vRes = Vec_IntAlloc( 2*nNodes + 1 );
+    Kit_IsopResubInt( pGraph, vRes );
+    assert( Vec_IntSize(vRes) == 2*nNodes + 1 );
+    Kit_GraphFree( pGraph );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Hop_Obj_t * Kit_GraphToHopInternal( Hop_Man_t * pMan, Kit_Graph_t * pGraph )
 {
     Kit_Node_t * pNode = NULL;

src/misc/util/utilTruth.h

@@ -356,6 +356,12 @@ static inline void Abc_TtOrAnd( word * pOut, word * pIn1, word * pIn2, int nWord
     for ( w = 0; w < nWords; w++ )
         pOut[w] |= pIn1[w] & pIn2[w];
 }
+static inline void Abc_TtSharpOr( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = (pOut[w] & ~pIn1[w]) | pIn2[w];
+}
 static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
 {
     int w;
@@ -2104,6 +2110,7 @@ static inline int Abc_TtCountOnesVec( word * x, int nWords )
 {
     int w, Count = 0;
     for ( w = 0; w < nWords; w++ )
+        if ( x[w] )
             Count += Abc_TtCountOnes( x[w] );
     return Count;
 }
@@ -2111,11 +2118,17 @@ static inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, in
 {
     int w, Count = 0;
     if ( fCompl )
+    {
         for ( w = 0; w < nWords; w++ )
+            if ( pMask[w] & ~x[w] )
                 Count += Abc_TtCountOnes( pMask[w] & ~x[w] );
+    }
     else
+    {
         for ( w = 0; w < nWords; w++ )
+            if ( pMask[w] & x[w] )
                 Count += Abc_TtCountOnes( pMask[w] & x[w] );
+    }
     return Count;
 }
 static inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int fComp1, word * pMask, int nWords )
@@ -2139,6 +2152,7 @@ static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords )
 {
     int w, Count = 0;
     for ( w = 0; w < nWords; w++ )
+        if ( x[w] ^ y[w] )
             Count += Abc_TtCountOnes( x[w] ^ y[w] );
     return Count;
 }
@@ -2163,6 +2177,16 @@ static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nW
     }
     return Count;
 }
+static inline void Abc_TtIsfPrint( word * pOff, word * pOn, int nWords )
+{
+    int nTotal  = 64*nWords;
+    int nOffset = Abc_TtCountOnesVec(pOff, nWords);
+    int nOnset  = Abc_TtCountOnesVec(pOn, nWords);
+    int nDcset  = nTotal - nOffset - nOnset;
+    printf( "OFF =%6d (%6.2f %%)  ", nOffset, 100.0*nOffset/nTotal );
+    printf( "ON =%6d (%6.2f %%)  ",  nOnset,  100.0*nOnset/nTotal );
+    printf( "DC =%6d (%6.2f %%)",    nDcset,  100.0*nDcset/nTotal );
+}
 
 /**Function*************************************************************
 
@@ -2263,6 +2287,22 @@ static inline int Abc_TtFindLastDiffBit2( word * pIn1, word * pIn2, int nWords )
             return 64*w + Abc_Tt6LastBit(pIn1[w] ^ pIn2[w]);
     return -1;
 }
+static inline int Abc_TtFindFirstAndBit2( word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        if ( pIn1[w] & pIn2[w] )
+            return 64*w + Abc_Tt6FirstBit(pIn1[w] & pIn2[w]);
+    return -1;
+}
+static inline int Abc_TtFindLastAndBit2( word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = nWords - 1; w >= 0; w-- )
+        if ( pIn1[w] & pIn2[w] )
+            return 64*w + Abc_Tt6LastBit(pIn1[w] & pIn2[w]);
+    return -1;
+}
 static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
 {
     int w, nWords = Abc_TtWordNum(nVars);

src/misc/vec/vecHsh.h

@@ -492,6 +492,10 @@ static inline int Hsh_VecSize( Hsh_VecMan_t * p )
 {
     return Vec_IntSize(p->vMap);
 }
+static inline double Hsh_VecManMemory( Hsh_VecMan_t * p )
+{
+    return !p ? 0.0 : Vec_IntMemory(p->vTable) + Vec_IntMemory(p->vData) + Vec_IntMemory(p->vMap);
+}
 
 /**Function*************************************************************
 

src/misc/vec/vecInt.h

@@ -1154,6 +1154,17 @@ static inline int Vec_IntFindMax( Vec_Int_t * p )
             Best = p->pArray[i];
     return Best;
 }
+static inline int Vec_IntArgMax( Vec_Int_t * p )
+{
+    int i, Best, Arg = 0;
+    if ( p->nSize == 0 )
+        return -1;
+    Best = p->pArray[0];
+    for ( i = 1; i < p->nSize; i++ )
+        if ( Best < p->pArray[i] )
+            Best = p->pArray[i], Arg = i;
+    return Arg;
+}
 
 /**Function*************************************************************
 
@@ -1177,6 +1188,17 @@ static inline int Vec_IntFindMin( Vec_Int_t * p )
             Best = p->pArray[i];
     return Best;
 }
+static inline int Vec_IntArgMin( Vec_Int_t * p )
+{
+    int i, Best, Arg = 0;
+    if ( p->nSize == 0 )
+        return 0;
+    Best = p->pArray[0];
+    for ( i = 1; i < p->nSize; i++ )
+        if ( Best > p->pArray[i] )
+            Best = p->pArray[i], Arg = i;
+    return Arg;
+}
 
 /**Function*************************************************************
 
@@ -2149,6 +2171,13 @@ static inline int Vec_IntCompareVec( Vec_Int_t * p1, Vec_Int_t * p2 )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Vec_IntClearAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
+{
+    int Entry, i;
+    Vec_IntClear( vVec1 );
+    Vec_IntForEachEntry( vVec2, Entry, i )
+        Vec_IntPush( vVec1, Entry );
+}
 static inline void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
 {
     int Entry, i;
@@ -2192,6 +2221,67 @@ static inline void Vec_IntRemapArray( Vec_Int_t * vOld2New, Vec_Int_t * vOld, Ve
             Vec_IntWriteEntry( vNew, iNew, Vec_IntEntry(vOld, iOld) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [File interface.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntDumpBin( char * pFileName, Vec_Int_t * p, int fVerbose )
+{
+    int RetValue;
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    RetValue = fwrite( Vec_IntArray(p), 1, sizeof(int)*Vec_IntSize(p), pFile );
+    fclose( pFile );
+    if ( RetValue != (int)sizeof(int)*Vec_IntSize(p) )
+        printf( "Error reading data from file.\n" );
+    if ( fVerbose )
+        printf( "Written %d integers into file \"%s\".\n", Vec_IntSize(p), pFileName );
+}
+static inline Vec_Int_t * Vec_IntReadBin( char * pFileName, int fVerbose )
+{
+    Vec_Int_t * p = NULL; int nSize, RetValue;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    fseek( pFile, 0, SEEK_END );
+    nSize = ftell( pFile );
+    if ( nSize == 0 )
+    {
+        printf( "The input file is empty.\n" );
+        fclose( pFile );
+        return NULL;
+    }
+    if ( nSize % sizeof(int) > 0 )
+    {
+        printf( "Cannot read file with integers because it is not aligned at 4 bytes (remainder = %d).\n", nSize % sizeof(int) );
+        fclose( pFile );
+        return NULL;
+    }
+    rewind( pFile );
+    p = Vec_IntStart( nSize/sizeof(int) );
+    RetValue = fread( Vec_IntArray(p), 1, nSize, pFile );
+    fclose( pFile );
+    if ( RetValue != nSize )
+        printf( "Error reading data from file.\n" );
+    if ( fVerbose )
+        printf( "Read %d integers from file \"%s\".\n", nSize/sizeof(int), pFileName );
+    return p;
+}
+
 ABC_NAMESPACE_HEADER_END
 
 #endif

src/misc/vec/vecQue.h

@@ -119,6 +119,10 @@ static inline void Vec_QueClear( Vec_Que_t * p )
     }
     p->nSize = 1;
 }
+static inline double Vec_QueMemory( Vec_Que_t * p )
+{
+    return !p ? 0.0 : 2.0 * sizeof(int) * (size_t)p->nCap + sizeof(Vec_Que_t) ;
+}
 
 /**Function*************************************************************
 

src/misc/vec/vecWrd.h

@@ -903,6 +903,14 @@ static inline void Vec_WrdInsert( Vec_Wrd_t * p, int iHere, word Entry )
         p->pArray[i] = p->pArray[i-1];
     p->pArray[i] = Entry;
 }
+static inline void Vec_WrdDrop( Vec_Wrd_t * p, int i )
+{
+    int k;
+    assert( i >= 0 && i < Vec_WrdSize(p) );
+    p->nSize--;
+    for ( k = i; k < p->nSize; k++ )
+        p->pArray[k] = p->pArray[k+1];
+}
 
 /**Function*************************************************************
 

src/proof/cec/cecSatG2.c

@@ -98,11 +98,13 @@ struct Cec4_Man_t_
     Vec_Int_t *      vCands;
     Vec_Int_t *      vVisit;
     Vec_Int_t *      vPat;
+    Vec_Int_t *      vPats;
     Vec_Int_t *      vDisprPairs;
     Vec_Bit_t *      vFails;
     int              iPosRead;       // candidate reading position
     int              iPosWrite;      // candidate writing position
     int              iLastConst;     // last const node proved
+    int              nPatsAll;
     // refinement
     Vec_Int_t *      vRefClasses;
     Vec_Int_t *      vRefNodes;
@@ -147,6 +149,63 @@ static inline void   Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Cec4_EvalCombine( Vec_Int_t * vPats, int nPats, int nInputs, int nWords )
+{
+    //Vec_Wrd_t * vSimsPi = Vec_WrdStart( nInputs * nWords );
+    Vec_Wrd_t * vSimsPi = Vec_WrdStartRandom( nInputs * nWords );
+    int i, k, iPat = 0; 
+    for ( i = 0; i < Vec_IntSize(vPats); )
+    {
+        int Size = Vec_IntEntry(vPats, i);
+        assert( Size > 0 );
+        for ( k = 1; k <= Size; k++ )
+        {
+            int iLit = Vec_IntEntry( vPats, i+k );
+            word * pSim;
+            if ( iLit == 0 )
+                continue;
+            assert( Abc_Lit2Var(iLit) > 0 && Abc_Lit2Var(iLit) <= nInputs );
+            pSim = Vec_WrdEntryP( vSimsPi, (Abc_Lit2Var(iLit)-1)*nWords );
+            if ( Abc_InfoHasBit( (unsigned*)pSim, iPat ) != Abc_LitIsCompl(iLit) )
+                Abc_InfoXorBit( (unsigned*)pSim, iPat );
+        }
+        iPat++;
+        i += Size + 1;
+    }
+    assert( iPat == nPats );
+    return vSimsPi;
+}
+void Cec4_EvalPatterns( Gia_Man_t * p, Vec_Int_t * vPats, int nPats )
+{
+    int nWords = Abc_Bit6WordNum(nPats);
+    Vec_Wrd_t * vSimsPi = Cec4_EvalCombine( vPats, nPats, Gia_ManCiNum(p), nWords );
+    Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( p, vSimsPi, 1 );
+    int i, Count = 0, nErrors = 0;
+    for ( i = 0; i < Gia_ManCoNum(p); i++ )
+    {
+        int CountThis = Abc_TtCountOnesVec( Vec_WrdEntryP(vSimsPo, i*nWords), nWords );
+        if ( CountThis == 0 )
+            continue;
+        printf( "%d ", CountThis );
+        nErrors += CountThis;
+        Count++;
+    }
+    printf( "\nDetected %d error POs with %d errors (average %.2f).\n", Count, nErrors, 1.0*nErrors/Abc_MaxInt(1, Count) );
+    Vec_WrdFree( vSimsPi );
+    Vec_WrdFree( vSimsPo );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Default parameter settings.]
 
   Description []
@@ -198,6 +257,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     p->vCands        = Vec_IntAlloc( 100 );
     p->vVisit        = Vec_IntAlloc( 100 );
     p->vPat          = Vec_IntAlloc( 100 );
+    p->vPats         = Vec_IntAlloc( 10000 );
     p->vDisprPairs   = Vec_IntAlloc( 100 );
     p->vFails        = Vec_BitStart( Gia_ManObjNum(pAig) );
     //pAig->pData     = p->pSat; // point AIG manager to the solver
@@ -226,6 +286,12 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
         ABC_PRTP( "TOTAL        ", timeTotal,        timeTotal );
         fflush( stdout );
     }
+    //printf( "Recorded %d patterns with %d literals (average %.2f).\n", 
+    //    p->nPatsAll, Vec_IntSize(p->vPats) - p->nPatsAll, 1.0*Vec_IntSize(p->vPats)/Abc_MaxInt(1, p->nPatsAll)-1 );
+    //Cec4_EvalPatterns( p->pAig, p->vPats, p->nPatsAll );
+    //Vec_IntFreeP( &p->vPats );
+    Vec_IntFreeP( &p->pAig->vPats );
+    p->pAig->vPats = p->vPats;
     Vec_WrdFreeP( &p->pAig->vSims );
     Vec_WrdFreeP( &p->pAig->vSimsPi );
     Gia_ManCleanMark01( p->pAig );
@@ -1392,6 +1458,9 @@ int Cec4_ManGeneratePatterns( Cec4_Man_t * p )
             if ( Res )
             {
                 int Ret = Cec4_ManPackAddPattern( p->pAig, p->vPat, 1 );
+                Vec_IntPush( p->vPats, Vec_IntSize(p->vPat) );
+                Vec_IntAppend( p->vPats, p->vPat );
+                p->nPatsAll++;
                 //Vec_IntPushTwo( p->vDisprPairs, iRepr, iCand );
                 Packs += Ret;
                 if ( Ret == 64 * p->pAig->nSimWords )
@@ -1566,6 +1635,9 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
         p->pAig->iPatsPi++;
         Vec_IntForEachEntry( p->vPat, iLit, i )
             Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
+        Vec_IntPush( p->vPats, Vec_IntSize(p->vPat) );
+        Vec_IntAppend( p->vPats, p->vPat );
+        p->nPatsAll++;
         //Cec4_ManPackAddPattern( p->pAig, p->vPat, 0 );
         //assert( iPatsOld + 1 == p->pAig->iPatsPi );
         if ( fEasy )