1 /**CFile****************************************************************
2
3 FileName [pdrSat.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Property driven reachability.]
8
9 Synopsis [SAT solver procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - November 20, 2010.]
16
17 Revision [$Id: pdrSat.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "pdrInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Creates new SAT solver.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Pdr_ManCreateSolver(Pdr_Man_t * p,int k)45 sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
46 {
47 sat_solver * pSat;
48 Aig_Obj_t * pObj;
49 int i;
50 assert( Vec_PtrSize(p->vSolvers) == k );
51 assert( Vec_VecSize(p->vClauses) == k );
52 assert( Vec_IntSize(p->vActVars) == k );
53 // create new solver
54 // pSat = sat_solver_new();
55 pSat = zsat_solver_new_seed(p->pPars->nRandomSeed);
56 pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
57 Vec_PtrPush( p->vSolvers, pSat );
58 Vec_VecExpand( p->vClauses, k );
59 Vec_IntPush( p->vActVars, 0 );
60 // add property cone
61 Saig_ManForEachPo( p->pAig, pObj, i )
62 Pdr_ObjSatVar( p, k, 1, pObj );
63 return pSat;
64 }
65
66 /**Function*************************************************************
67
68 Synopsis [Returns old or restarted solver.]
69
70 Description []
71
72 SideEffects []
73
74 SeeAlso []
75
76 ***********************************************************************/
Pdr_ManFetchSolver(Pdr_Man_t * p,int k)77 sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
78 {
79 sat_solver * pSat;
80 Vec_Ptr_t * vArrayK;
81 Pdr_Set_t * pCube;
82 int i, j;
83 pSat = Pdr_ManSolver(p, k);
84 if ( Vec_IntEntry(p->vActVars, k) < p->pPars->nRecycle )
85 return pSat;
86 assert( k < Vec_PtrSize(p->vSolvers) - 1 );
87 p->nStarts++;
88 // sat_solver_delete( pSat );
89 // pSat = sat_solver_new();
90 // sat_solver_restart( pSat );
91 zsat_solver_restart_seed( pSat, p->pPars->nRandomSeed );
92 // create new SAT solver
93 pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
94 // write new SAT solver
95 Vec_PtrWriteEntry( p->vSolvers, k, pSat );
96 Vec_IntWriteEntry( p->vActVars, k, 0 );
97 // set the property output
98 Pdr_ManSetPropertyOutput( p, k );
99 // add the clauses
100 Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
101 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
102 Pdr_ManSolverAddClause( p, k, pCube );
103 return pSat;
104 }
105
106 /**Function*************************************************************
107
108 Synopsis [Converts SAT variables into register IDs.]
109
110 Description []
111
112 SideEffects []
113
114 SeeAlso []
115
116 ***********************************************************************/
Pdr_ManLitsToCube(Pdr_Man_t * p,int k,int * pArray,int nArray)117 Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray )
118 {
119 int i, RegId;
120 Vec_IntClear( p->vLits );
121 for ( i = 0; i < nArray; i++ )
122 {
123 RegId = Pdr_ObjRegNum( p, k, Abc_Lit2Var(pArray[i]) );
124 if ( RegId == -1 )
125 continue;
126 assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
127 Vec_IntPush( p->vLits, Abc_Var2Lit(RegId, !Abc_LitIsCompl(pArray[i])) );
128 }
129 assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
130 return p->vLits;
131 }
132
133 /**Function*************************************************************
134
135 Synopsis [Converts the cube in terms of RO numbers into array of CNF literals.]
136
137 Description []
138
139 SideEffects []
140
141 SeeAlso []
142
143 ***********************************************************************/
Pdr_ManCubeToLits(Pdr_Man_t * p,int k,Pdr_Set_t * pCube,int fCompl,int fNext)144 Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext )
145 {
146 Aig_Obj_t * pObj;
147 int i, iVar, iVarMax = 0;
148 abctime clk = Abc_Clock();
149 Vec_IntClear( p->vLits );
150 // assert( !(fNext && fCompl) );
151 for ( i = 0; i < pCube->nLits; i++ )
152 {
153 if ( pCube->Lits[i] == -1 )
154 continue;
155 if ( fNext )
156 pObj = Saig_ManLi( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
157 else
158 pObj = Saig_ManLo( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
159 iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - Abc_LitIsCompl(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
160 iVarMax = Abc_MaxInt( iVarMax, iVar );
161 Vec_IntPush( p->vLits, Abc_Var2Lit( iVar, fCompl ^ Abc_LitIsCompl(pCube->Lits[i]) ) );
162 }
163 // sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
164 p->tCnf += Abc_Clock() - clk;
165 return p->vLits;
166 }
167
168 /**Function*************************************************************
169
170 Synopsis [Sets the property output to 0 (sat) forever.]
171
172 Description []
173
174 SideEffects []
175
176 SeeAlso []
177
178 ***********************************************************************/
Pdr_ManSetPropertyOutput(Pdr_Man_t * p,int k)179 void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
180 {
181 sat_solver * pSat;
182 Aig_Obj_t * pObj;
183 int Lit, RetValue, i;
184 if ( !p->pPars->fUsePropOut )
185 return;
186 pSat = Pdr_ManSolver(p, k);
187 Saig_ManForEachPo( p->pAig, pObj, i )
188 {
189 // skip solved outputs
190 if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
191 continue;
192 // skip timedout outputs
193 if ( p->pPars->vOutMap && Vec_IntEntry(p->pPars->vOutMap, i) == -1 )
194 continue;
195 Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
196 RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
197 assert( RetValue == 1 );
198 }
199 sat_solver_compress( pSat );
200 }
201
202 /**Function*************************************************************
203
204 Synopsis [Adds one clause in terms of ROs to the k-th SAT solver.]
205
206 Description []
207
208 SideEffects []
209
210 SeeAlso []
211
212 ***********************************************************************/
Pdr_ManSolverAddClause(Pdr_Man_t * p,int k,Pdr_Set_t * pCube)213 void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
214 {
215 sat_solver * pSat;
216 Vec_Int_t * vLits;
217 int RetValue;
218 pSat = Pdr_ManSolver(p, k);
219 vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
220 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
221 assert( RetValue == 1 );
222 sat_solver_compress( pSat );
223 }
224
225 /**Function*************************************************************
226
227 Synopsis [Collects values of the RO/RI variables in k-th SAT solver.]
228
229 Description []
230
231 SideEffects []
232
233 SeeAlso []
234
235 ***********************************************************************/
Pdr_ManCollectValues(Pdr_Man_t * p,int k,Vec_Int_t * vObjIds,Vec_Int_t * vValues)236 void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues )
237 {
238 sat_solver * pSat;
239 Aig_Obj_t * pObj;
240 int iVar, i;
241 Vec_IntClear( vValues );
242 pSat = Pdr_ManSolver(p, k);
243 Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i )
244 {
245 iVar = Pdr_ObjSatVar( p, k, 3, pObj ); assert( iVar >= 0 );
246 Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
247 }
248 }
249
250 /**Function*************************************************************
251
252 Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]
253
254 Description [Return 1/0 if cube or property are proved to hold/fail
255 in k-th timeframe. Returns the predecessor bad state in ppPred.]
256
257 SideEffects []
258
259 SeeAlso []
260
261 ***********************************************************************/
Pdr_ManCheckCubeCs(Pdr_Man_t * p,int k,Pdr_Set_t * pCube)262 int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
263 {
264 sat_solver * pSat;
265 Vec_Int_t * vLits;
266 abctime Limit;
267 int RetValue;
268 pSat = Pdr_ManFetchSolver( p, k );
269 vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
270 Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
271 RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
272 sat_solver_set_runtime_limit( pSat, Limit );
273 if ( RetValue == l_Undef )
274 return -1;
275 return (RetValue == l_False);
276 }
277
278 /**Function*************************************************************
279
280 Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]
281
282 Description [Return 1/0 if cube or property are proved to hold/fail
283 in k-th timeframe. Returns the predecessor bad state in ppPred.]
284
285 SideEffects []
286
287 SeeAlso []
288
289 ***********************************************************************/
Pdr_ManCheckCube(Pdr_Man_t * p,int k,Pdr_Set_t * pCube,Pdr_Set_t ** ppPred,int nConfLimit,int fTryConf,int fUseLit)290 int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit )
291 {
292 //int fUseLit = 0;
293 int fLitUsed = 0;
294 sat_solver * pSat;
295 Vec_Int_t * vLits;
296 int Lit, RetValue;
297 abctime clk, Limit;
298 p->nCalls++;
299 pSat = Pdr_ManFetchSolver( p, k );
300 if ( pCube == NULL ) // solve the property
301 {
302 clk = Abc_Clock();
303 Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)), 0 ); // pos literal (property fails)
304 Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
305 RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
306 sat_solver_set_runtime_limit( pSat, Limit );
307 if ( RetValue == l_Undef )
308 return -1;
309 }
310 else // check relative containment in terms of next states
311 {
312 if ( fUseLit )
313 {
314 fLitUsed = 1;
315 Vec_IntAddToEntry( p->vActVars, k, 1 );
316 // add the cube in terms of current state variables
317 vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
318 // add activation literal
319 Lit = Abc_Var2Lit( Pdr_ManFreeVar(p, k), 0 );
320 // add activation literal
321 Vec_IntPush( vLits, Lit );
322 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
323 assert( RetValue == 1 );
324 sat_solver_compress( pSat );
325 // create assumptions
326 vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
327 // add activation literal
328 Vec_IntPush( vLits, Abc_LitNot(Lit) );
329 }
330 else
331 vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
332
333 // solve
334 clk = Abc_Clock();
335 Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
336 RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), fTryConf ? p->pPars->nConfGenLimit : nConfLimit, 0, 0, 0 );
337 sat_solver_set_runtime_limit( pSat, Limit );
338 if ( RetValue == l_Undef )
339 {
340 if ( fTryConf && p->pPars->nConfGenLimit )
341 RetValue = l_True;
342 else
343 return -1;
344 }
345 }
346 clk = Abc_Clock() - clk;
347 p->tSat += clk;
348 assert( RetValue != l_Undef );
349 if ( RetValue == l_False )
350 {
351 p->tSatUnsat += clk;
352 p->nCallsU++;
353 if ( ppPred )
354 *ppPred = NULL;
355 RetValue = 1;
356 }
357 else // if ( RetValue == l_True )
358 {
359 p->tSatSat += clk;
360 p->nCallsS++;
361 if ( ppPred )
362 {
363 abctime clk = Abc_Clock();
364 if ( p->pPars->fNewXSim )
365 *ppPred = Txs3_ManTernarySim( p->pTxs3, k, pCube );
366 else
367 *ppPred = Pdr_ManTernarySim( p, k, pCube );
368 p->tTsim += Abc_Clock() - clk;
369 p->nXsimLits += (*ppPred)->nLits;
370 p->nXsimRuns++;
371 }
372 RetValue = 0;
373 }
374
375 /* // for some reason, it does not work...
376 if ( fLitUsed )
377 {
378 int RetValue;
379 Lit = Abc_LitNot(Lit);
380 RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
381 assert( RetValue == 1 );
382 sat_solver_compress( pSat );
383 }
384 */
385 return RetValue;
386 }
387
388
389 ////////////////////////////////////////////////////////////////////////
390 /// END OF FILE ///
391 ////////////////////////////////////////////////////////////////////////
392
393
394 ABC_NAMESPACE_IMPL_END
395
396