abc/src/sat/bsat/satSolver2.c
// returns memory in bytes used by the SAT solver
returns memory in bytes used by the SAT solver
returns memory in bytes used by the SAT solver
double sat_solver2_memory( sat_solver2* s, int fAll )
{
    int i;
    double Mem = sizeof(sat_solver2);
    if ( fAll )
        for (i = 0; i < s->cap*2; i++)
            Mem += s->wlists[i].cap * sizeof(int);
    Mem += s->cap * sizeof(veci);     
    Mem += s->act_clas.cap * sizeof(int);
    Mem += s->claProofs.cap * sizeof(int);
    Mem += s->cap * sizeof(varinfo2); 
    Mem += s->cap * sizeof(int);      
    Mem += s->cap * sizeof(char);     
#ifdef USE_FLOAT_ACTIVITY2
    Mem += s->cap * sizeof(double);   
#else
    Mem += s->cap * sizeof(unsigned); 
    if ( s->activity2 )
    Mem += s->cap * sizeof(unsigned); 
#endif
    Mem += s->cap * sizeof(lit);      
    Mem += s->cap * sizeof(int);      
    Mem += s->cap * sizeof(int);      
    Mem += s->cap * sizeof(int);      
    Mem += s->cap * sizeof(int);      
    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->temp_proof.cap * sizeof(int);
    Mem += Sat_MemMemoryAll( &s->Mem );
    return Mem;
}
double sat_solver2_memory ( sat_solver2 * s , int fAll ) { int i ; double Mem = sizeof ( sat_solver2 ) ; if ( fAll ) for ( i = 0 ; i < s -> cap * 2 ; i ++ ) Mem += s -> wlists [ i ] . cap * sizeof ( int ) ; Mem += s -> cap * sizeof ( veci ) ; Mem += s -> act_clas . cap * sizeof ( int ) ; Mem += s -> claProofs . cap * sizeof ( int ) ; Mem += s -> cap * sizeof ( varinfo2 ) ; Mem += s -> cap * sizeof ( int ) ; Mem += s -> cap * sizeof ( char ) ; #ifdef USE_FLOAT_ACTIVITY2 Mem += s -> cap * sizeof ( double ) ; #else Mem += s -> cap * sizeof ( unsigned ) ; if ( s -> activity2 ) Mem += s -> cap * sizeof ( unsigned ) ; #endif Mem += s -> cap * sizeof ( lit ) ; Mem += s -> cap * sizeof ( int ) ; Mem += s -> cap * sizeof ( int ) ; Mem += s -> cap * sizeof ( int ) ; Mem += s -> cap * sizeof ( int ) ; 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 -> temp_proof . cap * sizeof ( int ) ; Mem += Sat_MemMemoryAll ( & s -> Mem ) ; return Mem ; }
returns memory in bytes used by the SAT solver
returns memory in bytes used by the SAT solver
// ABC_FREE(s->wlists   ); //    Mem += s->cap * sizeof(char);     // ABC_FREE(s->polarity ); //    Mem += s->cap * sizeof(char);     // ABC_FREE(s->tags     ); // ABC_FREE(s->vi       ); // ABC_FREE(s->levels   ); // ABC_FREE(s->assigns  ); // ABC_FREE(s->activity ); // ABC_FREE(s->activity ); // ABC_FREE(s->activity2); // ABC_FREE(s->trail    ); // ABC_FREE(s->orderpos ); // ABC_FREE(s->reasons  ); // ABC_FREE(s->units    ); // ABC_FREE(s->model    ); //    Mem += Vec_ReportMemory( s->pPrf1 );