Added new options to testcex.

5 files changed, 78 insertions, 277 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 5e6745b6..d0007d9b 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -4182,230 +4182,6 @@ SOURCE=.\src\aig\llb\llb4Sweep.c
 SOURCE=.\src\aig\llb\llbInt.h
 # End Source File
 # End Group
-# Begin Group "au"
-
-# PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\aig\au\au.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\au.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auBridge.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auCec.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auCut.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auCutDiv.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auCutEnum.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auCutExp.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auData.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auDec6.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auDsdData.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auDsdForm.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auDsdTab.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auFanout.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auFour.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auHash.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auInt.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auMffc.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auNtk.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auNtk.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auResCore.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auResCut.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auResDec.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auResDiv.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auResTruth.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auSat.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auSatData.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auSatSim.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auSupp.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auSweep.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auTruth.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auTruth.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\au\auUtil.c
-# End Source File
-# End Group
-# Begin Group "ssm"
-
-# PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssm.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssm.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssmApi.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssmClock.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssmInt.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssmRandom.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssmRead.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssmReset.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssmSchedule.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssmSimple.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssmSimulate.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ssm\ssmWrite.c
-# End Source File
-# End Group
-# Begin Group "ddb"
-
-# PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\aig\ddb\ddb.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ddb\ddb.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ddb\ddbGarb.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ddb\ddbInt.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ddb\ddbMan.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ddb\ddbOper.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ddb\ddbReo.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\ddb\ddbTable.c
-# End Source File
-# End Group
 # End Group
 # End Group
 # Begin Group "Header Files"
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d0bd454f..efe4d1d3 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -803,7 +803,7 @@ extern int                 Gia_ManHasDangling( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
 extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern int                 Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
-extern int                 Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p );
+extern int                 Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
 extern Tas_Man_t *         Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 2794956a..125f3592 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1187,7 +1187,7 @@ int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p )
+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;
@@ -1209,12 +1209,14 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p )
     assert( iBit == p->nBits );
     // remember the number of failed output
     RetValue = -1;
-    Gia_ManForEachPo( pAig, pObj, i )
+    for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- )
+    {
         if ( Gia_ManPo(pAig, i)->fMark0 )
         {
             RetValue = i;
             break;
         }
+    }
     Gia_ManCleanMark0(pAig);
     return RetValue;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0988549a..1f15592d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -19786,11 +19786,27 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
 {    
     Abc_Ntk_t * pNtk;
     int c;
+    int nOutputs = 0;
+    int fCheckAnd = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Oah" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'O':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nOutputs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nOutputs < 0 ) 
+                goto usage;
+            break;
+        case 'a':
+            fCheckAnd ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -19805,63 +19821,70 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 
-    // check the main AIG
-    pNtk = Abc_FrameReadNtk(pAbc);
-    if ( pNtk == NULL )
-        Abc_Print( 1, "Main AIG: There is no current network.\n");
-    else if ( !Abc_NtkIsStrash(pNtk) )
-        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 ( !fCheckAnd )
     {
-        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-        Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
-//        if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
-        int iPoOld = pAbc->pCex->iPo;
-        pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pGia, pAbc->pCex );
-        if ( pAbc->pCex->iPo == -1 )
-            Abc_Print( 1, "Main AIG: The cex does not fail any outputs.\n" );
-        else if ( iPoOld != pAbc->pCex->iPo )
-            Abc_Print( 1, "Main AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
+        // check the main AIG
+        pNtk = Abc_FrameReadNtk(pAbc);
+        if ( pNtk == NULL )
+            Abc_Print( 1, "Main AIG: There is no current network.\n");
+        else if ( !Abc_NtkIsStrash(pNtk) )
+            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 
-            Abc_Print( 1, "Main AIG: The cex is correct.\n" );
-        Gia_ManStop( pGia );
-        Aig_ManStop( pAig );
+        {
+            extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+            Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+            Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
+    //        if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
+            int iPoOld = pAbc->pCex->iPo;
+            pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pGia, pAbc->pCex, nOutputs );
+            if ( pAbc->pCex->iPo == -1 )
+                Abc_Print( 1, "Main AIG: The cex does not fail any outputs.\n" );
+            else if ( iPoOld != pAbc->pCex->iPo )
+                Abc_Print( 1, "Main AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
+            else 
+                Abc_Print( 1, "Main AIG: The cex is correct.\n" );
+            Gia_ManStop( pGia );
+            Aig_ManStop( pAig );
+        }
     }
-
-    // check the AND AIG
-    if ( pAbc->pGia == NULL )
-        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 
+    else
     {
-//        if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
-        int iPoOld = pAbc->pCex->iPo;
-        pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex );
-        if ( pAbc->pCex->iPo == -1 )
-            Abc_Print( 1, "And  AIG: The cex does not fail any outputs.\n" );
-        else if ( iPoOld != pAbc->pCex->iPo )
-            Abc_Print( 1, "And  AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
+        // check the AND AIG
+        if ( pAbc->pGia == NULL )
+            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 
-            Abc_Print( 1, "And  AIG: The cex is correct.\n" );
+        {
+    //        if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
+            int iPoOld = pAbc->pCex->iPo;
+            pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex, nOutputs );
+            if ( pAbc->pCex->iPo == -1 )
+                Abc_Print( 1, "And  AIG: The cex does not fail any outputs.\n" );
+            else if ( iPoOld != pAbc->pCex->iPo )
+                Abc_Print( 1, "And  AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
+            else 
+                Abc_Print( 1, "And  AIG: The cex is correct.\n" );
+        }
     }
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: testcex -h\n" );
-    Abc_Print( -2, "\t        tests the current cex against the current AIG and &-AIG\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
+    Abc_Print( -2, "usage: testcex [-O num] [-ah]\n" );
+    Abc_Print( -2, "\t         tests the current cex against the current AIG or the &-AIG\n" );
+    Abc_Print( -2, "\t-O num : the number of real POs in the PO list [default = %d]\n", nOutputs );
+    Abc_Print( -2, "\t-a     : toggle checking the current AIG or the &-AIG [default = %s]\n", fCheckAnd ? "&-AIG": "current AIG" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
 
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index 958dac40..5617e75d 100644
--- a/src/base/cmd/cmdPlugin.c
+++ b/src/base/cmd/cmdPlugin.c
@@ -598,7 +598,7 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
 //                    Abc_Print( 1, "Generated counter-example is INVALID.\n" );
 
                 // remporary work-around to detect the output number - October 18, 2010
-                pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex );
+                pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex, 0 );
                 if ( pAbc->pCex->iPo == -1 )
                 {
                     Abc_Print( 1, "Generated counter-example is INVALID.\n" );