summaryrefslogtreecommitdiffstats
path: root/src/aig/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra')
-rw-r--r--src/aig/fra/fra.h49
-rw-r--r--src/aig/fra/fraAnd.c52
-rw-r--r--src/aig/fra/fraClass.c56
-rw-r--r--src/aig/fra/fraCnf.c72
-rw-r--r--src/aig/fra/fraCore.c10
-rw-r--r--src/aig/fra/fraMan.c38
-rw-r--r--src/aig/fra/fraSat.c36
-rw-r--r--src/aig/fra/fraSim.c96
8 files changed, 205 insertions, 204 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 29195d19..7f2df105 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -36,6 +36,7 @@ extern "C" {
#include <time.h>
#include "vec.h"
+#include "aig.h"
#include "dar.h"
#include "satSolver.h"
@@ -73,8 +74,8 @@ struct Fra_Man_t_
// high-level data
Fra_Par_t * pPars; // parameters governing fraiging
// AIG managers
- Dar_Man_t * pManAig; // the starting AIG manager
- Dar_Man_t * pManFraig; // the final AIG manager
+ Aig_Man_t * pManAig; // the starting AIG manager
+ Aig_Man_t * pManFraig; // the final AIG manager
// simulation info
unsigned * pSimWords; // memory for simulation information
int nSimWords; // the number of simulation words
@@ -86,8 +87,8 @@ struct Fra_Man_t_
Vec_Ptr_t * vClasses; // equivalence classes
Vec_Ptr_t * vClasses1; // equivalence class of Const1 node
Vec_Ptr_t * vClassesTemp; // temporary storage for new classes
- Dar_Obj_t ** pMemClasses; // memory allocated for equivalence classes
- Dar_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
+ Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes
+ Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
Vec_Ptr_t * vClassOld; // old equivalence class after splitting
Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
int nPairs; // the number of pairs of nodes
@@ -98,8 +99,8 @@ struct Fra_Man_t_
sint64 nBTLimitGlobal; // resource limit
sint64 nInsLimitGlobal; // resource limit
// various data members
- Dar_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
- Dar_Obj_t ** pMemRepr; // memory allocated for points to the node representatives
+ Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
+ Aig_Obj_t ** pMemRepr; // memory allocated for points to the node representatives
Vec_Ptr_t ** pMemFanins; // the arrays of fanins
int * pMemSatNums; // the array of SAT numbers
int nSizeAlloc; // allocated size of the arrays
@@ -135,21 +136,21 @@ struct Fra_Man_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-static inline unsigned * Fra_ObjSim( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; }
+static inline unsigned * Fra_ObjSim( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; }
static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
-static inline Dar_Obj_t * Fra_ObjFraig( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]; }
-static inline Dar_Obj_t * Fra_ObjRepr( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]; }
-static inline Vec_Ptr_t * Fra_ObjFaninVec( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; }
-static inline int Fra_ObjSatNum( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; }
+static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]; }
+static inline Aig_Obj_t * Fra_ObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]; }
+static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; }
+static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; }
-static inline void Fra_ObjSetFraig( Dar_Obj_t * pObj, Dar_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id] = pNode; }
-static inline void Fra_ObjSetRepr( Dar_Obj_t * pObj, Dar_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id] = pNode; }
-static inline void Fra_ObjSetFaninVec( Dar_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; }
-static inline void Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; }
+static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id] = pNode; }
+static inline void Fra_ObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id] = pNode; }
+static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; }
+static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; }
-static inline Dar_Obj_t * Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL; }
-static inline Dar_Obj_t * Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL; }
+static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; }
+static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
@@ -167,21 +168,21 @@ extern void Fra_CreateClasses( Fra_Man_t * p );
extern int Fra_RefineClasses( Fra_Man_t * p );
extern int Fra_RefineClasses1( Fra_Man_t * p );
/*=== fraCnf.c ========================================================*/
-extern void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
+extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== fraCore.c ========================================================*/
-extern Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pParams );
+extern Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pParams );
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
-extern Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pParams );
+extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
extern void Fra_ManPrepare( Fra_Man_t * p );
extern void Fra_ManStop( Fra_Man_t * p );
extern void Fra_ManPrint( Fra_Man_t * p );
/*=== fraSat.c ========================================================*/
-extern int Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
-extern int Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew );
+extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
/*=== fraSim.c ========================================================*/
-extern int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj );
-extern int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 );
+extern int Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj );
+extern int Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern void Fra_SavePattern( Fra_Man_t * p );
extern void Fra_Simulate( Fra_Man_t * p );
extern void Fra_Resimulate( Fra_Man_t * p );
diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c
index a360ce9b..36b4ccc3 100644
--- a/src/aig/fra/fraAnd.c
+++ b/src/aig/fra/fraAnd.c
@@ -40,48 +40,48 @@
SeeAlso []
***********************************************************************/
-Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
+Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
{
- Dar_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
+ Aig_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
int RetValue;
- assert( !Dar_IsComplement(pObjOld) );
- assert( Dar_ObjIsNode(pObjOld) );
+ assert( !Aig_IsComplement(pObjOld) );
+ assert( Aig_ObjIsNode(pObjOld) );
// get the fraiged fanins
pFanin0Fraig = Fra_ObjChild0Fra(pObjOld);
pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
// get the fraiged node
- pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
- if ( Dar_ObjIsConst1(Dar_Regular(pObjFraig)) )
+ pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
+ if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) )
return pObjFraig;
- Dar_Regular(pObjFraig)->pData = p;
+ Aig_Regular(pObjFraig)->pData = p;
// get representative of this class
pObjOldRepr = Fra_ObjRepr(pObjOld);
if ( pObjOldRepr == NULL || // this is a unique node
- (!p->pPars->fDoSparse && pObjOldRepr == Dar_ManConst1(p->pManAig)) ) // this is a sparse node
+ (!p->pPars->fDoSparse && pObjOldRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
{
- assert( Dar_Regular(pFanin0Fraig) != Dar_Regular(pFanin1Fraig) );
- assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin0Fraig) );
- assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin1Fraig) );
+ assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) );
+ assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) );
+ assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) );
return pObjFraig;
}
// get the fraiged representative
pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr);
// if the fraiged nodes are the same, return
- if ( Dar_Regular(pObjFraig) == Dar_Regular(pObjOldReprFraig) )
+ if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjOldReprFraig) )
return pObjFraig;
- assert( Dar_Regular(pObjFraig) != Dar_ManConst1(p->pManFraig) );
+ assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
// printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id );
// if they are proved different, the c-ex will be in p->pPatWords
- RetValue = Fra_NodesAreEquiv( p, Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) );
+ RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) );
if ( RetValue == 1 ) // proved equivalent
{
// pObjOld->fMarkA = 1;
- return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+ return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
}
if ( RetValue == -1 ) // failed
{
- Dar_Obj_t * ppNodes[2] = { Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) };
+ Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) };
Vec_Ptr_t * vNodes;
if ( !p->pPars->fSpeculate )
@@ -90,11 +90,11 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
// pObjOld->fMarkB = 1;
p->nSpeculs++;
- vNodes = Dar_ManDfsNodes( p->pManFraig, ppNodes, 2 );
+ vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 );
printf( "%d ", Vec_PtrSize(vNodes) );
Vec_PtrFree( vNodes );
- return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+ return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
}
// printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id );
// simulate the counter-example and return the Fraig node
@@ -118,18 +118,18 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
***********************************************************************/
void Fra_Sweep( Fra_Man_t * p )
{
- Dar_Obj_t * pObj, * pObjNew;
+ Aig_Obj_t * pObj, * pObjNew;
int i, k = 0;
p->nClassesZero = Vec_PtrSize(p->vClasses1);
p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
// duplicate internal nodes
-// p->pProgress = Extra_ProgressBarStart( stdout, Dar_ManNodeNum(p->pManAig) );
- Dar_ManForEachNode( p->pManAig, pObj, i )
+// p->pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p->pManAig) );
+ Aig_ManForEachNode( p->pManAig, pObj, i )
{
// Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
// default to simple strashing if simulation detected a counter-example for a PO
if ( p->pManFraig->pData )
- pObjNew = Dar_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
+ pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
else
pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
Fra_ObjSetFraig( pObj, pObjNew );
@@ -138,15 +138,15 @@ p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0
// Extra_ProgressBarStop( p->pProgress );
p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
// try to prove the outputs of the miter
- p->nNodesMiter = Dar_ManNodeNum(p->pManFraig);
+ p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
// Fra_MiterStatus( p->pManFraig );
// if ( p->pPars->fProve && p->pManFraig->pData == NULL )
// Fra_MiterProve( p );
// add the POs
- Dar_ManForEachPo( p->pManAig, pObj, i )
- Dar_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
+ Aig_ManForEachPo( p->pManAig, pObj, i )
+ Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
// remove dangling nodes
- Dar_ManCleanup( p->pManFraig );
+ Aig_ManCleanup( p->pManFraig );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 33421423..3de54453 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -36,8 +36,8 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static inline Dar_Obj_t * Fra_ObjNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj ) { return ppNexts[pObj->Id]; }
-static inline void Fra_ObjSetNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj, Dar_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
+static inline Aig_Obj_t * Fra_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; }
+static inline void Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -54,9 +54,9 @@ static inline void Fra_ObjSetNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pOb
SeeAlso []
***********************************************************************/
-void Fra_PrintClass( Dar_Obj_t ** pClass )
+void Fra_PrintClass( Aig_Obj_t ** pClass )
{
- Dar_Obj_t * pTemp;
+ Aig_Obj_t * pTemp;
int i;
printf( "{ " );
for ( i = 0; pTemp = pClass[i]; i++ )
@@ -75,9 +75,9 @@ void Fra_PrintClass( Dar_Obj_t ** pClass )
SeeAlso []
***********************************************************************/
-int Fra_CountClass( Dar_Obj_t ** pClass )
+int Fra_CountClass( Aig_Obj_t ** pClass )
{
- Dar_Obj_t * pTemp;
+ Aig_Obj_t * pTemp;
int i;
for ( i = 0; pTemp = pClass[i]; i++ );
return i;
@@ -96,7 +96,7 @@ int Fra_CountClass( Dar_Obj_t ** pClass )
***********************************************************************/
int Fra_CountPairsClasses( Fra_Man_t * p )
{
- Dar_Obj_t ** pClass;
+ Aig_Obj_t ** pClass;
int i, nNodes, nPairs = 0;
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
@@ -120,7 +120,7 @@ int Fra_CountPairsClasses( Fra_Man_t * p )
***********************************************************************/
void Fra_PrintClasses( Fra_Man_t * p )
{
- Dar_Obj_t ** pClass;
+ Aig_Obj_t ** pClass;
int i;
printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_CountPairsClasses(p) );
Vec_PtrForEachEntry( p->vClasses, pClass, i )
@@ -142,7 +142,7 @@ void Fra_PrintClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
-unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj )
+unsigned Fra_NodeHash( Fra_Man_t * p, Aig_Obj_t * pObj )
{
static int s_FPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
@@ -220,21 +220,21 @@ unsigned int Cudd_PrimeFra( unsigned int p )
***********************************************************************/
void Fra_CreateClasses( Fra_Man_t * p )
{
- Dar_Obj_t ** ppTable, ** ppNexts;
- Dar_Obj_t * pObj, * pTemp;
+ Aig_Obj_t ** ppTable, ** ppNexts;
+ Aig_Obj_t * pObj, * pTemp;
int i, k, nTableSize, nEntries, nNodes, iEntry;
// allocate the hash table hashing simulation info into nodes
- nTableSize = Cudd_PrimeFra( Dar_ManObjIdMax(p->pManAig) + 1 );
- ppTable = ALLOC( Dar_Obj_t *, nTableSize );
- ppNexts = ALLOC( Dar_Obj_t *, nTableSize );
- memset( ppTable, 0, sizeof(Dar_Obj_t *) * nTableSize );
+ nTableSize = Cudd_PrimeFra( Aig_ManObjIdMax(p->pManAig) + 1 );
+ ppTable = ALLOC( Aig_Obj_t *, nTableSize );
+ ppNexts = ALLOC( Aig_Obj_t *, nTableSize );
+ memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
// add all the nodes to the hash table
Vec_PtrClear( p->vClasses1 );
- Dar_ManForEachObj( p->pManAig, pObj, i )
+ Aig_ManForEachObj( p->pManAig, pObj, i )
{
- if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) )
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
// hash the node by its simulation info
iEntry = Fra_NodeHash( p, pObj ) % nTableSize;
@@ -242,7 +242,7 @@ void Fra_CreateClasses( Fra_Man_t * p )
if ( iEntry == 0 && Fra_NodeHasZeroSim( p, pObj ) )
{
Vec_PtrPush( p->vClasses1, pObj );
- Fra_ObjSetRepr( pObj, Dar_ManConst1(p->pManAig) );
+ Fra_ObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
continue;
}
// add the node to the class
@@ -275,15 +275,15 @@ void Fra_CreateClasses( Fra_Man_t * p )
}
// allocate room for classes
- p->pMemClasses = ALLOC( Dar_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
+ p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
p->pMemClassesFree = p->pMemClasses + 2*nEntries;
// copy the entries into storage in the topological order
Vec_PtrClear( p->vClasses );
nEntries = 0;
- Dar_ManForEachObj( p->pManAig, pObj, i )
+ Aig_ManForEachObj( p->pManAig, pObj, i )
{
- if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) )
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
// skip the nodes that are not representatives of non-trivial classes
if ( pObj->fMarkA == 0 )
@@ -307,7 +307,7 @@ void Fra_CreateClasses( Fra_Man_t * p )
Fra_ObjSetRepr( pTemp, pObj );
}
// add as many empty entries
-// memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Dar_Obj_t *) * nNodes );
+// memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Aig_Obj_t *) * nNodes );
p->pMemClasses[2*nEntries + nNodes] = NULL;
// increment the number of entries
nEntries += k;
@@ -329,9 +329,9 @@ void Fra_CreateClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
-Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
+Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass )
{
- Dar_Obj_t * pObj, ** ppThis;
+ Aig_Obj_t * pObj, ** ppThis;
int i;
assert( ppClass[0] != NULL && ppClass[1] != NULL );
@@ -390,7 +390,7 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
***********************************************************************/
int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
{
- Dar_Obj_t ** pClass, ** pClass2;
+ Aig_Obj_t ** pClass, ** pClass2;
int nRefis;
pClass = Vec_PtrEntryLast( vClasses );
for ( nRefis = 0; pClass2 = Fra_RefineClassOne( p, pClass ); nRefis++ )
@@ -426,7 +426,7 @@ int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
int Fra_RefineClasses( Fra_Man_t * p )
{
Vec_Ptr_t * vTemp;
- Dar_Obj_t ** pClass;
+ Aig_Obj_t ** pClass;
int clk, i, nRefis;
// check if some outputs already became non-constant
// this is a special case when computation can be stopped!!!
@@ -466,14 +466,14 @@ p->timeRef += clock() - clk;
***********************************************************************/
int Fra_RefineClasses1( Fra_Man_t * p )
{
- Dar_Obj_t * pObj, ** ppClass;
+ Aig_Obj_t * pObj, ** ppClass;
int i, k, nRefis, clk;
// check if there is anything to refine
if ( Vec_PtrSize(p->vClasses1) == 0 )
return 0;
clk = clock();
// make sure constant 1 class contains only non-constant nodes
- assert( Vec_PtrEntry(p->vClasses1,0) != Dar_ManConst1(p->pManAig) );
+ assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pManAig) );
// collect all the nodes to be refined
k = 0;
Vec_PtrClear( p->vClassNew );
diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c
index a662ade2..7df55d93 100644
--- a/src/aig/fra/fraCnf.c
+++ b/src/aig/fra/fraCnf.c
@@ -40,23 +40,23 @@
SeeAlso []
***********************************************************************/
-void Fra_AddClausesMux( Fra_Man_t * p, Dar_Obj_t * pNode )
+void Fra_AddClausesMux( Fra_Man_t * p, Aig_Obj_t * pNode )
{
- Dar_Obj_t * pNodeI, * pNodeT, * pNodeE;
+ Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
- assert( !Dar_IsComplement( pNode ) );
- assert( Dar_ObjIsMuxType( pNode ) );
+ assert( !Aig_IsComplement( pNode ) );
+ assert( Aig_ObjIsMuxType( pNode ) );
// get nodes (I = if, T = then, E = else)
- pNodeI = Dar_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+ pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
// get the variable numbers
VarF = Fra_ObjSatNum(pNode);
VarI = Fra_ObjSatNum(pNodeI);
- VarT = Fra_ObjSatNum(Dar_Regular(pNodeT));
- VarE = Fra_ObjSatNum(Dar_Regular(pNodeE));
+ VarT = Fra_ObjSatNum(Aig_Regular(pNodeT));
+ VarE = Fra_ObjSatNum(Aig_Regular(pNodeE));
// get the complementation flags
- fCompT = Dar_IsComplement(pNodeT);
- fCompE = Dar_IsComplement(pNodeE);
+ fCompT = Aig_IsComplement(pNodeT);
+ fCompE = Aig_IsComplement(pNodeE);
// f = ITE(i, t, e)
@@ -123,12 +123,12 @@ void Fra_AddClausesMux( Fra_Man_t * p, Dar_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
+void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
{
- Dar_Obj_t * pFanin;
+ Aig_Obj_t * pFanin;
int * pLits, nLits, RetValue, i;
- assert( !Dar_IsComplement(pNode) );
- assert( Dar_ObjIsNode( pNode ) );
+ assert( !Aig_IsComplement(pNode) );
+ assert( Aig_ObjIsNode( pNode ) );
// create storage for literals
nLits = Vec_PtrSize(vSuper) + 1;
pLits = ALLOC( int, nLits );
@@ -136,14 +136,14 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
// add !A => !C or A + !C
Vec_PtrForEachEntry( vSuper, pFanin, i )
{
- pLits[0] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), Dar_IsComplement(pFanin));
+ pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
// add A & B => C or !A + !B + C
Vec_PtrForEachEntry( vSuper, pFanin, i )
- pLits[i] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), !Dar_IsComplement(pFanin));
+ pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
assert( RetValue );
@@ -161,18 +161,18 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
SeeAlso []
***********************************************************************/
-void Fra_CollectSuper_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
{
// if the new node is complemented or a PI, another gate begins
- if ( Dar_IsComplement(pObj) || Dar_ObjIsPi(pObj) || (!fFirst && Dar_ObjRefs(pObj) > 1) ||
- (fUseMuxes && Dar_ObjIsMuxType(pObj)) )
+ if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) ||
+ (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
{
Vec_PtrPushUnique( vSuper, pObj );
return;
}
// go through the branches
- Fra_CollectSuper_rec( Dar_ObjChild0(pObj), vSuper, 0, fUseMuxes );
- Fra_CollectSuper_rec( Dar_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+ Fra_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+ Fra_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
}
/**Function*************************************************************
@@ -186,11 +186,11 @@ void Fra_CollectSuper_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
SeeAlso []
***********************************************************************/
-Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes )
+Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes )
{
Vec_Ptr_t * vSuper;
- assert( !Dar_IsComplement(pObj) );
- assert( !Dar_ObjIsPi(pObj) );
+ assert( !Aig_IsComplement(pObj) );
+ assert( !Aig_ObjIsPi(pObj) );
vSuper = Vec_PtrAlloc( 4 );
Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
return vSuper;
@@ -207,19 +207,19 @@ Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes )
SeeAlso []
***********************************************************************/
-void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
{
Fra_Man_t * pTemp = pObj->pData;
- assert( !Dar_IsComplement(pObj) );
+ assert( !Aig_IsComplement(pObj) );
if ( Fra_ObjSatNum(pObj) )
return;
assert( Fra_ObjSatNum(pObj) == 0 );
assert( Fra_ObjFaninVec(pObj) == NULL );
- if ( Dar_ObjIsConst1(pObj) )
+ if ( Aig_ObjIsConst1(pObj) )
return;
//printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
Fra_ObjSetSatNum( pObj, p->nSatVars++ );
- if ( Dar_ObjIsNode(pObj) )
+ if ( Aig_ObjIsNode(pObj) )
Vec_PtrPush( vFrontier, pObj );
}
@@ -234,10 +234,10 @@ void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontie
SeeAlso []
***********************************************************************/
-void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
Vec_Ptr_t * vFrontier, * vFanins;
- Dar_Obj_t * pNode, * pFanin;
+ Aig_Obj_t * pNode, * pFanin;
int i, k, fUseMuxes = 1;
assert( pOld || pNew );
// quit if CNF is ready
@@ -253,22 +253,22 @@ void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
// create the supergate
assert( Fra_ObjSatNum(pNode) );
assert( Fra_ObjFaninVec(pNode) == NULL );
- if ( fUseMuxes && Dar_ObjIsMuxType(pNode) )
+ if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
{
vFanins = Vec_PtrAlloc( 4 );
- Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin0(pNode) ) );
- Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin1(pNode) ) );
- Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin0(pNode) ) );
- Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin1(pNode) ) );
+ Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
+ Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
+ Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
+ Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
Vec_PtrForEachEntry( vFanins, pFanin, k )
- Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier );
+ Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
Fra_AddClausesMux( p, pNode );
}
else
{
vFanins = Fra_CollectSuper( pNode, fUseMuxes );
Vec_PtrForEachEntry( vFanins, pFanin, k )
- Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier );
+ Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
Fra_AddClausesSuper( p, pNode, vFanins );
}
assert( Vec_PtrSize(vFanins) > 1 );
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 7fdd1b83..5338d662 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -39,15 +39,15 @@
SeeAlso []
***********************************************************************/
-Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pPars )
+Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
{
Fra_Man_t * p;
- Dar_Man_t * pManAigNew;
+ Aig_Man_t * pManAigNew;
int clk;
- if ( Dar_ManNodeNum(pManAig) == 0 )
- return Dar_ManDup(pManAig);
+ if ( Aig_ManNodeNum(pManAig) == 0 )
+ return Aig_ManDup(pManAig);
clk = clock();
- assert( Dar_ManLatchNum(pManAig) == 0 );
+ assert( Aig_ManLatchNum(pManAig) == 0 );
p = Fra_ManStart( pManAig, pPars );
Fra_Simulate( p );
Fra_Sweep( p );
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 19ed6c03..78246a8c 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -66,7 +66,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
SeeAlso []
***********************************************************************/
-Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
+Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
{
Fra_Man_t * p;
// allocate the fraiging manager
@@ -74,15 +74,15 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
memset( p, 0, sizeof(Fra_Man_t) );
p->pPars = pPars;
p->pManAig = pManAig;
- p->pManFraig = Dar_ManStartFrom( pManAig );
- assert( Dar_ManPiNum(p->pManAig) == Dar_ManPiNum(p->pManFraig) );
+ p->pManFraig = Aig_ManStartFrom( pManAig );
+ assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManFraig) );
// allocate simulation info
p->nSimWords = pPars->nSimWords;
- p->pSimWords = ALLOC( unsigned, (Dar_ManObjIdMax(pManAig) + 1) * p->nSimWords );
+ p->pSimWords = ALLOC( unsigned, (Aig_ManObjIdMax(pManAig) + 1) * p->nSimWords );
// clean simulation info of the constant node
- memset( p->pSimWords, 0, sizeof(unsigned) * ((Dar_ManPiNum(pManAig) + 1) * p->nSimWords) );
+ memset( p->pSimWords, 0, sizeof(unsigned) * ((Aig_ManPiNum(pManAig) + 1) * p->nSimWords) );
// allocate storage for sim pattern
- p->nPatWords = Dar_BitWordNum( Dar_ManPiNum(pManAig) );
+ p->nPatWords = Aig_BitWordNum( Aig_ManPiNum(pManAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
p->pPatScores = ALLOC( int, 32 * p->nSimWords );
p->vPiVars = Vec_PtrAlloc( 100 );
@@ -92,11 +92,11 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
p->vClassNew = Vec_PtrAlloc( 100 );
p->vClassesTemp = Vec_PtrAlloc( 100 );
// allocate other members
- p->nSizeAlloc = Dar_ManObjIdMax(pManAig) + 1;
- p->pMemFraig = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
- memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) );
- p->pMemRepr = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
- memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) );
+ p->nSizeAlloc = Aig_ManObjIdMax(pManAig) + 1;
+ p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
+ memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
+ p->pMemRepr = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
+ memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc );
memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) );
p->pMemSatNums = ALLOC( int, p->nSizeAlloc );
@@ -123,18 +123,18 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
***********************************************************************/
void Fra_ManPrepare( Fra_Man_t * p )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i;
// set the pointers to the manager
- Dar_ManForEachObj( p->pManFraig, pObj, i )
+ Aig_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p;
// set the pointer to the manager
- Dar_ManForEachObj( p->pManAig, pObj, i )
+ Aig_ManForEachObj( p->pManAig, pObj, i )
pObj->pData = p;
// set the pointers to the available fraig nodes
- Fra_ObjSetFraig( Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManFraig) );
- Dar_ManForEachPi( p->pManAig, pObj, i )
- Fra_ObjSetFraig( pObj, Dar_ManPi(p->pManFraig, i) );
+ Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), Aig_ManConst1(p->pManFraig) );
+ Aig_ManForEachPi( p->pManAig, pObj, i )
+ Fra_ObjSetFraig( pObj, Aig_ManPi(p->pManFraig, i) );
}
/**Function*************************************************************
@@ -187,14 +187,14 @@ void Fra_ManStop( Fra_Man_t * p )
***********************************************************************/
void Fra_ManPrint( Fra_Man_t * p )
{
- double nMemory = 1.0*Dar_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
+ double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nSimWords, p->nSimRounds, nMemory );
printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pPars->nBTLimitNode, p->pPars->nBTLimitMiter );
printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n",
- Dar_ManNodeNum(p->pManFraig), p->nNodesMiter, Dar_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+ Aig_ManNodeNum(p->pManFraig), p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
PRT( "AIG simulation ", p->timeSim );
PRT( "AIG traversal ", p->timeTrav );
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index 1c72c807..66b1ba5a 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -24,7 +24,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
+static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -41,13 +41,13 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t *
SeeAlso []
***********************************************************************/
-int Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
// make sure the nodes are not complemented
- assert( !Dar_IsComplement(pNew) );
- assert( !Dar_IsComplement(pOld) );
+ assert( !Aig_IsComplement(pNew) );
+ assert( !Aig_IsComplement(pOld) );
assert( pNew != pOld );
// if at least one of the nodes is a failed node, perform adjustments:
@@ -189,12 +189,12 @@ p->timeSatFail += clock() - clk;
SeeAlso []
***********************************************************************/
-int Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew )
+int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
{
int pLits[2], RetValue1, RetValue, clk;
// make sure the nodes are not complemented
- assert( !Dar_IsComplement(pNew) );
+ assert( !Aig_IsComplement(pNew) );
assert( pNew != p->pManFraig->pConst1 );
p->nSatCalls++;
@@ -261,19 +261,19 @@ p->timeSatFail += clock() - clk;
SeeAlso []
***********************************************************************/
-int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, int LevelMax )
+int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, int LevelMax )
{
Vec_Ptr_t * vFanins;
- Dar_Obj_t * pFanin;
+ Aig_Obj_t * pFanin;
int i, Counter = 0;
- assert( !Dar_IsComplement(pObj) );
+ assert( !Aig_IsComplement(pObj) );
assert( Fra_ObjSatNum(pObj) );
// skip visited variables
- if ( Dar_ObjIsTravIdCurrent(p->pManFraig, pObj) )
+ if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pObj) )
return 0;
- Dar_ObjSetTravIdCurrent(p->pManFraig, pObj);
+ Aig_ObjSetTravIdCurrent(p->pManFraig, pObj);
// add the PI to the list
- if ( pObj->Level <= (unsigned)LevelMin || Dar_ObjIsPi(pObj) )
+ if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsPi(pObj) )
return 0;
// set the factor of this variable
// (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
@@ -282,7 +282,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, i
// explore the fanins
vFanins = Fra_ObjFaninVec( pObj );
Vec_PtrForEachEntry( vFanins, pFanin, i )
- Counter += Fra_SetActivityFactors_rec( p, Dar_Regular(pFanin), LevelMin, LevelMax );
+ Counter += Fra_SetActivityFactors_rec( p, Aig_Regular(pFanin), LevelMin, LevelMax );
return 1 + Counter;
}
@@ -297,7 +297,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, i
SeeAlso []
***********************************************************************/
-int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
int clk, LevelMin, LevelMax;
assert( pOld || pNew );
@@ -305,15 +305,15 @@ clk = clock();
// reset the active variables
veci_resize(&p->pSat->act_vars, 0);
// prepare for traversal
- Dar_ManIncrementTravId( p->pManFraig );
+ Aig_ManIncrementTravId( p->pManFraig );
// determine the min and max level to visit
assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
- LevelMax = DAR_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
+ LevelMax = AIG_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
// traverse
- if ( pOld && !Dar_ObjIsConst1(pOld) )
+ if ( pOld && !Aig_ObjIsConst1(pOld) )
Fra_SetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
- if ( pNew && !Dar_ObjIsConst1(pNew) )
+ if ( pNew && !Aig_ObjIsConst1(pNew) )
Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
//Fra_PrintActivity( p );
p->timeTrav += clock() - clk;
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 7207cfa2..beaa79fd 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -39,11 +39,11 @@
SeeAlso []
***********************************************************************/
-void Fra_NodeAssignRandom( Fra_Man_t * p, Dar_Obj_t * pObj )
+void Fra_NodeAssignRandom( Fra_Man_t * p, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i;
- assert( Dar_ObjIsPi(pObj) );
+ assert( Aig_ObjIsPi(pObj) );
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = Fra_ObjRandomSim();
@@ -60,11 +60,11 @@ void Fra_NodeAssignRandom( Fra_Man_t * p, Dar_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Fra_NodeAssignConst( Fra_Man_t * p, Dar_Obj_t * pObj, int fConst1 )
+void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1 )
{
unsigned * pSims;
int i;
- assert( Dar_ObjIsPi(pObj) );
+ assert( Aig_ObjIsPi(pObj) );
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = fConst1? ~(unsigned)0 : 0;
@@ -83,9 +83,9 @@ void Fra_NodeAssignConst( Fra_Man_t * p, Dar_Obj_t * pObj, int fConst1 )
***********************************************************************/
void Fra_AssignRandom( Fra_Man_t * p )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i;
- Dar_ManForEachPi( p->pManAig, pObj, i )
+ Aig_ManForEachPi( p->pManAig, pObj, i )
Fra_NodeAssignRandom( p, pObj );
}
@@ -102,17 +102,17 @@ void Fra_AssignRandom( Fra_Man_t * p )
***********************************************************************/
void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i, Limit;
- Dar_ManForEachPi( p->pManAig, pObj, i )
+ Aig_ManForEachPi( p->pManAig, pObj, i )
{
- Fra_NodeAssignConst( p, pObj, Dar_InfoHasBit(pPat, i) );
-// printf( "%d", Dar_InfoHasBit(pPat, i) );
+ Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, i) );
+// printf( "%d", Aig_InfoHasBit(pPat, i) );
}
// printf( "\n" );
- Limit = DAR_MIN( Dar_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
+ Limit = AIG_MIN( Aig_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
for ( i = 0; i < Limit; i++ )
- Dar_InfoXorBit( Fra_ObjSim( Dar_ManPi(p->pManAig,i) ), i+1 );
+ Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 );
}
/**Function*************************************************************
@@ -126,7 +126,7 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
SeeAlso []
***********************************************************************/
-int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj )
+int Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i;
@@ -148,7 +148,7 @@ int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Fra_NodeComplementSim( Fra_Man_t * p, Dar_Obj_t * pObj )
+void Fra_NodeComplementSim( Fra_Man_t * p, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i;
@@ -168,7 +168,7 @@ void Fra_NodeComplementSim( Fra_Man_t * p, Dar_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 )
+int Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
unsigned * pSims0, * pSims1;
int i;
@@ -192,20 +192,20 @@ int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 )
SeeAlso []
***********************************************************************/
-void Fra_NodeSimulate( Fra_Man_t * p, Dar_Obj_t * pObj )
+void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj )
{
unsigned * pSims, * pSims0, * pSims1;
int fCompl, fCompl0, fCompl1, i;
- assert( !Dar_IsComplement(pObj) );
- assert( Dar_ObjIsNode(pObj) );
+ assert( !Aig_IsComplement(pObj) );
+ assert( Aig_ObjIsNode(pObj) );
// get hold of the simulation information
pSims = Fra_ObjSim(pObj);
- pSims0 = Fra_ObjSim(Dar_ObjFanin0(pObj));
- pSims1 = Fra_ObjSim(Dar_ObjFanin1(pObj));
+ pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj));
+ pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj));
// get complemented attributes of the children using their random info
fCompl = pObj->fPhase;
- fCompl0 = Dar_ObjFaninPhase(Dar_ObjChild0(pObj));
- fCompl1 = Dar_ObjFaninPhase(Dar_ObjChild1(pObj));
+ fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj));
+ fCompl1 = Aig_ObjFaninPhase(Aig_ObjChild1(pObj));
// simulate
if ( fCompl0 && fCompl1 )
{
@@ -290,13 +290,13 @@ void Fra_SavePattern1( Fra_Man_t * p )
***********************************************************************/
void Fra_SavePattern( Fra_Man_t * p )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
- Dar_ManForEachPi( p->pManFraig, pObj, i )
+ Aig_ManForEachPi( p->pManFraig, pObj, i )
// Vec_PtrForEachEntry( p->vPiVars, pObj, i )
if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
- Dar_InfoSetBit( p->pPatWords, i );
+ Aig_InfoSetBit( p->pPatWords, i );
// Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
}
@@ -329,7 +329,7 @@ void Fra_CleanPatScores( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
-void Fra_AddToPatScores( Fra_Man_t * p, Dar_Obj_t * pClass, Dar_Obj_t * pClassNew )
+void Fra_AddToPatScores( Fra_Man_t * p, Aig_Obj_t * pClass, Aig_Obj_t * pClassNew )
{
unsigned * pSims0, * pSims1;
unsigned uDiff;
@@ -363,7 +363,7 @@ void Fra_AddToPatScores( Fra_Man_t * p, Dar_Obj_t * pClass, Dar_Obj_t * pClassNe
int Fra_SelectBestPat( Fra_Man_t * p )
{
unsigned * pSims;
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
for ( i = 1; i < nLimit; i++ )
{
@@ -379,11 +379,11 @@ int Fra_SelectBestPat( Fra_Man_t * p )
// printf( "Max score is %3d. ", MaxScore );
// copy the best pattern into the selected pattern
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
- Dar_ManForEachPi( p->pManAig, pObj, i )
+ Aig_ManForEachPi( p->pManAig, pObj, i )
{
pSims = Fra_ObjSim(pObj);
- if ( Dar_InfoHasBit(pSims, BestPat) )
- Dar_InfoSetBit(p->pPatWords, i);
+ if ( Aig_InfoHasBit(pSims, BestPat) )
+ Aig_InfoSetBit(p->pPatWords, i);
}
return MaxScore;
}
@@ -401,17 +401,17 @@ int Fra_SelectBestPat( Fra_Man_t * p )
***********************************************************************/
void Fra_SimulateOne( Fra_Man_t * p )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i, clk;
clk = clock();
- Dar_ManForEachNode( p->pManAig, pObj, i )
+ Aig_ManForEachNode( p->pManAig, pObj, i )
{
Fra_NodeSimulate( p, pObj );
/*
- if ( Dar_ObjFraig(pObj) == NULL )
+ if ( Aig_ObjFraig(pObj) == NULL )
printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase );
else
- printf( "%3d %3d %2d %d : ", pObj->Id, Dar_Regular(Dar_ObjFraig(pObj))->Id, Dar_ObjSatNum(Dar_Regular(Dar_ObjFraig(pObj))), pObj->fPhase );
+ printf( "%3d %3d %2d %d : ", pObj->Id, Aig_Regular(Aig_ObjFraig(pObj))->Id, Aig_ObjSatNum(Aig_Regular(Aig_ObjFraig(pObj))), pObj->fPhase );
Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 30 );
printf( "\n" );
*/
@@ -527,7 +527,7 @@ void Fra_Simulate( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
-void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj )
+void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i, k, BestPat, * pModel;
@@ -545,10 +545,10 @@ void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj )
// determine the best pattern
BestPat = i * 32 + k;
// fill in the counter-example data
- pModel = ALLOC( int, Dar_ManPiNum(p->pManFraig) );
- Dar_ManForEachPi( p->pManAig, pObj, i )
+ pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig) );
+ Aig_ManForEachPi( p->pManAig, pObj, i )
{
- pModel[i] = Dar_InfoHasBit(Fra_ObjSim(pObj), BestPat);
+ pModel[i] = Aig_InfoHasBit(Fra_ObjSim(pObj), BestPat);
// printf( "%d", pModel[i] );
}
// printf( "\n" );
@@ -571,26 +571,26 @@ void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj )
***********************************************************************/
int Fra_CheckOutputSims( Fra_Man_t * p )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i;
// make sure the reference simulation pattern does not detect the bug
- pObj = Dar_ManPo( p->pManAig, 0 );
- assert( Dar_ObjFanin0(pObj)->fPhase == (unsigned)Dar_ObjFaninC0(pObj) ); // Dar_ObjFaninPhase(Dar_ObjChild0(pObj)) == 0
- Dar_ManForEachPo( p->pManAig, pObj, i )
+ pObj = Aig_ManPo( p->pManAig, 0 );
+ assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); // Aig_ObjFaninPhase(Aig_ObjChild0(pObj)) == 0
+ Aig_ManForEachPo( p->pManAig, pObj, i )
{
// complement simulation info
-// if ( Dar_ObjFanin0(pObj)->fPhase ^ Dar_ObjFaninC0(pObj) ) // Dar_ObjFaninPhase(Dar_ObjChild0(pObj))
-// Fra_NodeComplementSim( p, Dar_ObjFanin0(pObj) );
+// if ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) ) // Aig_ObjFaninPhase(Aig_ObjChild0(pObj))
+// Fra_NodeComplementSim( p, Aig_ObjFanin0(pObj) );
// check
- if ( !Fra_NodeHasZeroSim( p, Dar_ObjFanin0(pObj) ) )
+ if ( !Fra_NodeHasZeroSim( p, Aig_ObjFanin0(pObj) ) )
{
// create the counter-example from this pattern
- Fra_CheckOutputSimsSavePattern( p, Dar_ObjFanin0(pObj) );
+ Fra_CheckOutputSimsSavePattern( p, Aig_ObjFanin0(pObj) );
return 1;
}
// complement simulation info
-// if ( Dar_ObjFanin0(pObj)->fPhase ^ Dar_ObjFaninC0(pObj) )
-// Fra_NodeComplementSim( p, Dar_ObjFanin0(pObj) );
+// if ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) )
+// Fra_NodeComplementSim( p, Aig_ObjFanin0(pObj) );
}
return 0;
}