summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/cec/cec.h1
-rw-r--r--src/proof/cec/cecSatG2.c93
2 files changed, 56 insertions, 38 deletions
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 1bc037c4..7c101570 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -101,6 +101,7 @@ struct Cec_ParFra_t_
int nRounds; // the number of simulation rounds
int nItersMax; // the maximum number of iterations of SAT sweeping
int nBTLimit; // conflict limit at a node
+ int nBTLimitPo; // conflict limit at an output
int TimeLimit; // the runtime limit in seconds
int nLevelMax; // restriction on the level nodes to be swept
int nDepthMax; // the depth in terms of steps of speculative reduction
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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 02:08:44 +0000