diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-07 18:11:29 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-07 18:11:29 -0700 |
| commit | a735d95a5bfa8ab21ddbe5a2a66695327d3b7206 (patch) | |
| tree | 96f083283877e8d8e8695aae7cf4101afc3cf6da /src/aig | |
| parent | 51db560206d030e3f0b7628169a92ce58c601db7 (diff) | |
| download | abc-a735d95a5bfa8ab21ddbe5a2a66695327d3b7206.tar.gz abc-a735d95a5bfa8ab21ddbe5a2a66695327d3b7206.tar.bz2 abc-a735d95a5bfa8ab21ddbe5a2a66695327d3b7206.zip | |
SAT sweeping under constraints (bug fix).
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaEquiv.c | 7 | ||||
| -rw-r--r-- | src/aig/gia/giaSweep.c | 2 |
3 files changed, 6 insertions, 5 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 48f0c215..ed38806e 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -891,7 +891,7 @@ extern int Gia_ManEquivCountLitsAll( Gia_Man_t * p ); extern int Gia_ManEquivCountClasses( Gia_Man_t * p ); extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ); extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ); -extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ); +extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose ); extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ); extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fSkipSome, int fVerbose ); diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 3067f956..d795856a 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -414,7 +414,7 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ) +Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose ) { Gia_Man_t * pNew; Gia_Obj_t * pObj; @@ -445,7 +445,8 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV return NULL; } */ - Gia_ManSetPhase( p ); + if ( !fSkipPhase ) + Gia_ManSetPhase( p ); if ( fDualOut ) Gia_ManEquivSetColors( p, fVerbose ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); @@ -637,7 +638,7 @@ Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p ) Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ) { Gia_Man_t * pNew, * pFinal; - pNew = Gia_ManEquivReduce( p, 0, 0, 0 ); + pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 ); if ( pNew == NULL ) return NULL; if ( fMiterPairs ) diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c index 994aedc1..4517bb7b 100644 --- a/src/aig/gia/giaSweep.c +++ b/src/aig/gia/giaSweep.c @@ -288,7 +288,7 @@ Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars ) if ( p->pManTime == NULL ) { Gia_ManFraigSweepPerform( p, pPars ); - pNew = Gia_ManEquivReduce( p, 1, 0, 0 ); + pNew = Gia_ManEquivReduce( p, 1, 0, 0, 0 ); if ( pNew == NULL ) return Gia_ManDup(p); return pNew; |