Printing counter-examples in "cec" and "&cec".

src/aig/gia/giaDeep.c

@@ -238,6 +238,22 @@ Gia_Man_t * Gia_ManRandSyn( Gia_Man_t * p, unsigned random_seed )
     return pRes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDeepSyn2( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fChoices, int fVerbose )
+{
+    return Gia_ManDeepSyn( pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fChoices, fVerbose );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abc.c

@@ -42510,6 +42510,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
     }
+    pPars->pNameSpec = pGias[0] ? (pGias[0]->pSpec ? pGias[0]->pSpec : pGias[0]->pName) : NULL;
+    pPars->pNameImpl = pGias[1] ? (pGias[1]->pSpec ? pGias[1]->pSpec : pGias[1]->pName) : NULL;
+    pPars->vNamesIn  = pGias[0] ? pGias[0]->vNamesIn : NULL;
     // compute the miter
     if ( Gia_ManCiNum(pGias[0]) < 6 )
     {
@@ -54533,9 +54536,10 @@ usage:
 int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fChoices, int fVerbose );
-    Gia_Man_t * pTemp; int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 0, nAnds = 0, Seed = 0, fUseTwo = 0, fChoices = 0, fVerbose = 0;
+    extern Gia_Man_t * Gia_ManDeepSyn2( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fChoices, int fVerbose );
+    Gia_Man_t * pTemp; int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 0, nAnds = 0, Seed = 0, fUseTwo = 0, fChoices = 0, fOpt = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "IJTAStcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IJTAStcovh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -54600,6 +54604,9 @@ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fChoices ^= 1;
             break;
+        case 'o':
+            fOpt ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -54614,12 +54621,15 @@ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9DeepSyn(): There is no AIG.\n" );
         return 0;
     }
+    if ( fOpt ) 
+        pTemp = Gia_ManDeepSyn2( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fChoices, fVerbose );
+    else
         pTemp = Gia_ManDeepSyn( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fChoices, fVerbose );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &deepsyn [-IJTAS <num>] [-tcvh]\n" );
+    Abc_Print( -2, "usage: &deepsyn [-IJTAS <num>] [-tcovh]\n" );
     Abc_Print( -2, "\t           performs synthesis\n" );
     Abc_Print( -2, "\t-I <num> : the number of iterations [default = %d]\n",                   nIters  );
     Abc_Print( -2, "\t-J <num> : the number of steps without improvements [default = %d]\n",   nNoImpr  );
@@ -54628,6 +54638,7 @@ usage:
     Abc_Print( -2, "\t-S <num> : user-specified random seed (0 <= num <= 100) [default = %d]\n", Seed  );
     Abc_Print( -2, "\t-t       : toggle using two-input LUTs [default = %s]\n",                fUseTwo? "yes": "no" );
     Abc_Print( -2, "\t-c       : toggle computing structural choices [default = %s]\n",        fChoices? "yes": "no" );
+    Abc_Print( -2, "\t-o       : toggle using optimization [default = %s]\n",                  fOpt? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",       fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;

src/base/abci/abcVerify.c

@@ -731,6 +731,147 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
     return pValues;
 }
 
+typedef struct Abc_NtkCexWord_t_
+{
+    char *      pBase;
+    Vec_Int_t * vBits;
+} Abc_NtkCexWord_t;
+
+static Abc_NtkCexWord_t * Abc_NtkVerifyFindWord( Vec_Ptr_t * vWords, const char * pBase )
+{
+    Abc_NtkCexWord_t * pWord;
+    int i;
+    Vec_PtrForEachEntry( Abc_NtkCexWord_t *, vWords, pWord, i )
+        if ( !strcmp( pWord->pBase, pBase ) )
+            return pWord;
+    pWord = ABC_ALLOC( Abc_NtkCexWord_t, 1 );
+    pWord->pBase = ABC_ALLOC( char, strlen(pBase) + 1 );
+    strcpy( pWord->pBase, pBase );
+    pWord->vBits = Vec_IntAlloc( 0 );
+    Vec_PtrPush( vWords, pWord );
+    return pWord;
+}
+
+static void Abc_NtkVerifyFreeWords( Vec_Ptr_t * vWords )
+{
+    Abc_NtkCexWord_t * pWord;
+    int i;
+    Vec_PtrForEachEntry( Abc_NtkCexWord_t *, vWords, pWord, i )
+    {
+        ABC_FREE( pWord->pBase );
+        Vec_IntFree( pWord->vBits );
+        ABC_FREE( pWord );
+    }
+    Vec_PtrFree( vWords );
+}
+
+static int Abc_NtkVerifyParseBitName( const char * pName, char ** ppBase, int * pIndex )
+{
+    const char * pOpen;
+    const char * pClose;
+    char * pEnd;
+    long Index;
+    *ppBase = NULL;
+    pClose = strrchr( pName, ']' );
+    pOpen  = pClose ? strrchr( pName, '[' ) : NULL;
+    if ( pOpen == NULL || pClose == NULL || pClose < pOpen || pClose[1] != 0 )
+        return 0;
+    Index = strtol( pOpen + 1, &pEnd, 10 );
+    if ( pEnd != pClose || Index < 0 )
+        return 0;
+    *pIndex = (int)Index;
+    *ppBase = ABC_ALLOC( char, pOpen - pName + 1 );
+    strncpy( *ppBase, pName, pOpen - pName );
+    (*ppBase)[pOpen - pName] = 0;
+    return 1;
+}
+
+static int Abc_NtkVerifyCollectWords( Vec_Ptr_t * vWords, const char * const * ppNames, const int * pValues, int nEntries )
+{
+    int i, fHasVector = 0;
+    for ( i = 0; i < nEntries; i++ )
+    {
+        char * pBase = NULL;
+        int Index = 0;
+        int fVector = Abc_NtkVerifyParseBitName( ppNames[i], &pBase, &Index );
+        Abc_NtkCexWord_t * pWord = Abc_NtkVerifyFindWord( vWords, fVector ? pBase : ppNames[i] );
+        Vec_IntSetEntry( pWord->vBits, fVector ? Index : 0, pValues[i] );
+        fHasVector |= fVector;
+        if ( pBase )
+            ABC_FREE( pBase );
+    }
+    return fHasVector;
+}
+
+static void Abc_NtkVerifyPrintWords( Vec_Ptr_t * vWords )
+{
+    Abc_NtkCexWord_t * pWord;
+    int i, d, b, nBits, nHex, Digit;
+    Vec_PtrForEachEntry( Abc_NtkCexWord_t *, vWords, pWord, i )
+    {
+        nBits = Vec_IntSize( pWord->vBits );
+        nHex  = (nBits + 3) / 4;
+        nHex  = nHex ? nHex : 1;
+        {
+            char * pHex = ABC_ALLOC( char, nHex + 1 );
+            for ( d = 0; d < nHex; d++ )
+            {
+                Digit = 0;
+                for ( b = 0; b < 4; b++ )
+                {
+                    int iBit = d * 4 + b;
+                    if ( iBit < nBits && Vec_IntEntry( pWord->vBits, iBit ) )
+                        Digit |= 1 << b;
+                }
+                pHex[nHex - d - 1] = "0123456789ABCDEF"[Digit];
+            }
+            pHex[nHex] = 0;
+            printf( "%s = %d'h%s", pWord->pBase, nBits, pHex );
+            ABC_FREE( pHex );
+        }
+        if ( i + 1 < Vec_PtrSize(vWords) )
+            printf( ", " );
+    }
+}
+
+void Abc_NtkVerifyPrintCex( const int * pModel, const int * pValues1, const int * pValues2, 
+    const char * const * ppInputNames, int nInputs, const char * const * ppOutputNames, int nOutputs, 
+    const char * pNtkName1, const char * pNtkName2 )
+{
+    Vec_Ptr_t * vInputs   = Vec_PtrAlloc( 0 );
+    Vec_Ptr_t * vOutputs1 = Vec_PtrAlloc( 0 );
+    Vec_Ptr_t * vOutputs2 = Vec_PtrAlloc( 0 );
+    Abc_NtkVerifyCollectWords( vInputs, ppInputNames, pModel, nInputs );
+    Abc_NtkVerifyCollectWords( vOutputs1, ppOutputNames, pValues1, nOutputs );
+    if ( pValues2 )
+        Abc_NtkVerifyCollectWords( vOutputs2, ppOutputNames, pValues2, nOutputs );
+    if ( Vec_PtrSize(vInputs) || Vec_PtrSize(vOutputs1) || Vec_PtrSize(vOutputs2) )
+    {
+        printf( "INPUT: " );
+        Abc_NtkVerifyPrintWords( vInputs );
+        printf( ".  OUTPUT: " );
+        Abc_NtkVerifyPrintWords( vOutputs1 );
+        printf( " (%s)", pNtkName1 ? pNtkName1 : "network1" );
+        if ( pValues2 && Vec_PtrSize(vOutputs2) )
+        {
+            printf( ", " );
+            Abc_NtkVerifyPrintWords( vOutputs2 );
+            printf( " (%s)", pNtkName2 ? pNtkName2 : "network2" );
+        }
+        printf( ".\n" );
+    }
+    Abc_NtkVerifyFreeWords( vInputs );
+    Abc_NtkVerifyFreeWords( vOutputs1 );
+    Abc_NtkVerifyFreeWords( vOutputs2 );
+}
+
+static const char * Abc_NtkVerifyNetworkName( Abc_Ntk_t * pNtk )
+{
+    if ( pNtk == NULL )
+        return NULL;
+    return Abc_NtkSpec(pNtk) ? Abc_NtkSpec(pNtk) : Abc_NtkName(pNtk);
+}
+
 
 /**Function*************************************************************
 
@@ -747,6 +888,8 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
 {
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
+    const char ** ppCiNames = NULL;
+    const char ** ppCoNames = NULL;
     int * pValues1, * pValues2;
     int nErrors, nPrinted, i, iNode = -1;
 
@@ -755,6 +898,17 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
     // get the CO values under this model
     pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel );
     pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel );
+    // print word-level counter-example, if available
+    ppCiNames = ABC_ALLOC( const char *, Abc_NtkCiNum(pNtk1) );
+    Abc_NtkForEachCi( pNtk1, pNode, i )
+        ppCiNames[i] = Abc_ObjName( pNode );
+    ppCoNames = ABC_ALLOC( const char *, Abc_NtkCoNum(pNtk1) );
+    Abc_NtkForEachCo( pNtk1, pNode, i )
+        ppCoNames[i] = Abc_ObjName( pNode );
+    Abc_NtkVerifyPrintCex( pModel, pValues1, pValues2, ppCiNames, Abc_NtkCiNum(pNtk1), 
+        ppCoNames, Abc_NtkCoNum(pNtk1), Abc_NtkVerifyNetworkName(pNtk1), Abc_NtkVerifyNetworkName(pNtk2) );
+    ABC_FREE( ppCiNames );
+    ABC_FREE( ppCoNames );
     // count the mismatches
     nErrors = 0;
     for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
@@ -1115,4 +1269,3 @@ int Abc_NtkIsValidCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
 
 
 ABC_NAMESPACE_IMPL_END
-

src/proof/cec/cec.h

@@ -140,6 +140,9 @@ struct Cec_ParCec_t_
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
     int              iOutFail;      // the number of failed output
+    const char *     pNameSpec;     // name of the first (spec) network
+    const char *     pNameImpl;     // name of the second (impl) network
+    Vec_Ptr_t *      vNamesIn;      // input names of the first network
 };
 
 // sequential register correspodence parameters
@@ -273,4 +276,3 @@ ABC_NAMESPACE_HEADER_END
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-

src/proof/cec/cecCec.c

@@ -24,6 +24,10 @@
 #include "misc/extra/extra.h"
 #include "sat/cnf/cnf.h"
 
+void Abc_NtkVerifyPrintCex( const int * pModel, const int * pValues1, const int * pValues2, 
+    const char * const * ppInputNames, int nInputs, const char * const * ppOutputNames, int nOutputs, 
+    const char * pNtkName1, const char * pNtkName2 );
+
 ABC_NAMESPACE_IMPL_START
 
 
@@ -35,6 +39,105 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+static int * Cec_ManSimulateCombOutputs( Gia_Man_t * p, const int * pInputs )
+{
+    Gia_Obj_t * pObj;
+    int * pValues, * pOutputs, i;
+    pValues = ABC_ALLOC( int, Gia_ManObjNum(p) );
+    if ( pValues == NULL )
+        return NULL;
+    pValues[0] = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        pValues[Gia_ObjId(p, pObj)] = pInputs[i];
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        int v0 = pValues[Gia_ObjFaninId0p(p, pObj)] ^ Gia_ObjFaninC0(pObj);
+        int v1 = pValues[Gia_ObjFaninId1p(p, pObj)] ^ Gia_ObjFaninC1(pObj);
+        pValues[Gia_ObjId(p, pObj)] = v0 & v1;
+    }
+    pOutputs = ABC_ALLOC( int, Gia_ManPoNum(p) );
+    Gia_ManForEachPo( p, pObj, i )
+        pOutputs[i] = pValues[Gia_ObjFaninId0p(p, pObj)] ^ Gia_ObjFaninC0(pObj);
+    ABC_FREE( pValues );
+    return pOutputs;
+}
+
+static const char * Cec_ManGetName( const char * pName, const char * pPrefix, int Idx, Vec_Ptr_t * vStore )
+{
+    if ( pName )
+        return pName;
+    {
+        char Buffer[64];
+        sprintf( Buffer, "%s[%d]", pPrefix, Idx );
+        pName = Abc_UtilStrsav( Buffer );
+        Vec_PtrPush( vStore, (void *)pName );
+        return pName;
+    }
+}
+
+static void Cec_ManPrintCexSummary( Gia_Man_t * p, Abc_Cex_t * pCex, Cec_ParCec_t * pPars )
+{
+    Vec_Ptr_t * vToFree = NULL;
+    const char ** ppInNames = NULL;
+    const char ** ppOutNames = NULL;
+    int * pInputs = NULL;
+    int * pOutputs = NULL;
+    int * pOut1 = NULL;
+    int * pOut2 = NULL;
+    int nPis, nPairs, i;
+    if ( (pPars && pPars->fSilent) || pCex == NULL )
+        return;
+    if ( pCex->nRegs || pCex->iFrame || Gia_ManRegNum(p) )
+        return;
+    if ( (Gia_ManPoNum(p) & 1) || Gia_ManPiNum(p) != pCex->nPis )
+        return;
+    nPis   = Gia_ManPiNum(p);
+    nPairs = Gia_ManPoNum(p) / 2;
+    pInputs = ABC_ALLOC( int, nPis );
+    for ( i = 0; i < nPis; i++ )
+        pInputs[i] = Abc_InfoHasBit( pCex->pData, pCex->nRegs + i );
+    pOutputs = Cec_ManSimulateCombOutputs( p, pInputs );
+    if ( pOutputs == NULL )
+        goto finish;
+    pOut1 = ABC_ALLOC( int, nPairs );
+    pOut2 = ABC_ALLOC( int, nPairs );
+    for ( i = 0; i < nPairs; i++ )
+    {
+        pOut1[i] = pOutputs[2 * i];
+        pOut2[i] = pOutputs[2 * i + 1];
+    }
+    vToFree = Vec_PtrAlloc( 16 );
+    ppInNames = ABC_ALLOC( const char *, nPis );
+    for ( i = 0; i < nPis; i++ )
+    {
+        const char * pName = Gia_ObjCiName(p, i);
+        if ( pName == NULL && pPars && pPars->vNamesIn && i < Vec_PtrSize(pPars->vNamesIn) )
+            pName = (const char *)Vec_PtrEntry( pPars->vNamesIn, i );
+        ppInNames[i] = Cec_ManGetName( pName, "a", i, vToFree );
+    }
+    ppOutNames = ABC_ALLOC( const char *, nPairs );
+    for ( i = 0; i < nPairs; i++ )
+        ppOutNames[i] = Cec_ManGetName( Gia_ObjCoName(p, 2 * i), "z", i, vToFree );
+    Abc_NtkVerifyPrintCex( pInputs, pOut1, pOut2, ppInNames, nPis, ppOutNames, nPairs, 
+        pPars && pPars->pNameSpec ? pPars->pNameSpec : Gia_ManName(p), 
+        pPars && pPars->pNameImpl ? pPars->pNameImpl : (p->pSpec ? p->pSpec : Gia_ManName(p)) );
+
+finish:
+    if ( vToFree )
+    {
+        char * pName;
+        Vec_PtrForEachEntry( char *, vToFree, pName, i )
+            ABC_FREE( pName );
+        Vec_PtrFree( vToFree );
+    }
+    ABC_FREE( ppInNames );
+    ABC_FREE( ppOutNames );
+    ABC_FREE( pOut1 );
+    ABC_FREE( pOut2 );
+    ABC_FREE( pOutputs );
+    ABC_FREE( pInputs );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Saves the input pattern with the given number.]
@@ -160,6 +263,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
             }
             pPars->iOutFail = i/2;
             Cec_ManTransformPattern( p, i/2, NULL );
+            Cec_ManPrintCexSummary( p, p->pCexComb, pPars );
             return 0;
         }
         // get the drivers
@@ -178,6 +282,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
             // if their compl attributes are the same - one should be complemented
             assert( Gia_ObjFaninC0(pObj1) == Gia_ObjFaninC0(pObj2) );
             Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri1) );
+            Cec_ManPrintCexSummary( p, p->pCexComb, pPars );
             return 0;
         }
         // one of the drivers is a PI; another is a constant 0
@@ -197,6 +302,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
                 Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri1) );
             else
                 Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri2) );
+            Cec_ManPrintCexSummary( p, p->pCexComb, pPars );
             return 0;
         }
     }
@@ -383,6 +489,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
             Abc_Print( 1, "Networks are NOT EQUIVALENT.  " );
             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
             }
+            Cec_ManPrintCexSummary( p, p->pCexComb, pPars );
             return 0;
         }
         Vec_IntFreeP( &pInit->vIdsEquiv );
@@ -417,6 +524,8 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;
     if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
         Abc_Print( 1, "Counter-example simulation has failed.\n" );
+    if ( RetValue == 0 )
+        Cec_ManPrintCexSummary( p, p->pCexComb, pPars );
     Gia_ManStop( pNew );
     return RetValue;
 }
@@ -601,4 +710,3 @@ Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose )
 
 
 ABC_NAMESPACE_IMPL_END
-

src/proof/cec/cecCore.c

@@ -167,6 +167,9 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
     p->fVeryVerbose   =       0;  // verbose stats
     p->fVerbose       =       0;  // verbose stats
     p->iOutFail       =      -1;  // the number of failed output
+    p->pNameSpec      =    NULL;  // name of the first (spec) network
+    p->pNameImpl      =    NULL;  // name of the second (impl) network
+    p->vNamesIn       =    NULL;  // input names of the first network
 }  
 
 /**Function*************************************************************
@@ -569,4 +572,3 @@ finalize:
 
 
 ABC_NAMESPACE_IMPL_END
-