Added new options to testcex.

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"

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 );

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;
 }

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,6 +19821,8 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 
+    if ( !fCheckAnd )
+    {
         // check the main AIG
         pNtk = Abc_FrameReadNtk(pAbc);
         if ( pNtk == NULL )
@@ -19822,9 +19840,9 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
             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 ) )
+    //        if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
             int iPoOld = pAbc->pCex->iPo;
-        pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pGia, pAbc->pCex );
+            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 )
@@ -19834,7 +19852,9 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
             Gia_ManStop( pGia );
             Aig_ManStop( pAig );
         }
-
+    }
+    else
+    {
         // check the AND AIG
         if ( pAbc->pGia == NULL )
             Abc_Print( 1, "And  AIG: There is no current network.\n");
@@ -19846,9 +19866,9 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
             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 ) )
+    //        if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
             int iPoOld = pAbc->pCex->iPo;
-        pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex );
+            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 )
@@ -19856,11 +19876,14 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
             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, "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;
 }

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" );