1 /**CFile****************************************************************
2
3 FileName [pdrInt.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Property driven reachability.]
8
9 Synopsis [Internal declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - November 20, 2010.]
16
17 Revision [$Id: pdrInt.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__sat__pdr__pdrInt_h
22 #define ABC__sat__pdr__pdrInt_h
23
24 ////////////////////////////////////////////////////////////////////////
25 /// INCLUDES ///
26 ////////////////////////////////////////////////////////////////////////
27
28 #include "aig/saig/saig.h"
29 #include "misc/vec/vecWec.h"
30 #include "sat/cnf/cnf.h"
31 #include "pdr.h"
32 #include "misc/hash/hashInt.h"
33 #include "aig/gia/giaAig.h"
34
35 //#define PDR_USE_SATOKO 1
36
37 #ifndef PDR_USE_SATOKO
38 #include "sat/bsat/satSolver.h"
39 #else
40 #include "sat/satoko/satoko.h"
41 #define l_Undef 0
42 #define l_True 1
43 #define l_False -1
44 #define sat_solver satoko_t
45 #define sat_solver_new satoko_create
46 #define sat_solver_delete satoko_destroy
47 #define zsat_solver_new_seed(s) satoko_create()
48 #define zsat_solver_restart_seed(s,a) satoko_reset(s)
49 #define sat_solver_nvars satoko_varnum
50 #define sat_solver_setnvars satoko_setnvars
51 #define sat_solver_addclause(s,b,e) satoko_add_clause(s,b,e-b)
52 #define sat_solver_final satoko_final_conflict
53 #define sat_solver_solve(s,b,e,c,x,y,z) satoko_solve_assumptions_limit(s,b,e-b,(int)c)
54 #define sat_solver_var_value satoko_read_cex_varvalue
55 #define sat_solver_set_runtime_limit satoko_set_runtime_limit
56 #define sat_solver_set_runid satoko_set_runid
57 #define sat_solver_set_stop_func satoko_set_stop_func
58 #define sat_solver_compress(s)
59 #endif
60
61 ABC_NAMESPACE_HEADER_START
62
63 ////////////////////////////////////////////////////////////////////////
64 /// PARAMETERS ///
65 ////////////////////////////////////////////////////////////////////////
66
67 ////////////////////////////////////////////////////////////////////////
68 /// BASIC TYPES ///
69 ////////////////////////////////////////////////////////////////////////
70
71 typedef struct Txs_Man_t_ Txs_Man_t;
72 typedef struct Txs3_Man_t_ Txs3_Man_t;
73
74 typedef struct Pdr_Set_t_ Pdr_Set_t;
75 struct Pdr_Set_t_
76 {
77 word Sign; // signature
78 int nRefs; // ref counter
79 int nTotal; // total literals
80 int nLits; // num flop literals
81 int Lits[0];
82 };
83
84 typedef struct Pdr_Obl_t_ Pdr_Obl_t;
85 struct Pdr_Obl_t_
86 {
87 int iFrame; // time frame
88 int prio; // priority
89 int nRefs; // reference counter
90 Pdr_Set_t * pState; // state cube
91 Pdr_Obl_t * pNext; // next one
92 Pdr_Obl_t * pLink; // queue link
93 };
94
95 typedef struct Pdr_Man_t_ Pdr_Man_t;
96 struct Pdr_Man_t_
97 {
98 // input problem
99 Pdr_Par_t * pPars; // parameters
100 Aig_Man_t * pAig; // user's AIG
101 Gia_Man_t * pGia; // user's AIG
102 // static CNF representation
103 Cnf_Man_t * pCnfMan; // CNF manager
104 Cnf_Dat_t * pCnf1; // CNF for this AIG
105 Vec_Int_t * vVar2Reg; // mapping of SAT var into registers
106 // dynamic CNF representation
107 Cnf_Dat_t * pCnf2; // CNF for this AIG
108 Vec_Int_t * pvId2Vars; // for each used ObjId, maps frame into SAT var
109 Vec_Ptr_t vVar2Ids; // for each used frame, maps SAT var into ObjId
110 Vec_Wec_t * vVLits; // CNF literals
111 // data representation
112 int iOutCur; // current output
113 int nPrioShift;// priority shift
114 Vec_Ptr_t * vCexes; // counter-examples for each output
115 Vec_Ptr_t * vSolvers; // SAT solvers
116 Vec_Vec_t * vClauses; // clauses by timeframe
117 Pdr_Obl_t * pQueue; // proof obligations
118 int * pOrder; // ordering of the lits
119 Vec_Int_t * vActVars; // the counter of activation variables
120 int iUseFrame; // the first used frame
121 int nAbsFlops; // the number of flops used
122 Vec_Int_t * vAbsFlops; // flops currently used
123 Vec_Int_t * vMapFf2Ppi;
124 Vec_Int_t * vMapPpi2Ff;
125 int nCexes;
126 int nCexesTotal;
127 // terminary simulation
128 Txs3_Man_t * pTxs3;
129 // internal use
130 Vec_Int_t * vPrio; // priority flops
131 Vec_Int_t * vLits; // array of literals
132 Vec_Int_t * vCiObjs; // cone leaves
133 Vec_Int_t * vCoObjs; // cone roots
134 Vec_Int_t * vCiVals; // cone leaf values
135 Vec_Int_t * vCoVals; // cone root values
136 Vec_Int_t * vNodes; // cone nodes
137 Vec_Int_t * vUndo; // cone undos
138 Vec_Int_t * vVisits; // intermediate
139 Vec_Int_t * vCi2Rem; // CIs to be removed
140 Vec_Int_t * vRes; // final result
141 abctime * pTime4Outs;// timeout per output
142 Vec_Ptr_t * vInfCubes; // infinity clauses/cubes
143 // statistics
144 int nBlocks; // the number of times blockState was called
145 int nObligs; // the number of proof obligations derived
146 int nCubes; // the number of cubes derived
147 int nCalls; // the number of SAT calls
148 int nCallsS; // the number of SAT calls (sat)
149 int nCallsU; // the number of SAT calls (unsat)
150 int nStarts; // the number of SAT solver restarts
151 int nFrames; // frames explored
152 int nCasesSS;
153 int nCasesSU;
154 int nCasesUS;
155 int nCasesUU;
156 int nQueCur;
157 int nQueMax;
158 int nQueLim;
159 int nXsimRuns;
160 int nXsimLits;
161 // runtime
162 abctime timeToStop;
163 abctime timeToStopOne;
164 // time stats
165 abctime tSat;
166 abctime tSatSat;
167 abctime tSatUnsat;
168 abctime tGeneral;
169 abctime tPush;
170 abctime tTsim;
171 abctime tContain;
172 abctime tCnf;
173 abctime tAbs;
174 abctime tTotal;
175 };
176
177 ////////////////////////////////////////////////////////////////////////
178 /// MACRO DEFINITIONS ///
179 ////////////////////////////////////////////////////////////////////////
180
Pdr_ManSolver(Pdr_Man_t * p,int k)181 static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); }
182
Pdr_ManTimeLimit(Pdr_Man_t * p)183 static inline abctime Pdr_ManTimeLimit( Pdr_Man_t * p )
184 {
185 if ( p->timeToStop == 0 )
186 return p->timeToStopOne;
187 if ( p->timeToStopOne == 0 )
188 return p->timeToStop;
189 if ( p->timeToStop < p->timeToStopOne )
190 return p->timeToStop;
191 return p->timeToStopOne;
192 }
193
194 ////////////////////////////////////////////////////////////////////////
195 /// FUNCTION DECLARATIONS ///
196 ////////////////////////////////////////////////////////////////////////
197
198 /*=== pdrCnf.c ==========================================================*/
199 extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj );
200 extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
201 extern int Pdr_ManFreeVar( Pdr_Man_t * p, int k );
202 extern sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit );
203 /*=== pdrCore.c ==========================================================*/
204 extern int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet );
205 /*=== pdrInv.c ==========================================================*/
206 extern Vec_Int_t * Pdr_ManCountFlopsInv( Pdr_Man_t * p );
207 extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time );
208 extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
209 extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved );
210 extern Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p );
211 extern void Pdr_ManReportInvariant( Pdr_Man_t * p );
212 extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p );
213 extern Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce );
214 /*=== pdrMan.c ==========================================================*/
215 extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
216 extern void Pdr_ManStop( Pdr_Man_t * p );
217 extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
218 extern Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p );
219 /*=== pdrSat.c ==========================================================*/
220 extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k );
221 extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k );
222 extern void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k );
223 extern Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext );
224 extern Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray );
225 extern void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
226 extern void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues );
227 extern int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
228 extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit );
229 /*=== pdrTsim.c ==========================================================*/
230 extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
231 /*=== pdrTsim2.c ==========================================================*/
232 extern Txs_Man_t * Txs_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio );
233 extern void Txs_ManStop( Txs_Man_t * );
234 extern Pdr_Set_t * Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube );
235 /*=== pdrTsim3.c ==========================================================*/
236 extern Txs3_Man_t * Txs3_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio );
237 extern void Txs3_ManStop( Txs3_Man_t * );
238 extern Pdr_Set_t * Txs3_ManTernarySim( Txs3_Man_t * p, int k, Pdr_Set_t * pCube );
239 /*=== pdrUtil.c ==========================================================*/
240 extern Pdr_Set_t * Pdr_SetAlloc( int nSize );
241 extern Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits );
242 extern Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove );
243 extern Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits );
244 extern Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet );
245 extern Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p );
246 extern void Pdr_SetDeref( Pdr_Set_t * p );
247 extern Pdr_Set_t * ZPdr_SetIntersection( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep );
248 extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
249 extern int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
250 extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
251 extern int ZPdr_SetIsInit( Pdr_Set_t * p );
252 extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
253 extern void ZPdr_SetPrint( Pdr_Set_t * p );
254 extern void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
255 extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
256 extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
257 extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p );
258 extern void Pdr_OblDeref( Pdr_Obl_t * p );
259 extern int Pdr_QueueIsEmpty( Pdr_Man_t * p );
260 extern Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p );
261 extern Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p );
262 extern void Pdr_QueueClean( Pdr_Man_t * p );
263 extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
264 extern void Pdr_QueuePrint( Pdr_Man_t * p );
265 extern void Pdr_QueueStop( Pdr_Man_t * p );
266
267 ABC_NAMESPACE_HEADER_END
268
269
270 #endif
271
272 ////////////////////////////////////////////////////////////////////////
273 /// END OF FILE ///
274 ////////////////////////////////////////////////////////////////////////
275
276