diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2021-10-06 17:14:57 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2021-10-06 17:14:57 -0700 |
commit | 31f88974e211f9bf9db74dd1dba5b4e026ed173e (patch) | |
tree | ba0136717a10c8e243a1caddd7fdd802a29243e0 /src/proof/cec/cecSatG2.c | |
parent | eb44a80bf2eb8723231e72bb095c97d1e4834d56 (diff) | |
download | abc-31f88974e211f9bf9db74dd1dba5b4e026ed173e.tar.gz abc-31f88974e211f9bf9db74dd1dba5b4e026ed173e.tar.bz2 abc-31f88974e211f9bf9db74dd1dba5b4e026ed173e.zip |
Various changes.
Diffstat (limited to 'src/proof/cec/cecSatG2.c')
-rw-r--r-- | src/proof/cec/cecSatG2.c | 93 |
1 files changed, 55 insertions, 38 deletions
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index b58aada8..ce299c66 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -98,13 +98,12 @@ struct Cec4_Man_t_ Vec_Int_t * vCands; Vec_Int_t * vVisit; Vec_Int_t * vPat; - Vec_Int_t * vPats; Vec_Int_t * vDisprPairs; Vec_Bit_t * vFails; + Vec_Bit_t * vCoDrivers; int iPosRead; // candidate reading position int iPosWrite; // candidate writing position int iLastConst; // last const node proved - int nPatsAll; // refinement Vec_Int_t * vRefClasses; Vec_Int_t * vRefNodes; @@ -162,25 +161,16 @@ Vec_Wrd_t * Cec4_EvalCombine( Vec_Int_t * vPats, int nPats, int nInputs, int nWo { //Vec_Wrd_t * vSimsPi = Vec_WrdStart( nInputs * nWords ); Vec_Wrd_t * vSimsPi = Vec_WrdStartRandom( nInputs * nWords ); - int i, k, iPat = 0; - for ( i = 0; i < Vec_IntSize(vPats); ) - { - int Size = Vec_IntEntry(vPats, i); - assert( Size > 0 ); - for ( k = 1; k <= Size; k++ ) - { - int iLit = Vec_IntEntry( vPats, i+k ); - word * pSim; - if ( iLit == 0 ) - continue; - assert( Abc_Lit2Var(iLit) > 0 && Abc_Lit2Var(iLit) <= nInputs ); - pSim = Vec_WrdEntryP( vSimsPi, (Abc_Lit2Var(iLit)-1)*nWords ); - if ( Abc_InfoHasBit( (unsigned*)pSim, iPat ) != Abc_LitIsCompl(iLit) ) - Abc_InfoXorBit( (unsigned*)pSim, iPat ); - } - iPat++; - i += Size + 1; - } + int i, k, iLit, iPat = 0; word * pSim; + for ( i = 0; i < Vec_IntSize(vPats); i += Vec_IntEntry(vPats, i), iPat++ ) + for ( k = 1; k < Vec_IntEntry(vPats, i)-1; k++ ) + if ( (iLit = Vec_IntEntry(vPats, i+k)) ) + { + assert( Abc_Lit2Var(iLit) > 0 && Abc_Lit2Var(iLit) <= nInputs ); + pSim = Vec_WrdEntryP( vSimsPi, (Abc_Lit2Var(iLit)-1)*nWords ); + if ( Abc_InfoHasBit( (unsigned*)pSim, iPat ) != Abc_LitIsCompl(iLit) ) + Abc_InfoXorBit( (unsigned*)pSim, iPat ); + } assert( iPat == nPats ); return vSimsPi; } @@ -224,6 +214,7 @@ void Cec4_ManSetParams( Cec_ParFra_t * pPars ) pPars->nRounds = 10; // simulation rounds pPars->nItersMax = 2000; // this is a miter pPars->nBTLimit = 1000000; // use logic cones + pPars->nBTLimitPo = 0; // use logic outputs pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver pPars->nGenIters = 100; // pattern generation iterations @@ -257,10 +248,18 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) p->vCands = Vec_IntAlloc( 100 ); p->vVisit = Vec_IntAlloc( 100 ); p->vPat = Vec_IntAlloc( 100 ); - p->vPats = Vec_IntAlloc( 10000 ); p->vDisprPairs = Vec_IntAlloc( 100 ); p->vFails = Vec_BitStart( Gia_ManObjNum(pAig) ); //pAig->pData = p->pSat; // point AIG manager to the solver + //Vec_IntFreeP( &p->pAig->vPats ); + //p->pAig->vPats = Vec_IntAlloc( 1000 ); + if ( pPars->nBTLimitPo ) + { + int i, Driver; + p->vCoDrivers = Vec_BitStart( Gia_ManObjNum(pAig) ); + Gia_ManForEachCoDriverId( pAig, Driver, i ) + Vec_BitWriteEntry( p->vCoDrivers, Driver, 1 ); + } return p; } void Cec4_ManDestroy( Cec4_Man_t * p ) @@ -287,11 +286,9 @@ void Cec4_ManDestroy( Cec4_Man_t * p ) fflush( stdout ); } //printf( "Recorded %d patterns with %d literals (average %.2f).\n", - // p->nPatsAll, Vec_IntSize(p->vPats) - p->nPatsAll, 1.0*Vec_IntSize(p->vPats)/Abc_MaxInt(1, p->nPatsAll)-1 ); - //Cec4_EvalPatterns( p->pAig, p->vPats, p->nPatsAll ); - //Vec_IntFreeP( &p->vPats ); - Vec_IntFreeP( &p->pAig->vPats ); - p->pAig->vPats = p->vPats; + // p->pAig->nBitPats, Vec_IntSize(p->pAig->vPats) - 2*p->pAig->nBitPats, 1.0*Vec_IntSize(p->pAig->vPats)/Abc_MaxInt(1, p->pAig->nBitPats)-2 ); + //Cec4_EvalPatterns( p->pAig, p->pAig->vPats, p->pAig->nBitPats ); + //Vec_IntFreeP( &p->pAig->vPats ); Vec_WrdFreeP( &p->pAig->vSims ); Vec_WrdFreeP( &p->pAig->vSimsPi ); Gia_ManCleanMark01( p->pAig ); @@ -307,6 +304,7 @@ void Cec4_ManDestroy( Cec4_Man_t * p ) Vec_IntFreeP( &p->vPat ); Vec_IntFreeP( &p->vDisprPairs ); Vec_BitFreeP( &p->vFails ); + Vec_BitFreeP( &p->vCoDrivers ); Vec_IntFreeP( &p->vRefClasses ); Vec_IntFreeP( &p->vRefNodes ); Vec_IntFreeP( &p->vRefBins ); @@ -1458,9 +1456,12 @@ int Cec4_ManGeneratePatterns( Cec4_Man_t * p ) if ( Res ) { int Ret = Cec4_ManPackAddPattern( p->pAig, p->vPat, 1 ); - Vec_IntPush( p->vPats, Vec_IntSize(p->vPat) ); - Vec_IntAppend( p->vPats, p->vPat ); - p->nPatsAll++; + if ( p->pAig->vPats ) + { + Vec_IntPush( p->pAig->vPats, Vec_IntSize(p->vPat)+2 ); + Vec_IntAppend( p->pAig->vPats, p->vPat ); + Vec_IntPush( p->pAig->vPats, -1 ); + } //Vec_IntPushTwo( p->vDisprPairs, iRepr, iCand ); Packs += Ret; if ( Ret == 64 * p->pAig->nSimWords ) @@ -1506,12 +1507,13 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p ) Vec_IntClear( &p->pNew->vCopiesTwo ); // pairs (CiAigId, SatId) Vec_IntClear( &p->pNew->vVarMap ); // mapping of SatId into AigId } -int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose ) +int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose, int fEffort ) { abctime clk; - int nBTLimit = Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1) ? Abc_MaxInt(1, p->pPars->nBTLimit/10) : p->pPars->nBTLimit; + int nBTLimit = fEffort ? p->pPars->nBTLimitPo : (Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1)) ? Abc_MaxInt(1, p->pPars->nBTLimit/10) : p->pPars->nBTLimit; int nConfEnd, nConfBeg, status, iVar0, iVar1, Lits[2]; int UnsatConflicts[3] = {0}; + //printf( "%d ", nBTLimit ); if ( iObj1 < iObj0 ) iObj1 ^= iObj0, iObj0 ^= iObj1, iObj1 ^= iObj0; assert( iObj0 < iObj1 ); @@ -1567,8 +1569,6 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf *pfEasy = nConfEnd == nConfBeg; } } - else - return status; } if ( status == GLUCOSE_UNSAT && iObj0 > 0 ) { @@ -1601,6 +1601,8 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf } } } + //if ( status == GLUCOSE_UNDEC ) + // printf( "* " ); return status; } int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr ) @@ -1610,7 +1612,8 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr ) Gia_Obj_t * pObj = Gia_ManObj( p->pAig, iObj ); Gia_Obj_t * pRepr = Gia_ManObj( p->pAig, iRepr ); int fCompl = Abc_LitIsCompl(pObj->Value) ^ Abc_LitIsCompl(pRepr->Value) ^ pObj->fPhase ^ pRepr->fPhase; - status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose ); + int fEffort = p->vCoDrivers ? Vec_BitEntry(p->vCoDrivers, iObj) || Vec_BitEntry(p->vCoDrivers, iRepr) : 0; + status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose, fEffort ); if ( status == GLUCOSE_SAT ) { int iLit; @@ -1635,9 +1638,12 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr ) p->pAig->iPatsPi++; Vec_IntForEachEntry( p->vPat, iLit, i ) Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) ); - Vec_IntPush( p->vPats, Vec_IntSize(p->vPat) ); - Vec_IntAppend( p->vPats, p->vPat ); - p->nPatsAll++; + if ( p->pAig->vPats ) + { + Vec_IntPush( p->pAig->vPats, Vec_IntSize(p->vPat)+2 ); + Vec_IntAppend( p->pAig->vPats, p->vPat ); + Vec_IntPush( p->pAig->vPats, -1 ); + } //Cec4_ManPackAddPattern( p->pAig, p->vPat, 0 ); //assert( iPatsOld + 1 == p->pAig->iPatsPi ); if ( fEasy ) @@ -1887,6 +1893,17 @@ Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose ) Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); return pNew; } +Gia_Man_t * Cec4_ManSimulateTest4( Gia_Man_t * p, int nBTLimit, int nBTLimitPo, int fVerbose ) +{ + Gia_Man_t * pNew = NULL; + Cec_ParFra_t ParsFra, * pPars = &ParsFra; + Cec4_ManSetParams( pPars ); + pPars->fVerbose = fVerbose; + pPars->nBTLimit = nBTLimit; + pPars->nBTLimitPo = nBTLimitPo; + Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); + return pNew; +} int Cec4_ManSimulateOnlyTest( Gia_Man_t * p, int fVerbose ) { Cec_ParFra_t ParsFra, * pPars = &ParsFra; |