diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaAbsGla2.c | 12 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 1 |
2 files changed, 7 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 ); } diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 2b65170a..180659a4 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1276,6 +1276,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end, int Id) int maxvar, count, temp; assert( solver2_dlevel(s) == 0 ); assert( begin < end ); + assert( Id != 0 ); // copy clause into storage veci_resize( &s->temp_clause, 0 ); |