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

优化参数的表达方式

Browse Source
This commit is contained in:
YuhangQ 2023-03-27 15:44:39 +08:00
parent c620e058c6
commit 7320c729b0
13 changed files with 187 additions and 100 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
.vscode/settings.json vendored
View File

@ -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"
}
}

4
src-light-master/master.cpp
View File

@ -6,5 +6,9 @@ int main() {
printf("=====================================\n");
return 0;
}

35
src-light-solver/light.cpp
View File

@ -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<std::string>("inst", 'i', "CNF format instance", true, "");
#define STR_PARA(N, S, M, D, C) \
parser.add<std::string>(#N, S, C, M, D);
STR_PARAS
#undef STR_PARA
#define PARA(N, T, D, L, H, C) \
if (!strcmp(#T, "int")) parser.add<int>(#N, '\0', C, false, D, cmdline::range((int)L, (int)H)); \
else parser.add<double>(#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<int>(#N, S, C, M, D, cmdline::range((int)L, (int)H)); \
else parser.add<double>(#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<std::string>("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<std::string>(#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<int>(#N); \
else OPT(N) = parser.get<double>(#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());
}

8
src-light-solver/light.hpp
View File

@ -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 <atomic>
#include <iostream>
#include <boost/thread.hpp>
@ -32,13 +34,13 @@ struct light
public:
light();
~light();
char *filename;
paras *opt;
preprocess *pre;
vec<int> solver_type;
vec<basesolver *> workers;
vec<sharer *> sharers;
char* filename;
vec<char*> *configure_name;
vec<double> *configure_val;

24
src-light-solver/main.cpp
View File

@ -3,10 +3,28 @@
#include <thread>
#include <fstream>
#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;
}

60
src-light-solver/network.cpp Normal file
View File

@ -0,0 +1,60 @@
#include <iostream>
#include <sys/socket.h>
#include <netinet/in.h>
#include <arpa/inet.h>
#include <unistd.h>
#include <cstring>
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);
}
}

4
src-light-solver/network.h Normal file
View File

@ -0,0 +1,4 @@
void listen(int port);

12
src-light-solver/utils/paras.cpp → src-light-solver/paras.cpp
View File

@ -4,25 +4,25 @@
#include <string>
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

55
src-light-solver/paras.hpp Normal file
View File

@ -0,0 +1,55 @@
#ifndef _paras_hpp_INCLUDED
#define _paras_hpp_INCLUDED
#include <cstring>
#include <unordered_map>
// 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<std::string, int> map_int;
std::unordered_map<std::string, double> map_double;
std::unordered_map<std::string, char*> 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

19
src-light-solver/solve.cpp
View File

@ -1,6 +1,7 @@
#include "light.hpp"
#include "workers/basekissat.hpp"
#include "workers/sharer.hpp"
#include "paras.hpp"
#include <unistd.h>
#include <chrono>
#include <algorithm>
@ -208,22 +209,4 @@ void print_model(vec<int> &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;
}

3
src-light-solver/solve.hpp
View File

@ -1,3 +0,0 @@
#include "light.hpp"
void solve(int argc, char **argv);

52
src-light-solver/utils/paras.hpp
View File

@ -1,52 +0,0 @@
#ifndef _paras_hpp_INCLUDED
#define _paras_hpp_INCLUDED
#include <cstring>
#include <unordered_map>
// 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<std::string, int> map_int;
std::unordered_map<std::string, double> map_double;
std::unordered_map<std::string, char*> 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

2
src-light-solver/workers/sharer.hpp
View File

@ -1,6 +1,6 @@
#ifndef _sharer_hpp_INCLUDED
#define _sharer_hpp_INCLUDED
#include "../utils/paras.hpp"
#include "../paras.hpp"
#include <boost/thread.hpp>
class basesolver;