summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmc.h
blob: 71a33595712efe20c2feb712948bc3aeed3b8b0d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
/**CFile****************************************************************

  FileName    [bmc.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [SAT-based bounded model checking.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: bmc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/
 
#ifndef ABC___sat_bmc_BMC_h
#define ABC___sat_bmc_BMC_h


////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include "aig/saig/saig.h"
#include "aig/gia/gia.h"

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////

ABC_NAMESPACE_HEADER_START

//#define USE_NODE_ORDER 1

////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////


// exact synthesis parameters

typedef struct Bmc_EsPar_t_ Bmc_EsPar_t;
struct Bmc_EsPar_t_
{
    int        nVars; 
    int        nNodes;
    int        nLutSize;
    int        nMajSupp;
    int        fMajority;
    int        fUseIncr;
    int        fOnlyAnd;
    int        fGlucose;
    int        fOrderNodes;
    int        fEnumSols;
    int        fFewerVars;
    int        fVerbose; 
    char *     pTtStr;
};

static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
{
    memset( pPars, 0, sizeof(Bmc_EsPar_t) );
    pPars->nVars       = 0; 
    pPars->nNodes      = 0; 
    pPars->nLutSize    = 2; 
    pPars->nMajSupp    = 0;
    pPars->fMajority   = 0; 
    pPars->fUseIncr    = 0;
    pPars->fOnlyAnd    = 0; 
    pPars->fGlucose    = 0; 
    pPars->fOrderNodes = 0; 
    pPars->fEnumSols   = 0; 
    pPars->fFewerVars  = 0; 
    pPars->fVerbose    = 1; 
}


// unrolling manager 
typedef struct Unr_Man_t_ Unr_Man_t;

typedef struct Saig_ParBmc_t_ Saig_ParBmc_t;
struct Saig_ParBmc_t_
{
    int         nStart;         // starting timeframe
    int         nFramesMax;     // maximum number of timeframes 
    int         nConfLimit;     // maximum number of conflicts at a node
    int         nConfLimitJump; // maximum number of conflicts after jumping
    int         nFramesJump;    // the number of tiemframes to jump
    int         nTimeOut;       // approximate timeout in seconds
    int         nTimeOutGap;    // approximate timeout in seconds since the last change
    int         nTimeOutOne;    // timeout per output in multi-output solving
    int         nPisAbstract;   // the number of PIs to abstract
    int         fSolveAll;      // does not stop at the first SAT output
    int         fStoreCex;      // enable storing CEXes in the MO mode
    int         fUseBridge;     // use bridge interface
    int         fDropSatOuts;   // replace sat outputs by constant 0
    int         nFfToAddMax;    // max number of flops to add during CBA
    int         fSkipRand;      // skip random decisions
    int         fNoRestarts;    // disables periodic restarts
    int         fUseSatoko;     // enables using Satoko
    int         fUseGlucose;    // enables using Glucose 3.0
    int         nLearnedStart;  // starting learned clause limit
    int         nLearnedDelta;  // delta of learned clause limit
    int         nLearnedPerce;  // ratio of learned clause limit
    int         fVerbose;       // verbose 
    int         fNotVerbose;    // skip line-by-line print-out 
    char *      pLogFileName;   // log file name
    int         fSilent;        // completely silent
    int         iFrame;         // explored up to this frame
    int         nFailOuts;      // the number of failed outputs
    int         nDropOuts;      // the number of dropped outputs
    abctime     timeLastSolved; // the time when the last output was solved
    int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
    int         RunId;          // BMC id in this run 
    int(*pFuncStop)(int);       // callback to terminate
};

 
typedef struct Bmc_AndPar_t_ Bmc_AndPar_t;
struct Bmc_AndPar_t_
{
    int         nStart;         // starting timeframe
    int         nFramesMax;     // maximum number of timeframes 
    int         nFramesAdd;     // the number of additional frames
    int         nConfLimit;     // maximum number of conflicts at a node
    int         nTimeOut;       // timeout in seconds
    int         nLutSize;       // LUT size for cut computation
    int         nProcs;         // the number of parallel solvers
    int         fLoadCnf;       // dynamic CNF loading
    int         fDumpFrames;    // dump unrolled timeframes
    int         fUseSynth;      // use synthesis
    int         fUseOldCnf;     // use old CNF construction
    int         fUseGlucose;    // use Glucose 3.0 as the default solver
    int         fUseEliminate;  // use variable elimination
    int         fVerbose;       // verbose 
    int         fVeryVerbose;   // very verbose 
    int         fNotVerbose;    // skip line-by-line print-out 
    int         iFrame;         // explored up to this frame
    int         nFailOuts;      // the number of failed outputs
    int         nDropOuts;      // the number of dropped outputs
    
    void (*pFuncOnFrameDone)(int, int, int); // callback on each frame status (frame, po, statuss)
};
  
typedef struct Bmc_BCorePar_t_ Bmc_BCorePar_t;
struct Bmc_BCorePar_t_
{
    int         iFrame;         // timeframe
    int         iOutput;        // property output
    int         nTimeOut;       // timeout in seconds
    char *      pFilePivots;    // file name with AIG IDs of pivot objects
    char *      pFileProof;     // file name to write the resulting proof
    int         fVerbose;       // verbose output
};

typedef struct Bmc_MulPar_t_ Bmc_MulPar_t;
struct Bmc_MulPar_t_
{
    int         TimeOutGlo;
    int         TimeOutLoc;
    int         TimeOutInc;
    int         TimeOutGap;
    int         TimePerOut;
    int         fUseSyn;
    int         fDumpFinal;
    int         fVerbose;
    int         fVeryVerbose;
};

typedef struct Bmc_ParFf_t_ Bmc_ParFf_t;
struct Bmc_ParFf_t_
{
    char *     pFileName;
    char *     pFormStr;
    int        Algo;
    int        fComplVars;
    int        fStartPats;
    int        nTimeOut;
    int        nIterCheck;
    int        nCardConstr;
    int        fNonStrict;
    int        fBasic;
    int        fFfOnly;
    int        fDump;
    int        fDumpDelay;
    int        fDumpUntest;
    int        fDumpNewFaults;
    int        fVerbose;
};

////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== bmcBCore.c ==========================================================*/
extern void              Bmc_ManBCorePerform( Gia_Man_t * pGia, Bmc_BCorePar_t * pPars );
/*=== bmcBmc.c ==========================================================*/
extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit, int fUseSatoko );
/*=== bmcBmc2.c ==========================================================*/
extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent, int fUseSatoko );
/*=== bmcBmc3.c ==========================================================*/
extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
/*=== bmcBmcAnd.c ==========================================================*/
extern int               Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars );
/*=== bmcCexCare.c ==========================================================*/
extern Abc_Cex_t *       Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
extern Abc_Cex_t *       Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
extern Abc_Cex_t *       Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
extern void              Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
extern Abc_Cex_t *       Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose );
extern Abc_Cex_t *       Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose );
/*=== bmcCexCut.c ==========================================================*/
extern Gia_Man_t *       Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
/*=== bmcCexMin.c ==========================================================*/
extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
/*=== bmcCexTool.c ==========================================================*/
extern void              Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose );
extern int               Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
/*=== bmcICheck.c ==========================================================*/
extern void              Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
extern Vec_Int_t *       Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose );
/*=== bmcUnroll.c ==========================================================*/
extern Unr_Man_t *       Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose );
extern Gia_Man_t *       Unr_ManUnrollFrame( Unr_Man_t * p, int f );
extern void              Unr_ManFree( Unr_Man_t * p );


ABC_NAMESPACE_HEADER_END



#endif

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////