abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llb2Core.c File Reference
#include "llbInt.h"

Go to the source code of this file.

Data Structures

struct  Llb_Img_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Llb_Img_t_ 
Llb_Img_t
 DECLARATIONS ///. More...
 

Functions

DdNodeLlb_CoreComputeCube (DdManager *dd, Vec_Int_t *vVars, int fUseVarIndex, char *pValues)
 FUNCTION DEFINITIONS ///. More...
 
Abc_Cex_tLlb_CoreDeriveCex (Llb_Img_t *p)
 
int Llb_CoreReachability_int (Llb_Img_t *p, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1)
 
int Llb_CoreReachability (Llb_Img_t *p)
 
Vec_Ptr_tLlb_CoreConstructAll (Aig_Man_t *p, Vec_Ptr_t *vResult, Vec_Int_t *vVarsNs, abctime TimeTarget)
 
void Llb_CoreSetVarMaps (Llb_Img_t *p)
 
Llb_Img_tLlb_CoreStart (Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
 
void Llb_CoreStop (Llb_Img_t *p)
 
int Llb_CoreExperiment (Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars, Vec_Ptr_t *vResult, abctime TimeTarget)
 
int Llb_ManReachMinCut (Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Llb_Img_t_ Llb_Img_t

DECLARATIONS ///.

CFile****************************************************************

FileName [llb2Core.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Core procedure.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
llb2Core.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 30 of file llb2Core.c.

Function Documentation

DdNode* Llb_CoreComputeCube ( DdManager dd,
Vec_Int_t vVars,
int  fUseVarIndex,
char *  pValues 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes cube composed of given variables with given values.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file llb2Core.c.

69 {
70  DdNode * bRes, * bVar, * bTemp;
71  int i, iVar, Index;
72  abctime TimeStop;
73  TimeStop = dd->TimeStop; dd->TimeStop = 0;
74  bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
75  Vec_IntForEachEntry( vVars, Index, i )
76  {
77  iVar = fUseVarIndex ? Index : i;
78  bVar = Cudd_NotCond( Cudd_bddIthVar(dd, iVar), (int)(pValues == NULL || pValues[i] != 1) );
79  bRes = Cudd_bddAnd( dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
80  Cudd_RecursiveDeref( dd, bTemp );
81  }
82  Cudd_Deref( bRes );
83  dd->TimeStop = TimeStop;
84  return bRes;
85 }
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
abctime TimeStop
Definition: cuddInt.h:489
Definition: cudd.h:278
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Ptr_t* Llb_CoreConstructAll ( Aig_Man_t p,
Vec_Ptr_t vResult,
Vec_Int_t vVarsNs,
abctime  TimeTarget 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 534 of file llb2Core.c.

535 {
536  DdManager * dd;
537  Vec_Ptr_t * vDdMans;
538  Vec_Ptr_t * vLower, * vUpper = NULL;
539  int i;
540  vDdMans = Vec_PtrStart( Vec_PtrSize(vResult) );
541  Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vResult, vLower, i )
542  {
543  if ( i < Vec_PtrSize(vResult) - 1 )
544  dd = Llb_ImgPartition( p, vLower, vUpper, TimeTarget );
545  else
546  dd = Llb_DriverLastPartition( p, vVarsNs, TimeTarget );
547  if ( dd == NULL )
548  {
549  Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
550  {
551  if ( dd == NULL )
552  continue;
553  if ( dd->bFunc )
554  Cudd_RecursiveDeref( dd, dd->bFunc );
555  Extra_StopManager( dd );
556  }
557  Vec_PtrFree( vDdMans );
558  return NULL;
559  }
560  Vec_PtrWriteEntry( vDdMans, i, dd );
561  vUpper = vLower;
562  }
563  return vDdMans;
564 }
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition: vecPtr.h:63
DdManager * Llb_DriverLastPartition(Aig_Man_t *p, Vec_Int_t *vVarsNs, abctime TimeTarget)
Definition: llb2Driver.c:163
DdNode * bFunc
Definition: cuddInt.h:487
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
DdManager * Llb_ImgPartition(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper, abctime TimeTarget)
Definition: llb2Image.c:183
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Abc_Cex_t* Llb_CoreDeriveCex ( Llb_Img_t p)

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

Synopsis [Derives counter-example by backward reachability.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file llb2Core.c.

99 {
100  Abc_Cex_t * pCex;
101  Aig_Obj_t * pObj;
102  Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
103  DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
104  int i, v, RetValue, nPiOffset;
105  char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
106  assert( Vec_PtrSize(p->vRings) > 0 );
107 
108  p->dd->TimeStop = 0;
109  p->ddR->TimeStop = 0;
110 
111  // get supports and quantified variables
112  Vec_PtrReverseOrder( p->vDdMans );
113  vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsNs, p->vVarsCs, 1, 0 );
114  Llb_ImgSchedule( vSupps, &vQuant0, &vQuant1, 0 );
115  Vec_VecFree( (Vec_Vec_t *)vSupps );
116  Llb_ImgQuantifyReset( p->vDdMans );
117 // Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0 );
118 
119  // allocate room for the counter-example
120  pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
121  pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
122  pCex->iPo = -1;
123 
124  // get the last cube
125  bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
126  RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
127  Cudd_RecursiveDeref( p->ddR, bOneCube );
128  assert( RetValue );
129 
130  // write PIs of counter-example
131  nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
132  Saig_ManForEachPi( p->pAig, pObj, i )
133  if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
134  Abc_InfoSetBit( pCex->pData, nPiOffset + i );
135 
136  // write state in terms of NS variables
137  if ( Vec_PtrSize(p->vRings) > 1 )
138  {
139  bState = Llb_CoreComputeCube( p->dd, p->vVarsNs, 1, pValues ); Cudd_Ref( bState );
140  }
141  // perform backward analysis
142  Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
143  {
144  if ( v == Vec_PtrSize(p->vRings) - 1 )
145  continue;
146  // compute the next states
147  bImage = Llb_ImgComputeImage( p->pAig, p->vDdMans, p->dd, bState,
148  vQuant0, vQuant1, p->vDriRefs, p->pPars->TimeTarget, 1, 0, 0 );
149  assert( bImage != NULL );
150  Cudd_Ref( bImage );
151  Cudd_RecursiveDeref( p->dd, bState );
152 //Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
153 
154  // move reached states into ring manager
155  bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
156  Cudd_RecursiveDeref( p->dd, bTemp );
157 
158  // intersect with the previous set
159  bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
160  Cudd_RecursiveDeref( p->ddR, bImage );
161 
162  // find any assignment of the BDD
163  RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
164  Cudd_RecursiveDeref( p->ddR, bOneCube );
165  assert( RetValue );
166 
167  // write PIs of counter-example
168  nPiOffset -= Saig_ManPiNum(p->pAig);
169  Saig_ManForEachPi( p->pAig, pObj, i )
170  if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
171  Abc_InfoSetBit( pCex->pData, nPiOffset + i );
172 
173  // check that we get the init state
174  if ( v == 0 )
175  {
176  Saig_ManForEachLo( p->pAig, pObj, i )
177  assert( pValues[i] == 0 );
178  break;
179  }
180 
181  // write state in terms of NS variables
182  bState = Llb_CoreComputeCube( p->dd, p->vVarsNs, 1, pValues ); Cudd_Ref( bState );
183  }
184  assert( nPiOffset == Saig_ManRegNum(p->pAig) );
185  // update the output number
186  RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
187  assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
188  pCex->iPo = RetValue;
189  // cleanup
190  ABC_FREE( pValues );
191  Vec_VecFree( (Vec_Vec_t *)vQuant0 );
192  Vec_VecFree( (Vec_Vec_t *)vQuant1 );
193  return pCex;
194 }
void Llb_ImgSchedule(Vec_Ptr_t *vSupps, Vec_Ptr_t **pvQuant0, Vec_Ptr_t **pvQuant1, int fVerbose)
Definition: llb2Image.c:122
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static void Vec_PtrReverseOrder(Vec_Ptr_t *p)
Definition: vecPtr.h:785
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
DdManager * dd
Definition: llb3Image.c:52
Aig_Man_t * pAig
Definition: llb3Image.c:49
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
abctime TimeStop
Definition: cuddInt.h:489
Definition: cudd.h:278
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 Llb_Mgr_t * p
Definition: llb3Image.c:950
int Cudd_bddPickOneCube(DdManager *ddm, DdNode *node, char *string)
Definition: cuddUtil.c:1221
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition: vecPtr.h:63
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
Definition: extraBddMisc.c:87
DdNode * Llb_ImgComputeImage(Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, DdManager *dd, DdNode *bInit, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1, Vec_Int_t *vDriRefs, abctime TimeTarget, int fBackward, int fReorder, int fVerbose)
Definition: llb2Image.c:364
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
int Cudd_ReadSize(DdManager *dd)
Definition: cuddAPI.c:1441
static void * Vec_PtrEntryLast(Vec_Ptr_t *p)
Definition: vecPtr.h:413
if(last==0)
Definition: sparse_int.h:34
DdNode * Llb_CoreComputeCube(DdManager *dd, Vec_Int_t *vVars, int fUseVarIndex, char *pValues)
FUNCTION DEFINITIONS ///.
Definition: llb2Core.c:68
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Vec_Ptr_t * Llb_ImgSupports(Aig_Man_t *p, Vec_Ptr_t *vDdMans, Vec_Int_t *vStart, Vec_Int_t *vStop, int fAddPis, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: llb2Image.c:48
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
void Llb_ImgQuantifyReset(Vec_Ptr_t *vDdMans)
Definition: llb2Image.c:340
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
DdNode * Cudd_bddIntersect(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:282
int Saig_ManFindFailedPoCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:434
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
int Llb_CoreExperiment ( Aig_Man_t pInit,
Aig_Man_t pAig,
Gia_ParLlb_t pPars,
Vec_Ptr_t vResult,
abctime  TimeTarget 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 694 of file llb2Core.c.

695 {
696  int RetValue;
697  Llb_Img_t * p;
698 // printf( "\n" );
699 // pPars->fVerbose = 1;
700  p = Llb_CoreStart( pInit, pAig, pPars );
701  p->vDdMans = Llb_CoreConstructAll( pAig, vResult, p->vVarsNs, TimeTarget );
702  if ( p->vDdMans == NULL )
703  {
704  if ( !pPars->fSilent )
705  printf( "Reached timeout (%d seconds) while deriving the partitions.\n", pPars->TimeLimit );
706  Llb_CoreStop( p );
707  return -1;
708  }
709  RetValue = Llb_CoreReachability( p );
710  Llb_CoreStop( p );
711  return RetValue;
712 }
typedefABC_NAMESPACE_IMPL_START struct Llb_Img_t_ Llb_Img_t
DECLARATIONS ///.
Definition: llb2Core.c:30
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Llb_Img_t * Llb_CoreStart(Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
Definition: llb2Core.c:618
int Llb_CoreReachability(Llb_Img_t *p)
Definition: llb2Core.c:499
void Llb_CoreStop(Llb_Img_t *p)
Definition: llb2Core.c:650
Vec_Ptr_t * Llb_CoreConstructAll(Aig_Man_t *p, Vec_Ptr_t *vResult, Vec_Int_t *vVarsNs, abctime TimeTarget)
Definition: llb2Core.c:534
int Llb_CoreReachability ( Llb_Img_t p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 499 of file llb2Core.c.

500 {
501  Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
502  int RetValue;
503  // get supports and quantified variables
504  if ( p->pPars->fBackward )
505  {
506  Vec_PtrReverseOrder( p->vDdMans );
507  vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsNs, p->vVarsCs, 0, p->pPars->fVeryVerbose );
508  }
509  else
510  vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsCs, p->vVarsNs, 0, p->pPars->fVeryVerbose );
511  Llb_ImgSchedule( vSupps, &vQuant0, &vQuant1, p->pPars->fVeryVerbose );
512  Vec_VecFree( (Vec_Vec_t *)vSupps );
513  // remove variables
514  Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0, p->pPars->fVeryVerbose );
515  // perform reachability
516  RetValue = Llb_CoreReachability_int( p, vQuant0, vQuant1 );
517  Vec_VecFree( (Vec_Vec_t *)vQuant0 );
518  Vec_VecFree( (Vec_Vec_t *)vQuant1 );
519  return RetValue;
520 }
void Llb_ImgSchedule(Vec_Ptr_t *vSupps, Vec_Ptr_t **pvQuant0, Vec_Ptr_t **pvQuant1, int fVerbose)
Definition: llb2Image.c:122
static void Vec_PtrReverseOrder(Vec_Ptr_t *p)
Definition: vecPtr.h:785
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_Man_t * pAig
Definition: llb3Image.c:49
int Llb_CoreReachability_int(Llb_Img_t *p, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1)
Definition: llb2Core.c:207
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Llb_ImgQuantifyFirst(Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, Vec_Ptr_t *vQuant0, int fVerbose)
Definition: llb2Image.c:288
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Vec_Ptr_t * Llb_ImgSupports(Aig_Man_t *p, Vec_Ptr_t *vDdMans, Vec_Int_t *vStart, Vec_Int_t *vStop, int fAddPis, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: llb2Image.c:48
int Llb_CoreReachability_int ( Llb_Img_t p,
Vec_Ptr_t vQuant0,
Vec_Ptr_t vQuant1 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file llb2Core.c.

208 {
209  int * pLoc2Glo = p->pPars->fBackward? Vec_IntArray( p->vCs2Glo ) : Vec_IntArray( p->vNs2Glo );
210  int * pLoc2GloR = p->pPars->fBackward? Vec_IntArray( p->vNs2Glo ) : Vec_IntArray( p->vCs2Glo );
211  int * pGlo2Loc = p->pPars->fBackward? Vec_IntArray( p->vGlo2Ns ) : Vec_IntArray( p->vGlo2Cs );
212  DdNode * bCurrent, * bReached, * bNext, * bTemp;
213  abctime clk2, clk = Abc_Clock();
214  int nIters, nBddSize;//, iOutFail = -1;
215 /*
216  // compute time to stop
217  if ( p->pPars->TimeLimit )
218  p->pPars->TimeTarget = Abc_Clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
219  else
220  p->pPars->TimeTarget = 0;
221 */
222 
223  if ( Abc_Clock() > p->pPars->TimeTarget )
224  {
225  if ( !p->pPars->fSilent )
226  printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit );
227  p->pPars->iFrame = -1;
228  return -1;
229  }
230 
231  // set the stop time parameter
232  p->dd->TimeStop = p->pPars->TimeTarget;
233  p->ddG->TimeStop = p->pPars->TimeTarget;
234  p->ddR->TimeStop = p->pPars->TimeTarget;
235 
236  // compute initial states
237  if ( p->pPars->fBackward )
238  {
239  // create init state in the global manager
240  bTemp = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );
241  if ( bTemp == NULL )
242  {
243  if ( !p->pPars->fSilent )
244  printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
245  p->pPars->iFrame = -1;
246  return -1;
247  }
248  Cudd_Ref( bTemp );
249  // create bad state in the ring manager
250  p->ddR->bFunc = Llb_CoreComputeCube( p->ddR, p->vVarsCs, 0, NULL ); Cudd_Ref( p->ddR->bFunc );
251  bCurrent = Llb_BddQuantifyPis( p->pInit, p->ddR, bTemp ); Cudd_Ref( bCurrent );
252  Cudd_RecursiveDeref( p->ddR, bTemp );
253  bReached = Cudd_bddTransfer( p->ddR, p->ddG, bCurrent ); Cudd_Ref( bReached );
254  Cudd_RecursiveDeref( p->ddR, bCurrent );
255  // move init state to the working manager
256  bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Loc );
257  if ( bCurrent == NULL )
258  {
259  Cudd_RecursiveDeref( p->ddG, bReached );
260  if ( !p->pPars->fSilent )
261  printf( "Reached timeout (%d seconds) during transfer 0.\n", p->pPars->TimeLimit );
262  p->pPars->iFrame = -1;
263  return -1;
264  }
265  Cudd_Ref( bCurrent );
266  }
267  else
268  {
269  // create bad state in the ring manager
270  p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );
271  if ( p->ddR->bFunc == NULL )
272  {
273  if ( !p->pPars->fSilent )
274  printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
275  p->pPars->iFrame = -1;
276  return -1;
277  }
278  Cudd_Ref( p->ddR->bFunc );
279  // create init state in the working and global manager
280  bCurrent = Llb_CoreComputeCube( p->dd, p->vVarsCs, 1, NULL ); Cudd_Ref( bCurrent );
281  bReached = Llb_CoreComputeCube( p->ddG, p->vVarsCs, 0, NULL ); Cudd_Ref( bReached );
282 //Extra_bddPrint( p->dd, bCurrent ); printf( "\n" );
283 //Extra_bddPrint( p->ddG, bReached ); printf( "\n" );
284  }
285 
286  // compute onion rings
287  for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
288  {
289  clk2 = Abc_Clock();
290  // check the runtime limit
291  if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
292  {
293  if ( !p->pPars->fSilent )
294  printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
295  p->pPars->iFrame = nIters - 1;
296  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
297  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
298  return -1;
299  }
300 
301  // save the onion ring
302  bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pLoc2GloR );
303  if ( bTemp == NULL )
304  {
305  if ( !p->pPars->fSilent )
306  printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
307  p->pPars->iFrame = nIters - 1;
308  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
309  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
310  return -1;
311  }
312  Cudd_Ref( bTemp );
313  Vec_PtrPush( p->vRings, bTemp );
314 
315  // check it for bad states
316  if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
317  {
318  assert( p->pInit->pSeqModel == NULL );
319  if ( !p->pPars->fBackward )
320  p->pInit->pSeqModel = Llb_CoreDeriveCex( p );
321  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
322  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
323  if ( !p->pPars->fSilent )
324  {
325  if ( !p->pPars->fBackward )
326  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, p->pInit->pName, nIters );
327  else
328  Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
329  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
330  }
331  p->pPars->iFrame = nIters - 1;
332  return 0;
333  }
334 
335  // compute the next states
336  bNext = Llb_ImgComputeImage( p->pAig, p->vDdMans, p->dd, bCurrent,
337  vQuant0, vQuant1, p->vDriRefs, p->pPars->TimeTarget,
338  p->pPars->fBackward, p->pPars->fReorder, p->pPars->fVeryVerbose );
339  if ( bNext == NULL )
340  {
341  if ( !p->pPars->fSilent )
342  printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
343  p->pPars->iFrame = nIters - 1;
344  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
345  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
346  return -1;
347  }
348  Cudd_Ref( bNext );
349  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
350 //Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" );
351 
352  // remap these states into the global manager
353 // bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo ); Cudd_Ref( bNext );
354 // Cudd_RecursiveDeref( p->dd, bTemp );
355 
356 // bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pLoc2Glo, p->pPars->TimeTarget );
357  bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo );
358  if ( bNext == NULL )
359  {
360  if ( !p->pPars->fSilent )
361  printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
362  p->pPars->iFrame = nIters - 1;
363  Cudd_RecursiveDeref( p->dd, bTemp );
364  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
365  return -1;
366  }
367  Cudd_Ref( bNext );
368  Cudd_RecursiveDeref( p->dd, bTemp );
369 
370  nBddSize = Cudd_DagSize(bNext);
371  // check if there are any new states
372  if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states
373  {
374  Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
375  break;
376  }
377 
378  // get the new states
379  bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );
380  if ( bCurrent == NULL )
381  {
382  if ( !p->pPars->fSilent )
383  printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
384  p->pPars->iFrame = nIters - 1;
385  Cudd_RecursiveDeref( p->ddG, bNext );
386  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
387  return -1;
388  }
389  Cudd_Ref( bCurrent );
390 
391  // remap these states into the current state vars
392 // bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc ); Cudd_Ref( bCurrent );
393 // Cudd_RecursiveDeref( p->ddG, bTemp );
394 
395 // bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc, p->pPars->TimeTarget );
396  bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc );
397  if ( bCurrent == NULL )
398  {
399  if ( !p->pPars->fSilent )
400  printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
401  p->pPars->iFrame = nIters - 1;
402  Cudd_RecursiveDeref( p->ddG, bTemp );
403  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
404  return -1;
405  }
406  Cudd_Ref( bCurrent );
407  Cudd_RecursiveDeref( p->ddG, bTemp );
408 
409  // add to the reached states
410  bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext ); Cudd_Ref( bReached );
411  Cudd_RecursiveDeref( p->ddG, bTemp );
412  Cudd_RecursiveDeref( p->ddG, bNext );
413  bNext = NULL;
414 
415  if ( p->pPars->fVeryVerbose )
416  {
417  double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
418 // Extra_bddPrint( p->ddG, bReached );printf( "\n" );
419  fprintf( stdout, " Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
420  fflush( stdout );
421  }
422  if ( p->pPars->fVerbose )
423  {
424  fprintf( stdout, "F =%3d : ", nIters );
425  fprintf( stdout, "Image =%6d ", nBddSize );
426  fprintf( stdout, "(%4d%4d) ",
428  fprintf( stdout, "Reach =%6d ", Cudd_DagSize(bReached) );
429  fprintf( stdout, "(%4d%4d) ",
431  Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
432  }
433 
434  // check timeframe limit
435  if ( nIters == p->pPars->nIterMax - 1 )
436  {
437  if ( !p->pPars->fSilent )
438  printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax );
439  p->pPars->iFrame = nIters;
440  Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
441  Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
442  return -1;
443  }
444  }
445  if ( bReached == NULL )
446  {
447  p->pPars->iFrame = nIters - 1;
448  return 0; // reachable
449  }
450  if ( bCurrent )
451  Cudd_RecursiveDeref( p->dd, bCurrent );
452  // report the stats
453  if ( p->pPars->fVerbose )
454  {
455  double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
456  if ( nIters >= p->pPars->nIterMax )
457  fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
458  else
459  fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
460  fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
461  fflush( stdout );
462  }
463  if ( p->pPars->fDumpReached )
464  {
465  Llb_ManDumpReached( p->ddG, bReached, p->pAig->pName, "reached.blif" );
466  printf( "Reached states with %d BDD nodes are dumpted into file \"reached.blif\".\n", Cudd_DagSize(bReached) );
467  }
468  Cudd_RecursiveDeref( p->ddG, bReached );
469  if ( nIters >= p->pPars->nIterMax )
470  {
471  if ( !p->pPars->fSilent )
472  {
473  printf( "Verified only for states reachable in %d frames. ", nIters );
474  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
475  }
476  p->pPars->iFrame = p->pPars->nIterMax;
477  return -1; // undecided
478  }
479  if ( !p->pPars->fSilent )
480  {
481  printf( "The miter is proved unreachable after %d iterations. ", nIters );
482  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
483  }
484  p->pPars->iFrame = nIters - 1;
485  return 1; // unreachable
486 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
DdManager * dd
Definition: llb3Image.c:52
Aig_Man_t * pAig
Definition: llb3Image.c:49
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Definition: cuddUtil.c:578
abctime TimeStop
Definition: cuddInt.h:489
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Cudd_ReadReorderings(DdManager *dd)
Definition: cuddAPI.c:1696
ABC_NAMESPACE_IMPL_START DdNode * Llb_BddComputeBad(Aig_Man_t *pInit, DdManager *dd, abctime TimeOut)
DECLARATIONS ///.
Definition: llb2Bad.c:45
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
Definition: extraBddMisc.c:87
DdNode * Llb_ImgComputeImage(Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, DdManager *dd, DdNode *bInit, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1, Vec_Int_t *vDriRefs, abctime TimeTarget, int fBackward, int fReorder, int fVerbose)
Definition: llb2Image.c:364
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static abctime Abc_Clock()
Definition: abc_global.h:279
DdNode * Cudd_bddTransfer(DdManager *ddSource, DdManager *ddDestination, DdNode *f)
Definition: cuddBridge.c:409
DdNode * Llb_BddQuantifyPis(Aig_Man_t *pInit, DdManager *dd, DdNode *bFunc)
Definition: llb2Bad.c:109
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
DdNode * Llb_CoreComputeCube(DdManager *dd, Vec_Int_t *vVars, int fUseVarIndex, char *pValues)
FUNCTION DEFINITIONS ///.
Definition: llb2Core.c:68
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
void Llb_ManDumpReached(DdManager *ddG, DdNode *bReached, char *pModel, char *pFileName)
Definition: llb2Dump.c:63
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Abc_Cex_t * Llb_CoreDeriveCex(Llb_Img_t *p)
Definition: llb2Core.c:98
#define assert(ex)
Definition: util_old.h:213
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
ABC_INT64_T abctime
Definition: abc_global.h:278
int Cudd_ReadGarbageCollections(DdManager *dd)
Definition: cuddAPI.c:1741
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
void Llb_CoreSetVarMaps ( Llb_Img_t p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 577 of file llb2Core.c.

578 {
579  Aig_Obj_t * pObj;
580  int i, iVarCs, iVarNs;
581  assert( p->vVarsCs != NULL );
582  assert( p->vVarsNs != NULL );
583  assert( p->vCs2Glo == NULL );
584  assert( p->vNs2Glo == NULL );
585  assert( p->vGlo2Cs == NULL );
586  assert( p->vGlo2Ns == NULL );
587  p->vCs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
588  p->vNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
589  p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
590  p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
591  for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
592  {
593  iVarCs = Vec_IntEntry( p->vVarsCs, i );
594  iVarNs = Vec_IntEntry( p->vVarsNs, i );
595  assert( iVarCs >= 0 && iVarCs < Aig_ManObjNumMax(p->pAig) );
596  assert( iVarNs >= 0 && iVarNs < Aig_ManObjNumMax(p->pAig) );
597  Vec_IntWriteEntry( p->vCs2Glo, iVarCs, i );
598  Vec_IntWriteEntry( p->vNs2Glo, iVarNs, i );
599  Vec_IntWriteEntry( p->vGlo2Cs, i, iVarCs );
600  Vec_IntWriteEntry( p->vGlo2Ns, i, iVarNs );
601  }
602  // add mapping of the PIs
603  Saig_ManForEachPi( p->pAig, pObj, i )
604  Vec_IntWriteEntry( p->vCs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
605 }
Aig_Man_t * pAig
Definition: llb3Image.c:49
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Definition: aig.h:69
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
Llb_Img_t* Llb_CoreStart ( Aig_Man_t pInit,
Aig_Man_t pAig,
Gia_ParLlb_t pPars 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 618 of file llb2Core.c.

619 {
620  Llb_Img_t * p;
621  p = ABC_CALLOC( Llb_Img_t, 1 );
622  p->pInit = pInit;
623  p->pAig = pAig;
624  p->pPars = pPars;
626  p->ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
627  p->ddR = Cudd_Init( Aig_ManCiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
631  p->vRings = Vec_PtrAlloc( 100 );
632  p->vDriRefs = Llb_DriverCountRefs( pAig );
633  p->vVarsCs = Llb_DriverCollectCs( pAig );
634  p->vVarsNs = Llb_DriverCollectNs( pAig, p->vDriRefs );
635  Llb_CoreSetVarMaps( p );
636  return p;
637 }
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
typedefABC_NAMESPACE_IMPL_START struct Llb_Img_t_ Llb_Img_t
DECLARATIONS ///.
Definition: llb2Core.c:30
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
ABC_NAMESPACE_IMPL_START Vec_Int_t * Llb_DriverCountRefs(Aig_Man_t *p)
DECLARATIONS ///.
Definition: llb2Driver.c:56
Vec_Int_t * Llb_DriverCollectNs(Aig_Man_t *pAig, Vec_Int_t *vDriRefs)
Definition: llb2Driver.c:78
Vec_Int_t * Llb_DriverCollectCs(Aig_Man_t *pAig)
Definition: llb2Driver.c:106
void Llb_CoreSetVarMaps(Llb_Img_t *p)
Definition: llb2Core.c:577
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
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
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
void Llb_CoreStop ( Llb_Img_t p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 650 of file llb2Core.c.

651 {
652  DdManager * dd;
653  DdNode * bTemp;
654  int i;
655  if ( p->vDdMans )
656  Vec_PtrForEachEntry( DdManager *, p->vDdMans, dd, i )
657  {
658  if ( dd->bFunc )
659  Cudd_RecursiveDeref( dd, dd->bFunc );
660  if ( dd->bFunc2 )
661  Cudd_RecursiveDeref( dd, dd->bFunc2 );
662  Extra_StopManager( dd );
663  }
664  Vec_PtrFreeP( &p->vDdMans );
665  if ( p->ddR->bFunc )
666  Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
667  Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
668  Cudd_RecursiveDeref( p->ddR, bTemp );
669  Vec_PtrFree( p->vRings );
670  Extra_StopManager( p->dd );
671  Extra_StopManager( p->ddG );
672  Extra_StopManager( p->ddR );
673  Vec_IntFreeP( &p->vDriRefs );
674  Vec_IntFreeP( &p->vVarsCs );
675  Vec_IntFreeP( &p->vVarsNs );
676  Vec_IntFreeP( &p->vCs2Glo );
677  Vec_IntFreeP( &p->vNs2Glo );
678  Vec_IntFreeP( &p->vGlo2Cs );
679  Vec_IntFreeP( &p->vGlo2Ns );
680  ABC_FREE( p );
681 }
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
static Llb_Mgr_t * p
Definition: llb3Image.c:950
DdNode * bFunc
Definition: cuddInt.h:487
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
DdNode * bFunc2
Definition: cuddInt.h:488
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
#define ABC_FREE(obj)
Definition: abc_global.h:232
static void Vec_PtrFreeP(Vec_Ptr_t **p)
Definition: vecPtr.h:240
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
int Llb_ManReachMinCut ( Aig_Man_t pAig,
Gia_ParLlb_t pPars 
)

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

Synopsis [Finds balanced cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 725 of file llb2Core.c.

726 {
727  extern Vec_Ptr_t * Llb_ManComputeCuts( Aig_Man_t * p, int Num, int fVerbose, int fVeryVerbose );
728  Vec_Ptr_t * vResult;
729  Aig_Man_t * p;
730  int RetValue = -1;
731  abctime clk = Abc_Clock();
732 
733  // compute time to stop
734  pPars->TimeTarget = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
735 
736  p = Aig_ManDupFlopsOnly( pAig );
737 //Aig_ManShow( p, 0, NULL );
738  if ( pPars->fVerbose )
739  Aig_ManPrintStats( pAig );
740  if ( pPars->fVerbose )
741  Aig_ManPrintStats( p );
742  Aig_ManFanoutStart( p );
743 
744  vResult = Llb_ManComputeCuts( p, pPars->nPartValue, pPars->fVerbose, pPars->fVeryVerbose );
745 
746  if ( pPars->TimeLimit && Abc_Clock() > pPars->TimeTarget )
747  {
748  if ( !pPars->fSilent )
749  printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit );
750 
751  Vec_VecFree( (Vec_Vec_t *)vResult );
752  Aig_ManFanoutStop( p );
753  Aig_ManCleanMarkAB( p );
754  Aig_ManStop( p );
755  return RetValue;
756  }
757 
758  if ( !pPars->fSkipReach )
759  RetValue = Llb_CoreExperiment( pAig, p, pPars, vResult, pPars->TimeTarget );
760 
761  Vec_VecFree( (Vec_Vec_t *)vResult );
762  Aig_ManFanoutStop( p );
763  Aig_ManCleanMarkAB( p );
764  Aig_ManStop( p );
765 
766  if ( RetValue == -1 )
767  Abc_PrintTime( 1, "Total runtime of the min-cut-based reachability engine", Abc_Clock() - clk );
768  return RetValue;
769 }
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
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
Vec_Ptr_t * Llb_ManComputeCuts(Aig_Man_t *p, int Num, int fVerbose, int fVeryVerbose)
Definition: llb2Flow.c:1226
static abctime Abc_Clock()
Definition: abc_global.h:279
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
void Aig_ManFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: aigFanout.c:56
void Aig_ManFanoutStop(Aig_Man_t *p)
Definition: aigFanout.c:89
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Aig_Man_t * Aig_ManDupFlopsOnly(Aig_Man_t *p)
Definition: aigDup.c:871
int Llb_CoreExperiment(Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars, Vec_Ptr_t *vResult, abctime TimeTarget)
Definition: llb2Core.c:694
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition: aigUtil.c:186
ABC_INT64_T abctime
Definition: abc_global.h:278