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

Reducing memory usage in proof-based abstraction.

This commit is contained in:
Alan Mishchenko 2012-07-29 22:31:00 -07:00
parent 5838789ee7
commit 8982bf58cb
7 changed files with 524 additions and 85 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

107
src/aig/gia/giaAbsGla.c
View File

@ -74,6 +74,9 @@ struct Gla_Man_t_
unsigned * pObj2Obj; // mapping of GIA obj into GLA obj
int nObjs; // the number of objects
int nAbsOld; // previous abstraction
int nAbsNew; // previous abstraction
int nLrnOld; // the number of bytes
int nLrnNew; // the number of bytes
// other data
int nCexes; // the number of counter-examples
int nObjAdded; // total number of objects added
@ -84,6 +87,8 @@ struct Gla_Man_t_
Vec_Int_t * vAddedNew; // temporary array
Vec_Int_t * vObjCounts; // object counters
Vec_Int_t * vCoreCounts; // counts how many times each object appears in the core
Vec_Int_t * vProofIds; // counts how many times each object appears in the core
int nProofIds; // proof ID counter
// refinement
Vec_Int_t * pvRefis; // vectors of each object
// refinement manager
@ -1056,6 +1061,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
assert( pGia0->vGateClasses != 0 );
p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
p->vCoreCounts = Vec_IntStart( Gia_ManObjNum(p->pGia) );
p->vProofIds = Vec_IntAlloc(0);
// update p->pCnf->vMapping, p->pCnf->pObj2Count, p->pCnf->pObj2Clause
// (here are not updating p->pCnf->pVarNums because it is not needed)
vMappingNew = Vec_IntStart( Gia_ManObjNum(p->pGia) );
@ -1318,6 +1324,7 @@ void Gla_ManStop( Gla_Man_t * p )
Vec_IntFreeP( &p->vObjCounts );
Vec_IntFreeP( &p->vAddedNew );
Vec_IntFreeP( &p->vCoreCounts );
Vec_IntFreeP( &p->vProofIds );
Vec_IntFreeP( &p->vTemp );
Vec_IntFreeP( &p->vAbs );
ABC_FREE( p->pvRefis );
@ -1567,15 +1574,29 @@ void Gia_GlaAddToCounters( Gla_Man_t * p, Vec_Int_t * vCore )
void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
{
Gla_Obj_t * pGla;
int i;
int i, Counter = 0;
Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i )
{
assert( !fCheck || pGla->fAbs == 0 );
if ( fCheck )
{
assert( pGla->fAbs == 0 );
if ( p->pSat->pPrf2 )
Vec_IntWriteEntry( p->vProofIds, Gla_ObjId(p, pGla), p->nProofIds++ );
}
if ( pGla->fAbs )
continue;
if ( !fCheck )
{
Counter++;
// printf( "%d ", Gla_ObjId(p, pGla) );
}
pGla->fAbs = 1;
Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
}
// if ( Counter )
// printf( " Total = %d\n", Counter );
}
void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f )
{
@ -1635,7 +1656,7 @@ int Gla_ManGetOutLit( Gla_Man_t * p, int f )
}
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;
Vec_Int_t * vCore = NULL;
int nConfPrev = pSat->stats.conflicts;
int RetValue, iLit = Gla_ManGetOutLit( p, f );
clock_t clk = clock();
@ -1675,6 +1696,8 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nCon
// derive the UNSAT core
clk = clock();
vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
if ( vCore )
Vec_IntSort( vCore, 1 );
if ( fVerbose )
{
// Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
@ -1717,6 +1740,9 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
// Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 );
Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
// Abc_PrintInt( p->nAbsNew );
// Abc_PrintInt( p->nLrnNew );
// Abc_Print( 1, "%4.1f MB", 4.0 * p->nLrnNew * Abc_BitWordNum(p->nAbsNew) / (1<<20) );
Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" );
fflush( stdout );
}
@ -1740,13 +1766,13 @@ void Gla_ManReportMemory( Gla_Man_t * p )
memOth += Vec_IntCap(p->vTemp) * sizeof(int);
memOth += Vec_IntCap(p->vAbs) * sizeof(int);
memTot = memAig + memSat + memPro + memMap + memRef + memOth;
ABC_PRMP( "Memory: AIG ", memAig, memTot );
ABC_PRMP( "Memory: SAT ", memSat, memTot );
ABC_PRMP( "Memory: Proof ", memPro, memTot );
ABC_PRMP( "Memory: Map ", memMap, memTot );
ABC_PRMP( "Memory: Refine", memRef, memTot );
ABC_PRMP( "Memory: Other ", memOth, memTot );
ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
ABC_PRMP( "Memory: AIG ", memAig, memTot );
ABC_PRMP( "Memory: SAT ", memSat, memTot );
ABC_PRMP( "Memory: Proof ", memPro, memTot );
ABC_PRMP( "Memory: Map ", memMap, memTot );
ABC_PRMP( "Memory: Refine ", memRef, memTot );
ABC_PRMP( "Memory: Other ", memOth, memTot );
ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
}
@ -1830,7 +1856,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
{
extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
Gla_Man_t * p;
Vec_Int_t * vCore, * vPPis;
Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL;
Abc_Cex_t * pCex = NULL;
int f, i, iPrev, nConfls, Status, nVarsOld, nCoreSize, fOneIsSent = 0, RetValue = -1;
clock_t clk2, clk = clock();
@ -1913,24 +1939,31 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
Vec_IntClear( p->vAddedNew );
p->nAbsOld = Vec_IntSize( p->vAbs );
nVarsOld = p->nSatVars;
p->nLrnOld = sat_solver2_nlearnts( p->pSat );
// iterate as long as there are counter-examples
p->nAbsNew = 0;
p->nLrnNew = 0;
for ( i = 0; ; i++ )
{
clk2 = clock();
vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
assert( (vCore != NULL) == (Status == 1) );
// assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 || (p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached
{
if ( p->pSat->pPrf2 )
Prf_ManStopP( &p->pSat->pPrf2 );
if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstration
Gla_ManRollBack( p );
goto finish;
}
if ( vCore != NULL )
if ( Status == 1 )
{
if ( p->pSat->pPrf2 )
Prf_ManStopP( &p->pSat->pPrf2 );
p->timeUnsat += clock() - clk2;
break;
}
}
p->timeSat += clock() - clk2;
assert( Status == 0 );
p->nCexes++;
@ -1954,17 +1987,37 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
vPPis = Gla_ManRefinement( p );
if ( vPPis == NULL )
{
if ( p->pSat->pPrf2 )
Prf_ManStopP( &p->pSat->pPrf2 );
pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
break;
}
}
assert( pCex == NULL );
// start proof logging
if ( i == 0 )
{
assert( p->pSat->pPrf2 == NULL );
p->pSat->pPrf2 = Prf_ManAlloc();
if ( p->pSat->pPrf2 )
{
p->nProofIds = 0;
Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
}
}
else
{
// resize the proof logger
if ( p->pSat->pPrf2 )
Prf_ManGrow( p->pSat->pPrf2, Vec_IntSize(p->vAbs) - p->nAbsOld + Vec_IntSize(vPPis) );
}
Gia_GlaAddToAbs( p, vPPis, 1 );
Gia_GlaAddOneSlice( p, f, vPPis );
Vec_IntFree( vPPis );
p->timeCex += clock() - clk2;
if ( pCex != NULL )
goto finish;
// print the result (do not count it towards change)
if ( p->pPars->fVerbose )
Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
@ -1972,24 +2025,30 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
if ( pCex != NULL )
break;
assert( Status == 1 );
// valid core is obtained
nCoreSize = Vec_IntSize( vCore );
Gia_GlaAddToCounters( p, vCore );
nCoreSize = 1;
if ( vCore )
{
nCoreSize += Vec_IntSize( vCore );
Gia_GlaAddToCounters( p, vCore );
}
if ( i == 0 )
{
p->pPars->nFramesNoChange++;
Vec_IntFree( vCore );
Vec_IntFreeP( &vCore );
}
else
{
p->pPars->nFramesNoChange = 0;
p->nAbsNew = Vec_IntSize( p->vAbs ) - p->nAbsOld;
p->nLrnNew = Abc_AbsInt( sat_solver2_nlearnts( p->pSat ) - p->nLrnOld );
// update the SAT solver
sat_solver2_rollback( p->pSat );
// update storage
Gla_ManRollBack( p );
p->nSatVars = nVarsOld;
// load this timeframe
Vec_IntSort( vCore, 1 );
Gia_GlaAddToAbs( p, vCore, 0 );
Gia_GlaAddOneSlice( p, f, vCore );
Vec_IntFree( vCore );
@ -1997,7 +2056,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
clk2 = clock();
vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
p->timeUnsat += clock() - clk2;
assert( (vCore != NULL) == (Status == 1) );
// assert( (vCore != NULL) == (Status == 1) );
Vec_IntFreeP( &vCore );
if ( Status == -1 ) // resource limit is reached
break;
@ -2046,10 +2105,10 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
}
finish:
// analize the results
if ( p->pPars->fVerbose )
printf( "\n" );
if ( pCex == NULL )
{
if ( p->pPars->fVerbose && Status == -1 )
printf( "\n" );
if ( pAig->vGateClasses != NULL )
Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
Vec_IntFreeP( &pAig->vGateClasses );

60
src/aig/gia/giaAbsGla2.c
View File

@ -41,21 +41,22 @@ struct Ga2_Man_t_
Gia_Man_t * pGia; // working AIG manager
Gia_ParVta_t * pPars; // parameters
// markings
int nMarked; // total number of marked nodes and flops
Vec_Ptr_t * vCnfs; // for each object: CNF0, CNF1
// abstraction
Vec_Int_t * vIds; // abstraction ID for each object
Vec_Int_t * vIds; // abstraction ID for each GIA object
Vec_Int_t * vAbs; // array of abstracted objects
Vec_Int_t * vValues; // array of objects with SAT numbers assigned
Vec_Int_t * vValues; // array of objects with abstraction ID assigned
Vec_Int_t * vProofIds; // proof IDs for these objects (1-to-1 with vValues)
int nProofIds; // the counter of proof IDs
int LimAbs; // limit value for starting abstraction objects
int LimPpi; // limit value for starting PPI objects
int nMarked; // total number of marked nodes and flops
// refinement
Rnm_Man_t * pRnm; // refinement manager
// SAT solver and variables
Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal
sat_solver2 * pSat; // incremental SAT solver
int nSatVars; // the number of SAT variables
int nProofIds; // the counter of proof IDs
// temporaries
Vec_Int_t * vLits;
Vec_Int_t * vIsopMem;
@ -356,7 +357,9 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vIds = Vec_IntStart( Gia_ManObjNum(pGia) );
p->vAbs = Vec_IntAlloc( 1000 );
p->vValues = Vec_IntAlloc( 1000 );
p->vProofIds = Vec_IntAlloc( 1000 );
Vec_IntPush( p->vValues, -1 );
Vec_IntPush( p->vProofIds, -1 );
// refinement
p->pRnm = Rnm_ManStart( pGia );
// SAT solver and variables
@ -380,17 +383,18 @@ void Ga2_ManReportMemory( Ga2_Man_t * p )
memOth += Vec_IntMemory( p->vIds );
memOth += Vec_IntMemory( p->vAbs );
memOth += Vec_IntMemory( p->vValues );
memOth += Vec_IntMemory( p->vProofIds );
memOth += Vec_IntMemory( p->vLits );
memOth += Vec_IntMemory( p->vIsopMem );
memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536;
memTot = memAig + memSat + memPro + memMap + memRef + memOth;
ABC_PRMP( "Memory: AIG ", memAig, memTot );
ABC_PRMP( "Memory: SAT ", memSat, memTot );
ABC_PRMP( "Memory: Proof ", memPro, memTot );
ABC_PRMP( "Memory: Map ", memMap, memTot );
ABC_PRMP( "Memory: Refine", memRef, memTot );
ABC_PRMP( "Memory: Other ", memOth, memTot );
ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
ABC_PRMP( "Memory: AIG ", memAig, memTot );
ABC_PRMP( "Memory: SAT ", memSat, memTot );
ABC_PRMP( "Memory: Proof ", memPro, memTot );
ABC_PRMP( "Memory: Map ", memMap, memTot );
ABC_PRMP( "Memory: Refine ", memRef, memTot );
ABC_PRMP( "Memory: Other ", memOth, memTot );
ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
}
void Ga2_ManStop( Ga2_Man_t * p )
{
@ -404,6 +408,7 @@ void Ga2_ManStop( Ga2_Man_t * p )
Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
Vec_IntFree( p->vIds );
Vec_IntFree( p->vAbs );
Vec_IntFree( p->vProofIds );
Vec_IntFree( p->vValues );
Vec_IntFree( p->vLits );
Vec_IntFree( p->vIsopMem );
@ -610,17 +615,19 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In
SeeAlso []
***********************************************************************/
void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs, int ProofId )
{
unsigned uTruth;
int nLeaves;
assert( pObj->fPhase );
assert( Vec_PtrSize(p->vCnfs) == 2 * Vec_IntSize(p->vValues) );
assert( Vec_IntSize(p->vProofIds) == Vec_IntSize(p->vValues) );
// assign abstraction ID to the node
if ( Ga2_ObjId(p,pObj) == 0 )
{
Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) );
Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) );
Vec_IntPush( p->vProofIds, ProofId );
Vec_PtrPush( p->vCnfs, NULL );
Vec_PtrPush( p->vCnfs, NULL );
}
@ -629,14 +636,14 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
return;
// compute parameters
nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj);
uTruth = Ga2_ObjTruth( p->pGia, pObj );
// create CNF for pos/neg phases
uTruth = Ga2_ObjTruth( p->pGia, pObj );
Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) );
uTruth = (~uTruth) & Abc_InfoMask( (1 << nLeaves) );
Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) );
}
void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId )
{
Vec_Int_t * vLeaves, * vMap;
Gia_Obj_t * pObj, * pFanin;
@ -644,15 +651,16 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
// add abstraction objects
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
{
Ga2_ManSetupNode( p, pObj, 1 );
Ga2_ManSetupNode( p, pObj, 1, ProofId );
Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) );
Vec_IntPush( p->vProofIds, ProofId );
}
// add PPI objects
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
{
vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
Ga2_ManSetupNode( p, pObj, 0 );
Ga2_ManSetupNode( p, pObj, 0, -1 );
}
// clean mapping in the timeframes
Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
@ -666,8 +674,12 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
Vec_IntClear( p->vLits );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) );
Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, p->nProofIds + i );
Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Vec_IntEntry(p->vProofIds, Ga2_ObjId(p, pObj)) );
}
// verify -- if ProofId == -1, all proof IDs should be the same
if ( ProofId == -1 )
Vec_IntForEachEntry( p->vProofIds, k, i )
assert( k == -1 );
}
void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
@ -679,11 +691,11 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
{
if ( i < p->LimAbs )
continue;
iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f );
vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Vec_IntClear( p->vLits );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) );
iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f );
Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, i - p->LimAbs );
}
}
@ -717,6 +729,7 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues )
Ga2_ObjSetId( p, pObj, 0 );
}
Vec_IntShrink( p->vValues, nValues );
Vec_IntShrink( p->vProofIds, nValues );
Vec_PtrShrink( p->vCnfs, 2 * nValues );
// clean mapping into timeframes
Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
@ -775,6 +788,7 @@ void Ga2_ManRestart( Ga2_Man_t * p )
Vec_Int_t * vToAdd;
assert( p->pGia != NULL && p->pGia->vGateClasses != NULL );
assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set
p->nProofIds = 0;
// clear mappings from objects
Ga2_ManShrinkAbs( p, 0, 1 );
// clear SAT variable numbers (begin with 1)
@ -783,11 +797,10 @@ void Ga2_ManRestart( Ga2_Man_t * p )
p->nSatVars = 1;
// start abstraction
vToAdd = Ga2_ManAbsDerive( p->pGia );
Ga2_ManAddToAbs( p, vToAdd );
Ga2_ManAddToAbs( p, vToAdd, -1 );
Vec_IntFree( vToAdd );
p->LimAbs = Vec_IntSize(p->vAbs) + 1;
p->LimPpi = Vec_IntSize(p->vValues);
p->nProofIds = 0;
// set runtime limit
if ( p->pPars->nTimeOut )
sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart );
@ -1069,7 +1082,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
{
p->pPars->iFrame = f;
// add abstraction clauses
// add static clauses to this timeframe
Ga2_ManAddAbsClauses( p, f );
// get the output literal
Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f );
@ -1087,7 +1100,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
p->timeCex += clock() - clk;
if ( vPPis == NULL )
goto finish;
Ga2_ManAddToAbs( p, vPPis );
Ga2_ManAddToAbs( p, vPPis, p->nProofIds++ );
Vec_IntFree( vPPis );
// verify
if ( Vec_IntCheckUnique(p->vAbs) )
@ -1103,8 +1116,9 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// derive UNSAT core
vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
Ga2_ManShrinkAbs( p, nAbs, nValues );
Ga2_ManAddToAbs( p, vCore );
Ga2_ManAddToAbs( p, vCore, -1 );
Vec_IntFree( vCore );
p->nProofIds = 0;
// remember current limits
nAbs = Vec_IntSize(p->vAbs);
nValues = Vec_IntSize(p->vValues);

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

@ -1035,6 +1035,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
// other data
p->vCores = Vec_PtrAlloc( 100 );
p->pSat = sat_solver2_new();
p->pSat->pPrf1 = Vec_SetAlloc( 20 );
// p->pSat->fVerbose = p->pPars->fVerbose;
// sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
p->pSat->nLearntStart = p->pPars->nLearnedStart;
@ -1499,12 +1500,12 @@ void Gia_VtaPrintMemory( Vta_Man_t * p )
memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
memTot = memAig + memSat + memPro + memMap + memOth;
ABC_PRMP( "Memory: AIG ", memAig, memTot );
ABC_PRMP( "Memory: SAT ", memSat, memTot );
ABC_PRMP( "Memory: Proof", memPro, memTot );
ABC_PRMP( "Memory: Map ", memMap, memTot );
ABC_PRMP( "Memory: Other", memOth, memTot );
ABC_PRMP( "Memory: TOTAL", memTot, memTot );
ABC_PRMP( "Memory: AIG ", memAig, memTot );
ABC_PRMP( "Memory: SAT ", memSat, memTot );
ABC_PRMP( "Memory: Proof ", memPro, memTot );
ABC_PRMP( "Memory: Map ", memMap, memTot );
ABC_PRMP( "Memory: Other ", memOth, memTot );
ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
}
@ -1694,10 +1695,10 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
}
finish:
// analize the results
if ( p->pPars->fVerbose )
printf( "\n" );
if ( pCex == NULL )
{
if ( p->pPars->fVerbose && Status == -1 )
printf( "\n" );
if ( Vec_PtrSize(p->vCores) == 0 )
Abc_Print( 1, "Abstraction is not produced because first frame is not solved. " );
else

2
src/misc/vec/vecSet.h
View File

@ -168,12 +168,14 @@ static inline void Vec_SetRestart( Vec_Set_t * p )
static inline void Vec_SetFree_( Vec_Set_t * p )
{
int i;
if ( p == NULL ) return;
for ( i = 0; i < p->nPagesAlloc; i++ )
ABC_FREE( p->pPages[i] );
ABC_FREE( p->pPages );
}
static inline void Vec_SetFree( Vec_Set_t * p )
{
if ( p == NULL ) return;
Vec_SetFree_( p );
ABC_FREE( p );
}

326
src/sat/bsat/satProof2.h Normal file
View File

@ -0,0 +1,326 @@
/**CFile****************************************************************
FileName [satProof2.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver.]
Synopsis [Proof logging.]
Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 1, 2004.]
Revision [$Id: satProof2.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__sat__bsat__satProof2_h
#define ABC__sat__bsat__satProof2_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "misc/vec/vec.h"
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Prf_Man_t_ Prf_Man_t;
struct Prf_Man_t_
{
int iFirst; // first learned clause with proof
int iFirst2; // first learned clause with proof
int nWords; // the number of proof words
word * pInfo; // pointer to the current proof
Vec_Wrd_t * vInfo; // proof information
Vec_Int_t * vSaved; // IDs of saved clauses
Vec_Int_t * vId2Pr; // mapping proof IDs of problem clauses into bitshifts (user's array)
};
////////////////////////////////////////////////////////////////////////
/// GLOBAL VARIABLES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Prf_BitWordNum( int nWidth ) { return (nWidth >> 6) + ((nWidth & 63) > 0); }
static inline int Prf_ManSize( Prf_Man_t * p ) { return Vec_WrdSize( p->vInfo ) / p->nWords; }
static inline void Prf_ManClearNewInfo( Prf_Man_t * p ) { int w; for ( w = 0; w < p->nWords; w++ ) Vec_WrdPush( p->vInfo, 0 ); }
static inline word * Prf_ManClauseInfo( Prf_Man_t * p, int Id ) { return Vec_WrdEntryP( p->vInfo, Id * p->nWords ); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Prf_Man_t * Prf_ManAlloc()
{
Prf_Man_t * p;
p = ABC_CALLOC( Prf_Man_t, 1 );
p->iFirst = -1;
p->iFirst2 = -1;
p->vInfo = Vec_WrdAlloc( 1000 );
p->vSaved = Vec_IntAlloc( 1000 );
return p;
}
static inline void Prf_ManStop( Prf_Man_t * p )
{
if ( p == NULL )
return;
Vec_IntFree( p->vSaved );
Vec_WrdFree( p->vInfo );
ABC_FREE( p );
}
static inline void Prf_ManStopP( Prf_Man_t ** p )
{
Prf_ManStop( *p );
*p = NULL;
}
static inline double Prf_ManMemory( Prf_Man_t * p )
{
return Vec_WrdMemory(p->vInfo) + Vec_IntMemory(p->vSaved) + sizeof(Prf_Man_t);
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Prf_ManRestart( Prf_Man_t * p, Vec_Int_t * vId2Pr, int iFirst, int nWidth )
{
assert( p->iFirst == -1 );
p->iFirst = iFirst;
p->nWords = Prf_BitWordNum( nWidth );
p->vId2Pr = vId2Pr;
p->pInfo = NULL;
Vec_WrdClear( p->vInfo );
}
static inline void Prf_ManGrow( Prf_Man_t * p, int nWidth )
{
Vec_Wrd_t * vInfoNew;
int i, w, nSize, nWordsNew;
assert( p->iFirst >= 0 );
assert( p->pInfo == NULL );
if ( nWidth < 64 * p->nWords )
return;
// get word count after resizing
nWordsNew = Abc_MaxInt( Prf_BitWordNum(nWidth), 2 * p->nWords );
// remap the entries
nSize = Prf_ManSize( p );
vInfoNew = Vec_WrdAlloc( (nSize + 1000) * nWordsNew );
for ( i = 0; i < nSize; i++ )
{
p->pInfo = Prf_ManClauseInfo( p, i );
for ( w = 0; w < p->nWords; w++ )
Vec_WrdPush( vInfoNew, p->pInfo[w] );
for ( ; w < nWordsNew; w++ )
Vec_WrdPush( vInfoNew, 0 );
}
Vec_WrdFree( p->vInfo );
p->vInfo = vInfoNew;
p->nWords = nWordsNew;
p->pInfo = NULL;
}
static inline void Prf_ManShrink( Prf_Man_t * p, int iClause )
{
assert( p->iFirst >= 0 );
assert( iClause - p->iFirst >= 0 );
assert( iClause - p->iFirst < Prf_ManSize(p) );
Vec_WrdShrink( p->vInfo, (iClause - p->iFirst) * p->nWords );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Prf_ManAddSaved( Prf_Man_t * p, int i, int iNew )
{
assert( p->iFirst >= 0 );
if ( i < p->iFirst )
return;
if ( Vec_IntSize(p->vSaved) == 0 )
{
assert( p->iFirst2 == -1 );
p->iFirst2 = iNew;
}
Vec_IntPush( p->vSaved, i );
}
static inline void Prf_ManCompact( Prf_Man_t * p, int iNew )
{
int i, w, k = 0, Entry, nSize;
assert( p->iFirst >= 0 );
assert( p->pInfo == NULL );
nSize = Prf_ManSize( p );
Vec_IntForEachEntry( p->vSaved, Entry, i )
{
assert( Entry - p->iFirst >= 0 && Entry - p->iFirst < nSize );
p->pInfo = Prf_ManClauseInfo( p, Entry - p->iFirst );
for ( w = 0; w < p->nWords; w++ )
Vec_WrdWriteEntry( p->vInfo, k++, p->pInfo[w] );
}
Vec_WrdShrink( p->vInfo, k );
Vec_IntClear( p->vSaved );
p->pInfo = NULL;
// update first
if ( p->iFirst2 == -1 )
p->iFirst = iNew;
else
p->iFirst = p->iFirst2;
p->iFirst2 = -1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Prf_ManChainResolve( Prf_Man_t * p, clause * c )
{
assert( p->iFirst >= 0 );
assert( p->pInfo != NULL );
// add to proof info
if ( c->lrn ) // learned clause
{
if ( clause_id(c) >= p->iFirst )
{
word * pProofStart;
int w;
assert( clause_id(c) - p->iFirst >= 0 );
assert( clause_id(c) - p->iFirst < Prf_ManSize(p) );
pProofStart = Prf_ManClauseInfo( p, clause_id(c) - p->iFirst );
for ( w = 0; w < p->nWords; w++ )
p->pInfo[w] |= pProofStart[w];
}
}
else // problem clause
{
if ( clause_id(c) ) // has proof ID
{
int Entry;
if ( p->vId2Pr == NULL )
Entry = clause_id(c);
else
Entry = Vec_IntEntry( p->vId2Pr, clause_id(c) );
if ( Entry >= 0 )
{
assert( Entry < 64 * p->nWords );
Abc_InfoSetBit( (unsigned *)p->pInfo, Entry );
}
}
}
}
static inline void Prf_ManChainStart( Prf_Man_t * p, clause * c )
{
assert( p->iFirst >= 0 );
// prepare info for new clause
Prf_ManClearNewInfo( p );
// get pointer to the proof
assert( p->pInfo == NULL );
p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
// add to proof info
Prf_ManChainResolve( p, c );
}
static inline int Prf_ManChainStop( Prf_Man_t * p )
{
assert( p->pInfo != NULL );
p->pInfo = NULL;
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Prf_ManUnsatCore( Prf_Man_t * p )
{
Vec_Int_t * vCore;
int i, Entry;
assert( p->iFirst >= 0 );
assert( p->pInfo == NULL );
vCore = Vec_IntAlloc( 64 * p->nWords );
p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
if ( p->vId2Pr == NULL )
{
for ( i = 0; i < 64 * p->nWords; i++ )
if ( Abc_InfoHasBit( (unsigned *)p->pInfo, i ) )
Vec_IntPush( vCore, i );
}
else
{
Vec_IntForEachEntry( p->vId2Pr, Entry, i )
{
if ( Entry < 0 )
continue;
assert( Entry < 64 * p->nWords );
if ( Abc_InfoHasBit( (unsigned *)p->pInfo, Entry ) )
Vec_IntPush( vCore, i );
}
}
p->pInfo = NULL;
Vec_IntSort( vCore, 1 );
return vCore;
}
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -161,7 +161,11 @@ static inline veci* solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l
static inline void proof_chain_start( sat_solver2* s, clause* c )
{
if ( s->fProofLogging )
if ( !s->fProofLogging )
return;
if ( s->pPrf2 )
Prf_ManChainStart( s->pPrf2, c );
if ( s->pPrf1 )
{
int ProofId = clause2_proofid(s, c, 0);
assert( (ProofId >> 2) > 0 );
@ -174,7 +178,14 @@ static inline void proof_chain_start( sat_solver2* s, clause* c )
static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
{
if ( s->fProofLogging )
if ( !s->fProofLogging )
return;
if ( s->pPrf2 )
{
clause* c = cls ? cls : var_unit_clause( s, Var );
Prf_ManChainResolve( s->pPrf2, c );
}
if ( s->pPrf1 )
{
clause* c = cls ? cls : var_unit_clause( s, Var );
int ProofId = clause2_proofid(s, c, var_is_partA(s,Var));
@ -185,11 +196,15 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
static inline int proof_chain_stop( sat_solver2* s )
{
if ( s->fProofLogging )
if ( !s->fProofLogging )
return 0;
if ( s->pPrf2 )
Prf_ManChainStop( s->pPrf2 );
if ( s->pPrf1 )
{
extern void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts );
int h = Vec_SetAppend( &s->Proofs, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
Proof_ClauseSetEnts( &s->Proofs, h, veci_size(&s->temp_proof) - 2 );
int h = Vec_SetAppend( s->pPrf1, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
Proof_ClauseSetEnts( s->pPrf1, h, veci_size(&s->temp_proof) - 2 );
return h;
}
return 0;
@ -371,7 +386,7 @@ static inline int sat_clause_compute_lbd( sat_solver2* s, clause* c )
return lbd;
}
static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id)
static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id )
{
clause* c;
int h, size = end - begin;
@ -385,11 +400,11 @@ static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt,
c = clause2_read( s, h );
if (learnt)
{
if ( s->fProofLogging )
if ( s->pPrf1 )
assert( proof_id );
c->lbd = sat_clause_compute_lbd( s, c );
assert( clause_id(c) == veci_size(&s->act_clas) );
if ( proof_id )
if ( s->pPrf1 )
veci_push(&s->claProofs, proof_id);
// veci_push(&s->act_clas, (1<<10));
veci_push(&s->act_clas, 0);
@ -674,7 +689,8 @@ static int solver2_lit_removable(sat_solver2* s, int x)
while (veci_size(&s->stack))
{
x = veci_pop(&s->stack);
if ( s->fProofLogging ){
if ( s->fProofLogging )
{
if ( x & 1 ){
if ( var_tag(s,x >> 1) & 1 )
veci_push(&s->min_lit_order, x >> 1 );
@ -910,7 +926,8 @@ clause* solver2_propagate(sat_solver2* s)
// Did not find watch -- clause is unit under assignment:
Lit = lits[0];
if (s->fProofLogging && solver2_dlevel(s) == 0){
if ( s->fProofLogging && solver2_dlevel(s) == 0 )
{
int k, x, proof_id, Cid, Var = lit_var(Lit);
int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit));
// Log production of top-level unit clause:
@ -990,7 +1007,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
s->stats.conflicts++; conflictC++;
if (solver2_dlevel(s) <= s->root_level){
proof_id = solver2_analyze_final(s, confl, 0);
assert( proof_id > 0 );
if ( s->pPrf1 )
assert( proof_id > 0 );
s->hProofLast = proof_id;
veci_delete(&learnt_clause);
return l_False;
@ -1112,12 +1130,11 @@ sat_solver2* sat_solver2_new(void)
veci_new(&s->min_lit_order);
veci_new(&s->min_step_order);
// veci_new(&s->learnt_live);
Sat_MemAlloc_( &s->Mem, 14 );
veci_new(&s->act_clas);
// proof-logging
veci_new(&s->claProofs);
if ( s->fProofLogging )
Vec_SetAlloc_( &s->Proofs, 20 );
// s->pPrf1 = Vec_SetAlloc( 20 );
// initialize clause pointers
s->hLearntLast = -1; // the last learnt clause
@ -1218,7 +1235,8 @@ void sat_solver2_delete(sat_solver2* s)
// veci_delete(&s->lrns);
Sat_MemFree_( &s->Mem );
// veci_delete(&s->proofs);
Vec_SetFree_( &s->Proofs );
Vec_SetFree( s->pPrf1 );
Prf_ManStop( s->pPrf2 );
// delete arrays
if (s->vi != 0){
@ -1424,7 +1442,7 @@ void sat_solver2_reducedb(sat_solver2* s)
// mark learned clauses to remove
Counter = j = 0;
pClaProofs = s->fProofLogging ? veci_begin(&s->claProofs) : NULL;
pClaProofs = veci_size(&s->claProofs) ? veci_begin(&s->claProofs) : NULL;
Sat_MemForEachLearned( pMem, c, i, k )
{
assert( c->mark == 0 );
@ -1432,7 +1450,9 @@ void sat_solver2_reducedb(sat_solver2* s)
{
pSortValues[j] = pSortValues[clause_id(c)];
if ( pClaProofs )
pClaProofs[j] = pClaProofs[clause_id(c)];
pClaProofs[j] = pClaProofs[clause_id(c)];
if ( s->pPrf2 )
Prf_ManAddSaved( s->pPrf2, clause_id(c), j );
j++;
}
else // delete
@ -1443,13 +1463,15 @@ void sat_solver2_reducedb(sat_solver2* s)
}
}
ABC_FREE( pSortValues );
if ( s->pPrf2 )
Prf_ManCompact( s->pPrf2, j );
// if ( j == nLearnedOld )
// return;
assert( s->stats.learnts == (unsigned)j );
assert( Counter == nLearnedOld );
veci_resize(&s->act_clas,j);
if ( s->fProofLogging )
if ( veci_size(&s->claProofs) )
veci_resize(&s->claProofs,j);
// update ID of each clause to be its new handle
@ -1508,8 +1530,8 @@ void sat_solver2_reducedb(sat_solver2* s)
assert( Counter == (int)s->stats.learnts );
// compact proof (compacts 'proofs' and update 'claProofs')
if ( s->fProofLogging )
s->hProofPivot = Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
if ( s->pPrf1 )
s->hProofPivot = Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
// report the results
@ -1531,7 +1553,7 @@ void sat_solver2_rollback( sat_solver2* s )
Count++;
assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(&s->Proofs) );
assert( s->pPrf1 == NULL || (s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(s->pPrf1)) );
// reset implication queue
solver2_canceluntil_rollback( s, s->iTrailPivot );
// update order
@ -1568,14 +1590,17 @@ void sat_solver2_rollback( sat_solver2* s )
// resize learned arrays
veci_resize(&s->act_clas, s->stats.learnts);
if ( s->fProofLogging )
if ( s->pPrf1 )
{
veci_resize(&s->claProofs, s->stats.learnts);
// Vec_SetShrink(&s->Proofs, s->hProofPivot);
// some weird bug here, which shows only on 64-bits!
// temporarily, perform more general proof reduction
Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
}
assert( s->pPrf2 == NULL );
// if ( s->pPrf2 )
// Prf_ManShrink( s->pPrf2, s->stats.learnts );
// initialize other vars
s->size = s->iVarPivot;
@ -1641,8 +1666,6 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
#else
Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );
#endif
// if ( s->factors )
// Mem += s->cap * sizeof(double); // ABC_FREE(s->factors );
Mem += s->cap * sizeof(lit); // ABC_FREE(s->trail );
Mem += s->cap * sizeof(int); // ABC_FREE(s->orderpos );
Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons );
@ -1659,12 +1682,15 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
Mem += s->min_step_order.cap * sizeof(int);
Mem += s->temp_proof.cap * sizeof(int);
Mem += Sat_MemMemoryAll( &s->Mem );
// Mem += Vec_ReportMemory( &s->Proofs );
// Mem += Vec_ReportMemory( s->pPrf1 );
return Mem;
}
double sat_solver2_memory_proof( sat_solver2* s )
{
return Vec_ReportMemory( &s->Proofs );
double Mem = s->dPrfMemory;
if ( s->pPrf1 )
Mem += Vec_ReportMemory( s->pPrf1 );
return Mem;
}
@ -1911,7 +1937,14 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
void * Sat_ProofCore( sat_solver2 * s )
{
extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot );
return Proof_DeriveCore( &s->Proofs, s->hProofLast );
if ( s->pPrf1 )
return Proof_DeriveCore( s->pPrf1, s->hProofLast );
if ( s->pPrf2 )
{
s->dPrfMemory = Abc_MaxDouble( s->dPrfMemory, Prf_ManMemory(s->pPrf2) );
return Prf_ManUnsatCore( s->pPrf2 );
}
return NULL;
}
ABC_NAMESPACE_IMPL_END

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

@ -31,6 +31,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "satVec.h"
#include "satClause.h"
#include "misc/vec/vecSet.h"
#include "satProof2.h"
ABC_NAMESPACE_HEADER_START
@ -147,10 +148,12 @@ struct sat_solver2_t
veci learnt_live; // remaining clauses after reduce DB
// proof logging
Vec_Set_t Proofs; // sequence of proof records
Vec_Set_t * pPrf1; // sequence of proof records
veci temp_proof; // temporary place to store proofs
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)
Prf_Man_t * pPrf2; // another proof manager
double dPrfMemory; // memory used by the proof-logger
// statistics
stats_t stats;
@ -234,7 +237,8 @@ static inline void sat_solver2_bookmark(sat_solver2* s)
assert( s->qhead == s->qtail );
s->iVarPivot = s->size;
s->iTrailPivot = s->qhead;
s->hProofPivot = Vec_SetHandCurrent(&s->Proofs);
if ( s->pPrf1 )
s->hProofPivot = Vec_SetHandCurrent(s->pPrf1);
Sat_MemBookMark( &s->Mem );
}