89 static bool clause_pool_invariant(clause_pool_t *pool) {  in clause_pool_invariant()  argument
91     pool->learned <= pool->size &&  in clause_pool_invariant()
92     pool->size <= pool->capacity &&  in clause_pool_invariant()
93     pool->available == pool->capacity - pool->size &&  in clause_pool_invariant()
94     is_multiple_of_four(pool->learned) &&  in clause_pool_invariant()
95     is_multiple_of_four(pool->size) &&  in clause_pool_invariant()
96     is_multiple_of_four(pool->capacity);  in clause_pool_invariant()
102 static bool good_statistics(clause_pool_t *pool) {  in good_statistics()  argument
110   i = clause_pool_first_clause(pool);  in good_statistics()
111   while (i < pool->learned) {  in good_statistics()
113     prob_lits += clause_length(pool, i);  in good_statistics()
114     i = clause_pool_next_clause(pool, i);  in good_statistics()
116   while (i < pool->size) {  in good_statistics()
118     learned_lits += clause_length(pool, i);  in good_statistics()
119     i = clause_pool_next_clause(pool, i);  in good_statistics()
123     prob_clauses == pool->num_prob_clauses &&  in good_statistics()
124     prob_lits == pool->num_prob_literals &&  in good_statistics()
125     learned_clauses == pool->num_learned_clauses &&  in good_statistics()
126     learned_lits == pool->num_learned_literals;  in good_statistics()
135 void init_clause_pool(clause_pool_t *pool) {  in init_clause_pool()  argument
143   pool->data = tmp;  in init_clause_pool()
144   pool->learned = 0;  in init_clause_pool()
145   pool->size = 0;  in init_clause_pool()
146   pool->capacity = DEF_CLAUSE_POOL_CAPACITY;  in init_clause_pool()
147   pool->available = DEF_CLAUSE_POOL_CAPACITY;  in init_clause_pool()
149   pool->num_prob_clauses = 0;  in init_clause_pool()
150   pool->num_prob_literals = 0;  in init_clause_pool()
151   pool->num_learned_clauses = 0;  in init_clause_pool()
152   pool->num_learned_literals = 0;  in init_clause_pool()
154   assert(clause_pool_invariant(pool));  in init_clause_pool()
157 void delete_clause_pool(clause_pool_t *pool) {  in delete_clause_pool()  argument
158   assert(clause_pool_invariant(pool));  in delete_clause_pool()
159   free(pool->data);  in delete_clause_pool()
160   pool->data = NULL;  in delete_clause_pool()
163 void reset_clause_pool(clause_pool_t *pool) {  in reset_clause_pool()  argument
166   assert(clause_pool_invariant(pool));  in reset_clause_pool()
168   if (pool->capacity > RESET_CLAUSE_POOL_CAPACITY) {  in reset_clause_pool()
169     free(pool->data);  in reset_clause_pool()
174     pool->data = tmp;  in reset_clause_pool()
175     pool->capacity = RESET_CLAUSE_POOL_CAPACITY;  in reset_clause_pool()
178   pool->learned = 0;  in reset_clause_pool()
179   pool->size = 0;  in reset_clause_pool()
180   pool->available = pool->capacity;  in reset_clause_pool()
183   pool->num_prob_clauses = 0;  in reset_clause_pool()
184   pool->num_prob_literals = 0;  in reset_clause_pool()
185   pool->num_learned_clauses = 0;  in reset_clause_pool()
186   pool->num_learned_literals = 0;  in reset_clause_pool()
188   assert(clause_pool_invariant(pool));  in reset_clause_pool()
196 static void resize_clause_pool(clause_pool_t *pool, uint32_t n) {  in resize_clause_pool()  argument
200   assert(clause_pool_invariant(pool));  in resize_clause_pool()
202   min_cap = pool->size + n;  in resize_clause_pool()
208   cap = pool->capacity;  in resize_clause_pool()
217   tmp = (uint32_t *) realloc(pool->data, cap * sizeof(uint32_t));  in resize_clause_pool()
222   pool->data = tmp;  in resize_clause_pool()
223   pool->capacity = cap;  in resize_clause_pool()
224   pool->available = cap - pool->size;  in resize_clause_pool()
226   assert(clause_pool_invariant(pool));  in resize_clause_pool()
233 static cidx_t clause_pool_alloc_array(clause_pool_t *pool, uint32_t n) {  in clause_pool_alloc_array()  argument
236   assert(clause_pool_invariant(pool));  in clause_pool_alloc_array()
239   if (n > pool->available) {  in clause_pool_alloc_array()
240     resize_clause_pool(pool, n);  in clause_pool_alloc_array()
242   assert(n <= pool->available);  in clause_pool_alloc_array()
244   i = pool->size;  in clause_pool_alloc_array()
245   pool->size += n;  in clause_pool_alloc_array()
246   pool->available -= n;  in clause_pool_alloc_array()
248   assert(clause_pool_invariant(pool));  in clause_pool_alloc_array()
259 static void init_clause(clause_pool_t *pool, cidx_t cidx, uint32_t n, const literal_t *a) {  in init_clause()  argument
263   pool->data[cidx] = n;  in init_clause()
264   pool->data[cidx + 1] = 0;  in init_clause()
265   p = pool->data + cidx + 2;  in init_clause()
274 cidx_t clause_pool_add_problem_clause(clause_pool_t *pool, uint32_t n, const literal_t *a) {  in clause_pool_add_problem_clause()  argument
277   assert(pool->learned == pool->size);  in clause_pool_add_problem_clause()
279   cidx = clause_pool_alloc_array(pool, n+2);  in clause_pool_add_problem_clause()
280   init_clause(pool, cidx, n, a);  in clause_pool_add_problem_clause()
282   pool->num_prob_clauses ++;  in clause_pool_add_problem_clause()
283   pool->num_prob_literals += n;  in clause_pool_add_problem_clause()
284   pool->learned = pool->size;  in clause_pool_add_problem_clause()
286   assert(good_statistics(pool));  in clause_pool_add_problem_clause()
294 cidx_t clause_pool_add_learned_clause(clause_pool_t *pool, uint32_t n, const literal_t *a) {  in clause_pool_add_learned_clause()  argument
297   cidx = clause_pool_alloc_array(pool, n+2);  in clause_pool_add_learned_clause()
298   init_clause(pool, cidx, n, a);  in clause_pool_add_learned_clause()
300   pool->num_learned_clauses ++;  in clause_pool_add_learned_clause()
301   pool->num_learned_literals += n;  in clause_pool_add_learned_clause()
303   assert(good_statistics(pool));  in clause_pool_add_learned_clause()
321 static inline uint32_t clause_full_length(clause_pool_t *pool, uint32_t i) {  in clause_full_length()  argument
322   assert(good_clause_idx(pool, i));  in clause_full_length()
323   return full_length(pool->data[i]);  in clause_full_length()
330 static inline bool is_padding_start(clause_pool_t *pool, uint32_t i) {  in is_padding_start()  argument
331   assert(i < pool->size && is_multiple_of_four(i));  in is_padding_start()
332   return pool->data[i] == 0;  in is_padding_start()
338 static inline uint32_t padding_length(clause_pool_t *pool, uint32_t i) {  in padding_length()  argument
339   assert(is_padding_start(pool, i));  in padding_length()
340   return pool->data[i+1];  in padding_length()
347 static void clause_pool_padding(clause_pool_t *pool, uint32_t i, uint32_t n) {  in clause_pool_padding()  argument
350   assert(i < pool->size && is_multiple_of_four(i)  in clause_pool_padding()
355   if (j == pool->size) {  in clause_pool_padding()
357     pool->size = i;  in clause_pool_padding()
358     if (pool->learned == j) {  in clause_pool_padding()
359       pool->learned = i;  in clause_pool_padding()
362     if (is_padding_start(pool, j)) {  in clause_pool_padding()
364       n += padding_length(pool, j);  in clause_pool_padding()
366     pool->data[i] = 0;  in clause_pool_padding()
367     pool->data[i+1] = n;  in clause_pool_padding()
375 void clause_pool_delete_clause(clause_pool_t *pool, cidx_t idx) {  in clause_pool_delete_clause()  argument
378   assert(good_clause_idx(pool, idx) && pool->learned > 0);  in clause_pool_delete_clause()
380   n = pool->data[idx]; // clause length  in clause_pool_delete_clause()
381   clause_pool_padding(pool, idx, n);  in clause_pool_delete_clause()
384   if (is_problem_clause_idx(pool, idx)) {  in clause_pool_delete_clause()
385     assert(pool->num_prob_clauses > 0);  in clause_pool_delete_clause()
386     assert(pool->num_prob_literals >= n);  in clause_pool_delete_clause()
387     pool->num_prob_clauses --;  in clause_pool_delete_clause()
388     pool->num_prob_literals -= n;  in clause_pool_delete_clause()
390     assert(pool->num_learned_clauses > 0);  in clause_pool_delete_clause()
391     assert(pool->num_learned_literals >= n);  in clause_pool_delete_clause()
392     pool->num_learned_clauses --;  in clause_pool_delete_clause()
393     pool->num_learned_literals -= n;  in clause_pool_delete_clause()
396   assert(good_statistics(pool));  in clause_pool_delete_clause()
403 void clause_pool_shrink_clause(clause_pool_t *pool, cidx_t idx, uint32_t n) {  in clause_pool_shrink_clause()  argument
406   assert(good_clause_idx(pool, idx) && pool->learned > 0 &&  in clause_pool_shrink_clause()
407 	 n >= 2 && n <= clause_length(pool, idx));  in clause_pool_shrink_clause()
409   old_n = clause_length(pool, idx);  in clause_pool_shrink_clause()
415     clause_pool_padding(pool, idx + new_len, old_len - new_len);  in clause_pool_shrink_clause()
418   pool->data[idx] = n;  in clause_pool_shrink_clause()
420   if (is_problem_clause_idx(pool, idx)) {  in clause_pool_shrink_clause()
421     assert(pool->num_prob_clauses > 0);  in clause_pool_shrink_clause()
422     assert(pool->num_prob_literals >= old_n);  in clause_pool_shrink_clause()
423     pool->num_prob_literals -= (old_n - n);  in clause_pool_shrink_clause()
425     assert(pool->num_learned_clauses > 0);  in clause_pool_shrink_clause()
426     assert(pool->num_learned_literals >= old_n);  in clause_pool_shrink_clause()
427     pool->num_learned_literals -= (old_n - n);  in clause_pool_shrink_clause()
430   assert(good_statistics(pool));  in clause_pool_shrink_clause()
438 static cidx_t next_clause_index(clause_pool_t *pool, cidx_t i) {  in next_clause_index()  argument
439   while (i < pool->size && is_padding_start(pool, i)) {  in next_clause_index()
440     i += padding_length(pool, i);  in next_clause_index()
449 cidx_t clause_pool_first_clause(clause_pool_t *pool) {  in clause_pool_first_clause()  argument
450   return next_clause_index(pool, 0);  in clause_pool_first_clause()
456 cidx_t clause_pool_first_learned_clause(clause_pool_t *pool) {  in clause_pool_first_learned_clause()  argument
457   return next_clause_index(pool, pool->learned);  in clause_pool_first_learned_clause()
463 cidx_t clause_pool_next_clause(clause_pool_t *pool, cidx_t idx) {  in clause_pool_next_clause()  argument
464   assert(good_clause_idx(pool, idx));  in clause_pool_next_clause()
465   return next_clause_index(pool, idx + clause_full_length(pool, idx));  in clause_pool_next_clause()