abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cecSolve.c
Go to the documentation of this file.
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 
30 static inline int Cec_ObjSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj ) { return p->pSatVars[Gia_ObjId(p->pAig,pObj)]; }
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
676 void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
677 {
678  Bar_Progress_t * pProgress = NULL;
679  Cec_ManSat_t * p;
680  Gia_Obj_t * pObj;
681  int i, status;
682  abctime clk = Abc_Clock(), clk2;
683  // reset the manager
684  if ( pPat )
685  {
686  pPat->iStart = Vec_StrSize(pPat->vStorage);
687  pPat->nPats = 0;
688  pPat->nPatLits = 0;
689  pPat->nPatLitsMin = 0;
690  }
691  Gia_ManSetPhase( pAig );
692  Gia_ManLevelNum( pAig );
693  Gia_ManIncrementTravId( pAig );
694  p = Cec_ManSatCreate( pAig, pPars );
695  pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
696  Gia_ManForEachCo( pAig, pObj, i )
697  {
698  if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
699  {
700  pObj->fMark0 = 0;
701  pObj->fMark1 = 1;
702  continue;
703  }
704  Bar_ProgressUpdate( pProgress, i, "SAT..." );
705 clk2 = Abc_Clock();
706  status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
707  pObj->fMark0 = (status == 0);
708  pObj->fMark1 = (status == 1);
709 /*
710  if ( status == -1 )
711  {
712  Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
713  Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0 );
714  Gia_ManStop( pTemp );
715  Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
716  }
717 */
718  if ( status != 0 )
719  continue;
720  // save the pattern
721  if ( pPat )
722  {
723  abctime clk3 = Abc_Clock();
724  Cec_ManPatSavePattern( pPat, p, pObj );
725  pPat->timeTotalSave += Abc_Clock() - clk3;
726  }
727  // quit if one of them is solved
728  if ( pPars->fCheckMiter )
729  break;
730  }
731  p->timeTotal = Abc_Clock() - clk;
732  Bar_ProgressStop( pProgress );
733  if ( pPars->fVerbose )
734  Cec_ManSatPrintStats( p );
735  Cec_ManSatStop( p );
736 }
737 
738 /**Function*************************************************************
739 
740  Synopsis [Performs one round of solving for the POs of the AIG.]
741 
742  Description [Labels the nodes that have been proved (pObj->fMark1)
743  and returns the set of satisfying assignments.]
744 
745  SideEffects []
746 
747  SeeAlso []
748 
749 ***********************************************************************/
750 int Cec_ManSatSolveExractPattern( Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vPat )
751 {
752  int k, nSize;
753  Vec_IntClear( vPat );
754  // skip the output number
755  iStart++;
756  // get the number of items
757  nSize = Vec_IntEntry( vCexStore, iStart++ );
758  if ( nSize <= 0 )
759  return iStart;
760  // extract pattern
761  for ( k = 0; k < nSize; k++ )
762  Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
763  return iStart;
764 }
765 void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
766 {
767  Vec_Str_t * vStatus;
768  Vec_Int_t * vPat = Vec_IntAlloc( 1000 );
769  Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 );
770  Gia_Obj_t * pObj;
771  int i, status, iStart = 0;
772  assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) );
773  // reset the manager
774  if ( pPat )
775  {
776  pPat->iStart = Vec_StrSize(pPat->vStorage);
777  pPat->nPats = 0;
778  pPat->nPatLits = 0;
779  pPat->nPatLitsMin = 0;
780  }
781  Gia_ManForEachCo( pAig, pObj, i )
782  {
783  status = (int)Vec_StrEntry(vStatus, i);
784  pObj->fMark0 = (status == 0);
785  pObj->fMark1 = (status == 1);
786  if ( Vec_IntSize(vCexStore) > 0 && status != 1 )
787  iStart = Cec_ManSatSolveExractPattern( vCexStore, iStart, vPat );
788  if ( status != 0 )
789  continue;
790  // save the pattern
791  if ( pPat && Vec_IntSize(vPat) > 0 )
792  {
793  abctime clk3 = Abc_Clock();
794  Cec_ManPatSavePatternCSat( pPat, vPat );
795  pPat->timeTotalSave += Abc_Clock() - clk3;
796  }
797  // quit if one of them is solved
798  if ( pPars->fCheckMiter )
799  break;
800  }
801  assert( iStart == Vec_IntSize(vCexStore) );
802  Vec_IntFree( vPat );
803  Vec_StrFree( vStatus );
804  Vec_IntFree( vCexStore );
805 }
806 
807 
808 
809 /**Function*************************************************************
810 
811  Synopsis [Returns the pattern stored.]
812 
813  Description []
814 
815  SideEffects []
816 
817  SeeAlso []
818 
819 ***********************************************************************/
820 Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * pSat )
821 {
822  return pSat->vCex;
823 }
824 
825 /**Function*************************************************************
826 
827  Synopsis [Save values in the cone of influence.]
828 
829  Description []
830 
831  SideEffects []
832 
833  SeeAlso []
834 
835 ***********************************************************************/
836 void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vInfo, int iPat, int nRegs )
837 {
838  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
839  return;
840  Gia_ObjSetTravIdCurrent(p, pObj);
841  if ( Gia_ObjIsCi(pObj) )
842  {
843  unsigned * pInfo = (unsigned *)Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
844  if ( Cec_ObjSatVarValue( pSat, pObj ) != Abc_InfoHasBit( pInfo, iPat ) )
845  Abc_InfoXorBit( pInfo, iPat );
846  pSat->nCexLits++;
847 // Vec_IntPush( pSat->vCex, Abc_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
848  return;
849  }
850  assert( Gia_ObjIsAnd(pObj) );
851  Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin0(pObj), vInfo, iPat, nRegs );
852  Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin1(pObj), vInfo, iPat, nRegs );
853 }
854 
855 /**Function*************************************************************
856 
857  Synopsis [Performs one round of solving for the POs of the AIG.]
858 
859  Description [Labels the nodes that have been proved (pObj->fMark1)
860  and returns the set of satisfying assignments.]
861 
862  SideEffects []
863 
864  SeeAlso []
865 
866 ***********************************************************************/
867 Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats )
868 {
869  Bar_Progress_t * pProgress = NULL;
870  Vec_Str_t * vStatus;
871  Cec_ManSat_t * p;
872  Gia_Obj_t * pObj;
873  int iPat = 0, nPatsInit, nPats;
874  int i, status;
875  abctime clk = Abc_Clock();
876  nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
877  Gia_ManSetPhase( pAig );
878  Gia_ManLevelNum( pAig );
879  Gia_ManIncrementTravId( pAig );
880  p = Cec_ManSatCreate( pAig, pPars );
881  vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
882  pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
883  Gia_ManForEachCo( pAig, pObj, i )
884  {
885  Bar_ProgressUpdate( pProgress, i, "SAT..." );
886  if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
887  {
888  if ( Gia_ObjFaninC0(pObj) )
889  {
890 // Abc_Print( 1, "Constant 1 output of SRM!!!\n" );
891  Vec_StrPush( vStatus, 0 );
892  }
893  else
894  {
895 // Abc_Print( 1, "Constant 0 output of SRM!!!\n" );
896  Vec_StrPush( vStatus, 1 );
897  }
898  continue;
899  }
900  status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
901 //Abc_Print( 1, "output %d status = %d\n", i, status );
902  Vec_StrPush( vStatus, (char)status );
903  if ( status != 0 )
904  continue;
905  // resize storage
906  if ( iPat == nPats )
907  {
908  int nWords = Vec_PtrReadWordsSimInfo(vPatts);
909  Vec_PtrReallocSimInfo( vPatts );
910  Vec_PtrCleanSimInfo( vPatts, nWords, 2*nWords );
911  nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
912  }
913  if ( iPat % nPatsInit == 0 )
914  iPat++;
915  // save the pattern
916  Gia_ManIncrementTravId( pAig );
917 // Vec_IntClear( p->vCex );
918  Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
919 // Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
920 // Cec_ManSatAddToStore( p->vCexStore, p->vCex );
921 // if ( iPat == nPats )
922 // break;
923  // quit if one of them is solved
924 // if ( pPars->fFirstStop )
925 // break;
926 // if ( iPat == 32 * 15 * 16 - 1 )
927 // break;
928  }
929  p->timeTotal = Abc_Clock() - clk;
930  Bar_ProgressStop( pProgress );
931  if ( pPars->fVerbose )
932  Cec_ManSatPrintStats( p );
933 // Abc_Print( 1, "Total number of cex literals = %d. (Ave = %d)\n", p->nCexLits, p->nCexLits/p->nSatSat );
934  Cec_ManSatStop( p );
935  if ( pnPats )
936  *pnPats = iPat-1;
937  return vStatus;
938 }
939 
940 
941 /**Function*************************************************************
942 
943  Synopsis [Save values in the cone of influence.]
944 
945  Description []
946 
947  SideEffects []
948 
949  SeeAlso []
950 
951 ***********************************************************************/
952 void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out )
953 {
954  int i, Entry;
955  Vec_IntPush( vCexStore, Out );
956  if ( vCex == NULL ) // timeout
957  {
958  Vec_IntPush( vCexStore, -1 );
959  return;
960  }
961  // write the counter-example
962  Vec_IntPush( vCexStore, Vec_IntSize(vCex) );
963  Vec_IntForEachEntry( vCex, Entry, i )
964  Vec_IntPush( vCexStore, Entry );
965 }
966 
967 /**Function*************************************************************
968 
969  Synopsis [Save values in the cone of influence.]
970 
971  Description []
972 
973  SideEffects []
974 
975  SeeAlso []
976 
977 ***********************************************************************/
978 void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
979 {
980  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
981  return;
982  Gia_ObjSetTravIdCurrent(p, pObj);
983  if ( Gia_ObjIsCi(pObj) )
984  {
985  pSat->nCexLits++;
986  Vec_IntPush( pSat->vCex, Abc_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
987  return;
988  }
989  assert( Gia_ObjIsAnd(pObj) );
990  Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin0(pObj) );
991  Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin1(pObj) );
992 }
993 
994 /**Function*************************************************************
995 
996  Synopsis [Save patterns.]
997 
998  Description []
999 
1000  SideEffects []
1001 
1002  SeeAlso []
1003 
1004 ***********************************************************************/
1005 void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 )
1006 {
1007  Vec_IntClear( p->vCex );
1008  Gia_ManIncrementTravId( p->pAig );
1009  Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj1) );
1010  if ( pObj2 )
1011  Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) );
1012 }
1013 
1014 /**Function*************************************************************
1015 
1016  Synopsis [Performs one round of solving for the POs of the AIG.]
1017 
1018  Description [Labels the nodes that have been proved (pObj->fMark1)
1019  and returns the set of satisfying assignments.]
1020 
1021  SideEffects []
1022 
1023  SeeAlso []
1024 
1025 ***********************************************************************/
1026 Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus )
1027 {
1028  Bar_Progress_t * pProgress = NULL;
1029  Vec_Int_t * vCexStore;
1030  Vec_Str_t * vStatus;
1031  Cec_ManSat_t * p;
1032  Gia_Obj_t * pObj;
1033  int i, status;
1034  abctime clk = Abc_Clock();
1035  // prepare AIG
1036  Gia_ManSetPhase( pAig );
1037  Gia_ManLevelNum( pAig );
1038  Gia_ManIncrementTravId( pAig );
1039  // create resulting data-structures
1040  vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
1041  vCexStore = Vec_IntAlloc( 10000 );
1042  // perform solving
1043  p = Cec_ManSatCreate( pAig, pPars );
1044  pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
1045  Gia_ManForEachCo( pAig, pObj, i )
1046  {
1047  Vec_IntClear( p->vCex );
1048  Bar_ProgressUpdate( pProgress, i, "SAT..." );
1049  if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
1050  {
1051  if ( Gia_ObjFaninC0(pObj) )
1052  {
1053 // Abc_Print( 1, "Constant 1 output of SRM!!!\n" );
1054  Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example
1055  Vec_StrPush( vStatus, 0 );
1056  }
1057  else
1058  {
1059 // Abc_Print( 1, "Constant 0 output of SRM!!!\n" );
1060  Vec_StrPush( vStatus, 1 );
1061  }
1062  continue;
1063  }
1064  status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
1065  Vec_StrPush( vStatus, (char)status );
1066  if ( status == -1 )
1067  {
1068  Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
1069  continue;
1070  }
1071  if ( status == 1 )
1072  continue;
1073  assert( status == 0 );
1074  // save the pattern
1075 // Gia_ManIncrementTravId( pAig );
1076 // Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
1077  Cec_ManSavePattern( p, Gia_ObjFanin0(pObj), NULL );
1078 // Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
1079  Cec_ManSatAddToStore( vCexStore, p->vCex, i );
1080  }
1081  p->timeTotal = Abc_Clock() - clk;
1082  Bar_ProgressStop( pProgress );
1083 // if ( pPars->fVerbose )
1084 // Cec_ManSatPrintStats( p );
1085  Cec_ManSatStop( p );
1086  *pvStatus = vStatus;
1087  return vCexStore;
1088 }
1089 
1090 
1091 ////////////////////////////////////////////////////////////////////////
1092 /// END OF FILE ///
1093 ////////////////////////////////////////////////////////////////////////
1094 
1095 
1096 ABC_NAMESPACE_IMPL_END
1097 
Cec_ManSat_t_::timeSatSat
int timeSatSat
Definition: cecInt.h:105
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Cec_ManSatSolveMiter
Vec_Int_t * Cec_ManSatSolveMiter(Gia_Man_t *pAig, Cec_ParSat_t *pPars, Vec_Str_t **pvStatus)
Definition: cecSolve.c:1026
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Cec_ManSat_t_::timeTotal
int timeTotal
Definition: cecInt.h:107
Cec_ManSatSolveSeq_rec
void Cec_ManSatSolveSeq_rec(Cec_ManSat_t *pSat, Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Ptr_t *vInfo, int iPat, int nRegs)
Definition: cecSolve.c:836
sat_solver_t::act_vars
veci act_vars
Definition: satSolver.h:167
Cec_ManPatSavePatternCSat
void Cec_ManPatSavePatternCSat(Cec_ManPat_t *pMan, Vec_Int_t *vPat)
Definition: cecPat.c:402
Cec_ObjSatNum
static ABC_NAMESPACE_IMPL_START int Cec_ObjSatNum(Cec_ManSat_t *p, Gia_Obj_t *pObj)
DECLARATIONS ///.
Definition: cecSolve.c:30
sat_solver_t::cap
int cap
Definition: satSolver.h:94
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Cec_ManSatPrintStats
void Cec_ManSatPrintStats(Cec_ManSat_t *p)
Definition: cecMan.c:74
Cec_ManSat_t_::nConfUndec
int nConfUndec
Definition: cecInt.h:102
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Gia_Regular
static Gia_Obj_t * Gia_Regular(Gia_Obj_t *p)
Definition: gia.h:377
Gia_ObjIsTravIdCurrent
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Cec_ManSat_t_::pSat
sat_solver * pSat
Definition: cecInt.h:83
Cec_ManSat_t_::nConfUnsat
int nConfUnsat
Definition: cecInt.h:100
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Cec_ManSatReadCex
Vec_Int_t * Cec_ManSatReadCex(Cec_ManSat_t *pSat)
Definition: cecSolve.c:820
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
veci_push
static void veci_push(veci *v, int e)
Definition: satVec.h:53
Cec_CollectSuper
void Cec_CollectSuper(Gia_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
Definition: cecSolve.c:262
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Cec_ManSat_t_::pPars
Cec_ParSat_t * pPars
Definition: cecInt.h:78
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Cec_ManSat_t_::nSatUnsat
int nSatUnsat
Definition: cecInt.h:94
Vec_PtrCleanSimInfo
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
Cec_ManSat_t_::pAig
Gia_Man_t * pAig
Definition: cecInt.h:80
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
l_True
#define l_True
Definition: SolverTypes.h:84
Cec_ManSat_t_::pSatVars
int * pSatVars
Definition: cecInt.h:85
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Gia_Obj_t_::fMark1
unsigned fMark1
Definition: gia.h:84
Vec_StrAlloc
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
veci_resize
static void veci_resize(veci *v, int k)
Definition: satVec.h:47
sat_solver_t::qhead
int qhead
Definition: satSolver.h:95
Cec_ManSavePattern
void Cec_ManSavePattern(Cec_ManSat_t *p, Gia_Obj_t *pObj1, Gia_Obj_t *pObj2)
Definition: cecSolve.c:1005
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_StrPush
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
sat_solver_t::stats
stats_t stats
Definition: satSolver.h:156
Cec_CollectSuper_rec
void Cec_CollectSuper_rec(Gia_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition: cecSolve.c:236
Cec_ManSat_t_::nSatVars
int nSatVars
Definition: cecInt.h:84
nWords
int nWords
Definition: abcNpn.c:127
Cec_ObjSetSatNum
static void Cec_ObjSetSatNum(Cec_ManSat_t *p, Gia_Obj_t *pObj, int Num)
Definition: cecSolve.c:31
Gia_Obj_t_
Definition: gia.h:75
Gia_ManConst1
static Gia_Obj_t * Gia_ManConst1(Gia_Man_t *p)
Definition: gia.h:401
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Cec_ManSatSolve
void Cec_ManSatSolve(Cec_ManPat_t *pPat, Gia_Man_t *pAig, Cec_ParSat_t *pPars)
Definition: cecSolve.c:676
Cec_ManSatSolverRecycle
void Cec_ManSatSolverRecycle(Cec_ManSat_t *p)
Definition: cecSolve.c:365
Cec_ManSat_t_::nRecycles
int nRecycles
Definition: cecInt.h:87
Cbs_ManSolveMiterNc
Vec_Int_t * Cbs_ManSolveMiterNc(Gia_Man_t *pGia, int nConfs, Vec_Str_t **pvStatus, int fVerbose)
Definition: giaCSat.c:998
Cec_ManSatSolveExractPattern
int Cec_ManSatSolveExractPattern(Vec_Int_t *vCexStore, int iStart, Vec_Int_t *vPat)
Definition: cecSolve.c:750
Gia_ObjChild1
static Gia_Obj_t * Gia_ObjChild1(Gia_Obj_t *pObj)
Definition: gia.h:458
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
sat_solver_t::factors
double * factors
Definition: satSolver.h:168
Gia_Not
static Gia_Obj_t * Gia_Not(Gia_Obj_t *p)
Definition: gia.h:378
Gia_ObjLevel
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
Cec_ManSat_t_::nSatUndec
int nSatUndec
Definition: cecInt.h:96
Vec_StrEntry
static char Vec_StrEntry(Vec_Str_t *p, int i)
Definition: vecStr.h:336
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Bar_ProgressUpdate
static void Bar_ProgressUpdate(Bar_Progress_t *p, int nItemsCur, char *pString)
Definition: bar.h:63
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Cec_ManSat_t_::vFanins
Vec_Ptr_t * vFanins
Definition: cecInt.h:89
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Cec_ManSatCheckNodeTwo
int Cec_ManSatCheckNodeTwo(Cec_ManSat_t *p, Gia_Obj_t *pObj1, Gia_Obj_t *pObj2)
Definition: cecSolve.c:569
Cec_ManPatSavePattern
void Cec_ManPatSavePattern(Cec_ManPat_t *pPat, Cec_ManSat_t *p, Gia_Obj_t *pObj)
Definition: cecPat.c:359
Cec_ManSat_t_::vCex
Vec_Int_t * vCex
Definition: cecInt.h:91
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_ObjSetTravIdCurrent
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
Cec_ObjAddToFrontier
void Cec_ObjAddToFrontier(Cec_ManSat_t *p, Gia_Obj_t *pObj, Vec_Ptr_t *vFrontier)
Definition: cecSolve.c:281
Cec_ManPat_t
typedefABC_NAMESPACE_HEADER_START struct Cec_ManPat_t_ Cec_ManPat_t
INCLUDES ///.
Definition: cecInt.h:48
Cec_ManSatSolveCSat
void Cec_ManSatSolveCSat(Cec_ManPat_t *pPat, Gia_Man_t *pAig, Cec_ParSat_t *pPars)
Definition: cecSolve.c:765
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Cec_SetActivityFactors_rec
void Cec_SetActivityFactors_rec(Cec_ManSat_t *p, Gia_Obj_t *pObj, int LevelMin, int LevelMax)
Definition: cecSolve.c:406
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Cec_ManSatCheckNode
int Cec_ManSatCheckNode(Cec_ManSat_t *p, Gia_Obj_t *pObj)
Definition: cecSolve.c:470
Cec_ManSat_t_::vUsedNodes
Vec_Ptr_t * vUsedNodes
Definition: cecInt.h:86
Bar_Progress_t_
DECLARATIONS ///.
Definition: bar.c:36
Cec_ManSat_t_::timeSatUnsat
int timeSatUnsat
Definition: cecInt.h:104
Cec_ManSat_t_::nSatTotal
int nSatTotal
Definition: cecInt.h:97
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cec_AddClausesSuper
void Cec_AddClausesSuper(Cec_ManSat_t *p, Gia_Obj_t *pNode, Vec_Ptr_t *vSuper)
Definition: cecSolve.c:183
Cec_ManSatAddToStore
void Cec_ManSatAddToStore(Vec_Int_t *vCexStore, Vec_Int_t *vCex, int Out)
Definition: cecSolve.c:952
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Cec_ManSat_t_::nConfSat
int nConfSat
Definition: cecInt.h:101
Cec_ManSatStop
void Cec_ManSatStop(Cec_ManSat_t *p)
Definition: cecMan.c:104
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Cec_ManSat_t_
Definition: cecInt.h:75
Cec_ManSat_t_::nCallsSince
int nCallsSince
Definition: cecInt.h:88
stats_t::conflicts
ABC_INT64_T conflicts
Definition: satVec.h:154
Cec_ManSat_t_::timeSatUndec
int timeSatUndec
Definition: cecInt.h:106
Vec_PtrReadWordsSimInfo
static int Vec_PtrReadWordsSimInfo(Vec_Ptr_t *p)
Definition: vecPtr.h:952
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
Gia_Obj_t_::fPhase
unsigned fPhase
Definition: gia.h:85
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Cec_CnfNodeAddToSolver
void Cec_CnfNodeAddToSolver(Cec_ManSat_t *p, Gia_Obj_t *pObj)
Definition: cecSolve.c:306
sat_solver_t::qtail
int qtail
Definition: satSolver.h:96
Cec_ManSat_t_::nSatSat
int nSatSat
Definition: cecInt.h:95
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Vec_Str_t_
Definition: bblif.c:47
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_ObjRecognizeMux
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition: giaUtil.c:959
Gia_Man_t_
Definition: gia.h:95
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
l_False
#define l_False
Definition: SolverTypes.h:85
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Vec_PtrReallocSimInfo
static void Vec_PtrReallocSimInfo(Vec_Ptr_t *vInfo)
Definition: vecPtr.h:1035
Cec_ParSat_t
typedefABC_NAMESPACE_HEADER_START struct Cec_ParSat_t_ Cec_ParSat_t
INCLUDES ///.
Definition: cec.h:43
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition: giaUtil.c:505
Cec_AddClausesMux
void Cec_AddClausesMux(Cec_ManSat_t *p, Gia_Obj_t *pNode)
Definition: cecSolve.c:64
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Cec_ObjSatVarValue
int Cec_ObjSatVarValue(Cec_ManSat_t *p, Gia_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition: cecSolve.c:48
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Bar_ProgressStop
void Bar_ProgressStop(Bar_Progress_t *p)
Definition: bar.c:126
Cec_ManSat_t_::nCexLits
int nCexLits
Definition: cecInt.h:98
Cec_SetActivityFactors
int Cec_SetActivityFactors(Cec_ManSat_t *p, Gia_Obj_t *pObj)
Definition: cecSolve.c:440
Cec_ManSatCreate
Cec_ManSat_t * Cec_ManSatCreate(Gia_Man_t *pAig, Cec_ParSat_t *pPars)
DECLARATIONS ///.
Definition: cecMan.c:45
Bar_ProgressStart
Bar_Progress_t * Bar_ProgressStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition: bar.c:66
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Cec_ManSatSolveMiter_rec
void Cec_ManSatSolveMiter_rec(Cec_ManSat_t *pSat, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: cecSolve.c:978
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Cec_ManSatSolveSeq
Vec_Str_t * Cec_ManSatSolveSeq(Vec_Ptr_t *vPatts, Gia_Man_t *pAig, Cec_ParSat_t *pPars, int nRegs, int *pnPats)
Definition: cecSolve.c:867