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 +++++------ 4 files changed, 39 insertions(+), 104 deletions(-) (limited to 'src/aig') 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 ); -- cgit v1.2.3