diff options
| -rw-r--r-- | src/aig/gia/giaAbsGla2.c | 28 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsRef.c | 217 |
2 files changed, 226 insertions, 19 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 4dcdb975..f3fcbbd0 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -661,7 +661,7 @@ static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], } } } -static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int Lits[], int iLitOut, int ProofId ) +void Ga2_ManCnfAddStatic( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int Lits[], int iLitOut, int ProofId ) { Vec_Int_t * vCnf; int i, k, b, Cube, Literal, nClaLits, ClaLits[6]; @@ -688,12 +688,11 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In else if ( Literal != 0 ) assert( 0 ); } - sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId ); + sat_solver2_addclause( pSat, ClaLits, ClaLits+nClaLits, ProofId ); } } } - /**Function************************************************************* Synopsis [] @@ -795,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, 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, Gia_ObjId(p->pGia, pObj) ); else { unsigned uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits ); @@ -899,7 +898,7 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, i ) Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pLeaf, f ) ); Lit = Ga2_ObjFindOrAddLit(p, pObj, f); - Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), Lit, -1 ); + Ga2_ManCnfAddStatic( p->pSat, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), Lit, -1 ); } else { @@ -1222,7 +1221,7 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p ) Abc_Cex_t * pCex; Vec_Int_t * vMap, * vVec; Gia_Obj_t * pObj; - int i; + int i, k; Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap ); // Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 ); vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 ); @@ -1237,9 +1236,16 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p ) return NULL; } Vec_IntFree( vMap ); + // remove those already added + k = 0; + Gia_ManForEachObjVec( vVec, p->pGia, pObj, i ) + if ( !Ga2_ObjIsAbs(p, pObj) ) + Vec_IntWriteEntry( vVec, k++, Gia_ObjId(p->pGia, pObj) ); + Vec_IntShrink( vVec, k ); + // these objects should be PPIs that are not abstracted yet Gia_ManForEachObjVec( vVec, p->pGia, pObj, i ) - assert( pObj->fPhase && Ga2_ObjIsLeaf(p, pObj) ); + assert( pObj->fPhase );//&& Ga2_ObjIsLeaf(p, pObj) ); p->nObjAdded += Vec_IntSize(vVec); return vVec; } @@ -1450,6 +1456,12 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) p->pPars->iFrame = f; // add static clauses to this timeframe Ga2_ManAddAbsClauses( p, f ); + // skip checking if skipcheck is enabled (&gla -s) + if ( p->pPars->fUseSkip && f <= iFrameProved ) + continue; + // skip checking if we need to skip several starting frames (&gla -S <num>) + if ( p->pPars->nFramesStart && f <= p->pPars->nFramesStart ) + continue; // get the output literal // Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f ); Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(Gia_ManPo(pAig,0)), f ); @@ -1457,8 +1469,6 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(Gia_ManPo(pAig,0)) ); if ( Lit == 0 ) continue; - if ( p->pPars->fUseSkip && f <= iFrameProved ) - continue; assert( Lit > 1 ); // check for counter-examples if ( p->nSatVars > sat_solver2_nvars(p->pSat) ) diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c index a30250a5..473afc92 100644 --- a/src/aig/gia/giaAbsRef.c +++ b/src/aig/gia/giaAbsRef.c @@ -20,6 +20,7 @@ #include "gia.h" #include "giaAbsRef.h" +#include "sat/bsat/satSolver2.h" ABC_NAMESPACE_IMPL_START @@ -94,6 +95,11 @@ struct Rnm_Man_t_ Vec_Int_t * vObjs; // internal objects used in value propagation Vec_Str_t * vCounts; // fanin counters Vec_Int_t * vFanins; // fanins + // SAT solver + sat_solver2 * pSat; // incremental SAT solver + Vec_Int_t * vSatVars; // SAT variables + Vec_Int_t * vSat2Ids; // mapping of SAT variables into object IDs + Vec_Int_t * vIsopMem; // memory for ISOP computation // internal data Rnm_Obj_t * pObjs; // refinement objects int nObjs; // the number of used objects @@ -118,16 +124,24 @@ static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f ) return p->pObjs + f * p->nObjsFrame + pObj->Value; } -static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); } -static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); } -static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); } -static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); } -static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); } -static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; } +static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); } +static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); } +static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); } +static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); } +static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); } +static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; } -static inline int Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) ); } -static inline void Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c ); } -static inline int Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { int c = Rnm_ObjCount(p, pObj); if ( c < 16 ) Rnm_ObjSetCount(p, pObj, c+1); return c; } +static inline int Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) ); } +static inline void Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c ); } +static inline int Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { int c = Rnm_ObjCount(p, pObj); if ( c < 16 ) Rnm_ObjSetCount(p, pObj, c+1); return c; } + +static inline int Rnm_ObjSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj) ); } +static inline void Rnm_ObjSetSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj, int c) { Vec_IntWriteEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj), c ); } +static inline int Rnm_ObjFindOrAddSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj) { if ( Rnm_ObjSatVar(p, pObj) == 0 ) { Rnm_ObjSetSatVar(p, pObj, Vec_IntSize(p->vSat2Ids)); Vec_IntPush(p->vSat2Ids, Gia_ObjId(p->pGia, pObj)); }; return 2*Rnm_ObjSatVar(p, pObj); } + +extern void Ga2_ManCnfAddStatic( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int * pLits, int iLitOut, int ProofId ); + +extern Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -135,6 +149,168 @@ static inline int Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) /**Function************************************************************* + Synopsis [Performs UNSAT-core-based refinement.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rnm_ManRefineCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisited, Vec_Int_t * vFlops ) +{ + Vec_Int_t * vLeaves; + Gia_Obj_t * pFanin; + int k; + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsCi(pObj) ) + { + if ( Gia_ObjIsRo(p, pObj) ) + Vec_IntPush( vFlops, Gia_ObjId(p, pObj) ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + vLeaves = Ga2_ObjLeaves( p, pObj ); + Gia_ManForEachObjVec( vLeaves, p, pFanin, k ) + Rnm_ManRefineCollect_rec( p, pFanin, vVisited, vFlops ); + Vec_IntPush( vVisited, Gia_ObjId(p, pObj) ); +} + +Vec_Int_t * Rnm_ManRefineUnsatCore( Rnm_Man_t * p, Vec_Int_t * vPPIs ) +{ + Vec_Int_t * vCnf0, * vCnf1; + Vec_Int_t * vLeaves, * vLits, * vPpi2Map; + Vec_Int_t * vVisited, * vFlops, * vCore, * vCoreFinal; + Gia_Obj_t * pObj, * pFanin; + int i, k, f, Status, Entry, pLits[5], iBit = p->pCex->nRegs; + // map PPIs into their positions in the map // CAN BE MADE FASTER + vPpi2Map = Vec_IntAlloc( Vec_IntSize(vPPIs) ); + Vec_IntForEachEntry( vPPIs, Entry, i ) + { + Entry = Vec_IntFind( p->vMap, Entry ); + assert( Entry >= 0 ); + Vec_IntPush( vPpi2Map, Entry ); + } + // collect nodes between selected PPIs and CIs + vFlops = Vec_IntAlloc( 100 ); + vVisited = Vec_IntAlloc( 100 ); + Gia_ManIncrementTravId( p->pGia ); + Gia_ManForEachObjVec( vPPIs, p->pGia, pObj, i ) +// if ( !Gia_ObjIsRo(p->pGia, pObj) ) // SKIP PPIs that are flops + Rnm_ManRefineCollect_rec( p->pGia, pObj, vVisited, vFlops ); + // create SAT variables and SAT solver + Vec_IntFill( p->vSat2Ids, 1, -1 ); + assert( p->pSat == NULL ); + p->pSat = sat_solver2_new(); + Vec_IntFill( p->vSatVars, Gia_ManObjNum(p->pGia), 0 ); // NO NEED TO CLEAN EACH TIME + // assign PPI variables + Gia_ManForEachObjVec( vFlops, p->pGia, pObj, i ) + Rnm_ObjFindOrAddSatVar( p, pObj ); + // assign other variables + Gia_ManForEachObjVec( vVisited, p->pGia, pObj, i ) + { + vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) + pLits[k] = Rnm_ObjFindOrAddSatVar( p, pFanin ); + vCnf0 = Ga2_ManCnfCompute( Ga2_ObjTruth(p->pGia, pObj), Vec_IntSize(vLeaves), p->vIsopMem ); + vCnf1 = Ga2_ManCnfCompute( ~Ga2_ObjTruth(p->pGia, pObj), Vec_IntSize(vLeaves), p->vIsopMem ); + Ga2_ManCnfAddStatic( p->pSat, vCnf0, vCnf1, pLits, Rnm_ObjFindOrAddSatVar(p, pObj), Rnm_ObjFindOrAddSatVar(p, pObj)/2 ); + Vec_IntFree( vCnf0 ); + Vec_IntFree( vCnf1 ); + } + +// printf( "\n" ); + + p->pSat->pPrf2 = Prf_ManAlloc(); + Prf_ManRestart( p->pSat->pPrf2, NULL, sat_solver2_nlearnts(p->pSat), Vec_IntSize(p->vSat2Ids) ); + + // iterate UNSAT core computation for each timeframe + vLits = Vec_IntAlloc( 100 ); + vCoreFinal = Vec_IntAlloc( 100 ); + for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) + { + // collect values of PPIs in this timeframe + Vec_IntClear( vLits ); + Gia_ManForEachObjVec( vPPIs, p->pGia, pObj, i ) + { + Entry = Abc_InfoHasBit( p->pCex->pData, iBit + Vec_IntEntry(vPpi2Map, i) ); + Vec_IntPush( vLits, Abc_LitNotCond( Rnm_ObjFindOrAddSatVar(p, pObj), !Entry ) ); + } + + // handle the first timeframe in a special vay + if ( f == 0 ) + Gia_ManForEachObjVec( vFlops, p->pGia, pObj, i ) + if ( Vec_IntFind( vPPIs, Gia_ObjId(p->pGia, pObj) ) == -1 ) + Vec_IntPush( vLits, Abc_LitNotCond( Rnm_ObjFindOrAddSatVar(p, pObj), 1 ) ); +/* + // uniqify literals and detect special conflicts + Vec_IntUniqify( vLits ); + Vec_IntForEachEntryStart( vLits, Entry, i, 1 ) + if ( Vec_IntEntry(vLits, i-1) == Abc_LitNot(Entry) ) + break; + if ( i < Vec_IntSize(vLits) ) + printf( "triv_unsat " ); + else +*/ + + Status = sat_solver2_solve( p->pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( Status != l_False ) + continue; + vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat ); +// vCore = Vec_IntAlloc( 0 ); + // add to the UNSAT core + Vec_IntAppend( vCoreFinal, vCore ); + +// printf( "Frame %d : ", f ); +// Vec_IntPrint( vCore ); + Vec_IntFree( vCore ); + } + assert( iBit == p->pCex->nBits ); + Vec_IntUniqify( vCoreFinal ); + Vec_IntFree( vLits ); + Prf_ManStopP( &p->pSat->pPrf2 ); + sat_solver2_delete( p->pSat ); + p->pSat = NULL; + + // translate from entry into ID + Vec_IntForEachEntry( vCoreFinal, Entry, i ) + { + assert( Vec_IntEntry(p->vSat2Ids, Entry) >= 0 ); + assert( Vec_IntEntry(p->vSat2Ids, Entry) < Gia_ManObjNum(p->pGia) ); + Vec_IntWriteEntry( vCoreFinal, i, Vec_IntEntry(p->vSat2Ids, Entry) ); + } + // if there are flop outputs, add them + Gia_ManForEachObjVec( vPPIs, p->pGia, pObj, i ) + if ( Gia_ObjIsRo(p->pGia, pObj) ) + Vec_IntPush( vCoreFinal, Gia_ObjId(p->pGia, pObj) ); + Vec_IntUniqify( vCoreFinal ); + +// printf( "\n" ); +// Vec_IntPrint( vPPIs ); +// Vec_IntPrint( vCoreFinal ); + +// printf( "\n" ); + + // clean SAT variable numbers + Gia_ManForEachObjVec( vVisited, p->pGia, pObj, i ) + { + Rnm_ObjSetSatVar( p, pObj, 0 ); + vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) + Rnm_ObjSetSatVar( p, pFanin, 0 ); + } + Vec_IntFree( vFlops ); + Vec_IntFree( vVisited ); + Vec_IntFree( vPpi2Map ); + return vCoreFinal; +} + + +/**Function************************************************************* + Synopsis [Creates a new manager.] Description [] @@ -152,7 +328,10 @@ Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia ) p->pGia = pGia; p->vObjs = Vec_IntAlloc( 100 ); p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) ); - p->vFanins = Vec_IntAlloc( 100 ); + p->vFanins = Vec_IntAlloc( 1000 ); + p->vSatVars = Vec_IntAlloc( 0 ); + p->vSat2Ids = Vec_IntAlloc( 1000 ); + p->vIsopMem = Vec_IntAlloc( 0 ); p->nObjsAlloc = 10000; p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc ); if ( p->pGia->vFanout == NULL ) @@ -185,6 +364,9 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile ) Gia_ManCleanMark1(p->pGia); Gia_ManStaticFanoutStop(p->pGia); // Gia_ManSetPhase(p->pGia); + Vec_IntFree( p->vIsopMem ); + Vec_IntFree( p->vSatVars ); + Vec_IntFree( p->vSat2Ids ); Vec_StrFree( p->vCounts ); Vec_IntFree( p->vFanins ); Vec_IntFree( p->vObjs ); @@ -769,6 +951,21 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in // printf( "\nBig refinement.\n" ); } } + else + { + vNew = Rnm_ManRefineUnsatCore( p, vSelected ); + if ( Vec_IntSize(vNew) > 0 ) + { + Vec_IntFree( vSelected ); + vSelected = vNew; +// Vec_IntFree( vNew ); + } + else + { + Vec_IntFree( vNew ); + // printf( "\nBig refinement.\n" ); + } + } // clean values Rnm_ManCleanValues( p ); |