From 7320c729b0c12aa99615399b6a85bc4099c899a6 Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Mon, 27 Mar 2023 15:44:39 +0800 Subject: [PATCH] =?UTF-8?q?=E4=BC=98=E5=8C=96=E5=8F=82=E6=95=B0=E7=9A=84?= =?UTF-8?q?=E8=A1=A8=E8=BE=BE=E6=96=B9=E5=BC=8F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .vscode/settings.json | 9 +++- src-light-master/master.cpp | 4 ++ src-light-solver/light.cpp | 35 +++++++++------ src-light-solver/light.hpp | 8 ++-- src-light-solver/main.cpp | 24 +++++++++-- src-light-solver/network.cpp | 60 ++++++++++++++++++++++++++ src-light-solver/network.h | 4 ++ src-light-solver/{utils => }/paras.cpp | 12 +++--- src-light-solver/paras.hpp | 55 +++++++++++++++++++++++ src-light-solver/solve.cpp | 19 +------- src-light-solver/solve.hpp | 3 -- src-light-solver/utils/paras.hpp | 52 ---------------------- src-light-solver/workers/sharer.hpp | 2 +- 13 files changed, 187 insertions(+), 100 deletions(-) create mode 100644 src-light-solver/network.cpp create mode 100644 src-light-solver/network.h rename src-light-solver/{utils => }/paras.cpp (85%) create mode 100644 src-light-solver/paras.hpp delete mode 100644 src-light-solver/solve.hpp delete mode 100644 src-light-solver/utils/paras.hpp diff --git a/.vscode/settings.json b/.vscode/settings.json index 7283762..34271f4 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -76,6 +76,13 @@ "scoped_allocator": "cpp", "shared_mutex": "cpp", "valarray": "cpp", - "strstream": "cpp" + "strstream": "cpp", + "buffer": "cpp", + "executor": "cpp", + "internet": "cpp", + "io_context": "cpp", + "netfwd": "cpp", + "socket": "cpp", + "timer": "cpp" } } \ No newline at end of file diff --git a/src-light-master/master.cpp b/src-light-master/master.cpp index 93e5628..300ae74 100644 --- a/src-light-master/master.cpp +++ b/src-light-master/master.cpp @@ -6,5 +6,9 @@ int main() { 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 4b8440d..41619b9 100644 --- a/src-light-solver/light.cpp +++ b/src-light-solver/light.cpp @@ -67,24 +67,25 @@ void light::configure_from_file(const char* file) { void light::arg_parse(int argc, char **argv) { cmdline::parser parser; - // define argument list - parser.add("inst", 'i', "CNF format instance", true, ""); + #define STR_PARA(N, S, M, D, C) \ + parser.add(#N, S, C, M, D); + STR_PARAS + #undef STR_PARA - #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)); + #define PARA(N, T, S, M, D, L, H, C) \ + if (!strcmp(#T, "int")) parser.add(#N, S, C, M, D, cmdline::range((int)L, (int)H)); \ + else parser.add(#N, S, C, M, 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 STR_PARA(N, S, M, D, C) \ + OPT(N) = parser.get(#N); + STR_PARAS + #undef STR_PARA - #define PARA(N, T, D, L, H, C) \ + #define PARA(N, T, S, M, D, L, H, C) \ if (!strcmp(#T, "int")) OPT(N) = parser.get(#N); \ else OPT(N) = parser.get(#N); PARAS @@ -93,9 +94,12 @@ void light::arg_parse(int argc, char **argv) { // print arguments printf("------------ arguments ------------\n"); - printf("%-20s: %s\n", "inst", filename); + #define STR_PARA(N, S, M, D, C) \ + printf("%-20s: %s\n", #N, OPT(N)); + STR_PARAS + #undef STR_PARA - #define PARA(N, T, D, L, H, C) \ + #define PARA(N, T, S, M, 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 @@ -103,5 +107,10 @@ void light::arg_parse(int argc, char **argv) { printf("-----------------------------------\n"); + std::string file_string = OPT(instance); + filename = new char[file_string.size() + 1]; + memcpy(filename, file_string.c_str(), file_string.length()); + filename[file_string.length()] = '\0'; + configure_from_file(OPT(config).c_str()); } \ No newline at end of file diff --git a/src-light-solver/light.hpp b/src-light-solver/light.hpp index 02d0d5e..ef4a980 100644 --- a/src-light-solver/light.hpp +++ b/src-light-solver/light.hpp @@ -1,9 +1,11 @@ #ifndef _light_hpp_INCLUDED #define _light_hpp_INCLUDED -#include "utils/paras.hpp" + #include "utils/parse.hpp" #include "preprocess/preprocess.hpp" +#include "paras.hpp" + #include #include #include @@ -32,13 +34,13 @@ struct light public: light(); ~light(); - - char *filename; paras *opt; preprocess *pre; vec solver_type; vec workers; vec sharers; + + char* filename; vec *configure_name; vec *configure_val; diff --git a/src-light-solver/main.cpp b/src-light-solver/main.cpp index 924ad32..d9f4817 100644 --- a/src-light-solver/main.cpp +++ b/src-light-solver/main.cpp @@ -3,10 +3,28 @@ #include #include -#include "solve.hpp" +#include "light.hpp" #include "utils/cmdline.h" +#include "network.h" +#include "paras.hpp" + +int main(int argc, char **argv) { + + light* S = new light(); + S->arg_parse(argc, argv); + + int res = S->run(); + if (res == 10) { + printf("s SATISFIABLE\n"); + // print_model(model); + } + else if (res == 20) { + printf("s UNSATISFIABLE\n"); + } + else { + printf("s UNKNOWN\n"); + } + delete(S); -int main(int argc, char **argv) { - solve(argc, argv); return 0; } \ No newline at end of file diff --git a/src-light-solver/network.cpp b/src-light-solver/network.cpp new file mode 100644 index 0000000..b9827e2 --- /dev/null +++ b/src-light-solver/network.cpp @@ -0,0 +1,60 @@ +#include +#include +#include +#include +#include +#include + +const int BACKLOG = 5; + +void listen(int port) { + int server_fd, new_socket; + struct sockaddr_in address; + int addrlen = sizeof(address); + + // 创建socket + if ((server_fd = socket(AF_INET, SOCK_STREAM, 0)) == 0) { + perror("socket failed"); + exit(EXIT_FAILURE); + } + + // 设置服务器地址和端口号 + address.sin_family = AF_INET; + address.sin_addr.s_addr = INADDR_ANY; + address.sin_port = htons(port); + + // 绑定socket到地址 + if (bind(server_fd, (struct sockaddr *)&address, sizeof(address))<0) { + perror("bind failed"); + exit(EXIT_FAILURE); + } + + // 开始监听客户端连接 + if (listen(server_fd, BACKLOG) < 0) { + perror("listen failed"); + exit(EXIT_FAILURE); + } + + std::cout << "Server started, listening on port " << port << std::endl; + + while(true) { + // 接受客户端连接请求并处理 + if ((new_socket = accept(server_fd, (struct sockaddr *)&address, (socklen_t*)&addrlen)) < 0) { + perror("accept failed"); + exit(EXIT_FAILURE); + } + + std::cout << "New client connected: " << inet_ntoa(address.sin_addr) << ":" << ntohs(address.sin_port) << std::endl; + + // 处理客户端请求 + char buffer[1024] = {0}; + int valread = read(new_socket , buffer, 1024); + std::cout << "Received message: " << buffer << std::endl; + + const char* msg = "Hello from server!"; + send(new_socket, msg, strlen(msg), 0); + + // 关闭连接 + close(new_socket); + } +} \ No newline at end of file diff --git a/src-light-solver/network.h b/src-light-solver/network.h new file mode 100644 index 0000000..56efb3b --- /dev/null +++ b/src-light-solver/network.h @@ -0,0 +1,4 @@ + + + +void listen(int port); \ No newline at end of file diff --git a/src-light-solver/utils/paras.cpp b/src-light-solver/paras.cpp similarity index 85% rename from src-light-solver/utils/paras.cpp rename to src-light-solver/paras.cpp index 377cb9e..2b71c0e 100644 --- a/src-light-solver/utils/paras.cpp +++ b/src-light-solver/paras.cpp @@ -4,25 +4,25 @@ #include void paras::init_paras() { -#define PARA(N, T, D, L, H, C) \ +#define PARA(N, T, S, M, D, L, H, C) \ if (!strcmp(#T, "int")) map_int[#N] = D; \ else map_double[#N] = D; PARAS #undef PARA -#define STR_PARA(N, D, C) \ +#define STR_PARA(N, S, M, D, C) \ map_string[#N] = D; STR_PARAS #undef STR_PARA } void paras::sync_paras() { -#define PARA(N, T, D, L, H, C) \ +#define PARA(N, T, S, M, D, L, H, C) \ if (!strcmp(#T, "int")) N = map_int[#N]; \ else N = map_double[#N]; PARAS #undef PARA -#define STR_PARA(N, D, C) \ +#define STR_PARA(N, S, M, D, C) \ N = map_string[#N]; STR_PARAS #undef STR_PARAs @@ -47,13 +47,13 @@ void paras::print_change() { printf("c %-20s\t %-10s\t %-10s\t %-10s\t %s\n", "Name", "Type", "Now", "Default", "Comment"); -#define PARA(N, T, D, L, H, C) \ +#define PARA(N, T, S, M, D, L, H, C) \ if (map_int.count(#N)) printf("c %-20s\t %-10s\t %-10d\t %-10s\t %s\n", (#N), (#T), N, (#D), (C)); \ else printf("c %-20s\t %-10s\t %-10f\t %-10s\t %s\n", (#N), (#T), N, (#D), (C)); PARAS #undef PARA -#define STR_PARA(N, D, C) \ +#define STR_PARA(N, S, M, D, C) \ printf("c %-20s\t string\t\t %-10s\t %-10s\t %s\n", (#N), N.c_str(), (#D), (C)); STR_PARAS #undef STR_PARA diff --git a/src-light-solver/paras.hpp b/src-light-solver/paras.hpp new file mode 100644 index 0000000..8fc233f --- /dev/null +++ b/src-light-solver/paras.hpp @@ -0,0 +1,55 @@ +#ifndef _paras_hpp_INCLUDED +#define _paras_hpp_INCLUDED + +#include +#include + +// name, type, short-name,must-need, default ,low, high, comments +#define PARAS \ + PARA( DPS , int , '\0' , false , 0 , 0 , 1 , "DPS/NPS") \ + PARA( DPS_period , int , '\0' , false , 10000 , 1 , 1e8 , "DPS sharing period") \ + PARA( margin , int , '\0' , false , 0 , 0 , 1e3 , "DPS margin") \ + PARA( pakis , int , '\0' , false , 0 , 0 , 1 , "Use pakis diversity") \ + PARA( reset , int , '\0' , false , 0 , 0 , 1 , "Dynamically reseting") \ + PARA( reset_time , int , '\0' , false , 10 , 1 , 1e5 , "Reseting base interval (seconds)") \ + PARA( share , int , '\0' , false , 0 , 0 , 1 , "Sharing learnt clauses") \ + PARA( share_intv , int , '\0' , false , 500000, 0 , 1e9 , "Sharing interval (microseconds)") \ + PARA( share_lits , int , '\0' , false , 1500 , 0 , 1e6 , "Sharing lits (per every #share_intv seconds)") \ + PARA( shuffle , int , '\0' , false , 1 , 0 , 1 , "Use random shuffle") \ + PARA( simplify , int , '\0' , false , 1 , 0 , 1 , "Use Simplify (only preprocess)") \ + PARA( threads , int , '\0' , false , 32 , 1 , 128 , "Thread number") \ + PARA( times , double , '\0' , false , 5000 , 0 , 1e8 , "Cutoff time") + + +// name, short-name, must-need, default, comments +#define STR_PARAS \ + STR_PARA( config , '\0' , false , "" , "Config file") \ + STR_PARA( instance , 'i' , true , "" , "CNF format instance") + +struct paras +{ +#define PARA(N, T, S, M, D, L, H, C) \ + T N = D; + PARAS +#undef PARA + +#define STR_PARA(N, S, M, D, C) \ + std::string N = D; + STR_PARAS +#undef STR_PARA + + std::unordered_map map_int; + std::unordered_map map_double; + std::unordered_map map_string; + + void init_paras (); + void sync_paras (); + void print_change (); + void set_para (char *arg, int val); + void set_para (char *arg, double val); + void set_para (char *arg, char* val); +}; + +#define OPT(N) (opt->N) + +#endif \ No newline at end of file diff --git a/src-light-solver/solve.cpp b/src-light-solver/solve.cpp index 946a139..5c7edc4 100644 --- a/src-light-solver/solve.cpp +++ b/src-light-solver/solve.cpp @@ -1,6 +1,7 @@ #include "light.hpp" #include "workers/basekissat.hpp" #include "workers/sharer.hpp" +#include "paras.hpp" #include #include #include @@ -208,22 +209,4 @@ void print_model(vec &model) { printf(" %d", model[i]); } puts(" 0"); -} - -void solve(int argc, char **argv) { - light* S = new light(); - S->arg_parse(argc, argv); - int res = S->run(); - if (res == 10) { - printf("s SATISFIABLE\n"); - // print_model(model); - } - else if (res == 20) { - printf("s UNSATISFIABLE\n"); - } - else { - printf("s UNKNOWN\n"); - } - delete(S); - return; } \ No newline at end of file diff --git a/src-light-solver/solve.hpp b/src-light-solver/solve.hpp deleted file mode 100644 index e4fa8af..0000000 --- a/src-light-solver/solve.hpp +++ /dev/null @@ -1,3 +0,0 @@ -#include "light.hpp" - -void solve(int argc, char **argv); \ No newline at end of file diff --git a/src-light-solver/utils/paras.hpp b/src-light-solver/utils/paras.hpp deleted file mode 100644 index 5a63ca0..0000000 --- a/src-light-solver/utils/paras.hpp +++ /dev/null @@ -1,52 +0,0 @@ -#ifndef _paras_hpp_INCLUDED -#define _paras_hpp_INCLUDED - -#include -#include - -// name, type, default, low, high, comments -#define PARAS \ - PARA( DPS , int , 0 , 0 , 1 , "DPS/NPS") \ - PARA( DPS_period , int , 10000 , 1 , 1e8 , "DPS sharing period") \ - PARA( margin , int , 0 , 0 , 1e3 , "DPS margin") \ - PARA( pakis , int , 0 , 0 , 1 , "Use pakis diversity") \ - PARA( reset , int , 0 , 0 , 1 , "Dynamically reseting") \ - PARA( reset_time , int , 10 , 1 , 1e5 , "Reseting base interval (seconds)") \ - PARA( share , int , 0 , 0 , 1 , "Sharing learnt clauses") \ - PARA( share_intv , int , 500000, 0 , 1e9 , "Sharing interval (microseconds)") \ - PARA( share_lits , int , 1500 , 0 , 1e6 , "Sharing lits (per every #share_intv seconds)") \ - PARA( shuffle , int , 1 , 0 , 1 , "Use random shuffle") \ - PARA( simplify , int , 1 , 0 , 1 , "Use Simplify (only preprocess)") \ - PARA( threads , int , 32 , 1 , 128 , "Thread number") \ - PARA( times , double , 5000 , 0 , 1e8 , "Cutoff time") - -#define STR_PARAS \ - STR_PARA( config , "" , "Config file") - -struct paras -{ -#define PARA(N, T, D, L, H, C) \ - T N = D; - PARAS -#undef PARA - -#define STR_PARA(N, D, C) \ - std::string N = D; - STR_PARAS -#undef STR_PARA - - std::unordered_map map_int; - std::unordered_map map_double; - std::unordered_map map_string; - - void init_paras (); - void sync_paras (); - void print_change (); - void set_para (char *arg, int val); - void set_para (char *arg, double val); - void set_para (char *arg, char* val); -}; - -#define OPT(N) (opt->N) - -#endif \ No newline at end of file diff --git a/src-light-solver/workers/sharer.hpp b/src-light-solver/workers/sharer.hpp index 8c94da9..233864a 100644 --- a/src-light-solver/workers/sharer.hpp +++ b/src-light-solver/workers/sharer.hpp @@ -1,6 +1,6 @@ #ifndef _sharer_hpp_INCLUDED #define _sharer_hpp_INCLUDED -#include "../utils/paras.hpp" +#include "../paras.hpp" #include class basesolver;