Cross Reference: /pkg/src/modules/solver/solver.c

Lines Matching defs:size
62 // Returns a random integer 0 <= x < size. Seed must never be 0.
63 static inline int irand(double* seed, int size) {
64     return (int)(drand(seed) * size); }
70 void sort(void** array, int size, int(*comp)(const void *, const void *));
177         int next = irand(&s->random_seed,s->size);
178         assert(next >= 0 && next < s->size);
192         int    size  = veci_size(&s->order)-1;
193         int    x     = heap[size];
195         veci_resize(&s->order,size);
199         if (size > 0){
206             while (child < size){
207                 if (child+1 < size && activity[heap[child]] < activity[heap[child+1]])
210                 assert(child < size);
237     for (i = 0; i < s->size; i++)
279 /* pre: size > 1 && no variable occurs twice
283     int size;
289     size           = end - begin;
290     c              = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
291     c->size_learnt = (size << 1) | learnt;
294     for (i = 0; i < size; i++)
298         *((float*)&c->lits[size]) = 0.0;
301     assert(begin[0] < s->size*2);
303     assert(begin[1] < s->size*2);
305     assert(lit_neg(begin[0]) < s->size*2);
306     assert(lit_neg(begin[1]) < s->size*2);
311     vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
312     vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
320     assert(lit_neg(lits[0]) < s->size*2);
321     assert(lit_neg(lits[1]) < s->size*2);
326     assert(lits[0] < s->size*2);
379     for (var = s->size; var < n; var++){
396     s->size = n > s->size ? n : s->size;
495     double  F        = 1.0 / s->size;
496     for (i = 0; i < s->size; i++)
499     return progress / s->size;
512     assert(lit_var(l) >= 0 && lit_var(l) < s->size);
520         assert(v >= 0 && v < s->size);
588             assert(lit_var(q) >= 0 && lit_var(q) < s->size);
607                 assert(lit_var(q) >= 0 && lit_var(q) < s->size);
643     // update size of learnt + statistics
655     for (i = 0; i < s->size; i++)
870                 for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]);
876                 for (i = 0; i < s->size; i++) 
920     s->size                   = 0;
1005     vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
1006     vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
1055         for (i = 0; i < s->size*2; i++)
1226     return s->size;
1244 static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
1249     for (i = 0; i < size-1; i++){
1251         for (j = i+1; j < size; j++){
1260 static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
1262     if (size <= 15)
1263         selectionsort(array, size, comp);
1266         void*       pivot = array[irand(seed, size)];
1269         int         j = size;
1281         sortrnd(&array[i], size-i, comp, seed);
1285 void sort(void** array, int size, int(*comp)(const void *, const void *))
1288     sortrnd(array,size,comp,&seed);