CVC3
|
#include <xchaff_dbase.h>
Public Attributes | |
int | mem_used_up_counts |
bool | mem_used_up |
int | init_num_clauses |
int | init_num_literals |
int | num_added_clauses |
int | num_added_literals |
int | num_deleted_clauses |
int | num_deleted_literals |
Struct**********************************************************************
Synopsis [Definition of the statistics of clause database]
Description []
SeeAlso [CDatabase]
Definition at line 69 of file xchaff_dbase.h.
int CDatabaseStats::mem_used_up_counts |
Definition at line 70 of file xchaff_dbase.h.
Referenced by CDatabase::CDatabase().
bool CDatabaseStats::mem_used_up |
Definition at line 71 of file xchaff_dbase.h.
Referenced by CDatabase::CDatabase(), CSolver::delete_unrelevant_clauses(), and CDatabase::enlarge_lit_pool().
int CDatabaseStats::init_num_clauses |
Definition at line 72 of file xchaff_dbase.h.
Referenced by CDatabase::CDatabase(), and CDatabase::init_num_clauses().
int CDatabaseStats::init_num_literals |
Definition at line 73 of file xchaff_dbase.h.
Referenced by CDatabase::CDatabase(), and CDatabase::init_num_literals().
int CDatabaseStats::num_added_clauses |
Definition at line 74 of file xchaff_dbase.h.
Referenced by CSolver::add_clause(), CDatabase::CDatabase(), and CDatabase::num_added_clauses().
int CDatabaseStats::num_added_literals |
Definition at line 75 of file xchaff_dbase.h.
Referenced by CSolver::add_clause(), CDatabase::CDatabase(), CDatabase::num_added_literals(), and CDatabase::num_literals().
int CDatabaseStats::num_deleted_clauses |
Definition at line 76 of file xchaff_dbase.h.
Referenced by CDatabase::CDatabase(), CDatabase::mark_clause_deleted(), and CDatabase::num_deleted_clauses().
int CDatabaseStats::num_deleted_literals |
Definition at line 77 of file xchaff_dbase.h.
Referenced by CDatabase::CDatabase(), CDatabase::mark_clause_deleted(), CDatabase::num_deleted_literals(), and CDatabase::num_literals().