luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Variable timeframe abstraction.

This commit is contained in:
Alan Mishchenko 2012-01-27 00:48:06 -08:00
parent c7e855619a
commit ce0e8caf79
6 changed files with 200 additions and 307 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

160
src/aig/gia/giaAbsVta.c
View File

@ -66,7 +66,12 @@ struct Vta_Man_t_
Vec_Int_t * vCla2Var; // map clauses into variables
Vec_Ptr_t * vCores; // unsat core for each frame
sat_solver2 * pSat; // incremental SAT solver
int iPivot;
Vec_Int_t * vAddedNew; // the IDs of variables added to the solver
// statistics
int timeSat;
int timeUnsat;
int timeCex;
int timeOther;
};
@ -351,7 +356,7 @@ int Vec_IntDoubleWidth( Vec_Int_t * p, int nWords )
***********************************************************************/
static inline int Vga_ManHash( int iObj, int iFrame, int nBins )
{
return ((iObj + iFrame)*(iObj + iFrame + 1)) % nBins;
return ((unsigned)((iObj + iFrame)*(iObj + iFrame + 1))) % nBins;
}
static inline int * Vga_ManLookup( Vta_Man_t * p, int iObj, int iFrame )
{
@ -605,6 +610,8 @@ void Vta_ManSatVerify( Vta_Man_t * p )
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
int VarA = Vta_ObjId(p,pThis);
int VarB = !pThis0 ? 0 : Vta_ObjId(p,pThis0);
pObj = Gia_ObjRoToRi( p->pGia, pObj );
if ( pThis->iFrame == 0 )
assert( pThis->Value == VTA_VAR0 );
@ -637,7 +644,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
Gia_Obj_t * pObj;
int i, Counter;
Vta_ManSatVerify( p );
// Vta_ManSatVerify( p );
// collect nodes in a topological order
vOrder = Vta_ManCollectNodes( p, f );
@ -647,7 +654,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
pThis->fVisit = 0;
}
/*
// verify
Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
{
@ -674,7 +681,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
else assert( 0 );
}
}
*/
// compute distance in reverse order
pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
pThis->Prio = 1;
@ -787,7 +794,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
pTop = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
pTop->fVisit = 1;
vTermsToAdd = Vec_IntAlloc( 100 );
printf( "\n\n" );
Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
{
if ( !pThis->fVisit )
@ -816,8 +822,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
assert( pThis1->Prio <= pThis->Prio );
pThis0->fVisit = 1;
pThis1->fVisit = 1;
// printf( "And1 %d requires %d %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0), Vta_ObjId(p,pThis1) );
}
else if ( pThis->Value == VTA_VAR0 )
{
@ -825,36 +829,30 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
{
if ( pThis0->fVisit )
{
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
}
else if ( pThis1->fVisit )
{
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
}
else if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
{
pThis0->fVisit = 1;
assert( pThis0->Prio == pThis->Prio );
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
}
else
{
pThis1->fVisit = 1;
assert( pThis1->Prio == pThis->Prio );
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
}
}
else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
{
pThis0->fVisit = 1;
assert( pThis0->Prio == pThis->Prio );
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
}
else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
{
pThis1->fVisit = 1;
assert( pThis1->Prio == pThis->Prio );
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
}
else assert( 0 );
}
@ -869,14 +867,13 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
assert( pThis0 );
pThis0->fVisit = 1;
assert( pThis0->Prio == pThis->Prio );
// printf( "Reg %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
}
}
else if ( !Gia_ObjIsConst0(pObj) )
assert( 0 );
}
//printf( "\n" );
/*
// verify
Vta_ManForEachObjVec( vOrder, p, pThis, i )
pThis->Value = VTA_VARX;
@ -941,32 +938,18 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
// else
// printf( "Verification OK.\n" );
*/
// produce true counter-example
if ( pTop->Prio == 0 )
pCex = Vga_ManDeriveCex( p );
/*
{
pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
pCex->iPo = 0;
pCex->iFrame = p->pPars->iFrame;
Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
{
assert( pThis->Value == VTA_VAR0 || pThis->Value == VTA_VAR1 );
assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsCi(pObj) );
if ( Gia_ObjIsRo(p->pGia, pObj) )
assert( pThis->iFrame == 0 && pThis->Value == VTA_VAR0 );
else if ( Gia_ObjIsPi(p->pGia, pObj) && pThis->Value == VTA_VAR1 )
Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
}
}
*/
// perform refinement
else
{
int nObjOld = p->nObjs;
Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
if ( !Gia_ObjIsPi(p->pGia, pObj) )
Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
sat_solver2_simplify( p->pSat );
}
Vec_IntFree( vTermsToAdd );
return pCex;
@ -993,7 +976,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->nObjsAlloc = (1 << 20);
p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc );
p->nObjs = 1;
p->nBins = Abc_PrimeCudd( p->nObjsAlloc/2 );
p->nBins = Abc_PrimeCudd( 2*p->nObjsAlloc );
p->pBins = ABC_CALLOC( int, p->nBins );
p->vOrder = Vec_IntAlloc( 1013 );
// abstraction
@ -1023,10 +1006,10 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
}
}
// other data
p->vCla2Var = Vec_IntAlloc( 1000 );
p->vCla2Var = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Var, -1 );
p->vCores = Vec_PtrAlloc( 100 );
p->pSat = sat_solver2_new();
p->iPivot = Gia_ObjFaninId0p(p->pGia, Gia_ManPo(p->pGia, 0));
p->vAddedNew = Vec_IntAlloc( 1000 );
return p;
}
@ -1043,7 +1026,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
***********************************************************************/
void Vga_ManStop( Vta_Man_t * p )
{
if ( p->pPars->fVerbose )
// if ( p->pPars->fVerbose )
printf( "SAT solver: Variables = %d. Clauses = %d. Conflicts = %d.\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat) );
@ -1053,6 +1036,7 @@ void Vga_ManStop( Vta_Man_t * p )
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 );
ABC_FREE( p->pObjs );
@ -1144,7 +1128,7 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
SeeAlso []
***********************************************************************/
void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int fVerbose )
void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCexes, int fVerbose )
{
unsigned * pInfo;
int * pCountAll, * pCountUni;
@ -1176,6 +1160,7 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int fV
{
// printf( "%5d%5d", pCountAll[0], pCountUni[0] );
printf( "%6d", p->nSeenGla );
printf( "%5d", nCexes );
printf( "%6d", pCountAll[0] );
for ( k = 0; k < nFrames; k++ )
// printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] );
@ -1203,38 +1188,25 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
Vta_Obj_t * pThis0, * pThis1;
Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
int iMainVar = Vta_ObjId(p, pThis);
int iThis0, iMainVar = Vta_ObjId(p, pThis);
assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
if ( iObj == 317 && iFrame == 0 )
{
int s = 0;
}
if ( pThis->fAdded )
{
// if ( p->iPivot == iObj )
// printf( "Pivot in frame %d is already added\n", iFrame );
return;
}
// if ( p->iPivot == iObj )
// printf( "Adding pivot in frame %d\n", iFrame );
// printf( "(%d,%d) ", iObj, iFrame );
pThis->fAdded = 1;
Vec_IntPush( p->vAddedNew, iMainVar );
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
iThis0 = Vta_ObjId(p, pThis0);
pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
sat_solver2_add_and( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Vta_ObjId(p, pThis1),
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 );
//printf( "Adding node %d (var %d)\n", iObj, iMainVar );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
//printf( "Adding flop %d (var %d)\n", iObj, iMainVar );
if ( iFrame == 0 )
{
if ( p->pPars->fUseTermVars )
@ -1253,7 +1225,7 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
else
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
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 );
@ -1261,7 +1233,6 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
}
else if ( Gia_ObjIsConst0(pObj) )
{
//printf( "Adding const %d (var %d)\n", iObj, iMainVar );
sat_solver2_add_const( p->pSat, iMainVar, 1, 0 );
Vec_IntPush( p->vCla2Var, iMainVar );
}
@ -1286,7 +1257,7 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
Vec_IntForEachEntry( vOne, Entry, i )
Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
sat_solver2_simplify( p->pSat );
printf( "\n\n" );
// printf( "\n\n" );
}
/**Function*************************************************************
@ -1346,10 +1317,18 @@ void Vga_ManRollBack( Vta_Man_t * p, int nObjOld )
{
Vta_Obj_t * pThis = p->pObjs + nObjOld;
Vta_Obj_t * pLimit = p->pObjs + p->nObjs;
int i, Entry;
for ( ; pThis < pLimit; pThis++ )
Vga_ManDelete( p, pThis->iObj, pThis->iFrame );
memset( p->pObjs + nObjOld, 0, sizeof(Vta_Obj_t) * (p->nObjs - nObjOld) );
p->nObjs = nObjOld;
Vec_IntForEachEntry( p->vAddedNew, Entry, i )
if ( Entry < p->nObjs )
{
pThis = Vta_ManObj(p, Entry);
assert( pThis->fAdded == 1 );
pThis->fAdded = 0;
}
}
/**Function*************************************************************
@ -1369,7 +1348,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Vec_Int_t * vCore;
Abc_Cex_t * pCex = NULL;
int i, f, nConfls, Status, RetValue = -1;
int clk = clock();
int clk = clock(), clk2;
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
@ -1377,7 +1356,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
p = Vga_ManStart( pAig, pPars );
// perform initial abstraction
if ( p->pPars->fVerbose )
printf( "Frame Confl One All F0 F1 F2 F3 ...\n" );
printf( "Frame Confl One Cex All F0 F1 F2 F3 ...\n" );
for ( f = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{
if ( p->pPars->fVerbose )
@ -1387,62 +1366,60 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
if ( f == p->nWords * 32 )
p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
// check this timeframe
i = 0;
if ( f < p->pPars->nFramesStart )
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
else
// for ( f = 0; f < p->pPars->nFramesStart; f++ )
// Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
{
// create bookmark to be used for rollback
int nObjOld;
int nClaOld;
//start:
nObjOld = p->nObjs;
nClaOld = Vec_IntSize(p->vCla2Var);
int nObjOld = p->nObjs;
sat_solver2_bookmark( p->pSat );
Vec_IntClear( p->vAddedNew );
// load the time frame
for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesOver, p->pPars->nFramesStart); i++ )
{
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
//Vga_ManPrintCore( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
}
// iterate as long as there are counter-examples
for ( i = 1; ; i++ )
for ( i = 0; ; i++ )
{
clk2 = clock();
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 ) // resource limit is reached
goto finish;
if ( vCore != NULL )
{
p->timeUnsat += clock() - clk2;
break;
printf( "Frame %d iter %d...\n", f, i );
}
p->timeSat += clock() - clk2;
assert( Status == 0 );
// perform the refinement
clk2 = clock();
pCex = Vta_ManRefineAbstraction( p, f );
p->timeCex += clock() - clk2;
if ( pCex != NULL )
goto finish;
}
assert( Status == 1 );
/*
// valid core is obtained
Vta_ManUnsatCoreRemap( p, vCore );
printf( "Double checked core...\n" );
Vga_ManPrintCore( p, vCore, 0 );
// Vec_IntSort( vCore, 0 );
Vec_IntSort( vCore, 1 );
// update the SAT solver
sat_solver2_rollback( p->pSat );
// update storage
Vga_ManRollBack( p, nObjOld );
Vec_IntShrink( p->vCla2Var, nClaOld );
Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 );
// load this timeframe
nObjOld = p->nObjs;
Vga_ManLoadSlice( p, vCore, 0 );
*/
Vec_IntFree( vCore );
// goto start;
}
// run SAT solver
clk2 = clock();
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
p->timeUnsat += clock() - clk2;
if ( p->pPars->fVerbose )
printf( "%6d", nConfls );
printf( "%5d", nConfls );
assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 ) // resource limit is reached
goto finish;
@ -1454,20 +1431,11 @@ Vga_ManPrintCore( p, vCore, 0 );
}
// add the core
Vta_ManUnsatCoreRemap( p, vCore );
if ( f >= p->pPars->nFramesStart )
{
// printf( "Core to record:\n" );
// Vga_ManPrintCore( p, vCore, 0 );
}
// add in direct topological order
// Vec_IntSort( vCore, 1 );
Vec_IntSort( vCore, 1 );
Vec_PtrPush( p->vCores, vCore );
// print the result
Vta_ManAbsPrintFrame( p, vCore, f+1, p->pPars->fVerbose );
// if ( f == p->pPars->nFramesStart-1 )
// break;
Vta_ManAbsPrintFrame( p, vCore, f+1, i, p->pPars->fVerbose );
}
finish:
// analize the results
@ -1481,7 +1449,7 @@ finish:
if ( Status == -1 )
printf( "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );
else
printf( "SAT solver completed %d frames and produced an abstraction. ", f+1 );
printf( "SAT solver completed %d frames and produced an abstraction. ", f );
}
else
{
@ -1492,6 +1460,14 @@ finish:
printf( "Counter-example detected in frame %d. ", f );
}
Abc_PrintTime( 1, "Time", clock() - clk );
p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
ABC_PRTP( "Solver UNSAT", p->timeUnsat, clock() - clk );
ABC_PRTP( "Solver SAT ", p->timeSat, clock() - clk );
ABC_PRTP( "Refinement ", p->timeCex, clock() - clk );
ABC_PRTP( "Other ", p->timeOther, clock() - clk );
ABC_PRTP( "TOTAL ", clock() - clk, clock() - clk );
Vga_ManStop( p );
return RetValue;
}

6
src/aig/saig/saigGlaPba2.c
View File

@ -308,7 +308,7 @@ int Aig_Gla3CreateSatSolver( Aig_Gla3Man_t * p )
Vec_IntPush( p->vCla2Fra, 0 );
assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) );
assert( nVars == Vec_IntSize(p->vVar2Inf) );
assert( Vec_IntSize(p->vCla2Obj) == (int)p->pSat->stats.clauses );
assert( Vec_IntSize(p->vCla2Obj) == (int)p->pSat->stats.clauses+1 );
if ( p->fVerbose )
printf( "The resulting SAT problem contains %d variables and %d clauses.\n",
p->pSat->size, p->pSat->stats.clauses );
@ -337,8 +337,8 @@ Aig_Gla3Man_t * Aig_Gla3ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax,
p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) );
p->vVec2Var = Vec_IntAlloc( 1 << 20 );
p->vVar2Inf = Vec_IntAlloc( 1 << 20 );
p->vCla2Obj = Vec_IntAlloc( 1 << 20 );
p->vCla2Fra = Vec_IntAlloc( 1 << 20 );
p->vCla2Obj = Vec_IntAlloc( 1 << 20 ); Vec_IntPush( p->vCla2Obj, -1 );
p->vCla2Fra = Vec_IntAlloc( 1 << 20 ); Vec_IntPush( p->vCla2Fra, -1 );
// skip first vector ID
p->nStart = nStart;

2
src/base/abci/abc.c
View File

@ -26234,7 +26234,7 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The number of frames should be a positive integer.\n" );
return 0;
}
if ( pPars->nStart > 0 && pPars->nStart >= pPars->nFramesMax )
if ( pPars->nStart > 0 && pPars->nFramesMax > 0 && pPars->nStart >= pPars->nFramesMax )
{
Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
return 0;

35
src/sat/bsat/satProof.c
View File

@ -447,9 +447,13 @@ void Sat_ProofCheck( sat_solver2 * s )
Vec_Int_t * vUsed, * vTemp;
satset * pSet, * pSet0, * pSet1;
int i, k, hRoot, Handle, Counter = 0, clk = clock();
if ( s->hLearntLast < 0 )
// if ( s->hLearntLast < 0 )
// return;
// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
hRoot = s->hProofLast;
if ( hRoot == -1 )
return;
hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
// collect visited clauses
vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
Proof_CleanCollected( vProof, vUsed );
@ -490,7 +494,7 @@ void Sat_ProofCheck( sat_solver2 * s )
Synopsis [Collects nodes belonging to the UNSAT core.]
Description [The resulting array contains 0-based IDs of root clauses.]
Description [The resulting array contains 1-based IDs of root clauses.]
SideEffects []
@ -518,7 +522,8 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
{
pNode->mark = 0;
if ( fUseIds )
Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
// Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
Vec_IntWriteEntry( vCore, i, pNode->Id );
}
return vCore;
}
@ -592,9 +597,12 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
Aig_Man_t * pAig;
Aig_Obj_t * pObj;
int i, k, iVar, Lit, Entry, hRoot;
if ( s->hLearntLast < 0 )
// if ( s->hLearntLast < 0 )
// return NULL;
// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
hRoot = s->hProofLast;
if ( hRoot == -1 )
return NULL;
hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Sat_ProofInterpolantCheckVars( s, vGlobVars );
@ -693,9 +701,12 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
word * pRes = ABC_ALLOC( word, nWords );
int i, k, iVar, Lit, Entry, hRoot;
assert( nVars > 0 && nVars <= 16 );
if ( s->hLearntLast < 0 )
// if ( s->hLearntLast < 0 )
// return NULL;
// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
hRoot = s->hProofLast;
if ( hRoot == -1 )
return NULL;
hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Sat_ProofInterpolantCheckVars( s, vGlobVars );
@ -794,9 +805,13 @@ void * Sat_ProofCore( sat_solver2 * s )
Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
Vec_Int_t * vCore, * vUsed;
int hRoot;
if ( s->hLearntLast < 0 )
// if ( s->hLearntLast < 0 )
// return NULL;
// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
hRoot = s->hProofLast;
if ( hRoot == -1 )
return NULL;
hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
// collect visited clauses
vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
// collect core clauses

296
src/sat/bsat/satSolver2.c
View File

@ -28,7 +28,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
ABC_NAMESPACE_IMPL_START
#define SAT_USE_ANALYZE_FINAL
#define SAT_USE_PROOF_LOGGING
//=================================================================================================
@ -150,7 +149,9 @@ static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1
static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; }
static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; }
static inline satset* var_unit_clause(sat_solver2* s, int v) { return clause_read(s, s->units[v]); }
static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; }
static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){
assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++;
}
//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; }
// these two only work after creating a clause before the solver is called
@ -501,13 +502,8 @@ static void solver2_canceluntil(sat_solver2* s, int level) {
int bound;
int lastLev;
int c, x;
if ( level == 0 )
{
int ss = 0;
}
if (solver2_dlevel(s) <= level)
if (solver2_dlevel(s) < level)
return;
trail = s->trail;
@ -532,7 +528,7 @@ static void solver2_canceluntil(sat_solver2* s, int level) {
}
static void solver2_record(sat_solver2* s, veci* cls, int proof_id, int fSkipUnit)
static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
{
lit* begin = veci_begin(cls);
lit* end = begin + veci_size(cls);
@ -540,7 +536,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id, int fSkipUni
assert(veci_size(cls) > 0);
if ( veci_size(cls) == 1 )
{
if ( s->fProofLogging && !fSkipUnit)
if ( s->fProofLogging )
var_set_unit_clause(s, lit_var(begin[0]), Cid);
Cid = 0;
}
@ -610,14 +606,12 @@ void Solver::analyzeFinal(satset* confl, bool skip_first)
}
*/
#ifdef SAT_USE_ANALYZE_FINAL
static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
{
int i, j, x;//, start;
veci_resize(&s->conf_final,0);
if ( s->root_level == 0 )
return -1;
return s->hProofLast;
proof_chain_start( s, conf );
assert( veci_size(&s->tagged) == 0 );
satset_foreach_var( conf, x, i, skip_first ){
@ -650,9 +644,6 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
return proof_chain_stop( s );
}
#endif
static int solver2_lit_removable_rec(sat_solver2* s, int v)
{
// tag[0]: True if original conflict clause literal.
@ -916,8 +907,6 @@ satset* solver2_propagate(sat_solver2* s)
end = begin + veci_size(ws);
s->stats.propagations++;
s->simpdb_props--;
for (i = j = begin; i < end; ){
c = clause_read(s,*i);
lits = c->pEnts;
@ -968,7 +957,8 @@ satset* solver2_propagate(sat_solver2* s)
proof_chain_start( s, clause_read(s,Cid) );
proof_chain_resolve( s, NULL, Var );
proof_id = proof_chain_stop( s );
clause_create_new( s, &Lit, &Lit, 1, proof_id );
s->hProofLast = proof_id;
// clause_create_new( s, &Lit, &Lit, 1, proof_id );
}
}
@ -990,71 +980,10 @@ WatchFound: i++;
return confl;
}
/*
static void clause_remove(sat_solver2* s, satset* c)
{
assert(lit_neg(c->pEnts[0]) < s->size*2);
assert(lit_neg(c->pEnts[1]) < s->size*2);
veci_remove(solver2_wlist(s,lit_neg(c->pEnts[0])),clause_handle(s,c));
veci_remove(solver2_wlist(s,lit_neg(c->pEnts[1])),clause_handle(s,c));
if (c->learnt){
s->stats.learnts--;
s->stats.learnts_literals -= c->nEnts;
}else{
s->stats.clauses--;
s->stats.clauses_literals -= c->nEnts;
}
}
*/
static lbool clause_simplify(sat_solver2* s, satset* c)
{
int i, x;
assert(solver2_dlevel(s) == 0);
satset_foreach_var( c, x, i, 0 )
if (var_value(s, x) == lit_sign(c->pEnts[i]))
return l_True;
return l_False;
}
int sat_solver2_simplify(sat_solver2* s)
{
int TailOld = s->qtail;
// int type;
int Counter = 0;
assert(solver2_dlevel(s) == 0);
// reset the head
s->qhead = 0;
if (solver2_propagate(s) != 0)
return false;
// printf( "Tail moved from %d to %d.\n", TailOld, s->qtail );
if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
return true;
/*
for (type = 0; type < 2; type++){
veci* cs = type ? &s->learnts : &s->clauses;
int* cls = (int*)veci_begin(cs);
int i, j;
for (j = i = 0; i < veci_size(cs); i++){
satset* c = clause_read(s,cls[i]);
if (lit_reason(s,c->pEnts[0]) != cls[i] &&
clause_simplify(s,c) == l_True)
clause_remove(s,c), Counter++;
else
cls[j++] = cls[i];
}
veci_resize(cs,j);
}
*/
//printf( "Simplification removed %d clauses (out of %d)...\n", Counter, s->stats.clauses );
s->simpdb_assigns = s->qhead;
// (shouldn't depend on 'stats' really, but it will do for now)
s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
return true;
return (solver2_propagate(s) == NULL);
}
/*
@ -1123,11 +1052,10 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
#endif
s->stats.conflicts++; conflictC++;
if (solver2_dlevel(s) <= s->root_level){
#ifdef SAT_USE_ANALYZE_FINAL
proof_id = solver2_analyze_final(s, confl, 0);
assert( proof_id > 0 );
solver2_record(s,&s->conf_final, proof_id, 0);
#endif
// solver2_record(s,&s->conf_final, proof_id);
s->hProofLast = proof_id;
veci_delete(&learnt_clause);
return l_False;
}
@ -1137,13 +1065,11 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level;
blevel = s->root_level > blevel ? s->root_level : blevel;
solver2_canceluntil(s,blevel);
solver2_record(s,&learnt_clause, proof_id, 0);
#ifdef SAT_USE_ANALYZE_FINAL
solver2_record(s,&learnt_clause, proof_id);
// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;
// (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
if ( learnt_clause.size == 1 )
var_set_level( s, lit_var(learnt_clause.ptr[0]), 0 );
#endif
act_var_decay(s);
act_clause_decay(s);
@ -1169,9 +1095,9 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
return l_Undef;
}
if (solver2_dlevel(s) == 0 && !s->fSkipSimplify)
// if (solver2_dlevel(s) == 0 && !s->fSkipSimplify)
// Simplify the set of problem clauses:
sat_solver2_simplify(s);
// sat_solver2_simplify(s);
// New variable decision:
s->stats.decisions++;
@ -1267,9 +1193,12 @@ sat_solver2* sat_solver2_new(void)
veci_push(&s->proofs, -1);
}
// initialize clause pointers
s->hClausePivot = 1;
s->hLearntPivot = 1;
s->hLearntLast = -1; // the last learnt clause
s->hProofLast = -1; // the last proof ID
s->hClausePivot = 1; // the pivot among clauses
s->hLearntPivot = 1; // the pivot moang learned clauses
s->iVarPivot = 0; // the pivot among the variables
s->iSimpPivot = 0; // marker of unit-clauses
return s;
}
@ -1381,65 +1310,12 @@ void sat_solver2_delete(sat_solver2* s)
}
int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end)
{
lit *i,*j;
int maxvar;
lit last;
if (begin == end)
{
assert( 0 );
return false;
}
// copy clause into storage
veci_resize( &s->temp_clause, 0 );
for ( i = begin; i < end; i++ )
veci_push( &s->temp_clause, *i );
begin = veci_begin( &s->temp_clause );
end = begin + veci_size( &s->temp_clause );
//printlits(begin,end); printf("\n");
// insertion sort
maxvar = lit_var(*begin);
for (i = begin + 1; i < end; i++){
lit l = *i;
maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
for (j = i; j > begin && *(j-1) > l; j--)
*j = *(j-1);
*j = l;
}
sat_solver2_setnvars(s,maxvar+1);
// delete duplicates
last = lit_Undef;
for (i = j = begin; i < end; i++){
//printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -var_value(s, lit_var(*i)) : var_value(s, lit_var(*i))));
if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i))
return true; // tautology
else if (*i != last && var_value(s, lit_var(*i)) == varX)
last = *j++ = *i;
}
//printf("final: "); printlits(begin,j); printf("\n");
if (j == begin) // empty clause
{
assert( 0 );
return false;
}
if (j - begin == 1) // unit clause
return solver2_enqueue(s,*begin,0);
// create new clause
return clause_create_new(s,begin,j,0,0);
}
int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
{
cla Cid;
lit *i,*j;
int maxvar;
lit *i,*j,*iFree = NULL;
int maxvar, count, temp;
assert( solver2_dlevel(s) == 0 );
assert( begin < end );
// copy clause into storage
@ -1460,19 +1336,58 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
}
sat_solver2_setnvars(s,maxvar+1);
// coount the number of 0-literals
count = 0;
for ( i = begin; i < end; i++ )
{
// make sure all literals are unique
assert( i == begin || lit_var(*(i-1)) != lit_var(*i) );
// consider the value of this literal
if ( var_value(s, lit_var(*i)) == lit_sign(*i) ) // this clause is always true
return clause_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count
if ( var_value(s, lit_var(*i)) == varX ) // unassigned literal
iFree = i;
else
count++; // literal is 0
}
assert( count < end-begin ); // the clause cannot be UNSAT
// swap variables to make sure the clause is watched using unassigned variable
temp = *iFree;
*iFree = *begin;
*begin = temp;
// create a new clause
Cid = clause_create_new( s, begin, end, 0, 0 );
// handle unit clause
if ( begin + 1 == end )
if ( count+1 == end-begin )
{
// printf( "Adding unit clause %d\n", begin[0] );
// solver2_canceluntil(s, 0);
if ( s->fProofLogging )
var_set_unit_clause( s, lit_var(begin[0]), Cid );
if ( !solver2_enqueue(s,begin[0],0) )
assert( 0 );
{
if ( count == 0 ) // original learned clause
{
var_set_unit_clause( s, lit_var(begin[0]), Cid );
if ( !solver2_enqueue(s,begin[0],0) )
assert( 0 );
}
else
{
// Log production of top-level unit clause:
int x, k, proof_id, CidNew;
satset* c = clause_read(s, Cid);
proof_chain_start( s, c );
satset_foreach_var( c, x, k, 1 )
proof_chain_resolve( s, NULL, x );
proof_id = proof_chain_stop( s );
// generate a new clause
CidNew = clause_create_new( s, begin, begin+1, 1, proof_id );
var_set_unit_clause( s, lit_var(begin[0]), CidNew );
if ( !solver2_enqueue(s,begin[0],Cid) )
assert( 0 );
}
}
}
//satset_print( clause_read(s, Cid) );
return Cid;
}
@ -1571,6 +1486,7 @@ void solver2_reducedb(sat_solver2* s)
void sat_solver2_rollback( sat_solver2* s )
{
int i, k, j;
assert( s->qhead == s->qtail );
assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) );
assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) );
assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
@ -1596,34 +1512,37 @@ void sat_solver2_rollback( sat_solver2* s )
veci_resize(&s->wlists[i],j);
}
// compact units
if ( s->fProofLogging )
for ( i = 0; i < s->size; i++ )
if ( s->units[i] && !clause_is_used(s, s->units[i]) )
s->units[i] = 0;
if ( s->fProofLogging ) {
for ( i = 0; i < s->size; i++ )
if ( s->units[i] && !clause_is_used(s, s->units[i]) )
{
var_set_value(s, i, varX);
s->reasons[i] = 0;
s->units[i] = 0;
}
}
}
// reset implication queue
assert( (&s->trail_lim)->ptr[0] == s->simpdb_assigns );
assert( s->simpdb_assigns >= s->iSimpPivot );
assert( (&s->trail_lim)->ptr[0] >= s->iSimpPivot );
(&s->trail_lim)->ptr[0] = s->iSimpPivot;
s->simpdb_assigns = s->iSimpPivot;
solver2_canceluntil( s, 0 );
// reset problem clauses
if ( s->hClausePivot < veci_size(&s->clauses) )
{
satset* first = satset_read(&s->clauses, s->hClausePivot);
s->stats.clauses = first->Id;
s->stats.clauses = first->Id-1;
veci_resize(&s->clauses, s->hClausePivot);
}
// resetn learned clauses
if ( s->hLearntPivot < veci_size(&s->learnts) )
{
satset* first = satset_read(&s->learnts, s->hLearntPivot);
veci_resize(&s->claActs, first->Id+1);
veci_resize(&s->claActs, first->Id);
if ( s->fProofLogging ) {
veci_resize(&s->claProofs, first->Id+1);
veci_resize(&s->claProofs, first->Id);
Sat_ProofReduce( s );
}
s->stats.learnts = first->Id;
s->stats.learnts = first->Id-1;
veci_resize(&s->learnts, s->hLearntPivot);
}
// reset watcher lists
@ -1647,8 +1566,6 @@ void sat_solver2_rollback( sat_solver2* s )
s->cla_inc = (1 << 11);
#endif
s->root_level = 0;
s->simpdb_assigns = 0;
s->simpdb_props = 0;
s->random_seed = 91648253;
s->progress_estimate = 0;
s->verbosity = 0;
@ -1664,9 +1581,12 @@ void sat_solver2_rollback( sat_solver2* s )
s->stats.learnts_literals = 0;
s->stats.tot_literals = 0;
// initialize clause pointers
s->hClausePivot = 1;
s->hLearntPivot = 1;
s->hLearntLast = -1; // the last learnt clause
s->hProofLast = -1; // the last proof ID
s->hClausePivot = 1; // the pivot among clauses
s->hLearntPivot = 1; // the pivot moang learned clauses
s->iVarPivot = 0; // the pivot among the variables
s->iSimpPivot = 0; // marker of unit-clauses
}
}
@ -1717,10 +1637,10 @@ void sat_solver2_verify( sat_solver2* s )
Counter++;
}
}
if ( Counter == 0 )
printf( "Verification passed.\n" );
else
if ( Counter != 0 )
printf( "Verification failed!\n" );
// else
// printf( "Verification passed.\n" );
}
@ -1734,6 +1654,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
lit * i;
s->hLearntLast = -1;
s->hProofLast = -1;
// set the external limits
// s->nCalls++;
@ -1750,27 +1671,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
s->nInsLimit = nInsLimitGlobal;
#ifndef SAT_USE_ANALYZE_FINAL
//printf("solve: "); printlits(begin, end); printf("\n");
for (i = begin; i < end; i++){
switch (var_value(s, *i)) {
case var1: // l_True:
break;
case varX: // l_Undef
solver2_assume(s, *i);
if (solver2_propagate(s) == NULL)
break;
// fallthrough
case var0: // l_False
solver2_canceluntil(s, 0);
return l_False;
}
}
s->root_level = solver2_dlevel(s);
#endif
/*
// Perform assumptions:
root_level = assumps.size();
@ -1803,7 +1703,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
assert(root_level == decisionLevel());
*/
#ifdef SAT_USE_ANALYZE_FINAL
// Perform assumptions:
s->root_level = end - begin;
for ( i = begin; i < end; i++ )
@ -1822,6 +1721,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
}
else
{
assert( 0 );
proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions)
veci_resize(&s->conf_final,0);
veci_push(&s->conf_final, lit_neg(p));
@ -1829,7 +1729,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
if (var_level(s, lit_var(p)) > 0)
veci_push(&s->conf_final, p);
}
solver2_record(s, &s->conf_final, proof_id, 1);
// solver2_record(s, &s->conf_final, proof_id, 1);
s->hProofLast = proof_id;
solver2_canceluntil(s, 0);
return l_False;
}
@ -1839,14 +1740,14 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
if (confl != NULL){
proof_id = solver2_analyze_final(s, confl, 0);
assert(s->conf_final.size > 0);
// solver2_record(s,&s->conf_final, proof_id, 1);
s->hProofLast = proof_id;
solver2_canceluntil(s, 0);
solver2_record(s,&s->conf_final, proof_id, 1);
return l_False;
}
}
}
assert(s->root_level == solver2_dlevel(s));
#endif
if (s->verbosity >= 1){
printf("==================================[MINISAT]===================================\n");
@ -1891,6 +1792,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
printf("==============================================================================\n");
solver2_canceluntil(s,0);
assert( s->qhead == s->qtail );
// if ( status == l_True )
// sat_solver2_verify( s );
return status;

8
src/sat/bsat/satSolver2.h
View File

@ -85,8 +85,6 @@ struct sat_solver2_t
int qtail; // Tail index of queue.
int root_level; // Level of first proper decision.
int simpdb_assigns; // Number of top-level assignments at last 'simplifyDB()'.
int simpdb_props; // Number of propagations before next 'simplifyDB()'.
double random_seed;
double progress_estimate;
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything // activities
@ -111,9 +109,10 @@ struct sat_solver2_t
veci clauses; // clause memory
veci learnts; // learnt memory
veci* wlists; // watcher lists (for each literal)
int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
int hClausePivot; // the pivot among problem clause
int hLearntPivot; // the pivot among learned clause
int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
int iVarPivot; // the pivot among the variables
int iSimpPivot; // marker of unit-clauses
@ -247,10 +246,11 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
static inline void sat_solver2_bookmark(sat_solver2* s)
{
assert( s->qhead == s->qtail );
s->hLearntPivot = veci_size(&s->learnts);
s->hClausePivot = veci_size(&s->clauses);
s->iVarPivot = s->size;
s->iSimpPivot = s->simpdb_assigns;
s->iSimpPivot = s->qhead;
}
static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark )