abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcDarUnfold2.c
Go to the documentation of this file.
1 /**Function*************************************************************
2 
3  Synopsis [Performs BDD-based reachability analysis.]
4 
5  Description []
6 
7  SideEffects []
8 
9  SeeAlso []
10 
11 ***********************************************************************/
12 Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int);
13 Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
14 {
15  Abc_Ntk_t * pNtkAig;
16  Aig_Man_t * pMan, * pTemp;
17  int typeII_cnt = 0;
18  assert( Abc_NtkIsStrash(pNtk) );
19  pMan = Abc_NtkToDar( pNtk, 0, 1 );
20  if ( pMan == NULL )
21  return NULL;
22  if ( fStruct ){
23  assert(0);//pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
24  }else
25  pMan = Saig_ManDupUnfoldConstrsFunc2( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose , &typeII_cnt);
26  Aig_ManStop( pTemp );
27  if ( pMan == NULL )
28  return NULL;
29  // typeII_cnt = pMan->nConstrsTypeII;
30  pNtkAig = Abc_NtkFromAigPhase( pMan );
31  pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
32  pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
33  Aig_ManStop( pMan );
34 
35  return pNtkAig;//Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt);
36 
37  //return pNtkAig;
38 }
39 
40 /**Function*************************************************************
41 
42  Synopsis [Performs BDD-based reachability analysis.]
43 
44  Description []
45 
46  SideEffects []
47 
48  SeeAlso []
49 
50 ***********************************************************************/
51 Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose
52  , int typeII_cnt
53  )
54 {
55  Abc_Ntk_t * pNtkAig;
56  Aig_Man_t * pMan, * pTemp;
57  assert( Abc_NtkIsStrash(pNtk) );
58  pMan = Abc_NtkToDar( pNtk, 0, 1 );
59  if ( pMan == NULL )
60  return NULL;
61  pMan = Saig_ManDupFoldConstrsFunc2( pTemp = pMan, fCompl, fVerbose, typeII_cnt );
62  Aig_ManStop( pTemp );
63  pNtkAig = Abc_NtkFromAigPhase( pMan );
64  pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
65  pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
66  Aig_ManStop( pMan );
67  return pNtkAig;
68 }
69 
Abc_NtkIsStrash
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Abc_Ntk_t_
Definition: abc.h:153
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition: extraUtilUtil.c:169
Saig_ManDupFoldConstrsFunc2
Aig_Man_t * Saig_ManDupFoldConstrsFunc2(Aig_Man_t *pAig, int fCompl, int fVerbose, int typeII_cnt)
Definition: saigUnfold2.c:375
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
Definition: abcDar.c:233
Saig_ManDupUnfoldConstrsFunc2
Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2(Aig_Man_t *pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose, int *typeII_cnt)
Definition: saigUnfold2.c:295
Abc_NtkFromAigPhase
Abc_Ntk_t * Abc_NtkFromAigPhase(Aig_Man_t *pMan)
Definition: abcDar.c:590
Abc_Ntk_t_::pSpec
char * pSpec
Definition: abc.h:159
Abc_NtkDarFold2
Abc_Ntk_t * Abc_NtkDarFold2(Abc_Ntk_t *pNtk, int fCompl, int fVerbose, int)
Definition: abcDarUnfold2.c:51
assert
#define assert(ex)
Definition: util_old.h:213
Abc_NtkDarUnfold2
Abc_Ntk_t * Abc_NtkDarUnfold2(Abc_Ntk_t *pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose)
Definition: abcDarUnfold2.c:13
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158