summaryrefslogtreecommitdiffstats
path: root/src/proof/ssw/sswFilter.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/ssw/sswFilter.c')
-rw-r--r--src/proof/ssw/sswFilter.c47
1 files changed, 23 insertions, 24 deletions
diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c
index 047e2201..534fc275 100644
--- a/src/proof/ssw/sswFilter.c
+++ b/src/proof/ssw/sswFilter.c
@@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames )
-{
+{
Aig_Obj_t * pObj, * pObjLi;
int f, i, RetValue1, RetValue2;
assert( nFrames > 0 );
@@ -87,14 +87,14 @@ void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames )
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
-
+
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames )
-{
+{
Aig_Obj_t * pObj, * pObjLi;
int f, i;
assert( nFrames > 0 );
@@ -129,14 +129,14 @@ void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames )
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
-
+
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
-{
+{
Aig_Obj_t * pObj, * pObjLi;
int f, i, iBit;
// assign register outputs
@@ -164,7 +164,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
// check that the output failed as expected -- cannot check because it is not an SRM!
// pObj = Aig_ManCo( p->pAig, pCex->iPo );
// if ( pObj->fMarkB != 1 )
-// printf( "The counter-example does not refine the output.\n" );
+// Abc_Print( 1, "The counter-example does not refine the output.\n" );
// record the new pattern
Saig_ManForEachLo( p->pAig, pObj, i )
if ( pObj->fMarkB ^ Abc_InfoHasBit(p->pPatWords, Saig_ManPiNum(p->pAig) + i) )
@@ -183,7 +183,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
***********************************************************************/
int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
-{
+{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue;
// get representative of this class
@@ -199,7 +199,7 @@ int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) );
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
- return 0;
+ return 0;
// call equivalence checking
if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
@@ -222,7 +222,7 @@ int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
{
- printf( "Ssw_ManSweepNodeFilter(): Failed to refine representative.\n" );
+ Abc_Print( 1, "Ssw_ManSweepNodeFilter(): Failed to refine representative.\n" );
}
return 0;
}
@@ -287,15 +287,15 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
if ( Abc_InfoHasBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i ) )
{
Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst1(p->pFrames) );
-//printf( "1" );
+//Abc_Print( 1, "1" );
}
else
{
Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );
-//printf( "0" );
+//Abc_Print( 1, "0" );
}
}
-//printf( "\n" );
+//Abc_Print( 1, "\n" );
// sweep internal nodes
for ( f = 0; f < p->pPars->nFramesK; f++ )
@@ -332,20 +332,20 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
// printout
if ( p->pPars->fVerbose )
{
- printf( "Frame %4d : ", f );
+ Abc_Print( 1, "Frame %4d : ", f );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
if ( i < Vec_PtrSize(p->pAig->vObjs) )
{
if ( p->pPars->fVerbose )
- printf( "Exceeded the resource limits (%d conflicts). Quitting...\n", p->pPars->nBTLimit );
+ Abc_Print( 1, "Exceeded the resource limits (%d conflicts). Quitting...\n", p->pPars->nBTLimit );
break;
- }
+ }
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
{
if ( p->pPars->fVerbose )
- printf( "Exceeded the time frame limit (%d time frames). Quitting...\n", p->pPars->nFramesK );
+ Abc_Print( 1, "Exceeded the time frame limit (%d time frames). Quitting...\n", p->pPars->nFramesK );
break;
}
// check timeout
@@ -371,9 +371,9 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
Synopsis [Filter equivalence classes of nodes.]
- Description [Unrolls at most nFramesMax frames. Works with nConfMax
+ Description [Unrolls at most nFramesMax frames. Works with nConfMax
conflicts until the first undefined SAT call. Verbose prints the message.]
-
+
SideEffects []
SeeAlso []
@@ -415,18 +415,18 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
for ( r = 0; r < nRounds; r++ )
{
if ( p->pPars->fVerbose )
- printf( "Round %3d:\n", r );
+ Abc_Print( 1, "Round %3d:\n", r );
// start filtering equivalence classes
Ssw_ManRefineByFilterSim( p, p->pPars->nFramesK );
if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
{
- printf( "All equivalences are refined away.\n" );
+ Abc_Print( 1, "All equivalences are refined away.\n" );
break;
}
// printout
if ( p->pPars->fVerbose )
{
- printf( "Initial : " );
+ Abc_Print( 1, "Initial : " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
p->pMSat = Ssw_SatStart( 0 );
@@ -447,7 +447,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
// check timeout
if ( TimeLimit && clock() > nTimeToStop )
{
- printf( "Reached timeout (%d seconds).\n", TimeLimit );
+ Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeLimit );
break;
}
}
@@ -471,7 +471,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
***********************************************************************/
void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
-{
+{
Aig_Man_t * pAig;
pAig = Gia_ManToAigSimple( p );
if ( p->pReprs != NULL )
@@ -491,4 +491,3 @@ void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRoun
ABC_NAMESPACE_IMPL_END
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-27 15:26:52 +0000