Skip to content

A
abc
Commit d931de7f by Alan Mishchenko
Options

Variable timeframe abstraction.

parent 6f4bb33c
Showing with 100 additions and 31 deletions
src/aig/gia/giaAbsVta.c
......@@ -62,6 +62,7 @@ struct Vta_Man_t_
Vec_Int_t * vSeens; // seen objects
Vec_Bit_t * vSeenGla; // seen objects in all frames
int nSeenGla; // seen objects in all frames
int nSeenAll; // seen objects in all frames
// other data
Vec_Int_t * vCla2Var; // map clauses into variables
Vec_Ptr_t * vCores; // unsat core for each frame
......@@ -149,7 +150,7 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
p->nFramesStart = 5; // starting frame
p->nFramesPast = 4; // overlap frames
p->nConfLimit = 0; // conflict limit
p->nLearntMax = 0; // max number of learned clauses
p->nLearntMax = 15000; // max number of learned clauses
p->nTimeOut = 0; // timeout in seconds
p->nRatioMin = 10; // stop when less than this % of object is abstracted
p->fUseTermVars = 1; // use terminal variables
......@@ -968,6 +969,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
if ( !Gia_ObjIsPi(p->pGia, pObj) )
Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
sat_solver2_simplify( p->pSat );
// printf( "VecCla grew to %d. \n\n", Vec_IntSize(p->vCla2Var) );
}
Vec_IntFree( vTermsToAdd );
return pCex;
......@@ -1005,6 +1008,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vSeens = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords );
p->vSeenGla = Vec_BitStart( Gia_ManObjNum(pGia) );
p->nSeenGla = 1;
p->nSeenAll = 1;
// start the abstraction
if ( pGia->vObjClasses == NULL )
p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart );
......@@ -1167,6 +1171,7 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nC
Abc_InfoSetBit( pInfo, iFrame );
pCountUni[iFrame+1]++;
pCountUni[0]++;
p->nSeenAll++;
}
pCountAll[iFrame+1]++;
pCountAll[0]++;
......@@ -1180,8 +1185,12 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nC
// printf( "%5d%5d", pCountAll[0], pCountUni[0] );
printf( "%3d :", nFrames-1 );
printf( "%6d", p->nSeenGla );
printf( "%8d", nConfls );
printf( "%5d", nCexes );
printf( "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) );
printf( "%8d", nConfls );
if ( nCexes == 0 )
printf( "%5c", '-' );
else
printf( "%5d", nCexes );
if ( vCore == NULL )
{
printf( " ..." );
......@@ -1414,7 +1423,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
printf( "FrameStart = %d FramePast = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n",
p->pPars->nFramesStart, p->pPars->nFramesPast, p->pPars->nFramesMax,
p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
printf( "Frame Abs Confl Cex Core F0 F1 F2 F3 ...\n" );
printf( "Frame Abs %% Confl Cex Core F0 F1 F2 F3 ...\n" );
}
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{
......@@ -1428,6 +1437,8 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
Vga_ManAddClausesOne( p, 0, f );
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
// printf( "VecCla grew ttto %d. \n\n", Vec_IntSize(p->vCla2Var) );
}
else
{
......
src/sat/bsat/satProof.c
......@@ -295,7 +295,55 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR
/**Function*************************************************************
Synopsis [Checks the validity of the check point.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sat_ProofReduceCheck_rec( Vec_Int_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited )
{
satset * pFanin;
int k;
if ( pNode->Id )
return;
pNode->Id = -1;
Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
Sat_ProofReduceCheck_rec( vProof, vClauses, pFanin, hClausePivot, vVisited );
else // problem clause
assert( (pNode->pEnts[k] >> 2) < hClausePivot );
Vec_PtrPush( vVisited, pNode );
}
void Sat_ProofReduceCheckOne( sat_solver2 * s, int iLearnt, Vec_Ptr_t * vVisited )
{
Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs;
int hProofNode = Vec_IntEntry( vRoots, iLearnt );
satset * pNode = Proof_NodeRead( vProof, hProofNode );
Sat_ProofReduceCheck_rec( vProof, vClauses, pNode, s->hClausePivot, vVisited );
}
void Sat_ProofReduceCheck( sat_solver2 * s )
{
Vec_Ptr_t * vVisited;
satset * c;
int h, i = 1;
vVisited = Vec_PtrAlloc( 1000 );
sat_solver_foreach_learnt( s, c, h )
if ( h < s->hLearntPivot )
Sat_ProofReduceCheckOne( s, i++, vVisited );
Vec_PtrForEachEntry( satset *, vVisited, c, i )
c->Id = 0;
Vec_PtrFree( vVisited );
}
/**Function*************************************************************
Synopsis [Reduces the proof to contain only roots and their children.]
......@@ -311,6 +359,7 @@ void Sat_ProofReduce( sat_solver2 * s )
{
Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs;
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
int fVerbose = 0;
Vec_Int_t * vUsed;
......@@ -328,9 +377,11 @@ void Sat_ProofReduce( sat_solver2 * s )
Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
{
pNode->Id = hNewHandle; hNewHandle += Proof_NodeSize(pNode->nEnts);
Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
if ( pFanin )
Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
else // problem clause
assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
}
// update roots
Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
......@@ -352,6 +403,8 @@ void Sat_ProofReduce( sat_solver2 * s )
Abc_PrintTime( 1, "Time", TimeTotal );
}
Vec_IntShrink( vProof, hNewHandle );
Sat_ProofReduceCheck( s );
}
......@@ -520,6 +573,7 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
// clean core clauses and reexpress core in terms of clause IDs
Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
{
assert( (int*)pNode < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
pNode->mark = 0;
if ( fUseIds )
// Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
......
src/sat/bsat/satSolver2.c
......@@ -1399,23 +1399,35 @@ void luby2_test()
void sat_solver2_reducedb(sat_solver2* s)
{
static int TimeTotal = 0;
cla h,* pArray,* pArray2;
satset * c, * pivot;
int Counter, CounterStart;
cla h,* pArray,* pArray2;
int * pPerm, * pClaAct, nClaAct, ActCutOff;
int i, j, k, hTemp, hHandle, clk = clock();
int Counter, CounterStart;
// check if it is time to reduce
if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax )
return;
CounterStart = s->stats.learnts - (s->nLearntMax / 3);
s->nLearntMax = s->nLearntMax * 11 / 10;
// remove 2/3 of learned clauses while skipping small clauses
// preserve 1/10 of last clauses
CounterStart = s->stats.learnts - (s->nLearntMax / 10);
// preserve 1/10 of most active clauses
pClaAct = veci_begin(&s->claActs) + 1;
nClaAct = veci_size(&s->claActs) - 1;
pPerm = Abc_SortCost( pClaAct, nClaAct );
assert( pClaAct[pPerm[0]] <= pClaAct[pPerm[nClaAct-1]] );
ActCutOff = pClaAct[pPerm[nClaAct*9/10]];
ABC_FREE( pPerm );
// ActCutOff = ABC_INFINITY;
// mark learned clauses to remove
Counter = 0;
veci_resize( &s->learnt_live, 0 );
sat_solver_foreach_learnt( s, c, h )
{
if ( Counter++ > CounterStart || c->nEnts < 3 || s->reasons[lit_var(c->pEnts[0])] == (h<<1)+1 )
if ( Counter++ > CounterStart || c->nEnts < 3 || pClaAct[c->Id-1] >= ActCutOff || s->reasons[lit_var(c->pEnts[0])] == (h<<1)+1 )
veci_push( &s->learnt_live, h );
else
c->mark = 1;
......@@ -1471,6 +1483,7 @@ void sat_solver2_reducedb(sat_solver2* s)
}
// compact clauses
pivot = satset_read( &s->learnts, s->hLearntPivot );
s->hLearntPivot = hHandle;
satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i )
{
hTemp = c->Id; c->Id = i + 1;
......@@ -1484,6 +1497,8 @@ void sat_solver2_reducedb(sat_solver2* s)
assert( hHandle == hTemp + satset_size(c->nEnts) );
veci_resize(&s->learnts,hHandle);
s->stats.learnts = veci_size(&s->learnt_live);
assert( s->hLearntPivot <= veci_size(&s->learnts) );
assert( s->hClausePivot <= veci_size(&s->clauses) );
// compact proof (compacts 'proofs' and update 'claProofs')
if ( s->fProofLogging )
......@@ -1551,24 +1566,9 @@ void sat_solver2_rollback( sat_solver2* s )
// reset watcher lists
for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
s->wlists[i].size = 0;
// clean the room
for ( i = s->iVarPivot; i < s->size; i++ )
{
*((int*)s->vi + i) = 0;
s->levels [i] = 0;
s->assigns [i] = varX;
s->reasons [i] = 0;
s->units [i] = 0;
#ifdef USE_FLOAT_ACTIVITY2
s->activity[i] = 0;
#else
s->activity[i] = (1<<10);
#endif
s->model [i] = 0;
s->orderpos[i] = -1;
}
s->size = s->iVarPivot;
// initialize other vars
s->size = s->iVarPivot;
if ( s->size == 0 )
{
// s->size = 0;
......
src/sat/bsat/satVec.h
......@@ -44,7 +44,11 @@ static inline void veci_new (veci* v) {
static inline void veci_delete (veci* v) { ABC_FREE(v->ptr); }
static inline int* veci_begin (veci* v) { return v->ptr; }
static inline int veci_size (veci* v) { return v->size; }
static inline void veci_resize (veci* v, int k) { assert(k <= v->size); v->size = k; } // only safe to shrink !!
static inline void veci_resize (veci* v, int k) {
assert(k <= v->size);
// memset( veci_begin(v) + k, -1, sizeof(int) * (veci_size(v) - k) );
v->size = k;
} // only safe to shrink !!
static inline int veci_pop (veci* v) { assert(v->size); return v->ptr[--v->size]; }
static inline void veci_push (veci* v, int e)
{
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment