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
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
|
/**CFile****************************************************************
FileName [pdrInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Property driven reachability.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - November 20, 2010.]
Revision [$Id: pdrInt.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__sat__pdr__pdrInt_h
#define ABC__sat__pdr__pdrInt_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "aig/saig/saig.h"
#include "misc/vec/vecWec.h"
#include "sat/cnf/cnf.h"
#include "pdr.h"
#include "misc/hash/hashInt.h"
#include "aig/gia/giaAig.h"
#define PDR_USE_SATOKO 1
#ifndef PDR_USE_SATOKO
#include "sat/bsat/satSolver.h"
#else
#include "sat/satoko/satoko.h"
#define l_Undef 0
#define l_True 1
#define l_False -1
#define sat_solver satoko_t
#define sat_solver_new satoko_create
#define sat_solver_delete satoko_destroy
#define zsat_solver_new_seed(s) satoko_create()
#define zsat_solver_restart_seed(s,a) satoko_reset(s)
#define sat_solver_nvars satoko_varnum
#define sat_solver_setnvars satoko_setnvars
#define sat_solver_addclause(s,b,e) satoko_add_clause(s,b,e-b)
#define sat_solver_final satoko_final_conflict
#define sat_solver_solve(s,b,e,c,x,y,z) satoko_solve_assumptions_limit(s,b,e-b,(int)c)
#define sat_solver_var_value satoko_read_cex_varvalue
#define sat_solver_set_runtime_limit satoko_set_runtime_limit
#define sat_solver_set_runid satoko_set_runid
#define sat_solver_set_stop_func satoko_set_stop_func
#define sat_solver_compress(s)
#endif
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Txs_Man_t_ Txs_Man_t;
typedef struct Txs3_Man_t_ Txs3_Man_t;
typedef struct Pdr_Set_t_ Pdr_Set_t;
struct Pdr_Set_t_
{
word Sign; // signature
int nRefs; // ref counter
int nTotal; // total literals
int nLits; // num flop literals
int Lits[0];
};
typedef struct Pdr_Obl_t_ Pdr_Obl_t;
struct Pdr_Obl_t_
{
int iFrame; // time frame
int prio; // priority
int nRefs; // reference counter
Pdr_Set_t * pState; // state cube
Pdr_Obl_t * pNext; // next one
Pdr_Obl_t * pLink; // queue link
};
typedef struct Pdr_Man_t_ Pdr_Man_t;
struct Pdr_Man_t_
{
// input problem
Pdr_Par_t * pPars; // parameters
Aig_Man_t * pAig; // user's AIG
Gia_Man_t * pGia; // user's AIG
// static CNF representation
Cnf_Man_t * pCnfMan; // CNF manager
Cnf_Dat_t * pCnf1; // CNF for this AIG
Vec_Int_t * vVar2Reg; // mapping of SAT var into registers
// dynamic CNF representation
Cnf_Dat_t * pCnf2; // CNF for this AIG
Vec_Int_t * pvId2Vars; // for each used ObjId, maps frame into SAT var
Vec_Ptr_t vVar2Ids; // for each used frame, maps SAT var into ObjId
Vec_Wec_t * vVLits; // CNF literals
// data representation
int iOutCur; // current output
int nPrioShift;// priority shift
Vec_Ptr_t * vCexes; // counter-examples for each output
Vec_Ptr_t * vSolvers; // SAT solvers
Vec_Vec_t * vClauses; // clauses by timeframe
Pdr_Obl_t * pQueue; // proof obligations
int * pOrder; // ordering of the lits
Vec_Int_t * vActVars; // the counter of activation variables
int iUseFrame; // the first used frame
int nAbsFlops; // the number of flops used
Vec_Int_t * vAbsFlops; // flops currently used
Vec_Int_t * vMapFf2Ppi;
Vec_Int_t * vMapPpi2Ff;
int nCexes;
int nCexesTotal;
// terminary simulation
Txs3_Man_t * pTxs3;
// internal use
Vec_Int_t * vPrio; // priority flops
Vec_Int_t * vLits; // array of literals
Vec_Int_t * vCiObjs; // cone leaves
Vec_Int_t * vCoObjs; // cone roots
Vec_Int_t * vCiVals; // cone leaf values
Vec_Int_t * vCoVals; // cone root values
Vec_Int_t * vNodes; // cone nodes
Vec_Int_t * vUndo; // cone undos
Vec_Int_t * vVisits; // intermediate
Vec_Int_t * vCi2Rem; // CIs to be removed
Vec_Int_t * vRes; // final result
abctime * pTime4Outs;// timeout per output
Vec_Ptr_t * vInfCubes; // infinity clauses/cubes
// statistics
int nBlocks; // the number of times blockState was called
int nObligs; // the number of proof obligations derived
int nCubes; // the number of cubes derived
int nCalls; // the number of SAT calls
int nCallsS; // the number of SAT calls (sat)
int nCallsU; // the number of SAT calls (unsat)
int nStarts; // the number of SAT solver restarts
int nFrames; // frames explored
int nCasesSS;
int nCasesSU;
int nCasesUS;
int nCasesUU;
int nQueCur;
int nQueMax;
int nQueLim;
int nXsimRuns;
int nXsimLits;
// runtime
abctime timeToStop;
abctime timeToStopOne;
// time stats
abctime tSat;
abctime tSatSat;
abctime tSatUnsat;
abctime tGeneral;
abctime tPush;
abctime tTsim;
abctime tContain;
abctime tCnf;
abctime tAbs;
abctime tTotal;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); }
static inline abctime Pdr_ManTimeLimit( Pdr_Man_t * p )
{
if ( p->timeToStop == 0 )
return p->timeToStopOne;
if ( p->timeToStopOne == 0 )
return p->timeToStop;
if ( p->timeToStop < p->timeToStopOne )
return p->timeToStop;
return p->timeToStopOne;
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== pdrCnf.c ==========================================================*/
extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj );
extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
extern int Pdr_ManFreeVar( Pdr_Man_t * p, int k );
extern sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit );
/*=== pdrCore.c ==========================================================*/
extern int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet );
/*=== pdrInv.c ==========================================================*/
extern Vec_Int_t * Pdr_ManCountFlopsInv( Pdr_Man_t * p );
extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time );
extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved );
extern Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p );
extern void Pdr_ManReportInvariant( Pdr_Man_t * p );
extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p );
extern Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce );
/*=== pdrMan.c ==========================================================*/
extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
extern void Pdr_ManStop( Pdr_Man_t * p );
extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
extern Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p );
/*=== pdrSat.c ==========================================================*/
extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k );
extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k );
extern void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k );
extern Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext );
extern Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray );
extern void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
extern void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues );
extern int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit );
/*=== pdrTsim.c ==========================================================*/
extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
/*=== pdrTsim2.c ==========================================================*/
extern Txs_Man_t * Txs_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio );
extern void Txs_ManStop( Txs_Man_t * );
extern Pdr_Set_t * Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube );
/*=== pdrTsim3.c ==========================================================*/
extern Txs3_Man_t * Txs3_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio );
extern void Txs3_ManStop( Txs3_Man_t * );
extern Pdr_Set_t * Txs3_ManTernarySim( Txs3_Man_t * p, int k, Pdr_Set_t * pCube );
/*=== pdrUtil.c ==========================================================*/
extern Pdr_Set_t * Pdr_SetAlloc( int nSize );
extern Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits );
extern Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove );
extern Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits );
extern Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet );
extern Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p );
extern void Pdr_SetDeref( Pdr_Set_t * p );
extern Pdr_Set_t * ZPdr_SetIntersection( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep );
extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
extern int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
extern int ZPdr_SetIsInit( Pdr_Set_t * p );
extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
extern void ZPdr_SetPrint( Pdr_Set_t * p );
extern void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p );
extern void Pdr_OblDeref( Pdr_Obl_t * p );
extern int Pdr_QueueIsEmpty( Pdr_Man_t * p );
extern Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p );
extern Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p );
extern void Pdr_QueueClean( Pdr_Man_t * p );
extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
extern void Pdr_QueuePrint( Pdr_Man_t * p );
extern void Pdr_QueueStop( Pdr_Man_t * p );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
