diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 786 | ||||
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 99 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 197 |
4 files changed, 1074 insertions, 10 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index b4ce11e6..dc3a3b01 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -625,6 +625,8 @@ extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ); extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ); extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver ); +/*=== giaAbsGla.c ===========================================================*/ +extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars ); /*=== giaAbsVta.c ===========================================================*/ extern void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ); extern Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs ); diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 5dac89a6..368505e9 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -20,6 +20,9 @@ #include "gia.h" #include "giaAig.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver2.h" +#include "src/base/main/main.h" ABC_NAMESPACE_IMPL_START @@ -28,6 +31,63 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +typedef struct Gla_Obj_t_ Gla_Obj_t; // object +struct Gla_Obj_t_ +{ + int iGiaObj; // corresponding GIA obj + unsigned fAbs : 1; // belongs to abstraction + unsigned fCompl0 : 1; // compl bit of the first fanin +// unsigned fCompl1 : 1; // compl bit of the second fanin + unsigned fConst : 1; // object attribute + unsigned fPi : 1; // object attribute + unsigned fPo : 1; // object attribute + unsigned fRo : 1; // object attribute + unsigned fRi : 1; // object attribute + unsigned fAnd : 1; // object attribute + unsigned nFanins : 24; // fanin count + int Fanins[4]; // fanins + Vec_Int_t vFrames; // variables in each timeframe +}; + +typedef struct Gla_Man_t_ Gla_Man_t; // manager +struct Gla_Man_t_ +{ + // user data + Gia_Man_t * pGia; // AIG manager + Gia_ParVta_t* pPars; // parameters + // internal data + Gla_Obj_t * pObjs; // objects + int nObjs; // the number of objects + // other data + int nCexes; // the number of counter-examples + int nSatVars; // the number of SAT variables + Cnf_Dat_t * pCnf; // CNF derived for the nodes + sat_solver2 * pSat; // incremental SAT solver + Vec_Int_t * vCla2Obj; // mapping of clauses into GLA objs + Vec_Int_t * vTemp; // temporary array + Vec_Int_t * vAddedNew; // temporary array + // statistics + int timeSat; + int timeUnsat; + int timeCex; + int timeOther; +}; + +// object procedures +static inline int Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; } +static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; } +static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj ); } + +// iterator through abstracted objects +#define Gla_ManForEachObjAbs( p, pObj ) \ + for ( pObj = p->pObjs + 1; pObj < p->pObjs + p->nObjs; pObj++ ) if ( !pObj->fAbs ) {} else +#define Gla_ManForEachObjAbsVec( vVec, p, pObj, i ) \ + for ( i = 0; i < Vec_IntSize(vVec) && ((pObj = Gla_ManObj(p, Vec_IntEntry(vVec, i))),1); i++) + +// iterator through fanins of an abstracted object +#define Gla_ObjForEachFanin( p, pObj, pFanin, i ) \ + for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ ) + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -170,6 +230,732 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose return -1; } + + + + + + +/**Function************************************************************* + + Synopsis [Adds clauses for the given obj in the given frame.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManCollectFanins( Gla_Man_t * p, Gla_Obj_t * pGla, int iObj, Vec_Int_t * vFanins ) +{ + int i, nClauses, iFirstClause, * pLit; + nClauses = p->pCnf->pObj2Count[pGla->iGiaObj]; + iFirstClause = p->pCnf->pObj2Clause[pGla->iGiaObj]; + Vec_IntClear( vFanins ); + for ( i = iFirstClause; i < iFirstClause + nClauses; i++ ) + for ( pLit = p->pCnf->pClauses[i]; pLit < p->pCnf->pClauses[i+1]; pLit++ ) + if ( lit_var(*pLit) != iObj ) + Vec_IntPushUnique( vFanins, lit_var(*pLit) ); + assert( Vec_IntSize( vFanins ) <= 4 ); + Vec_IntSort( vFanins, 0 ); +} + +/**Function************************************************************* + + Synopsis [Creates a new manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) +{ + Gla_Man_t * p; + Aig_Man_t * pAig; + Gia_Obj_t * pObj; + Gla_Obj_t * pGla; + int i, * pLits; + // start + p = ABC_CALLOC( Gla_Man_t, 1 ); + p->pGia = pGia; + p->pPars = pPars; + p->vTemp = Vec_IntAlloc( 100 ); + p->vAddedNew = Vec_IntAlloc( 100 ); + // internal data + pAig = Gia_ManToAigSimple( p->pGia ); + p->pCnf = Cnf_DeriveOther( pAig ); + Aig_ManStop( pAig ); + // count the number of variables + p->nObjs = 1; + Gia_ManForEachObj( p->pGia, pObj, i ) + if ( p->pCnf->pObj2Count[i] >= 0 ) + pObj->Value = p->nObjs++; + else + pObj->Value = ~0; + // re-express CNF using new variable IDs + pLits = p->pCnf->pClauses[0]; + for ( i = 0; i < p->pCnf->nLiterals; i++ ) + { + pObj = Gia_ManObj( p->pGia, lit_var(pLits[i]) ); + assert( ~pObj->Value ); + pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) ); + } + // create objects + p->pObjs = ABC_CALLOC( Gla_Obj_t, p->nObjs ); + Gia_ManForEachObj( p->pGia, pObj, i ) + { + if ( !~pObj->Value ) + continue; + pGla = Gla_ManObj( p, pObj->Value ); + pGla->iGiaObj = i; + pGla->fCompl0 = Gia_ObjFaninC0(pObj); +// pGla->fCompl1 = Gia_ObjFaninC1(pObj); + pGla->fConst = Gia_ObjIsConst0(pObj); + pGla->fPi = Gia_ObjIsPi(p->pGia, pObj); + pGla->fPo = Gia_ObjIsPo(p->pGia, pObj); + pGla->fRi = Gia_ObjIsRi(p->pGia, pObj); + pGla->fRo = Gia_ObjIsRo(p->pGia, pObj); + pGla->fAnd = Gia_ObjIsAnd(pObj); + if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) ) + continue; + if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) ) + { + Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp ); + pGla->fConst = Gia_ObjIsConst0(pObj); + pGla->nFanins = Vec_IntSize( p->vTemp ); + memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) ); + continue; + } + assert( Gia_ObjIsRo(p->pGia, pObj) ); + pGla->nFanins = 1; + pGla->Fanins[0] = Gia_ObjFanin0( Gia_ObjRoToRi(p->pGia, pObj) )->Value; + pGla->fCompl0 = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) ); + } + // abstraction + assert( pGia->vGateClasses != NULL ); + for ( pGla = p->pObjs + 1; pGla < p->pObjs + p->nObjs; pGla++ ) + pGla->fAbs = (Vec_IntEntry( pGia->vGateClasses, pGla->iGiaObj ) == 1); + // other + p->vCla2Obj = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Obj, -1 ); + p->pSat = sat_solver2_new(); + p->nSatVars = 1; + return p; +} + +/**Function************************************************************* + + Synopsis [Creates a new manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManStop( Gla_Man_t * p ) +{ + Gla_Obj_t * pGla; + for ( pGla = p->pObjs + 1; pGla < p->pObjs + p->nObjs; pGla++ ) + ABC_FREE( pGla->vFrames.pArray ); + Cnf_DataFree( p->pCnf ); + sat_solver2_delete( p->pSat ); + Vec_IntFree( p->vCla2Obj ); + Vec_IntFree( p->vAddedNew ); + Vec_IntFree( p->vTemp ); + ABC_FREE( p->pObjs ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Creates a new manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_GlaAbsCount( Gla_Man_t * p, int fRo, int fAnd ) +{ + Gla_Obj_t * pObj; + int Counter = 0; + if ( fRo ) + Gla_ManForEachObjAbs( p, pObj ) + Counter += (pObj->fRo && pObj->fAbs); + else if ( fAnd ) + Gla_ManForEachObjAbs( p, pObj ) + Counter += (pObj->fAnd && pObj->fAbs); + else + Gla_ManForEachObjAbs( p, pObj ) + Counter += (pObj->fAbs); + return Counter; +} + + +/**Function************************************************************* + + Synopsis [Derives new abstraction map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + assert( Gia_ObjIsAnd(pObj) ); + Gla_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vMap ); + Gla_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vMap ); + Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), 1 ); +} +Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p ) +{ + Vec_Int_t * vRes; + Gla_Obj_t * pObj, * pFanin; + Gia_Obj_t * pGiaObj; + int k; + vRes = Vec_IntStart( Gia_ManObjNum(p->pGia) ); + Gla_ManForEachObjAbs( p, pObj ) + { + pGiaObj = Gla_ManGiaObj( p, pObj ); + Vec_IntWriteEntry( vRes, pObj->iGiaObj, 1 ); + if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) ) + continue; + assert( Gia_ObjIsAnd(pGiaObj) ); + Gia_ManIncrementTravId( p->pGia ); + Gla_ObjForEachFanin( p, pObj, pFanin, k ) + Gia_ObjSetTravIdCurrent( p->pGia, Gla_ManGiaObj(p, pFanin) ); + Gla_ManTranslate_rec( p->pGia, Gla_ManGiaObj(p, pObj), vRes ); + } + return vRes; +} + + +/**Function************************************************************* + + Synopsis [Collect pseudo-PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p ) +{ + Vec_Int_t * vPPis; + Gla_Obj_t * pObj, * pFanin; + int k; + vPPis = Vec_IntAlloc( 1000 ); + Gla_ManForEachObjAbs( p, pObj ) + { + assert( pObj->fConst || pObj->fRo || pObj->fAnd ); + Gla_ObjForEachFanin( p, pObj, pFanin, k ) + if ( !pFanin->fPi && !pFanin->fAbs ) + Vec_IntPush( vPPis, pObj->Fanins[k] ); + } + Vec_IntUniqify( vPPis ); + Vec_IntReverseOrder( vPPis ); + return vPPis; +} +int Gla_ManCountPPis( Gla_Man_t * p ) +{ + Vec_Int_t * vPPis = Gla_ManCollectPPis( p ); + int RetValue = Vec_IntSize( vPPis ); + Vec_IntFree( vPPis ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Adds CNF for the given timeframe.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame ) +{ + Gla_Obj_t * pGla = Gla_ManObj( p, iObj ); + int iVar = Vec_IntGetEntry( &pGla->vFrames, iFrame ); + assert( !pGla->fPo && !pGla->fRi ); + if ( iVar == 0 ) + { + Vec_IntSetEntry( &pGla->vFrames, iFrame, (iVar = p->nSatVars++) ); + // remember the change + Vec_IntPush( p->vAddedNew, iObj ); + Vec_IntPush( p->vAddedNew, iFrame ); + } + return iVar; +} +void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits ) +{ + Gla_Obj_t * pGlaObj = Gla_ManObj( p, iObj ); + int iVar, iVar1, iVar2; + if ( iObj == 4753 ) + { + int s = 0; + } + if ( pGlaObj->fConst ) + { + iVar = Gla_ManGetVar( p, iObj, iFrame ); + sat_solver2_add_const( p->pSat, iVar, 1, 0 ); + // remember the clause + Vec_IntPush( p->vCla2Obj, iObj ); + } + else if ( pGlaObj->fRo ) + { + assert( pGlaObj->nFanins == 1 ); + if ( iFrame == 0 ) + { + iVar = Gla_ManGetVar( p, iObj, iFrame ); + sat_solver2_add_const( p->pSat, iVar, 1, 0 ); + // remember the clause + Vec_IntPush( p->vCla2Obj, iObj ); + } + else + { + iVar1 = Gla_ManGetVar( p, iObj, iFrame ); +// pGlaObj = Gla_ManObj( p, pGlaObj->Fanins[0] ); +// assert( pGlaObj->fRo && pGlaObj->nFanins == 1 ); +// assert( Vec_IntSize(&pGlaObj->vFrames) == 0 ); + iVar2 = Gla_ManGetVar( p, pGlaObj->Fanins[0], iFrame-1 ); + sat_solver2_add_buffer( p->pSat, iVar1, iVar2, pGlaObj->fCompl0, 0 ); + // remember the clause + Vec_IntPush( p->vCla2Obj, iObj ); + Vec_IntPush( p->vCla2Obj, iObj ); + } + } + else if ( pGlaObj->fAnd ) + { + int i, RetValue, nClauses, iFirstClause, * pLit; + nClauses = p->pCnf->pObj2Count[pGlaObj->iGiaObj]; + iFirstClause = p->pCnf->pObj2Clause[pGlaObj->iGiaObj]; + for ( i = iFirstClause; i < iFirstClause + nClauses; i++ ) + { + Vec_IntClear( vLits ); + for ( pLit = p->pCnf->pClauses[i]; pLit < p->pCnf->pClauses[i+1]; pLit++ ) + { + iVar = Gla_ManGetVar( p, lit_var(*pLit), iFrame ); + Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) ); + } + RetValue = sat_solver2_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); + assert( RetValue ); + // remember the clause + Vec_IntPush( p->vCla2Obj, iObj ); + } + } + else assert( 0 ); +} +void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck ) +{ + Gla_Obj_t * pGla; + int i; + Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i ) + { + assert( !fCheck || pGla->fAbs == 0 ); + pGla->fAbs = 1; + // remember the change + Vec_IntPush( p->vAddedNew, Gla_ObjId(p, pGla) ); + Vec_IntPush( p->vAddedNew, -1 ); + } +} +void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f ) +{ + Gla_Obj_t * pObj; + Gla_ManForEachObjAbs( p, pObj ) + Gla_ManAddClauses( p, Gla_ObjId(p, pObj), f, p->vTemp ); + sat_solver2_simplify( p->pSat ); +} +void Gia_GlaAddOneSlice( Gla_Man_t * p, int fCur, Vec_Int_t * vCore ) +{ + int f, i, iGlaObj; + for ( f = fCur; f >= 0; f-- ) + Vec_IntForEachEntry( vCore, iGlaObj, i ) + Gla_ManAddClauses( p, iGlaObj, f, p->vTemp ); + sat_solver2_simplify( p->pSat ); +} +void Gla_ManRollBack( Gla_Man_t * p ) +{ + int i, iObj, iFrame; + Vec_IntForEachEntryDouble( p->vAddedNew, iObj, iFrame, i ) + { + if ( iFrame == -1 ) + { + assert( Gla_ManObj(p, iObj)->fAbs == 1 ); + Gla_ManObj(p, iObj)->fAbs = 0; + } + else + { + assert( Vec_IntEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame ) > 0 ); + Vec_IntWriteEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame, 0 ); + } + } +} + + + + + +/**Function************************************************************* + + Synopsis [Finds the set of clauses involved in the UNSAT core.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gla_ManGetOutLit( Gla_Man_t * p, int f ) +{ + Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0); + Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj); + Gla_Obj_t * pGla = Gla_ManObj(p, pFanin->Value); + int iSat = Vec_IntEntry( &pGla->vFrames, f ); + assert( iSat > 0 ); + return Abc_Var2Lit( iSat, Gia_ObjFaninC0(pObj) ); +} +Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls ) +{ + Vec_Int_t * vCore; + int iLit = Gla_ManGetOutLit( p, f ); + int nConfPrev = pSat->stats.conflicts; + int i, Entry, RetValue, clk = clock(); + if ( piRetValue ) + *piRetValue = 1; + // solve the problem + RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( pnConfls ) + *pnConfls = (int)pSat->stats.conflicts - nConfPrev; + if ( RetValue == l_Undef ) + { + if ( piRetValue ) + *piRetValue = -1; + return NULL; + } + if ( RetValue == l_True ) + { + if ( piRetValue ) + *piRetValue = 0; + return NULL; + } + if ( fVerbose ) + { +// Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev ); +// Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts ); +// Abc_PrintTime( 1, "Time", clock() - clk ); + } + assert( RetValue == l_False ); + + // derive the UNSAT core + clk = clock(); + vCore = (Vec_Int_t *)Sat_ProofCore( pSat ); + if ( fVerbose ) + { +// Abc_Print( 1, "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) ); +// Abc_PrintTime( 1, "Time", clock() - clk ); + } + + // remap core into original objects + Vec_IntForEachEntry( vCore, Entry, i ) + Vec_IntWriteEntry( vCore, i, Vec_IntEntry(p->vCla2Obj, Entry) ); + Vec_IntUniqify( vCore ); + Vec_IntReverseOrder( vCore ); + if ( fVerbose ) + { +// Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) ); +// Abc_PrintTime( 1, "Time", clock() - clk ); + } + return vCore; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, int Time ) +{ + Abc_Print( 1, "%3d :", nFrames-1 ); + Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 0) ); + Abc_Print( 1, "%5d", Gla_ManCountPPis(p) ); + Abc_Print( 1, "%5d", Gia_GlaAbsCount(p, 1, 0) ); + Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 1) ); + Abc_Print( 1, "%8d", nConfls ); + if ( nCexes == 0 ) + Abc_Print( 1, "%5c", '-' ); + else + Abc_Print( 1, "%5d", nCexes ); + Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); + Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); + Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) ); + Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" ); + fflush( stdout ); +} +void Gla_ManReportMemory( Gla_Man_t * p ) +{ + Gla_Obj_t * pGla; + double memTot = 0; + double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t); + double memSat = sat_solver2_memory( p->pSat ); + double memPro = sat_solver2_memory_proof( p->pSat ); + double memMap = p->nObjs * sizeof(Gla_Obj_t); + double memOth = sizeof(Gla_Man_t); + for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ ) + memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int); + memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int); + memOth += Vec_IntCap(p->vAddedNew) * sizeof(int); + memOth += Vec_IntCap(p->vTemp) * sizeof(int); + memTot = memAig + memSat + memPro + memMap + memOth; + ABC_PRMP( "Memory: AIG ", memAig, memTot ); + ABC_PRMP( "Memory: SAT ", memSat, memTot ); + ABC_PRMP( "Memory: Proof", memPro, memTot ); + ABC_PRMP( "Memory: Map ", memMap, memTot ); + ABC_PRMP( "Memory: Other", memOth, memTot ); + ABC_PRMP( "Memory: TOTAL", memTot, memTot ); +} + + +/**Function************************************************************* + + Synopsis [Send abstracted model or send cancel.] + + Description [Counter-example will be sent automatically when &vta terminates.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose ) +{ + char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"; + Gia_Man_t * pAbs; + if ( fVerbose ) + Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName ); +// if ( !Abc_FrameIsBridgeMode() ) +// return; + // create gate classes + Vec_IntFreeP( &p->pGia->vGateClasses ); + p->pGia->vGateClasses = Gla_ManTranslate( p ); + // create abstrated model + pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses ); + Vec_IntFreeP( &p->pGia->vGateClasses ); + // send it out + Gia_WriteAiger( pAbs, pFileName, 0, 0 ); + Gia_ManStop( pAbs ); +} + + +/**Function************************************************************* + + Synopsis [Performs gate-level abstraction] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) +{ + Gla_Man_t * p; + Vec_Int_t * vCore, * vPPis; + Abc_Cex_t * pCex = NULL; + int i, f, nConfls, Status, nCoreSize, RetValue = -1; + int clk = clock(), clk2; + // preconditions + assert( Gia_ManPoNum(pAig) == 1 ); + assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); + // start the manager + p = Gla_ManStart( pAig, pPars ); + p->pSat->fVerbose = p->pPars->fVerbose; + sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax ); + // set runtime limit + if ( p->pPars->nTimeOut ) + sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 ); + // perform initial abstraction + if ( p->pPars->fVerbose ) + { + Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" ); + Abc_Print( 1, "FrameStart = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n", + p->pPars->nFramesStart, p->pPars->nFramesMax, p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin ); + Abc_Print( 1, "Frame Abs PPI FF AND Confl Cex Core SatVar Time\n" ); + } + for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ ) + { + int nConflsBeg = sat_solver2_nconflicts(p->pSat); + p->pPars->iFrame = f; + // load timeframe + Gia_GlaAddTimeFrame( p, f ); + // create bookmark to be used for rollback +// sat_solver2_reducedb( p->pSat ); + sat_solver2_bookmark( p->pSat ); + Vec_IntClear( p->vAddedNew ); +// nClaOld = Vec_IntSize( p->vCla2Obj ); + // iterate as long as there are counter-examples + for ( i = 0; ; i++ ) + { + clk2 = clock(); + vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); + assert( (vCore != NULL) == (Status == 1) ); + if ( Status == -1 ) // resource limit is reached + goto finish; + if ( vCore != NULL ) + { + p->timeUnsat += clock() - clk2; + break; + } + p->timeSat += clock() - clk2; + assert( Status == 0 ); + p->nCexes++; + // perform the refinement + clk2 = clock(); +// pCex = Vta_ManRefineAbstraction( p, f ); + pCex = NULL; + + vPPis = Gla_ManCollectPPis( p ); + Gia_GlaAddToAbs( p, vPPis, 1 ); + Gia_GlaAddOneSlice( p, f, vPPis ); + Vec_IntFree( vPPis ); + + p->timeCex += clock() - clk2; + if ( pCex != NULL ) + { + RetValue = 0; + goto finish; + } + // print the result (do not count it towards change) + if ( p->pPars->fVerbose ) + Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk ); + } + assert( Status == 1 ); + // valid core is obtained + nCoreSize = Vec_IntSize(vCore); + if ( i == 0 ) + Vec_IntFree( vCore ); + else + { + // update the SAT solver + sat_solver2_rollback( p->pSat ); + // update storage + Gla_ManRollBack( p ); + Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 ); + // load this timeframe + Gia_GlaAddToAbs( p, vCore, 0 ); + Gia_GlaAddOneSlice( p, f, vCore ); + Vec_IntFree( vCore ); + // run SAT solver + clk2 = clock(); + vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); + p->timeUnsat += clock() - clk2; + assert( (vCore != NULL) == (Status == 1) ); + Vec_IntFree( vCore ); + if ( Status == -1 ) // resource limit is reached + break; + if ( Status == 0 ) + { + // Vta_ManSatVerify( p ); + // make sure, there was no initial abstraction (otherwise, it was invalid) + assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart ); + // pCex = Vga_ManDeriveCex( p ); + RetValue = 0; + break; + } + } + // print the result + if ( p->pPars->fVerbose ) + Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk ); + + // dump the model + if ( p->pPars->fDumpVabs && (f & 1) ) + { + Abc_FrameSetCex( NULL ); + Abc_FrameSetNFrames( f+1 ); + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "write_status gla.status" ); + Gia_GlaDumpAbsracted( p, pPars->fVerbose ); + } + + // check if the number of objects is below limit + if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 ) + { + Status = -1; + break; + } + } +finish: + // analize the results + if ( pCex == NULL ) + { + if ( pAig->vGateClasses != NULL ) + Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); + Vec_IntFreeP( &pAig->vGateClasses ); + pAig->vGateClasses = Gla_ManTranslate( p ); + if ( Status == -1 ) + { + if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) + Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f ); + else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) + Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f ); + else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 ) + Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f ); + else + Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f ); + } + else + Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); + } + else + { + ABC_FREE( p->pGia->pCexSeq ); + p->pGia->pCexSeq = pCex; + if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) ) + Abc_Print( 1, " Gia_GlaPerform(): CEX verification has failed!\n" ); + Abc_Print( 1, "Counter-example detected in frame %d. ", f ); + p->pPars->iFrame = pCex->iFrame - 1; + } + Abc_PrintTime( 1, "Time", clock() - clk ); + + p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex; + ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk ); + ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk ); + ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); + ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); + ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); + Gla_ManReportMemory( p ); + + Gla_ManStop( p ); + fflush( stdout ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index cf19947a..17a85bad 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -57,6 +57,7 @@ struct Gia_ManBmc_t_ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +#define SAIG_TER_NON 0 #define SAIG_TER_ZER 1 #define SAIG_TER_ONE 2 #define SAIG_TER_UND 3 @@ -91,6 +92,13 @@ static inline void Saig_ManBmcSimInfoSet( unsigned * pInfo, Aig_Obj_t * pObj, in pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1)); } +static inline int Saig_ManBmcSimInfoClear( unsigned * pInfo, Aig_Obj_t * pObj ) +{ + int Value = Saig_ManBmcSimInfoGet( pInfo, pObj ); + pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1)); + return Value; +} + /**Function************************************************************* Synopsis [Returns the number of LIs with binary ternary info.] @@ -220,6 +228,97 @@ void Saig_ManBmcTerSimTest( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Count the number of non-ternary per frame.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManBmcCountNonternary_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vInfos, unsigned * pInfo, int f, int * pCounter ) +{ + int Value = Saig_ManBmcSimInfoClear( pInfo, pObj ); + if ( Value == SAIG_TER_NON ) + return 0; + assert( f >= 0 ); + pCounter[f] += (Value == SAIG_TER_UND); + if ( Saig_ObjIsPi(p, pObj) || (f == 0 && Saig_ObjIsLo(p, pObj)) || Aig_ObjIsConst1(pObj) ) + return 0; + if ( Saig_ObjIsLi(p, pObj) ) + return Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter ); + if ( Saig_ObjIsLo(p, pObj) ) + return Saig_ManBmcCountNonternary_rec( p, Saig_ObjLoToLi(p, pObj), vInfos, (unsigned *)Vec_PtrEntry(vInfos, f-1), f-1, pCounter ); + assert( Aig_ObjIsNode(pObj) ); + Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter ); + Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin1(pObj), vInfos, pInfo, f, pCounter ); + return 0; +} +void Saig_ManBmcCountNonternary( Aig_Man_t * p, Vec_Ptr_t * vInfos, int iFrame ) +{ + int i, * pCounters = ABC_CALLOC( int, iFrame + 1 ); + unsigned * pInfo = (unsigned *)Vec_PtrEntry(vInfos, iFrame); + assert( Saig_ManBmcSimInfoGet( pInfo, Aig_ManCo(p, 0) ) == SAIG_TER_UND ); + Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(Aig_ManCo(p, 0)), vInfos, pInfo, iFrame, pCounters ); + for ( i = 0; i <= iFrame; i++ ) + printf( "%d=%d ", i, pCounters[i] ); + printf( "\n" ); + ABC_FREE( pCounters ); +} + + +/**Function************************************************************* + + Synopsis [Returns the number of POs with binary ternary info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManBmcTerSimCount01Po( Aig_Man_t * p, unsigned * pInfo ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Saig_ManForEachPo( p, pObj, i ) + Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND); + return Counter; +} +Vec_Ptr_t * Saig_ManBmcTerSimPo( Aig_Man_t * p ) +{ + Vec_Ptr_t * vInfos; + unsigned * pInfo = NULL; + int i, nPoBin; + vInfos = Vec_PtrAlloc( 100 ); + for ( i = 0; ; i++ ) + { + if ( i % 100 == 0 ) + printf( "Frame %5d\n", i ); + pInfo = Saig_ManBmcTerSimOne( p, pInfo ); + Vec_PtrPush( vInfos, pInfo ); + nPoBin = Saig_ManBmcTerSimCount01Po( p, pInfo ); + if ( nPoBin < Saig_ManPoNum(p) ) + break; + } + printf( "Detected terminary PO in frame %d.\n", i ); + Saig_ManBmcCountNonternary( p, vInfos, i ); + return vInfos; +} +void Saig_ManBmcTerSimTestPo( Aig_Man_t * p ) +{ + Vec_Ptr_t * vInfos; + vInfos = Saig_ManBmcTerSimPo( p ); + Vec_PtrFreeFree( vInfos ); +} + + + + +/**Function************************************************************* + Synopsis [Collects internal nodes in the DFS order.] Description [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c7c811f0..2b0bd0af 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -349,6 +349,7 @@ static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9GlaRefine ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Gla ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Vta ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Vta2Gla ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -793,6 +794,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&gla_refine", Abc_CommandAbc9GlaRefine, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&gla", Abc_CommandAbc9Gla, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&vta", Abc_CommandAbc9Vta, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&vta_gla", Abc_CommandAbc9Vta2Gla, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 ); @@ -9211,20 +9213,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig ); extern Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap ); extern void Abc2_NtkTestGia( char * pFileName, int fVerbose ); + extern void Saig_ManBmcTerSimTestPo( Aig_Man_t * p ); if ( pNtk ) { -/* + Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); - if ( fNewAlgo ) - Saig_IsoDetectFast( pAig ); - else - { - Aig_Man_t * pRes = Iso_ManTest( pAig, fVerbose ); - Aig_ManStopP( &pRes ); - } + Saig_ManBmcTerSimTestPo( pAig ); Aig_ManStop( pAig ); -*/ + /* extern Abc_Ntk_t * Abc_NtkShareXor( Abc_Ntk_t * pNtk ); Abc_Ntk_t * pNtkRes = Abc_NtkShareXor( pNtk ); @@ -27370,6 +27367,186 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_ParVta_t Pars, * pPars = &Pars; + int c; + Gia_VtaSetDefaultParams( pPars ); + pPars->nLearntMax = 100000; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesMax < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesStart = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesStart < 0 ) + goto usage; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesPast = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesPast < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nConfLimit < 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLearntMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLearntMax < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTimeOut < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nRatioMin = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nRatioMin < 0 ) + goto usage; + break; + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by a file name.\n" ); + goto usage; + } + pPars->pFileVabs = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 't': + pPars->fUseTermVars ^= 1; + break; + case 'r': + pPars->fUseRollback ^= 1; + break; + case 'd': + pPars->fDumpVabs ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "There is no AIG.\n" ); + return 0; + } + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + Abc_Print( -1, "The network is combinational.\n" ); + return 0; + } + if ( Gia_ManPoNum(pAbc->pGia) > 1 ) + { + Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" ); + return 0; + } + if ( pPars->nFramesMax < 0 ) + { + Abc_Print( 1, "The number of starting frames should be a positive integer.\n" ); + return 0; + } + if ( pPars->nFramesMax && pPars->nFramesStart > pPars->nFramesMax ) + { + Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" ); + return 0; + } + if ( pPars->nFramesStart < 1 ) + { + Abc_Print( 1, "The starting frame should be 1 or larger.\n" ); + return 0; + } + pAbc->Status = Gia_GlaPerform( pAbc->pGia, pPars ); + pAbc->nFrames = pPars->iFrame; + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + return 0; + +usage: + Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-dvh]\n" ); + Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" ); + Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); + Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart ); +// Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast ); + Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit ); + Abc_Print( -2, "\t-L num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearntMax ); + Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); + Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin ); + Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" ); +// Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" ); +// Abc_Print( -2, "\t-r : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_ParVta_t Pars, * pPars = &Pars; @@ -27486,7 +27663,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" ); + Abc_Print( -1, "There is no AIG.\n" ); return 1; } if ( Gia_ManRegNum(pAbc->pGia) == 0 ) |