added -I options in &bmiter

.gitignore

@@ -8,6 +8,12 @@ ReleaseExt/
 
 _/
 _TEST/
+_sandwich/
+_scripts/
+*.aig
+*.vcproj
+*.sh
+*.v
 lib/abc*
 lib/m114*
 lib/bip*

src/aig/gia/giaDup.c

@@ -5669,7 +5669,7 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
+Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum)
 {
     Vec_Int_t * vLits;
     Gia_Man_t * pNew, * pTemp;
@@ -5717,6 +5717,9 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
     Vec_Int_t * vTypeSpec = Vec_IntAlloc( 16 );
     Vec_IntFill( vTypeSpec, Gia_ManObjNum(p1), 0 );
     int n = Gia_ManBufNum(p1) / 2;
+    if(biNum > 0){
+        n = biNum;
+    }
 
     Gia_ManStaticFanoutStart( p1 );
     Vec_Ptr_t * vQ = Vec_PtrAlloc(16);

src/base/abci/abc.c

@@ -37921,7 +37921,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0;
     Cec4_ManSetParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -38074,6 +38074,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'w':
             pPars->fVeryVerbose ^= 1;
             break;
+        case 'q':
+            pPars->fBMiterInfo ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -38138,6 +38141,7 @@ usage:
     Abc_Print( -2, "\t-o     : toggle using the old SAT sweeper [default = %s]\n", fUseIvy? "yes": "no" );
     Abc_Print( -2, "\t-p     : toggle trying to prove when running the old SAT sweeper [default = %s]\n", fUseProve? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-q     : toggle printing additional information for boundary miters [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -51689,16 +51693,25 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
+    extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum);
     Gia_Man_t * pTemp, * pSecond;
     char * FileName = NULL;
     FILE * pFile = NULL;
     int c, fVerbose = 0;
+    int bi  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            bi = atoi(argv[globalUtilOptind++]);
+            break;    
         case 'v':
             fVerbose ^= 1;
             break;
@@ -51737,14 +51750,15 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9BMiter(): Cannot read the file name on the command line.\n" );
         return 0;
     }    
-    pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose );
+    pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose, bi);
     Gia_ManStop( pSecond );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &bmiter [-vh] <file>\n" );
+    Abc_Print( -2, "usage: &bmiter -I <biNum> [-vh] <file>\n" );
     Abc_Print( -2, "\t         creates the boundary miter\n" );
+    Abc_Print( -2, "\t-I <biNum>:   number of boundary inputs\n" );
     Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : the implementation file\n");    

src/base/abci/abcMiter.c

@@ -789,6 +789,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVer
     pNtkFrames->pName = Extra_UtilStrsav(Buffer);
     // map the constant nodes
     Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames);
+    
     // create new latches (or their initial values) and remember them in the new latches
     if ( !fInitial )
     {

src/proof/cec/cec.h

@@ -120,6 +120,7 @@ struct Cec_ParFra_t_
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
     int              iOutFail;      // the failed output
+    int              fBMiterInfo;   // printing BMiter information
 };
 
 // combinational equivalence checking parameters

src/proof/cec/cecSatG2.c

@@ -222,6 +222,7 @@ void Cec4_ManSetParams( Cec_ParFra_t * pPars )
     pPars->nSatVarMax     =    1000;    // the max number of SAT variables before recycling SAT solver
     pPars->nCallsRecycle  =     500;    // calls to perform before recycling SAT solver
     pPars->nGenIters      =     100;    // pattern generation iterations
+    pPars->fBMiterInfo    =       0;    // printing BMiter information
 }
 
 /**Function*************************************************************
@@ -1891,39 +1892,41 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
         }
         if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) )
         {
-            if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 )
+            if (pPars->fBMiterInfo){
-            {
+                if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 )
-                switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) )
                 {
-                    case 1:
+                    switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) )
-                    case 4:
-                        Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 );
-                        break;
-                    case 2:
-                    case 5:
-                        Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 );
-                        break;
-                    default:
-                        break;
-                }
-            }
-            else 
-            {
-                if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 ) 
-                    switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) )
                     {
                         case 1:
                         case 4:
-                            Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 );
+                            Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 );
                             break;
                         case 2:
                         case 5:
-                            Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 );
+                            Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 );
                             break;
                         default:
                             break;
-
                     }
+                }
+                else 
+                {
+                    if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 ) 
+                        switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) )
+                        {
+                            case 1:
+                            case 4:
+                                Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 );
+                                break;
+                            case 2:
+                            case 5:
+                                Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 );
+                                break;
+                            default:
+                                break;
+
+                        }
+                }
             }
             pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
         }
@@ -1979,22 +1982,24 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
     Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
 
     // TODO
-    int e, i, c1=0, c2=0, c3=0, c4=0, c5=0;
+    if (pPars -> fBMiterInfo){
-    Vec_IntForEachEntry( vLitBmiter, e, i )
+        int e, i, c1=0, c2=0, c3=0, c4=0, c5=0;
-    {
+        Vec_IntForEachEntry( vLitBmiter, e, i )
-        if ( i%2 ) continue;
-        switch (e)
         {
-        case 1: c1++; break;
+            if ( i%2 ) continue;
-        case 2: c2++; break;
+            switch (e)
-        case 3: c3++; break;
+            {
-        case 4: c4++; break;
+            case 1: c1++; break;
-        case 5: c5++; break;
+            case 2: c2++; break;
-        default:
+            case 3: c3++; break;
-            break;
+            case 4: c4++; break;
+            case 5: c5++; break;
+            default:
+                break;
+            }
         }
+        printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5);
     }
-    printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5);
     return pNew;
 }
 void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )