diff options
Diffstat (limited to 'src/aig/fra/fraAnd.c')
-rw-r--r-- | src/aig/fra/fraAnd.c | 52 |
1 files changed, 26 insertions, 26 deletions
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 ); } //////////////////////////////////////////////////////////////////////// |