summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/aig/aig.h5
-rw-r--r--src/aig/aig/aigDup.c66
-rw-r--r--src/aig/aig/aigMan.c23
-rw-r--r--src/aig/aig/aigObj.c40
-rw-r--r--src/aig/aig/aigPart.c8
-rw-r--r--src/aig/saig/module.make1
-rw-r--r--src/aig/saig/saigHaig.c733
-rw-r--r--src/base/abc/abc.h1
-rw-r--r--src/base/abc/abcAig.c9
-rw-r--r--src/base/abc/abcNtk.c3
-rw-r--r--src/base/abci/abcBalance.c3
-rw-r--r--src/base/abci/abcHaig.c181
-rw-r--r--src/base/abci/abcPart.c1
-rw-r--r--src/base/abci/module.make2
-rw-r--r--src/opt/dar/darBalance.c23
-rw-r--r--src/opt/dar/darScript.c35
-rw-r--r--src/proof/fra/fraLcr.c1
17 files changed, 2 insertions, 1133 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 3e682391..9953cf6a 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -66,7 +66,7 @@ typedef enum {
} Aig_Type_t;
// the AIG node
-struct Aig_Obj_t_ // 9 words
+struct Aig_Obj_t_ // 8 words
{
union {
Aig_Obj_t * pNext; // strashing table
@@ -74,7 +74,6 @@ struct Aig_Obj_t_ // 9 words
};
Aig_Obj_t * pFanin0; // fanin
Aig_Obj_t * pFanin1; // fanin
- Aig_Obj_t * pHaig; // pointer to the HAIG node
unsigned int Type : 3; // object type
unsigned int fPhase : 1; // value under 000...0 pattern
unsigned int fMarkA : 1; // multipurpose mask
@@ -156,7 +155,6 @@ struct Aig_Man_t_
Vec_Ptr_t * vSeqModelVec; // vector of counter-examples (for sequential miters)
Aig_Man_t * pManExdc;
Vec_Ptr_t * vOnehots;
- Aig_Man_t * pManHaig;
int fCreatePios;
Vec_Int_t * vEquPairs;
Vec_Vec_t * vClockDoms;
@@ -326,7 +324,6 @@ static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) {
static inline void Aig_ObjSetEquiv( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pEqu ) { assert(p->pEquivs); p->pEquivs[pObj->Id] = pEqu; }
static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pReprs? p->pReprs[pObj->Id] : NULL; }
static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) { assert(p->pReprs); p->pReprs[pObj->Id] = pRepr; }
-static inline Aig_Obj_t * Aig_ObjHaig( Aig_Obj_t * pObj ) { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); }
static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )
{
if ( Aig_ObjFanin0(pObj) == pFanin ) return 0;
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 9d87db92..67b71d61 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -49,7 +49,6 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
Aig_Obj_t * pObj, * pObjNew;
int i;
assert( p->pManTime == NULL );
- assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
@@ -61,11 +60,9 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachCi( p, pObj, i )
{
pObjNew = Aig_ObjCreateCi( pNew );
- pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
}
@@ -74,30 +71,21 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
if ( Aig_ObjIsBuf(pObj) )
{
pObjNew = Aig_ObjChild0Copy(pObj);
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
// add the POs
Aig_ManForEachCo( p, pObj, i )
{
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
- pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
- // pass the HAIG manager
- if ( p->pManHaig != NULL )
- {
- pNew->pManHaig = p->pManHaig;
- p->pManHaig = NULL;
- }
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupSimple(): The check has failed.\n" );
@@ -120,7 +108,6 @@ Aig_Man_t * Aig_ManDupSimpleWithHints( Aig_Man_t * p, Vec_Int_t * vHints )
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i, Entry;
- assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
assert( p->nAsserts == 0 || p->nConstrs == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
@@ -175,7 +162,6 @@ Aig_Obj_t * Aig_ManDupSimpleDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- Aig_Regular((Aig_Obj_t *)pObj->pData)->pHaig = pObj->pHaig;
return (Aig_Obj_t *)pObj->pData;
}
@@ -200,7 +186,6 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
Aig_Obj_t * pObj, * pObjNew;
int i;
assert( p->pManTime == NULL );
- assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
@@ -212,11 +197,9 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachCi( p, pObj, i )
{
pObjNew = Aig_ObjCreateCi( pNew );
- pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
}
@@ -231,17 +214,10 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
Aig_ManForEachCo( p, pObj, i )
{
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
- pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
- // pass the HAIG manager
- if ( p->pManHaig != NULL )
- {
- pNew->pManHaig = p->pManHaig;
- p->pManHaig = NULL;
- }
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupSimple(): The check has failed.\n" );
@@ -337,7 +313,6 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
}
else
assert( 0 );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
@@ -347,12 +322,6 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
- // pass the HAIG manager
- if ( p->pManHaig != NULL )
- {
- pNew->pManHaig = p->pManHaig;
- p->pManHaig = NULL;
- }
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupOrdered(): The check has failed.\n" );
@@ -376,7 +345,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
Aig_Obj_t * pObj, * pObjNew;
int i;
assert( p->pManTime == NULL );
- assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
@@ -388,7 +356,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachCi( p, pObj, i )
{
if ( i == iInput )
@@ -396,7 +363,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
else
{
pObjNew = Aig_ObjCreateCi( pNew );
- pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
}
pObj->pData = pObjNew;
@@ -406,31 +372,22 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
if ( Aig_ObjIsBuf(pObj) )
{
pObjNew = Aig_ObjChild0Copy(pObj);
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
// add the POs
Aig_ManForEachCo( p, pObj, i )
{
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
- pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
// assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
Aig_ManCleanup( pNew );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
- // pass the HAIG manager
- if ( p->pManHaig != NULL )
- {
- pNew->pManHaig = p->pManHaig;
- p->pManHaig = NULL;
- }
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupSimple(): The check has failed.\n" );
@@ -539,7 +496,6 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
}
else
assert( 0 );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
Aig_ManCleanup( pNew );
@@ -576,10 +532,6 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- if ( p->pManHaig != NULL )
- Aig_Regular(pObjNew)->pHaig = Aig_NotCond( pObj->pHaig, Aig_IsComplement(pObjNew) );
- else if ( pObj->pHaig )
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
if ( pEquivNew )
{
assert( Aig_Regular(pEquivNew)->Id < Aig_Regular(pObjNew)->Id );
@@ -624,14 +576,12 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
Aig_ManCleanData( p );
// duplicate internal nodes
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjIsCi(pObj) )
{
pObjNew = Aig_ObjCreateCi( pNew );
pObjNew->Level = pObj->Level;
- pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsCo(pObj) )
@@ -639,7 +589,6 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
// assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
- pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
}
@@ -650,12 +599,6 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
- // pass the HAIG manager
- if ( p->pManHaig != NULL )
- {
- pNew->pManHaig = p->pManHaig;
- p->pManHaig = NULL;
- }
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupDfs(): The check has failed.\n" );
@@ -720,8 +663,6 @@ Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
if ( !Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin1(pObj) ) )
return NULL;
pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- if ( pObj->pHaig )
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
if ( pEquivNew )
{
if ( pNew->pEquivs )
@@ -771,14 +712,12 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
Aig_ManCleanData( p );
// duplicate internal nodes
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Vec_PtrForEachEntry( Aig_Obj_t *, vPios, pObj, i )
{
if ( Aig_ObjIsCi(pObj) )
{
pObjNew = Aig_ObjCreateCi( pNew );
pObjNew->Level = pObj->Level;
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsCo(pObj) )
@@ -786,7 +725,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) );
// assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
}
@@ -841,11 +779,9 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
}
// create the PIs
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachCi( p, pObj, i )
{
pObjNew = Aig_ObjCreateCi( pNew );
- pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
}
@@ -854,7 +790,6 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
Vec_VecForEachEntry( Aig_Obj_t *, vLevels, pObj, i, k )
{
pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
Vec_VecFree( vLevels );
@@ -862,7 +797,6 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
Aig_ManForEachCo( p, pObj, i )
{
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
- pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 6a0555a0..230a2b18 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -100,7 +100,6 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
{
pObjNew = Aig_ObjCreateCi( pNew );
pObjNew->Level = pObj->Level;
- pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
return pNew;
@@ -127,7 +126,6 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
return (Aig_Obj_t *)(pObj->pData = pObjNew);
}
@@ -361,27 +359,6 @@ int Aig_ManCoCleanup( Aig_Man_t * p )
/**Function*************************************************************
- Synopsis [Performs one iteration of AIG rewriting.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManHaigCounter( Aig_Man_t * pAig )
-{
- Aig_Obj_t * pObj;
- int Counter, i;
- Counter = 0;
- Aig_ManForEachNode( pAig, pObj, i )
- Counter += (pObj->pHaig != NULL);
- return Counter;
-}
-
-/**Function*************************************************************
-
Synopsis [Stops the AIG manager.]
Description []
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 41a07823..e1eab364 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -49,12 +49,6 @@ Aig_Obj_t * Aig_ObjCreateCi( Aig_Man_t * p )
pObj->Type = AIG_OBJ_CI;
Vec_PtrPush( p->vCis, pObj );
p->nObjs[AIG_OBJ_CI]++;
- if ( p->pManHaig && p->fCreatePios )
- {
- p->pManHaig->nRegs++;
- pObj->pHaig = Aig_ObjCreateCi( p->pManHaig );
-// printf( "Creating PI HAIG node %d equivalent to PI %d.\n", pObj->pHaig->Id, pObj->Id );
- }
return pObj;
}
@@ -77,11 +71,6 @@ Aig_Obj_t * Aig_ObjCreateCo( Aig_Man_t * p, Aig_Obj_t * pDriver )
Vec_PtrPush( p->vCos, pObj );
Aig_ObjConnect( p, pObj, pDriver, NULL );
p->nObjs[AIG_OBJ_CO]++;
- if ( p->pManHaig && p->fCreatePios )
- {
- pObj->pHaig = Aig_ObjCreateCo( p->pManHaig, Aig_ObjHaig( pDriver ) );
-// printf( "Creating PO HAIG node %d equivalent to PO %d.\n", pObj->pHaig->Id, pObj->Id );
- }
return pObj;
}
@@ -111,14 +100,6 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
// update node counters of the manager
p->nObjs[Aig_ObjType(pObj)]++;
assert( pObj->pData == NULL );
- if ( p->pManHaig )
- {
- pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 );
- pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 );
- pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost );
- assert( !Aig_IsComplement(pObj->pHaig) );
-// printf( "Creating HAIG node %d equivalent to node %d.\n", pObj->pHaig->Id, pObj->Id );
- }
// create the power counter
if ( p->vProbs )
{
@@ -384,14 +365,6 @@ void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
}
return;
}
- if ( fHaig )
- {
- if ( pObj->pHaig == NULL )
- printf( " HAIG node not given" );
- else
- printf( " HAIG node = %d%s", Aig_Regular(pObj->pHaig)->Id, (Aig_IsComplement(pObj->pHaig)? "\'" : " ") );
- return;
- }
// there are choices
if ( p->pEquivs && p->pEquivs[pObj->Id] )
{
@@ -511,19 +484,6 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
printf( "Aig_ObjReplace(): Internal error!\n" );
exit(1);
}
- // map the HAIG nodes
- if ( p->pManHaig != NULL )
- {
-// printf( "Setting HAIG node %d equivalent to HAIG node %d (over = %d).\n",
-// pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
- assert( pObjNewR->pHaig != NULL );
- assert( !Aig_IsComplement(pObjNewR->pHaig) );
- assert( p->pManHaig->vEquPairs != NULL );
- Vec_IntPush( p->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
- Vec_IntPush( p->pManHaig->vEquPairs, pObjOld->pHaig->Id );
- }
- else
- pObjOld->pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;
// recursively delete the old node - but leave the object there
pObjNewR->nRefs++;
Aig_ObjDelete_rec( p, pObjOld, 0 );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index d2d92b82..717f3192 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1493,8 +1493,6 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
// make sure the nodes of pThis point to pPrev
Aig_ManForEachObj( pPrev, pObj, i )
pObj->fMarkB = 1;
- Aig_ManForEachObj( pThis, pObj, i )
- assert( pObj->pHaig == NULL || (!Aig_IsComplement(pObj->pHaig) && pObj->pHaig->fMarkB) );
Aig_ManForEachObj( pPrev, pObj, i )
pObj->fMarkB = 0;
// remap nodes of pThis on top of pNew using pPrev
@@ -1506,13 +1504,7 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
pObj->pData = Aig_ManCo(pNew, i);
// go through the nodes in the topological order
Aig_ManForEachNode( pThis, pObj, i )
- {
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- if ( pObj->pHaig == NULL )
- continue;
- // pObj->pData and pObj->pHaig->pData are equivalent
- Aig_ObjSetRepr_( pNew, Aig_Regular((Aig_Obj_t *)pObj->pData), Aig_Regular((Aig_Obj_t *)pObj->pHaig->pData) );
- }
// set the inputs of POs as equivalent
Aig_ManForEachCo( pThis, pObj, i )
{
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index edf5798e..a3231929 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -7,7 +7,6 @@ SRC += src/aig/saig/saigBmc.c \
src/aig/saig/saigConstr2.c \
src/aig/saig/saigDual.c \
src/aig/saig/saigDup.c \
- src/aig/saig/saigHaig.c \
src/aig/saig/saigInd.c \
src/aig/saig/saigIoa.c \
src/aig/saig/saigIso.c \
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
deleted file mode 100644
index 7cb34c5d..00000000
--- a/src/aig/saig/saigHaig.c
+++ /dev/null
@@ -1,733 +0,0 @@
-/**CFile****************************************************************
-
- FileName [saigHaig.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Sequential AIG package.]
-
- Synopsis [Experiments with history AIG recording.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - April 28, 2007.]
-
- Revision [$Id: saigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-#include "sat/bsat/satSolver.h"
-#include "sat/cnf/cnf.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Prepares the inductive case with speculative reduction.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;//, * pMiter;
- Aig_Obj_t * pPo;
- // skip nodes without representative
- pObjRepr = pObj->pHaig;
- if ( pObjRepr == NULL )
- return;
-// assert( pObjRepr->Id < pObj->Id );
- // get the new node
- pObjNew = (Aig_Obj_t *)pObj->pData;
- // get the new node of the representative
- pObjReprNew = (Aig_Obj_t *)pObjRepr->pData;
- // if this is the same node, no need to add constraints
- assert( pObjNew != NULL && pObjReprNew != NULL );
- if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
- return;
- // these are different nodes - perform speculative reduction
- pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
- // set the new node
- pObj->pData = pObjNew2;
- // add the constraint
- if ( pObj->fMarkA )
- return;
-// pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
-// pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
-// assert( Aig_ObjPhaseReal(pMiter) == 1 );
-// Aig_ObjCreateCo( pFrames, pMiter );
- if ( Aig_ObjPhaseReal(pObjNew) != Aig_ObjPhaseReal(pObjReprNew) )
- pObjReprNew = Aig_Not(pObjReprNew);
- pPo = Aig_ObjCreateCo( pFrames, pObjNew );
- Aig_ObjCreateCo( pFrames, pObjReprNew );
-
- // remember the node corresponding to this PO
- pPo->pData = pObj;
-}
-
-/**Function*************************************************************
-
- Synopsis [Prepares the inductive case with speculative reduction.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
-{
- Aig_Man_t * pFrames;
- Aig_Obj_t * pObj, * pObjLi, * pObjLo;
- int i, f, nAssumptions = 0;
- assert( nFrames == 1 || nFrames == 2 );
- assert( nFrames == 1 || Saig_ManRegNum(pHaig) > 0 );
- // start AIG manager for timeframes
- pFrames = Aig_ManStart( Aig_ManNodeNum(pHaig) * nFrames );
- pFrames->pName = Abc_UtilStrsav( pHaig->pName );
- pFrames->pSpec = Abc_UtilStrsav( pHaig->pSpec );
- // map the constant node
- Aig_ManConst1(pHaig)->pData = Aig_ManConst1( pFrames );
- // create variables for register outputs
- Saig_ManForEachLo( pHaig, pObj, i )
- pObj->pData = Aig_ObjCreateCi( pFrames );
- // add timeframes
- Aig_ManSetCioIds( pHaig );
- for ( f = 0; f < nFrames; f++ )
- {
- // create primary inputs
- Saig_ManForEachPi( pHaig, pObj, i )
- pObj->pData = Aig_ObjCreateCi( pFrames );
- // create internal nodes
- Aig_ManForEachNode( pHaig, pObj, i )
- {
- pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- Aig_ManHaigSpeculate( pFrames, pObj );
- }
- if ( f == nFrames - 2 )
- nAssumptions = Aig_ManCoNum(pFrames);
- if ( f == nFrames - 1 )
- break;
- // save register inputs
- Saig_ManForEachLi( pHaig, pObj, i )
- pObj->pData = Aig_ObjChild0Copy(pObj);
- // transfer to register outputs
- Saig_ManForEachLiLo( pHaig, pObjLi, pObjLo, i )
- pObjLo->pData = pObjLi->pData;
- }
- Aig_ManCleanup( pFrames );
- pFrames->nAsserts = Aig_ManCoNum(pFrames) - nAssumptions;
- Aig_ManSetRegNum( pFrames, 0 );
- return pFrames;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
-{
- Aig_Obj_t * pObj1, * pObj2;
- int Id1, Id2, i, Counter = 0;
- Aig_ManForEachObj( pHaig, pObj1, i )
- pObj1->pHaig = NULL;
- Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
- {
- Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
- pObj1 = Aig_ManObj( pHaig, Id1 );
- pObj2 = Aig_ManObj( pHaig, Id2 );
- assert( pObj1 != pObj2 );
- assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) );
- if ( Aig_ObjIsCi(pObj1) )
- {
- Counter += (int)(pObj2->pHaig != NULL);
- pObj2->pHaig = pObj1;
- }
- else if ( Aig_ObjIsCi(pObj2) )
- {
- Counter += (int)(pObj1->pHaig != NULL);
- pObj1->pHaig = pObj2;
- }
- else if ( pObj1->Id < pObj2->Id )
- {
- Counter += (int)(pObj2->pHaig != NULL);
- pObj2->pHaig = pObj1;
- }
- else
- {
- Counter += (int)(pObj1->pHaig != NULL);
- pObj1->pHaig = pObj2;
- }
- }
-// printf( "Overwrites %d out of %d.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, clock_t clkSynth )
-{
- int nBTLimit = 0;
- Aig_Man_t * pFrames, * pTemp;
- Cnf_Dat_t * pCnf;
- sat_solver * pSat;
- Aig_Obj_t * pObj1, * pObj2;
- int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
- clock_t clk = clock(), clkVerif;
-
- nOvers = Aig_ManMapHaigNodes( pHaig );
-
- // create time frames with speculative reduction and convert them into CNF
-clk = clock();
- pFrames = Aig_ManHaigFrames( pHaig, nFrames );
- Aig_ManCleanMarkA( pHaig );
-
- printf( "Frames: " );
- Aig_ManPrintStats( pFrames );
-
- pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
- Aig_ManStop( pTemp );
-
- printf( "Frames synt:" );
- Aig_ManPrintStats( pFrames );
-
- printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n",
- Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
-// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
- pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) );
-
-
-
-// pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) - pFrames->nAsserts );
-//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
-// Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
-// Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
- // create the SAT solver to be used for this problem
- pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
- if ( pSat == NULL )
- {
- printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
- return 0;
- }
-
- if ( nFrames == 2 )
- {
- // add clauses for the first frame
- Aig_ManForEachCo( pFrames, pObj1, i )
- {
- if ( i >= Aig_ManCoNum(pFrames) - pFrames->nAsserts )
- break;
-
- pObj2 = Aig_ManCo( pFrames, ++i );
- assert( pObj1->fPhase == pObj2->fPhase );
-
- Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
- Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
- if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
- {
- sat_solver_delete( pSat );
- return 0;
- }
- Lits[0]++;
- Lits[1]--;
- if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
- {
- sat_solver_delete( pSat );
- return 0;
- }
- }
-
- if ( !sat_solver_simplify(pSat) )
- {
- sat_solver_delete( pSat );
- return 0;
- }
- }
-ABC_PRT( "Preparation", clock() - clk );
-
-
- // check in the second timeframe
-clk = clock();
- Counter = 0;
- printf( "Started solving ...\r" );
- Aig_ManForEachCo( pFrames, pObj1, i )
- {
- if ( i < Aig_ManCoNum(pFrames) - pFrames->nAsserts )
- continue;
-
- pObj2 = Aig_ManCo( pFrames, ++i );
- assert( pObj1->fPhase == pObj2->fPhase );
-
- Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
- Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
-
- RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
- if ( RetValue1 == l_False )
- {
- Lits[0] = lit_neg( Lits[0] );
- Lits[1] = lit_neg( Lits[1] );
-// RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
-// assert( RetValue );
- }
-
- Lits[0]++;
- Lits[1]--;
-
- RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
- if ( RetValue2 == l_False )
- {
- Lits[0] = lit_neg( Lits[0] );
- Lits[1] = lit_neg( Lits[1] );
-// RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
-// assert( RetValue );
- }
-
- if ( RetValue1 != l_False || RetValue2 != l_False )
- Counter++;
-
- if ( i % 50 == 1 )
- printf( "Solving assertion %6d out of %6d.\r",
- (i - (Aig_ManCoNum(pFrames) - pFrames->nAsserts))/2,
- pFrames->nAsserts/2 );
-// if ( nClasses == 1000 )
-// break;
- }
- printf( " \r" );
-ABC_PRT( "Solving ", clock() - clk );
-clkVerif = clock() - clk;
- if ( Counter )
- printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
- else
- printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
-
- // print the statistic into a file
- {
- FILE * pTable;
- Aig_Man_t * pTemp, * pHaig2;
-
- pHaig2 = pAig->pManHaig;
- pAig->pManHaig = NULL;
- pTemp = Aig_ManDupDfs( pAig );
- pAig->pManHaig = pHaig2;
-
- Aig_ManSeqCleanup( pTemp );
-
- pTable = fopen( "stats.txt", "a+" );
- fprintf( pTable, "%s ", p->pName );
- fprintf( pTable, "%d ", Saig_ManPiNum(p) );
- fprintf( pTable, "%d ", Saig_ManPoNum(p) );
-
- fprintf( pTable, "%d ", Saig_ManRegNum(p) );
- fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
- fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
-
- fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
- fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
- fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
-
- fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
- fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
- fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
-
- fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) );
- fprintf( pTable, "\n" );
- fclose( pTable );
-
-
- pTable = fopen( "stats2.txt", "a+" );
- fprintf( pTable, "%s ", p->pName );
- fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
- fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
-
- fprintf( pTable, "%d ", pCnf->nVars );
- fprintf( pTable, "%d ", pCnf->nClauses );
- fprintf( pTable, "%d ", pCnf->nLiterals );
-
- fprintf( pTable, "%d ", Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2 );
- fprintf( pTable, "%d ", pFrames->nAsserts/2 );
- fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
-
- fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) );
- fprintf( pTable, "\n" );
- fclose( pTable );
-
- Aig_ManStop( pTemp );
- }
-
- // clean up
- Aig_ManStop( pFrames );
- Cnf_DataFree( pCnf );
- sat_solver_delete( pSat );
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
-{
- int nBTLimit = 0;
- Cnf_Dat_t * pCnf;
- sat_solver * pSat;
- Aig_Obj_t * pObj1, * pObj2;
- int i, RetValue1, RetValue2, Counter, Lits[2];
- clock_t clk = clock();
- int Delta;
- int Id1, Id2;
-
- assert( nFrames == 1 || nFrames == 2 );
-
-clk = clock();
- pCnf = Cnf_DeriveSimple( pHaig, Aig_ManCoNum(pHaig) );
-// Aig_ManForEachObj( pHaig, pObj, i )
-// printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
-// printf( "\n" );
-
- // create the SAT solver to be used for this problem
- pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
-//Sat_SolverWriteDimacs( pSat, "1.cnf", NULL, NULL, 0 );
- if ( pSat == NULL )
- {
- printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
- return -1;
- }
-
- if ( nFrames == 2 )
- {
- Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
- {
- Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
- pObj1 = Aig_ManObj( pHaig, Id1 );
- pObj2 = Aig_ManObj( pHaig, Id2 );
- if ( pObj1->fPhase ^ pObj2->fPhase )
- {
- Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
- Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 0 );
- if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
- {
- sat_solver_delete( pSat );
- return 0;
- }
- Lits[0]++;
- Lits[1]++;
- if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
- {
- sat_solver_delete( pSat );
- return 0;
- }
- }
- else
- {
- Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
- Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
- if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
- {
- sat_solver_delete( pSat );
- return 0;
- }
- Lits[0]++;
- Lits[1]--;
- if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
- {
- sat_solver_delete( pSat );
- return 0;
- }
- }
- }
-
- if ( !sat_solver_simplify(pSat) )
- {
- sat_solver_delete( pSat );
- return 0;
- }
- }
-ABC_PRT( "Preparation", clock() - clk );
-
-
- // check in the second timeframe
-clk = clock();
- Counter = 0;
- Delta = (nFrames == 2)? pCnf->nVars : 0;
- Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
- {
- Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
- pObj1 = Aig_ManObj( pHaig, Id1 );
- pObj2 = Aig_ManObj( pHaig, Id2 );
- if ( pObj1->fPhase ^ pObj2->fPhase )
- {
- Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
- Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 0 );
-
- RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
- Lits[0]++;
- Lits[1]++;
-
- RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
- if ( RetValue1 != l_False || RetValue2 != l_False )
- Counter++;
- }
- else
- {
- Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
- Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 1 );
-
- RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
- Lits[0]++;
- Lits[1]--;
-
- RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
- if ( RetValue1 != l_False || RetValue2 != l_False )
- Counter++;
- }
- if ( i % 50 == 1 )
- printf( "Solving assertion %6d out of %6d.\r", i/2, Vec_IntSize(pHaig->vEquPairs)/2 );
-
-// if ( i / 2 > 1000 )
-// break;
- }
-ABC_PRT( "Solving ", clock() - clk );
- if ( Counter )
- printf( "Verification failed for %d out of %d classes.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
- else
- printf( "Verification is successful for all %d classes.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
-
- Cnf_DataFree( pCnf );
- sat_solver_delete( pSat );
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig )
-{
- Vec_Ptr_t * vTemp;
- Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter;
- int Id1, Id2, i;
- // remove regular POs
- Aig_ManSetCioIds( pHaig );
- vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) );
- Aig_ManForEachCo( pHaig, pObj, i )
- {
- if ( Saig_ObjIsPo(pHaig, pObj) )
- {
- Aig_ObjDisconnect( pHaig, pObj );
- Vec_PtrWriteEntry( pHaig->vObjs, pObj->Id, NULL );
- }
- else
- {
- Vec_PtrPush( vTemp, pObj );
- }
- }
- Vec_PtrShrink( pHaig->vCos, 0 );
- pHaig->nObjs[AIG_OBJ_CO] = Vec_PtrSize( vTemp );
- // add new POs
- Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
- {
- Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
- pObj1 = Aig_ManObj( pHaig, Id1 );
- pObj2 = Aig_ManObj( pHaig, Id2 );
- assert( pObj1 != pObj2 );
- assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) );
- pMiter = Aig_Exor( pHaig, pObj1, pObj2 );
- pMiter = Aig_NotCond( pMiter, Aig_ObjPhaseReal(pMiter) );
- assert( Aig_ObjPhaseReal(pMiter) == 0 );
- Aig_ObjCreateCo( pHaig, pMiter );
- }
- printf( "Added %d property outputs.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
- // add the registers
- Vec_PtrForEachEntry( Aig_Obj_t *, vTemp, pObj, i )
- Vec_PtrPush( pHaig->vCos, pObj );
- Vec_PtrFree( vTemp );
- assert( pHaig->nObjs[AIG_OBJ_CO] == Vec_PtrSize(pHaig->vCos) );
- Aig_ManCleanup( pHaig );
- Aig_ManSetRegNum( pHaig, pHaig->nRegs );
-// return pHaig;
-
- printf( "HAIG: " );
- Aig_ManPrintStats( pHaig );
- printf( "HAIG is written into file \"haig.blif\".\n" );
- Saig_ManDumpBlif( pHaig, "haig.blif" );
-
- Vec_IntFree( pHaig->vEquPairs );
- Aig_ManStop( pHaig );
- return NULL;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
-{
- int fSeqHaig = (int)( Aig_ManRegNum(p) > 0 );
- Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
- Aig_Man_t * pNew, * pTemp;
- Aig_Obj_t * pObj;
- int i, k, nStepsReal;
- clock_t clk = clock(), clkSynth;
- Dar_ManDefaultRwrParams( pParsRwr );
-
-clk = clock();
- // duplicate this manager
- pNew = Aig_ManDupSimple( p );
- // create its history AIG
- pNew->pManHaig = Aig_ManDupSimple( pNew );
- Aig_ManForEachObj( pNew, pObj, i )
- pObj->pHaig = (Aig_Obj_t *)pObj->pData;
- // remove structural hashing table
- Aig_TableClear( pNew->pManHaig );
- pNew->pManHaig->vEquPairs = Vec_IntAlloc( 10000 );
-ABC_PRT( "HAIG setup time", clock() - clk );
-
-clk = clock();
- if ( fSeqHaig )
- {
- if ( fRetimingOnly )
- {
- // perform retiming
- nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs );
- pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
- Aig_ManStop( pTemp );
- printf( "Performed %d retiming moves.\n", nStepsReal );
- }
- else
- {
- for ( k = 0; k < nIters; k++ )
- {
- // perform balancing
- pNew = Dar_ManBalance( pTemp = pNew, 0 );
- Aig_ManStop( pTemp );
-
- // perform rewriting
- Dar_ManRewrite( pNew, pParsRwr );
- pNew = Aig_ManDupDfs( pTemp = pNew );
- Aig_ManStop( pTemp );
-
- // perform retiming
- nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs );
- pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
- Aig_ManStop( pTemp );
- printf( "Performed %d retiming moves.\n", nStepsReal );
- }
- }
- }
- else
- {
- for ( k = 0; k < nIters; k++ )
- {
- // perform balancing
- pNew = Dar_ManBalance( pTemp = pNew, 0 );
- Aig_ManStop( pTemp );
-
- // perform rewriting
- Dar_ManRewrite( pNew, pParsRwr );
- pNew = Aig_ManDupDfs( pTemp = pNew );
- Aig_ManStop( pTemp );
- }
- }
-ABC_PRT( "Synthesis time ", clock() - clk );
-clkSynth = clock() - clk;
-
- // use the haig for verification
-// Aig_ManAntiCleanup( pNew->pManHaig );
- Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
-//Aig_ManShow( pNew->pManHaig, 0, NULL );
-
- printf( "AIG before: " );
- Aig_ManPrintStats( p );
- printf( "AIG after: " );
- Aig_ManPrintStats( pNew );
- printf( "HAIG: " );
- Aig_ManPrintStats( pNew->pManHaig );
-
- if ( fUseCnf )
- {
- if ( !Aig_ManHaigVerify2( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
- printf( "Constructing SAT solver has failed.\n" );
- }
- else
- {
- if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) )
- printf( "Constructing SAT solver has failed.\n" );
- }
-
- Saig_ManHaigDump( pNew->pManHaig );
- pNew->pManHaig = NULL;
- return pNew;
-/*
- // cleanup
- Vec_IntFree( pNew->pManHaig->vEquPairs );
- Aig_ManStop( pNew->pManHaig );
- pNew->pManHaig = NULL;
- return pNew;
-*/
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 91f10590..fd93ccec 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -215,7 +215,6 @@ struct Abc_Ntk_t_
void * pExcare; // the EXDC network (if given)
void * pData; // misc
Abc_Ntk_t * pCopy; // copy of this network
- void * pHaig; // history AIG
float * pLutTimes; // arrivals/requireds/slacks using LUT-delay model
Vec_Ptr_t * vOnehots; // names of one-hot-encoded registers
Vec_Int_t * vObjPerm; // permutation saved
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 4e725a01..5fc3ffd3 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -344,9 +344,6 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
// add the node to the list of updated nodes
if ( pMan->vAddedCells )
Vec_PtrPush( pMan->vAddedCells, pAnd );
- // create HAIG
-// if ( pAnd->pNtk->pHaig )
-// pAnd->pEquiv = Hop_And( pAnd->pNtk->pHaig, Abc_ObjChild0Equiv(pAnd), Abc_ObjChild1Equiv(pAnd) );
return pAnd;
}
@@ -387,9 +384,6 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
// add the node to the list of updated nodes
// if ( pMan->vAddedCells )
// Vec_PtrPush( pMan->vAddedCells, pAnd );
- // create HAIG
-// if ( pAnd->pNtk->pHaig )
-// pAnd->pEquiv = Hop_And( pAnd->pNtk->pHaig, Abc_ObjChild0Equiv(pAnd), Abc_ObjChild1Equiv(pAnd) );
return pAnd;
}
@@ -858,9 +852,6 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int f
Vec_PtrPush( pMan->vStackReplaceOld, pOld );
Vec_PtrPush( pMan->vStackReplaceNew, pNew );
assert( !Abc_ObjIsComplement(pOld) );
- // create HAIG
-// if ( pOld->pNtk->pHaig )
-// Hop_ObjCreateChoice( pOld->pEquiv, Abc_ObjRegular(pNew)->pEquiv );
// process the replacements
while ( Vec_PtrSize(pMan->vStackReplaceOld) )
{
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 5f9c0f0d..db54643d 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -1070,9 +1070,6 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
// int LargePiece = (4 << ABC_NUM_STEPS);
if ( pNtk == NULL )
return;
- // free the HAIG
-// if ( pNtk->pHaig )
-// Abc_NtkHaigStop( pNtk );
// free EXDC Ntk
if ( pNtk->pExdc )
Abc_NtkDelete( pNtk->pExdc );
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 2c391e89..9807997c 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -277,9 +277,6 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
// if ( Abc_ObjRegular(pNodeOld->pCopy) == Abc_AigConst1(pNtkNew) )
// printf( "Constant node\n" );
// assert( pNodeOld->Level >= Abc_ObjRegular(pNodeOld->pCopy)->Level );
- // update HAIG
-// if ( Abc_ObjRegular(pNodeOld->pCopy)->pNtk->pHaig )
-// Hop_ObjCreateChoice( pNodeOld->pEquiv, Abc_ObjRegular(pNodeOld->pCopy)->pEquiv );
return pNodeOld->pCopy;
}
diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
index d6c0ddad..02547de1 100644
--- a/src/base/abci/abcHaig.c
+++ b/src/base/abci/abcHaig.c
@@ -31,129 +31,6 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-#if 0
-
-/**Function*************************************************************
-
- Synopsis [Start history AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NtkHaigStart( Abc_Ntk_t * pNtk )
-{
- Hop_Man_t * p;
- Abc_Obj_t * pObj, * pTemp;
- int i;
- assert( Abc_NtkIsStrash(pNtk) );
- // check if the package is already started
- if ( pNtk->pHaig )
- {
- Abc_NtkHaigStop( pNtk );
- assert( pNtk->pHaig == NULL );
- printf( "Warning: Previous history AIG was removed.\n" );
- }
- // make sure the data is clean
- Abc_NtkForEachObj( pNtk, pObj, i )
- assert( pObj->pEquiv == NULL );
- // start the HOP package
- p = Hop_ManStart();
- p->vObjs = Vec_PtrAlloc( 4096 );
- Vec_PtrPush( p->vObjs, Hop_ManConst1(p) );
- // map the constant node
- Abc_AigConst1(pNtk)->pEquiv = Hop_ManConst1(p);
- // map the CIs
- Abc_NtkForEachCi( pNtk, pObj, i )
- pObj->pEquiv = Hop_ObjCreatePi(p);
- // map the internal nodes
- Abc_NtkForEachNode( pNtk, pObj, i )
- pObj->pEquiv = Hop_And( p, Abc_ObjChild0Equiv(pObj), Abc_ObjChild1Equiv(pObj) );
- // map the choice nodes
- if ( Abc_NtkGetChoiceNum( pNtk ) )
- {
- // print warning about choice nodes
- printf( "Warning: The choice nodes in the original AIG are converted into HAIG.\n" );
- Abc_NtkForEachNode( pNtk, pObj, i )
- {
- if ( !Abc_AigNodeIsChoice( pObj ) )
- continue;
- for ( pTemp = pObj->pData; pTemp; pTemp = pTemp->pData )
- Hop_ObjCreateChoice( pObj->pEquiv, pTemp->pEquiv );
- }
- }
- // make sure everything is okay
- if ( !Hop_ManCheck(p) )
- {
- printf( "Abc_NtkHaigStart: Check for History AIG has failed.\n" );
- Hop_ManStop(p);
- return 0;
- }
- pNtk->pHaig = p;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Stops history AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NtkHaigStop( Abc_Ntk_t * pNtk )
-{
- Abc_Obj_t * pObj;
- int i;
- assert( Abc_NtkIsStrash(pNtk) );
- if ( pNtk->pHaig == NULL )
- {
- printf( "Warning: History AIG is not allocated.\n" );
- return 1;
- }
- Abc_NtkForEachObj( pNtk, pObj, i )
- pObj->pEquiv = NULL;
- Hop_ManStop( pNtk->pHaig );
- pNtk->pHaig = NULL;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Transfers the HAIG to the new network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
-{
- Abc_Obj_t * pObj;
- int i;
- if ( pNtkOld->pHaig == NULL )
- return;
- // transfer the package
- assert( pNtkNew->pHaig == NULL );
- pNtkNew->pHaig = pNtkOld->pHaig;
- pNtkOld->pHaig = NULL;
- // transfer constant pointer
- Abc_AigConst1(pNtkOld)->pCopy->pEquiv = Abc_AigConst1(pNtkOld)->pEquiv;
- // transfer the CI pointers
- Abc_NtkForEachCi( pNtkOld, pObj, i )
- pObj->pCopy->pEquiv = pObj->pEquiv;
-}
-
-
-#endif
/**Function*************************************************************
@@ -642,64 +519,6 @@ int Abc_NtkHaigResetReprs( Hop_Man_t * p )
return nFanouts;
}
-#if 0
-
-/**Function*************************************************************
-
- Synopsis [Stops history AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
-{
- Hop_Man_t * pMan, * pManTemp;
- Abc_Ntk_t * pNtkAig;
- Abc_Obj_t * pObj;
- int i;
-
- // check if HAIG is available
- assert( Abc_NtkIsStrash(pNtk) );
- if ( pNtk->pHaig == NULL )
- {
- printf( "Warning: History AIG is not available.\n" );
- return NULL;
- }
- // convert HOP package into AIG with choices
- // print HAIG stats
-// Hop_ManPrintStats( pMan ); // USES DATA!!!
-
- // add the POs
- Abc_NtkForEachCo( pNtk, pObj, i )
- Hop_ObjCreatePo( pNtk->pHaig, Abc_ObjChild0Equiv(pObj) );
-
- // clean the old network
- Abc_NtkForEachObj( pNtk, pObj, i )
- pObj->pEquiv = NULL;
- pMan = pNtk->pHaig;
- pNtk->pHaig = 0;
-
- // iteratively reconstruct the HOP manager to create choice nodes
- while ( Abc_NtkHaigResetReprs( pMan ) )
- {
- pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
- Hop_ManStop( pManTemp );
- }
-
- // traverse in the topological order and create new AIG
- pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
- Hop_ManStop( pMan );
-
- // free HAIG
- return pNtkAig;
-}
-
-#endif
-
/**Function*************************************************************
Synopsis [Transform HOP manager into the one without loops.]
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 779c5c7e..c68e0729 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -1000,7 +1000,6 @@ Hop_Man_t * Abc_NtkPartStartHop( Abc_Ntk_t * pNtk )
Abc_Ntk_t * Abc_NtkPartStitchChoices( Abc_Ntk_t * pNtk, Vec_Ptr_t * vParts )
{
extern Abc_Ntk_t * Abc_NtkHopRemoveLoops( Abc_Ntk_t * pNtk, Hop_Man_t * pMan );
-
Hop_Man_t * pMan;
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew, * pNtkTemp;
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index e25e497d..cb57acaa 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -21,7 +21,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcFraig.c \
src/base/abci/abcFxu.c \
src/base/abci/abcGen.c \
- src/base/abci/abcHaig.c \
+ src/base/abci/abcHaig.c \
src/base/abci/abcIf.c \
src/base/abci/abcIfif.c \
src/base/abci/abcIfMux.c \
diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c
index 75f0eaf4..f31c6fc7 100644
--- a/src/opt/dar/darBalance.c
+++ b/src/opt/dar/darBalance.c
@@ -532,19 +532,6 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
// make sure the balanced node is not assigned
// assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
assert( pObjOld->pData == NULL );
- if ( pNew->pManHaig != NULL )
- {
- Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew);
-// printf( "Balancing HAIG node %d equivalent to HAIG node %d (over = %d).\n",
-// pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
- assert( pObjNewR->pHaig != NULL );
- assert( !Aig_IsComplement(pObjNewR->pHaig) );
- assert( pNew->pManHaig->vEquPairs != NULL );
- Vec_IntPush( pNew->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
- Vec_IntPush( pNew->pManHaig->vEquPairs, pObjOld->pHaig->Id );
- }
- else
- Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
return (Aig_Obj_t *)(pObjOld->pData = pObjNew);
}
@@ -574,12 +561,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
- // pass the HAIG manager
- if ( p->pManHaig != NULL )
- {
- pNew->pManHaig = p->pManHaig; p->pManHaig = NULL;
- Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(pNew->pManHaig);
- }
// map the PI nodes
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -598,7 +579,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
// copy the PI
pObjNew = Aig_ObjCreateCi(pNew);
pObj->pData = pObjNew;
- pObjNew->pHaig = pObj->pHaig;
// set the arrival time of the new PI
arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
pObjNew->Level = (int)arrTime;
@@ -614,7 +594,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime );
// create PO
pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
- pObjNew->pHaig = pObj->pHaig;
}
else
assert( 0 );
@@ -629,7 +608,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pObjNew = Aig_ObjCreateCi(pNew);
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
- pObjNew->pHaig = pObj->pHaig;
}
Aig_ManForEachCo( p, pObj, i )
{
@@ -637,7 +615,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
- pObjNew->pHaig = pObj->pHaig;
}
}
Vec_VecFree( vStore );
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index b3830cc3..583ca563 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -134,27 +134,6 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
/**Function*************************************************************
- Synopsis [Performs one iteration of AIG rewriting.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dar_ManHaigPrintStats( Aig_Man_t * pAig )
-{
- Aig_Obj_t * pObj;
- int Counter, i;
- Counter = 0;
- Aig_ManForEachNode( pAig, pObj, i )
- Counter += (pObj->pHaig != NULL);
- printf( "Total nodes = %6d. Equiv nodes = %6d.\n", Aig_ManNodeNum(pAig), Counter );
-}
-
-/**Function*************************************************************
-
Synopsis [Reproduces script "compress".]
Description []
@@ -352,34 +331,20 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
//alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
{
Vec_Ptr_t * vAigs;
- Aig_Obj_t * pObj;
- int i;
vAigs = Vec_PtrAlloc( 3 );
pAig = Aig_ManDupDfs(pAig);
Vec_PtrPush( vAigs, pAig );
- Aig_ManForEachObj( pAig, pObj, i )
- pObj->pHaig = pObj;
-
pAig = Dar_ManCompress(pAig, fBalance, fUpdateLevel, fPower, fVerbose);
Vec_PtrPush( vAigs, pAig );
//Aig_ManPrintStats( pAig );
- Aig_ManForEachObj( pAig, pObj, i )
- {
- pObj->pNext = pObj->pHaig;
- pObj->pHaig = pObj;
- }
-
pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose);
Vec_PtrPush( vAigs, pAig );
//Aig_ManPrintStats( pAig );
pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 1 );
- Aig_ManForEachObj( pAig, pObj, i )
- pObj->pHaig = pObj->pNext;
-
return vAigs;
}
diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c
index 2941f24f..9d573bee 100644
--- a/src/proof/fra/fraLcr.c
+++ b/src/proof/fra/fraLcr.c
@@ -273,7 +273,6 @@ Aig_Obj_t * Fra_LcrManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
return (Aig_Obj_t *)(pObj->pData = pObjNew);
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 06:38:47 +0000