Updating testcext to ignore the diff in register count and other things.

5 files changed, 93 insertions, 20 deletions

diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index 0e49cd7c..e9f3df37 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -242,8 +242,8 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex
     Vec_PtrFree( vSimInfo );
     if ( pPars->fVerbose )
         ABC_PRT( "Time", clock() - clkTotal );
-    if ( RetValue && pPars->fCheckMiter )
-        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
+//    if ( RetValue && pPars->fCheckMiter )
+//        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
     return RetValue;
 }
 
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 125f3592..d94a0412 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1191,9 +1191,11 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
 {
     Gia_Obj_t * pObj, * pObjRi, * pObjRo;
     int RetValue, i, k, iBit = 0;
+    assert( Gia_ManPiNum(pAig) == p->nPis );
     Gia_ManCleanMark0(pAig);
-    Gia_ManForEachRo( pAig, pObj, i )
-        pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+//    Gia_ManForEachRo( pAig, pObj, i )
+//       pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+    iBit = p->nRegs;
     for ( i = 0; i <= p->iFrame; i++ )
     {
         Gia_ManForEachPi( pAig, pObj, k )
@@ -1207,7 +1209,7 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
             pObjRo->fMark0 = pObjRi->fMark0;
     }
     assert( iBit == p->nBits );
-    // remember the number of failed output
+    // figure out the number of failed output
     RetValue = -1;
     for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- )
     {
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 62ac35ac..c21ac625 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -62,6 +62,7 @@ struct Saig_ParBmc_t_
     int         nFramesMax;   // maximum number of timeframes 
     int         nConfLimit;   // maximum number of conflicts at a node
     int         nTimeOut;     // approximate timeout in seconds
+    int         nPisAbstract; // the number of PIs to abstract
     int         fSolveAll;    // does not stop at the first SAT output
     int         fDropSatOuts; // replace sat outputs by constant 0
     int         fVerbose;     // verbose 
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index e038d7a0..d82b4c39 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -551,10 +551,6 @@ void Saig_ManBmcMappingTest( Aig_Man_t * p )
 
 
 
-
-
-
-
 /**Function*************************************************************
 
   Synopsis    [Create manager.]
@@ -613,6 +609,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
 ***********************************************************************/
 void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
 {
+    Aig_ManCleanMarkA( p->pAig );
     if ( p->vCexes )
     {
         assert( p->pAig->pSeqModelVec == NULL );
@@ -1002,6 +999,58 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
 
 /**Function*************************************************************
 
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeCompareRefsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
+{
+    int Diff = Aig_ObjRefs(*pp1) - Aig_ObjRefs(*pp2);
+    if ( Diff > 0 )
+        return -1;
+    if ( Diff < 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mark PIs to be skipped based on nPisAbstract.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract )
+{
+    Vec_Ptr_t * vPis;
+    Aig_Obj_t * pObj;
+    int i;
+    if ( nPisAbstract < 1 )
+        return;
+    // sort PIs by the number of their fanouts
+//    Saig_ManForEachPi( pAig, pObj, i )
+//        printf( "%d=%d ", i, Aig_ObjRefs(pObj) );
+//    printf( "\n" );
+    vPis = Vec_PtrAlloc( 100 );
+    Saig_ManForEachPi( pAig, pObj, i )
+        Vec_PtrPush( vPis, pObj );
+    Vec_PtrSort( vPis, (int (*)(void))Aig_NodeCompareRefsDecrease );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vPis, pObj, i )
+        if ( i > Saig_ManPiNum(pAig) - nPisAbstract )
+            pObj->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [This procedure sets default parameters.]
 
   Description []
@@ -1018,6 +1067,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
     p->nFramesMax     =  2000;    // maximum number of timeframes 
     p->nConfLimit     =  2000;    // maximum number of conflicts at a node
     p->nTimeOut       =     0;    // approximate timeout in seconds
+    p->nPisAbstract   =     0;    // the number of PIs to abstract
     p->fSolveAll      =     0;    // stops on the first SAT instance
     p->fDropSatOuts   =     0;    // replace sat outputs by constant 0
     p->fVerbose       =     0;    // verbose 
@@ -1058,6 +1108,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     if ( p->pPars->nTimeOut )
         sat_solver_set_runtime_limit( p->pSat, clock() + p->pPars->nTimeOut * CLOCKS_PER_SEC );
     // perform frames
+//    Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract );
     for ( f = 0; f < pPars->nFramesMax; f++ )
     {
         pPars->iFrame = f;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1f15592d..10360809 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8544,7 +8544,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
 //    Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" );
 //    Ssm_ManExperiment( "m\\big3.ssim", "m\\big3_.ssim" );
-    Ssm_ManExperiment( "m\\tb.ssim", "m\\tb_.ssim" );
+//    Ssm_ManExperiment( "m\\tb.ssim", "m\\tb_.ssim" );
+    Ssm_ManExperiment( "m\\simp.ssim", "m\\simp_.ssim" );
+}
+*/
+/*
+{
+    Gia_Man_t * pGia = Abc_ManReadAig( "bug\\61\\tmp.out", "aig:" );
+    Gia_ManStop( pGia );
 }
 */
     return 0;
@@ -18340,7 +18347,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Saig_ParBmcSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCLsdrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCILsdrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -18388,6 +18395,17 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nConfLimit < 0 ) 
                 goto usage;
             break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nPisAbstract = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nPisAbstract < 0 ) 
+                goto usage;
+            break;
         case 'L':
             if ( globalUtilOptind >= argc )
             {
@@ -18454,12 +18472,13 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: bmc3 [-SFTC num] [-L file] [-sdvh]\n" );
+    Abc_Print( -2, "usage: bmc3 [-SFTCI num] [-L file] [-sdvh]\n" );
     Abc_Print( -2, "\t         performs bounded model checking with dynamic unrolling\n" );
     Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
     Abc_Print( -2, "\t-F num : the max number of time frames [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract );
     Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
     Abc_Print( -2, "\t-s     : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" );
     Abc_Print( -2, "\t-d     : drops (replaces by 0) satisfiable outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" );
@@ -19831,10 +19850,10 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
         else if ( Abc_NtkPiNum(pNtk) != pAbc->pCex->nPis )
             Abc_Print( 1, "Main AIG: The number of PIs (%d) is different from cex (%d).\n", Abc_NtkPiNum(pNtk), pAbc->pCex->nPis );
-        else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs )
-            Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs );
-        else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo )
-            Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
+//        else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs )
+//            Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs );
+//        else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo )
+//            Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
         else 
         {
             extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
@@ -19860,10 +19879,10 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( 1, "And  AIG: There is no current network.\n");
         else if ( Gia_ManPiNum(pAbc->pGia) != pAbc->pCex->nPis )
             Abc_Print( 1, "And  AIG: The number of PIs (%d) is different from cex (%d).\n", Gia_ManPiNum(pAbc->pGia), pAbc->pCex->nPis );
-        else if ( Gia_ManRegNum(pAbc->pGia) != pAbc->pCex->nRegs )
-            Abc_Print( 1, "And  AIG: The number of registers (%d) is different from cex (%d).\n", Gia_ManRegNum(pAbc->pGia), pAbc->pCex->nRegs );
-        else if ( Gia_ManPoNum(pAbc->pGia) <= pAbc->pCex->iPo )
-            Abc_Print( 1, "And  AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo );
+//        else if ( Gia_ManRegNum(pAbc->pGia) != pAbc->pCex->nRegs )
+//            Abc_Print( 1, "And  AIG: The number of registers (%d) is different from cex (%d).\n", Gia_ManRegNum(pAbc->pGia), pAbc->pCex->nRegs );
+//        else if ( Gia_ManPoNum(pAbc->pGia) <= pAbc->pCex->iPo )
+//            Abc_Print( 1, "And  AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo );
         else 
         {
     //        if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )