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
|
/**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 "sat/bsat/satSolver.h"
#include "pdr.h"
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
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
// 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
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
// 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
Vec_Int_t * vSuppLits; // support literals
Pdr_Set_t * pCubeJust; // justification
abctime * pTime4Outs;// timeout per output
// 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;
// runtime
abctime timeToStop;
abctime timeToStopOne;
// time stats
abctime tSat;
abctime tSatSat;
abctime tSatUnsat;
abctime tGeneral;
abctime tPush;
abctime tTsim;
abctime tContain;
abctime tCnf;
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 ///
////////////////////////////////////////////////////////////////////////
/*=== pdrCex.c ==========================================================*/
extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
/*=== 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 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 void Pdr_ManReportInvariant( Pdr_Man_t * p );
extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p );
/*=== 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 );
/*=== 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 );
/*=== pdrTsim.c ==========================================================*/
extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_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 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 void Pdr_SetPrint( FILE * pFile, 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 );
extern int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
