Adding symbolic fault representation in &fftest.

1 files changed, 26 insertions, 17 deletions

diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index 9d24f9a6..c52b5033 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -345,8 +345,6 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars )
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
     assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + 4 * Gia_ManAndNum(p) );
-//    if ( fUseFaults )
-//        Gia_AigerWrite( pNew, "newfault.aig", 0, 0 );
     return pNew;
 }
 
@@ -418,6 +416,23 @@ int Gia_FormStrCount( char * pStr, int * pnVars, int * pnPars )
         { printf( "The number of parameters should be between 1 and %d\n", *pnPars ); return 1; }
     return 0;
 }
+void Gia_FormStrTransform( char * pStr, char * pForm )
+{
+    int i, k;
+    for ( k = i = 0; pForm[i]; i++ )
+    {
+        if ( pForm[i] == '~' )
+        {
+            i++;
+            assert( pForm[i] >= 'a' && pForm[i] <= 'z' );
+            pStr[k++] = 'A' + pForm[i] - 'a';
+        }
+        else
+            pStr[k++] = pForm[i];
+    }
+    pStr[k] = 0; 
+}   
+
 
 /**Function*************************************************************
 
@@ -497,31 +512,21 @@ int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * p
     iFans[2] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars );
     return Gia_ManHashMux( p, iFans[0], iFans[1], iFans[2] );
 }
-int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pForm, int nPars )
+int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pStr, int nPars )
 {
-    char pStr[100];  int i, k;
-    for ( k = i = 0; pForm[i]; i++ )
-    {
-        if ( pForm[i] == '~' )
-        {
-            i++;
-            assert( pForm[i] >= 'a' && pForm[i] <= 'z' );
-            pStr[k++] = 'A' + pForm[i] - 'a';
-        }
-        else
-            pStr[k++] = pForm[i];
-    }
-    pStr[k] = 0;   
     return Gia_ManRealizeFormula_rec( p, pVars, pPars, pStr, pStr + strlen(pStr), nPars );
 }
 Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, char * pForm )
 {
+    char pStr[100];
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
     int i, k, iCtrl[FFTEST_MAX_PARS], iFans[FFTEST_MAX_VARS];
     int nVars, nPars;
+    assert( strlen(pForm) < 100 );
     Gia_FormStrCount( pForm, &nVars, &nPars );
     assert( nVars == 2 );
+    Gia_FormStrTransform( pStr, pForm );
     pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
@@ -536,7 +541,7 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars,
         {
             iFans[0] = Gia_ObjFanin0Copy(pObj);
             iFans[1] = Gia_ObjFanin1Copy(pObj);
-            pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pForm, nPars );
+            pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars );
         }
         else
             pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -660,6 +665,8 @@ void Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Ve
     int i, Lit;
     // derive the cofactor
     pC = Gia_ManFaultCofactor( pM, vLits );
+//Gia_AigerWrite( pC, "fftest_cof.aig", 0, 0 );
+//printf( "Dumped cofactor circuit into file \"%s\".\n", "fftest_cof.aig" );
     // derive new CNF
     pCnf2 = Cnf_DeriveGiaRemapped( pC );
     Cnf_DataLiftGia( pCnf2, pC, sat_solver_nvars(pSat) );
@@ -877,6 +884,8 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
         p0 = Gia_ManFOFUnfold( p, 0, pPars->fComplVars );
         p1 = Gia_ManFOFUnfold( p, 1, pPars->fComplVars );
     }
+//    Gia_AigerWrite( p1, "newfault.aig", 0, 0 );
+//    printf( "Dumped circuit with fault parameters into file \"newfault.aig\".\n" );
 
     // create miter
     pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );