105 lines
3.5 KiB
C++
105 lines
3.5 KiB
C++
#include "../light.hpp"
|
|
#include "basesolver.hpp"
|
|
#include "sharer.hpp"
|
|
#include "clause.hpp"
|
|
#include <unistd.h>
|
|
|
|
void * share_worker(void *arg) {
|
|
sharer * sq = (sharer *)arg;
|
|
while (true) {
|
|
usleep(sq->share_intv);
|
|
if (terminated) break;
|
|
// printf("start sharing %d\n", sq->share_intv);
|
|
for (int i = 0; i < sq->producers.size(); i++) {
|
|
sq->cls.clear();
|
|
sq->producers[i]->export_clauses_to(sq->cls);
|
|
int number = sq->cls.size();
|
|
// printf("get %d exported clauses\n", number);
|
|
int percent = sq->sort_clauses(i);
|
|
if (percent < 75) {
|
|
sq->producers[i]->broaden_export_limit();
|
|
}
|
|
else if (percent > 98) {
|
|
sq->producers[i]->restrict_export_limit();
|
|
}
|
|
// for (int k = 0; k < sq->cls.size(); k++) {
|
|
// int x = sq->cls[k]->refs;
|
|
// printf("%d ", x);
|
|
// }
|
|
// puts("");
|
|
for (int j = 0; j < sq->consumers.size(); j++) {
|
|
if (sq->producers[i]->id == sq->consumers[j]->id) continue;
|
|
for (int k = 0; k < sq->cls.size(); k++)
|
|
sq->cls[k]->increase_refs(1);
|
|
sq->consumers[j]->import_clauses_from(sq->cls);
|
|
}
|
|
for (int k = 0; k < sq->cls.size(); k++) {
|
|
sq->cls[k]->free_clause();
|
|
}
|
|
}
|
|
// printf("end sharing\n");
|
|
// terminated = 1;
|
|
}
|
|
if (terminated) puts("terminated set to 1");
|
|
return NULL;
|
|
}
|
|
|
|
int sharer::sort_clauses(int x) {
|
|
for (int i = 0; i < cls.size(); i++) {
|
|
int sz = cls[i]->size;
|
|
// for (int j = 0; j < sz; j++) printf("%d ", cls[i]->data[j]);
|
|
// puts("");
|
|
while (sz > bucket[x].size()) bucket[x].push();
|
|
if (sz * (bucket[x][sz - 1].size() + 1) <= share_lits)
|
|
bucket[x][sz - 1].push(cls[i]);
|
|
// else
|
|
// cls[i]->free_clause();
|
|
}
|
|
cls.clear();
|
|
int space = share_lits;
|
|
for (int i = 0; i < bucket[x].size(); i++) {
|
|
int clause_num = space / (i + 1);
|
|
// printf("%d %d\n", clause_num, bucket[x][i].size());
|
|
if (!clause_num) break;
|
|
if (clause_num >= bucket[x][i].size()) {
|
|
space -= bucket[x][i].size() * (i + 1);
|
|
for (int j = 0; j < bucket[x][i].size(); j++)
|
|
cls.push(bucket[x][i][j]);
|
|
bucket[x][i].clear();
|
|
}
|
|
else {
|
|
space -= clause_num * (i + 1);
|
|
for (int j = 0; j < clause_num; j++) {
|
|
cls.push(bucket[x][i].last());
|
|
bucket[x][i].pop();
|
|
}
|
|
}
|
|
}
|
|
// for (int i = 0; i < cls.size(); i++) {
|
|
// int sz = cls[i]->size;
|
|
// for (int j = 0; j < sz; j++) printf("%d ", cls[i]->data[j]);
|
|
// puts("");
|
|
// }
|
|
return (share_lits - space) * 100 / share_lits;
|
|
}
|
|
|
|
void light::share() {
|
|
int sharers_number = 1;
|
|
for (int i = 0; i < sharers_number; i++) {
|
|
sharer* s = new sharer(i, OPT(share_intv), OPT(share_lits));
|
|
for (int j = 0; j < OPT(threads); j++) {
|
|
s->producers.push(workers[j]);
|
|
s->consumers.push(workers[j]);
|
|
}
|
|
sharers.push(s);
|
|
}
|
|
|
|
pthread_t *ptr = new pthread_t[sharers_number];
|
|
for (int i = 0; i < sharers_number; i++) {
|
|
pthread_create(&ptr[i], NULL, share_worker, sharers[i]);
|
|
}
|
|
|
|
// for (int i = 0; i < sharers_number; i++) {
|
|
// pthread_join(ptr[i], NULL);
|
|
// }
|
|
} |