Skip to content

A
abc
Commit 24275632 by Alan Mishchenko
Options

Changes to clause mapping.

parent 05c8b785
Showing with 70 additions and 129 deletions
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
......
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 );
......
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 );
......@@ -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
......
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 );
......
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; }
......
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);
......
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);
......@@ -166,6 +166,7 @@ static inline int clause2_proofid(sat_solver2* s, clause* c, int partA) {
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;
......
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;
......
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