From 7b734f23fc23694ccffdb7e3cd31335ffe6cb272 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 5 Jul 2008 08:01:00 -0700 Subject: Version abc80705 --- abc.rc | 2 +- src/aig/cnf/cnf.h | 2 + src/aig/cnf/cnfMan.c | 93 +++++++++++++++++++++++++++++++- src/aig/cnf/cnfUtil.c | 1 + src/aig/fra/fra.h | 2 +- src/aig/fra/fraCec.c | 35 +++++++++--- src/aig/fra/fraInd.c | 2 + src/aig/ntl/ntl.h | 1 + src/aig/ntl/ntlExtract.c | 4 +- src/aig/ntl/ntlFraig.c | 4 ++ src/aig/ntl/ntlUtil.c | 58 ++++++++++++++++++-- src/aig/nwk/nwkTiming.c | 20 +++---- src/aig/saig/saigInter.c | 2 +- src/base/abc/abc.h | 1 + src/base/abc/abcDfs.c | 27 ++++++++++ src/base/abci/abc.c | 114 ++++++++++++++++++++++++++++++++++++--- src/base/abci/abcDar.c | 15 +++--- src/base/abci/abcStrash.c | 133 ++++++++++++++++++++++++++++++++++++++++++++-- src/base/cmd/cmdApi.c | 2 +- src/base/cmd/cmdInt.h | 3 +- src/base/cmd/cmdUtils.c | 43 +++++++++++++-- src/base/io/io.c | 6 ++- src/base/main/main.c | 4 +- 23 files changed, 520 insertions(+), 54 deletions(-) diff --git a/abc.rc b/abc.rc index 526a08de..e0304667 100644 --- a/abc.rc +++ b/abc.rc @@ -2,7 +2,7 @@ #set check # checks intermediate networks #set checkfio # prints warnings when fanins/fanouts are duplicated #set checkread # checks new networks after reading from file -set backup # saves backup networks retrived by "undo" and "recall" +#set backup # saves backup networks retrived by "undo" and "recall" set savesteps 1 # sets the maximum number of backup networks to save set progressbar # display the progress bar diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index bf109b17..5c742f5d 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -140,6 +140,8 @@ extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); extern int Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf ); +extern int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ); +extern void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf ); /*=== cnfMap.c ========================================================*/ extern void Cnf_DeriveMapping( Cnf_Man_t * p ); extern int Cnf_ManMapForCnf( Cnf_Man_t * p ); diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index fc71f936..e3e6bfe1 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -20,6 +20,7 @@ #include "cnf.h" #include "satSolver.h" +#include "zlib.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -237,7 +238,7 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ) SeeAlso [] ***********************************************************************/ -void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) +void Cnf_DataWriteIntoFile_old( Cnf_Dat_t * p, char * pFileName, int fReadable ) { FILE * pFile; int * pLit, * pStop, i; @@ -259,6 +260,39 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) fclose( pFile ); } +/**Function************************************************************* + + Synopsis [Writes CNF into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) +{ + gzFile pFile; + int * pLit, * pStop, i; + pFile = gzopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" ); + return; + } + gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); + gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); + for ( i = 0; i < p->nClauses; i++ ) + { + for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) + gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); + gzprintf( pFile, "0\n" ); + } + gzprintf( pFile, "\n" ); + gzclose( pFile ); +} + /**Function************************************************************* Synopsis [Writes CNF into a file.] @@ -379,6 +413,63 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) return 1; } +/**Function************************************************************* + + Synopsis [Adds the OR-clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ) +{ + sat_solver * pSat = p; + Aig_Obj_t * pObj; + int i, Lit; + Aig_ManForEachPo( pCnf->pMan, pObj, i ) + { + Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Transforms polarity of the internal veriables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf ) +{ + Aig_Obj_t * pObj; + int * pVarToPol; + int i, iVar; + // create map from the variable number to its polarity + pVarToPol = CALLOC( int, pCnf->nVars ); + Aig_ManForEachObj( pCnf->pMan, pObj, i ) + if ( !Aig_ObjIsPo(pObj) && pCnf->pVarNums[pObj->Id] >= 0 ) + pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase; + // transform literals + for ( i = 0; i < pCnf->nLiterals; i++ ) + { + iVar = lit_var(pCnf->pClauses[0][i]); + assert( iVar < pCnf->nVars ); + if ( pVarToPol[iVar] ) + pCnf->pClauses[0][i] = lit_neg( pCnf->pClauses[0][i] ); + } + free( pVarToPol ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c index cd47cb58..3738fee5 100644 --- a/src/aig/cnf/cnfUtil.c +++ b/src/aig/cnf/cnfUtil.c @@ -140,6 +140,7 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped else { pCutBest = pObj->pData; +// assert( pCutBest->nFanins > 0 ); assert( pCutBest->Cost < 127 ); aArea = pCutBest->Cost; Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i ) diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index e9e7ad9c..6721634e 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -282,7 +282,7 @@ static inline int Fra_ImpCreate( int Left, int Right ) //////////////////////////////////////////////////////////////////////// /*=== fraCec.c ========================================================*/ -extern int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ); +extern int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); extern int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose ); extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose ); /*=== fraClass.c ========================================================*/ diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index d67839a4..e5940992 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -40,7 +40,7 @@ SeeAlso [] ***********************************************************************/ -int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ) +int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ) { sat_solver * pSat; Cnf_Dat_t * pCnf; @@ -53,6 +53,10 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe // derive CNF pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); // pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); + + if ( fFlipBits ) + Cnf_DataTranformPolarity( pCnf ); + // convert into SAT solver pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); if ( pSat == NULL ) @@ -60,12 +64,27 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe Cnf_DataFree( pCnf ); return 1; } - // add the OR clause for the outputs - if ( !Cnf_DataWriteOrClause( pSat, pCnf ) ) + + + if ( fAndOuts ) { - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); - return 1; + // assert each output independently + if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) ) + { + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } + } + else + { + // add the OR clause for the outputs + if ( !Cnf_DataWriteOrClause( pSat, pCnf ) ) + { + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } } vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); Cnf_DataFree( pCnf ); @@ -160,7 +179,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose ) // if SAT only, solve without iteration clk = clock(); - RetValue = Fra_FraigSat( pAig, (sint64)2*nBTLimitStart, (sint64)0, 0 ); + RetValue = Fra_FraigSat( pAig, (sint64)2*nBTLimitStart, (sint64)0, 1, 0, 0 ); if ( fVerbose ) { printf( "Initial SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) ); @@ -228,7 +247,7 @@ PRT( "Time", clock() - clk ); if ( RetValue == -1 ) { clk = clock(); - RetValue = Fra_FraigSat( pAig, (sint64)nBTLimitLast, (sint64)0, 0 ); + RetValue = Fra_FraigSat( pAig, (sint64)nBTLimitLast, (sint64)0, 1, 0, 0 ); if ( fVerbose ) { printf( "Final SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index ab076472..1935bb7f 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -437,6 +437,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams ) // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); + p->pPars->nBTLimitNode = 0; // derive and refine e-classes using K initialized frames if ( fUseOldSimulation ) { @@ -529,6 +530,7 @@ p->timeTrav += clock() - clk2; pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); else pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); +// Cnf_DataTranformPolarity( pCnf ); //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index e1d3edd1..b0f3b1fb 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -377,6 +377,7 @@ extern ABC_DLL void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManSetZeroInitValues( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManTransformInitValues( Ntl_Man_t * p ); extern ABC_DLL Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVerbose ); +extern ABC_DLL void Ntl_ManFilterRegisterClasses( Aig_Man_t * pAig, Vec_Int_t * vRegClasses, int fVerbose ); extern ABC_DLL int Ntl_ManLatchNum( Ntl_Man_t * p ); extern ABC_DLL int Ntl_ManIsComb( Ntl_Man_t * p ); extern ABC_DLL int Ntl_ModelCombLeafNum( Ntl_Mod_t * p ); diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index f6f1ebb2..f4d33cf1 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -649,9 +649,9 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize ) if ( pAig->vClockDoms ) { if ( Vec_VecSize(pAig->vClockDoms) == 0 ) - printf( "Clock domains are small. Seq synthesis is not performed.\n" ); + printf( "Register classes are small. Seq synthesis is not performed.\n" ); else - printf( "Performing seq synthesis for %d clock domains.\n", Vec_VecSize(pAig->vClockDoms) ); + printf( "Performing seq synthesis for %d register classes.\n", Vec_VecSize(pAig->vClockDoms) ); printf( "\n" ); } return pAig; diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 6449cc33..bd39956e 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -320,6 +320,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe // perform SCL for the given design pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose ); Aig_ManStop( pTemp ); + if ( pNew->vRegClasses && Vec_IntSize(pNew->vRegClasses) && pAigCol->pReprs ) + Ntl_ManFilterRegisterClasses( pAigCol, pNew->vRegClasses, fVerbose ); // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose ); @@ -353,6 +355,8 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) // perform SCL for the given design pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 ); Aig_ManStop( pTemp ); + if ( p->vRegClasses && Vec_IntSize(p->vRegClasses) && pAigCol->pReprs ) + Ntl_ManFilterRegisterClasses( pAigCol, p->vRegClasses, fVerbose ); // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose ); diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c index 4fd1762c..51f3b818 100644 --- a/src/aig/ntl/ntlUtil.c +++ b/src/aig/ntl/ntlUtil.c @@ -403,7 +403,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer printf( "The number of register clases = %d.\n", nClasses ); for ( i = 0; i <= ClassMax; i++ ) if ( pClassNums[i] ) - printf( "%d:%d ", i, pClassNums[i] ); + printf( "(%d, %d) ", i, pClassNums[i] ); printf( "\n" ); } // skip if there is only one class @@ -416,7 +416,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer vPart = Vec_IntStartNatural( Vec_IntSize(pMan->vRegClasses) ); Vec_PtrPush( vParts, vPart ); } - printf( "There is only one clock domain with %d registers.\n", Vec_IntSize(pMan->vRegClasses) ); + printf( "There is only one class with %d registers.\n", Vec_IntSize(pMan->vRegClasses) ); free( pClassNums ); return (Vec_Vec_t *)vParts; } @@ -434,17 +434,69 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer Vec_PtrPush( vParts, vPart ); } free( pClassNums ); + Vec_VecSort( (Vec_Vec_t *)vParts, 1 ); // report the selected classes if ( fVerbose ) { printf( "The number of selected register clases = %d.\n", Vec_PtrSize(vParts) ); Vec_PtrForEachEntry( vParts, vPart, i ) - printf( "%d:%d ", i, Vec_IntSize(vPart) ); + printf( "(%d, %d) ", i, Vec_IntSize(vPart) ); printf( "\n" ); } return (Vec_Vec_t *)vParts; } +/**Function************************************************************* + + Synopsis [Filter register clases using clock-domain information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManFilterRegisterClasses( Aig_Man_t * pAig, Vec_Int_t * vRegClasses, int fVerbose ) +{ + Aig_Obj_t * pObj, * pRepr; + int i, k, nOmitted, nTotal; + if ( pAig->pReprs == NULL ) + return; + assert( pAig->nRegs > 0 ); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->PioNum = -1; + k = 0; + Aig_ManForEachLoSeq( pAig, pObj, i ) + pObj->PioNum = k++; + // consider equivalences + nOmitted = nTotal = 0; + Aig_ManForEachObj( pAig, pObj, i ) + { + pRepr = pAig->pReprs[pObj->Id]; + if ( pRepr == NULL ) + continue; + nTotal++; + assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsPi(pRepr) || Aig_ObjIsConst1(pRepr) ); + if ( Aig_ObjIsConst1(pRepr) ) + continue; + assert( pObj->PioNum >= 0 && pRepr->PioNum >= 0 ); + // remove equivalence if they belong to different classes + if ( Vec_IntEntry( vRegClasses, pObj->PioNum ) == + Vec_IntEntry( vRegClasses, pRepr->PioNum ) ) + continue; + pAig->pReprs[pObj->Id] = NULL; + nOmitted++; + } + Aig_ManForEachPi( pAig, pObj, i ) + pObj->PioNum = -1; + if ( fVerbose ) + printf( "Omitted %d (out of %d) equivs due to register class mismatch.\n", + nOmitted, nTotal ); +} + + /**Function************************************************************* Synopsis [Counts the number of CIs in the model.] diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c index 64508474..fc56b387 100644 --- a/src/aig/nwk/nwkTiming.c +++ b/src/aig/nwk/nwkTiming.c @@ -589,14 +589,14 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj ) { if ( pManTime ) { - // it may happen that a box-input (CO) was already marked as visited - // when some other box-input of the same box was visited - here we undo this iBox = Tim_ManBoxForCo( pManTime, pTemp->PioId ); - if ( Tim_ManIsCoTravIdCurrent( pManTime, pTemp->PioId ) ) - Tim_ManSetPreviousTravIdBoxInputs( pManTime, iBox ); - Tim_ManSetCoArrival( pManTime, pTemp->PioId, tArrival ); if ( iBox >= 0 ) // this CO is an input of the box { + // it may happen that a box-input (CO) was already marked as visited + // when some other box-input of the same box was visited - here we undo this + if ( Tim_ManIsCoTravIdCurrent( pManTime, pTemp->PioId ) ) + Tim_ManSetPreviousTravIdBoxInputs( pManTime, iBox ); + Tim_ManSetCoArrival( pManTime, pTemp->PioId, tArrival ); Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox ); iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox ); nTerms = Tim_ManBoxOutputNum( pManTime, iBox ); @@ -673,14 +673,14 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj ) { if ( pManTime ) { - // it may happen that a box-output (CI) was already marked as visited - // when some other box-output of the same box was visited - here we undo this iBox = Tim_ManBoxForCi( pManTime, pTemp->PioId ); - if ( Tim_ManIsCiTravIdCurrent( pManTime, pTemp->PioId ) ) - Tim_ManSetPreviousTravIdBoxOutputs( pManTime, iBox ); - Tim_ManSetCiRequired( pManTime, pTemp->PioId, tRequired ); if ( iBox >= 0 ) // this CI is an output of the box { + // it may happen that a box-output (CI) was already marked as visited + // when some other box-output of the same box was visited - here we undo this + if ( Tim_ManIsCiTravIdCurrent( pManTime, pTemp->PioId ) ) + Tim_ManSetPreviousTravIdBoxOutputs( pManTime, iBox ); + Tim_ManSetCiRequired( pManTime, pTemp->PioId, tRequired ); Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox ); iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox ); nTerms = Tim_ManBoxInputNum( pManTime, iBox ); diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index afc4a34a..ae8d02ec 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -412,7 +412,7 @@ int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ) pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); RetValue = Fra_FraigMiterStatus( pAigTemp ); Aig_ManStop( pAigTemp ); -// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0 ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); } assert( RetValue != -1 ); Aig_ManStop( pMiter ); diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 9cb7a855..09ea8b16 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -589,6 +589,7 @@ extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsReverseNodesContained( Abc_Ntk_t * p extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsSeq( Abc_Ntk_t * pNtk ); extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk ); extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll ); +extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsIterNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots ); extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsHie( Abc_Ntk_t * pNtk, int fCollectAll ); extern ABC_DLL bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk ); extern ABC_DLL Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index 8759500b..e83bd132 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -558,6 +558,33 @@ Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll ) return vNodes; } +/**Function************************************************************* + + Synopsis [Returns the DFS ordered array of logic nodes.] + + Description [Collects only the internal nodes, leaving CIs and CO. + However it marks with the current TravId both CIs and COs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkDfsIterNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots ) +{ + Vec_Ptr_t * vNodes, * vStack; + Abc_Obj_t * pObj; + int i; + Abc_NtkIncrementTravId( pNtk ); + vNodes = Vec_PtrAlloc( 1000 ); + vStack = Vec_PtrAlloc( 1000 ); + Vec_PtrForEachEntry( vRoots, pObj, i ) + if ( !Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pObj)) ) + Abc_NtkDfs_iter( vStack, Abc_ObjRegular(pObj), vNodes ); + Vec_PtrFree( vStack ); + return vNodes; +} + /**Function************************************************************* diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ae1c110f..2c34ed67 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -105,6 +105,7 @@ static int Abc_CommandReach ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTopAnd ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTrim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -361,6 +362,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 ); Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 ); Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 ); + Cmd_CommandAdd( pAbc, "Various", "topand", Abc_CommandTopAnd, 1 ); Cmd_CommandAdd( pAbc, "Various", "trim", Abc_CommandTrim, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 ); @@ -6270,6 +6272,91 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTopAnd( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + extern Abc_Ntk_t * Abc_NtkTopAnd( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + + if ( Abc_NtkLatchNum(pNtk) > 0 ) + { + fprintf( stdout, "Currently can only works for combinational circuits.\n" ); + return 0; + } + if ( Abc_NtkPoNum(pNtk) != 1 ) + { + fprintf( stdout, "Currently expects a single-output miter.\n" ); + return 0; + } + if ( Abc_ObjFaninC0(Abc_NtkPo(pNtk, 0)) ) + { + fprintf( stdout, "The PO driver is complemented. AND-decomposition is impossible.\n" ); + return 0; + } + if ( !Abc_ObjIsNode(Abc_ObjChild0(Abc_NtkPo(pNtk, 0))) ) + { + fprintf( stdout, "The PO driver is not a node. AND-decomposition is impossible.\n" ); + return 0; + } + pNtkRes = Abc_NtkTopAnd( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "The command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: topand [-h]\n" ); + fprintf( pErr, "\t AND-decomposition of single-output combinational miter\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tname : the node name\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -13997,7 +14084,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv ) int fPartition; int fMiter; - extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ); + extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); @@ -14097,7 +14184,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv ) // perform equivalence checking if ( fSat && fMiter ) - Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, fVerbose ); + Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, fVerbose ); else Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose ); @@ -14651,12 +14738,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; int RetValue; + int fFlipBits; + int fAndOuts; int fVerbose; int nConfLimit; int nInsLimit; int clk; - extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ); + extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); @@ -14664,11 +14753,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults + fFlipBits = 0; + fAndOuts = 0; fVerbose = 0; nConfLimit = 100000; nInsLimit = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CIfavh" ) ) != EOF ) { switch ( c ) { @@ -14694,6 +14785,12 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nInsLimit < 0 ) goto usage; break; + case 'f': + fFlipBits ^= 1; + break; + case 'a': + fAndOuts ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -14714,12 +14811,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); return 0; } +/* if ( Abc_NtkPoNum(pNtk) != 1 ) { fprintf( stdout, "Currently expects a single-output miter.\n" ); return 0; } - +*/ if ( !Abc_NtkIsStrash(pNtk) ) { fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); @@ -14727,7 +14825,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) } clk = clock(); - RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose ); + RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fFlipBits, fAndOuts, fVerbose ); // verify that the pattern is correct if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 ) { @@ -14760,11 +14858,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dsat [-C num] [-I num] [-vh]\n" ); + fprintf( pErr, "usage: dsat [-C num] [-I num] [-favh]\n" ); fprintf( pErr, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" ); fprintf( pErr, "\t derives CNF from the current network and leave it unchanged\n" ); fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit ); + fprintf( pErr, "\t-f : flip polarity of SAT variables [default = %s]\n", fFlipBits? "yes": "no" ); + fprintf( pErr, "\t-a : constrain each output of multi-output miter [default = %s]\n", fAndOuts? "yes": "no" ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index d89ee618..2a234b68 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -932,9 +932,9 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t ***********************************************************************/ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) { - Vec_Ptr_t * vMapped; + Vec_Ptr_t * vMapped = NULL; Aig_Man_t * pMan; - Cnf_Man_t * pManCnf; + Cnf_Man_t * pManCnf = NULL; Cnf_Dat_t * pCnf; Abc_Ntk_t * pNtkNew = NULL; assert( Abc_NtkIsStrash(pNtk) ); @@ -954,13 +954,14 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) // derive CNF pCnf = Cnf_Derive( pMan, 0 ); - pManCnf = Cnf_ManRead(); - + Cnf_DataTranformPolarity( pCnf ); +/* // write the network for verification + pManCnf = Cnf_ManRead(); vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 ); pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped ); Vec_PtrFree( vMapped ); - +*/ // write CNF into a file Cnf_DataWriteIntoFile( pCnf, pFileName, 0 ); Cnf_DataFree( pCnf ); @@ -982,7 +983,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) SeeAlso [] ***********************************************************************/ -int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ) +int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ) { Aig_Man_t * pMan; int RetValue;//, clk = clock(); @@ -990,7 +991,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer assert( Abc_NtkLatchNum(pNtk) == 0 ); assert( Abc_NtkPoNum(pNtk) == 1 ); pMan = Abc_NtkToDar( pNtk, 0, 0 ); - RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fVerbose ); + RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fFlipBits, fAndOuts, fVerbose ); pNtk->pModel = pMan->pData, pMan->pData = NULL; Aig_ManStop( pMan ); return RetValue; diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 084f6a6c..ad09f084 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -443,7 +443,7 @@ Abc_Obj_t * Abc_NtkTopmost_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int Leve Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ) { Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObjNew, * pPoNew; + Abc_Obj_t * pObjNew, * pObjPo; int LevelCut; assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkCoNum(pNtk) == 1 ); @@ -458,10 +458,10 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ) pObjNew = Abc_NtkTopmost_rec( pNtkNew, Abc_ObjFanin0(Abc_NtkPo(pNtk, 0)), LevelCut ); pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(Abc_NtkPo(pNtk, 0)) ); // add the PO node and name - pPoNew = Abc_NtkCreatePo(pNtkNew); - Abc_ObjAddFanin( pPoNew, pObjNew ); + pObjPo = Abc_NtkCreatePo(pNtkNew); + Abc_ObjAddFanin( pObjPo, pObjNew ); Abc_NtkAddDummyPiNames( pNtkNew ); - Abc_ObjAssignName( pPoNew, Abc_ObjName(Abc_NtkPo(pNtk, 0)), NULL ); + Abc_ObjAssignName( pObjPo, Abc_ObjName(Abc_NtkPo(pNtk, 0)), NULL ); // make sure everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) { @@ -473,6 +473,131 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ) } + +/**Function************************************************************* + + Synopsis [Comparison procedure for two integers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Vec_CompareNodeIds( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ) +{ + if ( Abc_ObjRegular(*pp1)->Id < Abc_ObjRegular(*pp2)->Id ) + return -1; + if ( Abc_ObjRegular(*pp1)->Id > Abc_ObjRegular(*pp2)->Id ) // + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Collects the large supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NodeGetSuper( Abc_Obj_t * pNode ) +{ + Vec_Ptr_t * vSuper, * vFront; + Abc_Obj_t * pAnd, * pFanin; + int i; + assert( Abc_ObjIsNode(pNode) && !Abc_ObjIsComplement(pNode) ); + vSuper = Vec_PtrAlloc( 100 ); + // explore the frontier + vFront = Vec_PtrAlloc( 100 ); + Vec_PtrPush( vFront, pNode ); + Vec_PtrForEachEntry( vFront, pAnd, i ) + { + pFanin = Abc_ObjChild0(pAnd); + if ( Abc_ObjIsNode(pFanin) && !Abc_ObjIsComplement(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + Vec_PtrPush( vFront, pFanin ); + else + Vec_PtrPush( vSuper, pFanin ); + + pFanin = Abc_ObjChild1(pAnd); + if ( Abc_ObjIsNode(pFanin) && !Abc_ObjIsComplement(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + Vec_PtrPush( vFront, pFanin ); + else + Vec_PtrPush( vSuper, pFanin ); + } + Vec_PtrFree( vFront ); + // reverse the array of pointers to start with lower IDs + vFront = Vec_PtrAlloc( Vec_PtrSize(vSuper) ); + Vec_PtrForEachEntryReverse( vSuper, pNode, i ) + Vec_PtrPush( vFront, pNode ); + Vec_PtrFree( vSuper ); + vSuper = vFront; + // uniquify and return the frontier + Vec_PtrUniqify( vSuper, Vec_CompareNodeIds ); + return vSuper; +} + +/**Function************************************************************* + + Synopsis [Copies the topmost levels of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkTopAnd( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes, * vOrder; + Abc_Ntk_t * pNtkAig; + Abc_Obj_t * pObj, * pDriver, * pObjPo; + int i, nNodes; + assert( Abc_NtkIsStrash(pNtk) ); + // get the first PO + pObjPo = Abc_NtkPo(pNtk, 0); + vNodes = Abc_NodeGetSuper( Abc_ObjChild0(pObjPo) ); + assert( Vec_PtrSize(vNodes) >= 2 ); + // start the new network (constants and CIs of the old network will point to the their counterparts in the new network) + Abc_NtkCleanCopy( pNtk ); + pNtkAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); + pNtkAig->pName = Extra_UtilStrsav(pNtk->pName); + pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkAig); + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkDupObj( pNtkAig, pObj, 1 ); + // restrash the nodes reachable from the roots + vOrder = Abc_NtkDfsIterNodes( pNtk, vNodes ); + Vec_PtrForEachEntry( vOrder, pObj, i ) + pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + Vec_PtrFree( vOrder ); + // finalize the network + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + pObjPo = Abc_NtkCreatePo(pNtkAig); + pDriver = Abc_ObjNotCond(Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj)); + Abc_ObjAddFanin( pObjPo, pDriver ); + Abc_ObjAssignName( pObjPo, Abc_ObjName(pObjPo), NULL ); + } + Vec_PtrFree( vNodes ); + // perform cleanup if requested + if ( (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) + printf( "Abc_NtkTopAnd(): AIG cleanup removed %d nodes (this is a bug).\n", nNodes ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkStrash: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/cmd/cmdApi.c b/src/base/cmd/cmdApi.c index 7167e22b..71db1846 100644 --- a/src/base/cmd/cmdApi.c +++ b/src/base/cmd/cmdApi.c @@ -90,7 +90,7 @@ int Cmd_CommandExecute( Abc_Frame_t * pAbc, char * sCommand ) loop = 0; fStatus = CmdApplyAlias( pAbc, &argc, &argv, &loop ); if ( fStatus == 0 ) - fStatus = CmdCommandDispatch( pAbc, argc, argv ); + fStatus = CmdCommandDispatch( pAbc, &argc, &argv ); CmdFreeArgv( argc, argv ); } while ( fStatus == 0 && *sCommandNext != '\0' ); diff --git a/src/base/cmd/cmdInt.h b/src/base/cmd/cmdInt.h index c082bd94..3a6a2803 100644 --- a/src/base/cmd/cmdInt.h +++ b/src/base/cmd/cmdInt.h @@ -65,12 +65,13 @@ extern void CmdCommandAliasPrint( Abc_Frame_t * pAbc, Abc_Alias * pAlias ) extern char * CmdCommandAliasLookup( Abc_Frame_t * pAbc, char * sCommand ); extern void CmdCommandAliasFree( Abc_Alias * p ); /*=== cmdUtils.c =======================================================*/ -extern int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char ** argv ); +extern int CmdCommandDispatch( Abc_Frame_t * pAbc, int * argc, char *** argv ); extern char * CmdSplitLine( Abc_Frame_t * pAbc, char * sCommand, int * argc, char *** argv ); extern int CmdApplyAlias( Abc_Frame_t * pAbc, int * argc, char *** argv, int * loop ); extern char * CmdHistorySubstitution( Abc_Frame_t * pAbc, char * line, int * changed ); extern FILE * CmdFileOpen( Abc_Frame_t * pAbc, char * sFileName, char * sMode, char ** pFileNameReal, int silent ); extern void CmdFreeArgv( int argc, char ** argv ); +extern char ** CmdAddToArgv( int argc, char ** argv ); extern void CmdCommandFree( Abc_Command * pCommand ); extern void CmdCommandPrint( Abc_Frame_t * pAbc, bool fPrintAll ); extern void CmdPrintTable( st_table * tTable, int fAliases ); diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c index 6b4bdcbe..8c3fd38c 100644 --- a/src/base/cmd/cmdUtils.c +++ b/src/base/cmd/cmdUtils.c @@ -85,8 +85,12 @@ int cmdCheckShellEscape( Abc_Frame_t * pAbc, int argc, char ** argv) SeeAlso [] ***********************************************************************/ -int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv ) +int CmdCommandDispatch( Abc_Frame_t * pAbc, int * pargc, char *** pargv ) { + int argc = *pargc; + char ** argv = *pargv; + char ** argv2; + Abc_Ntk_t * pNetCopy; int (*pFunc) ( Abc_Frame_t *, int, char ** ); Abc_Command * pCommand; @@ -103,8 +107,17 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv ) // get the command if ( !st_lookup( pAbc->tCommands, argv[0], (char **)&pCommand ) ) { // the command is not in the table - fprintf( pAbc->Err, "** cmd error: unknown command '%s'\n", argv[0] ); - return 1; +// fprintf( pAbc->Err, "** cmd error: unknown command '%s'\n", argv[0] ); +// return 1; + // add command 'read' assuming that this is the file name + argv2 = CmdAddToArgv( argc, argv ); + CmdFreeArgv( argc, argv ); + argc = argc+1; + argv = argv2; + *pargc = argc; + *pargv = argv; + if ( !st_lookup( pAbc->tCommands, argv[0], (char **)&pCommand ) ) + assert( 0 ); } // get the backup network if the command is going to change the network @@ -303,7 +316,7 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop ) fError = CmdApplyAlias( pAbc, &newc, &newv, loop ); if ( fError == 0 ) { - fError = CmdCommandDispatch( pAbc, newc, newv ); + fError = CmdCommandDispatch( pAbc, &newc, &newv ); } CmdFreeArgv( newc, newv ); } @@ -453,6 +466,28 @@ void CmdFreeArgv( int argc, char **argv ) FREE( argv ); } +/**Function************************************************************* + + Synopsis [Frees the previously allocated argv array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char ** CmdAddToArgv( int argc, char ** argv ) +{ + char ** argv2; + int i; + argv2 = ALLOC( char *, argc + 1 ); + argv2[0] = Extra_UtilStrsav( "read" ); + for ( i = 0; i < argc; i++ ) + argv2[i+1] = Extra_UtilStrsav( argv[i] ); + return argv2; +} + /**Function************************************************************* Synopsis [Frees the previously allocated command.] diff --git a/src/base/io/io.c b/src/base/io/io.c index 1695942e..371adfc9 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -144,7 +144,7 @@ void Io_End() int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk; - char * pFileName; + char * pFileName, * pTemp; int fCheck; int c; @@ -171,6 +171,10 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; // get the input file name pFileName = argv[globalUtilOptind]; + // fix the wrong symbol + for ( pTemp = pFileName; *pTemp; pTemp++ ) + if ( *pTemp == '>' ) + *pTemp = '\\'; // read the file using the corresponding file reader pNtk = Io_Read( pFileName, Io_ReadFileType(pFileName), fCheck ); if ( pNtk == NULL ) diff --git a/src/base/main/main.c b/src/base/main/main.c index 7ecbe48e..1f1f19ba 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -221,8 +221,8 @@ int main( int argc, char * argv[] ) // if the memory should be freed, quit packages if ( fStatus < 0 ) { - Abc_Stop(); - } + Abc_Stop(); + } return 0; usage: -- cgit v1.2.3