diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-31 18:45:10 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-31 18:45:10 -0700 |
| commit | fe1a16e9b43e841b740048b142dbb619175457ed (patch) | |
| tree | 15aa5a7ab668b36aa8469af3369d448496d74e2a /src/aig/gia/giaAbsGla2.c | |
| parent | 1e53a78a99d3c002363a8300aba46531baa0f3c5 (diff) | |
| download | abc-fe1a16e9b43e841b740048b142dbb619175457ed.tar.gz abc-fe1a16e9b43e841b740048b142dbb619175457ed.tar.bz2 abc-fe1a16e9b43e841b740048b142dbb619175457ed.zip | |
Changes to allow &gla to run with fSimple = 1 (useful for debugging).
Diffstat (limited to 'src/aig/gia/giaAbsGla2.c')
| -rw-r--r-- | src/aig/gia/giaAbsGla2.c | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index de516ee2..f296482d 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -769,7 +769,7 @@ static inline void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs ) Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(~uTruth, nLeaves, p->vIsopMem) ); } -static inline void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) +static inline void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int fUseId ) { Vec_Int_t * vLeaves; Gia_Obj_t * pLeaf; @@ -779,7 +779,7 @@ static inline void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, in if ( Gia_ObjIsConst0(pObj) || (f == 0 && Gia_ObjIsRo(p->pGia, pObj)) ) { iLitOut = Abc_LitNot( iLitOut ); - sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, Gia_ObjId(p->pGia, pObj) ); + sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, fUseId ? Gia_ObjId(p->pGia, pObj) : -1 ); } else { @@ -794,7 +794,7 @@ static inline void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, in fUseStatic = 0; } if ( fUseStatic || Gia_ObjIsRo(p->pGia, pObj) ) - Ga2_ManCnfAddStatic( p->pSat, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) ); + Ga2_ManCnfAddStatic( p->pSat, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, fUseId ? Gia_ObjId(p->pGia, pObj) : -1 ); else { unsigned uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits ); @@ -946,13 +946,13 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) if ( i == p->LimAbs ) break; if ( fSimple ) - Ga2_ManAddToAbsOneStatic( p, pObj, f ); + Ga2_ManAddToAbsOneStatic( p, pObj, f, 0 ); else Ga2_ManAddToAbsOneDynamic( p, pObj, f ); } Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) if ( i >= p->LimAbs ) - Ga2_ManAddToAbsOneStatic( p, pObj, f ); + Ga2_ManAddToAbsOneStatic( p, pObj, f, 1 ); // sat_solver2_simplify( p->pSat ); } @@ -981,7 +981,7 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd ) { Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 ); Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i ) - Ga2_ManAddToAbsOneStatic( p, pObj, f ); + Ga2_ManAddToAbsOneStatic( p, pObj, f, 1 ); } // sat_solver2_simplify( p->pSat ); } |