Added transformation of CEX after 'fix_aig' and checking of transformed CEXes using 'testcex -a'.

2 files changed, 40 insertions, 0 deletions

diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 08a56317..3acd7f77 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -436,6 +436,45 @@ Abc_Cex_t * Abc_CexTransformTempor( Abc_Cex_t * p, int nPisOld, int nPosOld, int
 
 /**Function*************************************************************
 
+  Synopsis    [Transform CEX after "logic; undc; st; zero".]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Abc_CexTransformUndc( Abc_Cex_t * p, char * pInit )
+{
+    Abc_Cex_t * pCex;
+    int nFlops = strlen(pInit);
+    int i, f, iBit, iAddPi = 0, nAddPis = 0;
+    // count how many flops got a new PI
+    for ( i = 0; i < nFlops; i++ )
+        nAddPis += (int)(pInit[i] == 'x');
+    // create new CEX
+    pCex = Abc_CexAlloc( nFlops, p->nPis - nAddPis, p->iFrame + 1 );
+    pCex->iPo    = p->iPo;
+    pCex->iFrame = p->iFrame;
+    for ( iBit = 0; iBit < nFlops; iBit++ )
+    {
+        if ( pInit[iBit] == '1' || (pInit[iBit] == 'x' && Abc_InfoHasBit(p->pData, p->nRegs + p->nPis - nAddPis + iAddPi)) )
+            Abc_InfoSetBit( pCex->pData, iBit );
+        iAddPi += (int)(pInit[iBit] == 'x');
+    }
+    assert( iAddPi == nAddPis );
+    // add timeframes
+    for ( f = 0; f <= p->iFrame; f++ )
+        for ( i = 0; i < pCex->nPis; i++, iBit++ )
+            if ( Abc_InfoHasBit(p->pData, p->nRegs + p->nPis * f + i) )
+                Abc_InfoSetBit( pCex->pData, iBit );
+    assert( iBit == pCex->nBits );
+    return pCex;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives permuted CEX using permutation of its inputs.]
 
   Description []
diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h
index c6904a60..4163a1fe 100644
--- a/src/misc/util/utilCex.h
+++ b/src/misc/util/utilCex.h
@@ -70,6 +70,7 @@ extern void          Abc_CexFreeP( Abc_Cex_t ** p );
 extern void          Abc_CexFree( Abc_Cex_t * p );
 extern Abc_Cex_t *   Abc_CexTransformPhase( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld );
 extern Abc_Cex_t *   Abc_CexTransformTempor( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld );
+extern Abc_Cex_t *   Abc_CexTransformUndc( Abc_Cex_t * p, char * pInit );
 extern Abc_Cex_t *   Abc_CexPermute( Abc_Cex_t * p, Vec_Int_t * vMapOld2New );
 extern Abc_Cex_t *   Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t * vPermNew );
 extern int           Abc_CexCountOnes( Abc_Cex_t * p );