summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--src/aig/gia/giaEquiv.c177
-rw-r--r--src/aig/saig/saigStrSim.c95
-rw-r--r--src/proof/pdr/pdrTsim.c46
-rw-r--r--src/proof/ssw/sswAig.c17
-rw-r--r--src/proof/ssw/sswBmc.c17
-rw-r--r--src/proof/ssw/sswClass.c91
-rw-r--r--src/proof/ssw/sswCnf.c27
-rw-r--r--src/proof/ssw/sswConstr.c69
-rw-r--r--src/proof/ssw/sswCore.c71
-rw-r--r--src/proof/ssw/sswDyn.c33
-rw-r--r--src/proof/ssw/sswFilter.c47
-rw-r--r--src/proof/ssw/sswIslands.c43
-rw-r--r--src/proof/ssw/sswLcorr.c25
-rw-r--r--src/proof/ssw/sswMan.c37
-rw-r--r--src/proof/ssw/sswPairs.c65
-rw-r--r--src/proof/ssw/sswPart.c9
-rw-r--r--src/proof/ssw/sswRarity.c183
-rw-r--r--src/proof/ssw/sswRarity2.c63
-rw-r--r--src/proof/ssw/sswSemi.c45
-rw-r--r--src/proof/ssw/sswSim.c139
-rw-r--r--src/proof/ssw/sswSimSat.c11
-rw-r--r--src/proof/ssw/sswSweep.c23
-rw-r--r--src/proof/ssw/sswUnique.c15
24 files changed, 680 insertions, 670 deletions
diff --git a/Makefile b/Makefile
index c69602f1..e3ebbd8b 100644
--- a/Makefile
+++ b/Makefile
@@ -86,7 +86,7 @@ clean:
@rm -rvf $(PROG) lib$(PROG).a $(OBJ) $(GARBAGE) $(OBJ:.o=.d)
tags:
- ctags -R .
+ etags `find . -type f -regex '.*\.\(c\|h\)'`
$(PROG): $(OBJ)
@echo "\`\` Building binary:" $(notdir $@)
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 2cbdb75f..9454fa8e 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -200,7 +200,7 @@ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
{
int nLitsReal = Gia_ManEquivCountLitsAll( p );
if ( nLitsReal != nLits )
- printf( "Detected a mismatch in counting equivalence classes (%d).\n", nLitsReal - nLits );
+ Abc_Print( 1, "Detected a mismatch in counting equivalence classes (%d).\n", nLitsReal - nLits );
return 1;
}
@@ -232,10 +232,10 @@ void Gia_ManPrintStatsClasses( Gia_Man_t * p )
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
-// printf( "i/o/ff =%5d/%5d/%5d ", Gia_ManPiNum(p), Gia_ManPoNum(p), Gia_ManRegNum(p) );
-// printf( "and =%5d ", Gia_ManAndNum(p) );
-// printf( "lev =%3d ", Gia_ManLevelNum(p) );
- printf( "cst =%3d cls =%6d lit =%8d\n", Counter0, Counter, nLits );
+// Abc_Print( 1, "i/o/ff =%5d/%5d/%5d ", Gia_ManPiNum(p), Gia_ManPoNum(p), Gia_ManRegNum(p) );
+// Abc_Print( 1, "and =%5d ", Gia_ManAndNum(p) );
+// Abc_Print( 1, "lev =%3d ", Gia_ManLevelNum(p) );
+ Abc_Print( 1, "cst =%3d cls =%6d lit =%8d\n", Counter0, Counter, nLits );
}
/**Function*************************************************************
@@ -291,14 +291,14 @@ int Gia_ManEquivCountOne( Gia_Man_t * p, int i )
void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter )
{
int Ent;
- printf( "Class %4d : Num = %2d {", Counter, Gia_ManEquivCountOne(p, i) );
+ Abc_Print( 1, "Class %4d : Num = %2d {", Counter, Gia_ManEquivCountOne(p, i) );
Gia_ClassForEachObj( p, i, Ent )
{
- printf(" %d", Ent );
+ Abc_Print( 1," %d", Ent );
if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB )
- printf(" <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB );
+ Abc_Print( 1," <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB );
}
- printf( " }\n" );
+ Abc_Print( 1, " }\n" );
}
void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
{
@@ -316,16 +316,16 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
}
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
- printf( "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f MB\n",
+ Abc_Print( 1, "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f MB\n",
Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
assert( Gia_ManEquivCheckLits( p, nLits ) );
if ( fVerbose )
{
// int Ent;
- printf( "Const0 = " );
+ Abc_Print( 1, "Const0 = " );
Gia_ManForEachConst( p, i )
- printf( "%d ", i );
- printf( "\n" );
+ Abc_Print( 1, "%d ", i );
+ Abc_Print( 1, "\n" );
Counter = 0;
Gia_ManForEachClass( p, i )
Gia_ManEquivPrintOne( p, i, ++Counter );
@@ -334,12 +334,12 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
Gia_ManForEachClass( p, i )
if ( i % 100 == 0 )
{
-// printf( "%d ", Gia_ManEquivCountOne(p, i) );
+// Abc_Print( 1, "%d ", Gia_ManEquivCountOne(p, i) );
Gia_ClassForEachObj( p, i, Ent )
{
- printf( "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) );
+ Abc_Print( 1, "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) );
}
- printf( "\n" );
+ Abc_Print( 1, "\n" );
}
*/
}
@@ -362,7 +362,7 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int
{
if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID )
return NULL;
- }
+ }
else
{
if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
@@ -420,27 +420,27 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
int i;
if ( !p->pReprs )
{
- printf( "Gia_ManEquivReduce(): Equivalence classes are not available.\n" );
+ Abc_Print( 1, "Gia_ManEquivReduce(): Equivalence classes are not available.\n" );
return NULL;
}
if ( fDualOut && (Gia_ManPoNum(p) & 1) )
{
- printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
+ Abc_Print( 1, "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
return NULL;
- }
+ }
// check if there are any equivalences defined
Gia_ManForEachObj( p, pObj, i )
if ( Gia_ObjReprObj(p, i) != NULL )
break;
if ( i == Gia_ManObjNum(p) )
{
-// printf( "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" );
+// Abc_Print( 1, "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" );
return NULL;
}
/*
if ( !Gia_ManCheckTopoOrder( p ) )
{
- printf( "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" );
+ Abc_Print( 1, "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" );
return NULL;
}
*/
@@ -479,7 +479,7 @@ void Gia_ManEquivFixOutputPairs( Gia_Man_t * p )
{
Gia_Obj_t * pObj0, * pObj1;
int i;
- assert( (Gia_ManPoNum(p) & 1) == 0 );
+ assert( (Gia_ManPoNum(p) & 1) == 0 );
Gia_ManForEachPo( p, pObj0, i )
{
pObj1 = Gia_ManPo( p, ++i );
@@ -497,7 +497,7 @@ void Gia_ManEquivFixOutputPairs( Gia_Man_t * p )
Synopsis [Removes pointers to the unmarked nodes..]
Description []
-
+
SideEffects []
SeeAlso []
@@ -522,7 +522,7 @@ void Gia_ManEquivUpdatePointers( Gia_Man_t * p, Gia_Man_t * pNew )
Synopsis [Removes pointers to the unmarked nodes..]
Description []
-
+
SideEffects []
SeeAlso []
@@ -581,7 +581,7 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
Synopsis [Removes pointers to the unmarked nodes..]
Description []
-
+
SideEffects []
SeeAlso []
@@ -627,7 +627,7 @@ Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
Synopsis [Reduces AIG while remapping equivalence classes.]
Description [Drops the pairs of outputs if they are proved equivalent.]
-
+
SideEffects []
SeeAlso []
@@ -705,8 +705,8 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
nDiffs[1] = Gia_ManCandNum(p) - nNodes[1];
if ( fVerbose )
{
- printf( "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n",
- Gia_ManCandNum(p), nNodes[0], nNodes[1], nDiffs[0], nDiffs[1],
+ Abc_Print( 1, "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n",
+ Gia_ManCandNum(p), nNodes[0], nNodes[1], nDiffs[0], nDiffs[1],
Gia_ManCandNum(p) - nDiffs[0] - nDiffs[1] );
}
return (nDiffs[0] + nDiffs[1]) / 2;
@@ -736,14 +736,14 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
iLitNew = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
{
- if ( vTrace )
+ if ( vTrace )
Vec_IntPush( vTrace, 1 );
if ( vGuide == NULL || Vec_IntEntry( vGuide, Vec_IntSize(vTrace)-1 ) )
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
}
else
{
- if ( vTrace )
+ if ( vTrace )
Vec_IntPush( vTrace, 0 );
}
if ( fSpeculate )
@@ -814,7 +814,7 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
int i, iLitNew;
if ( !p->pReprs )
{
- printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
+ Abc_Print( 1, "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
return NULL;
}
Vec_IntClear( vTrace );
@@ -838,7 +838,7 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
Gia_ManAppendCo( pNew, iLitNew );
if ( Vec_IntSize(vXorLits) == 0 )
{
- printf( "Speculatively reduced model has no primary outputs.\n" );
+ Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
Gia_ManAppendCo( pNew, 0 );
}
Gia_ManForEachRi( p, pObj, i )
@@ -871,12 +871,12 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
Vec_Int_t * vTrace = NULL, * vGuide = NULL;
if ( !p->pReprs )
{
- printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
+ Abc_Print( 1, "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
return NULL;
}
if ( fDualOut && (Gia_ManPoNum(p) & 1) )
{
- printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
+ Abc_Print( 1, "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
return NULL;
}
if ( fSkipSome )
@@ -912,7 +912,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
Gia_ManAppendCo( pNew, iLitNew );
if ( Vec_IntSize(vXorLits) == 0 )
{
- printf( "Speculatively reduced model has no primary outputs.\n" );
+ Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
Gia_ManAppendCo( pNew, 0 );
}
Gia_ManForEachRi( p, pObj, i )
@@ -944,7 +944,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
Synopsis [Duplicates the AIG in the DFS order.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1007,29 +1007,29 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames
int f, i, iLitNew;
if ( !p->pReprs )
{
- printf( "Gia_ManSpecReduceInit(): Equivalence classes are not available.\n" );
+ Abc_Print( 1, "Gia_ManSpecReduceInit(): Equivalence classes are not available.\n" );
return NULL;
}
if ( Gia_ManRegNum(p) == 0 )
{
- printf( "Gia_ManSpecReduceInit(): Circuit is not sequential.\n" );
+ Abc_Print( 1, "Gia_ManSpecReduceInit(): Circuit is not sequential.\n" );
return NULL;
}
if ( Gia_ManRegNum(p) != pInit->nRegs )
{
- printf( "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" );
+ Abc_Print( 1, "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" );
return NULL;
}
if ( fDualOut && (Gia_ManPoNum(p) & 1) )
{
- printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
+ Abc_Print( 1, "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
return NULL;
}
/*
if ( !Gia_ManCheckTopoOrder( p ) )
{
- printf( "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" );
+ Abc_Print( 1, "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" );
return NULL;
}
*/
@@ -1066,7 +1066,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames
Gia_ManAppendCo( pNew, iLitNew );
if ( Vec_IntSize(vXorLits) == 0 )
{
-// printf( "Speculatively reduced model has no primary outputs.\n" );
+// Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
Gia_ManAppendCo( pNew, 0 );
}
ABC_FREE( p->pCopies );
@@ -1097,7 +1097,7 @@ Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int n
for ( f = 1; ; f++ )
{
pFrames = Gia_ManSpecReduceInit( p, pInit, f, fDualOut );
- if ( (nMinOutputs == 0 && Gia_ManPoNum(pFrames) >= nLits/2+1) ||
+ if ( (nMinOutputs == 0 && Gia_ManPoNum(pFrames) >= nLits/2+1) ||
(nMinOutputs != 0 && Gia_ManPoNum(pFrames) >= nMinOutputs) )
break;
if ( f == nFramesMax )
@@ -1111,7 +1111,7 @@ Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int n
pFrames = NULL;
}
if ( f == nFramesMax )
- printf( "Stopped unrolling after %d frames.\n", nFramesMax );
+ Abc_Print( 1, "Stopped unrolling after %d frames.\n", nFramesMax );
if ( pnFrames )
*pnFrames = f;
return pFrames;
@@ -1174,7 +1174,7 @@ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
Vec_IntFree( vClass );
Vec_IntFree( vClassNew );
if ( fVerbose )
- printf( "Removed classes = %6d (out of %6d). Removed literals = %6d (out of %6d).\n",
+ Abc_Print( 1, "Removed classes = %6d (out of %6d). Removed literals = %6d (out of %6d).\n",
nRemovedClas, nTotalClas, nRemovedLits, nTotalLits );
}
@@ -1198,14 +1198,14 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
nLitsAll = Gia_ManEquivCountLitsAll( p );
if ( nLitsAll == 0 )
{
- printf( "Gia_ManEquivMark(): Current AIG does not have equivalences.\n" );
+ Abc_Print( 1, "Gia_ManEquivMark(): Current AIG does not have equivalences.\n" );
return;
}
// read AIGER file
pMiter = Gia_ReadAiger( pFileName, 0, 0 );
if ( pMiter == NULL )
{
- printf( "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
+ Abc_Print( 1, "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
return;
}
if ( fSkipSome )
@@ -1222,7 +1222,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
// check the number
if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nAddPos )
{
- printf( "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGFilteredEquivNum(%d).\n",
+ Abc_Print( 1, "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGFilteredEquivNum(%d).\n",
Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nAddPos );
Gia_ManStop( pMiter );
Vec_IntFreeP( &vTrace );
@@ -1251,7 +1251,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
{
if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nLitsAll )
{
- printf( "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n",
+ Abc_Print( 1, "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n",
Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nLitsAll );
Gia_ManStop( pMiter );
return;
@@ -1272,7 +1272,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
assert( nLits == nLitsAll );
}
if ( fVerbose )
- printf( "Set %d equivalences as proved.\n", Counter );
+ Abc_Print( 1, "Set %d equivalences as proved.\n", Counter );
Gia_ManStop( pMiter );
}
@@ -1319,7 +1319,7 @@ void Gia_ManEquivImprove( Gia_Man_t * p )
if ( i == iReprBest )
continue;
/*
- printf( "Repr/Best = %6d/%6d. Lev = %3d/%3d. Mffc = %3d/%3d.\n",
+ Abc_Print( 1, "Repr/Best = %6d/%6d. Lev = %3d/%3d. Mffc = %3d/%3d.\n",
i, iReprBest, Gia_ObjLevel( p,Gia_ManObj(p, i) ), Gia_ObjLevel( p,Gia_ManObj(p, iReprBest) ),
Gia_NodeMffcSize( p, Gia_ManObj(p, i) ), Gia_NodeMffcSize( p, Gia_ManObj(p, iReprBest) ) );
*/
@@ -1405,7 +1405,7 @@ int Gia_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
Synopsis [Adds the next entry while making choices.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1426,7 +1426,7 @@ void Gia_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode
Synopsis [Duplicates the AIG in the DFS order.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1471,7 +1471,7 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
{
assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
- Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew );
+ Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew );
}
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
@@ -1516,18 +1516,18 @@ void Gia_ManRemoveBadChoices( Gia_Man_t * p )
{
if ( !Gia_ManObj(p, iObj)->fMark0 )
{
- iPrev = iObj;
+ iPrev = iObj;
continue;
}
Gia_ObjSetRepr( p, iObj, GIA_VOID );
Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
Gia_ObjSetNext( p, iObj, 0 );
Counter++;
- }
+ }
}
// remove the marks
Gia_ManCleanMark0( p );
-// printf( "Removed %d bad choices.\n", Counter );
+// Abc_Print( 1, "Removed %d bad choices.\n", Counter );
}
/**Function*************************************************************
@@ -1660,7 +1660,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
int nIter, nStart = 0;
if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
{
- printf( "Gia_CommandSpecI(): Equivalence classes are not defined.\n" );
+ Abc_Print( 1, "Gia_CommandSpecI(): Equivalence classes are not defined.\n" );
return 0;
}
// (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
@@ -1670,12 +1670,12 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
{
if ( Gia_ManHasNoEquivs(pGia) )
{
- printf( "Gia_CommandSpecI: No equivalences left.\n" );
+ Abc_Print( 1, "Gia_CommandSpecI: No equivalences left.\n" );
break;
}
- printf( "ITER %3d : ", nIter );
+ Abc_Print( 1, "ITER %3d : ", nIter );
// if ( fVerbose )
-// printf( "Starting BMC from frame %d.\n", nStart );
+// Abc_Print( 1, "Starting BMC from frame %d.\n", nStart );
// if ( fVerbose )
// Gia_ManPrintStats( pGia, 0 );
Gia_ManPrintStatsClasses( pGia );
@@ -1683,10 +1683,10 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
// if ( Gia_ManPoNum(pSrm) <= Gia_ManPoNum(pGia) )
if ( !Cec_ManCheckNonTrivialCands(pGia) )
{
- printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
+ Abc_Print( 1, "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
break;
}
- pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
+ pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
// bmc2 -F 100 -C 25000
{
Abc_Cex_t * pCex;
@@ -1702,10 +1702,10 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
Aig_ManStop( pTemp );
if ( pCex == NULL )
{
- printf( "Gia_CommandSpecI(): Internal BMC could not find a counter-example.\n" );
+ Abc_Print( 1, "Gia_CommandSpecI(): Internal BMC could not find a counter-example.\n" );
break;
}
- if ( fStart )
+ if ( fStart )
nStart = pCex->iFrame;
// perform simulation
{
@@ -1719,7 +1719,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
}
ABC_FREE( pCex );
}
- }
+ }
// write equivalence classes
Gia_WriteAiger( pGia, "gore.aig", 0, 0 );
// reduce the model
@@ -1729,7 +1729,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
Gia_ManStop( pAux );
Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
-// printf( "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
+// Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
// Gia_ManPrintStatsShort( pReduce );
Gia_ManStop( pReduce );
}
@@ -1758,20 +1758,20 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
int i, iObj, iNext, Counter = 0;
if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
{
- printf( "Equivalences are not defined.\n" );
+ Abc_Print( 1, "Equivalences are not defined.\n" );
return 0;
}
pGia1 = Gia_ReadAiger( pName1, 0, 0 );
if ( pGia1 == NULL )
{
- printf( "Cannot read first file %s.\n", pName1 );
+ Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
return 0;
}
pGia2 = Gia_ReadAiger( pName2, 0, 0 );
if ( pGia2 == NULL )
{
Gia_ManStop( pGia2 );
- printf( "Cannot read second file %s.\n", pName2 );
+ Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
return 0;
}
pMiter = Gia_ManMiter( pGia1, pGia2, 0, 1, 0 );
@@ -1779,7 +1779,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
{
Gia_ManStop( pGia1 );
Gia_ManStop( pGia2 );
- printf( "Cannot create sequential miter.\n" );
+ Abc_Print( 1, "Cannot create sequential miter.\n" );
return 0;
}
// make sure the miter is isomorphic
@@ -1788,7 +1788,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
Gia_ManStop( pGia1 );
Gia_ManStop( pGia2 );
Gia_ManStop( pMiter );
- printf( "The number of objects in different.\n" );
+ Abc_Print( 1, "The number of objects in different.\n" );
return 0;
}
if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) )
@@ -1796,7 +1796,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
Gia_ManStop( pGia1 );
Gia_ManStop( pGia2 );
Gia_ManStop( pMiter );
- printf( "The AIG structure of the miter does not match.\n" );
+ Abc_Print( 1, "The AIG structure of the miter does not match.\n" );
return 0;
}
// transfer copies
@@ -1846,7 +1846,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
}
}
// undo equivalence classes
- for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
+ for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
{
Gia_ObjUnsetRepr( pGia, iObj );
@@ -1868,7 +1868,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
assert( Gia_ObjIsHead(pGia, ClassA) );
}
}
- printf( "The number of two-node classes after filtering = %d.\n", Counter );
+ Abc_Print( 1, "The number of two-node classes after filtering = %d.\n", Counter );
//Gia_ManEquivPrintClasses( pGia, 1, 0 );
Gia_ManCleanMark0( pGia );
@@ -1897,20 +1897,20 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
int iLitsOld, iLitsNew;
if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
{
- printf( "Equivalences are not defined.\n" );
+ Abc_Print( 1, "Equivalences are not defined.\n" );
return 0;
}
pGia1 = Gia_ReadAiger( pName1, 0, 0 );
if ( pGia1 == NULL )
{
- printf( "Cannot read first file %s.\n", pName1 );
+ Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
return 0;
}
pGia2 = Gia_ReadAiger( pName2, 0, 0 );
if ( pGia2 == NULL )
{
Gia_ManStop( pGia2 );
- printf( "Cannot read second file %s.\n", pName2 );
+ Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
return 0;
}
pMiter = Gia_ManMiter( pGia1, pGia2, 0, 1, 0 );
@@ -1918,7 +1918,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
{
Gia_ManStop( pGia1 );
Gia_ManStop( pGia2 );
- printf( "Cannot create sequential miter.\n" );
+ Abc_Print( 1, "Cannot create sequential miter.\n" );
return 0;
}
// make sure the miter is isomorphic
@@ -1927,7 +1927,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
Gia_ManStop( pGia1 );
Gia_ManStop( pGia2 );
Gia_ManStop( pMiter );
- printf( "The number of objects in different.\n" );
+ Abc_Print( 1, "The number of objects in different.\n" );
return 0;
}
if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) )
@@ -1935,7 +1935,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
Gia_ManStop( pGia1 );
Gia_ManStop( pGia2 );
Gia_ManStop( pMiter );
- printf( "The AIG structure of the miter does not match.\n" );
+ Abc_Print( 1, "The AIG structure of the miter does not match.\n" );
return 0;
}
// transfer copies
@@ -1995,7 +1995,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
}
iLitsOld--;
// undo equivalence classes
- for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
+ for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
{
Gia_ObjUnsetRepr( pGia, iObj );
@@ -2017,7 +2017,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
}
}
Vec_IntFree( vNodes );
- printf( "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
+ Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
//Gia_ManEquivPrintClasses( pGia, 1, 0 );
Gia_ManCleanMark0( pGia );
@@ -2050,7 +2050,7 @@ void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlo
iLitsOld++;
pObj = Gia_ManObj( pGia, i );
assert( pGia->pNexts[i] == 0 );
- if ( !Gia_ObjIsRo(pGia, pObj) )
+ if ( !Gia_ObjIsRo(pGia, pObj) )
Gia_ObjUnsetRepr( pGia, i );
else
iLitsNew++;
@@ -2070,7 +2070,7 @@ void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlo
}
iLitsOld--;
// undo equivalence classes
- for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
+ for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
{
Gia_ObjUnsetRepr( pGia, iObj );
@@ -2110,7 +2110,7 @@ void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlo
if ( fSeenFlop )
continue;
// undo equivalence classes
- for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
+ for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
{
Gia_ObjUnsetRepr( pGia, iObj );
@@ -2122,7 +2122,7 @@ void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlo
}
}
Vec_IntFree( vNodes );
- printf( "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
+ Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
}
////////////////////////////////////////////////////////////////////////
@@ -2131,4 +2131,3 @@ void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlo
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c
index bc54aa9e..72cf9bbe 100644
--- a/src/aig/saig/saigStrSim.c
+++ b/src/aig/saig/saigStrSim.c
@@ -50,19 +50,19 @@ static inline void Saig_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pO
***********************************************************************/
unsigned Saig_StrSimHash( Aig_Obj_t * pObj )
{
- static int s_SPrimes[128] = {
- 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
- 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
- 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
- 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
- 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
- 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
- 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
- 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
- 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
- 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
- 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
- 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
+ static int s_SPrimes[128] = {
+ 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
+ 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
+ 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
+ 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
+ 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
+ 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
+ 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
+ 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
+ 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
+ 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
+ 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
+ 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
@@ -144,7 +144,7 @@ int Saig_StrSimIsOne( Aig_Obj_t * pObj )
Synopsis [Assigns random simulation info.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -163,7 +163,7 @@ void Saig_StrSimAssignRandom( Aig_Obj_t * pObj )
Synopsis [Assigns constant 0 simulation info.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -182,7 +182,7 @@ void Saig_StrSimAssignOne( Aig_Obj_t * pObj )
Synopsis [Assigns constant 0 simulation info.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -199,7 +199,7 @@ void Saig_StrSimAssignZeroInit( Aig_Obj_t * pObj )
Synopsis [Simulated one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -225,7 +225,7 @@ void Saig_StrSimulateNode( Aig_Obj_t * pObj, int i )
Synopsis [Saves output of one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -237,7 +237,7 @@ void Saig_StrSimSaveOutput( Aig_Obj_t * pObj, int i )
unsigned * pSims0 = (unsigned *)Aig_ObjFanin0(pObj)->pData;
if ( Aig_ObjFaninC0(pObj) )
pSims[i] = ~pSims0[i];
- else
+ else
pSims[i] = pSims0[i];
}
@@ -246,7 +246,7 @@ void Saig_StrSimSaveOutput( Aig_Obj_t * pObj, int i )
Synopsis [Transfers simulation output to another node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -266,7 +266,7 @@ void Saig_StrSimTransfer( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
Synopsis [Transfers simulation output to another node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -285,7 +285,7 @@ void Saig_StrSimTransferNext( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int i )
Synopsis [Perform one round of simulation.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -336,7 +336,7 @@ void Saig_StrSimulateRound( Aig_Man_t * p0, Aig_Man_t * p1 )
Synopsis [Checks if the entry exists in the table.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -360,7 +360,7 @@ Aig_Obj_t * Saig_StrSimTableLookup( Aig_Obj_t ** ppTable, Aig_Obj_t ** ppNexts,
Synopsis [Inserts the entry into the table.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -385,7 +385,7 @@ void Saig_StrSimTableInsert( Aig_Obj_t ** ppTable, Aig_Obj_t ** ppNexts, int nTa
Synopsis [Perform one round of matching.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -399,11 +399,11 @@ int Saig_StrSimDetectUnique( Aig_Man_t * p0, Aig_Man_t * p1 )
// allocate the hash table hashing simulation info into nodes
nTableSize = Abc_PrimeCudd( Aig_ManObjNum(p0)/2 );
- ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
- ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) );
- ppCands = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) );
+ ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
+ ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) );
+ ppCands = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) );
- // hash nodes of the first AIG
+ // hash nodes of the first AIG
Aig_ManForEachObj( p0, pObj, i )
{
if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
@@ -467,7 +467,7 @@ int Saig_StrSimDetectUnique( Aig_Man_t * p0, Aig_Man_t * p1 )
Synopsis [Counts the number of matched flops.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -581,7 +581,7 @@ void Saig_StrSimSetFinalMatching( Aig_Man_t * p0, Aig_Man_t * p1 )
if ( pObj1 == NULL )
continue;
CountAll++;
- assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
+ assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
if ( Aig_ObjIsNode(pObj0) )
{
assert( Aig_ObjIsNode(pObj1) );
@@ -589,7 +589,7 @@ void Saig_StrSimSetFinalMatching( Aig_Man_t * p0, Aig_Man_t * p1 )
pFanin01 = Aig_ObjFanin1(pObj0);
pFanin10 = Aig_ObjFanin0(pObj1);
pFanin11 = Aig_ObjFanin1(pObj1);
- if ( Aig_ObjRepr(p0, pFanin00) != pFanin10 ||
+ if ( Aig_ObjRepr(p0, pFanin00) != pFanin10 ||
Aig_ObjRepr(p0, pFanin01) != pFanin11 )
{
Aig_ObjSetTravIdCurrent(p0, pObj0);
@@ -614,14 +614,14 @@ void Saig_StrSimSetFinalMatching( Aig_Man_t * p0, Aig_Man_t * p1 )
pObj1 = Aig_ObjRepr( p0, pObj0 );
if ( pObj1 == NULL )
continue;
- assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
+ assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
if ( Aig_ObjIsTravIdCurrent( p0, pObj0 ) )
{
Aig_ObjSetRepr( p0, pObj0, NULL );
Aig_ObjSetRepr( p1, pObj1, NULL );
}
}
- printf( "Total matches = %6d. Wrong matches = %6d. Ratio = %5.2f %%\n",
+ Abc_Print( 1, "Total matches = %6d. Wrong matches = %6d. Ratio = %5.2f %%\n",
CountAll, CountNot, 100.0*CountNot/CountAll );
}
@@ -691,7 +691,7 @@ void Saig_StrSimSetContiguousMatching( Aig_Man_t * p0, Aig_Man_t * p1 )
if ( pObj1 == NULL )
continue;
CountAll++;
- assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
+ assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
if ( !Aig_ObjIsTravIdCurrent( p0, pObj0 ) )
{
Aig_ObjSetRepr( p0, pObj0, NULL );
@@ -699,7 +699,7 @@ void Saig_StrSimSetContiguousMatching( Aig_Man_t * p0, Aig_Man_t * p1 )
CountNot++;
}
}
- printf( "Total matches = %6d. Wrong matches = %6d. Ratio = %5.2f %%\n",
+ Abc_Print( 1, "Total matches = %6d. Wrong matches = %6d. Ratio = %5.2f %%\n",
CountAll, CountNot, 100.0*CountNot/CountAll );
}
@@ -753,7 +753,7 @@ void Ssw_StrSimMatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
Vec_PtrPush( vNodes, pNext );
}
}
- Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
+ Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
{
if ( Saig_ObjIsPo(p, pNext) )
continue;
@@ -815,9 +815,9 @@ void Ssw_StrSimMatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fV
if ( fVerbose )
{
int nUnmached = Ssw_StrSimMatchingCountUnmached(p0);
- printf( "Extending islands by %d steps:\n", nDist );
- printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
- 0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
+ Abc_Print( 1, "Extending islands by %d steps:\n", nDist );
+ Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
+ 0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
}
for ( d = 0; d < nDist; d++ )
@@ -849,8 +849,8 @@ void Ssw_StrSimMatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fV
if ( fVerbose )
{
int nUnmached = Ssw_StrSimMatchingCountUnmached(p0);
- printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
- d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
+ Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
+ d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
}
}
@@ -890,7 +890,7 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis
// demiter the miter
if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
{
- printf( "Demitering has failed.\n" );
+ Abc_Print( 1, "Demitering has failed.\n" );
return NULL;
}
}
@@ -910,9 +910,9 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis
Saig_StrSimSetInitMatching( pPart0, pPart1 );
if ( fVerbose )
{
- printf( "Allocated %6.2f MB to simulate the first AIG.\n",
+ Abc_Print( 1, "Allocated %6.2f MB to simulate the first AIG.\n",
1.0 * Aig_ManObjNumMax(pPart0) * SAIG_WORDS * sizeof(unsigned) / (1<<20) );
- printf( "Allocated %6.2f MB to simulate the second AIG.\n",
+ Abc_Print( 1, "Allocated %6.2f MB to simulate the second AIG.\n",
1.0 * Aig_ManObjNumMax(pPart1) * SAIG_WORDS * sizeof(unsigned) / (1<<20) );
}
// iterate matching
@@ -926,7 +926,7 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis
{
int nFlops = Saig_StrSimCountMatchedFlops(pPart0);
int nNodes = Saig_StrSimCountMatchedNodes(pPart0);
- printf( "%3d : Match =%6d. FF =%6d. (%6.2f %%) Node =%6d. (%6.2f %%) ",
+ Abc_Print( 1, "%3d : Match =%6d. FF =%6d. (%6.2f %%) Node =%6d. (%6.2f %%) ",
i, nMatches,
nFlops, 100.0*nFlops/Aig_ManRegNum(pPart0),
nNodes, 100.0*nNodes/Aig_ManNodeNum(pPart0) );
@@ -952,7 +952,7 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis
pObj1 = Aig_ObjRepr(pPart0, pObj0);
if ( pObj1 == NULL )
continue;
- assert( pObj0 == Aig_ObjRepr(pPart1, pObj1) );
+ assert( pObj0 == Aig_ObjRepr(pPart1, pObj1) );
Vec_IntPush( vPairs, pObj0->Id );
Vec_IntPush( vPairs, pObj1->Id );
}
@@ -974,4 +974,3 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 59127461..fa65edea 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -152,14 +152,14 @@ int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj )
Synopsis [Performs ternary simulation for one design.]
Description []
-
+
SideEffects []
SeeAlso []
***********************************************************************/
-int Pdr_ManSimDataInit( Aig_Man_t * pAig,
- Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes,
+int Pdr_ManSimDataInit( Aig_Man_t * pAig,
+ Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes,
Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals, Vec_Int_t * vCi2Rem )
{
Aig_Obj_t * pObj;
@@ -190,7 +190,7 @@ int Pdr_ManSimDataInit( Aig_Man_t * pAig,
Synopsis [Tries to assign ternary value to one of the CIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -368,7 +368,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
// collect CO objects
Vec_IntClear( vCoObjs );
if ( pCube == NULL ) // the target is the property output
- Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
+ Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
else // the target is the cube
{
for ( i = 0; i < pCube->nLits; i++ )
@@ -400,6 +400,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
assert( RetValue );
+#if 1
// try removing high-priority flops
Vec_IntClear( vCi2Rem );
Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
@@ -429,10 +430,42 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
else
Pdr_ManExtendUndo( p->pAig, vUndo );
}
+#else
+ // try removing low-priority flops
+ Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+ {
+ if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+ continue;
+ Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
+ if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
+ continue;
+ Vec_IntClear( vUndo );
+ if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
+ Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
+ else
+ Pdr_ManExtendUndo( p->pAig, vUndo );
+ }
+ // try removing high-priority flops
+ Vec_IntClear( vCi2Rem );
+ Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+ {
+ if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+ continue;
+ Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
+ if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
+ continue;
+ Vec_IntClear( vUndo );
+ if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
+ Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
+ else
+ Pdr_ManExtendUndo( p->pAig, vUndo );
+ }
+#endif
+
if ( p->pPars->fVeryVerbose )
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
- assert( RetValue );
+ assert( RetValue );
// derive the set of resulting registers
Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
@@ -447,4 +480,3 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswAig.c b/src/proof/ssw/sswAig.c
index cd0f0c7a..acd8f919 100644
--- a/src/proof/ssw/sswAig.c
+++ b/src/proof/ssw/sswAig.c
@@ -45,7 +45,7 @@ ABC_NAMESPACE_IMPL_START
Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig )
{
Ssw_Frm_t * p;
- p = ABC_ALLOC( Ssw_Frm_t, 1 );
+ p = ABC_ALLOC( Ssw_Frm_t, 1 );
memset( p, 0, sizeof(Ssw_Frm_t) );
p->pAig = pAig;
p->nObjs = Aig_ManObjNumMax( pAig );
@@ -80,7 +80,7 @@ void Ssw_FrmStop( Ssw_Frm_t * p )
Synopsis [Performs speculative reduction for one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -95,7 +95,7 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
return;
p->nConstrTotal++;
assert( pObjRepr->Id < pObj->Id );
- // get the new node
+ // get the new node
pObjNew = Ssw_ObjFrame( p, pObj, iFrame );
// get the new node of the representative
pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame );
@@ -135,7 +135,7 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -181,7 +181,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
// transfer to the primary outputs
Aig_ManForEachCo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) );
- // transfer latch input to the latch outputs
+ // transfer latch input to the latch outputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjFrame(p, pObjLi,f) );
}
@@ -203,7 +203,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -218,7 +218,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
p->nConstrTotal = p->nConstrReduced = 0;
-
+
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
pFrames->pName = Abc_UtilStrsav( p->pAig->pName );
@@ -245,7 +245,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
// remove dangling nodes
Aig_ManCleanup( pFrames );
Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
-// printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n",
+// Abc_Print( 1, "SpecRed: Total constraints = %d. Reduced constraints = %d.\n",
// p->nConstrTotal, p->nConstrReduced );
return pFrames;
}
@@ -256,4 +256,3 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c
index 4fa9c07a..c88b2dcc 100644
--- a/src/proof/ssw/sswBmc.c
+++ b/src/proof/ssw/sswBmc.c
@@ -60,10 +60,10 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
{
if ( f == 0 )
pRes = Aig_ManConst0( pFrm->pFrames );
- else
+ else
pRes = Ssw_BmcUnroll_rec( pFrm, Saig_ObjLoToLi(pFrm->pAig, pObj), f-1 );
}
- else
+ else
{
assert( Aig_ObjIsNode(pObj) );
Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
@@ -81,7 +81,7 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
Synopsis [Derives counter-example.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -140,7 +140,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
// report statistics
if ( fVerbose )
{
- printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
+ Abc_Print( 1, "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
fflush( stdout );
@@ -162,7 +162,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
Lit = toLitCond( Ssw_ObjSatNum(pSat,pObjFrame), Aig_IsComplement(pObjFrame) );
if ( fVerbose )
{
- printf( "Solving output %2d of frame %3d ... \r",
+ Abc_Print( 1, "Solving output %2d of frame %3d ... \r",
i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
}
status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
@@ -199,9 +199,9 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
}
if ( fVerbose )
{
- printf( "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), f );
- printf( "Conf =%8.0f. Var =%8d. AIG=%9d. ",
- (double)pSat->pSat->stats.conflicts,
+ Abc_Print( 1, "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), f );
+ Abc_Print( 1, "Conf =%8.0f. Var =%8d. AIG=%9d. ",
+ (double)pSat->pSat->stats.conflicts,
pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) );
ABC_PRT( "T", clock() - clkPart );
clkPart = clock();
@@ -222,4 +222,3 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswClass.c b/src/proof/ssw/sswClass.c
index 0b5c0ab1..9cf8871b 100644
--- a/src/proof/ssw/sswClass.c
+++ b/src/proof/ssw/sswClass.c
@@ -89,11 +89,11 @@ static inline void Ssw_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pOb
SeeAlso []
***********************************************************************/
-static inline void Ssw_ObjAddClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize )
+static inline void Ssw_ObjAddClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize )
{
assert( p->pId2Class[pRepr->Id] == NULL );
assert( pClass[0] == pRepr );
- p->pId2Class[pRepr->Id] = pClass;
+ p->pId2Class[pRepr->Id] = pClass;
assert( p->pClassSizes[pRepr->Id] == 0 );
assert( nSize > 1 );
p->pClassSizes[pRepr->Id] = nSize;
@@ -112,12 +112,12 @@ static inline void Ssw_ObjAddClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t
SeeAlso []
***********************************************************************/
-static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
+static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
{
Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id];
int nSize;
assert( pClass != NULL );
- p->pId2Class[pRepr->Id] = NULL;
+ p->pId2Class[pRepr->Id] = NULL;
nSize = p->pClassSizes[pRepr->Id];
assert( nSize > 1 );
p->nClasses--;
@@ -131,7 +131,7 @@ static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr
Synopsis [Starts representation of equivalence classes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -158,13 +158,13 @@ Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
Synopsis [Starts representation of equivalence classes.]
Description []
-
+
SideEffects []
SeeAlso []
***********************************************************************/
-void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
+void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns hash key of the node
int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), // returns 1 if the node is a constant
int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement
@@ -180,7 +180,7 @@ void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
Synopsis [Stop representation of equivalence classes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -202,7 +202,7 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
Synopsis [Stop representation of equivalence classes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -218,7 +218,7 @@ Aig_Man_t * Ssw_ClassesReadAig( Ssw_Cla_t * p )
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -234,7 +234,7 @@ Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p )
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -250,7 +250,7 @@ void Ssw_ClassesClearRefined( Ssw_Cla_t * p )
Synopsis [Stop representation of equivalence classes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -266,7 +266,7 @@ int Ssw_ClassesCand1Num( Ssw_Cla_t * p )
Synopsis [Stop representation of equivalence classes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -282,7 +282,7 @@ int Ssw_ClassesClassNum( Ssw_Cla_t * p )
Synopsis [Stop representation of equivalence classes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -298,7 +298,7 @@ int Ssw_ClassesLitNum( Ssw_Cla_t * p )
Synopsis [Stop representation of equivalence classes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -319,7 +319,7 @@ Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSiz
Synopsis [Stop representation of equivalence classes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -393,11 +393,11 @@ void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
{
Aig_Obj_t * pObj;
int i;
- printf( "{ " );
+ Abc_Print( 1, "{ " );
Ssw_ClassForEachNode( p, pRepr, pObj, i )
- printf( "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
+ Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
- printf( "}\n" );
+ Abc_Print( 1, "}\n" );
}
/**Function*************************************************************
@@ -416,22 +416,22 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
Aig_Obj_t ** ppClass;
Aig_Obj_t * pObj;
int i;
- printf( "Equiv classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
+ Abc_Print( 1, "Equiv classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
p->nCands1, p->nClasses, p->nCands1+p->nLits );
if ( !fVeryVerbose )
return;
- printf( "Constants { " );
+ Abc_Print( 1, "Constants { " );
Aig_ManForEachObj( p->pAig, pObj, i )
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
- printf( "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
+ Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
- printf( "}\n" );
+ Abc_Print( 1, "}\n" );
Ssw_ManForEachClass( p, ppClass, i )
{
- printf( "%3d (%3d) : ", i, p->pClassSizes[i] );
+ Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] );
Ssw_ClassesPrintOne( p, ppClass[0] );
}
- printf( "\n" );
+ Abc_Print( 1, "\n" );
}
/**Function*************************************************************
@@ -491,7 +491,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
Synopsis [Takes the set of const1 cands and rehashes them using sim info.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -506,8 +506,8 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr
// allocate the hash table hashing simulation info into nodes
nTableSize = Abc_PrimeCudd( Vec_PtrSize(vCands)/2 );
- ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
- ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
+ ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
+ ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
// sort through the candidates
nEntries = 0;
@@ -550,7 +550,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr
nEntries++;
}
}
-
+
// copy the entries into storage in the topological order
nEntries2 = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
@@ -563,7 +563,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr
// add the nodes to the class in the topological order
ppClassNew = p->pMemClassesFree + nEntries2;
ppClassNew[0] = pObj;
- for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
+ for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
{
ppClassNew[nNodes-k] = pTemp;
@@ -622,9 +622,9 @@ clk = clock();
pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
if ( fVerbose )
{
- printf( "Allocated %.2f MB to store simulation information.\n",
+ Abc_Print( 1, "Allocated %.2f MB to store simulation information.\n",
1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
- printf( "Initial simulation of %d frames with %d words. ", nFrames, nWords );
+ Abc_Print( 1, "Initial simulation of %d frames with %d words. ", nFrames, nWords );
ABC_PRT( "Time", clock() - clk );
}
@@ -651,7 +651,7 @@ clk = clock();
}
Vec_PtrPush( vCands, pObj );
}
-
+
// this change will consider all PO drivers
if ( fOutputCorr )
{
@@ -676,7 +676,7 @@ clk = clock();
Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
if ( fVerbose )
{
- printf( "Collecting candidate equivalence classes. " );
+ Abc_Print( 1, "Collecting candidate equivalence classes. " );
ABC_PRT( "Time", clock() - clk );
}
@@ -701,7 +701,7 @@ clk = clock();
Vec_PtrFree( vCands );
if ( fVerbose )
{
- printf( "Simulation of %d frames with %d words (%2d rounds). ",
+ Abc_Print( 1, "Simulation of %d frames with %d words (%2d rounds). ",
nFrames, nWords, i-1 );
ABC_PRT( "Time", clock() - clk );
}
@@ -759,7 +759,7 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
Synopsis [Creates initial simulation classes.]
Description [Assumes that simulation info is assigned.]
-
+
SideEffects []
SeeAlso []
@@ -812,7 +812,7 @@ Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig )
p->nLits = nEntries - p->nClasses;
assert( memcmp(pClassSizes, p->pClassSizes, sizeof(int)*Aig_ManObjNumMax(pAig)) == 0 );
ABC_FREE( pClassSizes );
-// printf( "After converting:\n" );
+// Abc_Print( 1, "After converting:\n" );
// Ssw_ClassesPrint( p, 0 );
return p;
}
@@ -870,7 +870,7 @@ Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
// count the number of entries in the classes
nTotalObjs = 0;
for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
- nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0;
+ nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0;
// allocate memory for classes
p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nTotalObjs );
// create constant-1 class
@@ -919,7 +919,7 @@ Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
Synopsis [Creates classes from the temporary representation.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -961,7 +961,7 @@ Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPair
Synopsis [Iteratively refines the classes after simulation.]
Description [Returns the number of refinements performed.]
-
+
SideEffects []
SeeAlso []
@@ -971,7 +971,7 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
{
Aig_Obj_t ** pClassOld, ** pClassNew;
Aig_Obj_t * pObj, * pReprNew;
- int i;
+ int i;
// split the class
Vec_PtrClear( p->vClassOld );
@@ -1025,7 +1025,7 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
Synopsis [Refines the classes after simulation.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1045,7 +1045,7 @@ int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive )
Synopsis [Refines the classes after simulation.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1065,7 +1065,7 @@ int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive )
Synopsis [Refine the group of constant 1 nodes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1110,7 +1110,7 @@ int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs
Synopsis [Refine the group of constant 1 nodes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1168,4 +1168,3 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswCnf.c b/src/proof/ssw/sswCnf.c
index e3b422d5..dce61489 100644
--- a/src/proof/ssw/sswCnf.c
+++ b/src/proof/ssw/sswCnf.c
@@ -46,7 +46,7 @@ Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
{
Ssw_Sat_t * p;
int Lit;
- p = ABC_ALLOC( Ssw_Sat_t, 1 );
+ p = ABC_ALLOC( Ssw_Sat_t, 1 );
memset( p, 0, sizeof(Ssw_Sat_t) );
p->pAig = NULL;
p->fPolarFlip = fPolarFlip;
@@ -80,7 +80,7 @@ Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
***********************************************************************/
void Ssw_SatStop( Ssw_Sat_t * p )
{
-// printf( "Recycling SAT solver with %d vars and %d restarts.\n",
+// Abc_Print( 1, "Recycling SAT solver with %d vars and %d restarts.\n",
// p->pSat->size, p->pSat->stats.starts );
if ( p->pSat )
sat_solver_delete( p->pSat );
@@ -174,10 +174,10 @@ void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode )
// two additional clauses
// t' & e' -> f'
- // t & e -> f
+ // t & e -> f
// t + e + f'
- // t' + e' + f
+ // t' + e' + f
if ( VarT == VarE )
{
@@ -214,7 +214,7 @@ void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode )
Synopsis [Addes clauses to the solver.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -267,7 +267,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
Synopsis [Collects the supergate.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -276,8 +276,8 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
{
// if the new node is complemented or a PI, another gate begins
- if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ||
- (!fFirst && Aig_ObjRefs(pObj) > 1) ||
+ if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ||
+ (!fFirst && Aig_ObjRefs(pObj) > 1) ||
(fUseMuxes && Aig_ObjIsMuxType(pObj)) )
{
Vec_PtrPushUnique( vSuper, pObj );
@@ -294,7 +294,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
Synopsis [Collects the supergate.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -313,7 +313,7 @@ void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
Synopsis [Updates the solver clause database.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -342,14 +342,14 @@ void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
Synopsis [Updates the solver clause database.]
Description []
-
+
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj )
-{
+{
Vec_Ptr_t * vFrontier;
Aig_Obj_t * pNode, * pFanin;
int i, k, fUseMuxes = 1;
@@ -393,7 +393,7 @@ void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj )
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -425,4 +425,3 @@ int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj )
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index 2612191d..475ed70c 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -77,32 +77,32 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
continue;
Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) );
}
- // transfer latch inputs to the latch outputs
+ // transfer latch inputs to the latch outputs
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
Aig_ObjSetCopy( pObjLo, Aig_ObjCopy(pObjLi) );
}
// remove dangling nodes
Aig_ManCleanup( pFrames );
- return pFrames;
-}
+ return pFrames;
+}
/**Function*************************************************************
Synopsis [Finds one satisfiable assignment of the timeframes.]
Description []
-
+
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
-{
+{
Aig_Man_t * pFrames;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
- Aig_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i, RetValue;
if ( pvInits )
*pvInits = NULL;
@@ -110,7 +110,7 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
// derive the timeframes
pFrames = Ssw_FramesWithConstraints( p, nFrames );
// create CNF
- pCnf = Cnf_Derive( pFrames, 0 );
+ pCnf = Cnf_Derive( pFrames, 0 );
// create SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
@@ -120,7 +120,7 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
return 1;
}
// solve
- RetValue = sat_solver_solve( pSat, NULL, NULL,
+ RetValue = sat_solver_solve( pSat, NULL, NULL,
(ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_True && pvInits )
{
@@ -129,8 +129,8 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
Vec_IntPush( *pvInits, sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) );
// Aig_ManForEachCi( pFrames, pObj, i )
-// printf( "%d", Vec_IntEntry(*pvInits, i) );
-// printf( "\n" );
+// Abc_Print( 1, "%d", Vec_IntEntry(*pvInits, i) );
+// Abc_Print( 1, "\n" );
}
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
@@ -154,19 +154,19 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
***********************************************************************/
int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
-{
+{
Vec_Int_t * vLits;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
- Aig_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i, f, iVar, RetValue, nRegs;
if ( pvInits )
*pvInits = NULL;
assert( p->nConstrs > 0 );
// create CNF
nRegs = p->nRegs; p->nRegs = 0;
- pCnf = Cnf_Derive( p, Aig_ManCoNum(p) );
- p->nRegs = nRegs;
+ pCnf = Cnf_Derive( p, Aig_ManCoNum(p) );
+ p->nRegs = nRegs;
// create SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
assert( pSat->size == nFrames * pCnf->nVars );
@@ -188,8 +188,8 @@ int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
Vec_IntPush( vLits, toLitCond(iVar, 1) );
}
}
- RetValue = sat_solver_solve( pSat, (int *)Vec_IntArray(vLits),
- (int *)Vec_IntArray(vLits) + Vec_IntSize(vLits),
+ RetValue = sat_solver_solve( pSat, (int *)Vec_IntArray(vLits),
+ (int *)Vec_IntArray(vLits) + Vec_IntSize(vLits),
(ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_True && pvInits )
{
@@ -225,12 +225,12 @@ int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
***********************************************************************/
void Ssw_ManPrintPolarity( Aig_Man_t * p )
-{
+{
Aig_Obj_t * pObj;
int i;
Aig_ManForEachObj( p, pObj, i )
- printf( "%d", pObj->fPhase );
- printf( "\n" );
+ Abc_Print( 1, "%d", pObj->fPhase );
+ Abc_Print( 1, "\n" );
}
/**Function*************************************************************
@@ -245,7 +245,7 @@ void Ssw_ManPrintPolarity( Aig_Man_t * p )
***********************************************************************/
void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
-{
+{
Aig_Obj_t * pObj, * pObjLi;
int f, i, iLits, RetValue1, RetValue2;
int nFrames = Vec_IntSize(p->vInits) / Saig_ManPiNum(p->pAig);
@@ -276,12 +276,12 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
{
if ( pObj->fMarkB )
- printf( "output %d failed in frame %d.\n", i, f );
+ Abc_Print( 1, "output %d failed in frame %d.\n", i, f );
}
else
{
if ( pObj->fMarkB )
- printf( "constraint %d failed in frame %d.\n", i, f );
+ Abc_Print( 1, "constraint %d failed in frame %d.\n", i, f );
}
}
// transfer
@@ -312,7 +312,7 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
***********************************************************************/
int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
-{
+{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue;
// get representative of this class
@@ -328,7 +328,7 @@ int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
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) );
@@ -351,7 +351,7 @@ int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
{
- printf( "Ssw_ManSweepNodeConstr(): Failed to refine representative.\n" );
+ Abc_Print( 1, "Ssw_ManSweepNodeConstr(): Failed to refine representative.\n" );
}
return 1;
}
@@ -398,7 +398,7 @@ Aig_Obj_t * Ssw_ManSweepBmcConstr_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
Synopsis [Performs fraiging for the internal nodes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -464,7 +464,7 @@ clk = clock();
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
break;
- // transfer latch input to the latch outputs
+ // transfer latch input to the latch outputs
Aig_ManForEachCo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
// build logic cones for register outputs
@@ -489,7 +489,7 @@ p->timeBmc += clock() - clk;
Synopsis [Performs fraiging for the internal nodes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -545,7 +545,7 @@ clk = clock();
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
break;
- // transfer latch input to the latch outputs
+ // transfer latch input to the latch outputs
Aig_ManForEachCo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
// build logic cones for register outputs
@@ -572,7 +572,7 @@ p->timeBmc += clock() - clk;
Synopsis [Performs fraiging for the internal nodes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -610,14 +610,14 @@ Aig_Obj_t * Ssw_FramesWithClasses_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
Synopsis [Performs fraiging for the internal nodes.]
Description []
-
+
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManSweepConstr( Ssw_Man_t * p )
-{
+{
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, i, f, iLits;
@@ -672,7 +672,7 @@ p->timeReduce += clock() - clk;
assert( Ssw_ObjChild0Fra(p,pObj,f) != Aig_ManConst1(p->pFrames) );
if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst1(p->pFrames) )
{
- printf( "Polarity violation.\n" );
+ Abc_Print( 1, "Polarity violation.\n" );
continue;
}
Ssw_NodesAreConstrained( p, Ssw_ObjChild0Fra(p,pObj,f), Aig_ManConst0(p->pFrames) );
@@ -695,7 +695,7 @@ p->timeReduce += clock() - clk;
if ( Saig_ObjIsLo(p->pAig, pObj) )
p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 );
else if ( Aig_ObjIsNode(pObj) )
- {
+ {
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 );
@@ -714,4 +714,3 @@ p->timeReduce += clock() - clk;
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c
index 8a08b227..7a9d4b9f 100644
--- a/src/proof/ssw/sswCore.c
+++ b/src/proof/ssw/sswCore.c
@@ -116,7 +116,7 @@ void Ssw_ReportConeReductions( Ssw_Man_t * p, Aig_Man_t * pAigInit, Aig_Man_t *
pAig2 = Aig_ManDupOneOutput( pAigStop, 0, 1 );
pAig2 = Aig_ManScl( pAux = pAig2, 1, 1, 0, -1, -1, 0, 0 );
Aig_ManStop( pAux );
-
+
p->nNodesBegC = Aig_ManNodeNum(pAig1);
p->nNodesEndC = Aig_ManNodeNum(pAig2);
p->nRegsBegC = Aig_ManRegNum(pAig1);
@@ -140,11 +140,11 @@ void Ssw_ReportConeReductions( Ssw_Man_t * p, Aig_Man_t * pAigInit, Aig_Man_t *
void Ssw_ReportOneOutput( Aig_Man_t * p, Aig_Obj_t * pObj )
{
if ( pObj == Aig_ManConst1(p) )
- printf( "1" );
+ Abc_Print( 1, "1" );
else if ( pObj == Aig_ManConst0(p) )
- printf( "0" );
- else
- printf( "X" );
+ Abc_Print( 1, "0" );
+ else
+ Abc_Print( 1, "X" );
}
/**Function*************************************************************
@@ -165,12 +165,12 @@ void Ssw_ReportOutputs( Aig_Man_t * pAig )
Saig_ManForEachPo( pAig, pObj, i )
{
if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
- printf( "o" );
+ Abc_Print( 1, "o" );
else
- printf( "c" );
+ Abc_Print( 1, "c" );
Ssw_ReportOneOutput( pAig, Aig_ObjChild0(pObj) );
}
- printf( "\n" );
+ Abc_Print( 1, "\n" );
}
/**Function*************************************************************
@@ -244,13 +244,13 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
// refine classes using BMC
if ( p->pPars->fVerbose )
{
- printf( "Before BMC: " );
+ Abc_Print( 1, "Before BMC: " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
if ( !p->pPars->fLatchCorr )
- {
+ {
p->pMSat = Ssw_SatStart( 0 );
- if ( p->pPars->fConstrs )
+ if ( p->pPars->fConstrs )
Ssw_ManSweepBmcConstr( p );
else
Ssw_ManSweepBmc( p );
@@ -260,7 +260,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
}
if ( p->pPars->fVerbose )
{
- printf( "After BMC: " );
+ Abc_Print( 1, "After BMC: " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// apply semi-formal filtering
@@ -282,7 +282,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
}
if ( p->pPars->nStepsMax == 0 )
{
- printf( "Stopped signal correspondence after BMC.\n" );
+ Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
goto finalize;
}
// refine classes using induction
@@ -291,7 +291,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
{
if ( p->pPars->nStepsMax == nIter )
{
- printf( "Stopped signal correspondence after %d refiment iterations.\n", nIter );
+ Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", nIter );
goto finalize;
}
if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter )
@@ -299,10 +299,10 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
Aig_ManStop( pSRed );
- printf( "Iterative refinement is stopped before iteration %d.\n", nIter );
- printf( "The network is reduced using candidate equivalences.\n" );
- printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
- printf( "If the miter is SAT, the reduced result is incorrect.\n" );
+ Abc_Print( 1, "Iterative refinement is stopped before iteration %d.\n", nIter );
+ Abc_Print( 1, "The network is reduced using candidate equivalences.\n" );
+ Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
+ Abc_Print( 1, "If the miter is SAT, the reduced result is incorrect.\n" );
break;
}
@@ -313,16 +313,16 @@ clk = clock();
RetValue = Ssw_ManSweepLatch( p );
if ( p->pPars->fVerbose )
{
- printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ",
- nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
- p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
+ Abc_Print( 1, "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ",
+ nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
+ p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
ABC_PRT( "T", clock() - clk );
- }
+ }
}
else
{
- if ( p->pPars->fConstrs )
+ if ( p->pPars->fConstrs )
RetValue = Ssw_ManSweepConstr( p );
else if ( p->pPars->fDynamic )
RetValue = Ssw_ManSweepDyn( p );
@@ -332,18 +332,18 @@ clk = clock();
p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts;
if ( p->pPars->fVerbose )
{
- printf( "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ",
- nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
+ Abc_Print( 1, "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ",
+ nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
if ( p->pPars->fDynamic )
{
- printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
- printf( "R =%4d. ", p->nRecycles-nRecycles );
+ Abc_Print( 1, "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
+ Abc_Print( 1, "R =%4d. ", p->nRecycles-nRecycles );
}
- printf( "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal,
+ Abc_Print( 1, "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal,
(Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" );
ABC_PRT( "T", clock() - clk );
- }
+ }
// if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
// p->pPars->nBTLimit = 10000;
@@ -376,11 +376,11 @@ clk = clock();
Ssw_SatStop( p->pMSat );
p->pMSat = NULL;
Ssw_ManCleanup( p );
- if ( !RetValue )
+ if ( !RetValue )
break;
if ( p->pPars->pFunc )
((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
- }
+ }
finalize:
p->pPars->nIters = nIter + 1;
@@ -405,7 +405,7 @@ p->timeTotal = clock() - clkTotal;
Synopsis [Performs computation of signal correspondence with constraints.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -460,7 +460,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
}
}
-
+
// start the induction manager
p = Ssw_ManCreate( pAig, pPars );
// compute candidate equivalence classes
@@ -473,7 +473,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// derive phase bits to satisfy the constraints
if ( Ssw_ManSetConstrPhases( pAig, p->pPars->nFramesK + 1, &p->vInits ) != 0 )
{
- printf( "Ssw_SignalCorrespondence(): The init state does not satisfy the constraints!\n" );
+ Abc_Print( 1, "Ssw_SignalCorrespondence(): The init state does not satisfy the constraints!\n" );
p->pPars->fVerbose = 0;
Ssw_ManStop( p );
return NULL;
@@ -498,7 +498,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
if ( p->pPars->fLocalSim )
p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) );
// perform refinement of classes
- pAigNew = Ssw_SignalCorrespondenceRefine( p );
+ pAigNew = Ssw_SignalCorrespondenceRefine( p );
// Ssw_ReportOutputs( pAigNew );
if ( pPars->fConstrs && pPars->fVerbose )
Ssw_ReportConeReductions( p, pAig, pAigNew );
@@ -537,4 +537,3 @@ Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index 96f1315b..5fc22fdf 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -94,7 +94,7 @@ void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis )
Synopsis [Collects new POs in p->vNewPos.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -129,11 +129,11 @@ void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos
Synopsis [Loads logic cones and relevant constraints.]
- Description [Both pRepr and pObj are objects of the AIG.
+ Description [Both pRepr and pObj are objects of the AIG.
The result is the current SAT solver loaded with the logic cones
- for pRepr and pObj corresponding to them in the frames,
+ for pRepr and pObj corresponding to them in the frames,
as well as all the relevant constraints.]
-
+
SideEffects []
SeeAlso []
@@ -151,7 +151,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
pObjFrames = Aig_Regular( Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
assert( pReprFrames != pObjFrames );
/*
- // compute the AIG support
+ // compute the AIG support
Vec_PtrClear( p->vNewLos );
Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
Ssw_ManCollectPis_rec( pObj, p->vNewLos );
@@ -166,7 +166,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames );
Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames );
- // compute the frames support
+ // compute the frames support
Vec_PtrClear( p->vNewLos );
Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos );
Ssw_ManCollectPis_rec( pObjFrames, p->vNewLos );
@@ -202,7 +202,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
Synopsis [Tranfers simulation information from FRAIG to AIG.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -254,7 +254,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
Synopsis [Performs one round of simulation with counter-examples.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -286,7 +286,7 @@ p->timeSimSat += clock() - clk;
Synopsis [Performs one round of simulation with counter-examples.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -364,14 +364,14 @@ p->timeSimSat += clock() - clk;
Synopsis [Performs fraiging for the internal nodes.]
Description []
-
+
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManSweepDyn( Ssw_Man_t * p )
-{
+{
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObjNew;
int i, f;
@@ -414,15 +414,15 @@ p->timeReduce += clock() - clk;
if ( Saig_ObjIsLo(p->pAig, pObj) )
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
else if ( Aig_ObjIsNode(pObj) )
- {
+ {
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
}
// check if it is time to recycle the solver
- if ( p->pMSat->pSat == NULL ||
- (p->pPars->nSatVarMax2 &&
- p->pMSat->nSatVars > p->pPars->nSatVarMax2 &&
+ if ( p->pMSat->pSat == NULL ||
+ (p->pPars->nSatVarMax2 &&
+ p->pMSat->nSatVars > p->pPars->nSatVarMax2 &&
p->nRecycleCalls > p->pPars->nRecycleCalls2) )
{
// resimulate
@@ -435,7 +435,7 @@ p->timeReduce += clock() - clk;
Ssw_ManSweepResimulateDyn( p, f );
p->iNodeStart = i+1;
}
-// printf( "Recycling SAT solver with %d vars and %d calls.\n",
+// Abc_Print( 1, "Recycling SAT solver with %d vars and %d calls.\n",
// p->pMSat->nSatVars, p->nRecycleCalls );
// Aig_ManCleanMarkAB( p->pAig );
Aig_ManCleanMarkAB( p->pFrames );
@@ -489,4 +489,3 @@ p->timeReduce += clock() - clk;
ABC_NAMESPACE_IMPL_END
-
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
-
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c
index 97e9cf54..d1758b75 100644
--- a/src/proof/ssw/sswIslands.c
+++ b/src/proof/ssw/sswIslands.c
@@ -104,7 +104,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
continue;
pObj1 = (Aig_Obj_t *)pObj0->pData;
if ( !Saig_ObjIsLo(p1, pObj1) )
- printf( "Mismatch between LO pairs.\n" );
+ Abc_Print( 1, "Mismatch between LO pairs.\n" );
}
Saig_ManForEachLo( p1, pObj1, i )
{
@@ -112,7 +112,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
continue;
pObj0 = (Aig_Obj_t *)pObj1->pData;
if ( !Saig_ObjIsLo(p0, pObj0) )
- printf( "Mismatch between LO pairs.\n" );
+ Abc_Print( 1, "Mismatch between LO pairs.\n" );
}
}
@@ -164,7 +164,7 @@ void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
Vec_PtrPush( vNodes, pNext );
}
}
- Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
+ Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
{
if ( Saig_ObjIsPo(p, pNext) )
continue;
@@ -184,7 +184,7 @@ void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
Synopsis [Establishes relationship between nodes using pairing.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -228,9 +228,9 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose
if ( fVerbose )
{
int nUnmached = Ssw_MatchingCountUnmached(p0);
- printf( "Extending islands by %d steps:\n", nDist );
- printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
- 0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
+ Abc_Print( 1, "Extending islands by %d steps:\n", nDist );
+ Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
+ 0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
}
for ( d = 0; d < nDist; d++ )
@@ -262,8 +262,8 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose
if ( fVerbose )
{
int nUnmached = Ssw_MatchingCountUnmached(p0);
- printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
- d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
+ Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
+ d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
}
}
@@ -323,7 +323,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
Synopsis [Derives matching for all pairs.]
Description [Modifies both AIGs.]
-
+
SideEffects []
SeeAlso []
@@ -361,7 +361,7 @@ Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 )
Synopsis [Transfers the result of matching to miter.]
Description [The array of pairs should be complete.]
-
+
SideEffects []
SeeAlso []
@@ -410,7 +410,7 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p
Synopsis [Solves SEC using structural similarity.]
Description [Modifies both p0 and p1 by adding extra logic.]
-
+
SideEffects []
SeeAlso []
@@ -418,7 +418,7 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p
***********************************************************************/
Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
{
- Ssw_Man_t * p;
+ Ssw_Man_t * p;
Vec_Int_t * vPairsAll, * vPairsMiter;
Aig_Man_t * pMiter, * pAigNew;
// derive full matching
@@ -446,10 +446,10 @@ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_
Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
Aig_ManDumpBlif( pSRed, "srm_part.blif", NULL, NULL );
Aig_ManStop( pSRed );
- printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
+ Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
}
else
- printf( "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
+ Abc_Print( 1, "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
}
p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
@@ -489,11 +489,11 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai
// report the result of verification
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
- printf( "Verification successful. " );
+ Abc_Print( 1, "Verification successful. " );
else if ( RetValue == 0 )
- printf( "Verification failed with a counter-example. " );
+ Abc_Print( 1, "Verification failed with a counter-example. " );
else
- printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
+ Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
ABC_PRT( "Time", clock() - clk );
Aig_ManStop( pAigRes );
@@ -545,7 +545,7 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
Aig_Man_t * pPart0, * pPart1;
int RetValue;
if ( pPars->fVerbose )
- printf( "Performing sequential verification using structural similarity.\n" );
+ Abc_Print( 1, "Performing sequential verification using structural similarity.\n" );
// consider the case when a miter is given
if ( p1 == NULL )
{
@@ -556,7 +556,7 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
// demiter the miter
if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
{
- printf( "Demitering has failed.\n" );
+ Abc_Print( 1, "Demitering has failed.\n" );
return -1;
}
}
@@ -573,7 +573,7 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
{
// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
-// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
+// Abc_Print( 1, "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
}
}
assert( Aig_ManRegNum(pPart0) > 0 );
@@ -596,4 +596,3 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c
index e58e9b50..cd212e0b 100644
--- a/src/proof/ssw/sswLcorr.c
+++ b/src/proof/ssw/sswLcorr.c
@@ -69,7 +69,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
Synopsis [Performs one round of simulation with counter-examples.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -99,7 +99,7 @@ p->timeSimSat += clock() - clk;
Synopsis [Saves one counter-example into internal storage.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -127,7 +127,7 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand )
Synopsis [Builds fraiged logic cone of the node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -151,7 +151,7 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
Synopsis [Recycles the SAT solver.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -173,17 +173,17 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
p->nCallsDelta = 0;
clk = clock();
// get the fraiged node
- pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
+ pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
// get the fraiged representative
if ( Aig_ObjIsCi(pObjRepr) )
{
- pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr );
+ pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
}
- else
+ else
pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, 0 );
p->timeReduce += clock() - clk;
// if the fraiged nodes are the same, return
@@ -200,7 +200,7 @@ p->timeReduce += clock() - clk;
p->fRefined = 1;
}
else
- {
+ {
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
if ( RetValue == 1 ) // proved equivalence
{
@@ -215,7 +215,7 @@ p->timeReduce += clock() - clk;
return;
}
else // disproved equivalence
- {
+ {
Ssw_SmlAddPattern( p, pObjRepr, pObj );
p->nPatterns++;
p->nCallsSat++;
@@ -229,7 +229,7 @@ p->timeReduce += clock() - clk;
Synopsis [Performs one iteration of sweeping latches.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -301,7 +301,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
if ( p->nPatterns == 32 )
Ssw_ManSweepResimulate( p );
// attempt recycling the SAT solver
- if ( p->pPars->nSatVarMax &&
+ if ( p->pPars->nSatVarMax &&
p->pMSat->nSatVars > p->pPars->nSatVarMax &&
p->nRecycleCalls > p->pPars->nRecycleCalls )
{
@@ -315,7 +315,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
}
// ABC_PRT( "reduce", p->timeReduce );
// Aig_TableProfile( p->pFrames );
-// printf( "And gates = %d\n", Aig_ManNodeNum(p->pFrames) );
+// Abc_Print( 1, "And gates = %d\n", Aig_ManNodeNum(p->pFrames) );
// resimulate
if ( p->nPatterns > 0 )
Ssw_ManSweepResimulate( p );
@@ -335,4 +335,3 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswMan.c b/src/proof/ssw/sswMan.c
index a982c0c5..45f08d89 100644
--- a/src/proof/ssw/sswMan.c
+++ b/src/proof/ssw/sswMan.c
@@ -50,7 +50,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
Aig_ManFanoutStart( pAig );
Aig_ManSetCioIds( pAig );
// create interpolation manager
- p = ABC_ALLOC( Ssw_Man_t, 1 );
+ p = ABC_ALLOC( Ssw_Man_t, 1 );
memset( p, 0, sizeof(Ssw_Man_t) );
p->pPars = pPars;
p->pAig = pAig;
@@ -60,7 +60,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->iOutputLit = -1;
// allocate storage for sim pattern
p->nPatWords = Abc_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
- p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords );
+ p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords );
// other
p->vNewLos = Vec_PtrAlloc( 100 );
p->vNewPos = Vec_IntAlloc( 100 );
@@ -75,7 +75,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
Synopsis [Prints stats of the manager.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -105,17 +105,17 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
{
double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
- printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f MB.\n",
+ Abc_Print( 1, "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f MB.\n",
p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, Saig_ManConstrNum(p->pAig), p->pPars->nMaxLevs, nMemory );
- printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n",
- Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig),
+ Abc_Print( 1, "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n",
+ Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig),
0/(p->pPars->nIters+1) );
- printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n",
+ Abc_Print( 1, "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p) );
- printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n",
+ Abc_Print( 1, "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n",
p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds );
- printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
- p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
+ Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
+ p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat;
@@ -133,13 +133,13 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
// report the reductions
if ( p->pAig->nConstrs )
{
- printf( "Statistics reflecting the use of constraints:\n" );
- printf( "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n",
+ Abc_Print( 1, "Statistics reflecting the use of constraints:\n" );
+ Abc_Print( 1, "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n",
p->nConesTotal, p->nConesConstr, 100.0*p->nConesConstr/p->nConesTotal );
- printf( "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n",
+ Abc_Print( 1, "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n",
p->nEquivsTotal, p->nEquivsConstr, 100.0*p->nEquivsConstr/p->nEquivsTotal );
- printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
- p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1),
+ Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
+ p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1),
p->nRegsBegC, p->nRegsEndC, 100.0*(p->nRegsBegC-p->nRegsEndC)/(p->nRegsBegC?p->nRegsBegC:1) );
}
}
@@ -166,7 +166,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
p->pFrames = NULL;
memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
}
- if ( p->vSimInfo )
+ if ( p->vSimInfo )
{
Vec_PtrFree( p->vSimInfo );
p->vSimInfo = NULL;
@@ -180,7 +180,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
Synopsis [Frees the manager.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -193,7 +193,7 @@ void Ssw_ManStop( Ssw_Man_t * p )
Ssw_ManPrintStats( p );
if ( p->ppClasses )
Ssw_ClassesStop( p->ppClasses );
- if ( p->pSml )
+ if ( p->pSml )
Ssw_SmlStop( p->pSml );
if ( p->vDiffPairs )
Vec_IntFree( p->vDiffPairs );
@@ -215,4 +215,3 @@ void Ssw_ManStop( Ssw_Man_t * p )
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswPairs.c b/src/proof/ssw/sswPairs.c
index e4228685..3068adc4 100644
--- a/src/proof/ssw/sswPairs.c
+++ b/src/proof/ssw/sswPairs.c
@@ -80,11 +80,11 @@ int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose )
if ( fVerbose )
{
- printf( "Miter has %d outputs. ", Saig_ManPoNum(p) );
- printf( "Const0 = %d. ", CountConst0 );
- printf( "NonConst0 = %d. ", CountNonConst0 );
- printf( "Undecided = %d. ", CountUndecided );
- printf( "\n" );
+ Abc_Print( 1, "Miter has %d outputs. ", Saig_ManPoNum(p) );
+ Abc_Print( 1, "Const0 = %d. ", CountConst0 );
+ Abc_Print( 1, "NonConst0 = %d. ", CountNonConst0 );
+ Abc_Print( 1, "Undecided = %d. ", CountUndecided );
+ Abc_Print( 1, "\n" );
}
if ( CountNonConst0 )
@@ -140,7 +140,7 @@ Vec_Int_t * Ssw_TransferSignalPairs( Aig_Man_t * pMiter, Aig_Man_t * pAig1, Aig_
Synopsis [Transform pairs into class representation.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -187,12 +187,12 @@ Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumM
else if ( idReprRepr == -1 && idReprObj >= 0 )
{ // object has a class
assert( idReprObj != idRepr );
- if ( idReprObj < idRepr )
+ if ( idReprObj < idRepr )
{ // add idRepr to the same class
Vec_IntPushUniqueOrder( pvClasses[idReprObj], idRepr );
pReprs[ idRepr ] = idReprObj;
}
- else // if ( idReprObj > idRepr )
+ else // if ( idReprObj > idRepr )
{ // make idRepr new representative
Vec_IntPushFirst( pvClasses[idReprObj], idRepr );
pvClasses[idRepr] = pvClasses[idReprObj];
@@ -243,7 +243,7 @@ Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumM
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -253,7 +253,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax )
{
int i;
for ( i = 0; i < nObjNumMax; i++ )
- if ( pvClasses[i] )
+ if ( pvClasses[i] )
Vec_IntFree( pvClasses[i] );
ABC_FREE( pvClasses );
}
@@ -263,7 +263,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax )
Synopsis [Performs signal correspondence for the miter of two AIGs with node pairs defined.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -271,7 +271,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax )
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars )
{
- Ssw_Man_t * p;
+ Ssw_Man_t * p;
Aig_Man_t * pAigNew, * pMiter;
Ssw_Pars_t Pars;
Vec_Int_t * vPairs;
@@ -308,7 +308,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA
Synopsis [Runs inductive SEC for the miter of two AIGs with node pairs defined.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -337,16 +337,16 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
continue;
/*
if ( Aig_ObjIsNode(pObj) )
- printf( "n " );
+ Abc_Print( 1, "n " );
else if ( Saig_ObjIsPi(pAig, pObj) )
- printf( "pi " );
+ Abc_Print( 1, "pi " );
else if ( Saig_ObjIsLo(pAig, pObj) )
- printf( "lo " );
+ Abc_Print( 1, "lo " );
*/
Vec_IntPush( vIds1, Aig_ObjId(pObj) );
Vec_IntPush( vIds2, Aig_ObjId(pRepr) );
}
- printf( "Recorded %d pairs (before: %d after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) );
+ Abc_Print( 1, "Recorded %d pairs (before: %d after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) );
// try the new AIGs
pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig, pAigNew, vIds1, vIds2, pPars );
Vec_IntFree( vIds1 );
@@ -354,11 +354,11 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
// report the results
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
- printf( "Verification successful. " );
+ Abc_Print( 1, "Verification successful. " );
else if ( RetValue == 0 )
- printf( "Verification failed with the counter-example. " );
+ Abc_Print( 1, "Verification failed with the counter-example. " );
else
- printf( "Verification UNDECIDED. Remaining registers %d (total %d). ",
+ Abc_Print( 1, "Verification UNDECIDED. Remaining registers %d (total %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) );
ABC_PRT( "Time", clock() - clk );
// cleanup
@@ -384,16 +384,16 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V
clock_t clk = clock();
assert( vIds1 != NULL && vIds2 != NULL );
// try the new AIGs
- printf( "Performing specialized verification with node pairs.\n" );
+ Abc_Print( 1, "Performing specialized verification with node pairs.\n" );
pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig1, pAig2, vIds1, vIds2, pPars );
// report the results
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
- printf( "Verification successful. " );
+ Abc_Print( 1, "Verification successful. " );
else if ( RetValue == 0 )
- printf( "Verification failed with a counter-example. " );
+ Abc_Print( 1, "Verification failed with a counter-example. " );
else
- printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
+ Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
ABC_PRT( "Time", clock() - clk );
// cleanup
@@ -418,7 +418,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
int RetValue;
clock_t clk = clock();
// try the new AIGs
- printf( "Performing general verification without node pairs.\n" );
+ Abc_Print( 1, "Performing general verification without node pairs.\n" );
pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
Aig_ManCleanup( pMiter );
pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
@@ -426,11 +426,11 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
// report the results
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
- printf( "Verification successful. " );
+ Abc_Print( 1, "Verification successful. " );
else if ( RetValue == 0 )
- printf( "Verification failed with a counter-example. " );
+ Abc_Print( 1, "Verification failed with a counter-example. " );
else
- printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
+ Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
ABC_PRT( "Time", clock() - clk );
// cleanup
@@ -455,16 +455,16 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
int RetValue;
clock_t clk = clock();
// try the new AIGs
-// printf( "Performing general verification without node pairs.\n" );
+// Abc_Print( 1, "Performing general verification without node pairs.\n" );
pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
// report the results
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
- printf( "Verification successful. " );
+ Abc_Print( 1, "Verification successful. " );
else if ( RetValue == 0 )
- printf( "Verification failed with a counter-example. " );
+ Abc_Print( 1, "Verification failed with a counter-example. " );
else
- printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
+ Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) );
ABC_PRT( "Time", clock() - clk );
// cleanup
@@ -478,4 +478,3 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c
index 78ddbc5c..dbe8a877 100644
--- a/src/proof/ssw/sswPart.c
+++ b/src/proof/ssw/sswPart.c
@@ -56,7 +56,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
clock_t clk = clock();
if ( pPars->fConstrs )
{
- printf( "Cannot use partitioned computation with constraints.\n" );
+ Abc_Print( 1, "Cannot use partitioned computation with constraints.\n" );
return NULL;
}
// save parameters
@@ -82,14 +82,14 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
if ( fPrintParts )
{
// print partitions
- printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
+ Abc_Print( 1, "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
{
// extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
sprintf( Buffer, "part%03d.aig", i );
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
- printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
+ Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
Aig_ManStop( pTemp );
}
@@ -109,7 +109,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
pNew = Ssw_SignalCorrespondence( pTemp, pPars );
nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
if ( fVerbose )
- printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
+ Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
Aig_ManStop( pNew );
}
@@ -138,4 +138,3 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 9536bed1..8df54822 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -17,7 +17,7 @@
Revision [$Id: sswRarity.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
-
+
#include "sswInt.h"
#include "aig/gia/giaAig.h"
#include "base/main/main.h"
@@ -59,19 +59,19 @@ struct Ssw_RarMan_t_
};
-static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
+static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
return p->pRarity[iBin * (1 << p->nBinSize) + iPat];
}
-static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
+static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value;
}
-static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
+static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
@@ -93,7 +93,7 @@ static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 6
Synopsis [Prepares random number generator.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -112,7 +112,7 @@ void Ssw_RarManPrepareRandom( int nRandSeed )
Synopsis [Initializes random primary inputs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -139,7 +139,7 @@ void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
Synopsis [Derives the counter-example.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -184,13 +184,13 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
// verify the counter example
if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
{
- printf( "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
+ Abc_Print( 1, "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
// Abc_CexFree( pCex );
// pCex = NULL;
}
else
{
-// printf( "Counter-example verification is successful.\n" );
+// Abc_Print( 1, "Counter-example verification is successful.\n" );
}
return pCex;
}
@@ -209,9 +209,9 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
***********************************************************************/
void transpose32( unsigned A[32] )
{
- int j, k;
- unsigned t, m = 0x0000FFFF;
- for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) )
+ int j, k;
+ unsigned t, m = 0x0000FFFF;
+ for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) )
{
for ( k = 0; k < 32; k = (k + j + 1) & ~j )
{
@@ -220,7 +220,7 @@ void transpose32( unsigned A[32] )
A[k+j] = A[k+j] ^ (t << j);
}
}
-}
+}
/**Function*************************************************************
@@ -235,9 +235,9 @@ void transpose32( unsigned A[32] )
***********************************************************************/
void transpose64( word A[64] )
{
- int j, k;
- word t, m = 0x00000000FFFFFFFF;
- for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
+ int j, k;
+ word t, m = 0x00000000FFFFFFFF;
+ for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
{
for ( k = 0; k < 64; k = (k + j + 1) & ~j )
{
@@ -246,14 +246,14 @@ void transpose64( word A[64] )
A[k+j] = A[k+j] ^ (t << j);
}
}
-}
+}
/**Function*************************************************************
Synopsis [Transposing 64-bit matrix.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -261,10 +261,10 @@ void transpose64( word A[64] )
***********************************************************************/
void transpose64Simple( word A[64], word B[64] )
{
- int i, k;
+ int i, k;
for ( i = 0; i < 64; i++ )
B[i] = 0;
- for ( i = 0; i < 64; i++ )
+ for ( i = 0; i < 64; i++ )
for ( k = 0; k < 64; k++ )
if ( (A[i] >> k) & 1 )
B[k] |= ((word)1 << (63-i));
@@ -292,7 +292,7 @@ void TransposeTest()
for ( i = 0; i < 64; i++ )
M[i] = i? (word)0 : ~(word)0;
// for ( i = 0; i < 64; i++ )
-// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
+// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
clk = clock();
for ( i = 0; i < 100001; i++ )
@@ -306,14 +306,14 @@ void TransposeTest()
for ( i = 0; i < 64; i++ )
if ( M[i] != N[i] )
- printf( "Mismatch\n" );
+ Abc_Print( 1, "Mismatch\n" );
/*
- printf( "\n" );
+ Abc_Print( 1, "\n" );
for ( i = 0; i < 64; i++ )
- Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
- printf( "\n" );
+ Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
+ Abc_Print( 1, "\n" );
for ( i = 0; i < 64; i++ )
- Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), printf( "\n" );
+ Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), Abc_Print( 1, "\n" );
*/
}
@@ -357,15 +357,15 @@ void Ssw_RarTranspose( Ssw_RarMan_t * p )
Saig_ManForEachLi( p->pAig, pObj, i )
{
word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
- Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); printf( "\n" );
+ Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); Abc_Print( 1, "\n" );
}
- printf( "\n" );
+ Abc_Print( 1, "\n" );
for ( i = 0; i < p->nWords*64; i++ )
{
word * pBitData = Ssw_RarPatSim( p, i );
- Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); printf( "\n" );
+ Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); Abc_Print( 1, "\n" );
}
- printf( "\n" );
+ Abc_Print( 1, "\n" );
*/
}
@@ -423,7 +423,7 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -446,7 +446,7 @@ int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation infos are equal.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -470,7 +470,7 @@ int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
Synopsis [Computes hash value of the node using its simulation info.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -479,19 +479,19 @@ int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj )
{
Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
- static int s_SPrimes[128] = {
- 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
- 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
- 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
- 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
- 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
- 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
- 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
- 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
- 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
- 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
- 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
- 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
+ static int s_SPrimes[128] = {
+ 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
+ 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
+ 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
+ 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
+ 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
+ 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
+ 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
+ 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
+ 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
+ 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
+ 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
+ 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
@@ -509,7 +509,7 @@ unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -537,7 +537,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
Synopsis [Check if any of the POs becomes non-constant.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -568,7 +568,7 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
Synopsis [Performs one round of simulation.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -580,7 +580,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
word * pSim, * pSim0, * pSim1;
word Flip, Flip0, Flip1;
int w, i;
- // initialize
+ // initialize
Ssw_RarManInitialize( p, vInit );
Vec_PtrClear( p->vUpdConst );
Vec_PtrClear( p->vUpdClass );
@@ -603,7 +603,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
}
}
- // simulate
+ // simulate
Aig_ManForEachNode( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
@@ -657,7 +657,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 );
Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 );
}
- }
+ }
}
@@ -666,7 +666,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -700,7 +700,7 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -725,7 +725,7 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p )
Synopsis [Select best patterns.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -762,7 +762,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
p->pPatCosts[k] += 1.0/(Value*Value);
}
// print the result
-//printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
+//Abc_Print( 1, "%3d : %9.6f\n", k, p->pPatCosts[k] );
}
// choose as many as there are words
@@ -785,7 +785,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest );
for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ )
Vec_IntPush( vInits, Abc_InfoHasBit(pPattern, k) );
-//printf( "Best pattern %5d\n", iPatBest );
+//Abc_Print( 1, "Best pattern %5d\n", iPatBest );
Vec_IntPush( p->vPatBests, iPatBest );
}
assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
@@ -804,7 +804,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
***********************************************************************/
static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
-{
+{
Vec_Int_t * vInit;
Aig_Obj_t * pObj, * pObjLi;
int f, i, iBit;
@@ -833,15 +833,15 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
// check that the output failed as expected -- cannot check because it is not an SRM!
// pObj = Aig_ManCo( 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
vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
{
-//printf( "%d", pObj->fMarkB );
+//Abc_Print( 1, "%d", pObj->fMarkB );
Vec_IntPush( vInit, pObj->fMarkB );
}
-//printf( "\n" );
+//Abc_Print( 1, "\n" );
Aig_ManCleanMarkB( pAig );
return vInit;
}
@@ -872,7 +872,7 @@ int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose )
pAig->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), 1 );
pAig->pSeqModel->iPo = i;
if ( fVerbose )
- printf( "Output %d is trivally SAT in frame 0. \n", i );
+ Abc_Print( 1, "Output %d is trivally SAT in frame 0. \n", i );
return 1;
}
}
@@ -911,7 +911,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) )
return 0;
if ( fVerbose )
- printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
+ Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
nWords, nFrames, nRounds, nRandSeed, TimeOut );
// reset random numbers
Ssw_RarManPrepareRandom( nSavedSeed );
@@ -929,7 +929,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0 );
// if ( pNewAig->pSeqModel != NULL )
-// printf( "BMC has found a counter-example in frame %d.\n", iFrameFail );
+// Abc_Print( 1, "BMC has found a counter-example in frame %d.\n", iFrameFail );
Aig_ManStop( pNewAig );
}
// simulate
@@ -938,12 +938,12 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
- if ( fVerbose ) printf( "\n" );
-// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+ if ( fVerbose ) Abc_Print( 1, "\n" );
+// Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
Ssw_RarManPrepareRandom( nSavedSeed );
ABC_FREE( pAig->pSeqModel );
if ( fVerbose )
- printf( "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
+ Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, fVerbose );
// print final report
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
@@ -954,9 +954,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
// check timeout
if ( TimeOut && clock() > nTimeToStop )
{
- if ( fVerbose ) printf( "\n" );
- printf( "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
- printf( "Reached timeout (%d sec).\n", TimeOut );
+ if ( fVerbose ) Abc_Print( 1, "\n" );
+ Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
+ Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut );
goto finish;
}
}
@@ -977,16 +977,16 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
// printout
if ( fVerbose )
{
-// printf( "Round %3d: ", r );
+// Abc_Print( 1, "Round %3d: ", r );
// Abc_PrintTime( 1, "Time", clock() - clk );
- printf( "." );
+ Abc_Print( 1, "." );
}
}
finish:
if ( r == nRounds && f == nFrames )
{
- if ( fVerbose ) printf( "\n" );
- printf( "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
+ if ( fVerbose ) Abc_Print( 1, "\n" );
+ Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
@@ -1048,7 +1048,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
if ( fMiter && Ssw_RarCheckTrivial( pAig, 1 ) )
return 0;
if ( fVerbose )
- printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
+ Abc_Print( 1, "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
nWords, nFrames, nRounds, nRandSeed, TimeOut );
// reset random numbers
Ssw_RarManPrepareRandom( nSavedSeed );
@@ -1060,7 +1060,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
if ( pCex )
{
p->vInits = Ssw_RarFindStartingState( pAig, pCex );
- printf( "Beginning simulation from the state derived using the counter-example.\n" );
+ Abc_Print( 1, "Beginning simulation from the state derived using the counter-example.\n" );
}
else
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
@@ -1079,7 +1079,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
// print the stats
if ( fVerbose )
{
- printf( "Initial : " );
+ Abc_Print( 1, "Initial : " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// refine classes using BMC
@@ -1088,7 +1088,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
// start filtering equivalence classes
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;
}
// simulate
@@ -1097,11 +1097,11 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
- if ( !fVerbose )
- printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
-// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+ if ( !fVerbose )
+ Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
+// Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
if ( fVerbose )
- printf( "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
+ Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
Ssw_RarManPrepareRandom( nSavedSeed );
Abc_CexFree( pAig->pSeqModel );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, 1 );
@@ -1114,9 +1114,9 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
// check timeout
if ( TimeOut && clock() > nTimeToStop )
{
- if ( fVerbose ) printf( "\n" );
- printf( "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
- printf( "Reached timeout (%d sec).\n", TimeOut );
+ if ( fVerbose ) Abc_Print( 1, "\n" );
+ Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
+ Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut );
goto finish;
}
}
@@ -1137,21 +1137,21 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
// printout
if ( fVerbose )
{
- printf( "Round %3d: ", r );
+ Abc_Print( 1, "Round %3d: ", r );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
else
{
- printf( "." );
+ Abc_Print( 1, "." );
}
}
finish:
// report
if ( r == nRounds && f == nFrames )
{
- if ( !fVerbose )
- printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
- printf( "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
+ if ( !fVerbose )
+ Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
+ Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
@@ -1171,7 +1171,7 @@ finish:
***********************************************************************/
int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
-{
+{
Aig_Man_t * pAig;
int RetValue;
pAig = Gia_ManToAigSimple( p );
@@ -1197,4 +1197,3 @@ int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c
index 6a67dea6..f6b2c319 100644
--- a/src/proof/ssw/sswRarity2.c
+++ b/src/proof/ssw/sswRarity2.c
@@ -50,19 +50,19 @@ struct Ssw_RarMan_t_
};
-static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
+static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
return p->pRarity[iBin * (1 << p->nBinSize) + iPat];
}
-static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
+static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value;
}
-static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
+static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
@@ -78,7 +78,7 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -109,7 +109,7 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -148,7 +148,7 @@ static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
Saig_ManForEachLi( p->pAig, pObj, i )
{
pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
- Extra_PrintBinary( stdout, pData, 32 ); printf( "\n" );
+ Extra_PrintBinary( stdout, pData, 32 ); Abc_Print( 1, "\n" );
}
*/
for ( k = 0; k < p->nWords * 32; k++ )
@@ -168,8 +168,8 @@ static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
for ( i = 0; i < p->nGroups; i++ )
{
for ( k = 0; k < (1 << p->nBinSize); k++ )
- printf( "%d ", Ssw_RarGetBinPat(p, i, k) );
- printf( "\n" );
+ Abc_Print( 1, "%d ", Ssw_RarGetBinPat(p, i, k) );
+ Abc_Print( 1, "\n" );
}
*/
}
@@ -212,7 +212,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
p->pPatCosts[k] += 1.0/(Value*Value);
}
// print the result
-// printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
+// Abc_Print( 1, "%3d : %9.6f\n", k, p->pPatCosts[k] );
}
// choose as many as there are words
@@ -237,7 +237,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
Vec_IntPush( vInits, Abc_InfoHasBit(pData, iPatBest) );
}
-//printf( "Best pattern %5d\n", iPatBest );
+//Abc_Print( 1, "Best pattern %5d\n", iPatBest );
}
assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
}
@@ -255,7 +255,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
***********************************************************************/
static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
-{
+{
Vec_Int_t * vInit;
Aig_Obj_t * pObj, * pObjLi;
int f, i, iBit;
@@ -284,7 +284,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
// check that the output failed as expected -- cannot check because it is not an SRM!
// pObj = Aig_ManCo( 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
vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
@@ -318,7 +318,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
if ( Aig_ManNodeNum(pAig) == 0 )
return -1;
if ( fVerbose )
- printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
+ Abc_Print( 1, "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
nWords, nFrames, nBinSize, nRounds, TimeOut );
// reset random numbers
Aig_ManRandom( 1 );
@@ -336,8 +336,8 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
Ssw_SmlSimulateOne( p->pSml );
if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
{
- if ( fVerbose ) printf( "\n" );
- printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+ if ( fVerbose ) Abc_Print( 1, "\n" );
+ Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
RetValue = 0;
break;
}
@@ -348,22 +348,22 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
// printout
if ( fVerbose )
{
-// printf( "Round %3d: ", r );
+// Abc_Print( 1, "Round %3d: ", r );
// Abc_PrintTime( 1, "Time", clock() - clk );
- printf( "." );
+ Abc_Print( 1, "." );
}
// check timeout
if ( TimeOut && clock() > nTimeToStop )
{
- if ( fVerbose ) printf( "\n" );
- printf( "Reached timeout (%d seconds).\n", TimeOut );
+ if ( fVerbose ) Abc_Print( 1, "\n" );
+ Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeOut );
break;
}
}
if ( r == nRounds )
{
- if ( fVerbose ) printf( "\n" );
- printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
+ if ( fVerbose ) Abc_Print( 1, "\n" );
+ Abc_Print( 1, "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
@@ -397,7 +397,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
if ( Aig_ManNodeNum(pAig) == 0 )
return -1;
if ( fVerbose )
- printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
+ Abc_Print( 1, "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
nWords, nFrames, nBinSize, nRounds, TimeOut );
// reset random numbers
Aig_ManRandom( 1 );
@@ -427,7 +427,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
// print the stats
if ( fVerbose )
{
- printf( "Initial : " );
+ Abc_Print( 1, "Initial : " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// refine classes using BMC
@@ -436,15 +436,15 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
// start filtering equivalence classes
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;
}
// simulate
Ssw_SmlSimulateOne( p->pSml );
if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
{
- if ( fVerbose ) printf( "\n" );
- printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+ if ( fVerbose ) Abc_Print( 1, "\n" );
+ Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
RetValue = 0;
break;
}
@@ -454,7 +454,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
// printout
if ( fVerbose )
{
- printf( "Round %3d: ", r );
+ Abc_Print( 1, "Round %3d: ", r );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// get initialization patterns
@@ -464,14 +464,14 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
// check timeout
if ( TimeOut && clock() > nTimeToStop )
{
- if ( fVerbose ) printf( "\n" );
- printf( "Reached timeout (%d seconds).\n", TimeOut );
+ if ( fVerbose ) Abc_Print( 1, "\n" );
+ Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeOut );
break;
}
}
if ( r == nRounds )
{
- printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
+ Abc_Print( 1, "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
@@ -491,7 +491,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
***********************************************************************/
int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
-{
+{
Aig_Man_t * pAig;
int RetValue;
pAig = Gia_ManToAigSimple( p );
@@ -516,4 +516,3 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c
index e58ba848..822f63f5 100644
--- a/src/proof/ssw/sswSemi.c
+++ b/src/proof/ssw/sswSemi.c
@@ -67,7 +67,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
Aig_Obj_t * pObj;
int i;
// create interpolation manager
- p = ABC_ALLOC( Ssw_Sem_t, 1 );
+ p = ABC_ALLOC( Ssw_Sem_t, 1 );
memset( p, 0, sizeof(Ssw_Sem_t) );
p->nConfMaxStart = nConfMax;
p->nConfMax = nConfMax;
@@ -101,7 +101,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -120,7 +120,7 @@ void Ssw_SemManStop( Ssw_Sem_t * p )
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -141,7 +141,7 @@ int Ssw_SemCheckTargets( Ssw_Sem_t * p )
Synopsis []
Description []
-
+
SideEffects []
SeeAlso []
@@ -168,7 +168,7 @@ void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p )
Synopsis [Performs fraiging for the internal nodes.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -212,7 +212,7 @@ clk = clock();
{
fFirst = 1;
pBmc->nConfMax *= 10;
- }
+ }
}
if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
{
@@ -236,7 +236,7 @@ clk = clock();
Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );
}
-//printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
+//Abc_Print( 1, "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
}
if ( fFirst )
pBmc->nConfMax /= 10;
@@ -272,10 +272,10 @@ int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int
}
if ( fVerbose )
{
- printf( "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
- Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
+ Abc_Print( 1, "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
+ Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
- }
+ }
RetValue = 0;
for ( Iter = 0; Iter < p->nPatterns; Iter++ )
{
@@ -284,16 +284,16 @@ clk = clock();
Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
if ( fVerbose )
{
- printf( "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
- Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
- Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
+ Abc_Print( 1, "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
+ Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
+ Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
p->pMan->nSatFailsReal? "f" : " " );
ABC_PRT( "T", clock() - clk );
- }
+ }
Ssw_ManCleanup( p->pMan );
if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
{
- printf( "Target is hit!!!\n" );
+ Abc_Print( 1, "Target is hit!!!\n" );
RetValue = 1;
}
if ( p->nPatterns >= p->nPatternsAlloc )
@@ -304,14 +304,14 @@ clk = clock();
pMan->nStrangers = 0;
pMan->nSatCalls = 0;
pMan->nSatProof = 0;
- pMan->nSatFailsReal = 0;
+ pMan->nSatFailsReal = 0;
pMan->nSatCallsUnsat = 0;
- pMan->nSatCallsSat = 0;
- pMan->timeSimSat = 0;
- pMan->timeSat = 0;
- pMan->timeSatSat = 0;
- pMan->timeSatUnsat = 0;
- pMan->timeSatUndec = 0;
+ pMan->nSatCallsSat = 0;
+ pMan->timeSimSat = 0;
+ pMan->timeSat = 0;
+ pMan->timeSatSat = 0;
+ pMan->timeSatUnsat = 0;
+ pMan->timeSatUndec = 0;
return RetValue;
}
@@ -321,4 +321,3 @@ clk = clock();
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index bb4a55d2..469af654 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -62,19 +62,19 @@ static inline unsigned Ssw_ObjRandomSim() { return Aig_ManRa
***********************************************************************/
unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
{
- static int s_SPrimes[128] = {
- 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
- 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
- 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
- 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
- 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
- 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
- 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
- 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
- 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
- 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
- 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
- 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
+ static int s_SPrimes[128] = {
+ 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
+ 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
+ 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
+ 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
+ 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
+ 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
+ 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
+ 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
+ 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
+ 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
+ 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
+ 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
@@ -93,7 +93,7 @@ unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -115,7 +115,7 @@ int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation infos are equal.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -138,7 +138,7 @@ int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1
Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -154,7 +154,7 @@ int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if the nodes appear equal.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -171,7 +171,7 @@ int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
Synopsis [Counts the number of 1s in the XOR of simulation data.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -193,7 +193,7 @@ int Ssw_SmlNodeNotEquWeight( Ssw_Sml_t * p, int Left, int Right )
Synopsis [Checks implication.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -228,7 +228,7 @@ int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * p
Synopsis [Counts the number of 1s in the implication.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -261,7 +261,7 @@ int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * p
Synopsis [Counts the number of 1s in the implication.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -285,7 +285,7 @@ int Ssw_SmlCountEqual( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -307,7 +307,7 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -324,7 +324,7 @@ int Ssw_SmlNodeIsZeroFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f )
Synopsis [Counts the number of one's in the patten the object.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -353,7 +353,7 @@ int Ssw_SmlNodeCountOnesReal( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Counts the number of one's in the patten the object.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -389,7 +389,7 @@ int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs )
Synopsis [Generated const 0 pattern.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -405,7 +405,7 @@ void Ssw_SmlSavePattern0( Ssw_Man_t * p, int fInit )
Synopsis [[Generated const 1 pattern.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -431,14 +431,14 @@ void Ssw_SmlSavePattern1( Ssw_Man_t * p, int fInit )
Synopsis [Creates the counter-example from the successful pattern.]
Description []
-
+
SideEffects []
SeeAlso []
***********************************************************************/
int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo )
-{
+{
Aig_Obj_t * pFanin, * pObjPi;
unsigned * pSims;
int i, k, BestPat, * pModel;
@@ -461,10 +461,10 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo )
Aig_ManForEachCi( p->pAig, pObjPi, i )
{
pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat);
-// printf( "%d", pModel[i] );
+// Abc_Print( 1, "%d", pModel[i] );
}
pModel[Aig_ManCiNum(p->pAig)] = pObjPo->Id;
-// printf( "\n" );
+// Abc_Print( 1, "\n" );
return pModel;
}
@@ -485,7 +485,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
int i;
// make sure the reference simulation pattern does not detect the bug
pObj = Aig_ManCo( p->pAig, 0 );
- assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
+ assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
Aig_ManForEachCo( p->pAig, pObj, i )
{
if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) )
@@ -504,7 +504,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
Synopsis [Assigns random patterns to the PI node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -529,7 +529,7 @@ void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Assigns random patterns to the PI node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -551,7 +551,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
Synopsis [Assigns constant patterns to the PI node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -566,14 +566,14 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
for ( i = 0; i < p->nWordsFrame; i++ )
pSims[i] = fConst1? ~(unsigned)0 : 0;
-}
+}
/**Function*************************************************************
Synopsis [Assigns constant patterns to the PI node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -587,14 +587,14 @@ void Ssw_SmlObjAssignConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, in
assert( Aig_ObjIsCi(pObj) );
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
pSims[iWord] = fConst1? ~(unsigned)0 : 0;
-}
+}
/**Function*************************************************************
Synopsis [Assigns constant patterns to the PI node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -607,14 +607,14 @@ void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWor
assert( Aig_ObjIsCi(pObj) );
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
pSims[iWord] = Word;
-}
+}
/**Function*************************************************************
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -627,7 +627,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
assert( p->nFrames > 0 );
if ( p->nFrames == 1 )
{
- // copy the PI info
+ // copy the PI info
Aig_ManForEachCi( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
// flip one bit
@@ -644,7 +644,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
for ( f = 0; f < p->nFrames; f++ )
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
- // copy the latch info
+ // copy the latch info
k = 0;
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
@@ -665,7 +665,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -697,7 +697,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
Synopsis [Simulates one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -763,7 +763,7 @@ void Ssw_SmlNodeSimulate( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
Synopsis [Simulates one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -794,7 +794,7 @@ int Ssw_SmlNodesCompareInFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pO
Synopsis [Simulates one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -828,7 +828,7 @@ void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
Synopsis [Simulates one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -857,7 +857,7 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
Synopsis [Simulates one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -886,7 +886,7 @@ void Ssw_SmlNodeTransferFirst( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn
Synopsis [Assings random simulation info for the PIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -919,7 +919,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
Synopsis [Assings random simulation info for the PIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -946,7 +946,7 @@ void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit )
Synopsis [Assings random simulation info for the PIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -971,7 +971,7 @@ void Ssw_SmlReinitialize( Ssw_Sml_t * p )
Synopsis [Check if any of the POs becomes non-constant.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -996,7 +996,7 @@ int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p )
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
-
+
SideEffects []
SeeAlso []
@@ -1035,7 +1035,7 @@ p->nSimRounds++;
Synopsis [Converts simulation information to be not normallized.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1067,7 +1067,7 @@ void Ssw_SmlUnnormalize( Ssw_Sml_t * p )
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
-
+
SideEffects []
SeeAlso []
@@ -1108,7 +1108,7 @@ void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pV
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
-
+
SideEffects []
SeeAlso []
@@ -1139,7 +1139,7 @@ p->nSimRounds++;
Synopsis [Allocates simulation manager.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1164,7 +1164,7 @@ Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFr
Synopsis [Allocates simulation manager.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1180,7 +1180,7 @@ void Ssw_SmlClean( Ssw_Sml_t * p )
Synopsis [Get simulation data.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1202,7 +1202,7 @@ Vec_Ptr_t * Ssw_SmlSimDataPointers( Ssw_Sml_t * p )
Synopsis [Deallocates simulation manager.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1219,7 +1219,7 @@ void Ssw_SmlStop( Ssw_Sml_t * p )
Synopsis [Performs simulation of the uninitialized circuit.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1239,7 +1239,7 @@ Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
Synopsis [Performs simulation of the initialized circuit.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1260,7 +1260,7 @@ Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
Synopsis [Performs next round of sequential simulation.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1279,7 +1279,7 @@ void Ssw_SmlResimulateSeq( Ssw_Sml_t * p )
Synopsis [Returns the number of frames simulated in the manager.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1295,7 +1295,7 @@ int Ssw_SmlNumFrames( Ssw_Sml_t * p )
Synopsis [Returns the total number of simulation words.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1312,7 +1312,7 @@ int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p )
Description [The simulation info is normalized unless procedure
Ssw_SmlUnnormalize() is called in advance.]
-
+
SideEffects []
SeeAlso []
@@ -1329,7 +1329,7 @@ unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Creates sequential counter-example from the simulation info.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1391,7 +1391,7 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
// verify the counter example
if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
{
- printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
+ Abc_Print( 1, "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
@@ -1404,4 +1404,3 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswSimSat.c b/src/proof/ssw/sswSimSat.c
index 4d1b3ba2..6e5944d1 100644
--- a/src/proof/ssw/sswSimSat.c
+++ b/src/proof/ssw/sswSimSat.c
@@ -62,17 +62,17 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
// make sure refinement happened
- if ( Aig_ObjIsConst1(pRepr) )
+ if ( Aig_ObjIsConst1(pRepr) )
{
assert( RetValue1 );
if ( RetValue1 == 0 )
- printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
+ Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
- printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
+ Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
}
}
p->timeSimSat += clock() - clk;
@@ -105,13 +105,13 @@ void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr,
{
assert( RetValue1 );
if ( RetValue1 == 0 )
- printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
+ Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
- printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
+ Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
}
p->timeSimSat += clock() - clk;
}
@@ -122,4 +122,3 @@ p->timeSimSat += clock() - clk;
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index b4ff44c2..bccc6aa4 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -98,7 +98,7 @@ void Ssw_CheckConstraints( Ssw_Man_t * p )
Counter++;
}
}
- printf( "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter );
+ Abc_Print( 1, "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter );
}
/**Function*************************************************************
@@ -148,7 +148,7 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
Synopsis [Saves one counter-example into internal storage.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -178,14 +178,14 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
-
+
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs )
-{
+{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue;
clock_t clk;
@@ -202,7 +202,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_
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;
// add constraints on demand
if ( !fBmc && p->pPars->fDynamic )
{
@@ -248,7 +248,7 @@ p->timeMarkCones += clock() - clk;
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
{
- printf( "Ssw_ManSweepNode(): Failed to refine representative.\n" );
+ Abc_Print( 1, "Ssw_ManSweepNode(): Failed to refine representative.\n" );
}
return 1;
}
@@ -299,7 +299,7 @@ clk = clock();
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
break;
- // transfer latch input to the latch outputs
+ // transfer latch input to the latch outputs
Aig_ManForEachCo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
// build logic cones for register outputs
@@ -340,14 +340,14 @@ void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
pFile = fopen( pBuffer, "w" );
if ( pFile == NULL )
{
- printf( "Cannot open file %s for writing.\n", pBuffer );
+ Abc_Print( 1, "Cannot open file %s for writing.\n", pBuffer );
return;
}
fclose( pFile );
pNew = Saig_ManCreateEquivMiter( p, vPairs );
Ioa_WriteAiger( pNew, pBuffer, 0, 0 );
Aig_ManStop( pNew );
- printf( "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer );
+ Abc_Print( 1, "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer );
}
@@ -363,7 +363,7 @@ void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
***********************************************************************/
int Ssw_ManSweep( Ssw_Man_t * p )
-{
+{
static int Counter;
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
@@ -412,7 +412,7 @@ p->timeReduce += clock() - clk;
if ( Saig_ObjIsLo(p->pAig, pObj) )
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
else if ( Aig_ObjIsNode(pObj) )
- {
+ {
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
@@ -435,4 +435,3 @@ p->timeReduce += clock() - clk;
ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswUnique.c b/src/proof/ssw/sswUnique.c
index 1bd44a03..9fad9060 100644
--- a/src/proof/ssw/sswUnique.c
+++ b/src/proof/ssw/sswUnique.c
@@ -61,7 +61,7 @@ void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
// Vec_IntPush( p->vDiffPairs, 1 );
else if ( Aig_ObjPhaseReal(pObj0) != Aig_ObjPhaseReal(pObj1) )
Vec_IntPush( p->vDiffPairs, 1 );
- else
+ else
{
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObj0), Aig_Regular(pObj1) );
Vec_IntPush( p->vDiffPairs, RetValue!=1 );
@@ -72,7 +72,7 @@ void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
Counter = 0;
Vec_IntForEachEntry( p->vDiffPairs, RetValue, i )
Counter += RetValue;
-// printf( "The number of different register pairs = %d.\n", Counter );
+// Abc_Print( 1, "The number of different register pairs = %d.\n", Counter );
}
@@ -96,7 +96,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
assert( p->vDiffPairs && Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );
// compute the first support in terms of LOs
- ppObjs[0] = pRepr;
+ ppObjs[0] = pRepr;
ppObjs[1] = pObj;
Aig_SupportNodes( p->pAig, ppObjs, 2, p->vCommon );
// keep only LOs
@@ -116,7 +116,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
Vec_PtrShrink( p->vCommon, k );
if ( fVerbose )
- printf( "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ",
+ Abc_Print( 1, "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ",
Aig_ObjId(pObj), RetValue, Vec_PtrSize(p->vCommon),
fFeasible? "yes": "no " );
@@ -129,10 +129,10 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
if ( Value0 != Value1 )
RetValue = 0;
if ( fVerbose )
- printf( "%d", Value0 ^ Value1 );
+ Abc_Print( 1, "%d", Value0 ^ Value1 );
}
if ( fVerbose )
- printf( "\n" );
+ Abc_Print( 1, "\n" );
return RetValue && fFeasible;
}
@@ -166,7 +166,7 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int
}
if ( Aig_ObjIsConst1(Aig_Regular(pTotal)) )
{
-// printf( "Skipped\n" );
+// Abc_Print( 1, "Skipped\n" );
return 0;
}
// create CNF
@@ -194,4 +194,3 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int
ABC_NAMESPACE_IMPL_END
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-20 10:11:11 +0000