abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
dchSweep.c File Reference
#include "dchInt.h"
#include "misc/bar/bar.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START
Aig_Obj_t
Dch_ObjChild0Fra (Aig_Obj_t *pObj)
 DECLARATIONS ///. More...
 
static Aig_Obj_tDch_ObjChild1Fra (Aig_Obj_t *pObj)
 
void Dch_ManSweepNode (Dch_Man_t *p, Aig_Obj_t *pObj)
 FUNCTION DEFINITIONS ///. More...
 
void Dch_ManSweep (Dch_Man_t *p)
 

Function Documentation

void Dch_ManSweep ( Dch_Man_t p)

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file dchSweep.c.

107 {
108  Bar_Progress_t * pProgress = NULL;
109  Aig_Obj_t * pObj, * pObjNew;
110  int i;
111  // map constants and PIs
115  Aig_ManForEachCi( p->pAigTotal, pObj, i )
116  pObj->pData = Aig_ObjCreateCi( p->pAigFraig );
117  // sweep internal nodes
118  pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) );
119  Aig_ManForEachNode( p->pAigTotal, pObj, i )
120  {
121  Bar_ProgressUpdate( pProgress, i, NULL );
122  if ( Dch_ObjFraig(Aig_ObjFanin0(pObj)) == NULL ||
123  Dch_ObjFraig(Aig_ObjFanin1(pObj)) == NULL )
124  continue;
125  pObjNew = Aig_And( p->pAigFraig, Dch_ObjChild0Fra(pObj), Dch_ObjChild1Fra(pObj) );
126  if ( pObjNew == NULL )
127  continue;
128  Dch_ObjSetFraig( pObj, pObjNew );
129  Dch_ManSweepNode( p, pObj );
130  }
131  Bar_ProgressStop( pProgress );
132  // update the representatives of the nodes (makes classes invalid)
133  ABC_FREE( p->pAigTotal->pReprs );
134  p->pAigTotal->pReprs = p->pReprsProved;
135  p->pReprsProved = NULL;
136  // clean the mark
138 }
void * pData
Definition: aig.h:87
Aig_Man_t * pAigFraig
Definition: dchInt.h:58
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static Aig_Obj_t * Dch_ObjChild1Fra(Aig_Obj_t *pObj)
Definition: dchSweep.c:32
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
void Dch_ManSweepNode(Dch_Man_t *p, Aig_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition: dchSweep.c:49
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
static void Bar_ProgressUpdate(Bar_Progress_t *p, int nItemsCur, char *pString)
Definition: bar.h:63
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static Aig_Obj_t * Dch_ObjFraig(Aig_Obj_t *pObj)
Definition: dchInt.h:105
static void Dch_ObjSetFraig(Aig_Obj_t *pObj, Aig_Obj_t *pNode)
Definition: dchInt.h:106
Definition: aig.h:69
DECLARATIONS ///.
Definition: bar.c:36
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
#define ABC_FREE(obj)
Definition: abc_global.h:232
Aig_Man_t * pAigTotal
Definition: dchInt.h:57
static ABC_NAMESPACE_IMPL_START Aig_Obj_t * Dch_ObjChild0Fra(Aig_Obj_t *pObj)
DECLARATIONS ///.
Definition: dchSweep.c:31
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
void Bar_ProgressStop(Bar_Progress_t *p)
Definition: bar.c:126
Bar_Progress_t * Bar_ProgressStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition: bar.c:66
Aig_Obj_t ** pReprsProved
Definition: dchInt.h:61
void Dch_ManSweepNode ( Dch_Man_t p,
Aig_Obj_t pObj 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Performs fraiging for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 49 of file dchSweep.c.

50 {
51  Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
52  int RetValue;
53  // get representative of this class
54  pObjRepr = Aig_ObjRepr( p->pAigTotal, pObj );
55  if ( pObjRepr == NULL )
56  return;
57  // get the fraiged node
58  pObjFraig = Dch_ObjFraig( pObj );
59  if ( pObjFraig == NULL )
60  return;
61  // get the fraiged representative
62  pObjReprFraig = Dch_ObjFraig( pObjRepr );
63  if ( pObjReprFraig == NULL )
64  return;
65  // if the fraiged nodes are the same, return
66  if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
67  {
68  // remember the proved equivalence
69  p->pReprsProved[ pObj->Id ] = pObjRepr;
70  return;
71  }
72  assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pAigFraig) );
73  RetValue = Dch_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
74  if ( RetValue == -1 ) // timed out
75  {
76  Dch_ObjSetFraig( pObj, NULL );
77  return;
78  }
79  if ( RetValue == 1 ) // proved equivalent
80  {
81  pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
82  Dch_ObjSetFraig( pObj, pObjFraig2 );
83  // remember the proved equivalence
84  p->pReprsProved[ pObj->Id ] = pObjRepr;
85  return;
86  }
87  // disproved the equivalence
88  if ( p->pPars->fSimulateTfo )
89  Dch_ManResimulateCex( p, pObj, pObjRepr );
90  else
91  Dch_ManResimulateCex2( p, pObj, pObjRepr );
92  assert( Aig_ObjRepr( p->pAigTotal, pObj ) != pObjRepr );
93 }
static Aig_Obj_t * Aig_ObjRepr(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:330
Aig_Man_t * pAigFraig
Definition: dchInt.h:58
void Dch_ManResimulateCex2(Dch_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
Definition: dchSimSat.c:225
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
int Dch_NodesAreEquiv(Dch_Man_t *p, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
DECLARATIONS ///.
Definition: dchSat.c:45
void Dch_ManResimulateCex(Dch_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
Definition: dchSimSat.c:177
static Aig_Obj_t * Dch_ObjFraig(Aig_Obj_t *pObj)
Definition: dchInt.h:105
static void Dch_ObjSetFraig(Aig_Obj_t *pObj, Aig_Obj_t *pNode)
Definition: dchInt.h:106
Definition: aig.h:69
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
unsigned int fPhase
Definition: aig.h:78
Aig_Man_t * pAigTotal
Definition: dchInt.h:57
#define assert(ex)
Definition: util_old.h:213
Dch_Pars_t * pPars
Definition: dchInt.h:54
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
int Id
Definition: aig.h:85
Aig_Obj_t ** pReprsProved
Definition: dchInt.h:61
static ABC_NAMESPACE_IMPL_START Aig_Obj_t* Dch_ObjChild0Fra ( Aig_Obj_t pObj)
inlinestatic

DECLARATIONS ///.

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

FileName [dchSweep.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [One round of SAT sweeping.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:
dchSweep.c,v 1.00 2008/07/29 00:00:00 alanmi Exp

]

Definition at line 31 of file dchSweep.c.

31 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; }
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static Aig_Obj_t * Dch_ObjFraig(Aig_Obj_t *pObj)
Definition: dchInt.h:105
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
static Aig_Obj_t* Dch_ObjChild1Fra ( Aig_Obj_t pObj)
inlinestatic

Definition at line 32 of file dchSweep.c.

32 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; }
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static Aig_Obj_t * Dch_ObjFraig(Aig_Obj_t *pObj)
Definition: dchInt.h:105
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248