ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
llb.h
Go to the documentation of this file.
1
20
21#ifndef ABC__aig__llb__llb_h
22#define ABC__aig__llb__llb_h
23
24
28
32
33
35
36
40
43{
44 int nBddMax; // maximum BDD size
45 int nIterMax; // maximum iteration count
46 int nClusterMax; // maximum cluster size
47 int nHintDepth; // the number of times to cofactor
48 int HintFirst; // the number of first hint to use
49 int fUseFlow; // use flow computation
50 int nVolumeMax; // the largest volume
51 int nVolumeMin; // the smallest volume
52 int nPartValue; // partitioning value
53 int fBackward; // enable backward reachability
54 int fReorder; // enable dynamic variable reordering
55 int fIndConstr; // extract inductive constraints
56 int fUsePivots; // use internal pivot variables
57 int fCluster; // use partition clustering
58 int fSchedule; // use cluster scheduling
59 int fDumpReached; // dump reached states into a file
60 int fVerbose; // print verbose information
61 int fVeryVerbose; // print dependency matrices
62 int fSilent; // do not print any infomation
63 int fSkipReach; // skip reachability (preparation phase only)
64 int fSkipOutCheck; // does not check the property output
65 int TimeLimit; // time limit for one reachability run
66 int TimeLimitGlo; // time limit for all reachability runs
67 // internal parameters
68 abctime TimeTarget; // the time to stop
69 int iFrame; // explored up to this frame
70};
71
75
79
80/*=== llbCore.c ==========================================================*/
81extern void Llb_ManSetDefaultParams( Gia_ParLlb_t * pPars );
82/*=== llb4Nonlin.c ==========================================================*/
83extern int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
84
85
86
88
89
90
91#endif
92
96
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
void Llb_ManSetDefaultParams(Gia_ParLlb_t *pPars)
MACRO DEFINITIONS ///.
Definition llb1Core.c:46
int Llb_Nonlin4CoreReach(Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
typedefABC_NAMESPACE_HEADER_START struct Gia_ParLlb_t_ Gia_ParLlb_t
INCLUDES ///.
Definition llb.h:41
int fSkipOutCheck
Definition llb.h:64
int nClusterMax
Definition llb.h:46
int fVerbose
Definition llb.h:60
int fDumpReached
Definition llb.h:59
int HintFirst
Definition llb.h:48
int nIterMax
Definition llb.h:45
int nHintDepth
Definition llb.h:47
int fUsePivots
Definition llb.h:56
int fSchedule
Definition llb.h:58
abctime TimeTarget
Definition llb.h:68
int TimeLimitGlo
Definition llb.h:66
int fUseFlow
Definition llb.h:49
int fBackward
Definition llb.h:53
int fVeryVerbose
Definition llb.h:61
int TimeLimit
Definition llb.h:65
int nBddMax
Definition llb.h:44
int fSilent
Definition llb.h:62
int nPartValue
Definition llb.h:52
int fReorder
Definition llb.h:54
int nVolumeMin
Definition llb.h:51
int fIndConstr
Definition llb.h:55
int fSkipReach
Definition llb.h:63
int iFrame
Definition llb.h:69
int nVolumeMax
Definition llb.h:50
int fCluster
Definition llb.h:57