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

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START
Rwr_Node_t * 		Rwr_ManTryNode (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1, int fExor, int Level, int Volume)
 DECLARATIONS ///. More...
 
static void Rwr_MarkUsed_rec (Rwr_Man_t *p, Rwr_Node_t *pNode)
 
void Rwr_ManPrecompute (Rwr_Man_t *p)
 FUNCTION DEFINITIONS ///. More...
 
Rwr_Node_t * Rwr_ManAddNode (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1, int fExor, int Level, int Volume)
 
Rwr_Node_t * Rwr_ManAddVar (Rwr_Man_t *p, unsigned uTruth, int fPrecompute)
 
void Rwr_Trav_rec (Rwr_Man_t *p, Rwr_Node_t *pNode, int *pVolume)
 
int Rwr_ManNodeVolume (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1)
 
void Rwr_ManIncTravId (Rwr_Man_t *p)
 

Function Documentation

Rwr_Node_t* Rwr_ManAddNode ( Rwr_Man_t *  p,
Rwr_Node_t *  p0,
Rwr_Node_t *  p1,
int  fExor,
int  Level,
int  Volume 
)

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file rwrLib.c.

207 {
208  Rwr_Node_t * pNew;
209  unsigned uTruth;
210  // compute truth table, leve, volume
211  p->nConsidered++;
212  if ( fExor )
213  uTruth = (p0->uTruth ^ p1->uTruth);
214  else
215  uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) &
216  (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
217  // create the new node
218  pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
219  pNew->Id = p->vForest->nSize;
220  pNew->TravId = 0;
221  pNew->uTruth = uTruth;
222  pNew->Level = Level;
223  pNew->Volume = Volume;
224  pNew->fUsed = 0;
225  pNew->fExor = fExor;
226  pNew->p0 = p0;
227  pNew->p1 = p1;
228  pNew->pNext = NULL;
229  Vec_PtrPush( p->vForest, pNew );
230  // do not add if the node is not essential
231  if ( uTruth != p->puCanons[uTruth] )
232  return pNew;
233 
234  // add to the list
235  p->nAdded++;
236  if ( p->pTable[uTruth] == NULL )
237  p->nClasses++;
238  Rwr_ListAddToTail( p->pTable + uTruth, pNew );
239  return pNew;
240 }
Rwr_Node_t_::fUsed
unsigned fUsed
Definition: rwr.h:108
Rwr_Man_t_::nConsidered
int nConsidered
Definition: rwr.h:68
Rwr_Node_t_::Id
int Id
Definition: rwr.h:100
Rwr_Node_t_::Level
unsigned Level
Definition: rwr.h:107
Rwr_Man_t_::puCanons
unsigned short * puCanons
Definition: rwr.h:54
Rwr_Node_t_::uTruth
unsigned uTruth
Definition: rwr.h:105
Rwr_IsComplement
static int Rwr_IsComplement(Rwr_Node_t *p)
Definition: rwr.h:116
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Rwr_Node_t_::p0
Rwr_Node_t * p0
Definition: rwr.h:110
Extra_MmFixedEntryFetch
char * Extra_MmFixedEntryFetch(Extra_MmFixed_t *p)
Definition: extraUtilMemory.c:202
Rwr_Man_t_::pMmNode
Extra_MmFixed_t * pMmNode
Definition: rwr.h:65
Rwr_Node_t_::TravId
int TravId
Definition: rwr.h:101
Rwr_Node_t_::fExor
unsigned fExor
Definition: rwr.h:109
Rwr_Node_t_
Definition: rwr.h:98
Rwr_Man_t_::nClasses
int nClasses
Definition: rwr.h:70
Rwr_Man_t_::pTable
Rwr_Node_t ** pTable
Definition: rwr.h:63
Rwr_Node_t_::p1
Rwr_Node_t * p1
Definition: rwr.h:111
Rwr_Node_t_::Volume
unsigned Volume
Definition: rwr.h:106
Rwr_Man_t_::nAdded
int nAdded
Definition: rwr.h:69
Rwr_ListAddToTail
void Rwr_ListAddToTail(Rwr_Node_t **ppList, Rwr_Node_t *pNode)
Definition: rwrUtil.c:619
Rwr_Node_t_::pNext
Rwr_Node_t * pNext
Definition: rwr.h:112
Rwr_Regular
static Rwr_Node_t * Rwr_Regular(Rwr_Node_t *p)
Definition: rwr.h:117
Rwr_Man_t_::vForest
Vec_Ptr_t * vForest
Definition: rwr.h:62
Rwr_Node_t* Rwr_ManAddVar ( Rwr_Man_t *  p,
unsigned  uTruth,
int  fPrecompute 
)

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file rwrLib.c.

254 {
255  Rwr_Node_t * pNew;
256  pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
257  pNew->Id = p->vForest->nSize;
258  pNew->TravId = 0;
259  pNew->uTruth = uTruth;
260  pNew->Level = 0;
261  pNew->Volume = 0;
262  pNew->fUsed = 1;
263  pNew->fExor = 0;
264  pNew->p0 = NULL;
265  pNew->p1 = NULL;
266  pNew->pNext = NULL;
267  Vec_PtrPush( p->vForest, pNew );
268  if ( fPrecompute )
269  Rwr_ListAddToTail( p->pTable + uTruth, pNew );
270  return pNew;
271 }
Rwr_Node_t_::fUsed
unsigned fUsed
Definition: rwr.h:108
Rwr_Node_t_::Id
int Id
Definition: rwr.h:100
Rwr_Node_t_::Level
unsigned Level
Definition: rwr.h:107
Rwr_Node_t_::uTruth
unsigned uTruth
Definition: rwr.h:105
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Rwr_Node_t_::p0
Rwr_Node_t * p0
Definition: rwr.h:110
Extra_MmFixedEntryFetch
char * Extra_MmFixedEntryFetch(Extra_MmFixed_t *p)
Definition: extraUtilMemory.c:202
Rwr_Man_t_::pMmNode
Extra_MmFixed_t * pMmNode
Definition: rwr.h:65
Rwr_Node_t_::TravId
int TravId
Definition: rwr.h:101
Rwr_Node_t_::fExor
unsigned fExor
Definition: rwr.h:109
Rwr_Node_t_
Definition: rwr.h:98
Rwr_Man_t_::pTable
Rwr_Node_t ** pTable
Definition: rwr.h:63
Rwr_Node_t_::p1
Rwr_Node_t * p1
Definition: rwr.h:111
Rwr_Node_t_::Volume
unsigned Volume
Definition: rwr.h:106
Rwr_ListAddToTail
void Rwr_ListAddToTail(Rwr_Node_t **ppList, Rwr_Node_t *pNode)
Definition: rwrUtil.c:619
Rwr_Node_t_::pNext
Rwr_Node_t * pNext
Definition: rwr.h:112
Rwr_Man_t_::vForest
Vec_Ptr_t * vForest
Definition: rwr.h:62
void Rwr_ManIncTravId ( Rwr_Man_t *  p)

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file rwrLib.c.

351 {
352  Rwr_Node_t * pNode;
353  int i;
354  if ( p->nTravIds++ < 0x8FFFFFFF )
355  return;
356  Vec_PtrForEachEntry( Rwr_Node_t *, p->vForest, pNode, i )
357  pNode->TravId = 0;
358  p->nTravIds = 1;
359 }
Rwr_Man_t_::nTravIds
int nTravIds
Definition: rwr.h:67
Rwr_Node_t_
Definition: rwr.h:98
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Rwr_Man_t_::vForest
Vec_Ptr_t * vForest
Definition: rwr.h:62
int Rwr_ManNodeVolume ( Rwr_Man_t *  p,
Rwr_Node_t *  p0,
Rwr_Node_t *  p1 
)

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 330 of file rwrLib.c.

331 {
332  int Volume = 0;
333  Rwr_ManIncTravId( p );
334  Rwr_Trav_rec( p, p0, &Volume );
335  Rwr_Trav_rec( p, p1, &Volume );
336  return Volume;
337 }
Rwr_ManIncTravId
void Rwr_ManIncTravId(Rwr_Man_t *p)
Definition: rwrLib.c:350
Rwr_Trav_rec
void Rwr_Trav_rec(Rwr_Man_t *p, Rwr_Node_t *pNode, int *pVolume)
Definition: rwrLib.c:307
void Rwr_ManPrecompute ( Rwr_Man_t *  p)

FUNCTION DEFINITIONS ///.

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

Synopsis [Precomputes the forest in the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file rwrLib.c.

49 {
50  Rwr_Node_t * p0, * p1;
51  int i, k, Level, Volume;
52  int LevelOld = -1;
53  int nNodes;
54 
55  Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 1 )
56  Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p1, k, 1 )
57  {
58  if ( LevelOld < (int)p0->Level )
59  {
60  LevelOld = p0->Level;
61  printf( "Starting level %d (at %d nodes).\n", LevelOld+1, i );
62  printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
63  p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
64  }
65 
66  if ( k == i )
67  break;
68 // if ( p0->Level + p1->Level > 6 ) // hard
69 // break;
70 
71  if ( p0->Level + p1->Level > 5 ) // easy
72  break;
73 
74 // if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) )
75 // break;
76 
77  // compute the level and volume of the new nodes
78  Level = 1 + Abc_MaxInt( p0->Level, p1->Level );
79  Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
80  // try four different AND nodes
81  Rwr_ManTryNode( p, p0 , p1 , 0, Level, Volume );
82  Rwr_ManTryNode( p, Rwr_Not(p0), p1 , 0, Level, Volume );
83  Rwr_ManTryNode( p, p0 , Rwr_Not(p1), 0, Level, Volume );
84  Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume );
85  // try EXOR
86  Rwr_ManTryNode( p, p0 , p1 , 1, Level, Volume + 1 );
87  // report the progress
88  if ( p->nConsidered % 50000000 == 0 )
89  printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
90  p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
91  // quit after some time
92  if ( p->vForest->nSize == RWR_LIMIT + 5 )
93  {
94  printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
95  p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
96  goto save;
97  }
98  }
99 save :
100 
101  // mark the relevant ones
102  Rwr_ManIncTravId( p );
103  k = 5;
104  nNodes = 0;
105  Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 5 )
106  if ( p0->uTruth == p->puCanons[p0->uTruth] )
107  {
108  Rwr_MarkUsed_rec( p, p0 );
109  nNodes++;
110  }
111 
112  // compact the array by throwing away non-canonical
113  k = 5;
114  Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 5 )
115  if ( p0->fUsed )
116  {
117  p->vForest->pArray[k] = p0;
118  p0->Id = k++;
119  }
120  p->vForest->nSize = k;
121  printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize );
122 }
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
Rwr_Man_t_::nConsidered
int nConsidered
Definition: rwr.h:68
Rwr_MarkUsed_rec
static void Rwr_MarkUsed_rec(Rwr_Man_t *p, Rwr_Node_t *pNode)
Definition: rwrLib.c:286
Rwr_Node_t_::Id
int Id
Definition: rwr.h:100
Rwr_Node_t_::Level
unsigned Level
Definition: rwr.h:107
Rwr_ManNodeVolume
int Rwr_ManNodeVolume(Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1)
Definition: rwrLib.c:330
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
RWR_LIMIT
#define RWR_LIMIT
INCLUDES ///.
Definition: rwr.h:45
Rwr_ManTryNode
static ABC_NAMESPACE_IMPL_START Rwr_Node_t * Rwr_ManTryNode(Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1, int fExor, int Level, int Volume)
DECLARATIONS ///.
Definition: rwrLib.c:135
if
if(last==0)
Definition: sparse_int.h:34
Rwr_ManIncTravId
void Rwr_ManIncTravId(Rwr_Man_t *p)
Definition: rwrLib.c:350
Rwr_Node_t_
Definition: rwr.h:98
Rwr_Man_t_::nClasses
int nClasses
Definition: rwr.h:70
Rwr_Not
static Rwr_Node_t * Rwr_Not(Rwr_Node_t *p)
Definition: rwr.h:118
Rwr_Man_t_::vForest
Vec_Ptr_t * vForest
Definition: rwr.h:62
Rwr_Node_t * Rwr_ManTryNode ( Rwr_Man_t *  p,
Rwr_Node_t *  p0,
Rwr_Node_t *  p1,
int  fExor,
int  Level,
int  Volume 
)
static

DECLARATIONS ///.

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

FileName [rwrLib.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
rwrLib.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 135 of file rwrLib.c.

136 {
137  Rwr_Node_t * pOld, * pNew, ** ppPlace;
138  unsigned uTruth;
139  // compute truth table, level, volume
140  p->nConsidered++;
141  if ( fExor )
142  {
143 // printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id );
144  uTruth = (p0->uTruth ^ p1->uTruth);
145  }
146  else
147  uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) &
148  (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
149  // skip non-practical classes
150  if ( Level > 2 && !p->pPractical[p->puCanons[uTruth]] )
151  return NULL;
152  // enumerate through the nodes with the same canonical form
153  ppPlace = p->pTable + uTruth;
154  for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext )
155  {
156  if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume )
157  return NULL;
158  if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
159  return NULL;
160 // if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume )
161 // return NULL;
162  }
163 /*
164  // enumerate through the nodes with the opposite polarity
165  for ( pOld = p->pTable[~uTruth & 0xFFFF]; pOld; pOld = pOld->pNext )
166  {
167  if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume )
168  return NULL;
169  if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
170  return NULL;
171 // if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume )
172 // return NULL;
173  }
174 */
175  // count the classes
176  if ( p->pTable[uTruth] == NULL && p->puCanons[uTruth] == uTruth )
177  p->nClasses++;
178  // create the new node
179  pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
180  pNew->Id = p->vForest->nSize;
181  pNew->TravId = 0;
182  pNew->uTruth = uTruth;
183  pNew->Level = Level;
184  pNew->Volume = Volume;
185  pNew->fUsed = 0;
186  pNew->fExor = fExor;
187  pNew->p0 = p0;
188  pNew->p1 = p1;
189  pNew->pNext = NULL;
190  Vec_PtrPush( p->vForest, pNew );
191  *ppPlace = pNew;
192  return pNew;
193 }
Rwr_Node_t_::fUsed
unsigned fUsed
Definition: rwr.h:108
Rwr_Man_t_::nConsidered
int nConsidered
Definition: rwr.h:68
Rwr_Node_t_::Id
int Id
Definition: rwr.h:100
Rwr_Node_t_::Level
unsigned Level
Definition: rwr.h:107
Rwr_Man_t_::puCanons
unsigned short * puCanons
Definition: rwr.h:54
Rwr_Node_t_::uTruth
unsigned uTruth
Definition: rwr.h:105
Rwr_IsComplement
static int Rwr_IsComplement(Rwr_Node_t *p)
Definition: rwr.h:116
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Rwr_Node_t_::p0
Rwr_Node_t * p0
Definition: rwr.h:110
Extra_MmFixedEntryFetch
char * Extra_MmFixedEntryFetch(Extra_MmFixed_t *p)
Definition: extraUtilMemory.c:202
Rwr_Man_t_::pMmNode
Extra_MmFixed_t * pMmNode
Definition: rwr.h:65
Rwr_Node_t_::TravId
int TravId
Definition: rwr.h:101
Rwr_Node_t_::fExor
unsigned fExor
Definition: rwr.h:109
Rwr_Node_t_
Definition: rwr.h:98
Rwr_Man_t_::nClasses
int nClasses
Definition: rwr.h:70
Rwr_Man_t_::pTable
Rwr_Node_t ** pTable
Definition: rwr.h:63
Rwr_Node_t_::p1
Rwr_Node_t * p1
Definition: rwr.h:111
Rwr_Man_t_::pPractical
char * pPractical
Definition: rwr.h:59
Rwr_Node_t_::Volume
unsigned Volume
Definition: rwr.h:106
Rwr_Node_t_::pNext
Rwr_Node_t * pNext
Definition: rwr.h:112
Rwr_Regular
static Rwr_Node_t * Rwr_Regular(Rwr_Node_t *p)
Definition: rwr.h:117
Rwr_Man_t_::vForest
Vec_Ptr_t * vForest
Definition: rwr.h:62
void Rwr_MarkUsed_rec ( Rwr_Man_t *  p,
Rwr_Node_t *  pNode 
)
static

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 286 of file rwrLib.c.

287 {
288  if ( pNode->fUsed || pNode->TravId == p->nTravIds )
289  return;
290  pNode->TravId = p->nTravIds;
291  pNode->fUsed = 1;
292  Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) );
293  Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) );
294 }
Rwr_Node_t_::fUsed
unsigned fUsed
Definition: rwr.h:108
Rwr_MarkUsed_rec
static void Rwr_MarkUsed_rec(Rwr_Man_t *p, Rwr_Node_t *pNode)
Definition: rwrLib.c:286
Rwr_Node_t_::p0
Rwr_Node_t * p0
Definition: rwr.h:110
Rwr_Man_t_::nTravIds
int nTravIds
Definition: rwr.h:67
Rwr_Node_t_::TravId
int TravId
Definition: rwr.h:101
Rwr_Node_t_::p1
Rwr_Node_t * p1
Definition: rwr.h:111
Rwr_Regular
static Rwr_Node_t * Rwr_Regular(Rwr_Node_t *p)
Definition: rwr.h:117
void Rwr_Trav_rec ( Rwr_Man_t *  p,
Rwr_Node_t *  pNode,
int *  pVolume 
)

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file rwrLib.c.

308 {
309  if ( pNode->fUsed || pNode->TravId == p->nTravIds )
310  return;
311  pNode->TravId = p->nTravIds;
312  (*pVolume)++;
313  if ( pNode->fExor )
314  (*pVolume)++;
315  Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume );
316  Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume );
317 }
Rwr_Node_t_::fUsed
unsigned fUsed
Definition: rwr.h:108
Rwr_Node_t_::p0
Rwr_Node_t * p0
Definition: rwr.h:110
Rwr_Man_t_::nTravIds
int nTravIds
Definition: rwr.h:67
Rwr_Node_t_::TravId
int TravId
Definition: rwr.h:101
Rwr_Node_t_::fExor
unsigned fExor
Definition: rwr.h:109
Rwr_Node_t_::p1
Rwr_Node_t * p1
Definition: rwr.h:111
Rwr_Trav_rec
void Rwr_Trav_rec(Rwr_Man_t *p, Rwr_Node_t *pNode, int *pVolume)
Definition: rwrLib.c:307
Rwr_Regular
static Rwr_Node_t * Rwr_Regular(Rwr_Node_t *p)
Definition: rwr.h:117