Home
last modified time | relevance | path

Searched refs:lit_pool_size (Results 1 – 2 of 2) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/sat/
H A Dxchaff_dbase.cpp66 for (int i=1; i< lit_pool_size(); ++i){ //begin with 1 because 0 position is always 0 in compact_lit_pool()
82 for (int i=1; i< lit_pool_size(); ++i) { in compact_lit_pool()
90 for (int i=1; i< lit_pool_size(); ++i) { in compact_lit_pool()
103 if (lit_pool_size() - num_clauses() > num_literals() * 2) { in enlarge_lit_pool()
124 if (lit_pool_size() - num_clauses() > num_literals() * 1.1) { in enlarge_lit_pool()
169 cout << "Lit_Pool Used " << lit_pool_size() << " Free " << lit_pool_free_space() in output_lit_pool_state()
170 << " Total " << lit_pool_size() + lit_pool_free_space() in output_lit_pool_state()
172 …cout << " Efficiency " << (float)((float)num_literals()) / (float)((lit_pool_size() - num_clauses(… in output_lit_pool_state()
H A Dxchaff_dbase.h155 int lit_pool_size(void) { in lit_pool_size() function
175 (lit_pool_size() + lit_pool_free_space()); in estimate_mem_usage()
189 int lit_pool = (lit_pool_size() + lit_pool_free_space()) * sizeof(CLitPoolElement); in mem_usage()