abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
cnfCut.c File Reference
#include "cnf.h"
#include "bool/kit/kit.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
Cnf_Cut_t * 		Cnf_CutAlloc (Cnf_Man_t *p, int nLeaves)
 DECLARATIONS ///. More...
 
void Cnf_CutFree (Cnf_Cut_t *pCut)
 
Cnf_Cut_t * Cnf_CutCreate (Cnf_Man_t *p, Aig_Obj_t *pObj)
 
void Cnf_CutPrint (Cnf_Cut_t *pCut)
 
void Cnf_CutDeref (Cnf_Man_t *p, Cnf_Cut_t *pCut)
 
void Cnf_CutRef (Cnf_Man_t *p, Cnf_Cut_t *pCut)
 
void Cnf_CutUpdateRefs (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, Cnf_Cut_t *pCutRes)
 
static int Cnf_CutMergeLeaves (Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, int *pFanins)
 
static unsigned Cnf_TruthPhase (Cnf_Cut_t *pCut, Cnf_Cut_t *pCut1)
 
void Cnf_CutRemoveIthVar (Cnf_Cut_t *pCut, int iVar, int iFan)
 
void Cnf_CutInsertIthVar (Cnf_Cut_t *pCut, int iVar, int iFan)
 
Cnf_Cut_t * Cnf_CutCompose (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, int iFan)
 

Function Documentation

ABC_NAMESPACE_IMPL_START Cnf_Cut_t* Cnf_CutAlloc ( Cnf_Man_t *  p,
int  nLeaves 
)

DECLARATIONS ///.

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

FileName [cnfCut.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:
cnfCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file cnfCut.c.

47 {
48  Cnf_Cut_t * pCut;
49  int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Abc_TruthWordNum(nLeaves);
50  pCut = (Cnf_Cut_t *)Aig_MmFlexEntryFetch( p->pMemCuts, nSize );
51  pCut->nFanins = nLeaves;
52  pCut->nWords = Abc_TruthWordNum(nLeaves);
53  pCut->vIsop[0] = pCut->vIsop[1] = NULL;
54  return pCut;
55 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_MmFlexEntryFetch
char * Aig_MmFlexEntryFetch(Aig_MmFlex_t *p, int nBytes)
Definition: aigMem.c:366
Abc_TruthWordNum
static int Abc_TruthWordNum(int nVars)
Definition: abc_global.h:256
Cnf_Cut_t_::nWords
short nWords
Definition: cnf.h:75
Cnf_Cut_t_::vIsop
Vec_Int_t * vIsop[2]
Definition: cnf.h:76
Cnf_Cut_t_
Definition: cnf.h:71
Cnf_Cut_t
struct Cnf_Cut_t_ Cnf_Cut_t
Definition: cnf.h:53
Cnf_Cut_t_::nFanins
char nFanins
Definition: cnf.h:73
Cnf_Cut_t* Cnf_CutCompose ( Cnf_Man_t *  p,
Cnf_Cut_t *  pCut,
Cnf_Cut_t *  pCutFan,
int  iFan 
)

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

Synopsis [Merges two cuts.]

Description [Returns NULL of the cuts cannot be merged.]

SideEffects []

SeeAlso []

Definition at line 294 of file cnfCut.c.

295 {
296  Cnf_Cut_t * pCutRes;
297  static int pFanins[32];
298  unsigned * pTruth, * pTruthFan, * pTruthRes;
299  unsigned * pTop = p->pTruths[0], * pFan = p->pTruths[2], * pTemp = p->pTruths[3];
300  unsigned uPhase, uPhaseFan;
301  int i, iVar, nFanins, RetValue;
302 
303  // make sure the second cut is the fanin of the first
304  for ( iVar = 0; iVar < pCut->nFanins; iVar++ )
305  if ( pCut->pFanins[iVar] == iFan )
306  break;
307  assert( iVar < pCut->nFanins );
308  // remove this variable
309  Cnf_CutRemoveIthVar( pCut, iVar, iFan );
310  // merge leaves of the cuts
311  nFanins = Cnf_CutMergeLeaves( pCut, pCutFan, pFanins );
312  if ( nFanins+1 > p->nMergeLimit )
313  {
314  Cnf_CutInsertIthVar( pCut, iVar, iFan );
315  return NULL;
316  }
317  // create new cut
318  pCutRes = Cnf_CutAlloc( p, nFanins );
319  memcpy( pCutRes->pFanins, pFanins, sizeof(int) * nFanins );
320  assert( pCutRes->nFanins <= pCut->nFanins + pCutFan->nFanins );
321 
322  // derive its truth table
323  // get the truth tables in the composition space
324  pTruth = Cnf_CutTruth(pCut);
325  pTruthFan = Cnf_CutTruth(pCutFan);
326  pTruthRes = Cnf_CutTruth(pCutRes);
327  for ( i = 0; i < 2*pCutRes->nWords; i++ )
328  pTop[i] = pTruth[i % pCut->nWords];
329  for ( i = 0; i < pCutRes->nWords; i++ )
330  pFan[i] = pTruthFan[i % pCutFan->nWords];
331  // move the variable to the end
332  uPhase = Kit_BitMask( pCutRes->nFanins+1 ) & ~(1 << iVar);
333  Kit_TruthShrink( pTemp, pTop, pCutRes->nFanins, pCutRes->nFanins+1, uPhase, 1 );
334  // compute the phases
335  uPhase = Cnf_TruthPhase( pCutRes, pCut ) | (1 << pCutRes->nFanins);
336  uPhaseFan = Cnf_TruthPhase( pCutRes, pCutFan );
337  // permute truth-tables to the common support
338  Kit_TruthStretch( pTemp, pTop, pCut->nFanins+1, pCutRes->nFanins+1, uPhase, 1 );
339  Kit_TruthStretch( pTemp, pFan, pCutFan->nFanins, pCutRes->nFanins, uPhaseFan, 1 );
340  // perform Boolean operation
341  Kit_TruthMux( pTruthRes, pTop, pTop+pCutRes->nWords, pFan, pCutRes->nFanins );
342  // return the cut to its original condition
343  Cnf_CutInsertIthVar( pCut, iVar, iFan );
344  // consider the simple case
345  if ( pCutRes->nFanins < 5 )
346  {
347  pCutRes->Cost = p->pSopSizes[0xFFFF & *pTruthRes] + p->pSopSizes[0xFFFF & ~*pTruthRes];
348  return pCutRes;
349  }
350 
351  // derive ISOP for positive phase
352  RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
353  pCutRes->vIsop[1] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
354  // derive ISOP for negative phase
355  Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
356  RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
357  pCutRes->vIsop[0] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
358  Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
359 
360  // compute the cut cost
361  if ( pCutRes->vIsop[0] == NULL || pCutRes->vIsop[1] == NULL )
362  pCutRes->Cost = 127;
363  else if ( Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]) > 127 )
364  pCutRes->Cost = 127;
365  else
366  pCutRes->Cost = Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]);
367  return pCutRes;
368 }
Cnf_CutInsertIthVar
void Cnf_CutInsertIthVar(Cnf_Cut_t *pCut, int iVar, int iFan)
Definition: cnfCut.c:274
Vec_IntDup
static Vec_Int_t * Vec_IntDup(Vec_Int_t *pVec)
Definition: vecInt.h:214
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
memcpy
char * memcpy()
Kit_TruthStretch
void Kit_TruthStretch(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition: kitTruth.c:166
Cnf_Cut_t_::nWords
short nWords
Definition: cnf.h:75
for
for(p=first;p->value< newval;p=p->next)
Cnf_Cut_t_::Cost
char Cost
Definition: cnf.h:74
Cnf_Cut_t_::vIsop
Vec_Int_t * vIsop[2]
Definition: cnf.h:76
Kit_TruthMux
static void Kit_TruthMux(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, unsigned *pCtrl, int nVars)
Definition: kit.h:457
Cnf_CutTruth
static unsigned * Cnf_CutTruth(Cnf_Cut_t *pCut)
Definition: cnf.h:103
Cnf_Cut_t_
Definition: cnf.h:71
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
FUNCTION DEFINITIONS ///.
Definition: kitIsop.c:55
Cnf_Cut_t_::pFanins
int pFanins[0]
Definition: cnf.h:77
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
Cnf_CutAlloc
ABC_NAMESPACE_IMPL_START Cnf_Cut_t * Cnf_CutAlloc(Cnf_Man_t *p, int nLeaves)
DECLARATIONS ///.
Definition: cnfCut.c:46
Kit_TruthShrink
void Kit_TruthShrink(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition: kitTruth.c:200
Cnf_CutMergeLeaves
static int Cnf_CutMergeLeaves(Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, int *pFanins)
Definition: cnfCut.c:196
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
assert
#define assert(ex)
Definition: util_old.h:213
Cnf_CutRemoveIthVar
void Cnf_CutRemoveIthVar(Cnf_Cut_t *pCut, int iVar, int iFan)
Definition: cnfCut.c:254
Cnf_Cut_t_::nFanins
char nFanins
Definition: cnf.h:73
Cnf_TruthPhase
static unsigned Cnf_TruthPhase(Cnf_Cut_t *pCut, Cnf_Cut_t *pCut1)
Definition: cnfCut.c:226
Kit_BitMask
static unsigned Kit_BitMask(int nBits)
Definition: kit.h:225
Cnf_Cut_t* Cnf_CutCreate ( Cnf_Man_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Creates cut for the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file cnfCut.c.

88 {
89  Dar_Cut_t * pCutBest;
90  Cnf_Cut_t * pCut;
91  unsigned * pTruth;
92  assert( Aig_ObjIsNode(pObj) );
93  pCutBest = Dar_ObjBestCut( pObj );
94  assert( pCutBest != NULL );
95  assert( pCutBest->nLeaves <= 4 );
96  pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
97  memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
98  pTruth = Cnf_CutTruth(pCut);
99  *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
100  pCut->Cost = Cnf_CutSopCost( p, pCutBest );
101  return pCut;
102 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cnf_CutSopCost
static int Cnf_CutSopCost(Cnf_Man_t *p, Dar_Cut_t *pCut)
Definition: cnf.h:99
Dar_Cut_t_::uTruth
unsigned uTruth
Definition: darInt.h:58
memcpy
char * memcpy()
Cnf_Cut_t_::Cost
char Cost
Definition: cnf.h:74
Cnf_CutTruth
static unsigned * Cnf_CutTruth(Cnf_Cut_t *pCut)
Definition: cnf.h:103
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Dar_Cut_t_::pLeaves
int pLeaves[4]
Definition: darInt.h:63
Cnf_Cut_t_
Definition: cnf.h:71
Cnf_Cut_t_::pFanins
int pFanins[0]
Definition: cnf.h:77
Dar_Cut_t_
Definition: darInt.h:55
Dar_ObjBestCut
static Dar_Cut_t * Dar_ObjBestCut(Aig_Obj_t *pObj)
Definition: cnf.h:97
Dar_Cut_t_::nLeaves
unsigned nLeaves
Definition: darInt.h:62
Cnf_CutAlloc
ABC_NAMESPACE_IMPL_START Cnf_Cut_t * Cnf_CutAlloc(Cnf_Man_t *p, int nLeaves)
DECLARATIONS ///.
Definition: cnfCut.c:46
assert
#define assert(ex)
Definition: util_old.h:213
void Cnf_CutDeref ( Cnf_Man_t *  p,
Cnf_Cut_t *  pCut 
)

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 135 of file cnfCut.c.

136 {
137  Aig_Obj_t * pObj;
138  int i;
139  Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
140  {
141  assert( pObj->nRefs > 0 );
142  pObj->nRefs--;
143  }
144 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cnf_CutForEachLeaf
#define Cnf_CutForEachLeaf(p, pCut, pLeaf, i)
Definition: cnf.h:121
Aig_Obj_t_
Definition: aig.h:69
assert
#define assert(ex)
Definition: util_old.h:213
Aig_Obj_t_::nRefs
unsigned int nRefs
Definition: aig.h:81
void Cnf_CutFree ( Cnf_Cut_t *  pCut)

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file cnfCut.c.

69 {
70  if ( pCut->vIsop[0] )
71  Vec_IntFree( pCut->vIsop[0] );
72  if ( pCut->vIsop[1] )
73  Vec_IntFree( pCut->vIsop[1] );
74 }
Cnf_Cut_t_::vIsop
Vec_Int_t * vIsop[2]
Definition: cnf.h:76
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
void Cnf_CutInsertIthVar ( Cnf_Cut_t *  pCut,
int  iVar,
int  iFan 
)

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

Synopsis [Inserts the fanin variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 274 of file cnfCut.c.

275 {
276  int i;
277  for ( i = pCut->nFanins; i > iVar; i-- )
278  pCut->pFanins[i] = pCut->pFanins[i-1];
279  pCut->pFanins[iVar] = iFan;
280  pCut->nFanins++;
281 }
Cnf_Cut_t_::pFanins
int pFanins[0]
Definition: cnf.h:77
Cnf_Cut_t_::nFanins
char nFanins
Definition: cnf.h:73
static int Cnf_CutMergeLeaves ( Cnf_Cut_t *  pCut,
Cnf_Cut_t *  pCutFan,
int *  pFanins 
)
inlinestatic

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

Synopsis [Merges two arrays of integers.]

Description [Returns the number of items.]

SideEffects []

SeeAlso []

Definition at line 196 of file cnfCut.c.

197 {
198  int i, k, nFanins = 0;
199  for ( i = k = 0; i < pCut->nFanins && k < pCutFan->nFanins; )
200  {
201  if ( pCut->pFanins[i] == pCutFan->pFanins[k] )
202  pFanins[nFanins++] = pCut->pFanins[i], i++, k++;
203  else if ( pCut->pFanins[i] < pCutFan->pFanins[k] )
204  pFanins[nFanins++] = pCut->pFanins[i], i++;
205  else
206  pFanins[nFanins++] = pCutFan->pFanins[k], k++;
207  }
208  for ( ; i < pCut->nFanins; i++ )
209  pFanins[nFanins++] = pCut->pFanins[i];
210  for ( ; k < pCutFan->nFanins; k++ )
211  pFanins[nFanins++] = pCutFan->pFanins[k];
212  return nFanins;
213 }
for
for(p=first;p->value< newval;p=p->next)
Cnf_Cut_t_::pFanins
int pFanins[0]
Definition: cnf.h:77
Cnf_Cut_t_::nFanins
char nFanins
Definition: cnf.h:73
void Cnf_CutPrint ( Cnf_Cut_t *  pCut)

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 115 of file cnfCut.c.

116 {
117  int i;
118  printf( "{" );
119  for ( i = 0; i < pCut->nFanins; i++ )
120  printf( "%d ", pCut->pFanins[i] );
121  printf( " } " );
122 }
Cnf_Cut_t_::pFanins
int pFanins[0]
Definition: cnf.h:77
Cnf_Cut_t_::nFanins
char nFanins
Definition: cnf.h:73
void Cnf_CutRef ( Cnf_Man_t *  p,
Cnf_Cut_t *  pCut 
)

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 157 of file cnfCut.c.

158 {
159  Aig_Obj_t * pObj;
160  int i;
161  Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
162  {
163  pObj->nRefs++;
164  }
165 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cnf_CutForEachLeaf
#define Cnf_CutForEachLeaf(p, pCut, pLeaf, i)
Definition: cnf.h:121
Aig_Obj_t_
Definition: aig.h:69
Aig_Obj_t_::nRefs
unsigned int nRefs
Definition: aig.h:81
void Cnf_CutRemoveIthVar ( Cnf_Cut_t *  pCut,
int  iVar,
int  iFan 
)

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

Synopsis [Removes the fanin variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 254 of file cnfCut.c.

255 {
256  int i;
257  assert( pCut->pFanins[iVar] == iFan );
258  pCut->nFanins--;
259  for ( i = iVar; i < pCut->nFanins; i++ )
260  pCut->pFanins[i] = pCut->pFanins[i+1];
261 }
Cnf_Cut_t_::pFanins
int pFanins[0]
Definition: cnf.h:77
assert
#define assert(ex)
Definition: util_old.h:213
Cnf_Cut_t_::nFanins
char nFanins
Definition: cnf.h:73
void Cnf_CutUpdateRefs ( Cnf_Man_t *  p,
Cnf_Cut_t *  pCut,
Cnf_Cut_t *  pCutFan,
Cnf_Cut_t *  pCutRes 
)

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file cnfCut.c.

179 {
180  Cnf_CutDeref( p, pCut );
181  Cnf_CutDeref( p, pCutFan );
182  Cnf_CutRef( p, pCutRes );
183 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cnf_CutDeref
void Cnf_CutDeref(Cnf_Man_t *p, Cnf_Cut_t *pCut)
Definition: cnfCut.c:135
Cnf_CutRef
void Cnf_CutRef(Cnf_Man_t *p, Cnf_Cut_t *pCut)
Definition: cnfCut.c:157
static unsigned Cnf_TruthPhase ( Cnf_Cut_t *  pCut,
Cnf_Cut_t *  pCut1 
)
inlinestatic

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

Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 226 of file cnfCut.c.

227 {
228  unsigned uPhase = 0;
229  int i, k;
230  for ( i = k = 0; i < pCut->nFanins; i++ )
231  {
232  if ( k == pCut1->nFanins )
233  break;
234  if ( pCut->pFanins[i] < pCut1->pFanins[k] )
235  continue;
236  assert( pCut->pFanins[i] == pCut1->pFanins[k] );
237  uPhase |= (1 << i);
238  k++;
239  }
240  return uPhase;
241 }
Cnf_Cut_t_::pFanins
int pFanins[0]
Definition: cnf.h:77
assert
#define assert(ex)
Definition: util_old.h:213
Cnf_Cut_t_::nFanins
char nFanins
Definition: cnf.h:73