diff --git a/.gitignore b/.gitignore index c795b05..9acac60 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ -build \ No newline at end of file +build +.nfs* \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json index 0cb4a6f..7283762 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,5 +1,6 @@ { "files.associations": { + "*.ejs": "html", "cstring": "cpp", "typeinfo": "cpp", "iostream": "cpp", @@ -74,6 +75,7 @@ "regex": "cpp", "scoped_allocator": "cpp", "shared_mutex": "cpp", - "valarray": "cpp" + "valarray": "cpp", + "strstream": "cpp" } } \ No newline at end of file diff --git a/build.sh b/build.sh index 52be3c7..2d46fad 100755 --- a/build.sh +++ b/build.sh @@ -6,17 +6,15 @@ COMPILE_THREADS=16 # build kissat -cd kissat-inc -./configure -make -j $COMPILE_THREADS -cd .. +# cd kissat-inc +# ./configure +# make -j $COMPILE_THREADS +# cd .. # build and copy light-solver make -C src-light-solver -j $COMPILE_THREADS -cp src-light-solver/build/light-solver . # build and copy light-master -make -C src-light-master -j $COMPILE_THREADS -cp src-light-master/build/light-master . \ No newline at end of file +make -C src-light-master -j $COMPILE_THREADS \ No newline at end of file diff --git a/light-master b/light-master deleted file mode 100755 index a14e7f4..0000000 Binary files a/light-master and /dev/null differ diff --git a/light-master b/light-master new file mode 120000 index 0000000..2263418 --- /dev/null +++ b/light-master @@ -0,0 +1 @@ +./src-light-master/build/light-master \ No newline at end of file diff --git a/light-solver b/light-solver deleted file mode 100755 index 1eeeb77..0000000 Binary files a/light-solver and /dev/null differ diff --git a/light-solver b/light-solver new file mode 120000 index 0000000..f4bb3d2 --- /dev/null +++ b/light-solver @@ -0,0 +1 @@ +./src-light-solver/build/light-solver \ No newline at end of file diff --git a/makefile b/makefile deleted file mode 100644 index b1a6896..0000000 --- a/makefile +++ /dev/null @@ -1,18 +0,0 @@ - - - - - -build-kissat: - cd kissat-inc - ls - sh ./configure - make - - -all: build-kissat - make -C src-light-master - make -C src-light-solver - cp src-light-master/build/light-master . - cp src-light-solver/build/light-solver . - diff --git a/src-light-master/master.cpp b/src-light-master/master.cpp index 8aa9e3e..93e5628 100644 --- a/src-light-master/master.cpp +++ b/src-light-master/master.cpp @@ -2,28 +2,9 @@ #include "master.h" -// struct { -// std::string ip_addr; -// std::vector solver_ip_addrs; -// std::string instance; -// }opt; - -// void parse_input(const nlohmann::json& config) { - - - -// } - - -// void run_master(const nlohmann::json& config) { -// parse_input(config); - - - - -// } - int main() { - printf("This is master!\n"); + printf("=====================================\n"); + + return 0; } \ No newline at end of file diff --git a/src-light-solver/light.cpp b/src-light-solver/light.cpp index 34f5a3b..4b8440d 100644 --- a/src-light-solver/light.cpp +++ b/src-light-solver/light.cpp @@ -4,6 +4,8 @@ #include #include +#include "utils/cmdline.h" + light::light(): finalResult (0), winner_period (1e9), @@ -19,7 +21,6 @@ light::~light() { workers.clear(true); } - void light::configure_from_file(const char* file) { if (!strcmp(file, "")) { configure_name = new vec[OPT(threads)]; @@ -64,28 +65,43 @@ void light::configure_from_file(const char* file) { } void light::arg_parse(int argc, char **argv) { - for (int i = 1; i < argc; i++) { - char *arg = argv[i]; - if (arg[0] != '-' || arg[1] != '-') { - filename = arg; continue; - } - int l = strlen(arg), pos = 0; - for (int i = 2; i < l; i++) - if (arg[i] == '=') pos = i; - if (!pos) continue; - char name[50]; - strncpy(name, arg + 2, pos - 2); - name[pos - 2] = '\0'; - char* val = arg + pos + 1; - if (opt->map_int.count(name)) opt->set_para(name, atoi(val)); - else if (opt->map_double.count(name)) opt->set_para(name, atof(val)); - else opt->set_para(name, val); - } - opt->sync_paras(); - printf("%s\n", OPT(config).c_str()); + cmdline::parser parser; + + // define argument list + parser.add("inst", 'i', "CNF format instance", true, ""); + + #define PARA(N, T, D, L, H, C) \ + if (!strcmp(#T, "int")) parser.add(#N, '\0', C, false, D, cmdline::range((int)L, (int)H)); \ + else parser.add(#N, '\0', C, false, D, cmdline::range((double)L, (double)H)); + PARAS + #undef PARA + + parser.parse_check(argc, argv); + + // set cnf filename + std::string file_string = parser.get("inst"); + filename = new char[file_string.size() + 1]; + memcpy(filename, file_string.c_str(), file_string.length()); + filename[file_string.length()] = '\0'; + + #define PARA(N, T, D, L, H, C) \ + if (!strcmp(#T, "int")) OPT(N) = parser.get(#N); \ + else OPT(N) = parser.get(#N); + PARAS + #undef PARA + + // print arguments + printf("------------ arguments ------------\n"); + + printf("%-20s: %s\n", "inst", filename); + + #define PARA(N, T, D, L, H, C) \ + if (!strcmp(#T, "int")) printf("%-20s: %-10d\n", #N, OPT(N)); \ + else printf("%-20s: %-10.2f\n", #N, OPT(N)); + PARAS + #undef PARA + + printf("-----------------------------------\n"); + configure_from_file(OPT(config).c_str()); - printf("444\n"); - opt->sync_paras(); - opt->print_change(); - printf("c filename: %s\n", filename); } \ No newline at end of file diff --git a/src-light-solver/main.cpp b/src-light-solver/main.cpp index a5457d3..924ad32 100644 --- a/src-light-solver/main.cpp +++ b/src-light-solver/main.cpp @@ -7,14 +7,6 @@ #include "utils/cmdline.h" int main(int argc, char **argv) { - - cmdline::parser a; - - a.add("inst", 'i', "CNF format instance", true, ""); - - a.parse_check(argc, argv); - solve(argc, argv); - return 0; } \ No newline at end of file diff --git a/src-light-solver/makefile b/src-light-solver/makefile index f3daf3a..0223723 100644 --- a/src-light-solver/makefile +++ b/src-light-solver/makefile @@ -6,7 +6,7 @@ OBJECTS := $(addprefix build/,$(SOURCES:%=%.o)) # 声明编译器和编译选项 CXX := g++ -CXXFLAGS := -O3 -Wall -Wextra -MMD -MP -flto +CXXFLAGS := -O0 -Wall -Wextra -MMD -MP -g LIBS := -lkissat -L../kissat-inc/build -I ../kissat-inc/ \ -lm4ri -Lpreprocess/m4ri-20140914/.libs -I preprocess/m4ri-20140914/ \ diff --git a/src-light-solver/solve.cpp b/src-light-solver/solve.cpp index 7e62038..946a139 100644 --- a/src-light-solver/solve.cpp +++ b/src-light-solver/solve.cpp @@ -176,14 +176,17 @@ int light::solve() { } int light::run() { + init_workers(); diversity_workers(); + if (OPT(simplify)) { pre = new preprocess(); int res = pre->do_preprocess(filename); if (!res) return 20; } else worker_sign = filename; + parse_input(); if (OPT(share)) share(); int res = solve();