abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigUnfold2.c File Reference

Go to the source code of this file.

Functions

int Saig_ManFilterUsingIndOne2 (Aig_Man_t *p, Aig_Man_t *pFrame, sat_solver *pSat, Cnf_Dat_t *pCnf, int nConfs, int nProps, int Counter, int type_)
 
Aig_Man_tSaig_ManCreateIndMiter2 (Aig_Man_t *pAig, Vec_Vec_t *vCands)
 
void Saig_ManFilterUsingInd2 (Aig_Man_t *p, Vec_Vec_t *vCands, int nConfs, int nProps, int fVerbose)
 
Vec_Vec_tSsw_ManFindDirectImplications2 (Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fVerbose)
 
Aig_Man_tSaig_ManDupUnfoldConstrsFunc2 (Aig_Man_t *pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose, int *typeII_cnt)
 
Aig_Man_tSaig_ManDupFoldConstrsFunc2 (Aig_Man_t *pAig, int fCompl, int fVerbose, int typeII_cnt)
 

Function Documentation

Aig_Man_t* Saig_ManCreateIndMiter2 ( Aig_Man_t pAig,
Vec_Vec_t vCands 
)

Definition at line 22 of file saigUnfold2.c.

23 {
24  int nFrames = 3;
25  Vec_Ptr_t * vNodes;
26  Aig_Man_t * pFrames;
27  Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
28  Aig_Obj_t ** pObjMap;
29  int i, f, k;
30 
31  // create mapping for the frames nodes
32  pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
33 
34  // start the fraig package
35  pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
36  pFrames->pName = Abc_UtilStrsav( pAig->pName );
37  pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
38  // map constant nodes
39  for ( f = 0; f < nFrames; f++ )
40  Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
41  // create PI nodes for the frames
42  for ( f = 0; f < nFrames; f++ )
43  Aig_ManForEachPiSeq( pAig, pObj, i )
44  Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
45  // set initial state for the latches
46  Aig_ManForEachLoSeq( pAig, pObj, i )
47  Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
48 
49  // add timeframes
50  for ( f = 0; f < nFrames; f++ )
51  {
52  // add internal nodes of this frame
53  Aig_ManForEachNode( pAig, pObj, i )
54  {
55  pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
56  Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
57  }
58  // set the latch inputs and copy them into the latch outputs of the next frame
59  Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
60  {
61  pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
62  if ( f < nFrames - 1 )
63  Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
64  }
65  }
66 
67  // go through the candidates
68  Vec_VecForEachLevel( vCands, vNodes, i )
69  {
70  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
71  {
72  Aig_Obj_t * pObjR = Aig_Regular(pObj);
73  Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0];
74  Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1];
75  {
76  Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) );
77  Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) );
78  Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 );
79  Aig_ObjCreateCo( pFrames, pMiter );
80 
81  /* need to check p & Xp is satisfiable */
82  /* jlong -- begin */
83  {
84  Aig_Obj_t * pMiter2 = Aig_And( pFrames, pFan0, Aig_Not(pFan1));
85  Aig_ObjCreateCo( pFrames, pMiter2 );
86  }
87  /* jlong -- end */
88  }
89 
90  { /* jlong -- begin */
91  Aig_Obj_t * pNode2 = pObjMap[nFrames*Aig_ObjId(pObjR)+2];
92  Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) );
93  Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, Aig_IsComplement(pObj) );
94  Aig_Obj_t * pFan2 = Aig_NotCond( pNode2, !Aig_IsComplement(pObj) );
95  Aig_Obj_t * pMiter = Aig_And( pFrames, Aig_And(pFrames, pFan0, pFan1 ), pFan2);
96  Aig_ObjCreateCo( pFrames, pMiter ); /* jlong -- end */
97  }
98 
99  }
100  }
101  Aig_ManCleanup( pFrames );
102  ABC_FREE( pObjMap );
103 
104 //Aig_ManShow( pAig, 0, NULL );
105 //Aig_ManShow( pFrames, 0, NULL );
106  return pFrames;
107 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
#define Vec_VecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition: vecVec.h:55
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static Aig_Obj_t * Aig_ObjChild1Frames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i)
Definition: aigFrames.c:34
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
static void Aig_ObjSetFrames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
Definition: aigFrames.c:31
for(p=first;p->value< newval;p=p->next)
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
Definition: aig.h:69
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
#define ABC_FREE(obj)
Definition: abc_global.h:232
static Aig_Obj_t * Aig_ObjChild0Frames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i)
Definition: aigFrames.c:33
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438
Aig_Man_t* Saig_ManDupFoldConstrsFunc2 ( Aig_Man_t pAig,
int  fCompl,
int  fVerbose,
int  typeII_cnt 
)

Function*************************************************************

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 375 of file saigUnfold2.c.

377 {
378  Aig_Man_t * pAigNew;
379  Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
380  int i, typeII_cc, type_II;
381  if ( Aig_ManConstrNum(pAig) == 0 )
382  return Aig_ManDupDfs( pAig );
383  assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
384  // start the new manager
385  pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
386  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
387  pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
388  // map the constant node
389  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
390  // create variables for PIs
391  Aig_ManForEachCi( pAig, pObj, i )
392  pObj->pData = Aig_ObjCreateCi( pAigNew );
393  // add internal nodes of this frame
394  Aig_ManForEachNode( pAig, pObj, i )
395  pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
396 
397  // OR the constraint outputs
398  pMiter = Aig_ManConst0( pAigNew );
399  typeII_cc = 0;//typeII_cnt;
400  typeII_cnt = 0;
401  type_II = 0;
402 
403  Saig_ManForEachPo( pAig, pObj, i )
404  {
405 
406  if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
407  continue;
408  if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
409  type_II = 1;
410  }
411  /* now we got the constraint */
412  if (type_II) {
413 
414  Aig_Obj_t * type_II_latch
415  = Aig_ObjCreateCi(pAigNew); /* will get connected later; */
416  pMiter = Aig_Or(pAigNew, pMiter,
417  Aig_And(pAigNew,
418  Aig_NotCond(type_II_latch, fCompl),
419  Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) )
420  );
421  printf( "modeling typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
422  } else
423  pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
424  }
425 
426  // create additional flop
427  if ( Saig_ManRegNum(pAig) > 0 )
428  {
429  pFlopOut = Aig_ObjCreateCi( pAigNew );
430  pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut );
431  }
432  else
433  pFlopIn = pMiter;
434 
435  // create primary output
436  Saig_ManForEachPo( pAig, pObj, i )
437  {
438  if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
439  continue;
440  pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
441  Aig_ObjCreateCo( pAigNew, pMiter );
442  }
443 
444  // transfer to register outputs
445  {
446  /* the same for type I and type II */
447  Aig_Obj_t * pObjLi, *pObjLo;
448 
449  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) {
450  if( i + typeII_cc < Aig_ManRegNum(pAig)) {
451  Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn),
452  Aig_ObjChild0Copy(pObjLi) ,
453  pObjLo->pData);
454  Aig_ObjCreateCo( pAigNew, c);
455  } else {
456  printf ( "skipping: reg%d\n", i);
457  Aig_ObjCreateCo( pAigNew,Aig_ObjChild0Copy(pObjLi));
458  }
459  }
460 
461  }
462  if(0)Saig_ManForEachLi( pAig, pObj, i ) {
463  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
464  }
465  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
466 
467  type_II = 0;
468  Saig_ManForEachPo( pAig, pObj, i )
469  {
470 
471  if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
472  continue;
473  if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
474  type_II = 1;
475  }
476  /* now we got the constraint */
477  if (type_II) {
478  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj));
479  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
480  printf( "Latch for typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
481  }
482  }
483 
484 
485  // create additional flop
486 
487  if ( Saig_ManRegNum(pAig) > 0 )
488  {
489  Aig_ObjCreateCo( pAigNew, pFlopIn );
490  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
491  }
492  printf("#reg after fold2: %d\n", Aig_ManRegNum(pAigNew));
493  // perform cleanup
494  Aig_ManCleanup( pAigNew );
495  Aig_ManSeqCleanup( pAigNew );
496  return pAigNew;
497 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
static int Aig_ManConstrNum(Aig_Man_t *p)
Definition: aig.h:261
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition: aigScl.c:158
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
void * pData
Definition: aig.h:87
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition: aigDup.c:563
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Definition: aig.h:69
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Aig_Obj_t * Aig_Mux(Aig_Man_t *p, Aig_Obj_t *pC, Aig_Obj_t *p1, Aig_Obj_t *p0)
Definition: aigOper.c:317
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Aig_Man_t* Saig_ManDupUnfoldConstrsFunc2 ( Aig_Man_t pAig,
int  nFrames,
int  nConfs,
int  nProps,
int  fOldAlgo,
int  fVerbose,
int *  typeII_cnt 
)

Function*************************************************************

Synopsis [Duplicates the AIG while unfolding constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 295 of file saigUnfold2.c.

295  {
296  Aig_Man_t * pNew;
297  Vec_Vec_t * vCands;
298  Vec_Ptr_t * vNewFlops;
299  Aig_Obj_t * pObj;
300  int i, k, nNewFlops;
301  const int fCompl = 0 ;
302  if ( fOldAlgo )
303  vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
304  else
305  vCands = Ssw_ManFindDirectImplications2( pAig, nFrames, nConfs, nProps, fVerbose );
306  if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
307  {
308  Vec_VecFreeP( &vCands );
309  return Aig_ManDupDfs( pAig );
310  }
311  // create new manager
312  pNew = Aig_ManDupWithoutPos( pAig ); /* good */
313  pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
314  pNew->nConstrs = pAig->nConstrs + Vec_PtrSize(pAig->unfold2_type_II)
315  + Vec_PtrSize(pAig->unfold2_type_I);
316  // pNew->nConstrsTypeII = Vec_PtrSize(pAig->unfold2_type_II);
317  *typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II);
318 
319  /* new set of registers */
320 
321  // add normal POs
322  Saig_ManForEachPo( pAig, pObj, i )
323  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
324  // create constraint outputs
325  vNewFlops = Vec_PtrAlloc( 100 );
326 
327 
328  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){
329  Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
330  Aig_ObjCreateCo(pNew, x);
331  }
332 
333  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
334  Aig_Obj_t * type_II_latch
335  = Aig_ObjCreateCi(pNew); /* will get connected later; */
336  Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
337 
338  Aig_Obj_t * n = Aig_And(pNew,
339  Aig_NotCond(type_II_latch, fCompl),
340  Aig_NotCond(x, fCompl));
341  Aig_ObjCreateCo(pNew, n);//Aig_Not(n));
342  }
343 
344  // add latch outputs
345  Saig_ManForEachLi( pAig, pObj, i )
346  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
347 
348  Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
349  Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
350  Aig_ObjCreateCo(pNew, x);
351  }
352 
353  // add new latch outputs
354  nNewFlops = Vec_PtrSize(pAig->unfold2_type_II);
355  //assert( nNewFlops == Vec_PtrSize(vNewFlops) );
356  Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
357  printf("#reg after unfold2: %d\n", Aig_ManRegNum(pAig) + nNewFlops );
358  Vec_VecFreeP( &vCands );
359  Vec_PtrFree( vNewFlops );
360  return pNew;
361 
362 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition: aigDup.c:563
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
static Aig_Obj_t * Aig_ObjRealCopy(Aig_Obj_t *pObj)
Definition: aig.h:320
Vec_Vec_t * Ssw_ManFindDirectImplications2(Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fVerbose)
Definition: saigUnfold2.c:197
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Definition: aig.h:69
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
static int Vec_VecSizeSize(Vec_Vec_t *p)
Definition: vecVec.h:417
Vec_Vec_t * Saig_ManDetectConstrFunc(Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fVerbose)
Definition: saigConstr2.c:661
static void Vec_VecFreeP(Vec_Vec_t **p)
Definition: vecVec.h:367
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Aig_Man_t * Aig_ManDupWithoutPos(Aig_Man_t *p)
Definition: aigDup.c:835
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void Saig_ManFilterUsingInd2 ( Aig_Man_t p,
Vec_Vec_t vCands,
int  nConfs,
int  nProps,
int  fVerbose 
)

Function*************************************************************

Synopsis [Detects constraints functionally.]

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file saigUnfold2.c.

121 {
122  Vec_Ptr_t * vNodes;
123  Aig_Man_t * pFrames;
124  sat_solver * pSat;
125  Cnf_Dat_t * pCnf;
126  Aig_Obj_t * pObj;
127  int i, k, k2, Counter;
128  /*
129  Vec_VecForEachLevel( vCands, vNodes, i )
130  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
131  printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) );
132  printf( "\n" );
133  */
134  // create timeframes
135  // pFrames = Saig_ManUnrollInd( p );
136  pFrames = Saig_ManCreateIndMiter2( p, vCands );
137  assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands)*3 );
138  // start the SAT solver
139  pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
140  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
141  // check candidates
142  if ( fVerbose )
143  printf( "Filtered cands: \n" );
144  Counter = 0;
145  Vec_VecForEachLevel( vCands, vNodes, i )
146  {
147  assert(i==0); /* only one item */
148  k2 = 0;
149  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
150  {
151  if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ , 0) == l_False)
152  // if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) )
153  {
154  Vec_PtrWriteEntry( vNodes, k2++, pObj );
155  if ( fVerbose )
156  printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
157  printf( " type I : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
158  Vec_PtrPush(p->unfold2_type_I, pObj);
159  }
160  /* jlong -- begin */
161  else if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 1) == l_True ) /* can be self-conflicting */
162  {
163  if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 2) == l_False ){
164  //Vec_PtrWriteEntry( vNodes, k2++, pObj );
165  if ( fVerbose )
166  printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
167  printf( " type II: %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
168  Vec_PtrWriteEntry( vNodes, k2++, pObj ); /* add type II constraints */
169  Vec_PtrPush(p->unfold2_type_II, pObj);
170  }
171  }
172  /* jlong -- end */
173  }
174  Vec_PtrShrink( vNodes, k2 );
175  }
176 
177  // clean up
178  Cnf_DataFree( pCnf );
179  sat_solver_delete( pSat );
180  if ( fVerbose )
181  Aig_ManPrintStats( pFrames );
182  Aig_ManStop( pFrames );
183 }
#define Vec_VecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition: vecVec.h:55
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
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
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
int Saig_ManFilterUsingIndOne2(Aig_Man_t *p, Aig_Man_t *pFrame, sat_solver *pSat, Cnf_Dat_t *pCnf, int nConfs, int nProps, int Counter, int type_)
Definition: saigUnfold2.c:2
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
#define l_True
Definition: SolverTypes.h:84
Definition: cnf.h:56
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Definition: aig.h:69
static int Counter
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
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
static int Vec_VecSizeSize(Vec_Vec_t *p)
Definition: vecVec.h:417
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Vec_PtrShrink(Vec_Ptr_t *p, int nSizeNew)
Definition: vecPtr.h:528
Aig_Man_t * Saig_ManCreateIndMiter2(Aig_Man_t *pAig, Vec_Vec_t *vCands)
Definition: saigUnfold2.c:22
int Saig_ManFilterUsingIndOne2 ( Aig_Man_t p,
Aig_Man_t pFrame,
sat_solver pSat,
Cnf_Dat_t pCnf,
int  nConfs,
int  nProps,
int  Counter,
int  type_ 
)

Definition at line 2 of file saigUnfold2.c.

5 {
6  Aig_Obj_t * pObj;
7  int Lit, status;
8  pObj = Aig_ManCo( pFrame, Counter*3+type_ ); /* which co */
9  Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
10  status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
11  if ( status == l_False ) /* unsat */
12  return status;
13  if ( status == l_Undef )
14  {
15  printf( "Solver returned undecided.\n" );
16  return status;
17  }
18  assert( status == l_True );
19  return status;
20 }
#define l_Undef
Definition: SolverTypes.h:86
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
int * pVarNums
Definition: cnf.h:63
#define l_True
Definition: SolverTypes.h:84
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Definition: aig.h:69
static int Counter
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
#define l_False
Definition: SolverTypes.h:85
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
Vec_Vec_t* Ssw_ManFindDirectImplications2 ( Aig_Man_t p,
int  nFrames,
int  nConfs,
int  nProps,
int  fVerbose 
)

Function*************************************************************

Synopsis [Returns the number of variables implied by the output.]

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file saigUnfold2.c.

198 {
199  Vec_Vec_t * vCands = NULL;
200  Vec_Ptr_t * vNodes;
201  Cnf_Dat_t * pCnf;
202  sat_solver * pSat;
203  Aig_Man_t * pFrames;
204  Aig_Obj_t * pObj, * pRepr, * pReprR;
205  int i, f, k, value;
206  assert(nFrames == 1);
207  vCands = Vec_VecAlloc( nFrames );
208  assert(nFrames == 1);
209  // perform unrolling
210  pFrames = Saig_ManUnrollCOI( p, nFrames );
211  assert( Aig_ManCoNum(pFrames) == 1 );
212  // start the SAT solver
213  pCnf = Cnf_DeriveSimple( pFrames, 0 );
214  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
215  if ( pSat != NULL )
216  {
218  for ( f = 0; f < nFrames; f++ )
219  {
220  Aig_ManForEachObj( p, pObj, i )
221  {
222  if ( !Aig_ObjIsCand(pObj) )
223  continue;
224  //--jlong : also use internal nodes as well
225  /* if ( !Aig_ObjIsCi(pObj) ) */
226  /* continue; */
227  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
228  continue;
229  // get the node from timeframes
230  pRepr = p->pObjCopies[nFrames*i + nFrames-1-f];
231  pReprR = Aig_Regular(pRepr);
232  if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
233  continue;
234  // value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
235  value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] );
236  if ( value == l_Undef )
237  continue;
238  // label this node as taken
239  Aig_ObjSetTravIdCurrent(p, pObj);
240  if ( Saig_ObjIsLo(p, pObj) )
242  // remember the node
243  Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) );
244  // printf( "%s%d ", (value == l_False)? "":"!", i );
245  }
246  }
247  // printf( "\n" );
248  sat_solver_delete( pSat );
249  }
250  Aig_ManStop( pFrames );
251  Cnf_DataFree( pCnf );
252 
253  if ( fVerbose )
254  {
255  printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
256  Vec_VecForEachLevel( vCands, vNodes, k )
257  {
258  printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) );
259  // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
260  // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
261  printf( "\n" );
262  }
263  }
264 
265  ABC_FREE( p->pObjCopies );
266  /* -- jlong -- this does the SAT proof of the constraints */
267  Saig_ManFilterUsingInd2( p, vCands, nConfs, nProps, fVerbose );
268  if ( Vec_VecSizeSize(vCands) )
269  printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
270  if ( fVerbose )
271  {
272  Vec_VecForEachLevel( vCands, vNodes, k )
273  {
274  printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) );
275  // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
276  // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
277  printf( "\n" );
278  }
279  }
280 
281  return vCands;
282 }
#define Vec_VecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition: vecVec.h:55
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static void Vec_VecPush(Vec_Vec_t *p, int Level, void *Entry)
Definition: vecVec.h:456
static Vec_Vec_t * Vec_VecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecVec.h:145
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
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
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
#define l_Undef
Definition: SolverTypes.h:86
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
void Saig_ManFilterUsingInd2(Aig_Man_t *p, Vec_Vec_t *vCands, int nConfs, int nProps, int fVerbose)
Definition: saigUnfold2.c:120
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
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
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
int * pVarNums
Definition: cnf.h:63
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
#define l_True
Definition: SolverTypes.h:84
Aig_Man_t * Saig_ManUnrollCOI(Aig_Man_t *pAig, int nFrames)
Definition: saigConstr2.c:431
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Definition: cnf.h:56
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Definition: aig.h:69
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
#define ABC_FREE(obj)
Definition: abc_global.h:232
static int Vec_VecSizeSize(Vec_Vec_t *p)
Definition: vecVec.h:417
static int Aig_ObjIsCand(Aig_Obj_t *pObj)
Definition: aig.h:284
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
int value
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
int sat_solver_get_var_value(sat_solver *s, int v)
Definition: satSolver.c:117