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/aig/aigRepar.c | 24 +++++++++---------- src/aig/gia/giaAbsGla.c | 46 +++++++----------------------------- src/aig/gia/giaAbsVta.c | 59 +++++++++------------------------------------- src/aig/saig/saigGlaPba2.c | 14 +++++------ src/sat/bsat/satClause.h | 2 +- src/sat/bsat/satSolver2.c | 7 +++++- src/sat/bsat/satSolver2.h | 45 ++++++++++++++++++----------------- src/sat/cnf/cnfMan.c | 12 +++++----- 8 files changed, 75 insertions(+), 134 deletions(-) diff --git a/src/aig/aig/aigRepar.c b/src/aig/aig/aigRepar.c index f730a545..9232dc0f 100644 --- a/src/aig/aig/aigRepar.c +++ b/src/aig/aig/aigRepar.c @@ -52,13 +52,13 @@ static inline void Aig_ManInterAddBuffer( sat_solver2 * pSat, int iVarA, int iVa Lits[0] = toLitCond( iVarA, 0 ); Lits[1] = toLitCond( iVarB, !fCompl ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVarA, 1 ); Lits[1] = toLitCond( iVarB, fCompl ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); } @@ -83,28 +83,28 @@ static inline void Aig_ManInterAddXor( sat_solver2 * pSat, int iVarA, int iVarB, Lits[0] = toLitCond( iVarA, !fCompl ); Lits[1] = toLitCond( iVarB, 1 ); Lits[2] = toLitCond( iVarC, 1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, 0 ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVarA, !fCompl ); Lits[1] = toLitCond( iVarB, 0 ); Lits[2] = toLitCond( iVarC, 0 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, 0 ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVarA, fCompl ); Lits[1] = toLitCond( iVarB, 1 ); Lits[2] = toLitCond( iVarC, 0 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, 0 ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVarA, fCompl ); Lits[1] = toLitCond( iVarB, 0 ); Lits[2] = toLitCond( iVarC, 1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, 0 ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); } @@ -151,14 +151,14 @@ void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose ) // add clauses of A for ( i = 0; i < pCnf->nClauses; i++ ) { - Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ); + Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1], 0 ); clause2_set_partA( pSat, Cid, 1 ); } // add clauses of B Cnf_DataLift( pCnf, pCnf->nVars ); for ( i = 0; i < pCnf->nClauses; i++ ) - sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ); + sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1], 0 ); Cnf_DataLift( pCnf, -pCnf->nVars ); // add PI equality clauses @@ -282,7 +282,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose ) Cnf_DataLift( pCnf, ShiftCnf[k] ); for ( i = 0; i < pCnf->nClauses; i++ ) { - Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ); + Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1], 0 ); clause2_set_partA( pSat, Cid, k==0 ); } // add equality p[k] == A1/B1 @@ -292,7 +292,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose ) Cnf_DataLift( pCnf, pCnf->nVars ); for ( i = 0; i < pCnf->nClauses; i++ ) { - Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ); + Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1], 0 ); clause2_set_partA( pSat, Cid, k==0 ); } // add comparator (!p[k] ^ A2/B2) == or[k] @@ -302,7 +302,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose ) Aig_ManInterAddXor( pSat, ShiftP[k] + i, pCnf->pVarNums[pObj->Id], ShiftOr[k] + i, k==1, k==0 ); Vec_IntPush( vVars, toLitCond(ShiftOr[k] + i, 1) ); } - Cid = sat_solver2_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) ); + Cid = sat_solver2_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars), 0 ); clause2_set_partA( pSat, Cid, k==0 ); // return to normal Cnf_DataLift( pCnf, -ShiftCnf[k]-pCnf->nVars ); @@ -361,7 +361,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose ) // add to A for ( i = 0; i < pCnfInter->nClauses; i++ ) { - Cid = sat_solver2_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ); + Cid = sat_solver2_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1], 0 ); clause2_set_partA( pSat, Cid, c==0 ); } // connect to the inputs 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 ); diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index ee89d03f..735bb823 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -67,7 +67,6 @@ struct Vta_Man_t_ 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 sat_solver2 * pSat; // incremental SAT solver Vec_Int_t * vAddedNew; // the IDs of variables added to the solver @@ -1034,7 +1033,6 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) p->nSeenGla = 1; p->nSeenAll = 1; // other data - p->vCla2Var = Vec_IntAlloc( 1000 ); // Vec_IntPush( p->vCla2Var, -1 ); p->vCores = Vec_PtrAlloc( 100 ); p->pSat = sat_solver2_new(); // p->pSat->fVerbose = p->pPars->fVerbose; @@ -1071,7 +1069,6 @@ void Vga_ManStop( Vta_Man_t * p ) Vec_BitFreeP( &p->vSeenGla ); Vec_IntFreeP( &p->vSeens ); Vec_IntFreeP( &p->vOrder ); - Vec_IntFreeP( &p->vCla2Var ); Vec_IntFreeP( &p->vAddedNew ); sat_solver2_delete( p->pSat ); ABC_FREE( p->pBins ); @@ -1098,7 +1095,7 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f ) if ( f == 0 && Gia_ObjIsRo(p->pGia, Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj) ) return -Vta_ObjId(p, pThis); return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) ); -} +} /**Function************************************************************* @@ -1111,13 +1108,11 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls ) +Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls ) { - Vec_Int_t * vPres; - Vec_Int_t * vCore; - int k, i, Entry, RetValue; clock_t clk = clock(); - int nConfPrev = pSat->stats.conflicts; + Vec_Int_t * vCore; + int RetValue, nConfPrev = pSat->stats.conflicts; if ( piRetValue ) *piRetValue = 1; // consider special case when PO points to the flop @@ -1151,32 +1146,11 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat // 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 variables - clk = clock(); - vPres = Vec_IntStart( sat_solver2_nvars(pSat) ); - k = 0; - Vec_IntForEachEntry( vCore, Entry, i ) - { - Entry = Vec_IntEntry(vCla2Var, Entry); - if ( Vec_IntEntry(vPres, Entry) ) - continue; - Vec_IntWriteEntry( vPres, Entry, 1 ); - Vec_IntWriteEntry( vCore, k++, Entry ); - } - Vec_IntShrink( vCore, k ); - Vec_IntFree( vPres ); - 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 ); } @@ -1322,10 +1296,7 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ) iThis0 = Vta_ObjId(p, pThis0); pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame ); sat_solver2_add_and( p->pSat, iMainVar, iThis0, Vta_ObjId(p, pThis1), - Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); - Vec_IntPush( p->vCla2Var, iMainVar ); - Vec_IntPush( p->vCla2Var, iMainVar ); - Vec_IntPush( p->vCla2Var, iMainVar ); + Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0, iMainVar ); } else if ( Gia_ObjIsRo(p->pGia, pObj) ) { @@ -1334,29 +1305,23 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ) if ( p->pPars->fUseTermVars ) { pThis0 = Vga_ManFindOrAdd( p, iObj, -1 ); - sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0 ); - Vec_IntPush( p->vCla2Var, iMainVar ); - Vec_IntPush( p->vCla2Var, iMainVar ); + sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0, iMainVar ); } else { - sat_solver2_add_const( p->pSat, iMainVar, 1, 0 ); - Vec_IntPush( p->vCla2Var, iMainVar ); + sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar ); } } else { pObj = Gia_ObjRoToRi( p->pGia, pObj ); pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 ); - sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0 ); - Vec_IntPush( p->vCla2Var, iMainVar ); - Vec_IntPush( p->vCla2Var, iMainVar ); + sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0, iMainVar ); } } else if ( Gia_ObjIsConst0(pObj) ) { - sat_solver2_add_const( p->pSat, iMainVar, 1, 0 ); - Vec_IntPush( p->vCla2Var, iMainVar ); + sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar ); } else //if ( !Gia_ObjIsPi(p->pGia, pObj) ) assert( 0 ); @@ -1530,7 +1495,6 @@ void Gia_VtaPrintMemory( Vta_Man_t * p ) memOth += Vec_IntCap(p->vOrder) * sizeof(int); memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames ); memOth += Vec_BitCap(p->vSeenGla) * sizeof(int); - memOth += Vec_IntCap(p->vCla2Var) * sizeof(int); memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores ); memOth += Vec_IntCap(p->vAddedNew) * sizeof(int); memTot = memAig + memSat + memPro + memMap + memOth; @@ -1617,7 +1581,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) for ( i = 0; ; i++ ) { clk2 = clock(); - vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); + vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); assert( (vCore != NULL) == (Status == 1) ); if ( Status == -1 ) // resource limit is reached { @@ -1658,14 +1622,13 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) sat_solver2_rollback( p->pSat ); // update storage Vga_ManRollBack( p, nObjOld ); - Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses ); // load this timeframe Vga_ManLoadSlice( p, vCore, 0 ); Vec_IntFree( vCore ); // run SAT solver clk2 = clock(); - vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); + vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); p->timeUnsat += clock() - clk2; assert( (vCore != NULL) == (Status == 1) ); if ( Status == -1 ) // resource limit is reached diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c index 5e745f4c..cff7b7fc 100644 --- a/src/aig/saig/saigGlaPba2.c +++ b/src/aig/saig/saigGlaPba2.c @@ -72,7 +72,7 @@ struct Aig_Gla3Man_t_ static inline int Aig_Gla3AddConst( sat_solver2 * pSat, int iVar, int fCompl ) { lit Lit = toLitCond( iVar, fCompl ); - if ( !sat_solver2_addclause( pSat, &Lit, &Lit + 1 ) ) + if ( !sat_solver2_addclause( pSat, &Lit, &Lit + 1, 0 ) ) return 0; return 1; } @@ -94,12 +94,12 @@ static inline int Aig_Gla3AddBuffer( sat_solver2 * pSat, int iVar0, int iVar1, i Lits[0] = toLitCond( iVar0, 0 ); Lits[1] = toLitCond( iVar1, !fCompl ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) return 0; Lits[0] = toLitCond( iVar0, 1 ); Lits[1] = toLitCond( iVar1, fCompl ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) return 0; return 1; @@ -122,18 +122,18 @@ static inline int Aig_Gla3AddNode( sat_solver2 * pSat, int iVar, int iVar0, int Lits[0] = toLitCond( iVar, 1 ); Lits[1] = toLitCond( iVar0, fCompl0 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) return 0; Lits[0] = toLitCond( iVar, 1 ); Lits[1] = toLitCond( iVar1, fCompl1 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) return 0; Lits[0] = toLitCond( iVar, 0 ); Lits[1] = toLitCond( iVar0, !fCompl0 ); Lits[2] = toLitCond( iVar1, !fCompl1 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 3 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 3, 0 ) ) return 0; return 1; @@ -302,7 +302,7 @@ int Aig_Gla3CreateSatSolver( Aig_Gla3Man_t * p ) vPoLits = Vec_IntAlloc( p->nFramesMax ); for ( f = p->nStart; f < p->nFramesMax; f++ ) Vec_IntPush( vPoLits, 2 * Aig_Gla3FetchVar(p, Aig_ManCo(p->pAig, 0), f) ); - sat_solver2_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ); + sat_solver2_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits), 0 ); Vec_IntFree( vPoLits ); Vec_IntPush( p->vCla2Obj, 0 ); Vec_IntPush( p->vCla2Fra, 0 ); diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h index 7769dc36..d5df71ad 100644 --- a/src/sat/bsat/satClause.h +++ b/src/sat/bsat/satClause.h @@ -136,7 +136,7 @@ static inline lit clause_read_lit( cla h ) { return (li static inline int clause_learnt_h( Sat_Mem_t * p, cla h ) { return (h & p->uLearnedMask) > 0; } static inline int clause_learnt( clause * c ) { return c->lrn; } static inline int clause_id( clause * c ) { return c->lits[c->size]; } -static inline int clause_set_id( clause * c, int id ) { c->lits[c->size] = id; } +static inline void clause_set_id( clause * c, int id ) { c->lits[c->size] = id; } static inline int clause_size( clause * c ) { return c->size; } static inline lit * clause_begin( clause * c ) { return c->lits; } static inline lit * clause_end( clause * c ) { return c->lits + c->size; } diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 0bca05ed..7597207b 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1245,7 +1245,7 @@ void sat_solver2_delete(sat_solver2* s) } -int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) +int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end, int Id) { cla Cid; lit *i,*j,*iFree = NULL; @@ -1294,6 +1294,8 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) // create a new clause Cid = clause2_create_new( s, begin, end, 0, 0 ); + if ( Id ) + clause2_set_id( s, Cid, Id ); // handle unit clause if ( count+1 == end-begin ) @@ -1461,6 +1463,7 @@ void sat_solver2_reducedb(sat_solver2* s) continue; if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause continue; + assert( c->lrn ); c = clause2_read( s, s->reasons[i] ); assert( c->mark == 0 ); s->reasons[i] = clause_id(c); // updating handle here!!! @@ -1478,6 +1481,7 @@ void sat_solver2_reducedb(sat_solver2* s) pArray[j++] = pArray[k]; else { + assert( c->lrn ); c = clause2_read(s, pArray[k]); if ( !c->mark ) // useful learned clause pArray[j++] = clause_id(c); // updating handle here!!! @@ -1491,6 +1495,7 @@ void sat_solver2_reducedb(sat_solver2* s) for ( i = 0; i < s->size; i++ ) if ( s->units[i] && clause_learnt_h(pMem, s->units[i]) ) { + assert( c->lrn ); c = clause2_read( s, s->units[i] ); assert( c->mark == 0 ); s->units[i] = clause_id(c); diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index f5fe3000..81ecea76 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -45,7 +45,7 @@ typedef struct sat_solver2_t sat_solver2; extern sat_solver2* sat_solver2_new(void); extern void sat_solver2_delete(sat_solver2* s); -extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end); +extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end, int Id); extern int sat_solver2_simplify(sat_solver2* s); extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern void sat_solver2_rollback(sat_solver2* s); @@ -159,13 +159,14 @@ struct sat_solver2_t clock_t nRuntimeLimit; // external limit on runtime }; -static inline clause * clause2_read( sat_solver2 * s, cla h ) { return Sat_MemClauseHand( &s->Mem, h ); } +static inline clause * clause2_read( sat_solver2 * s, cla h ) { return Sat_MemClauseHand( &s->Mem, h ); } static inline int clause2_proofid(sat_solver2* s, clause* c, int partA) { return c->lrn ? (veci_begin(&s->claProofs)[clause_id(c)]<<2) | (partA<<1) : (clause_id(c)<<2) | (partA<<1) | 1; } // these two only work after creating a clause before the solver is called -static inline int clause2_is_partA (sat_solver2* s, int h) { return clause2_read(s, h)->partA; } -static inline void clause2_set_partA(sat_solver2* s, int h, int partA) { clause2_read(s, h)->partA = partA; } -static inline int clause2_id(sat_solver2* s, int h) { return clause_id(clause2_read(s, h)); } +static inline int clause2_is_partA (sat_solver2* s, int h) { return clause2_read(s, h)->partA; } +static inline void clause2_set_partA(sat_solver2* s, int h, int partA) { clause2_read(s, h)->partA = partA; } +static inline int clause2_id(sat_solver2* s, int h) { return clause_id(clause2_read(s, h)); } +static inline void clause2_set_id(sat_solver2* s, int h, int id) { clause_set_id(clause2_read(s, h), id); } //================================================================================================= // Public APIs: @@ -237,19 +238,19 @@ static inline void sat_solver2_bookmark(sat_solver2* s) Sat_MemBookMark( &s->Mem ); } -static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) +static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark, int Id ) { lit Lits[1]; int Cid; assert( iVar >= 0 ); Lits[0] = toLitCond( iVar, fCompl ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 1 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 1, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); return 1; } -static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark ) +static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark, int Id ) { lit Lits[2]; int Cid; @@ -257,43 +258,43 @@ static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVa Lits[0] = toLitCond( iVarA, 0 ); Lits[1] = toLitCond( iVarB, !fCompl ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVarA, 1 ); Lits[1] = toLitCond( iVarB, fCompl ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); return 2; } -static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark ) +static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark, int Id ) { lit Lits[3]; int Cid; Lits[0] = toLitCond( iVar, 1 ); Lits[1] = toLitCond( iVar0, fCompl0 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVar, 1 ); Lits[1] = toLitCond( iVar1, fCompl1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVar, 0 ); Lits[1] = toLitCond( iVar0, !fCompl0 ); Lits[2] = toLitCond( iVar1, !fCompl1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); return 3; } -static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark ) +static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark, int Id ) { lit Lits[3]; int Cid; @@ -302,33 +303,33 @@ static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, Lits[0] = toLitCond( iVarA, !fCompl ); Lits[1] = toLitCond( iVarB, 1 ); Lits[2] = toLitCond( iVarC, 1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVarA, !fCompl ); Lits[1] = toLitCond( iVarB, 0 ); Lits[2] = toLitCond( iVarC, 0 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVarA, fCompl ); Lits[1] = toLitCond( iVarB, 1 ); Lits[2] = toLitCond( iVarC, 0 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVarA, fCompl ); Lits[1] = toLitCond( iVarB, 0 ); Lits[2] = toLitCond( iVarC, 1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); return 4; } -static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int iVar2, int fCompl, int fMark ) +static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int iVar2, int fCompl, int fMark, int Id ) { lit Lits[2]; int Cid; @@ -336,13 +337,13 @@ static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int Lits[0] = toLitCond( iVar, fCompl ); Lits[1] = toLitCond( iVar2, 0 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVar, fCompl ); Lits[1] = toLitCond( iVar2, 1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id ); if ( fMark ) clause2_set_partA( pSat, Cid, 1 ); return 2; diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index 10043882..a8c63bf5 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -453,7 +453,7 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) sat_solver2_setnvars( pSat, p->nVars * nFrames ); for ( i = 0; i < p->nClauses; i++ ) { - if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) + if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1], 0 ) ) { sat_solver2_delete( pSat ); return NULL; @@ -472,14 +472,14 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) { Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 ); Lits[1] = f *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) { sat_solver2_delete( pSat ); return NULL; } Lits[0]++; Lits[1]--; - if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) ) { sat_solver2_delete( pSat ); return NULL; @@ -490,7 +490,7 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) pLits[i] += nLitsAll; for ( i = 0; i < p->nClauses; i++ ) { - if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) + if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1], 0 ) ) { sat_solver2_delete( pSat ); return NULL; @@ -509,7 +509,7 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) Aig_ManForEachLoSeq( p->pMan, pObjLo, i ) { Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver2_addclause( pSat, Lits, Lits + 1 ) ) + if ( !sat_solver2_addclause( pSat, Lits, Lits + 1, 0 ) ) { sat_solver2_delete( pSat ); return NULL; @@ -572,7 +572,7 @@ int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf ) pLits = ABC_ALLOC( int, Aig_ManCoNum(pCnf->pMan) ); Aig_ManForEachCo( pCnf->pMan, pObj, i ) pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan) ) ) + if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan), 0 ) ) { ABC_FREE( pLits ); return 0; -- cgit v1.2.3