From 735a831e13684334d55b422993a80d94d356f180 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 22 Jun 2012 10:30:22 -0700 Subject: Added memory reporting to &vta. --- src/aig/gia/giaAbsVta.c | 35 +++++++++++++++++++++++++------ src/aig/gia/giaCof.c | 2 +- src/aig/gia/giaGlitch.c | 2 +- src/aig/gia/giaSat.c | 4 ++-- src/aig/saig/saigBmc3.c | 20 +++++++++--------- src/misc/util/abc_global.h | 14 +++++++------ src/misc/vec/vecBit.h | 16 ++++++++++++++ src/misc/vec/vecFlt.h | 16 ++++++++++++++ src/misc/vec/vecPtr.h | 16 ++++++++++++++ src/misc/vec/vecSet.h | 4 ++-- src/misc/vec/vecStr.h | 16 ++++++++++++++ src/misc/vec/vecVec.h | 47 +++++++++++++++++++++++++++++++++++++++++ src/misc/vec/vecWrd.h | 16 ++++++++++++++ src/sat/bsat/satSolver.c | 5 +++-- src/sat/bsat/satSolver.h | 2 +- src/sat/bsat/satSolver2.c | 52 +++++++++++++++++++++++++++++++++++++++++++++- src/sat/bsat/satSolver2.h | 2 ++ 17 files changed, 237 insertions(+), 32 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 6bc5bd4f..d4ff109f 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -983,7 +983,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) p->pGia = pGia; p->pPars = pPars; // internal data - p->nObjsAlloc = (1 << 20); + p->nObjsAlloc = (1 << 18); p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc ); p->nObjs = 1; p->nBins = Abc_PrimeCudd( 2*p->nObjsAlloc ); @@ -1656,11 +1656,34 @@ finish: 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 ); + ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk ); + ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk ); + ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); + ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); + ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); + + + { // memory report + double memTot = 0; + double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t); + double memSat = sat_solver2_memory( p->pSat ); + double memPro = sat_solver2_memory_proof( p->pSat ); + double memMap = p->nObjsAlloc * sizeof(Vta_Obj_t) + p->nBins * sizeof(int); + double memOth = sizeof(Vta_Man_t); + 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; + 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 ); + } Vga_ManStop( p ); fflush( stdout ); diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c index 49142683..cf8ecf00 100644 --- a/src/aig/gia/giaCof.c +++ b/src/aig/gia/giaCof.c @@ -682,7 +682,7 @@ void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ) Gia_ManHashStart( pGia ); Cof_ManPrintHighFanout( p, nNodes ); Gia_ManHashStop( pGia ); -ABC_PRM( "Memory for logic network", 4*p->nObjData ); +ABC_PRMn( "Memory for logic network", 4*p->nObjData ); ABC_PRT( "Time", clock() - clk ); Cof_ManStop( p ); } diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c index 0dfee293..fc4d2736 100644 --- a/src/aig/gia/giaGlitch.c +++ b/src/aig/gia/giaGlitch.c @@ -772,7 +772,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb if ( fVerbose ) { printf( "\nSimulated %d patterns. ", nPatterns ); - ABC_PRM( "Memory", 4*p->nObjData ); + ABC_PRMn( "Memory", 4*p->nObjData ); ABC_PRT( "Time", clock() - clk ); } } diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c index cb410dd7..138eedd5 100644 --- a/src/aig/gia/giaSat.c +++ b/src/aig/gia/giaSat.c @@ -411,8 +411,8 @@ void Gia_ManSatExperiment( Gia_Man_t * p ) Gia_ManSatStop( pMan ); for ( i = 0; i < 2*GIA_LIMIT+2; i++ ) printf( "%2d=%6d %7.2f %% %7.2f %%\n", i, nCount[i], 100.0*nCount[i]/nCountAll, 100.0*i*nCount[i]/Gia_ManAndNum(p) ); - ABC_PRM( "MemoryEst", 4*nWords ); - ABC_PRM( "MemoryReal", 4*nWords2 ); + ABC_PRMn( "MemoryEst", 4*nWords ); + ABC_PRMn( "MemoryReal", 4*nWords2 ); printf( "%5.2f bpn ", 4.0*nWords2/Gia_ManObjNum(p) ); ABC_PRT( "Time", clock() - clk ); } diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index a67f84f3..cf19947a 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1248,11 +1248,11 @@ clkOther += clock() - clk2; printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts ); printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // ABC_PRT( "Time", clock() - clk ); - printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); - printf( "%4.0f Mb", 1+(float)sat_solver_memory(p->pSat)/(1<<20) ); + printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%5.0f Mb", 1.0+sat_solver_memory(p->pSat)/(1<<20) ); printf( "\n" ); -// ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 ); -// ABC_PRM( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); +// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); +// ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); // printf( "Simples = %6d. ", p->nBufNum ); // printf( "Dups = %6d. ", p->nDupNum ); // printf( "\n" ); @@ -1310,11 +1310,11 @@ clkOther += clock() - clk2; printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // ABC_PRT( "Time", clock() - clk ); - printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); - printf( "%4.0f Mb", 1+(float)sat_solver_memory(p->pSat)/(1<<20) ); + printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%5.0f Mb", 1.0+sat_solver_memory(p->pSat)/(1<<20) ); printf( "\n" ); -// ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 ); -// ABC_PRM( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); +// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); +// ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); // printf( "Simples = %6d. ", p->nBufNum ); // printf( "Dups = %6d. ", p->nDupNum ); // printf( "\n" ); @@ -1329,8 +1329,8 @@ clkOther += clock() - clk2; //ABC_PRT( "CNF generation runtime", clkOther ); if ( pPars->fVerbose ) { -// ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 ); -// ABC_PRM( "SAT", 48 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); +// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); +// ABC_PRMn( "SAT", 48 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); // printf( "Simples = %6d. ", p->nBufNum ); // printf( "Dups = %6d. ", p->nDupNum ); // printf( "\n" ); diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 5f0e1232..9524c505 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -205,12 +205,14 @@ typedef ABC_UINT64_T word; #define ABC_SWAP(Type, a, b) { Type t = a; a = b; b = t; } -#define ABC_PRT(a,t) (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))) -#define ABC_PRTr(a,t) (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%7.2f sec\r", (float)(t)/(float)(CLOCKS_PER_SEC))) -#define ABC_PRTn(a,t) (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC))) -#define ABC_PRTP(a,t,T) (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)) -#define ABC_PRM(a,f) (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%7.3f Mb ", 1.0*(f)/(1<<20))) -#define ABC_PRMP(a,f,F) (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%7.3f Mb (%6.2f %%) ", (1.0*(f)/(1<<20)), ((F)? 100.0*(f)/(F) : 0.0) ) ) +#define ABC_PRT(a,t) (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%9.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))) +#define ABC_PRTr(a,t) (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%9.2f sec\r", (float)(t)/(float)(CLOCKS_PER_SEC))) +#define ABC_PRTn(a,t) (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%9.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC))) +#define ABC_PRTP(a,t,T) (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%9.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)) +#define ABC_PRM(a,f) (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%10.3f Mb\n", 1.0*(f)/(1<<20))) +#define ABC_PRMr(a,f) (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%10.3f Mb\r", 1.0*(f)/(1<<20))) +#define ABC_PRMn(a,f) (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%10.3f Mb ", 1.0*(f)/(1<<20))) +#define ABC_PRMP(a,f,F) (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%10.3f Mb (%6.2f %%)\n", (1.0*(f)/(1<<20)), ((F)? 100.0*(f)/(F) : 0.0) ) ) #define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) #define ABC_CALLOC(type, num) ((type *) calloc((num), sizeof(type))) diff --git a/src/misc/vec/vecBit.h b/src/misc/vec/vecBit.h index 7f0d7409..4024d0ee 100644 --- a/src/misc/vec/vecBit.h +++ b/src/misc/vec/vecBit.h @@ -241,6 +241,22 @@ static inline int Vec_BitSize( Vec_Bit_t * p ) return p->nSize; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_BitCap( Vec_Bit_t * p ) +{ + return p->nCap; +} + /**Function************************************************************* Synopsis [] diff --git a/src/misc/vec/vecFlt.h b/src/misc/vec/vecFlt.h index 0ad6da27..19423ae0 100644 --- a/src/misc/vec/vecFlt.h +++ b/src/misc/vec/vecFlt.h @@ -284,6 +284,22 @@ static inline int Vec_FltSize( Vec_Flt_t * p ) return p->nSize; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_FltCap( Vec_Flt_t * p ) +{ + return p->nCap; +} + /**Function************************************************************* Synopsis [] diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index afad09d1..1d60ec50 100644 --- a/src/misc/vec/vecPtr.h +++ b/src/misc/vec/vecPtr.h @@ -287,6 +287,22 @@ static inline int Vec_PtrSize( Vec_Ptr_t * p ) return p->nSize; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_PtrCap( Vec_Ptr_t * p ) +{ + return p->nCap; +} + /**Function************************************************************* Synopsis [] diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h index df2a9a68..72358ea1 100644 --- a/src/misc/vec/vecSet.h +++ b/src/misc/vec/vecSet.h @@ -189,9 +189,9 @@ static inline void Vec_SetFree( Vec_Set_t * p ) SeeAlso [] ***********************************************************************/ -static inline int Vec_ReportMemory( Vec_Set_t * p ) +static inline double Vec_ReportMemory( Vec_Set_t * p ) { - int Mem = sizeof(Vec_Set_t); + double Mem = sizeof(Vec_Set_t); Mem += p->nPagesAlloc * sizeof(void *); Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage); return Mem; diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h index c794dc2f..cefa0ea9 100644 --- a/src/misc/vec/vecStr.h +++ b/src/misc/vec/vecStr.h @@ -278,6 +278,22 @@ static inline int Vec_StrSize( Vec_Str_t * p ) return p->nSize; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_StrCap( Vec_Str_t * p ) +{ + return p->nCap; +} + /**Function************************************************************* Synopsis [] diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index 8bed4574..6d309dc4 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -236,6 +236,22 @@ static inline int Vec_VecSize( Vec_Vec_t * p ) return p->nSize; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_VecCap( Vec_Vec_t * p ) +{ + return p->nCap; +} + /**Function************************************************************* Synopsis [] @@ -673,6 +689,37 @@ static inline void Vec_VecPrintInt( Vec_Vec_t * p, int fSkipSingles ) } } +/**Function************************************************************* + + Synopsis [Returns memory, in bytes, used by the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline double Vec_VecMemory( Vec_Vec_t * p ) +{ + int i; + Vec_Ptr_t * vVec; + double Mem = sizeof(Vec_Vec_t); + Mem += Vec_VecCap(p) * sizeof(void *); + Vec_VecForEachLevel( p, vVec, i ) + Mem += sizeof(Vec_Ptr_t) + Vec_PtrCap(vVec) * sizeof(void *); + return Mem; +} +static inline double Vec_VecMemoryInt( Vec_Vec_t * p ) +{ + int i; + Vec_Int_t * vVec; + double Mem = sizeof(Vec_Vec_t); + Mem += Vec_VecCap(p) * sizeof(void *); + Vec_VecForEachLevelInt( p, vVec, i ) + Mem += sizeof(Vec_Int_t) + Vec_IntCap(vVec) * sizeof(int); + return Mem; +} ABC_NAMESPACE_HEADER_END diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h index 11414ff7..97296401 100644 --- a/src/misc/vec/vecWrd.h +++ b/src/misc/vec/vecWrd.h @@ -334,6 +334,22 @@ static inline int Vec_WrdSize( Vec_Wrd_t * p ) return p->nSize; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_WrdCap( Vec_Wrd_t * p ) +{ + return p->nCap; +} + /**Function************************************************************* Synopsis [] diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index c48d277e..2d41e2fe 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1118,9 +1118,10 @@ void sat_solver_rollback( sat_solver* s ) } // returns memory in bytes used by the SAT solver -int sat_solver_memory( sat_solver* s ) +double sat_solver_memory( sat_solver* s ) { - int i, Mem = sizeof(sat_solver); + int i; + double Mem = sizeof(sat_solver); for (i = 0; i < s->cap*2; i++) Mem += s->wlists[i].cap * sizeof(int); Mem += s->cap * sizeof(veci); // ABC_FREE(s->wlists ); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 42473a6e..40f637ee 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -52,7 +52,7 @@ extern void sat_solver_rollback( sat_solver* s ); extern int sat_solver_nvars(sat_solver* s); extern int sat_solver_nclauses(sat_solver* s); extern int sat_solver_nconflicts(sat_solver* s); -extern int sat_solver_memory(sat_solver* s); +extern double sat_solver_memory(sat_solver* s); extern void sat_solver_setnvars(sat_solver* s,int n); extern int sat_solver_get_var_value(sat_solver* s, int v); diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index f014b6fc..2e0a5f4a 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1250,7 +1250,7 @@ void sat_solver2_delete(sat_solver2* s) } // report statistics - Abc_Print(1, "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 1.0 * Vec_SetMemory(&s->Proofs) / (1<<20), s->nUnits ); +// Abc_Print(1, "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 1.0 * Vec_ReportMemory(&s->Proofs) / (1<<20), s->nUnits ); // delete vectors veci_delete(&s->order); @@ -1618,6 +1618,56 @@ void sat_solver2_rollback( sat_solver2* s ) } } +// returns memory in bytes used by the SAT solver +double sat_solver2_memory( sat_solver2* s ) +{ + int i; + double Mem = sizeof(sat_solver2); + for (i = 0; i < s->cap*2; i++) + Mem += s->wlists[i].cap * sizeof(int); + Mem += s->cap * sizeof(veci); // ABC_FREE(s->wlists ); + Mem += s->clauses.cap * sizeof(int); + Mem += s->learnts.cap * sizeof(int); + Mem += s->claActs.cap * sizeof(int); + Mem += s->claProofs.cap * sizeof(int); +// Mem += s->cap * sizeof(char); // ABC_FREE(s->polarity ); +// Mem += s->cap * sizeof(char); // ABC_FREE(s->tags ); + Mem += s->cap * sizeof(varinfo2); // ABC_FREE(s->vi ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->levels ); + Mem += s->cap * sizeof(char); // ABC_FREE(s->assigns ); +#ifdef USE_FLOAT_ACTIVITY + Mem += s->cap * sizeof(double); // ABC_FREE(s->activity ); +#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 ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->units ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->model ); + + Mem += s->tagged.cap * sizeof(int); + Mem += s->stack.cap * sizeof(int); + Mem += s->order.cap * sizeof(int); + Mem += s->trail_lim.cap * sizeof(int); + Mem += s->temp_clause.cap * sizeof(int); + Mem += s->conf_final.cap * sizeof(int); + Mem += s->mark_levels.cap * sizeof(int); + Mem += s->min_lit_order.cap * sizeof(int); + Mem += s->min_step_order.cap * sizeof(int); + Mem += s->learnt_live.cap * sizeof(int); + Mem += s->temp_proof.cap * sizeof(int); +// Mem += Vec_ReportMemory( &s->Mem ); + return Mem; +} +double sat_solver2_memory_proof( sat_solver2* s ) +{ + return Vec_ReportMemory( &s->Proofs ); +} + + // find the clause in the watcher lists int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose ) { diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 07a03c9f..79eb64ed 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -49,6 +49,8 @@ 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); extern void sat_solver2_reducedb(sat_solver2* s); +extern double sat_solver2_memory( sat_solver2* s ); +extern double sat_solver2_memory_proof( sat_solver2* s ); extern void sat_solver2_setnvars(sat_solver2* s,int n); -- cgit v1.2.3