From 2427563269566c458f475dfe6fa4388dac80aa02 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 11 Jul 2012 15:33:31 -0700 Subject: Changes to clause mapping. --- src/aig/gia/giaAbsGla.c | 46 +++++++++------------------------------------- 1 file changed, 9 insertions(+), 37 deletions(-) (limited to 'src/aig/gia/giaAbsGla.c') diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 001cd6ee..a19d4d75 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -79,7 +79,6 @@ struct Gla_Man_t_ int nSatVars; // the number of SAT variables Cnf_Dat_t * pCnf; // CNF derived for the nodes sat_solver2 * pSat; // incremental SAT solver - Vec_Int_t * vCla2Obj; // mapping of clauses into GLA objs Vec_Int_t * vTemp; // temporary array Vec_Int_t * vAddedNew; // temporary array Vec_Int_t * vObjCounts; // object counters @@ -1096,7 +1095,6 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars ) Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) ); } // other - p->vCla2Obj = Vec_IntAlloc( 1000 ); // Vec_IntPush( p->vCla2Obj, -1 ); p->pSat = sat_solver2_new(); // p->pSat->fVerbose = p->pPars->fVerbose; // sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax ); @@ -1195,7 +1193,6 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) ); } // other - p->vCla2Obj = Vec_IntAlloc( 1000 ); // Vec_IntPush( p->vCla2Obj, -1 ); p->pSat = sat_solver2_new(); p->nSatVars = 1; return p; @@ -1229,7 +1226,6 @@ void Gla_ManStop( Gla_Man_t * p ) // Gia_ManStaticFanoutStart( p->pGia0 ); sat_solver2_delete( p->pSat ); Vec_IntFreeP( &p->vObjCounts ); - Vec_IntFreeP( &p->vCla2Obj ); Vec_IntFreeP( &p->vAddedNew ); Vec_IntFreeP( &p->vCoreCounts ); Vec_IntFreeP( &p->vTemp ); @@ -1434,9 +1430,7 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits ) if ( pGlaObj->fConst ) { iVar = Gla_ManGetVar( p, iObj, iFrame ); - sat_solver2_add_const( p->pSat, iVar, 1, 0 ); - // remember the clause - Vec_IntPush( p->vCla2Obj, iObj ); + sat_solver2_add_const( p->pSat, iVar, 1, 0, iObj ); } else if ( pGlaObj->fRo ) { @@ -1444,18 +1438,13 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits ) if ( iFrame == 0 ) { iVar = Gla_ManGetVar( p, iObj, iFrame ); - sat_solver2_add_const( p->pSat, iVar, 1, 0 ); - // remember the clause - Vec_IntPush( p->vCla2Obj, iObj ); + sat_solver2_add_const( p->pSat, iVar, 1, 0, iObj ); } else { iVar1 = Gla_ManGetVar( p, iObj, iFrame ); iVar2 = Gla_ManGetVar( p, pGlaObj->Fanins[0], iFrame-1 ); - sat_solver2_add_buffer( p->pSat, iVar1, iVar2, pGlaObj->fCompl0, 0 ); - // remember the clause - Vec_IntPush( p->vCla2Obj, iObj ); - Vec_IntPush( p->vCla2Obj, iObj ); + sat_solver2_add_buffer( p->pSat, iVar1, iVar2, pGlaObj->fCompl0, 0, iObj ); } } else if ( pGlaObj->fAnd ) @@ -1471,10 +1460,7 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits ) iVar = Gla_ManGetVar( p, lit_var(*pLit), iFrame ); Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) ); } - RetValue = sat_solver2_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); - assert( RetValue ); - // remember the clause - Vec_IntPush( p->vCla2Obj, iObj ); + RetValue = sat_solver2_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits), iObj ); } } else assert( 0 ); @@ -1555,12 +1541,11 @@ int Gla_ManGetOutLit( Gla_Man_t * p, int f ) return -1; return Abc_Var2Lit( iSat, p->pObjRoot->fCompl0 ); } -Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls ) +Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls ) { Vec_Int_t * vCore; - int iLit = Gla_ManGetOutLit( p, f ); int nConfPrev = pSat->stats.conflicts; - int i, Entry, RetValue; + int RetValue, iLit = Gla_ManGetOutLit( p, f ); clock_t clk = clock(); if ( piRetValue ) *piRetValue = 1; @@ -1595,23 +1580,11 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_so // Abc_PrintTime( 1, "Time", clock() - clk ); } assert( RetValue == l_False ); - // derive the UNSAT core clk = clock(); vCore = (Vec_Int_t *)Sat_ProofCore( pSat ); if ( fVerbose ) { -// Abc_Print( 1, "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) ); -// Abc_PrintTime( 1, "Time", clock() - clk ); - } - - // remap core into original objects - Vec_IntForEachEntry( vCore, Entry, i ) - Vec_IntWriteEntry( vCore, i, Vec_IntEntry(p->vCla2Obj, Entry) ); - Vec_IntUniqify( vCore ); - Vec_IntReverseOrder( vCore ); - if ( fVerbose ) - { // Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) ); // Abc_PrintTime( 1, "Time", clock() - clk ); } @@ -1670,7 +1643,6 @@ void Gla_ManReportMemory( Gla_Man_t * p ) memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int); for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ ) memRef += Vec_IntCap(&p->pvRefis[i]) * sizeof(int); - memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int); memOth += Vec_IntCap(p->vAddedNew) * sizeof(int); memOth += Vec_IntCap(p->vTemp) * sizeof(int); memOth += Vec_IntCap(p->vAbs) * sizeof(int); @@ -1841,7 +1813,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) for ( i = 0; ; i++ ) { clk2 = clock(); - vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); + vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); assert( (vCore != NULL) == (Status == 1) ); if ( Status == -1 ) // resource limit is reached { @@ -1914,15 +1886,15 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) sat_solver2_rollback( p->pSat ); // update storage Gla_ManRollBack( p ); - Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses ); p->nSatVars = nVarsOld; // load this timeframe + Vec_IntSort( vCore, 1 ); Gia_GlaAddToAbs( p, vCore, 0 ); Gia_GlaAddOneSlice( p, f, vCore ); Vec_IntFree( vCore ); // run SAT solver clk2 = clock(); - vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); + vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); p->timeUnsat += clock() - clk2; assert( (vCore != NULL) == (Status == 1) ); Vec_IntFreeP( &vCore ); -- cgit v1.2.3