Dumping equivalences after SAT sweeping.

5 files changed, 172 insertions, 6 deletions

diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h
index c501d326..0365b946 100644
--- a/src/aig/miniaig/miniaig.h
+++ b/src/aig/miniaig/miniaig.h
@@ -368,6 +368,20 @@ static inline int Mini_AigTruth( Mini_Aig_t * p, int * pVarLits, int nVars, unsi
     Lit1 = Mini_AigTruth( p, pVarLits, Var, Mini_AigTt5Cofactor1(Truth, Var) );
     return Mini_AigMuxProp( p, pVarLits[Var], Lit1, Lit0 );
 }
+static char * Mini_AigPhase( Mini_Aig_t * p )
+{
+    char * pRes = MINI_AIG_CALLOC( char, Mini_AigNodeNum(p) );
+    int i;
+    Mini_AigForEachAnd( p, i )
+    {
+        int iFaninLit0 = Mini_AigNodeFanin0( p, i );
+        int iFaninLit1 = Mini_AigNodeFanin1( p, i );
+        int Phase0 = pRes[Mini_AigLit2Var(iFaninLit0)] ^ Mini_AigLitIsCompl(iFaninLit0);
+        int Phase1 = pRes[Mini_AigLit2Var(iFaninLit1)] ^ Mini_AigLitIsCompl(iFaninLit1);
+        pRes[i] = Phase0 & Phase1;
+    }
+    return pRes;
+}
 
 // procedure to check the topological order during AIG construction
 static int Mini_AigCheck( Mini_Aig_t * p )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f1c8cc7f..33a8315c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -37195,13 +37195,14 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
     extern Gia_Man_t * Cec3_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
     extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
+    extern void        Cec4_ManSimulateTest5( Gia_Man_t * p, int nConfs, int fVerbose );
     extern Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle );
     Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
-    int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0;
+    int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0, fUseSave = 0;
     int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500;
     Cec4_ManSetParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxywvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxyswvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -37331,6 +37332,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'y':
             fUseAlgoY ^= 1;
             break;
+        case 's':
+            fUseSave ^= 1;
+            break;
         case 'w':
             pPars->fVeryVerbose ^= 1;
             break;
@@ -37346,7 +37350,12 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Fraig(): There is no AIG.\n" );
         return 1;
     }
-    if ( fUseAlgo )
+    if ( fUseSave )
+    {
+        Cec4_ManSimulateTest5( pAbc->pGia, pPars->nBTLimit, pPars->fVerbose );
+        return 0;
+    }
+    else if ( fUseAlgo )
         pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars );
     else if ( fUseAlgoG )
         pTemp = Cec3_ManSimulateTest( pAbc->pGia, pPars );
@@ -37354,7 +37363,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         pTemp = Cec4_ManSimulateTest( pAbc->pGia, pPars );
     else if ( fUseAlgoY )
         pTemp = Cec5_ManSimulateTest( pAbc->pGia, pPars, fCbs, approxLim, subBatchSz, adaRecycle );
-    else
+    else 
         pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 );
     if ( pAbc->pGia->pCexSeq != NULL )
     {
@@ -37366,7 +37375,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fraig [-JWRILDCNP <num>] [-rmdckngxywvh]\n" );
+    Abc_Print( -2, "usage: &fraig [-JWRILDCNP <num>] [-rmdckngxyswvh]\n" );
     Abc_Print( -2, "\t         performs combinational SAT sweeping\n" );
     Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType );
     Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
@@ -37386,6 +37395,7 @@ usage:
     Abc_Print( -2, "\t-g     : toggle using another new implementation [default = %s]\n", fUseAlgoG? "yes": "no" );
     Abc_Print( -2, "\t-x     : toggle using another new implementation [default = %s]\n", fUseAlgoX? "yes": "no" );
     Abc_Print( -2, "\t-y     : toggle using another new implementation [default = %s]\n", fUseAlgoY? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle dumping equivalences into a file [default = %s]\n", fUseSave? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing even more verbose information [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");
diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h
index 8275702a..fdbb1866 100644
--- a/src/misc/vec/vecWrd.h
+++ b/src/misc/vec/vecWrd.h
@@ -195,6 +195,14 @@ static inline Vec_Wrd_t * Vec_WrdStartTruthTables( int nVars )
     }
     return p;
 }
+static inline int Vec_WrdShiftOne( Vec_Wrd_t * p, int nWords )
+{
+    int i, nObjs = p->nSize/nWords;
+    assert( nObjs * nWords == p->nSize );
+    for ( i = 0; i < nObjs; i++ )
+        p->pArray[i*nWords] <<= 1;
+    return nObjs;
+}
 
 /**Function*************************************************************
 
diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c
index 963ea15b..49d0a58f 100644
--- a/src/proof/acec/acecXor.c
+++ b/src/proof/acec/acecXor.c
@@ -466,6 +466,7 @@ void Gia_ManTestXor( Gia_Man_t * p )
     }
     Vec_WrdFree( vSimsPi );
     Vec_WrdFree( vSims );
+    nWords = 0;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index ce299c66..2bbc03d2 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -1877,9 +1877,9 @@ void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )
     abctime clk = Abc_Clock();
     Cec_ParFra_t ParsFra, * pPars = &ParsFra;
     Cec4_ManSetParams( pPars );
-    Cec4_ManPerformSweeping( p, pPars, NULL, 0 );
     pPars->fVerbose = fVerbose;
     pPars->nBTLimit = nConfs;
+    Cec4_ManPerformSweeping( p, pPars, NULL, 0 );
     if ( fVerbose )
         Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk );
 }
@@ -1912,6 +1912,139 @@ int Cec4_ManSimulateOnlyTest( Gia_Man_t * p, int fVerbose )
     return Cec4_ManPerformSweeping( p, pPars, NULL, 1 );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Internal simulation APIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec4_ManSimulateTest5Int( Gia_Man_t * p, int nConfs, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+    Cec4_ManSetParams( pPars );
+    pPars->fVerbose = fVerbose;
+    pPars->nBTLimit = nConfs;
+    Cec4_ManPerformSweeping( p, pPars, NULL, 0 );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Equivalence detection time", Abc_Clock() - clk );
+}
+Gia_Man_t * Gia_ManLocalRehash( Gia_Man_t * p )  
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    Gia_ManHashStop( pNew );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        int iLitNew = Gia_ManObj(pTemp, Abc_Lit2Var(pObj->Value))->Value;
+        if ( iLitNew == ~0 )
+            pObj->Value = iLitNew;
+        else
+            pObj->Value = Abc_LitNotCond(iLitNew, Abc_LitIsCompl(pObj->Value));
+    }
+    Gia_ManStop( pTemp );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+Vec_Int_t * Cec4_ManComputeMapping( Gia_Man_t * p, Gia_Man_t * pAig, int fVerbose )
+{
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vReprs = Vec_IntStartFull( Gia_ManObjNum(p) );
+    int * pAig2Abc = ABC_FALLOC( int, Gia_ManObjNum(pAig) );
+    int i, nConsts = 0, nReprs = 0;
+    pAig2Abc[0] = 0;
+    Gia_ManForEachCand( p, pObj, i )
+    {
+        int iLitGia = pObj->Value, iReprGia;
+        if ( iLitGia == -1 )
+            continue;
+        iReprGia = Gia_ObjReprSelf( pAig, Abc_Lit2Var(iLitGia) );
+        if ( pAig2Abc[iReprGia] == -1 )
+            pAig2Abc[iReprGia] = i;
+        else
+        {
+            int iLitGia2 = Gia_ManObj(p, pAig2Abc[iReprGia] )->Value;
+            assert( Gia_ObjReprSelf(pAig, Abc_Lit2Var(iLitGia)) == Gia_ObjReprSelf(pAig, Abc_Lit2Var(iLitGia2)) );
+            assert( i > pAig2Abc[iReprGia] );
+            Vec_IntWriteEntry( vReprs, i, pAig2Abc[iReprGia] );
+            if ( pAig2Abc[iReprGia] == 0 )
+                nConsts++;
+            else
+                nReprs++;
+        }
+    }
+    ABC_FREE( pAig2Abc );
+    if ( fVerbose )
+        printf( "Found %d const reprs and %d other reprs.\n", nConsts, nReprs );
+    return vReprs;
+}
+void Cec4_ManVerifyEquivs( Gia_Man_t * p, Vec_Int_t * vRes, int fVerbose )
+{
+    int i, iRepr, nWords = 4; word * pSim0, * pSim1;
+    Vec_Wrd_t * vSimsCi = Vec_WrdStartRandom( Gia_ManCiNum(p) * nWords );
+    int nObjs = Vec_WrdShiftOne( vSimsCi, nWords ), nFails = 0;
+    Vec_Wrd_t * vSims   = Gia_ManSimPatSimOut( p, vSimsCi, 0 );
+    assert( Vec_IntSize(vRes) == Gia_ManObjNum(p) );
+    assert( nObjs == Gia_ManCiNum(p) );
+    Vec_IntForEachEntry( vRes, iRepr, i )
+    {
+        if ( iRepr == -1 )
+            continue;
+        assert( i > iRepr );
+        pSim0 = Vec_WrdEntryP( vSims, nWords*i );
+        pSim1 = Vec_WrdEntryP( vSims, nWords*iRepr );
+        if ( (pSim0[0] ^ pSim1[0]) & 1 )
+            nFails += !Abc_TtOpposite(pSim0, pSim1, nWords);
+        else
+            nFails += !Abc_TtEqual(pSim0, pSim1, nWords);
+    }
+    Vec_WrdFree( vSimsCi );
+    Vec_WrdFree( vSims );
+    if ( nFails )
+        printf( "Verification failed at %d nodes.\n", nFails );
+    else if ( fVerbose )
+        printf( "Verification succeeded for all (%d) nodes.\n", Gia_ManCandNum(p) );
+}
+void Cec4_ManConvertToLits( Gia_Man_t * p, Vec_Int_t * vRes )
+{
+    Gia_Obj_t * pObj; int i, iRepr;
+    Gia_ManSetPhase( p );
+    Gia_ManForEachObj( p, pObj, i )
+        if ( (iRepr = Vec_IntEntry(vRes, i)) >= 0 )
+            Vec_IntWriteEntry( vRes, i, Abc_Var2Lit(iRepr, Gia_ManObj(p, iRepr)->fPhase ^ pObj->fPhase) );
+}
+void Cec4_ManSimulateTest5( Gia_Man_t * p, int nConfs, int fVerbose )
+{
+    Vec_Int_t * vRes = NULL;
+    Gia_Man_t * pAig = Gia_ManLocalRehash( p );
+    Cec4_ManSimulateTest5Int( pAig, nConfs, fVerbose );
+    vRes = Cec4_ManComputeMapping( p, pAig, fVerbose );
+    Cec4_ManVerifyEquivs( p, vRes, fVerbose );
+    Cec4_ManConvertToLits( p, vRes );
+    Vec_IntDumpBin( "_temp_.equiv", vRes, fVerbose );
+    Vec_IntFree( vRes );
+    Gia_ManStop( pAig );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////