diff options
-rw-r--r-- | src/aig/gia/giaAbsGla2.c | 39 | ||||
-rw-r--r-- | src/aig/gia/giaAbsRef.c | 3 | ||||
-rw-r--r-- | src/sat/bsat/satProof2.h | 2 |
3 files changed, 21 insertions, 23 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 88b168fa..2960ddff 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -554,7 +554,7 @@ Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover ) SeeAlso [] ***********************************************************************/ -static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], int iLitOut, int ProofId ) +static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], int iLitOut ) { int i, k, b, Cube, nClaLits, ClaLits[6]; assert( uTruth > 0 && uTruth < 0xffff ); @@ -583,7 +583,7 @@ static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], } Cube = Cube / 3; } - sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId ); + sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, -1 ); } } } @@ -702,19 +702,11 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) int fSimple = 1; Gia_Obj_t * pObj; int i, Lit; -/* - Vec_Int_t * vMap = (f < Vec_PtrSize(p->vId2Lit) ? Ga2_MapFrameMap( p, f ) : NULL); -// Ga2_ObjAddLit( p, Gia_ManConst0(p->pGia), f, 0 ); - if ( f == 5 ) - { - int s = 0; - } -*/ if ( fSimple ) { Lit = Ga2_ObjFindOrAddLit( p, Gia_ManConst0(p->pGia), f ); Lit = Abc_LitNot( Lit ); - sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, 0 ); + sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, -1 ); } Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) if ( i >= p->LimAbs ) @@ -822,11 +814,7 @@ Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p ) if ( Gia_ObjIsAnd(pObj) ) Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 ); else if ( Gia_ObjIsRo(p->pGia, pObj) ) - { Vec_IntWriteEntry( vGateClasses, Gia_ObjId(p->pGia, pObj), 1 ); - pObj = Gia_ObjRoToRi( p->pGia, pObj ); - Vec_IntWriteEntry( vGateClasses, Gia_ObjFaninId0p(p->pGia, pObj), 1 ); - } else if ( !Gia_ObjIsConst0(pObj) ) assert( 0 ); } @@ -859,7 +847,7 @@ void Ga2_ManRestart( Ga2_Man_t * p ) if ( p->pSat ) sat_solver2_delete( p->pSat ); p->pSat = sat_solver2_new(); // add clause x0 = 0 (lit0 = 1; lit1 = 0) - sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, 0 ); + sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, -1 ); // remove previous abstraction Ga2_ManShrinkAbs( p, 1, 1, 1 ); // start new abstraction @@ -877,7 +865,7 @@ void Ga2_ManRestart( Ga2_Man_t * p ) /**Function************************************************************* - Synopsis [Unrolls one timeframe.] + Synopsis [Unrolls one timeframe.]` Description [] @@ -901,8 +889,8 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) Lit = Ga2_ObjFindOrAddLit( p, pObj, f ); Lit = Abc_LitNot(Lit); assert( Lit > 1 ); - sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, Gia_ObjId(p->pGia, pObj) ); - return Lit; + sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, -1 ); + return Abc_LitNot(Lit); } return 0; } @@ -956,7 +944,10 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) // minimize truth table uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, Ga2_ObjLeaves(p->pGia, pObj), p->vLits ); if ( uTruth == 0 || uTruth == ~0 ) // const 0 / 1 + { Lit = (uTruth > 0); + Ga2_ObjAddLit( p, pObj, f, Lit ); + } else if ( uTruth == 0xAAAAAAAA || uTruth == 0x55555555 ) // buffer / inverter { Lit = Vec_IntEntry( p->vLits, 0 ); @@ -966,6 +957,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f ); } Lit = Abc_LitNotCond( Lit, uTruth == 0x55555555 ); + Ga2_ObjAddLit( p, pObj, f, Lit ); } else { @@ -973,9 +965,8 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) // add new node Lit = Ga2_ObjFindOrAddLit(p, pObj, f); - Ga2_ManCnfAddDynamic( p, uTruth, Vec_IntArray(p->vLits), Lit, Gia_ObjId(p->pGia, pObj) ); + Ga2_ManCnfAddDynamic( p, uTruth, Vec_IntArray(p->vLits), Lit ); } - Ga2_ObjAddLit( p, pObj, f, Lit ); return Lit; } @@ -1014,6 +1005,7 @@ int Vec_IntCheckUnique( Vec_Int_t * p ) static inline int Ga2_ObjSatValue( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) { int Lit = Ga2_ObjFindLit( p, pObj, f ); + assert( !Gia_ObjIsConst0(pObj) ); if ( Lit == -1 ) return 0; return Abc_LitIsCompl(Lit) ^ sat_solver2_var_value( p->pSat, Abc_Lit2Var(Lit) ); @@ -1024,6 +1016,11 @@ void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pv Vec_Int_t * vMap; Gia_Obj_t * pObj; int f, i, k, Id; +/* + Gia_ManForEachObj( p->pGia, pObj, i ) + if ( Ga2_ObjId(p, pObj) >= 0 ) + assert( Vec_IntEntry(p->vValues, Ga2_ObjId(p, pObj)) == i ); +*/ // find PIs and PPIs vMap = Vec_IntAlloc( 1000 ); Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i ) diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c index 8e475863..a4401700 100644 --- a/src/aig/gia/giaAbsRef.c +++ b/src/aig/gia/giaAbsRef.c @@ -518,6 +518,7 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); clock_t clk, clk2 = clock(); p->nCalls++; +// Gia_ManCleanValue( p->pGia ); // initialize p->pCex = pCex; p->vMap = vMap; @@ -542,7 +543,7 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in p->timeBwd += clock() - clk; } // clean values - Rnm_ManCleanValues( p ); +// Rnm_ManCleanValues( p ); // verify (empty) refinement clk = clock(); Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected ); diff --git a/src/sat/bsat/satProof2.h b/src/sat/bsat/satProof2.h index 82ed9264..25ad0d07 100644 --- a/src/sat/bsat/satProof2.h +++ b/src/sat/bsat/satProof2.h @@ -239,7 +239,7 @@ static inline void Prf_ManChainResolve( Prf_Man_t * p, clause * c ) } else // problem clause { - if ( clause_id(c) ) // has proof ID + if ( clause_id(c) >= 0 ) // has proof ID { int Entry; if ( p->vId2Pr == NULL ) |