src/aig/cnf/cnfUtil.c File Reference
#include "cnf.h"
Go to the source code of this file.
Functions | |
| int | Aig_ManScanMapping_rec (Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped) |
| Vec_Ptr_t * | Aig_ManScanMapping (Cnf_Man_t *p, int fCollect) |
| int | Cnf_ManScanMapping_rec (Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped, int fPreorder) |
| Vec_Ptr_t * | Cnf_ManScanMapping (Cnf_Man_t *p, int fCollect, int fPreorder) |
Function Documentation
Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description [Collects the nodes in reverse topological order.]
SideEffects []
SeeAlso []
Definition at line 86 of file cnfUtil.c.
00087 { 00088 Vec_Ptr_t * vMapped = NULL; 00089 Aig_Obj_t * pObj; 00090 int i; 00091 // clean all references 00092 Aig_ManForEachObj( p->pManAig, pObj, i ) 00093 pObj->nRefs = 0; 00094 // allocate the array 00095 if ( fCollect ) 00096 vMapped = Vec_PtrAlloc( 1000 ); 00097 // collect nodes reachable from POs in the DFS order through the best cuts 00098 p->aArea = 0; 00099 Aig_ManForEachPo( p->pManAig, pObj, i ) 00100 p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped ); 00101 // printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); 00102 return vMapped; 00103 }
CFile****************************************************************
FileName [cnfUtil.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [
- Id
- cnfUtil.c,v 1.00 2007/04/28 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file cnfUtil.c.
00043 { 00044 Aig_Obj_t * pLeaf; 00045 Dar_Cut_t * pCutBest; 00046 int aArea, i; 00047 if ( pObj->nRefs++ || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) ) 00048 return 0; 00049 assert( Aig_ObjIsAnd(pObj) ); 00050 // collect the node first to derive pre-order 00051 if ( vMapped ) 00052 Vec_PtrPush( vMapped, pObj ); 00053 // visit the transitive fanin of the selected cut 00054 if ( pObj->fMarkB ) 00055 { 00056 Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 ); 00057 Aig_ObjCollectSuper( pObj, vSuper ); 00058 aArea = Vec_PtrSize(vSuper) + 1; 00059 Vec_PtrForEachEntry( vSuper, pLeaf, i ) 00060 aArea += Aig_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped ); 00061 Vec_PtrFree( vSuper ); 00063 pObj->fMarkB = 1; 00064 } 00065 else 00066 { 00067 pCutBest = Dar_ObjBestCut( pObj ); 00068 aArea = Cnf_CutSopCost( p, pCutBest ); 00069 Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i ) 00070 aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped ); 00071 } 00072 return aArea; 00073 }
Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description [Collects the nodes in reverse topological order.]
SideEffects []
SeeAlso []
Definition at line 165 of file cnfUtil.c.
00166 { 00167 Vec_Ptr_t * vMapped = NULL; 00168 Aig_Obj_t * pObj; 00169 int i; 00170 // clean all references 00171 Aig_ManForEachObj( p->pManAig, pObj, i ) 00172 pObj->nRefs = 0; 00173 // allocate the array 00174 if ( fCollect ) 00175 vMapped = Vec_PtrAlloc( 1000 ); 00176 // collect nodes reachable from POs in the DFS order through the best cuts 00177 p->aArea = 0; 00178 Aig_ManForEachPo( p->pManAig, pObj, i ) 00179 p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder ); 00180 // printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); 00181 return vMapped; 00182 }
Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description []
SideEffects []
SeeAlso []
Definition at line 116 of file cnfUtil.c.
00117 { 00118 Aig_Obj_t * pLeaf; 00119 Cnf_Cut_t * pCutBest; 00120 int aArea, i; 00121 if ( pObj->nRefs++ || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) ) 00122 return 0; 00123 assert( Aig_ObjIsAnd(pObj) ); 00124 assert( pObj->pData != NULL ); 00125 // add the node to the mapping 00126 if ( vMapped && fPreorder ) 00127 Vec_PtrPush( vMapped, pObj ); 00128 // visit the transitive fanin of the selected cut 00129 if ( pObj->fMarkB ) 00130 { 00131 Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 ); 00132 Aig_ObjCollectSuper( pObj, vSuper ); 00133 aArea = Vec_PtrSize(vSuper) + 1; 00134 Vec_PtrForEachEntry( vSuper, pLeaf, i ) 00135 aArea += Cnf_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped, fPreorder ); 00136 Vec_PtrFree( vSuper ); 00138 pObj->fMarkB = 1; 00139 } 00140 else 00141 { 00142 pCutBest = pObj->pData; 00143 assert( pCutBest->Cost < 127 ); 00144 aArea = pCutBest->Cost; 00145 Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i ) 00146 aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped, fPreorder ); 00147 } 00148 // add the node to the mapping 00149 if ( vMapped && !fPreorder ) 00150 Vec_PtrPush( vMapped, pObj ); 00151 return aArea; 00152 }
