abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ssc.h
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [ssc.h]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT sweeping under constraints.]
8 
9  Synopsis [External declarations.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 29, 2008.]
16 
17  Revision [$Id: ssc.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__aig__ssc__ssc_h
22 #define ABC__aig__ssc__ssc_h
23 
24 
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// PARAMETERS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 
34 
35 ABC_NAMESPACE_HEADER_START
36 
37 
38 ////////////////////////////////////////////////////////////////////////
39 /// BASIC TYPES ///
40 ////////////////////////////////////////////////////////////////////////
41 
42 // choicing parameters
43 typedef struct Ssc_Pars_t_ Ssc_Pars_t;
44 struct Ssc_Pars_t_
45 {
46  int nWords; // the number of simulation words
47  int nBTLimit; // conflict limit at a node
48  int nSatVarMax; // the max number of SAT variables
49  int nCallsRecycle; // calls to perform before recycling SAT solver
50  int fAppend; // append constraints to the resulting AIG
51  int fVerbose; // verbose stats
52  int fVerify; // enable internal verification
53 };
54 
55 ////////////////////////////////////////////////////////////////////////
56 /// MACRO DEFINITIONS ///
57 ////////////////////////////////////////////////////////////////////////
58 
59 ////////////////////////////////////////////////////////////////////////
60 /// FUNCTION DECLARATIONS ///
61 ////////////////////////////////////////////////////////////////////////
62 
63 /*=== sscCore.c ==========================================================*/
64 extern void Ssc_ManSetDefaultParams( Ssc_Pars_t * p );
65 extern Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars );
66 extern Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars );
67 
68 
69 ABC_NAMESPACE_HEADER_END
70 
71 
72 
73 #endif
74 
75 ////////////////////////////////////////////////////////////////////////
76 /// END OF FILE ///
77 ////////////////////////////////////////////////////////////////////////
78 
Ssc_Pars_t_::nSatVarMax
int nSatVarMax
Definition: ssc.h:48
Ssc_ManSetDefaultParams
void Ssc_ManSetDefaultParams(Ssc_Pars_t *p)
MACRO DEFINITIONS ///.
Definition: sscCore.c:46
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ssc_Pars_t
typedefABC_NAMESPACE_HEADER_START struct Ssc_Pars_t_ Ssc_Pars_t
INCLUDES ///.
Definition: ssc.h:43
Ssc_Pars_t_::nBTLimit
int nBTLimit
Definition: ssc.h:47
Ssc_PerformSweepingConstr
Gia_Man_t * Ssc_PerformSweepingConstr(Gia_Man_t *p, Ssc_Pars_t *pPars)
Definition: sscCore.c:420
Ssc_Pars_t_::nWords
int nWords
Definition: ssc.h:46
Ssc_Pars_t_::nCallsRecycle
int nCallsRecycle
Definition: ssc.h:49
Ssc_PerformSweeping
Gia_Man_t * Ssc_PerformSweeping(Gia_Man_t *pAig, Gia_Man_t *pCare, Ssc_Pars_t *pPars)
Definition: sscCore.c:413
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition: abc_global.h:105
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition: abc_global.h:106
Ssc_Pars_t_::fAppend
int fAppend
Definition: ssc.h:50
Gia_Man_t_
Definition: gia.h:95
Ssc_Pars_t_
Definition: ssc.h:44
Ssc_Pars_t_::fVerify
int fVerify
Definition: ssc.h:52
Ssc_Pars_t_::fVerbose
int fVerbose
Definition: ssc.h:51