summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bmc')
-rw-r--r--src/sat/bmc/bmcFault.c86
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 );