Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network.

7 files changed, 214 insertions, 19 deletions

diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index adbdafca..e4b764a1 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -44,6 +44,7 @@ struct Pdr_Par_t_
     int nRecycle;         // limit on vars for recycling
     int nFrameMax;        // limit on frame count
     int nConfLimit;       // limit on SAT solver conflicts
+    int nConfGenLimit;    // limit on SAT solver conflicts during generalization
     int nRestLimit;       // limit on the number of proof-obligations
     int nTimeOut;         // timeout in seconds
     int nTimeOutGap;      // approximate timeout in seconds since the last change
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 78cc16c1..8e81795b 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -55,6 +55,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->nTimeOut       =       0;  // timeout in seconds
     pPars->nTimeOutGap    =       0;  // timeout in seconds since the last solved
     pPars->nConfLimit     =       0;  // limit on SAT solver conflicts
+    pPars->nConfGenLimit  =       0;  // limit on SAT solver conflicts during generalization
     pPars->nRestLimit     =       0;  // limit on the number of proof-obligations
     pPars->fTwoRounds     =       0;  // use two rounds for generalization
     pPars->fMonoCnf       =       0;  // monolythic CNF
@@ -115,7 +116,7 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
     // make sure the cube works
     {
     int RetValue;
-    RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
+    RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0 );
     assert( RetValue );
     }
 */
@@ -162,7 +163,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
             }
 
             // check if the clause can be moved to the next frame
-            RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 );
+            RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0 );
             if ( RetValue2 == -1 )
                 return -1;
             if ( !RetValue2 )
@@ -310,7 +311,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
     int * pOrder;
     // if there is no induction, return
     *ppCubeMin = NULL;
-    RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit );
+    RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0 );
     if ( RetValue == -1 )
         return -1;
     if ( RetValue == 0 )
@@ -343,7 +344,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
                 continue;
             // try removing this literal
             Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
-            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 );
             if ( RetValue == -1 )
             {
                 Pdr_SetDeref( pCubeMin );
@@ -381,7 +382,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
                 continue;
             // try removing this literal
             Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
-            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0 );
             if ( RetValue == -1 )
             {
                 Pdr_SetDeref( pCubeMin );
@@ -494,7 +495,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
             assert( pPred == NULL );
             for ( k = pThis->iFrame; k < kMax; k++ )
             {
-                RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
+                RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0 );
                 if ( RetValue == -1 )
                 {
                     Pdr_OblDeref( pThis );
@@ -659,7 +660,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     p->pPars->iFrame = k;
                     return -1;
                 }
-                RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
+                RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit, 0 );
                 if ( RetValue == 1 )
                     break;
                 if ( RetValue == -1 )
@@ -911,10 +912,6 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
     RetValue = Pdr_ManSolveInt( p );
     if ( RetValue == 0 )
         assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
-    if ( RetValue == 1 )
-        Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) );
-    else
-        Abc_FrameSetInv( NULL );
     if ( p->vCexes )
     {
         assert( p->pAig->vSeqModelVec == NULL );
@@ -922,7 +919,12 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
         p->vCexes = NULL;
     }
     if ( p->pPars->fDumpInv )
+    {
+        Abc_FrameSetCnf( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
+        Abc_FrameSetStr( Pdr_ManDumpString(p) );
+        Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) );
         Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
+    }
     p->tTotal += Abc_Clock() - clk;
     Pdr_ManStop( p );
     pPars->iFrame--;
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index bd9fe87c..6a08a150 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -101,6 +101,7 @@ struct Pdr_Man_t_
     Vec_Int_t * vSuppLits; // support literals
     Pdr_Set_t * pCubeJust; // justification
     abctime *   pTime4Outs;// timeout per output
+    Vec_Ptr_t * vInfCubes; // infinity clauses/cubes
     // statistics
     int         nBlocks;   // the number of times blockState was called
     int         nObligs;   // the number of proof obligations derived
@@ -167,8 +168,10 @@ extern Vec_Int_t *     Pdr_ManCountFlopsInv( Pdr_Man_t * p );
 extern void            Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time );
 extern void            Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
 extern void            Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved );
+extern Vec_Str_t *     Pdr_ManDumpString( Pdr_Man_t * p );
 extern void            Pdr_ManReportInvariant( Pdr_Man_t * p );
 extern void            Pdr_ManVerifyInvariant( Pdr_Man_t * p );
+extern Vec_Int_t *     Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce );
 /*=== pdrMan.c ==========================================================*/
 extern Pdr_Man_t *     Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
 extern void            Pdr_ManStop( Pdr_Man_t * p );
@@ -182,7 +185,7 @@ extern Vec_Int_t *     Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, in
 extern void            Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
 extern void            Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues );
 extern int             Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
-extern int             Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit );
+extern int             Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf );
 /*=== pdrTsim.c ==========================================================*/
 extern Pdr_Set_t *     Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
 /*=== pdrUtil.c ==========================================================*/
@@ -197,6 +200,7 @@ extern int             Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
 extern int             Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
 extern int             Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
 extern void            Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
+extern void            Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
 extern int             Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
 extern Pdr_Obl_t *     Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
 extern Pdr_Obl_t *     Pdr_OblRef( Pdr_Obl_t * p );
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 860462c3..b548cf68 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -110,11 +110,15 @@ Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
     int i, n;
     vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 )
+            continue;
         for ( n = 0; n < pCube->nLits; n++ )
         {
             assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) );
             Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 );
         }
+    }
     return vFlopCount;
 }
 
@@ -202,7 +206,10 @@ int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart )
     Vec_Int_t * vFlopCounts;
     Vec_Ptr_t * vCubes;
     int i, Entry, Counter = 0;
-    vCubes = Pdr_ManCollectCubes( p, kStart );
+    if ( p->vInfCubes == NULL )
+        vCubes = Pdr_ManCollectCubes( p, kStart );
+    else
+        vCubes = Vec_PtrDup( p->vInfCubes );
     vFlopCounts = Pdr_ManCountFlops( p, vCubes );
     Vec_IntForEachEntry( vFlopCounts, Entry, i )
         Counter += (Entry > 0);
@@ -338,7 +345,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     Vec_Ptr_t * vCubes;
     Pdr_Set_t * pCube;
     char ** pNamesCi;
-    int i, kStart;
+    int i, kStart, Count = 0;
     // create file
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
@@ -348,9 +355,20 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     } 
     // collect cubes
     kStart = Pdr_ManFindInvariantStart( p );
-    vCubes = Pdr_ManCollectCubes( p, kStart );
+    if ( fProved )
+        vCubes = Pdr_ManCollectCubes( p, kStart );
+    else
+        vCubes = Vec_PtrDup( p->vInfCubes );
     Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
 //    Pdr_ManDumpAig( p->pAig, vCubes );
+    // count cubes
+    Count = 0;
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 )
+            continue;
+        Count++;
+    }
     // collect variable appearances
     vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
     // output the header
@@ -361,7 +379,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
     fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
     fprintf( pFile, ".o 1\n" );
-    fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) );
+    fprintf( pFile, ".p %d\n", Count );
     // output flop names
     pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 );
     if ( pNamesCi )
@@ -377,6 +395,8 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     // output cubes
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
     {
+        if ( pCube->nRefs == -1 )
+            continue;
         Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );  
         fprintf( pFile, " 1\n" ); 
     }
@@ -390,6 +410,48 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
         Abc_Print( 1, "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
+{
+    int fUseSupp = 1;
+    Vec_Str_t * vStr;
+    Vec_Int_t * vFlopCounts;
+    Vec_Ptr_t * vCubes;
+    Pdr_Set_t * pCube;
+    int i, kStart;
+    vStr = Vec_StrAlloc( 1000 );
+    // collect cubes
+    kStart = Pdr_ManFindInvariantStart( p );
+    if ( p->vInfCubes == NULL )
+        vCubes = Pdr_ManCollectCubes( p, kStart );
+    else
+        vCubes = Vec_PtrDup( p->vInfCubes );
+    Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
+    // collect variable appearances
+    vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
+    // output cubes
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 )
+            continue;
+        Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );  
+    }
+    Vec_IntFreeP( &vFlopCounts );
+    Vec_PtrFree( vCubes );
+    Vec_StrPush( vStr, '\0' );
+    return vStr;
+}
+
 
 /**Function*************************************************************
 
@@ -469,6 +531,86 @@ void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
     Vec_PtrFree( vCubes );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
+{
+    sat_solver * pSat;
+    Vec_Int_t * vLits;
+    Pdr_Set_t * pCube;
+    int i, kThis, RetValue, fChanges = 0, Counter = 0;
+    // create solver with the cubes
+    kThis = Vec_PtrSize(p->vSolvers);
+    pSat  = Pdr_ManCreateSolver( p, kThis );
+    // add the clauses
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 ) // skip non-inductive
+            continue;
+        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
+        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+        assert( RetValue );
+        sat_solver_compress( pSat );
+    }
+    // check each clause
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 ) // skip non-inductive
+            continue;
+        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
+        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
+        if ( RetValue != l_False ) // mark as non-inductive
+        {
+            pCube->nRefs = -1;
+            fChanges = 1;
+        }
+        else
+            Counter++;
+    }
+    //printf( "Clauses = %d.\n", Counter );
+    //sat_solver_delete( pSat );
+    return fChanges;
+}
+Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
+{
+    Vec_Int_t * vResult;
+    Vec_Ptr_t * vCubes;
+    Pdr_Set_t * pCube;
+    int i, v, kStart;
+    abctime clk = Abc_Clock();
+    // collect cubes used in the inductive invariant
+    kStart = Pdr_ManFindInvariantStart( p );
+    vCubes = Pdr_ManCollectCubes( p, kStart );
+    // refine as long as there are changes
+    if ( fReduce )
+        while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) );
+    // collect remaining clauses
+    vResult = Vec_IntAlloc( 1000 );
+    Vec_IntPush( vResult, 0 );
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 ) // skip non-inductive
+            continue;
+        Vec_IntAddToEntry( vResult, 0, 1 );
+        Vec_IntPush( vResult, pCube->nLits );
+        for ( v = 0; v < pCube->nLits; v++ )
+            Vec_IntPush( vResult, pCube->Lits[v] );
+    }
+    //Vec_PtrFree( vCubes );
+    Vec_PtrFreeP( &p->vInfCubes );
+    p->vInfCubes = vCubes;
+    return vResult;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 9a73b697..b58c479b 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -163,6 +163,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
     Vec_IntFree( p->vCi2Rem   );  // CIs to be removed
     Vec_IntFree( p->vRes      );  // final result
     Vec_IntFree( p->vSuppLits );  // support literals
+    Vec_PtrFreeP( &p->vInfCubes );
     ABC_FREE( p->pCubeJust );
     ABC_FREE( p->pTime4Outs );
     if ( p->vCexes )
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index 244d0311..f3681adb 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -283,7 +283,7 @@ int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
   SeeAlso     []
 
 ***********************************************************************/
-int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit )
+int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf )
 { 
     int fUseLit = 1;
     int fLitUsed = 0;
@@ -329,10 +329,15 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
         // solve 
         clk = Abc_Clock();
         Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
-        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 );
+        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), fTryConf ? p->pPars->nConfGenLimit : nConfLimit, 0, 0, 0 );
         sat_solver_set_runtime_limit( pSat, Limit );
         if ( RetValue == l_Undef )
-            return -1;
+        {
+            if ( fTryConf && p->pPars->nConfGenLimit )
+                RetValue = l_True;
+            else
+                return -1;
+        }
 /*
         if ( RetValue == l_True )
         {
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 1536c1cc..53a8a54a 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -251,6 +251,46 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
+{
+    char * pBuff;
+    int i, k = 0, Entry;
+    pBuff = ABC_ALLOC( char, nRegs + 1 );
+    for ( i = 0; i < nRegs; i++ )
+        pBuff[i] = '-';
+    pBuff[i] = 0;
+    for ( i = 0; i < p->nLits; i++ )
+    {
+        if ( p->Lits[i] == -1 )
+            continue;
+        pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
+    }
+    if ( vFlopCounts )
+    {
+        // skip some literals
+        Vec_IntForEachEntry( vFlopCounts, Entry, i )
+            if ( Entry ) 
+                pBuff[k++] = pBuff[i];
+        pBuff[k] = 0;
+    }
+    Vec_StrPushBuffer( vStr, pBuff, k );
+    Vec_StrPush( vStr, ' ' );
+    Vec_StrPush( vStr, '0' );
+    Vec_StrPush( vStr, '\n' );
+    ABC_FREE( pBuff );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Return 1 if pOld set-theoretically contains pNew.]
 
   Description []