abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraPart.c File Reference
#include "fra.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Fra_ManPartitionTest (Aig_Man_t *p, int nComLim)
 DECLARATIONS ///. More...
 
void Fra_ManPartitionTest2 (Aig_Man_t *p)
 

Function Documentation

ABC_NAMESPACE_IMPL_START void Fra_ManPartitionTest ( Aig_Man_t p,
int  nComLim 
)

DECLARATIONS ///.

CFile****************************************************************

FileName [fraPart.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Partitioning for induction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:
fraPart.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file fraPart.c.

46 {
47 // Bar_Progress_t * pProgress;
48  Vec_Vec_t * vSupps, * vSuppsIn;
49  Vec_Ptr_t * vSuppsNew;
50  Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn;
51  Vec_Int_t * vOverNew, * vQuantNew;
52  Aig_Obj_t * pObj;
53  int i, k, nCommon, CountOver, CountQuant;
54  int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar;
55  double Ratio, R;
56  abctime clk;
57 
58  nTotalSupp = 0;
59  nTotalSupp2 = 0;
60  Ratio = 0.0;
61 
62  // compute supports
63 clk = Abc_Clock();
64  vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
65 ABC_PRT( "Supports", Abc_Clock() - clk );
66  // remove last entry
67  Aig_ManForEachCo( p, pObj, i )
68  {
69  vSup = Vec_VecEntryInt( vSupps, i );
70  Vec_IntPop( vSup );
71  // remember support
72 // pObj->pNext = (Aig_Obj_t *)vSup;
73  }
74 
75  // create reverse supports
76 clk = Abc_Clock();
77  vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) );
78  Aig_ManForEachCo( p, pObj, i )
79  {
80  vSup = Vec_VecEntryInt( vSupps, i );
81  Vec_IntForEachEntry( vSup, Entry, k )
82  Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
83  }
84 ABC_PRT( "Inverse ", Abc_Clock() - clk );
85 
86 clk = Abc_Clock();
87  // compute extended supports
88  Largest = 0;
89  vSuppsNew = Vec_PtrAlloc( Aig_ManCoNum(p) );
90  vOverNew = Vec_IntAlloc( Aig_ManCoNum(p) );
91  vQuantNew = Vec_IntAlloc( Aig_ManCoNum(p) );
92 // pProgress = Bar_ProgressStart( stdout, Aig_ManCoNum(p) );
93  Aig_ManForEachCo( p, pObj, i )
94  {
95 // Bar_ProgressUpdate( pProgress, i, NULL );
96  // get old supports
97  vSup = Vec_VecEntryInt( vSupps, i );
98  if ( Vec_IntSize(vSup) < 2 )
99  continue;
100  // compute new supports
101  CountOver = CountQuant = 0;
102  vSupNew = Vec_IntDup( vSup );
103  // go through the nodes where the first var appears
104  Aig_ManForEachCo( p, pObj, k )
105 // iVar = Vec_IntEntry( vSup, 0 );
106 // vSupIn = Vec_VecEntry( vSuppsIn, iVar );
107 // Vec_IntForEachEntry( vSupIn, Entry, k )
108  {
109 // pObj = Aig_ManObj( p, Entry );
110  // get support of this output
111 // vSup2 = (Vec_Int_t *)pObj->pNext;
112  vSup2 = Vec_VecEntryInt( vSupps, k );
113  // count the number of common vars
114  nCommon = Vec_IntTwoCountCommon(vSup, vSup2);
115  if ( nCommon < 2 )
116  continue;
117  if ( nCommon > nComLim )
118  {
119  vSupNew = Vec_IntTwoMerge( vTemp = vSupNew, vSup2 );
120  Vec_IntFree( vTemp );
121  CountOver++;
122  }
123  else
124  CountQuant++;
125  }
126  // save the results
127  Vec_PtrPush( vSuppsNew, vSupNew );
128  Vec_IntPush( vOverNew, CountOver );
129  Vec_IntPush( vQuantNew, CountQuant );
130 
131  if ( Largest < Vec_IntSize(vSupNew) )
132  Largest = Vec_IntSize(vSupNew);
133 
134  nTotalSupp += Vec_IntSize(vSup);
135  nTotalSupp2 += Vec_IntSize(vSupNew);
136  if ( Vec_IntSize(vSup) )
137  R = Vec_IntSize(vSupNew) / Vec_IntSize(vSup);
138  else
139  R = 0;
140  Ratio += R;
141 
142  if ( R < 5.0 )
143  continue;
144 
145  printf( "%6d : ", i );
146  printf( "S = %5d. ", Vec_IntSize(vSup) );
147  printf( "SNew = %5d. ", Vec_IntSize(vSupNew) );
148  printf( "R = %7.2f. ", R );
149  printf( "Over = %5d. ", CountOver );
150  printf( "Quant = %5d. ", CountQuant );
151  printf( "\n" );
152 /*
153  Vec_IntForEachEntry( vSupNew, Entry, k )
154  printf( "%d ", Entry );
155  printf( "\n" );
156 */
157  }
158 // Bar_ProgressStop( pProgress );
159 ABC_PRT( "Scanning", Abc_Clock() - clk );
160 
161  // print cumulative statistics
162  printf( "PIs = %6d. POs = %6d. Lim = %3d. AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
163  Aig_ManCiNum(p), Aig_ManCoNum(p), nComLim,
164  nTotalSupp/Aig_ManCoNum(p), nTotalSupp2/Aig_ManCoNum(p),
165  Ratio/Aig_ManCoNum(p), Largest );
166 
167  Vec_VecFree( vSupps );
168  Vec_VecFree( vSuppsIn );
169  Vec_VecFree( (Vec_Vec_t *)vSuppsNew );
170  Vec_IntFree( vOverNew );
171  Vec_IntFree( vQuantNew );
172 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static void Vec_VecPush(Vec_Vec_t *p, int Level, void *Entry)
Definition: vecVec.h:456
static Vec_Int_t * Vec_IntDup(Vec_Int_t *pVec)
Definition: vecInt.h:214
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Ptr_t * Aig_ManSupports(Aig_Man_t *p)
Definition: aigPart.c:273
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static abctime Abc_Clock()
Definition: abc_global.h:279
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
static int Vec_IntTwoCountCommon(Vec_Int_t *vArr1, Vec_Int_t *vArr2)
Definition: vecInt.h:1528
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
static int Vec_IntPop(Vec_Int_t *p)
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static Vec_Int_t * Vec_IntTwoMerge(Vec_Int_t *vArr1, Vec_Int_t *vArr2)
Definition: vecInt.h:1684
static Vec_Vec_t * Vec_VecStart(int nSize)
Definition: vecVec.h:168
static Vec_Int_t * Vec_VecEntryInt(Vec_Vec_t *p, int i)
Definition: vecVec.h:276
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
#define ABC_PRT(a, t)
Definition: abc_global.h:220
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Fra_ManPartitionTest2 ( Aig_Man_t p)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file fraPart.c.

188 {
189  Vec_Vec_t * vSupps, * vSuppsIn;
190  Vec_Int_t * vSup, * vSup2, * vSup3;
191  Aig_Obj_t * pObj;
192  int Entry, Entry2, Entry3, Counter;
193  int i, k, m, n;
194  abctime clk;
195  char * pSupp;
196 
197  // compute supports
198 clk = Abc_Clock();
199  vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
200 ABC_PRT( "Supports", Abc_Clock() - clk );
201  // remove last entry
202  Aig_ManForEachCo( p, pObj, i )
203  {
204  vSup = Vec_VecEntryInt( vSupps, i );
205  Vec_IntPop( vSup );
206  // remember support
207 // pObj->pNext = (Aig_Obj_t *)vSup;
208  }
209 
210  // create reverse supports
211 clk = Abc_Clock();
212  vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) );
213  Aig_ManForEachCo( p, pObj, i )
214  {
215  if ( i == p->nAsserts )
216  break;
217  vSup = Vec_VecEntryInt( vSupps, i );
218  Vec_IntForEachEntry( vSup, Entry, k )
219  Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
220  }
221 ABC_PRT( "Inverse ", Abc_Clock() - clk );
222 
223  // create affective supports
224 clk = Abc_Clock();
225  pSupp = ABC_ALLOC( char, Aig_ManCiNum(p) );
226  Aig_ManForEachCo( p, pObj, i )
227  {
228  if ( i % 50 != 0 )
229  continue;
230  vSup = Vec_VecEntryInt( vSupps, i );
231  memset( pSupp, 0, sizeof(char) * Aig_ManCiNum(p) );
232  // go through each input of this output
233  Vec_IntForEachEntry( vSup, Entry, k )
234  {
235  pSupp[Entry] = 1;
236  vSup2 = Vec_VecEntryInt( vSuppsIn, Entry );
237  // go though each assert of this input
238  Vec_IntForEachEntry( vSup2, Entry2, m )
239  {
240  vSup3 = Vec_VecEntryInt( vSupps, Entry2 );
241  // go through each input of this assert
242  Vec_IntForEachEntry( vSup3, Entry3, n )
243  {
244  pSupp[Entry3] = 1;
245  }
246  }
247  }
248  // count the entries
249  Counter = 0;
250  for ( m = 0; m < Aig_ManCiNum(p); m++ )
251  Counter += pSupp[m];
252  printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
253  }
254  printf( "\n" );
255 ABC_PRT( "Extension ", Abc_Clock() - clk );
256 
257  ABC_FREE( pSupp );
258  Vec_VecFree( vSupps );
259  Vec_VecFree( vSuppsIn );
260 }
char * memset()
static void Vec_VecPush(Vec_Vec_t *p, int Level, void *Entry)
Definition: vecVec.h:456
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Ptr_t * Aig_ManSupports(Aig_Man_t *p)
Definition: aigPart.c:273
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static abctime Abc_Clock()
Definition: abc_global.h:279
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
static int Vec_IntPop(Vec_Int_t *p)
Definition: aig.h:69
static int Counter
static Vec_Vec_t * Vec_VecStart(int nSize)
Definition: vecVec.h:168
static Vec_Int_t * Vec_VecEntryInt(Vec_Vec_t *p, int i)
Definition: vecVec.h:276
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define ABC_PRT(a, t)
Definition: abc_global.h:220
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54