1 /**CFile****************************************************************
2
3 FileName [cecSolve.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Combinational equivalence checking.]
8
9 Synopsis [Performs one round of SAT solving.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: cecSolve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "cecInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
Cec_ObjSatNum(Cec_ManSat_t * p,Gia_Obj_t * pObj)30 static inline int Cec_ObjSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj ) { return p->pSatVars[Gia_ObjId(p->pAig,pObj)]; }
Cec_ObjSetSatNum(Cec_ManSat_t * p,Gia_Obj_t * pObj,int Num)31 static inline void Cec_ObjSetSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj, int Num ) { p->pSatVars[Gia_ObjId(p->pAig,pObj)] = Num; }
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis [Returns value of the SAT variable.]
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Cec_ObjSatVarValue(Cec_ManSat_t * p,Gia_Obj_t * pObj)48 int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj )
49 {
50 return sat_solver_var_value( p->pSat, Cec_ObjSatNum(p, pObj) );
51 }
52
53 /**Function*************************************************************
54
55 Synopsis [Addes clauses to the solver.]
56
57 Description []
58
59 SideEffects []
60
61 SeeAlso []
62
63 ***********************************************************************/
Cec_AddClausesMux(Cec_ManSat_t * p,Gia_Obj_t * pNode)64 void Cec_AddClausesMux( Cec_ManSat_t * p, Gia_Obj_t * pNode )
65 {
66 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
67 int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
68
69 assert( !Gia_IsComplement( pNode ) );
70 assert( Gia_ObjIsMuxType( pNode ) );
71 // get nodes (I = if, T = then, E = else)
72 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
73 // get the variable numbers
74 VarF = Cec_ObjSatNum(p,pNode);
75 VarI = Cec_ObjSatNum(p,pNodeI);
76 VarT = Cec_ObjSatNum(p,Gia_Regular(pNodeT));
77 VarE = Cec_ObjSatNum(p,Gia_Regular(pNodeE));
78 // get the complementation flags
79 fCompT = Gia_IsComplement(pNodeT);
80 fCompE = Gia_IsComplement(pNodeE);
81
82 // f = ITE(i, t, e)
83
84 // i' + t' + f
85 // i' + t + f'
86 // i + e' + f
87 // i + e + f'
88
89 // create four clauses
90 pLits[0] = toLitCond(VarI, 1);
91 pLits[1] = toLitCond(VarT, 1^fCompT);
92 pLits[2] = toLitCond(VarF, 0);
93 if ( p->pPars->fPolarFlip )
94 {
95 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
96 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
97 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
98 }
99 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
100 assert( RetValue );
101 pLits[0] = toLitCond(VarI, 1);
102 pLits[1] = toLitCond(VarT, 0^fCompT);
103 pLits[2] = toLitCond(VarF, 1);
104 if ( p->pPars->fPolarFlip )
105 {
106 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
107 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
108 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
109 }
110 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
111 assert( RetValue );
112 pLits[0] = toLitCond(VarI, 0);
113 pLits[1] = toLitCond(VarE, 1^fCompE);
114 pLits[2] = toLitCond(VarF, 0);
115 if ( p->pPars->fPolarFlip )
116 {
117 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
118 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
119 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
120 }
121 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
122 assert( RetValue );
123 pLits[0] = toLitCond(VarI, 0);
124 pLits[1] = toLitCond(VarE, 0^fCompE);
125 pLits[2] = toLitCond(VarF, 1);
126 if ( p->pPars->fPolarFlip )
127 {
128 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
129 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
130 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
131 }
132 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
133 assert( RetValue );
134
135 // two additional clauses
136 // t' & e' -> f'
137 // t & e -> f
138
139 // t + e + f'
140 // t' + e' + f
141
142 if ( VarT == VarE )
143 {
144 // assert( fCompT == !fCompE );
145 return;
146 }
147
148 pLits[0] = toLitCond(VarT, 0^fCompT);
149 pLits[1] = toLitCond(VarE, 0^fCompE);
150 pLits[2] = toLitCond(VarF, 1);
151 if ( p->pPars->fPolarFlip )
152 {
153 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
154 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
155 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
156 }
157 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
158 assert( RetValue );
159 pLits[0] = toLitCond(VarT, 1^fCompT);
160 pLits[1] = toLitCond(VarE, 1^fCompE);
161 pLits[2] = toLitCond(VarF, 0);
162 if ( p->pPars->fPolarFlip )
163 {
164 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
165 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
166 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
167 }
168 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
169 assert( RetValue );
170 }
171
172 /**Function*************************************************************
173
174 Synopsis [Addes clauses to the solver.]
175
176 Description []
177
178 SideEffects []
179
180 SeeAlso []
181
182 ***********************************************************************/
Cec_AddClausesSuper(Cec_ManSat_t * p,Gia_Obj_t * pNode,Vec_Ptr_t * vSuper)183 void Cec_AddClausesSuper( Cec_ManSat_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper )
184 {
185 Gia_Obj_t * pFanin;
186 int * pLits, nLits, RetValue, i;
187 assert( !Gia_IsComplement(pNode) );
188 assert( Gia_ObjIsAnd( pNode ) );
189 // create storage for literals
190 nLits = Vec_PtrSize(vSuper) + 1;
191 pLits = ABC_ALLOC( int, nLits );
192 // suppose AND-gate is A & B = C
193 // add !A => !C or A + !C
194 Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
195 {
196 pLits[0] = toLitCond(Cec_ObjSatNum(p,Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
197 pLits[1] = toLitCond(Cec_ObjSatNum(p,pNode), 1);
198 if ( p->pPars->fPolarFlip )
199 {
200 if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
201 if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
202 }
203 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
204 assert( RetValue );
205 }
206 // add A & B => C or !A + !B + C
207 Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
208 {
209 pLits[i] = toLitCond(Cec_ObjSatNum(p,Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
210 if ( p->pPars->fPolarFlip )
211 {
212 if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
213 }
214 }
215 pLits[nLits-1] = toLitCond(Cec_ObjSatNum(p,pNode), 0);
216 if ( p->pPars->fPolarFlip )
217 {
218 if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
219 }
220 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
221 assert( RetValue );
222 ABC_FREE( pLits );
223 }
224
225 /**Function*************************************************************
226
227 Synopsis [Collects the supergate.]
228
229 Description []
230
231 SideEffects []
232
233 SeeAlso []
234
235 ***********************************************************************/
Cec_CollectSuper_rec(Gia_Obj_t * pObj,Vec_Ptr_t * vSuper,int fFirst,int fUseMuxes)236 void Cec_CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
237 {
238 // if the new node is complemented or a PI, another gate begins
239 if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) ||
240 (!fFirst && Gia_ObjValue(pObj) > 1) ||
241 (fUseMuxes && Gia_ObjIsMuxType(pObj)) )
242 {
243 Vec_PtrPushUnique( vSuper, pObj );
244 return;
245 }
246 // go through the branches
247 Cec_CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
248 Cec_CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
249 }
250
251 /**Function*************************************************************
252
253 Synopsis [Collects the supergate.]
254
255 Description []
256
257 SideEffects []
258
259 SeeAlso []
260
261 ***********************************************************************/
Cec_CollectSuper(Gia_Obj_t * pObj,int fUseMuxes,Vec_Ptr_t * vSuper)262 void Cec_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
263 {
264 assert( !Gia_IsComplement(pObj) );
265 assert( !Gia_ObjIsCi(pObj) );
266 Vec_PtrClear( vSuper );
267 Cec_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
268 }
269
270 /**Function*************************************************************
271
272 Synopsis [Updates the solver clause database.]
273
274 Description []
275
276 SideEffects []
277
278 SeeAlso []
279
280 ***********************************************************************/
Cec_ObjAddToFrontier(Cec_ManSat_t * p,Gia_Obj_t * pObj,Vec_Ptr_t * vFrontier)281 void Cec_ObjAddToFrontier( Cec_ManSat_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier )
282 {
283 assert( !Gia_IsComplement(pObj) );
284 if ( Cec_ObjSatNum(p,pObj) )
285 return;
286 assert( Cec_ObjSatNum(p,pObj) == 0 );
287 if ( Gia_ObjIsConst0(pObj) )
288 return;
289 Vec_PtrPush( p->vUsedNodes, pObj );
290 Cec_ObjSetSatNum( p, pObj, p->nSatVars++ );
291 if ( Gia_ObjIsAnd(pObj) )
292 Vec_PtrPush( vFrontier, pObj );
293 }
294
295 /**Function*************************************************************
296
297 Synopsis [Updates the solver clause database.]
298
299 Description []
300
301 SideEffects []
302
303 SeeAlso []
304
305 ***********************************************************************/
Cec_CnfNodeAddToSolver(Cec_ManSat_t * p,Gia_Obj_t * pObj)306 void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Gia_Obj_t * pObj )
307 {
308 Vec_Ptr_t * vFrontier;
309 Gia_Obj_t * pNode, * pFanin;
310 int i, k, fUseMuxes = 1;
311 // quit if CNF is ready
312 if ( Cec_ObjSatNum(p,pObj) )
313 return;
314 if ( Gia_ObjIsCi(pObj) )
315 {
316 Vec_PtrPush( p->vUsedNodes, pObj );
317 Cec_ObjSetSatNum( p, pObj, p->nSatVars++ );
318 sat_solver_setnvars( p->pSat, p->nSatVars );
319 return;
320 }
321 assert( Gia_ObjIsAnd(pObj) );
322 // start the frontier
323 vFrontier = Vec_PtrAlloc( 100 );
324 Cec_ObjAddToFrontier( p, pObj, vFrontier );
325 // explore nodes in the frontier
326 Vec_PtrForEachEntry( Gia_Obj_t *, vFrontier, pNode, i )
327 {
328 // create the supergate
329 assert( Cec_ObjSatNum(p,pNode) );
330 if ( fUseMuxes && Gia_ObjIsMuxType(pNode) )
331 {
332 Vec_PtrClear( p->vFanins );
333 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) );
334 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) );
335 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) );
336 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) );
337 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
338 Cec_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier );
339 Cec_AddClausesMux( p, pNode );
340 }
341 else
342 {
343 Cec_CollectSuper( pNode, fUseMuxes, p->vFanins );
344 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
345 Cec_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier );
346 Cec_AddClausesSuper( p, pNode, p->vFanins );
347 }
348 assert( Vec_PtrSize(p->vFanins) > 1 );
349 }
350 Vec_PtrFree( vFrontier );
351 }
352
353
354 /**Function*************************************************************
355
356 Synopsis [Recycles the SAT solver.]
357
358 Description []
359
360 SideEffects []
361
362 SeeAlso []
363
364 ***********************************************************************/
Cec_ManSatSolverRecycle(Cec_ManSat_t * p)365 void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
366 {
367 int Lit;
368 if ( p->pSat )
369 {
370 Gia_Obj_t * pObj;
371 int i;
372 Vec_PtrForEachEntry( Gia_Obj_t *, p->vUsedNodes, pObj, i )
373 Cec_ObjSetSatNum( p, pObj, 0 );
374 Vec_PtrClear( p->vUsedNodes );
375 // memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) );
376 sat_solver_delete( p->pSat );
377 }
378 p->pSat = sat_solver_new();
379 sat_solver_setnvars( p->pSat, 1000 );
380 p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
381 // var 0 is not used
382 // var 1 is reserved for const0 node - add the clause
383 p->nSatVars = 1;
384 // p->nSatVars = 0;
385 Lit = toLitCond( p->nSatVars, 1 );
386 // if ( p->pPars->fPolarFlip ) // no need to normalize const0 node (bug fix by SS on 9/17/2012)
387 // Lit = lit_neg( Lit );
388 sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
389 Cec_ObjSetSatNum( p, Gia_ManConst0(p->pAig), p->nSatVars++ );
390
391 p->nRecycles++;
392 p->nCallsSince = 0;
393 }
394
395 /**Function*************************************************************
396
397 Synopsis [Sets variable activities in the cone.]
398
399 Description []
400
401 SideEffects []
402
403 SeeAlso []
404
405 ***********************************************************************/
Cec_SetActivityFactors_rec(Cec_ManSat_t * p,Gia_Obj_t * pObj,int LevelMin,int LevelMax)406 void Cec_SetActivityFactors_rec( Cec_ManSat_t * p, Gia_Obj_t * pObj, int LevelMin, int LevelMax )
407 {
408 float dActConeBumpMax = 20.0;
409 int iVar;
410 // skip visited variables
411 if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
412 return;
413 Gia_ObjSetTravIdCurrent(p->pAig, pObj);
414 // add the PI to the list
415 if ( Gia_ObjLevel(p->pAig, pObj) <= LevelMin || Gia_ObjIsCi(pObj) )
416 return;
417 // set the factor of this variable
418 // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
419 if ( (iVar = Cec_ObjSatNum(p,pObj)) )
420 {
421 p->pSat->factors[iVar] = dActConeBumpMax * (Gia_ObjLevel(p->pAig, pObj) - LevelMin)/(LevelMax - LevelMin);
422 veci_push(&p->pSat->act_vars, iVar);
423 }
424 // explore the fanins
425 Cec_SetActivityFactors_rec( p, Gia_ObjFanin0(pObj), LevelMin, LevelMax );
426 Cec_SetActivityFactors_rec( p, Gia_ObjFanin1(pObj), LevelMin, LevelMax );
427 }
428
429 /**Function*************************************************************
430
431 Synopsis [Sets variable activities in the cone.]
432
433 Description []
434
435 SideEffects []
436
437 SeeAlso []
438
439 ***********************************************************************/
Cec_SetActivityFactors(Cec_ManSat_t * p,Gia_Obj_t * pObj)440 int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj )
441 {
442 float dActConeRatio = 0.5;
443 int LevelMin, LevelMax;
444 // reset the active variables
445 veci_resize(&p->pSat->act_vars, 0);
446 // prepare for traversal
447 Gia_ManIncrementTravId( p->pAig );
448 // determine the min and max level to visit
449 assert( dActConeRatio > 0 && dActConeRatio < 1 );
450 LevelMax = Gia_ObjLevel(p->pAig,pObj);
451 LevelMin = (int)(LevelMax * (1.0 - dActConeRatio));
452 // traverse
453 Cec_SetActivityFactors_rec( p, pObj, LevelMin, LevelMax );
454 //Cec_PrintActivity( p );
455 return 1;
456 }
457
458
459 /**Function*************************************************************
460
461 Synopsis [Runs equivalence test for the two nodes.]
462
463 Description []
464
465 SideEffects []
466
467 SeeAlso []
468
469 ***********************************************************************/
Cec_ManSatCheckNode(Cec_ManSat_t * p,Gia_Obj_t * pObj)470 int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
471 {
472 Gia_Obj_t * pObjR = Gia_Regular(pObj);
473 int nBTLimit = p->pPars->nBTLimit;
474 int Lit, RetValue, status, nConflicts;
475 abctime clk, clk2;
476
477 if ( pObj == Gia_ManConst0(p->pAig) )
478 return 1;
479 if ( pObj == Gia_ManConst1(p->pAig) )
480 {
481 assert( 0 );
482 return 0;
483 }
484
485 p->nCallsSince++; // experiment with this!!!
486 p->nSatTotal++;
487
488 // check if SAT solver needs recycling
489 if ( p->pSat == NULL ||
490 (p->pPars->nSatVarMax &&
491 p->nSatVars > p->pPars->nSatVarMax &&
492 p->nCallsSince > p->pPars->nCallsRecycle) )
493 Cec_ManSatSolverRecycle( p );
494
495 // if the nodes do not have SAT variables, allocate them
496 clk2 = Abc_Clock();
497 Cec_CnfNodeAddToSolver( p, pObjR );
498 //ABC_PRT( "cnf", Abc_Clock() - clk2 );
499 //Abc_Print( 1, "%d \n", p->pSat->size );
500
501 clk2 = Abc_Clock();
502 // Cec_SetActivityFactors( p, pObjR );
503 //ABC_PRT( "act", Abc_Clock() - clk2 );
504
505 // propage unit clauses
506 if ( p->pSat->qtail != p->pSat->qhead )
507 {
508 status = sat_solver_simplify(p->pSat);
509 assert( status != 0 );
510 assert( p->pSat->qtail == p->pSat->qhead );
511 }
512
513 // solve under assumptions
514 // A = 1; B = 0 OR A = 1; B = 1
515 Lit = toLitCond( Cec_ObjSatNum(p,pObjR), Gia_IsComplement(pObj) );
516 if ( p->pPars->fPolarFlip )
517 {
518 if ( pObjR->fPhase ) Lit = lit_neg( Lit );
519 }
520 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
521 clk = Abc_Clock();
522 nConflicts = p->pSat->stats.conflicts;
523
524 clk2 = Abc_Clock();
525 RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1,
526 (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
527 //ABC_PRT( "sat", Abc_Clock() - clk2 );
528
529 if ( RetValue == l_False )
530 {
531 p->timeSatUnsat += Abc_Clock() - clk;
532 Lit = lit_neg( Lit );
533 RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
534 assert( RetValue );
535 p->nSatUnsat++;
536 p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;
537 //Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
538 return 1;
539 }
540 else if ( RetValue == l_True )
541 {
542 p->timeSatSat += Abc_Clock() - clk;
543 p->nSatSat++;
544 p->nConfSat += p->pSat->stats.conflicts - nConflicts;
545 //Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
546 return 0;
547 }
548 else // if ( RetValue == l_Undef )
549 {
550 p->timeSatUndec += Abc_Clock() - clk;
551 p->nSatUndec++;
552 p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
553 //Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
554 return -1;
555 }
556 }
557
558 /**Function*************************************************************
559
560 Synopsis [Runs equivalence test for the two nodes.]
561
562 Description []
563
564 SideEffects []
565
566 SeeAlso []
567
568 ***********************************************************************/
Cec_ManSatCheckNodeTwo(Cec_ManSat_t * p,Gia_Obj_t * pObj1,Gia_Obj_t * pObj2)569 int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 )
570 {
571 Gia_Obj_t * pObjR1 = Gia_Regular(pObj1);
572 Gia_Obj_t * pObjR2 = Gia_Regular(pObj2);
573 int nBTLimit = p->pPars->nBTLimit;
574 int Lits[2], RetValue, status, nConflicts;
575 abctime clk, clk2;
576
577 if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) )
578 return 1;
579 if ( pObj1 == Gia_ManConst1(p->pAig) && (pObj2 == NULL || pObj2 == Gia_ManConst1(p->pAig)) )
580 {
581 assert( 0 );
582 return 0;
583 }
584
585 p->nCallsSince++; // experiment with this!!!
586 p->nSatTotal++;
587
588 // check if SAT solver needs recycling
589 if ( p->pSat == NULL ||
590 (p->pPars->nSatVarMax &&
591 p->nSatVars > p->pPars->nSatVarMax &&
592 p->nCallsSince > p->pPars->nCallsRecycle) )
593 Cec_ManSatSolverRecycle( p );
594
595 // if the nodes do not have SAT variables, allocate them
596 clk2 = Abc_Clock();
597 Cec_CnfNodeAddToSolver( p, pObjR1 );
598 Cec_CnfNodeAddToSolver( p, pObjR2 );
599 //ABC_PRT( "cnf", Abc_Clock() - clk2 );
600 //Abc_Print( 1, "%d \n", p->pSat->size );
601
602 clk2 = Abc_Clock();
603 // Cec_SetActivityFactors( p, pObjR1 );
604 // Cec_SetActivityFactors( p, pObjR2 );
605 //ABC_PRT( "act", Abc_Clock() - clk2 );
606
607 // propage unit clauses
608 if ( p->pSat->qtail != p->pSat->qhead )
609 {
610 status = sat_solver_simplify(p->pSat);
611 assert( status != 0 );
612 assert( p->pSat->qtail == p->pSat->qhead );
613 }
614
615 // solve under assumptions
616 // A = 1; B = 0 OR A = 1; B = 1
617 Lits[0] = toLitCond( Cec_ObjSatNum(p,pObjR1), Gia_IsComplement(pObj1) );
618 Lits[1] = toLitCond( Cec_ObjSatNum(p,pObjR2), Gia_IsComplement(pObj2) );
619 if ( p->pPars->fPolarFlip )
620 {
621 if ( pObjR1->fPhase ) Lits[0] = lit_neg( Lits[0] );
622 if ( pObjR2->fPhase ) Lits[1] = lit_neg( Lits[1] );
623 }
624 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
625 clk = Abc_Clock();
626 nConflicts = p->pSat->stats.conflicts;
627
628 clk2 = Abc_Clock();
629 RetValue = sat_solver_solve( p->pSat, Lits, Lits + 2,
630 (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
631 //ABC_PRT( "sat", Abc_Clock() - clk2 );
632
633 if ( RetValue == l_False )
634 {
635 p->timeSatUnsat += Abc_Clock() - clk;
636 Lits[0] = lit_neg( Lits[0] );
637 Lits[1] = lit_neg( Lits[1] );
638 RetValue = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
639 assert( RetValue );
640 p->nSatUnsat++;
641 p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;
642 //Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
643 return 1;
644 }
645 else if ( RetValue == l_True )
646 {
647 p->timeSatSat += Abc_Clock() - clk;
648 p->nSatSat++;
649 p->nConfSat += p->pSat->stats.conflicts - nConflicts;
650 //Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
651 return 0;
652 }
653 else // if ( RetValue == l_Undef )
654 {
655 p->timeSatUndec += Abc_Clock() - clk;
656 p->nSatUndec++;
657 p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
658 //Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
659 return -1;
660 }
661 }
662
663
664 /**Function*************************************************************
665
666 Synopsis [Performs one round of solving for the POs of the AIG.]
667
668 Description [Labels the nodes that have been proved (pObj->fMark1)
669 and returns the set of satisfying assignments.]
670
671 SideEffects []
672
673 SeeAlso []
674
675 ***********************************************************************/
Cex_ManGenSimple(Cec_ManSat_t * p,int iOut)676 Abc_Cex_t * Cex_ManGenSimple( Cec_ManSat_t * p, int iOut )
677 {
678 Abc_Cex_t * pCex;
679 pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p->pAig), 1 );
680 pCex->iPo = iOut;
681 pCex->iFrame = 0;
682 return pCex;
683 }
Cex_ManGenCex(Cec_ManSat_t * p,int iOut)684 Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut )
685 {
686 Abc_Cex_t * pCex;
687 int i;
688 pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p->pAig), 1 );
689 pCex->iPo = iOut;
690 pCex->iFrame = 0;
691 for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
692 {
693 int iVar = Cec_ObjSatNum(p, Gia_ManCi(p->pAig, i));
694 if ( iVar > 0 && sat_solver_var_value(p->pSat, iVar) )
695 pCex->pData[i>>5] |= (1<<(i & 31));
696 }
697 return pCex;
698 }
Cec_ManSatSolve(Cec_ManPat_t * pPat,Gia_Man_t * pAig,Cec_ParSat_t * pPars,Vec_Int_t * vIdsOrig,Vec_Int_t * vMiterPairs,Vec_Int_t * vEquivPairs)699 void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs )
700 {
701 Bar_Progress_t * pProgress = NULL;
702 Cec_ManSat_t * p;
703 Gia_Obj_t * pObj;
704 int i, status;
705 abctime clk = Abc_Clock(), clk2;
706 Vec_PtrFreeP( &pAig->vSeqModelVec );
707 if ( pPars->fSaveCexes )
708 pAig->vSeqModelVec = Vec_PtrStart( Gia_ManCoNum(pAig) );
709 // reset the manager
710 if ( pPat )
711 {
712 pPat->iStart = Vec_StrSize(pPat->vStorage);
713 pPat->nPats = 0;
714 pPat->nPatLits = 0;
715 pPat->nPatLitsMin = 0;
716 }
717 Gia_ManSetPhase( pAig );
718 Gia_ManLevelNum( pAig );
719 Gia_ManIncrementTravId( pAig );
720 p = Cec_ManSatCreate( pAig, pPars );
721 pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
722 Gia_ManForEachCo( pAig, pObj, i )
723 {
724 if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
725 {
726 status = !Gia_ObjFaninC0(pObj);
727 pObj->fMark0 = (status == 0);
728 pObj->fMark1 = (status == 1);
729 if ( pPars->fSaveCexes )
730 Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenSimple(p, i) );
731 continue;
732 }
733 Bar_ProgressUpdate( pProgress, i, "SAT..." );
734 clk2 = Abc_Clock();
735 status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
736 pObj->fMark0 = (status == 0);
737 pObj->fMark1 = (status == 1);
738 if ( status == 1 && vIdsOrig )
739 {
740 int iObj1 = Vec_IntEntry(vMiterPairs, 2*i);
741 int iObj2 = Vec_IntEntry(vMiterPairs, 2*i+1);
742 int OrigId1 = Vec_IntEntry(vIdsOrig, iObj1);
743 int OrigId2 = Vec_IntEntry(vIdsOrig, iObj2);
744 assert( OrigId1 >= 0 && OrigId2 >= 0 );
745 Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 );
746 }
747 if ( pPars->fSaveCexes && status != -1 )
748 Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenCex(p, i) );
749
750 /*
751 if ( status == -1 )
752 {
753 Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
754 Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0, 0 );
755 Gia_ManStop( pTemp );
756 Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
757 }
758 */
759 if ( status != 0 )
760 continue;
761 // save the pattern
762 if ( pPat )
763 {
764 abctime clk3 = Abc_Clock();
765 Cec_ManPatSavePattern( pPat, p, pObj );
766 pPat->timeTotalSave += Abc_Clock() - clk3;
767 }
768 // quit if one of them is solved
769 if ( pPars->fCheckMiter )
770 break;
771 }
772 p->timeTotal = Abc_Clock() - clk;
773 Bar_ProgressStop( pProgress );
774 if ( pPars->fVerbose )
775 Cec_ManSatPrintStats( p );
776 Cec_ManSatStop( p );
777 }
778
779 /**Function*************************************************************
780
781 Synopsis [Performs one round of solving for the POs of the AIG.]
782
783 Description [Labels the nodes that have been proved (pObj->fMark1)
784 and returns the set of satisfying assignments.]
785
786 SideEffects []
787
788 SeeAlso []
789
790 ***********************************************************************/
Cec_ManSatSolveExractPattern(Vec_Int_t * vCexStore,int iStart,Vec_Int_t * vPat)791 int Cec_ManSatSolveExractPattern( Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vPat )
792 {
793 int k, nSize;
794 Vec_IntClear( vPat );
795 // skip the output number
796 iStart++;
797 // get the number of items
798 nSize = Vec_IntEntry( vCexStore, iStart++ );
799 if ( nSize <= 0 )
800 return iStart;
801 // extract pattern
802 for ( k = 0; k < nSize; k++ )
803 Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
804 return iStart;
805 }
Cec_ManSatSolveCSat(Cec_ManPat_t * pPat,Gia_Man_t * pAig,Cec_ParSat_t * pPars)806 void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
807 {
808 Vec_Str_t * vStatus;
809 Vec_Int_t * vPat = Vec_IntAlloc( 1000 );
810 Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 );
811 Gia_Obj_t * pObj;
812 int i, status, iStart = 0;
813 assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) );
814 // reset the manager
815 if ( pPat )
816 {
817 pPat->iStart = Vec_StrSize(pPat->vStorage);
818 pPat->nPats = 0;
819 pPat->nPatLits = 0;
820 pPat->nPatLitsMin = 0;
821 }
822 Gia_ManForEachCo( pAig, pObj, i )
823 {
824 status = (int)Vec_StrEntry(vStatus, i);
825 pObj->fMark0 = (status == 0);
826 pObj->fMark1 = (status == 1);
827 if ( Vec_IntSize(vCexStore) > 0 && status != 1 )
828 iStart = Cec_ManSatSolveExractPattern( vCexStore, iStart, vPat );
829 if ( status != 0 )
830 continue;
831 // save the pattern
832 if ( pPat && Vec_IntSize(vPat) > 0 )
833 {
834 abctime clk3 = Abc_Clock();
835 Cec_ManPatSavePatternCSat( pPat, vPat );
836 pPat->timeTotalSave += Abc_Clock() - clk3;
837 }
838 // quit if one of them is solved
839 if ( pPars->fCheckMiter )
840 break;
841 }
842 assert( iStart == Vec_IntSize(vCexStore) );
843 Vec_IntFree( vPat );
844 Vec_StrFree( vStatus );
845 Vec_IntFree( vCexStore );
846 }
847
848
849
850 /**Function*************************************************************
851
852 Synopsis [Returns the pattern stored.]
853
854 Description []
855
856 SideEffects []
857
858 SeeAlso []
859
860 ***********************************************************************/
Cec_ManSatReadCex(Cec_ManSat_t * pSat)861 Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * pSat )
862 {
863 return pSat->vCex;
864 }
865
866 /**Function*************************************************************
867
868 Synopsis [Save values in the cone of influence.]
869
870 Description []
871
872 SideEffects []
873
874 SeeAlso []
875
876 ***********************************************************************/
Cec_ManSatSolveSeq_rec(Cec_ManSat_t * pSat,Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Ptr_t * vInfo,int iPat,int nRegs)877 void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vInfo, int iPat, int nRegs )
878 {
879 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
880 return;
881 Gia_ObjSetTravIdCurrent(p, pObj);
882 if ( Gia_ObjIsCi(pObj) )
883 {
884 unsigned * pInfo = (unsigned *)Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
885 if ( Cec_ObjSatVarValue( pSat, pObj ) != Abc_InfoHasBit( pInfo, iPat ) )
886 Abc_InfoXorBit( pInfo, iPat );
887 pSat->nCexLits++;
888 // Vec_IntPush( pSat->vCex, Abc_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
889 return;
890 }
891 assert( Gia_ObjIsAnd(pObj) );
892 Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin0(pObj), vInfo, iPat, nRegs );
893 Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin1(pObj), vInfo, iPat, nRegs );
894 }
895
896 /**Function*************************************************************
897
898 Synopsis [Performs one round of solving for the POs of the AIG.]
899
900 Description [Labels the nodes that have been proved (pObj->fMark1)
901 and returns the set of satisfying assignments.]
902
903 SideEffects []
904
905 SeeAlso []
906
907 ***********************************************************************/
Cec_ManSatSolveSeq(Vec_Ptr_t * vPatts,Gia_Man_t * pAig,Cec_ParSat_t * pPars,int nRegs,int * pnPats)908 Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats )
909 {
910 Bar_Progress_t * pProgress = NULL;
911 Vec_Str_t * vStatus;
912 Cec_ManSat_t * p;
913 Gia_Obj_t * pObj;
914 int iPat = 0, nPatsInit, nPats;
915 int i, status;
916 abctime clk = Abc_Clock();
917 nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
918 Gia_ManSetPhase( pAig );
919 Gia_ManLevelNum( pAig );
920 Gia_ManIncrementTravId( pAig );
921 p = Cec_ManSatCreate( pAig, pPars );
922 vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
923 pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
924 Gia_ManForEachCo( pAig, pObj, i )
925 {
926 Bar_ProgressUpdate( pProgress, i, "SAT..." );
927 if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
928 {
929 if ( Gia_ObjFaninC0(pObj) )
930 {
931 // Abc_Print( 1, "Constant 1 output of SRM!!!\n" );
932 Vec_StrPush( vStatus, 0 );
933 }
934 else
935 {
936 // Abc_Print( 1, "Constant 0 output of SRM!!!\n" );
937 Vec_StrPush( vStatus, 1 );
938 }
939 continue;
940 }
941 status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
942 //Abc_Print( 1, "output %d status = %d\n", i, status );
943 Vec_StrPush( vStatus, (char)status );
944 if ( status != 0 )
945 continue;
946 // resize storage
947 if ( iPat == nPats )
948 {
949 int nWords = Vec_PtrReadWordsSimInfo(vPatts);
950 Vec_PtrReallocSimInfo( vPatts );
951 Vec_PtrCleanSimInfo( vPatts, nWords, 2*nWords );
952 nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
953 }
954 if ( iPat % nPatsInit == 0 )
955 iPat++;
956 // save the pattern
957 Gia_ManIncrementTravId( pAig );
958 // Vec_IntClear( p->vCex );
959 Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
960 // Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
961 // Cec_ManSatAddToStore( p->vCexStore, p->vCex );
962 // if ( iPat == nPats )
963 // break;
964 // quit if one of them is solved
965 // if ( pPars->fFirstStop )
966 // break;
967 // if ( iPat == 32 * 15 * 16 - 1 )
968 // break;
969 }
970 p->timeTotal = Abc_Clock() - clk;
971 Bar_ProgressStop( pProgress );
972 if ( pPars->fVerbose )
973 Cec_ManSatPrintStats( p );
974 // Abc_Print( 1, "Total number of cex literals = %d. (Ave = %d)\n", p->nCexLits, p->nCexLits/p->nSatSat );
975 Cec_ManSatStop( p );
976 if ( pnPats )
977 *pnPats = iPat-1;
978 return vStatus;
979 }
980
981
982 /**Function*************************************************************
983
984 Synopsis [Save values in the cone of influence.]
985
986 Description []
987
988 SideEffects []
989
990 SeeAlso []
991
992 ***********************************************************************/
Cec_ManSatAddToStore(Vec_Int_t * vCexStore,Vec_Int_t * vCex,int Out)993 void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out )
994 {
995 int i, Entry;
996 Vec_IntPush( vCexStore, Out );
997 if ( vCex == NULL ) // timeout
998 {
999 Vec_IntPush( vCexStore, -1 );
1000 return;
1001 }
1002 // write the counter-example
1003 Vec_IntPush( vCexStore, Vec_IntSize(vCex) );
1004 Vec_IntForEachEntry( vCex, Entry, i )
1005 Vec_IntPush( vCexStore, Entry );
1006 }
1007
1008 /**Function*************************************************************
1009
1010 Synopsis [Save values in the cone of influence.]
1011
1012 Description []
1013
1014 SideEffects []
1015
1016 SeeAlso []
1017
1018 ***********************************************************************/
Cec_ManSatSolveMiter_rec(Cec_ManSat_t * pSat,Gia_Man_t * p,Gia_Obj_t * pObj)1019 void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
1020 {
1021 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
1022 return;
1023 Gia_ObjSetTravIdCurrent(p, pObj);
1024 if ( Gia_ObjIsCi(pObj) )
1025 {
1026 pSat->nCexLits++;
1027 Vec_IntPush( pSat->vCex, Abc_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
1028 return;
1029 }
1030 assert( Gia_ObjIsAnd(pObj) );
1031 Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin0(pObj) );
1032 Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin1(pObj) );
1033 }
1034
1035 /**Function*************************************************************
1036
1037 Synopsis [Save patterns.]
1038
1039 Description []
1040
1041 SideEffects []
1042
1043 SeeAlso []
1044
1045 ***********************************************************************/
Cec_ManSavePattern(Cec_ManSat_t * p,Gia_Obj_t * pObj1,Gia_Obj_t * pObj2)1046 void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 )
1047 {
1048 Vec_IntClear( p->vCex );
1049 Gia_ManIncrementTravId( p->pAig );
1050 Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj1) );
1051 if ( pObj2 )
1052 Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) );
1053 }
1054
1055 /**Function*************************************************************
1056
1057 Synopsis [Performs one round of solving for the POs of the AIG.]
1058
1059 Description [Labels the nodes that have been proved (pObj->fMark1)
1060 and returns the set of satisfying assignments.]
1061
1062 SideEffects []
1063
1064 SeeAlso []
1065
1066 ***********************************************************************/
Cec_ManSatSolveMiter(Gia_Man_t * pAig,Cec_ParSat_t * pPars,Vec_Str_t ** pvStatus)1067 Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus )
1068 {
1069 Bar_Progress_t * pProgress = NULL;
1070 Vec_Int_t * vCexStore;
1071 Vec_Str_t * vStatus;
1072 Cec_ManSat_t * p;
1073 Gia_Obj_t * pObj;
1074 int i, status;
1075 abctime clk = Abc_Clock();
1076 // prepare AIG
1077 Gia_ManSetPhase( pAig );
1078 Gia_ManLevelNum( pAig );
1079 Gia_ManIncrementTravId( pAig );
1080 // create resulting data-structures
1081 vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
1082 vCexStore = Vec_IntAlloc( 10000 );
1083 // perform solving
1084 p = Cec_ManSatCreate( pAig, pPars );
1085 pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
1086 Gia_ManForEachCo( pAig, pObj, i )
1087 {
1088 Vec_IntClear( p->vCex );
1089 Bar_ProgressUpdate( pProgress, i, "SAT..." );
1090 if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
1091 {
1092 if ( Gia_ObjFaninC0(pObj) )
1093 {
1094 // Abc_Print( 1, "Constant 1 output of SRM!!!\n" );
1095 Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example
1096 Vec_StrPush( vStatus, 0 );
1097 }
1098 else
1099 {
1100 // Abc_Print( 1, "Constant 0 output of SRM!!!\n" );
1101 Vec_StrPush( vStatus, 1 );
1102 }
1103 continue;
1104 }
1105 status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
1106 Vec_StrPush( vStatus, (char)status );
1107 if ( status == -1 )
1108 {
1109 Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
1110 continue;
1111 }
1112 if ( status == 1 )
1113 continue;
1114 assert( status == 0 );
1115 // save the pattern
1116 // Gia_ManIncrementTravId( pAig );
1117 // Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
1118 Cec_ManSavePattern( p, Gia_ObjFanin0(pObj), NULL );
1119 // Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
1120 Cec_ManSatAddToStore( vCexStore, p->vCex, i );
1121 }
1122 p->timeTotal = Abc_Clock() - clk;
1123 Bar_ProgressStop( pProgress );
1124 // if ( pPars->fVerbose )
1125 // Cec_ManSatPrintStats( p );
1126 Cec_ManSatStop( p );
1127 *pvStatus = vStatus;
1128 return vCexStore;
1129 }
1130
1131
1132 ////////////////////////////////////////////////////////////////////////
1133 /// END OF FILE ///
1134 ////////////////////////////////////////////////////////////////////////
1135
1136
1137 ABC_NAMESPACE_IMPL_END
1138
1139