diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-05-11 20:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-05-11 20:01:00 -0700 |
| commit | 47036e1e44fb5f4e1948cdc26ab10254ccaa161d (patch) | |
| tree | 93ad0800fd9f38ea6a2732e0cf3a68412734efc5 /src/aig/fra/fra.h | |
| parent | 582cf0b923e0a461c2efdb4ecde9bfdb0716a328 (diff) | |
| download | abc-47036e1e44fb5f4e1948cdc26ab10254ccaa161d.tar.gz abc-47036e1e44fb5f4e1948cdc26ab10254ccaa161d.tar.bz2 abc-47036e1e44fb5f4e1948cdc26ab10254ccaa161d.zip | |
Version abc80511_2
Diffstat (limited to 'src/aig/fra/fra.h')
| -rw-r--r-- | src/aig/fra/fra.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 7311d414..f7ad40dd 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -104,6 +104,7 @@ struct Fra_Ssw_t_ int fUse1Hot; // use one-hotness constraints int fVerbose; // enable verbose output int nIters; // the number of iterations performed + float TimeLimit; // the runtime budget for this call }; // FRAIG equivalence classes @@ -312,7 +313,7 @@ extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars /*=== fraIndVer.c =====================================================*/ extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits ); /*=== fraLcr.c ========================================================*/ -extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter ); +extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); @@ -328,7 +329,7 @@ extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ); extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSec.c ========================================================*/ -extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ); +extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit ); /*=== fraSim.c ========================================================*/ extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); |