64 CHECK(cout <<
"Begin Compaction " <<
endl;);
77 for (
unsigned i=1; i<
variables().size(); ++i) {
110 CHECK(cout <<
"Begin Enlarge Lit Pool" <<
endl;);
135 int new_size = (int)(old_size * grow_ratio);
145 long displacement = _lit_pool_start - old_start;
146 for (
unsigned i=0; i<
clauses().size(); ++i)
150 for (
unsigned i=0; i<
variables().size(); ++i) {
152 for (
int j=0; j< 2 ; ++j) {
153 vector<CLitPoolElement *> & ht_ptr = v.
ht_ptr(j);
154 for (
unsigned k=0; k< ht_ptr.size(); ++k) {
155 ht_ptr[k] += displacement;
177 os <<
"Clause : " << cl_idx;
180 os <<
"\t\t\t======removed=====";
188 for (i=0; i<sz; ++i) {
198 os <<
"Dump Database: " <<
endl;
199 for(
unsigned i=0; i<
_clauses.size(); ++i)
203 os <<
"VID: " << i <<
"\t" <<
variable(i);
CLitPoolElement *& first_lit(void)
void compact_lit_pool(void)
int literal_value(CLitPoolElement l)
int lit_pool_free_space(void)
CLitPoolElement * lit_pool_begin(void)
void dump(ostream &os=cout)
vector< CClause > _clauses
vector< CClause > & clauses(void)
#define STARTUP_LIT_POOL_SIZE
void lit_pool_push_back(int value)
CLitPoolElement & literal(int idx)
vector< CVariable > & variables(void)
CLitPoolElement * _lit_pool_end_storage
void output_lit_pool_state(void)
int estimate_mem_usage(void)
CLitPoolElement * _lit_pool_finish
CVariable & variable(int idx)
vector< CLitPoolElement * > & ht_ptr(int i)
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
CLitPoolElement * literals(void)
bool enlarge_lit_pool(void)
CLitPoolElement * _lit_pool_start
CLitPoolElement & lit_pool(int i)
void detail_dump_cl(ClauseIdx cl_idx, ostream &os=cout)
CClause & clause(ClauseIdx idx)
vector< CVariable > _variables