1 files changed, 84 insertions, 2 deletions

diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index 28d8a0c1..93728660 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -614,10 +614,9 @@ void Gia_FormStrTransform( char * pStr, char * pForm )
     pStr[k] = 0; 
 }   
 
-
 /**Function*************************************************************
 
-  Synopsis    [Implements fault model formula using functional/parameter vars.]
+  Synopsis    [Print formula.]
 
   Description []
                
@@ -643,6 +642,88 @@ char * Gia_ManFormulaEndToken( char * pForm )
     assert( 0 );
     return NULL;
 }
+void Gia_ManPrintFormula_rec( char * pBeg, char * pEnd )
+{
+    int Oper = -1;
+    char * pEndNew;
+    if ( pBeg + 1 == pEnd )
+    {
+        if ( pBeg[0] >= 'a' && pBeg[0] <= 'b' )
+            printf( "%c", pBeg[0] );
+        else if ( pBeg[0] >= 'A' && pBeg[0] <= 'B' )
+            printf( "~%c", pBeg[0]-'A'+'a' );
+        else if ( pBeg[0] >= 'p' && pBeg[0] <= 'w' ) // pqrstuvw
+            printf( "%c", pBeg[0] );
+        else if ( pBeg[0] >= 'P' && pBeg[0] <= 'W' )
+            printf( "~%c", pBeg[0]-'A'+'a' );
+        return;
+    }
+    if ( pBeg[0] == '(' )
+    {
+        pEndNew = Gia_ManFormulaEndToken( pBeg );
+        if ( pEndNew == pEnd )
+        {
+            assert( pBeg[0] == '(' );
+            assert( pBeg[pEnd-pBeg-1] == ')' );
+            Gia_ManPrintFormula_rec( pBeg + 1, pEnd - 1 );
+            return;
+        }
+    }
+    // get first part
+    pEndNew  = Gia_ManFormulaEndToken( pBeg );
+    printf( "(" );
+    Gia_ManPrintFormula_rec( pBeg, pEndNew );
+    printf( ")" );
+    Oper     = pEndNew[0];
+    // derive the formula
+    if ( Oper == '&' )
+        printf( "&" );
+    else if ( Oper == '|' )
+        printf( "|" );
+    else if ( Oper == '^' )
+        printf( "^" );
+    else if ( Oper == '?' )
+        printf( "?" );
+    else assert( 0 );
+    // get second part
+    pBeg     = pEndNew + 1;
+    pEndNew  = Gia_ManFormulaEndToken( pBeg );
+    printf( "(" );
+    Gia_ManPrintFormula_rec( pBeg, pEndNew );
+    printf( ")" );
+    if ( Oper == '?' )
+    {
+        printf( ":" );
+        // get third part
+        assert( Oper == '?' );
+        assert( pEndNew[0] == ':' );
+        pBeg     = pEndNew + 1;
+        pEndNew  = Gia_ManFormulaEndToken( pBeg );
+        printf( "(" );
+        Gia_ManPrintFormula_rec( pBeg, pEndNew );
+        printf( ")" );
+    }
+}
+void Gia_ManPrintFormula( char * pStr )
+{
+    printf( "Using formula: " );
+    printf( "(" );
+    Gia_ManPrintFormula_rec( pStr, pStr + strlen(pStr) );
+    printf( ")" );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements fault model formula using functional/parameter vars.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * pBeg, char * pEnd, int nPars )
 {
     int iFans[3], Oper = -1;
@@ -709,6 +790,7 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm, int fFfOnly )
     Gia_FormStrCount( pForm, &nVars, &nPars );
     assert( nVars == 2 );
     Gia_FormStrTransform( pStr, pForm );
+    Gia_ManPrintFormula( pStr );
     pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );