YuhangQ/cloud-sat
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

delete unused code

Browse Source
This commit is contained in:
ihan-o 2023-04-21 17:31:53 +08:00
parent 07a2c5cc72
commit a55a8d4c2e
12 changed files with 31 additions and 374 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
hostfile Normal file
View File

@ -0,0 +1,2 @@
192.168.100.6
192.168.100.9

18
kissat-inc/makefile
View File

@ -1,17 +1,17 @@
all:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build"
$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build"
kissat:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" kissat
$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" kissat
tissat:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" tissat
$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" tissat
clean:
rm -f "/pub/netdisk1/qianyh/Light/kissat-inc"/makefile
-$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" clean
rm -rf "/pub/netdisk1/qianyh/Light/kissat-inc/build"
rm -f "/home/chenzh/solvers/cloud-sat/kissat-inc"/makefile
-$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" clean
rm -rf "/home/chenzh/solvers/cloud-sat/kissat-inc/build"
coverage:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" coverage
$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" coverage
indent:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" indent
$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" indent
test:
$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" test
$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" test
.PHONY: all clean coverage indent kissat test tissat

52
src/clause.hpp
View File

@ -54,56 +54,4 @@ struct clause_store {
}
};
struct period_clauses {
int period;
std::atomic<int> refs;
std::vector<shared_ptr<clause_store>> cls;
period_clauses(int p = 0) {
refs = 0;
period = p;
}
void increase_refs(int inc) {
refs += inc;
}
bool free_clause() {
int ref = refs.fetch_sub(1);
if (ref <= 1) {
if (ref <= 0) puts("**************************========================");
return true;
}
return false;
}
void release_clause() {
for (int i = 0; i < cls.size(); i++)
cls[i]->free_clause();
}
void push(shared_ptr<clause_store> c) {
cls.push_back(c);
}
};
struct period_queue {
std::deque<period_clauses *> q;
mutable boost::mutex mtx;
void push(period_clauses * c) {
boost::mutex::scoped_lock lock(mtx);
q.push_back(c);
}
void pop(int assert_period = -1) {
boost::mutex::scoped_lock lock(mtx);
if (assert_period != -1 && q.front()->period != assert_period) printf("c ............false free pos\n");
q.front()->release_clause();
q.pop_front();
}
period_clauses* find(int period) {
boost::mutex::scoped_lock lock(mtx);
int sp = q.front()->period;
if (period - sp >= q.size()) puts("may occur wrong");
return q[period - sp];
}
};
#endif

48
src/light.cpp
View File

@ -8,8 +8,7 @@
light::light():
finalResult (0),
winner_period (1e9),
winner_id (-1),
winner_id (1e9),
maxtime (5000)
{
// opt = new paras();
@ -21,50 +20,6 @@ light::~light() {
workers.clear(true);
}
void light::configure_from_file(const char* file) {
if (!strcmp(file, "")) {
configure_name = new vec<char*>[OPT(threads)];
configure_val = new vec<double>[OPT(threads)];
return;
}
assert(false);
// printf("c Get configure file: %s\n", file);
// std::ifstream fin(file);
// char buf[1000];
// fin.getline(buf, 1000);
// char *p = buf + 6;
// int ws, ss, id = 0;
// p = read_int(p, &ws);
// p = read_int(p, &ss);
// printf("%d %d\n", ws, ss);
// opt->set_para("threads", ws);
// configure_name = new vec<char*>[ws];
// configure_val = new vec<double>[ws];
// while (fin.getline(buf, 1000)) {
// p = strtok(buf, " ");
// printf("%s\n", p);
// solver_type.push(0);
// while (p) {
// p = strtok(NULL, " ");
// printf("%s\n", p);
// if (!p) break;
// int l = strlen(p), pos = 0;
// for (int i = 1; i < l; i++)
// if (p[i] == '=') pos = i;
// char *name = new char[pos];
// strncpy(name, p, pos);
// printf("%s\n", name);
// configure_name[id].push(name);
// char *val = p + pos + 1;
// double v = atof(val);
// printf("%.2lf\n", v);
// configure_val[id].push(v);
// }
// printf("out\n");
// id++;
// }
}
void light::arg_parse(int argc, char **argv) {
cmdline::parser parser;
@ -97,6 +52,5 @@ void light::arg_parse(int argc, char **argv) {
memcpy(filename, file_string.c_str(), file_string.length());
filename[file_string.length()] = '\0';
configure_from_file(OPT(config).c_str());
}

17
src/light.hpp
View File

@ -55,26 +55,18 @@ public:
char* filename;
char* instance;
vec<char*> *configure_name;
vec<double> *configure_val;
int finalResult;
int winner_period, winner_id;
int winner_id;
mutable boost::mutex winner_mtx;
int maxtime;
void update_winner(int id, int period) {
boost::mutex::scoped_lock lock(winner_mtx);
if (period < winner_period || (period == winner_period && id < winner_id)) {
winner_period = period;
boost::mutex::scoped_lock lock(winner_mtx);
if (id < winner_id) {
winner_id = id;
}
}
int get_winner_period() {
boost::mutex::scoped_lock lock(winner_mtx);
return winner_period;
}
void arg_parse(int argc, char **argv);
void init_workers();
void diversity_workers();
@ -83,7 +75,6 @@ public:
int run();
int solve();
void terminate_workers();
void configure_from_file(const char*);
};
#endif

31
src/sharer.cpp
View File

@ -256,37 +256,6 @@ void sharer::do_clause_sharing() {
auto clk_ed = std::chrono::high_resolution_clock::now();
share_time += 0.001 * std::chrono::duration_cast<std::chrono::milliseconds>(clk_ed - clk_now).count();
}
int sharer::import_clauses(int id) {
int current_period = producers[id]->get_period() - 1, import_period = current_period - OPT(margin);
if (import_period < 0) return 0;
basesolver *t = producers[id];
for (int i = 0; i < producers.size(); i++) {
if (i == id) continue;
basesolver *s = producers[i];
//wait for s reach period $import_period
// printf("c %d start waiting, since import_p is %d, current_p is %d\n", id, import_period, s->get_period());
boost::mutex::scoped_lock lock(s->mtx);
while (s->period <= import_period && s->terminate_period > import_period && !s->terminated) {
s->cond.wait(lock);
}
if (s->terminated) return -1;
if (s->terminate_period <= import_period) return -1;
period_clauses *pc = s->pq.find(import_period);
if (pc->period != import_period) {
printf("thread %d, now period = %d, import period = %d, import thread %d\n", id, current_period, import_period, i);
puts("*******************************************************");
}
// printf("c %d finish waiting %d %d\n", id, import_period, s->period_queue[pos]->period);
t->import_clauses_from(pc->cls);
}
t->unfree.push(import_period);
return 1;
// printf("c thread %d, period %d, import finish\n", id, current_period);
}
int sharer::sort_clauses(int x) {
for (int i = 0; i < cls.size(); i++) {

1
src/sharer.hpp
View File

@ -36,7 +36,6 @@ public:
int receive_clauses_from_other_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter);
int sort_clauses(int x);
int import_clauses(int id);
private:
light* S;

46
src/solve.cpp
View File

@ -29,32 +29,18 @@ void * solve_worker(void *arg) {
basesolver * sq = (basesolver *)arg;
while (!terminated) {
int res = sq->solve();
if (OPT(DPS)) {
//printf("c %d solved, res is %d\n", sq->id, res);
if (res) {
terminated = 1;
result = res;
//printf("c %d solved 1\n", sq->id);
sq->internal_terminate();
//printf("c %d solved 2\n", sq->id);
sq->controller->update_winner(sq->id, sq->period);
//printf("c %d solved 3\n", sq->id);
if (res == 10) sq->get_model(sq->model);
}
//printf("c %d really solved, period is %d\n", sq->id, sq->period);
}
else {
if (res && !terminated) {
//printf("c result: %d, winner is %d, winner run %d confs\n", res, sq->id, sq->get_conflicts());
terminated = 1;
sq->controller->terminate_workers();
result = res;
sq->controller->update_winner(sq->id, 0);
winner_conf = sq->get_conflicts();
if (res == 10) sq->get_model(sq->model);
}
//printf("get result %d with res %d\n", sq->id, res);
if (res && !terminated) {
//printf("c result: %d, winner is %d, winner run %d confs\n", res, sq->id, sq->get_conflicts());
terminated = 1;
sq->controller->terminate_workers();
result = res;
sq->controller->update_winner(sq->id, 0);
winner_conf = sq->get_conflicts();
if (res == 10) sq->get_model(sq->model);
}
//printf("get result %d with res %d\n", sq->id, res);
}
return NULL;
}
@ -163,20 +149,13 @@ void light::diversity_workers() {
else
workers[i]->configure("phase", 1);
}
for (int j = 0; j < configure_name[i].size(); j++) {
workers[i]->configure(configure_name[i][j], configure_val[i][j]);
}
}
}
void light::terminate_workers() {
// printf("c controller reach limit\n");
for (int i = 0; i < OPT(threads); i++) {
if (OPT(share) == 1 && OPT(DPS) == 1)
workers[i]->external_terminate();
else
workers[i]->terminate();
workers[i]->terminate();
}
}
@ -211,7 +190,6 @@ int light::solve() {
for (int j = 0; j < OPT(threads); j++) {
s->producers.push(workers[j]);
s->consumers.push(workers[j]);
workers[j]->in_sharer = s;
}
s->clause_sharing_init(sharing_groups);
}

26
src/solver_api/basekissat.cpp
View File

@ -108,8 +108,6 @@ basekissat::basekissat(int id, light* light) : basesolver(id, light) {
if (OPT(share)) {
solver -> cbkImportClause = call_back_in;
solver -> cbkExportClause = call_back_out;
solver -> cbk_start_new_period = cbk_start_new_period;
solver -> cbk_free_clauses = cbk_free_clauses;
solver -> dps = OPT(DPS);
solver -> dps_period = OPT(DPS_period);
}
@ -119,19 +117,6 @@ basekissat::~basekissat(){
delete solver;
}
void basekissat::parse_from_CNF(char* filename) {
int vars, clauses;
vec<vec<int>> clause;
readfile(filename, &vars, &clauses, clause);
maxvar = vars;
kissat_reserve(solver, vars);
for (int i = 1; i <= clauses; i++) {
int l = clause[i].size();
for (int j = 0; j < l; j++)
add(clause[i][j]);
add(0);
}
}
void basekissat::parse_from_MEM(char* instance) {
int vars, clauses;
@ -147,17 +132,6 @@ void basekissat::parse_from_MEM(char* instance) {
}
}
void basekissat::parse_from_PAR(preprocess* pre) {
maxvar = pre->vars;
kissat_reserve(solver, pre->vars);
for (int i = 1; i <= pre->clauses; i++) {
int l = pre->clause[i].size();
for (int j = 0; j < l; j++)
add(pre->clause[i][j]);
add(0);
}
}
int basekissat::get_conflicts() {
return solver->nconflict;
}

3
src/solver_api/basekissat.hpp
View File

@ -13,8 +13,6 @@ public:
int configure(const char* name, int id);
int get_conflicts();
void parse_from_CNF(char* filename);
void parse_from_PAR(preprocess *pre);
void parse_from_MEM(char* instance);
void exp_clause(void *cl, int lbd);
bool imp_clause(shared_ptr<clause_store>cls, void *cl);
@ -25,5 +23,4 @@ public:
friend int cbkImportClause(void *, int *, cvec *);
friend int cbkExportClause(void *, int *, cvec *);
friend void cbk_free_clauses(void *);
};

135
src/solver_api/basesolver.cpp
View File

@ -1,33 +1,6 @@
#include "basesolver.hpp"
#include "../sharer.hpp"
int basesolver::get_period() {
boost::mutex::scoped_lock lock(mtx);
return period;
};
void basesolver::inc_period() {
boost::mutex::scoped_lock lock(mtx);
period++;
if (period % 100 == 0) printf("c %d reach period %d\n", id, period);
cond.notify_all();
};
void basesolver::internal_terminate() {
boost::mutex::scoped_lock lock(mtx);
terminate_period = period;
cond.notify_all();
}
void basesolver::external_terminate() {
{
boost::mutex::scoped_lock lock(mtx);
terminated = 1;
cond.notify_all();
// printf("c thread %d terminated\n", id);
}
terminate();
}
void basesolver::broaden_export_limit() {
++good_clause_lbd;
}
@ -37,23 +10,11 @@ void basesolver::restrict_export_limit() {
--good_clause_lbd;
}
double basesolver::get_waiting_time() {
return waiting_time;
}
void basesolver::export_clauses_to(std::vector<shared_ptr<clause_store>> &clauses) {
shared_ptr<clause_store> cls;
while (export_clause.pop(cls)) {
// printf("size: %d [", cls->size);
// for(int i=0; i<cls->size; i++) {
// printf("%d ", cls->data[i]);
// }
// printf("] \n");
while (export_clause.pop(cls))
clauses.push_back(cls);
}
}
void basesolver::import_clauses_from(std::vector<shared_ptr<clause_store>> &clauses) {
@ -62,101 +23,9 @@ void basesolver::import_clauses_from(std::vector<shared_ptr<clause_store>> &clau
}
}
void basesolver::select_clauses() {
sharer *share = in_sharer;
cls.clear();
export_clauses_to(cls);
for (int i = 0; i < cls.size(); i++) {
int sz = cls[i]->size;
while (sz > bucket.size()) bucket.push();
if (sz * (bucket[sz - 1].size() + 1) <= OPT(share_lits))
bucket[sz - 1].push_back(cls[i]);
}
period_clauses *pcls = new period_clauses(period);
int space = OPT(share_lits);
for (int i = 0; i < bucket.size(); i++) {
int clause_num = space / (i + 1);
if (!clause_num) break;
if (clause_num >= bucket[i].size()) {
space -= bucket[i].size() * (i + 1);
for (int j = 0; j < bucket[i].size(); j++)
pcls->push(bucket[i][j]);
bucket[i].clear();
}
else {
space -= clause_num * (i + 1);
for (int j = 0; j < clause_num; j++) {
pcls->push(bucket[i].back());
bucket[i].pop_back();
}
}
}
int percent = (OPT(share_lits) - space) * 100 / OPT(share_lits);
if (percent < 75) broaden_export_limit();
if (percent > 98) restrict_export_limit();
//sort finish
pcls->increase_refs(share->producers.size() - 1);
pq.push(pcls);
}
void basesolver::get_model(vec<int> &model) {
model.clear();
for (int i = 1; i <= maxvar; i++) {
model.push(val(i));
}
}
void cbk_start_new_period(void *solver) {
auto clk_st = std::chrono::high_resolution_clock::now();
basesolver* S = (basesolver *) solver;
sharer *share = S->in_sharer;
int should_free = 1;
if (S->period >= S->controller->get_winner_period()) {
S->internal_terminate();
S->terminate();
return;
}
printf("c thread %d into select %d\n", S->id, S->period);
S->select_clauses();
// printf("c %d now finish period %d\n", S->id, S->get_period());
S->inc_period();
// printf("c thread %d start import at %d\n", S->id, S->period);
should_free = share->import_clauses(S->id);
printf("c thread %d finish import at %d\n", S->id, S->period);
if (should_free == -1) {
S->internal_terminate();
S->terminate();
}
auto clk_now = std::chrono::high_resolution_clock::now();
int solve_time = std::chrono::duration_cast<std::chrono::milliseconds>(clk_now - clk_st).count();
S->waiting_time += 0.001 * solve_time;
// printf("c %d wait for %d.%03ds\n", S->id, solve_time / 1000, solve_time % 1000);
// printf("c %d finish sharing\n", S->id);
}
void cbk_free_clauses(void *solver) {
basesolver* S = (basesolver *) solver;
sharer *share = S->in_sharer;
if (S->unfree.size()) printf("free %d period\n", S->unfree.size());
for (int id = 0; id < S->unfree.size(); id++) {
int import_period = S->unfree[id];
// int current_period = S->get_period() - 1, import_period = current_period - share->margin;
// if (import_period < 0) return;
for (int i = 0; i < share->producers.size(); i++) {
if (i == S->id) continue;
basesolver *s = share->producers[i];
period_clauses *pc = s->pq.find(import_period);
if (pc->period != import_period)
puts("*******************************************************");
if (pc->free_clause()) {
s->pq.pop(import_period);
// printf("thread %d enter, %d is free\n", S->id, i);
}
}
}
S->unfree.clear();
}
}

26
src/solver_api/basesolver.hpp
View File

@ -20,8 +20,6 @@ public:
virtual int configure(const char* name, int id) = 0;
virtual int get_conflicts() = 0;
virtual void parse_from_CNF(char* filename) = 0;
virtual void parse_from_PAR(preprocess* pre) = 0;
virtual void parse_from_MEM(char* instance) = 0;
virtual void exp_clause(void *cl, int lbd) = 0;
virtual bool imp_clause(shared_ptr<clause_store>cls, void *cl) = 0;
@ -30,38 +28,21 @@ public:
void import_clauses_from(std::vector<shared_ptr<clause_store>> &clauses);
void get_model(vec<int> &model);
void select_clauses();
void broaden_export_limit();
void restrict_export_limit();
double get_waiting_time();
int get_period();
void inc_period();
void internal_terminate();
void external_terminate();
double waiting_time = 0;
int good_clause_lbd = 0;
light * controller;
int id;
sharer* in_sharer;
vec<int> model;
int terminate_period = 1e9;
int maxvar, period, margin, terminated = 0;
mutable boost::mutex mtx;
boost::condition_variable cond;
period_queue pq;
std::vector<shared_ptr<clause_store>> cls;
vec<std::vector<shared_ptr<clause_store>>> bucket;
vec<int> unfree;
int maxvar, terminated = 0;
boost::lockfree::spsc_queue<shared_ptr<clause_store>, boost::lockfree::capacity<10240000>> import_clause;
boost::lockfree::spsc_queue<shared_ptr<clause_store>, boost::lockfree::capacity<10240000>> export_clause;
basesolver(int sid, light* light) : id(sid), controller(light) {
good_clause_lbd = 2;
period = 0;
margin = 0;
}
~basesolver() {
@ -69,11 +50,6 @@ public:
controller = NULL;
}
}
friend void cbk_start_new_period(void *);
friend void cbk_free_clauses(void *);
};
void cbk_start_new_period(void *);
void cbk_free_clauses(void *);
#endif