From ef893337741de07a94d2cf6056b1ca6822a5e28e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 4 Mar 2011 16:59:28 -0800 Subject: Improved the speed of refinement algorithm in &abs_refine. --- src/aig/gia/giaAbs.c | 6 +- src/aig/saig/module.make | 1 + src/aig/saig/saig.h | 13 +- src/aig/saig/saigAbs.c | 16 ++- src/aig/saig/saigSimExt.c | 12 +- src/aig/saig/saigSimExt2.c | 287 +++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abc.c | 22 +++- 7 files changed, 332 insertions(+), 25 deletions(-) create mode 100644 src/aig/saig/saigSimExt2.c diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 607e5ac6..d31e62f5 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -36,7 +36,7 @@ ABC_NAMESPACE_IMPL_START extern Vec_Int_t * Saig_ManProofAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); -extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fVerbose ); +extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -253,7 +253,7 @@ Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia ) SeeAlso [] ***********************************************************************/ -int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fVerbose ) +int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ) { Aig_Man_t * pNew; Vec_Int_t * vFlops; @@ -264,7 +264,7 @@ int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fVerbos } pNew = Gia_ManToAig( pGia, 0 ); vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); - if ( !Saig_ManCexRefineStep( pNew, vFlops, pCex, fVerbose ) ) + if ( !Saig_ManCexRefineStep( pNew, vFlops, pCex, fTryFour, fSensePath, fVerbose ) ) { pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL; Vec_IntFree( vFlops ); diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index a1f0e976..a83ac5e2 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -18,6 +18,7 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigRetStep.c \ src/aig/saig/saigScl.c \ src/aig/saig/saigSimExt.c \ + src/aig/saig/saigSimExt2.c \ src/aig/saig/saigSimFast.c \ src/aig/saig/saigSimMv.c \ src/aig/saig/saigSimSeq.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index bf5681b9..62ac35ac 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -29,14 +29,15 @@ #include "aig.h" #include "giaAbs.h" +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_HEADER_START - +#define SAIG_ZER 1 +#define SAIG_ONE 2 +#define SAIG_UND 3 //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -181,7 +182,9 @@ extern int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fFo extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig ); /*=== saigSimExt.c ==========================================================*/ extern Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ); -extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose ); +extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fTryFour, int fVerbose ); +/*=== saigSimExt.c ==========================================================*/ +extern Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose ); /*=== saigSimMv.c ==========================================================*/ extern int Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose ); /*=== saigStrSim.c ==========================================================*/ diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 471d5d2d..bed5edaf 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -225,7 +225,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo return NULL; if ( pnUseStart ) *pnUseStart = pAbs->pSeqModel->iFrame; - vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose ); + vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose ); if ( vFlopsNew == NULL ) return NULL; if ( Vec_IntSize(vFlopsNew) == 0 ) @@ -267,13 +267,16 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo SeeAlso [] ***********************************************************************/ -int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fVerbose ) +int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ) { Aig_Man_t * pAbs; Vec_Int_t * vFlopsNew; - int i, Entry; + int i, Entry, clk = clock(); pAbs = Saig_ManDeriveAbstraction( p, vFlops ); - vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); + if ( fSensePath ) + vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); + else + vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose ); if ( vFlopsNew == NULL ) { Aig_ManStop( pAbs ); @@ -289,7 +292,10 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, return 0; } if ( fVerbose ) - printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) ); + { + printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vFlopsNew) ); + Abc_PrintTime( 0, "Time", clock() - clk ); + } // vFlopsNew contains PI number that should be kept in pAbs // add to the abstraction Vec_IntForEachEntry( vFlopsNew, Entry, i ) diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c index 9828d17e..ac0fa697 100644 --- a/src/aig/saig/saigSimExt.c +++ b/src/aig/saig/saigSimExt.c @@ -28,10 +28,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define SAIG_ZER 1 -#define SAIG_ONE 2 -#define SAIG_UND 3 - static inline int Saig_ManSimInfoNot( int Value ) { if ( Value == SAIG_ZER ) @@ -521,7 +517,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Abc_C SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ) +Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fTryFour, int fVerbose ) { Vec_Int_t * vRes; Vec_Ptr_t * vSimInfo; @@ -537,8 +533,10 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, A Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) ); clk = clock(); -// vRes = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); + if ( fTryFour ) + vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); + else + vRes = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); if ( fVerbose ) { printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c new file mode 100644 index 00000000..ddad5364 --- /dev/null +++ b/src/aig/saig/saigSimExt2.c @@ -0,0 +1,287 @@ +/**CFile**************************************************************** + + FileName [saigSimExt2.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Extending simulation trace to contain ternary values.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigSimExt2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" +#include "ssw.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define SAIG_ZER_NEW 0 // 0 not visited +#define SAIG_ONE_NEW 1 // 1 not visited +#define SAIG_ZER_OLD 2 // 0 visited +#define SAIG_ONE_OLD 3 // 1 visited + +static inline int Saig_ManSimInfo2IsOld( int Value ) +{ + return Value == SAIG_ZER_OLD || Value == SAIG_ONE_OLD; +} + +static inline int Saig_ManSimInfo2SetOld( int Value ) +{ + if ( Value == SAIG_ZER_NEW ) + return SAIG_ZER_OLD; + if ( Value == SAIG_ONE_NEW ) + return SAIG_ONE_OLD; + assert( 0 ); + return 0; +} + +static inline int Saig_ManSimInfo2Not( int Value ) +{ + if ( Value == SAIG_ZER_NEW ) + return SAIG_ONE_NEW; + if ( Value == SAIG_ONE_NEW ) + return SAIG_ZER_NEW; + assert( 0 ); + return 0; +} + +static inline int Saig_ManSimInfo2And( int Value0, int Value1 ) +{ + if ( Value0 == SAIG_ZER_NEW || Value1 == SAIG_ZER_NEW ) + return SAIG_ZER_NEW; + if ( Value0 == SAIG_ONE_NEW && Value1 == SAIG_ONE_NEW ) + return SAIG_ONE_NEW; + assert( 0 ); + return 0; +} + +static inline int Saig_ManSimInfo2Get( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) +{ + unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); + return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1)); +} + +static inline void Saig_ManSimInfo2Set( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value ) +{ + unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); + Value ^= Saig_ManSimInfo2Get( vSimInfo, pObj, iFrame ); + pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1)); +} + +// performs ternary simulation +extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs ternary simulation for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManExtendOneEval2( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) +{ + int Value0, Value1, Value; + Value0 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin0(pObj), iFrame ); + if ( Aig_ObjFaninC0(pObj) ) + Value0 = Saig_ManSimInfo2Not( Value0 ); + if ( Aig_ObjIsPo(pObj) ) + { + Saig_ManSimInfo2Set( vSimInfo, pObj, iFrame, Value0 ); + return Value0; + } + assert( Aig_ObjIsNode(pObj) ); + Value1 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin1(pObj), iFrame ); + if ( Aig_ObjFaninC1(pObj) ) + Value1 = Saig_ManSimInfo2Not( Value1 ); + Value = Saig_ManSimInfo2And( Value0, Value1 ); + Saig_ManSimInfo2Set( vSimInfo, pObj, iFrame, Value ); + return Value; +} + +/**Function************************************************************* + + Synopsis [Performs sensitization analysis for one design.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManSimDataInit2( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo ) +{ + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f, iBit = 0; + Saig_ManForEachLo( p, pObj, i ) + Saig_ManSimInfo2Set( vSimInfo, pObj, 0, Aig_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW ); + for ( f = 0; f <= pCex->iFrame; f++ ) + { + Saig_ManSimInfo2Set( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE_NEW ); + Saig_ManForEachPi( p, pObj, i ) + Saig_ManSimInfo2Set( vSimInfo, pObj, f, Aig_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW ); + Aig_ManForEachNode( p, pObj, i ) + Saig_ManExtendOneEval2( vSimInfo, pObj, f ); + Aig_ManForEachPo( p, pObj, i ) + Saig_ManExtendOneEval2( vSimInfo, pObj, f ); + if ( f == pCex->iFrame ) + break; + Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) + Saig_ManSimInfo2Set( vSimInfo, pObjLo, f+1, Saig_ManSimInfo2Get(vSimInfo, pObjLi, f) ); + } + // make sure the output of the property failed + pObj = Aig_ManPo( p, pCex->iPo ); + return Saig_ManSimInfo2Get( vSimInfo, pObj, pCex->iFrame ); +} + +/**Function************************************************************* + + Synopsis [Performs recursive sensetization analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManExplorePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, Vec_Ptr_t * vSimInfo ) +{ + int Value = Saig_ManSimInfo2Get( vSimInfo, pObj, f ); + if ( Saig_ManSimInfo2IsOld( Value ) ) + return; + Saig_ManSimInfo2Set( vSimInfo, pObj, f, Saig_ManSimInfo2SetOld(Value) ); + if ( (Aig_ObjIsPi(pObj) && f == 0) || Saig_ObjIsPi(p, pObj) || Aig_ObjIsConst1(pObj) ) + return; + if ( Saig_ObjIsLo( p, pObj ) ) + { + assert( f > 0 ); + Saig_ManExplorePaths_rec( p, Saig_ObjLoToLi(p, pObj), f-1, vSimInfo ); + return; + } + if ( Aig_ObjIsPo(pObj) ) + { + Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, vSimInfo ); + return; + } + assert( Aig_ObjIsNode(pObj) ); + if ( Value == SAIG_ZER_OLD ) + Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, vSimInfo ); + else + { + Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, vSimInfo ); + Saig_ManExplorePaths_rec( p, Aig_ObjFanin1(pObj), f, vSimInfo ); + } +} + +/**Function************************************************************* + + Synopsis [Returns the array of PIs for flops that should not be absracted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManProcessCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) +{ + Vec_Int_t * vRes, * vResInv; + int i, f, Value; +// assert( Aig_ManRegNum(p) > 0 ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + // start simulation data + Value = Saig_ManSimDataInit2( p, pCex, vSimInfo ); + assert( Value == SAIG_ONE_NEW ); + // recursively compute justification + Saig_ManExplorePaths_rec( p, Aig_ManPo(p, pCex->iPo), pCex->iFrame, vSimInfo ); + // select the result + vRes = Vec_IntAlloc( 1000 ); + vResInv = Vec_IntAlloc( 1000 ); + for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) + { + for ( f = pCex->iFrame; f >= 0; f-- ) + { + Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManPi(p, i), f ); + if ( Saig_ManSimInfo2IsOld( Value ) ) + break; + } + if ( f >= 0 ) + Vec_IntPush( vRes, i ); + else + Vec_IntPush( vResInv, i ); + } + // resimulate to make sure it is valid + Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); + assert( Value == SAIG_ONE ); + Vec_IntFree( vResInv ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Returns the array of PIs for flops that should not be absracted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ) +{ + Vec_Int_t * vRes; + Vec_Ptr_t * vSimInfo; + int clk; + if ( Saig_ManPiNum(p) != pCex->nPis ) + { + printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", + Aig_ManPiNum(p), pCex->nPis ); + return NULL; + } + Aig_ManFanoutStart( p ); + vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) ); + Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) ); + +clk = clock(); + vRes = Saig_ManProcessCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); + if ( fVerbose ) + { + printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); +ABC_PRT( "Time", clock() - clk ); + } + Vec_PtrFree( vSimInfo ); + Aig_ManFanoutStop( p ); + return vRes; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 958f8d66..c8eccb76 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27467,13 +27467,23 @@ usage: int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp = NULL; - int c, fVerbose = 0; - extern int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fVerbose ); + int c; + int fTryFour = 1; + int fSensePath = 0; + int fVerbose = 0; + + extern int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "tsvh" ) ) != EOF ) { switch ( c ) { + case 't': + fTryFour ^= 1; + break; + case 's': + fSensePath ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -27498,13 +27508,15 @@ int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no counter-example.\n" ); return 1; } - pAbc->Status = Gia_ManCexAbstractionRefine( pAbc->pGia, pAbc->pCex, fVerbose ); + pAbc->Status = Gia_ManCexAbstractionRefine( pAbc->pGia, pAbc->pCex, fTryFour, fSensePath, fVerbose ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: - Abc_Print( -2, "usage: &abs_refine [-vh]\n" ); + Abc_Print( -2, "usage: &abs_refine [-tsvh]\n" ); Abc_Print( -2, "\t refines the pre-computed flop map using the counter-example\n" ); + Abc_Print( -2, "\t-t : toggle trying four abstractions instead of one [default = %s]\n", fTryFour? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle using the path sensitization algorithm [default = %s]\n", fSensePath? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; -- cgit v1.2.3