Fixing the problem with 'phase -c'.

5 files changed, 64 insertions, 4 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 62b7c89a..052966f7 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -963,6 +963,7 @@ extern Gia_Man_t *         Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
 /*=== giaCex.c ============================================================*/
 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, int nOutputs );
+extern int                 Gia_ManSetFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p );
 extern void                Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex );
 extern void                Gia_ManCounterExampleValueStop( Gia_Man_t * pGia );
 extern int                 Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame );
diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c
index fdc0c709..5a8125f3 100644
--- a/src/aig/gia/giaCex.c
+++ b/src/aig/gia/giaCex.c
@@ -121,6 +121,53 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Determines the failed PO when its exact frame is not known.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManSetFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p )
+{
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int i, k, iBit = 0;
+    assert( Gia_ManPiNum(pAig) == p->nPis );
+    Gia_ManCleanMark0(pAig);
+    p->iPo = -1;
+//    Gia_ManForEachRo( pAig, pObj, i )
+//       pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+    iBit = p->nRegs;
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Gia_ManForEachPi( pAig, pObj, k )
+            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+        Gia_ManForEachAnd( pAig, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( pAig, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMark0 = pObjRi->fMark0;
+        // check the POs
+        Gia_ManForEachPo( pAig, pObj, k )
+        {
+            if ( !pObj->fMark0 )
+                continue;
+            p->iPo = k;
+            p->iFrame = i;
+            p->nBits = iBit;
+            break;
+        }
+    }
+    Gia_ManCleanMark0(pAig);
+    return p->iPo;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bdf57e55..1cdd493a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -18864,6 +18864,18 @@ int Abc_CommandDarPhase( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         pCexNew = Abc_CexTransformPhase( pAbc->pCex, Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkLatchNum(pNtk) );
+        {
+            Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+            Gia_Man_t * pGia = Gia_ManFromAig( pAig );
+            int iPo = Gia_ManSetFailedPoCex( pGia, pCexNew );
+            Gia_ManStop( pGia );
+            Aig_ManStop( pAig );
+            if ( iPo == -1 )
+            {
+                Abc_Print( -1, "The counter-example does not fail any of the outputs of the original AIG.\n" );
+                return 1;
+            }
+        }
         Abc_FrameReplaceCex( pAbc, &pCexNew );
         return 0;
     }
diff --git a/src/misc/extra/extraUtilSupp.c b/src/misc/extra/extraUtilSupp.c
index 3cb0296e..c42a35f6 100644
--- a/src/misc/extra/extraUtilSupp.c
+++ b/src/misc/extra/extraUtilSupp.c
@@ -648,7 +648,7 @@ void Abc_SuppReadMinTest( char * pFileName )
 {
     int fVerbose = 0;
     abctime clk = Abc_Clock();
-    word Matrix[64];
+//    word Matrix[64];
     int nVars, nVarsMin;
     Vec_Wrd_t * vPairs, * vCubes;
     vCubes = Abc_SuppReadMin( pFileName, &nVars );
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 2f2901e0..08a56317 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -396,9 +396,9 @@ Abc_Cex_t * Abc_CexTransformPhase( Abc_Cex_t * p, int nPisOld, int nPosOld, int
     assert( p->iPo < nPosNew );
     pCex = Abc_CexDup( p, nRegsOld );
     pCex->nPis   = nPisOld;
-    pCex->iPo    = p->iPo % nPosOld;
-    pCex->iFrame = p->iFrame * nFrames + p->iPo / nPosOld;
-    pCex->nBits  = pCex->nRegs + pCex->nPis * (pCex->iFrame + 1);
+    pCex->iPo    = -1;
+    pCex->iFrame = (p->iFrame + 1) * nFrames - 1;
+    pCex->nBits  = p->nBits;
     return pCex;
 }