abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigRefSat.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigRefSat.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [SAT based refinement of a counter-example.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigRefSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satSolver.h"
24 
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 // local manager
35 {
36  // user data
37  Aig_Man_t * pAig; // user's AIG
38  Abc_Cex_t * pCex; // user's CEX
39  int nInputs; // the number of first inputs to skip
40  int fVerbose; // verbose flag
41  // unrolling
42  Aig_Man_t * pFrames; // unrolled timeframes
43  Vec_Int_t * vMapPiF2A; // mapping of frame PIs into real PIs
44 };
45 
46 // performs ternary simulation
47 extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes );
48 
49 ////////////////////////////////////////////////////////////////////////
50 /// FUNCTION DEFINITIONS ///
51 ////////////////////////////////////////////////////////////////////////
52 
53 /**Function*************************************************************
54 
55  Synopsis [Maps array of frame PI IDs into array of original PI IDs.]
56 
57  Description []
58 
59  SideEffects []
60 
61  SeeAlso []
62 
63 ***********************************************************************/
65 {
66  Vec_Int_t * vOriginal, * vVisited;
67  int i, Entry;
68  vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) );
69  vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
70  Vec_IntForEachEntry( vReasons, Entry, i )
71  {
72  int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
73  assert( iInput >= 0 && iInput < Aig_ManCiNum(p->pAig) );
74  if ( Vec_IntEntry(vVisited, iInput) == 0 )
75  Vec_IntPush( vOriginal, iInput );
76  Vec_IntAddToEntry( vVisited, iInput, 1 );
77  }
78  Vec_IntFree( vVisited );
79  return vOriginal;
80 }
81 
82 /**Function*************************************************************
83 
84  Synopsis [Creates the counter-example.]
85 
86  Description []
87 
88  SideEffects []
89 
90  SeeAlso []
91 
92 ***********************************************************************/
94 {
95  Abc_Cex_t * pCare;
96  int i, Entry, iInput, iFrame;
97  pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
98  memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
99  Vec_IntForEachEntry( vReasons, Entry, i )
100  {
101  assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pFrames) );
102  iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
103  iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 );
104  Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
105  }
106  return pCare;
107 }
108 
109 /**Function*************************************************************
110 
111  Synopsis [Returns reasons for the property to fail.]
112 
113  Description []
114 
115  SideEffects []
116 
117  SeeAlso []
118 
119 ***********************************************************************/
120 void Saig_RefManFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasons )
121 {
122  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
123  return;
124  Aig_ObjSetTravIdCurrent(p, pObj);
125  if ( Aig_ObjIsCi(pObj) )
126  {
127  Vec_IntPush( vReasons, Aig_ObjCioId(pObj) );
128  return;
129  }
130  assert( Aig_ObjIsNode(pObj) );
131  if ( pObj->fPhase )
132  {
133  Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
134  Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
135  }
136  else
137  {
138  int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
139  int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
140  assert( !fPhase0 || !fPhase1 );
141  if ( !fPhase0 && fPhase1 )
142  Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
143  else if ( fPhase0 && !fPhase1 )
144  Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
145  else
146  {
147  int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
148  int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
149  if ( iPrio0 <= iPrio1 )
150  Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
151  else
152  Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
153  }
154  }
155 }
156 
157 /**Function*************************************************************
158 
159  Synopsis [Returns reasons for the property to fail.]
160 
161  Description []
162 
163  SideEffects []
164 
165  SeeAlso []
166 
167 ***********************************************************************/
169 {
170  Aig_Obj_t * pObj;
171  Vec_Int_t * vPrios, * vPi2Prio, * vReasons;
172  int i, CountPrios;
173 
174  vPi2Prio = Vec_IntStartFull( Saig_ManPiNum(p->pAig) );
175  vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) );
176 
177  // set PI values according to CEX
178  CountPrios = 0;
179  Aig_ManConst1(p->pFrames)->fPhase = 1;
180  Aig_ManForEachCi( p->pFrames, pObj, i )
181  {
182  int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
183  int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
184  pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
185  // assign priority
186  if ( Vec_IntEntry(vPi2Prio, iInput) == ~0 )
187  Vec_IntWriteEntry( vPi2Prio, iInput, CountPrios++ );
188 // Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry(vPi2Prio, iInput) );
189  Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i );
190  }
191 // printf( "Priority numbers = %d.\n", CountPrios );
192  Vec_IntFree( vPi2Prio );
193 
194  // traverse and set the priority
195  Aig_ManForEachNode( p->pFrames, pObj, i )
196  {
197  int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
198  int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
199  int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
200  int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
201  pObj->fPhase = fPhase0 && fPhase1;
202  if ( fPhase0 && fPhase1 ) // both are one
203  Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) );
204  else if ( !fPhase0 && fPhase1 )
205  Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 );
206  else if ( fPhase0 && !fPhase1 )
207  Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 );
208  else // both are zero
209  Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) );
210  }
211  // check the property output
212  pObj = Aig_ManCo( p->pFrames, 0 );
213  assert( (int)Aig_ObjFanin0(pObj)->fPhase == Aig_ObjFaninC0(pObj) );
214 
215  // select the reason
216  vReasons = Vec_IntAlloc( 100 );
217  Aig_ManIncrementTravId( p->pFrames );
218  if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
219  Saig_RefManFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
220  Vec_IntFree( vPrios );
221  return vReasons;
222 }
223 
224 
225 /**Function*************************************************************
226 
227  Synopsis [Collect nodes in the unrolled timeframes.]
228 
229  Description []
230 
231  SideEffects []
232 
233  SeeAlso []
234 
235 ***********************************************************************/
236 void Saig_ManUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots )
237 {
238  if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
239  return;
240  Aig_ObjSetTravIdCurrent(pAig, pObj);
241  if ( Aig_ObjIsCo(pObj) )
242  Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
243  else if ( Aig_ObjIsNode(pObj) )
244  {
245  Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
246  Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots );
247  }
248  if ( vRoots && Saig_ObjIsLo( pAig, pObj ) )
249  Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
250  Vec_IntPush( vObjs, Aig_ObjId(pObj) );
251 }
252 
253 /**Function*************************************************************
254 
255  Synopsis [Derive unrolled timeframes.]
256 
257  Description []
258 
259  SideEffects []
260 
261  SeeAlso []
262 
263 ***********************************************************************/
264 Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A )
265 {
266  Aig_Man_t * pFrames; // unrolled timeframes
267  Vec_Vec_t * vFrameCos; // the list of COs per frame
268  Vec_Vec_t * vFrameObjs; // the list of objects per frame
269  Vec_Int_t * vRoots, * vObjs;
270  Aig_Obj_t * pObj;
271  int i, f;
272  // sanity checks
273  assert( Saig_ManPiNum(pAig) == pCex->nPis );
274  assert( Saig_ManRegNum(pAig) == pCex->nRegs );
275  assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
276 
277  // map PIs of the unrolled frames into PIs of the original design
278  *pvMapPiF2A = Vec_IntAlloc( 1000 );
279 
280  // collect COs and Objs visited in each frame
281  vFrameCos = Vec_VecStart( pCex->iFrame+1 );
282  vFrameObjs = Vec_VecStart( pCex->iFrame+1 );
283  // initialized the topmost frame
284  pObj = Aig_ManCo( pAig, pCex->iPo );
285  Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) );
286  for ( f = pCex->iFrame; f >= 0; f-- )
287  {
288  // collect nodes starting from the roots
289  Aig_ManIncrementTravId( pAig );
290  vRoots = Vec_VecEntryInt( vFrameCos, f );
291  Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
292  Saig_ManUnrollCollect_rec( pAig, pObj,
293  Vec_VecEntryInt(vFrameObjs, f),
294  (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
295  }
296 
297  // derive unrolled timeframes
298  pFrames = Aig_ManStart( 10000 );
299  pFrames->pName = Abc_UtilStrsav( pAig->pName );
300  pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
301  // initialize the flops
302  Saig_ManForEachLo( pAig, pObj, i )
303  pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) );
304  // iterate through the frames
305  for ( f = 0; f <= pCex->iFrame; f++ )
306  {
307  // construct
308  vObjs = Vec_VecEntryInt( vFrameObjs, f );
309  Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
310  {
311  if ( Aig_ObjIsNode(pObj) )
312  pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
313  else if ( Aig_ObjIsCo(pObj) )
314  pObj->pData = Aig_ObjChild0Copy(pObj);
315  else if ( Aig_ObjIsConst1(pObj) )
316  pObj->pData = Aig_ManConst1(pFrames);
317  else if ( Saig_ObjIsPi(pAig, pObj) )
318  {
319  if ( Aig_ObjCioId(pObj) < nInputs )
320  {
321  int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj);
322  pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) );
323  }
324  else
325  {
326  pObj->pData = Aig_ObjCreateCi( pFrames );
327  Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) );
328  Vec_IntPush( *pvMapPiF2A, f );
329  }
330  }
331  }
332  if ( f == pCex->iFrame )
333  break;
334  // transfer
335  vRoots = Vec_VecEntryInt( vFrameCos, f );
336  Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
337  Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
338  }
339  // create output
340  pObj = Aig_ManCo( pAig, pCex->iPo );
341  Aig_ObjCreateCo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) );
342  Aig_ManSetRegNum( pFrames, 0 );
343  // cleanup
344  Vec_VecFree( vFrameCos );
345  Vec_VecFree( vFrameObjs );
346  // finallize
347  Aig_ManCleanup( pFrames );
348  // return
349  return pFrames;
350 }
351 
352 /**Function*************************************************************
353 
354  Synopsis [Creates refinement manager.]
355 
356  Description []
357 
358  SideEffects []
359 
360  SeeAlso []
361 
362 ***********************************************************************/
363 Saig_RefMan_t * Saig_RefManStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
364 {
365  Saig_RefMan_t * p;
366  p = ABC_CALLOC( Saig_RefMan_t, 1 );
367  p->pAig = pAig;
368  p->pCex = pCex;
369  p->nInputs = nInputs;
370  p->fVerbose = fVerbose;
371  p->pFrames = Saig_ManUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A );
372  return p;
373 }
374 
375 /**Function*************************************************************
376 
377  Synopsis [Destroys refinement manager.]
378 
379  Description []
380 
381  SideEffects []
382 
383  SeeAlso []
384 
385 ***********************************************************************/
387 {
388  Aig_ManStopP( &p->pFrames );
389  Vec_IntFreeP( &p->vMapPiF2A );
390  ABC_FREE( p );
391 }
392 
393 /**Function*************************************************************
394 
395  Synopsis [Sets phase bits in the timeframe AIG.]
396 
397  Description []
398 
399  SideEffects []
400 
401  SeeAlso []
402 
403 ***********************************************************************/
404 int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 )
405 {
406  Aig_Obj_t * pObj;
407  int i, iFrame, iInput;
408  Aig_ManConst1( p->pFrames )->fPhase = 1;
409  Aig_ManForEachCi( p->pFrames, pObj, i )
410  {
411  iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
412  iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
413  pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
414  // update value if it is a don't-care
415  if ( pCare && !Abc_InfoHasBit( pCare->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ) )
416  pObj->fPhase = fValue1;
417  }
418  Aig_ManForEachNode( p->pFrames, pObj, i )
419  pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) )
420  & ( Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj) );
421  Aig_ManForEachCo( p->pFrames, pObj, i )
422  pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) );
423  pObj = Aig_ManCo( p->pFrames, 0 );
424  return pObj->fPhase;
425 }
426 
427 /**Function*************************************************************
428 
429  Synopsis [Tries to remove literals from abstraction.]
430 
431  Description [The literals are sorted more desirable first.]
432 
433  SideEffects []
434 
435  SeeAlso []
436 
437 ***********************************************************************/
439 {
440  Vec_Vec_t * vLits;
441  Vec_Int_t * vVar2New;
442  int i, Entry, iInput, iFrame;
443  // collect literals
444  vLits = Vec_VecAlloc( 100 );
445  vVar2New = Vec_IntStartFull( Saig_ManPiNum(p->pAig) );
446  Vec_IntForEachEntry( vAssumps, Entry, i )
447  {
448  int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
449  assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) );
450  iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
451  iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
452 // Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
453  if ( Vec_IntEntry( vVar2New, iInput ) == ~0 )
454  Vec_IntWriteEntry( vVar2New, iInput, Vec_VecSize(vLits) );
455  Vec_VecPushInt( vLits, Vec_IntEntry( vVar2New, iInput ), Entry );
456  }
457  Vec_IntFree( vVar2New );
458  return vLits;
459 }
460 
461 
462 /**Function*************************************************************
463 
464  Synopsis [Generate the care set using SAT solver.]
465 
466  Description []
467 
468  SideEffects []
469 
470  SeeAlso []
471 
472 ***********************************************************************/
474 {
475  Abc_Cex_t * pCare;
476  int i, Entry, iInput, iFrame;
477  // create counter-example
478  pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
479  memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
480  Vec_IntForEachEntry( vAssumps, Entry, i )
481  {
482  int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
483  assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) );
484  iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
485  iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
486  Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
487  }
488  return pCare;
489 }
490 
491 /**Function*************************************************************
492 
493  Synopsis [Generate the care set using SAT solver.]
494 
495  Description []
496 
497  SideEffects []
498 
499  SeeAlso []
500 
501 ***********************************************************************/
503 {
504  int nConfLimit = 1000000;
505  Abc_Cex_t * pCare;
506  Cnf_Dat_t * pCnf;
507  sat_solver * pSat;
508  Aig_Obj_t * pObj;
509  Vec_Vec_t * vLits = NULL;
510  Vec_Int_t * vAssumps, * vVar2PiId;
511  int i, k, Entry, RetValue;//, f = 0, Counter = 0;
512  int nCoreLits, * pCoreLits;
513  clock_t clk = clock();
514  // create CNF
515  assert( Aig_ManRegNum(p->pFrames) == 0 );
516 // pCnf = Cnf_Derive( p->pFrames, 0 ); // too slow
517  pCnf = Cnf_DeriveSimple( p->pFrames, 0 );
518  RetValue = Saig_RefManSetPhases( p, NULL, 0 );
519  if ( RetValue )
520  {
521  printf( "Constructed frames are incorrect.\n" );
522  Cnf_DataFree( pCnf );
523  return NULL;
524  }
525  Cnf_DataTranformPolarity( pCnf, 0 );
526  // create SAT solver
527  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
528  if ( pSat == NULL )
529  {
530  Cnf_DataFree( pCnf );
531  return NULL;
532  }
533 //Abc_PrintTime( 1, "Preparing", clock() - clk );
534  // look for a true counter-example
535  if ( p->nInputs > 0 )
536  {
537  RetValue = sat_solver_solve( pSat, NULL, NULL,
538  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
539  if ( RetValue == l_False )
540  {
541  printf( "The problem is trivially UNSAT. The CEX is real.\n" );
542  // create counter-example
543  pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
544  memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
545  return pCare;
546  }
547  // the problem is SAT - it is expected
548  }
549  // create assumptions
550  vVar2PiId = Vec_IntStartFull( pCnf->nVars );
551  vAssumps = Vec_IntAlloc( Aig_ManCiNum(p->pFrames) );
552  Aig_ManForEachCi( p->pFrames, pObj, i )
553  {
554 // RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
555 // Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) );
556  Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) );
557  Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i );
558  }
559 
560  // reverse the order of assumptions
561 // if ( fNewOrder )
562 // Vec_IntReverseOrder( vAssumps );
563 
564  if ( fNewOrder )
565  {
566  // create literals
567  vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
568  // sort literals
569  Vec_VecSort( vLits, 1 );
570  // save literals
571  Vec_IntClear( vAssumps );
572  Vec_VecForEachEntryInt( vLits, Entry, i, k )
573  Vec_IntPush( vAssumps, Entry );
574 
575  for ( i = 0; i < Vec_VecSize(vLits); i++ )
576  printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
577  printf( "\n" );
578 
579  if ( p->fVerbose )
580  printf( "Total PIs = %d. Essential PIs = %d.\n",
581  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) );
582  }
583 
584  // solve
585 clk = clock();
586  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
587  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
588 //Abc_PrintTime( 1, "Solving", clock() - clk );
589  if ( RetValue != l_False )
590  {
591  if ( RetValue == l_True )
592  printf( "Internal Error!!! The resulting problem is SAT.\n" );
593  else
594  printf( "Internal Error!!! SAT solver timed out.\n" );
595  Cnf_DataFree( pCnf );
596  sat_solver_delete( pSat );
597  Vec_IntFree( vAssumps );
598  Vec_IntFree( vVar2PiId );
599  return NULL;
600  }
601  assert( RetValue == l_False ); // UNSAT
602 
603  // get relevant SAT literals
604  nCoreLits = sat_solver_final( pSat, &pCoreLits );
605  assert( nCoreLits > 0 );
606  if ( p->fVerbose )
607  printf( "AnalizeFinal selected %d assumptions (out of %d). Conflicts = %d.\n",
608  nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
609 
610  // save literals
611  Vec_IntClear( vAssumps );
612  for ( i = 0; i < nCoreLits; i++ )
613  Vec_IntPush( vAssumps, pCoreLits[i] );
614 
615 
616  // create literals
617  vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
618  // sort literals
619 // Vec_VecSort( vLits, 0 );
620  // save literals
621  Vec_IntClear( vAssumps );
622  Vec_VecForEachEntryInt( vLits, Entry, i, k )
623  Vec_IntPush( vAssumps, Entry );
624 
625 // for ( i = 0; i < Vec_VecSize(vLits); i++ )
626 // printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
627 // printf( "\n" );
628 
629  if ( p->fVerbose )
630  printf( "Total PIs = %d. Essential PIs = %d.\n",
631  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) );
632 /*
633  // try assumptions in different order
634  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
635  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
636  printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
637  Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
638 
639  // create different sets of assumptions
640  Counter = Vec_VecSize(vLits);
641  for ( f = 0; f < Vec_VecSize(vLits); f++ )
642  {
643  Vec_IntClear( vAssumps );
644  Vec_VecForEachEntryInt( vLits, Entry, i, k )
645  if ( i != f )
646  Vec_IntPush( vAssumps, Entry );
647 
648  // try the new assumptions
649  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
650  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
651  printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
652  Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts );
653  if ( RetValue != l_False )
654  continue;
655 
656  // UNSAT - remove literals
657  Vec_IntClear( Vec_VecEntryInt(vLits, f) );
658  Counter--;
659  }
660 
661  for ( i = 0; i < Vec_VecSize(vLits); i++ )
662  printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
663  printf( "\n" );
664 
665  if ( p->fVerbose )
666  printf( "Total PIs = %d. Essential PIs = %d.\n",
667  Saig_ManPiNum(p->pAig) - p->nInputs, Counter );
668 
669  // save literals
670  Vec_IntClear( vAssumps );
671  Vec_VecForEachEntryInt( vLits, Entry, i, k )
672  Vec_IntPush( vAssumps, Entry );
673 */
674  // create counter-example
675  pCare = Saig_RefManCreateCex( p, vVar2PiId, vAssumps );
676 
677  // cleanup
678  Cnf_DataFree( pCnf );
679  sat_solver_delete( pSat );
680  Vec_IntFree( vAssumps );
681  Vec_IntFree( vVar2PiId );
682  Vec_VecFreeP( &vLits );
683 
684  // verify counter-example
685  RetValue = Saig_RefManSetPhases( p, pCare, 0 );
686  if ( RetValue )
687  printf( "Reduced CEX verification has failed.\n" );
688  RetValue = Saig_RefManSetPhases( p, pCare, 1 );
689  if ( RetValue )
690  printf( "Reduced CEX verification has failed.\n" );
691  return pCare;
692 }
693 
694 
695 /**Function*************************************************************
696 
697  Synopsis []
698 
699  Description []
700 
701  SideEffects []
702 
703  SeeAlso []
704 
705 ***********************************************************************/
707 {
708  int nConfLimit = 1000000;
709  Cnf_Dat_t * pCnf;
710  sat_solver * pSat;
711  Aig_Obj_t * pObj;
712  Vec_Vec_t * vLits;
713  Vec_Int_t * vReasons, * vAssumps, * vVisited, * vVar2PiId;
714  int i, k, f, Entry, RetValue, Counter;
715 
716  // create CNF and SAT solver
717  pCnf = Cnf_DeriveSimple( p->pFrames, 0 );
718  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
719  if ( pSat == NULL )
720  {
721  Cnf_DataFree( pCnf );
722  return NULL;
723  }
724 
725  // mark used AIG inputs
726  vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
727  Vec_IntForEachEntry( vAigPis, Entry, i )
728  {
729  assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pAig) );
730  Vec_IntWriteEntry( vVisited, Entry, 1 );
731  }
732 
733  // create assumptions
734  vVar2PiId = Vec_IntStartFull( pCnf->nVars );
735  vAssumps = Vec_IntAlloc( Aig_ManCiNum(p->pFrames) );
736  Aig_ManForEachCi( p->pFrames, pObj, i )
737  {
738  int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
739  int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
740  if ( Vec_IntEntry(vVisited, iInput) == 0 )
741  continue;
742  RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
743  Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) );
744 // Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) );
745  Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i );
746  }
747  Vec_IntFree( vVisited );
748 
749  // try assumptions in different order
750  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
751  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
752  printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
753  Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
754 
755 /*
756  // AnalizeFinal does not work because it implications propagate directly
757  // and SAT solver does not kick in (the number of conflicts in 0).
758 
759  // count the number of lits in the unsat core
760  {
761  int nCoreLits, * pCoreLits;
762  nCoreLits = sat_solver_final( pSat, &pCoreLits );
763  assert( nCoreLits > 0 );
764 
765  // count the number of flops
766  vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
767  for ( i = 0; i < nCoreLits; i++ )
768  {
769  int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(pCoreLits[i]) );
770  int iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
771  int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
772  Vec_IntWriteEntry( vVisited, iInput, 1 );
773  }
774  // count the number of entries
775  Counter = 0;
776  Vec_IntForEachEntry( vVisited, Entry, i )
777  Counter += Entry;
778  Vec_IntFree( vVisited );
779 
780 // if ( p->fVerbose )
781  printf( "AnalizeFinal: Assumptions %d (out of %d). Essential PIs = %d. Conflicts = %d.\n",
782  nCoreLits, Vec_IntSize(vAssumps), Counter, (int)pSat->stats.conflicts );
783  }
784 */
785 
786  // derive literals
787  vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
788  for ( i = 0; i < Vec_VecSize(vLits); i++ )
789  printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
790  printf( "\n" );
791 
792  // create different sets of assumptions
793  Counter = Vec_VecSize(vLits);
794  for ( f = 0; f < Vec_VecSize(vLits); f++ )
795  {
796  Vec_IntClear( vAssumps );
797  Vec_VecForEachEntryInt( vLits, Entry, i, k )
798  if ( i != f )
799  Vec_IntPush( vAssumps, Entry );
800 
801  // try the new assumptions
802  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
803  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
804  printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
805  Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts );
806  if ( RetValue != l_False )
807  continue;
808 
809  // UNSAT - remove literals
810  Vec_IntClear( Vec_VecEntryInt(vLits, f) );
811  Counter--;
812  }
813 
814  for ( i = 0; i < Vec_VecSize(vLits); i++ )
815  printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
816  printf( "\n" );
817 
818  // create assumptions
819  Vec_IntClear( vAssumps );
820  Vec_VecForEachEntryInt( vLits, Entry, i, k )
821  Vec_IntPush( vAssumps, Entry );
822 
823  // try assumptions in different order
824  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
825  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
826  printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
827  Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
828 
829 // if ( p->fVerbose )
830 // printf( "Total PIs = %d. Essential PIs = %d.\n",
831 // Saig_ManPiNum(p->pAig) - p->nInputs, Counter );
832 
833 
834  // transform assumptions into reasons
835  vReasons = Vec_IntAlloc( 100 );
836  Vec_IntForEachEntry( vAssumps, Entry, i )
837  {
838  int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
839  assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) );
840  Vec_IntPush( vReasons, iPiNum );
841  }
842 
843  // cleanup
844  Cnf_DataFree( pCnf );
845  sat_solver_delete( pSat );
846  Vec_IntFree( vAssumps );
847  Vec_IntFree( vVar2PiId );
848  Vec_VecFreeP( &vLits );
849 
850  return vReasons;
851 }
852 
853 /**Function*************************************************************
854 
855  Synopsis [SAT-based refinement of the counter-example.]
856 
857  Description [The first parameter (nInputs) indicates how many first
858  primary inputs to skip without considering as care candidates.]
859 
860 
861  SideEffects []
862 
863  SeeAlso []
864 
865 ***********************************************************************/
866 Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose )
867 {
868  Saig_RefMan_t * p;
869  Vec_Int_t * vReasons;
870  Abc_Cex_t * pCare;
871  clock_t clk = clock();
872 
873  clk = clock();
874  p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose );
875  vReasons = Saig_RefManFindReason( p );
876 
877 if ( fVerbose )
878 Aig_ManPrintStats( p->pFrames );
879 
880 // if ( fVerbose )
881  {
882  Vec_Int_t * vRes = Saig_RefManReason2Inputs( p, vReasons );
883  printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
884  Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
885  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
886 ABC_PRT( "Time", clock() - clk );
887 
888  Vec_IntFree( vRes );
889 
890 /*
891  ////////////////////////////////////
892  Vec_IntFree( vReasons );
893  vReasons = Saig_RefManRefineWithSat( p, vRes );
894  ////////////////////////////////////
895 
896  Vec_IntFree( vRes );
897  vRes = Saig_RefManReason2Inputs( p, vReasons );
898  printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
899  Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
900  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
901 
902  Vec_IntFree( vRes );
903 ABC_PRT( "Time", clock() - clk );
904 */
905  }
906 
907  pCare = Saig_RefManReason2Cex( p, vReasons );
908  Vec_IntFree( vReasons );
909  Saig_RefManStop( p );
910 
911 if ( fVerbose )
912 Abc_CexPrintStats( pCex );
913 if ( fVerbose )
914 Abc_CexPrintStats( pCare );
915 
916  return pCare;
917 }
918 
919 /**Function*************************************************************
920 
921  Synopsis [Returns the array of PIs for flops that should not be absracted.]
922 
923  Description []
924 
925  SideEffects []
926 
927  SeeAlso []
928 
929 ***********************************************************************/
930 Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose )
931 {
932  Saig_RefMan_t * p;
933  Vec_Int_t * vRes, * vReasons;
934  clock_t clk;
935  if ( Saig_ManPiNum(pAig) != pCex->nPis )
936  {
937  printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n",
938  Aig_ManCiNum(pAig), pCex->nPis );
939  return NULL;
940  }
941 
942 clk = clock();
943 
944  p = Saig_RefManStart( pAig, pCex, iFirstFlopPi, fVerbose );
945  vReasons = Saig_RefManFindReason( p );
946  vRes = Saig_RefManReason2Inputs( p, vReasons );
947 
948 // if ( fVerbose )
949  {
950  printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
951  Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
952  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
953 ABC_PRT( "Time", clock() - clk );
954  }
955 
956 /*
957  ////////////////////////////////////
958  Vec_IntFree( vReasons );
959  vReasons = Saig_RefManRefineWithSat( p, vRes );
960  ////////////////////////////////////
961 
962  // derive new result
963  Vec_IntFree( vRes );
964  vRes = Saig_RefManReason2Inputs( p, vReasons );
965 // if ( fVerbose )
966  {
967  printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
968  Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
969  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
970 ABC_PRT( "Time", clock() - clk );
971  }
972 */
973 
974  Vec_IntFree( vReasons );
975  Saig_RefManStop( p );
976  return vRes;
977 }
978 
979 
980 ////////////////////////////////////////////////////////////////////////
981 /// END OF FILE ///
982 ////////////////////////////////////////////////////////////////////////
983 
984 
986 
char * memset()
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vec_Int_t * vMapPiF2A
Definition: saigRefSat.c:43
static Vec_Vec_t * Vec_VecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecVec.h:145
static int Aig_ObjFaninId0(Aig_Obj_t *pObj)
Definition: aig.h:304
Aig_Man_t * Saig_ManUnrollWithCex(Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, Vec_Int_t **pvMapPiF2A)
Definition: saigRefSat.c:264
static void Vec_VecSort(Vec_Vec_t *p, int fReverse)
Definition: vecVec.h:546
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Abc_Cex_t * Saig_RefManReason2Cex(Saig_RefMan_t *p, Vec_Int_t *vReasons)
Definition: saigRefSat.c:93
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Vec_Int_t * Saig_RefManFindReason(Saig_RefMan_t *p)
Definition: saigRefSat.c:168
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
void * pData
Definition: aig.h:87
Abc_Cex_t * Saig_ManFindCexCareBits(Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fNewOrder, int fVerbose)
Definition: saigRefSat.c:866
static int lit_var(lit l)
Definition: satVec.h:145
Vec_Int_t * Saig_RefManRefineWithSat(Saig_RefMan_t *p, Vec_Int_t *vAigPis)
Definition: saigRefSat.c:706
Abc_Cex_t * Saig_RefManRunSat(Saig_RefMan_t *p, int fNewOrder)
Definition: saigRefSat.c:502
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Vec_Vec_t * Saig_RefManOrderLiterals(Saig_RefMan_t *p, Vec_Int_t *vVar2PiId, Vec_Int_t *vAssumps)
Definition: saigRefSat.c:438
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
int Saig_RefManSetPhases(Saig_RefMan_t *p, Abc_Cex_t *pCare, int fValue1)
Definition: saigRefSat.c:404
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int * pVarNums
Definition: cnf.h:63
void Cnf_DataTranformPolarity(Cnf_Dat_t *pCnf, int fTransformPos)
Definition: cnfMan.c:652
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
#define l_True
Definition: SolverTypes.h:84
Abc_Cex_t * pCex
Definition: saigRefSat.c:38
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
void Aig_ManStopP(Aig_Man_t **p)
Definition: aigMan.c:246
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
static int Aig_ObjFaninId1(Aig_Obj_t *pObj)
Definition: aig.h:305
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
stats_t stats
Definition: satSolver.h:156
Definition: cnf.h:56
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
#define Vec_VecForEachEntryInt(vGlob, Entry, i, k)
Definition: vecVec.h:109
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
void Saig_ManUnrollCollect_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vObjs, Vec_Int_t *vRoots)
Definition: saigRefSat.c:236
static int sat_solver_final(sat_solver *s, int **ppArray)
Definition: satSolver.h:227
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_Man_t * pAig
Definition: saigRefSat.c:37
int Saig_ManSimDataInit(Aig_Man_t *p, Abc_Cex_t *pCex, Vec_Ptr_t *vSimInfo, Vec_Int_t *vRes)
Definition: absOldSim.c:174
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Abc_Cex_t * Saig_RefManCreateCex(Saig_RefMan_t *p, Vec_Int_t *vVar2PiId, Vec_Int_t *vAssumps)
Definition: saigRefSat.c:473
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static void Vec_VecPushInt(Vec_Vec_t *p, int Level, int Entry)
Definition: vecVec.h:468
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
static lit toLitCond(int v, int c)
Definition: satVec.h:143
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
void Abc_CexPrintStats(Abc_Cex_t *p)
Definition: utilCex.c:256
static Aig_Obj_t * Saig_ObjLiToLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:87
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
void Saig_RefManFindReason_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Int_t *vPrios, Vec_Int_t *vReasons)
Definition: saigRefSat.c:120
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Counter
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static Vec_Vec_t * Vec_VecStart(int nSize)
Definition: vecVec.h:168
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static Vec_Int_t * Vec_VecEntryInt(Vec_Vec_t *p, int i)
Definition: vecVec.h:276
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Saig_RefMan_t * Saig_RefManStart(Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
Definition: saigRefSat.c:363
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
ABC_INT64_T conflicts
Definition: satVec.h:154
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
unsigned int fPhase
Definition: aig.h:78
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
Aig_Man_t * pFrames
Definition: saigRefSat.c:42
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_Cex_t * Abc_CexDup(Abc_Cex_t *p, int nRegsNew)
Definition: utilCex.c:145
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Vec_Int_t * Saig_RefManReason2Inputs(Saig_RefMan_t *p, Vec_Int_t *vReasons)
FUNCTION DEFINITIONS ///.
Definition: saigRefSat.c:64
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
static int Vec_VecSize(Vec_Vec_t *p)
Definition: vecVec.h:222
void Saig_RefManStop(Saig_RefMan_t *p)
Definition: saigRefSat.c:386
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
static void Vec_VecFreeP(Vec_Vec_t **p)
Definition: vecVec.h:367
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
static Vec_Ptr_t * Vec_VecEntry(Vec_Vec_t *p, int i)
Definition: vecVec.h:271
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Int_t * Saig_ManExtendCounterExampleTest3(Aig_Man_t *pAig, int iFirstFlopPi, Abc_Cex_t *pCex, int fVerbose)
Definition: saigRefSat.c:930
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
typedefABC_NAMESPACE_IMPL_START struct Saig_RefMan_t_ Saig_RefMan_t
DECLARATIONS ///.
Definition: saigRefSat.c:33
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285