diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-05-15 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-05-15 08:01:00 -0700 |
| commit | 74ff01bfb54e9f0a68ac88b827521a422269a144 (patch) | |
| tree | 240c07b87e355dba9caa1e6187d6673b92996eac /src/aig/fra/fra.h | |
| parent | 37b6c727f1276d9d97a79a8f40271aee446a4ba4 (diff) | |
| download | abc-74ff01bfb54e9f0a68ac88b827521a422269a144.tar.gz abc-74ff01bfb54e9f0a68ac88b827521a422269a144.tar.bz2 abc-74ff01bfb54e9f0a68ac88b827521a422269a144.zip | |
Version abc80515
Diffstat (limited to 'src/aig/fra/fra.h')
| -rw-r--r-- | src/aig/fra/fra.h | 27 |
1 files changed, 25 insertions, 2 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index f7ad40dd..7cb846fa 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -51,6 +51,7 @@ extern "C" { typedef struct Fra_Par_t_ Fra_Par_t; typedef struct Fra_Ssw_t_ Fra_Ssw_t; +typedef struct Fra_Sec_t_ Fra_Sec_t; typedef struct Fra_Man_t_ Fra_Man_t; typedef struct Fra_Cla_t_ Fra_Cla_t; typedef struct Fra_Sml_t_ Fra_Sml_t; @@ -87,7 +88,7 @@ struct Fra_Par_t_ int fDontShowBar; // does not show progressbar during fraiging }; -// seq SAT sweeping parametesr +// seq SAT sweeping parameters struct Fra_Ssw_t_ { int nPartSize; // size of the partition @@ -107,6 +108,27 @@ struct Fra_Ssw_t_ float TimeLimit; // the runtime budget for this call }; +// SEC parametesr +struct Fra_Sec_t_ +{ + int fTryComb; // try CEC call as a preprocessing step + int fTryBmc; // try BMC call as a preprocessing step + int nFramesMax; // the max number of frames used for induction + int fPhaseAbstract; // enables phase abstraction + int fRetimeFirst; // enables most-forward retiming at the beginning + int fRetimeRegs; // enables min-register retiming at the beginning + int fFraiging; // enables fraiging at the beginning + int fInterpolation; // enables interpolation + int fReachability; // enables BDD based reachability + int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove + int fVerbose; // enables verbose reporting of statistics + int fVeryVerbose; // enables very verbose reporting + int TimeLimit; // enables the timeout + // internal parameters + int fRecursive; // set to 1 when SEC is called recursively + int fReportSolution; // enables report solution in a special form +}; + // FRAIG equivalence classes struct Fra_Cla_t_ { @@ -329,7 +351,8 @@ 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, int TimeLimit ); +extern void Fra_SecSetDefaultParams( Fra_Sec_t * p ); +extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec ); /*=== fraSim.c ========================================================*/ extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); |