summaryrefslogtreecommitdiffstats
path: root/src/proof/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/ssw')
-rw-r--r--src/proof/ssw/sswAig.c17
-rw-r--r--src/proof/ssw/sswBmc.c17
-rw-r--r--src/proof/ssw/sswCnf.c27
-rw-r--r--src/proof/ssw/sswConstr.c69
-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
18 files changed, 425 insertions, 443 deletions
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/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/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-07-16 03:49:37 +0000