修改了OPT配置的实现，但存在BUG

.gitignore

@@ -3,4 +3,5 @@ build
 *.o
 myeasylog.log
 light
-exp-result*
+exp-result*
+experiment

bug.txt

@@ -0,0 +1,5 @@
+退出太慢了：
+3fb045f58aaf394165735c39c49fad92-linked_list_swap_contents_safety_unwind56.cnf
+
+预处理退出了：
+59e596f5f845a2487370950b37ec3db2-aws-encryption-sdk-c:aws_cryptosdk_enc_ctx_size.cnf

experiment/cal.py

@@ -12,7 +12,7 @@ from time import monotonic, sleep
 from tokenize import Number
 
 # global limit
-CUTOFF = 3600
+CUTOFF = 1000
 PUNISH = 2 #PAR2
 MEMS_MAX = 61440 # 60G
 
@@ -273,11 +273,14 @@ def gen_samples(dir):
 
 if __name__ == "__main__":
     solvers = []
-    solvers.append(solver_SAT_standard_gnomon("./result","light-cloud-circle"))
+    solvers.append(solver_SAT_standard_gnomon("./light-circle","light-circle"))
+    solvers.append(solver_SAT_standard_gnomon("./light-circle-unique","light-circle-unique"))
+    solvers.append(solver_SAT_standard_gnomon("./first_version","bug-cloud"))
     # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_sat/kissat-mab","origin-mab"))
     # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_simp/kissat-mab","preprocess-mab"))
     samples = []
-    samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "dump_sat"])
+    samples.append(["/pub/data/chenzh/data/sat2022/vbs.txt", "dump_sat"])
+    # samples.append(["./nohup.log", "dump_sat"])
     clt = calculater(solvers, samples)
     clt.cal_and_show()
 

experiment/run_solvers.sh

@@ -1,24 +0,0 @@
-#!/bin/bash
-
-instance="/pub/data/chenzh/data/sat2022"
-
-run_solver(){
-    solver=$1
-    res_solver_ins=$2
-    solver_args=$3
-        if [ ! -d "$res_solver_ins" ]; then
-                mkdir -p $res_solver_ins
-        fi
-        for dir_file in `cat $instance/all.txt`
-        do
-            file=$dir_file
-            echo "$res_solver_ins $file $solver_args"
-            touch $res_solver_ins/$file
-            { /usr/bin/time -f "\nreal\t%e\nuser\t%U\nsys\t%S\nmem\t%M\n" $solver $instance/$file $solver_args; } > $res_solver_ins/$file 2>&1
-        done
-}
-
-run_solver \
-		'mpirun -np 9 --allow-run-as-root ./light -i ' \
-        'exp-result'\
-        '--share=1 --threads=32 --times=3600'

experiment/run_solvers_seed_10.sh

@@ -1,24 +0,0 @@
-#!/bin/bash
-
-instance="/pub/data/chenzh/data/sat2022"
-
-run_solver(){
-    solver=$1
-    res_solver_ins=$2
-    solver_args=$3
-        if [ ! -d "$res_solver_ins" ]; then
-                mkdir -p $res_solver_ins
-        fi
-        for dir_file in `cat ./test.txt`
-        do
-            file=$dir_file
-            echo "$res_solver_ins $file $solver_args"
-            touch $res_solver_ins/$file
-            { /usr/bin/time -f "\nreal\t%e\nuser\t%U\nsys\t%S\nmem\t%M\n" $solver $instance/$file $solver_args; } > $res_solver_ins/$file 2>&1
-        done
-}
-
-run_solver \
-		'mpirun -np 9 --allow-run-as-root ./light -i ' \
-        'exp-result-seed10'\
-        '--share=1 --threads=32 --times=3600'

makefile

@@ -6,7 +6,7 @@ OBJECTS := $(addprefix build/,$(SOURCES:%=%.o))
 
 # 声明编译器和编译选项
 CXX := mpicxx
-CXXFLAGS := -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g
+CXXFLAGS := -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g 
 
 LIBS := -Wl,-Bstatic -lkissat -L kissat-inc/build -I kissat-inc/ \
 	    -lm4ri -L m4ri-20140914/.libs -I m4ri-20140914/ \

src/distributed/leader.hpp

@@ -15,13 +15,13 @@ void leader_main(light* S, int num_procs, int rank) {
 
     auto clk_st = std::chrono::high_resolution_clock::now();
 
-    S->opt->print_change();
+    __global_paras.print_change();
 
     printf("c [leader] preprocess(simplify) input data\n");
 
     // 进行化简    
     auto pre = new preprocess();
-    char *filename = const_cast<char*>(S->opt->instance.c_str());
+    char *filename = const_cast<char*>(OPT(instance).c_str());
     int start = pre->do_preprocess(filename);
 
     // 给每个 worker 发布是否启动计算流程的信息
@@ -82,7 +82,7 @@ void leader_main(light* S, int num_procs, int rank) {
         // 检测时间是否超限
         auto clk_now = std::chrono::high_resolution_clock::now();
         int solve_time = std::chrono::duration_cast<std::chrono::seconds>(clk_now - clk_st).count();
-        if (solve_time >= S->opt->times) {
+        if (solve_time >= OPT(times)) {
             printf("c [leader] solve time out\n");
             break;
         }

src/distributed/worker.hpp

@@ -60,7 +60,7 @@ void worker_main(light* S, int num_procs, int rank) {
 
             auto clk_now = std::chrono::high_resolution_clock::now();
             int solve_time = std::chrono::duration_cast<std::chrono::seconds>(clk_now - clk_st).count();
-            if (solve_time >= S->opt->times) {
+            if (solve_time >= OPT(times)) {
                 printf("c [worker%d] solve time out\n", rank);
                 break;
             }

src/light.cpp

@@ -12,8 +12,8 @@ light::light():
   winner_id             (-1),
   maxtime               (5000)
 {
-    opt = new paras();
+    // opt = new paras();
-    opt->init_paras();
+    //opt->init_paras();
 }
 
 light::~light() {
@@ -21,48 +21,48 @@ light::~light() {
     workers.clear(true);
 }
 
-void light::configure_from_file(const char* file) {
+// void light::configure_from_file(const char* file) {
-    if (!strcmp(file, "")) {
+//     if (!strcmp(file, "")) {
-        configure_name = new vec<char*>[OPT(threads)];
+//         configure_name = new vec<char*>[OPT(threads)];
-        configure_val = new vec<double>[OPT(threads)];
+//         configure_val = new vec<double>[OPT(threads)];
-        return;
+//         return;
-    }
+//     }
-    printf("c Get configure file: %s\n", file);
+//     printf("c Get configure file: %s\n", file);
-    std::ifstream fin(file);
+//     std::ifstream fin(file);
-    char buf[1000];
+//     char buf[1000];
-    fin.getline(buf, 1000);
+//     fin.getline(buf, 1000);
-    char *p = buf + 6;
+//     char *p = buf + 6;
-    int ws, ss, id = 0;
+//     int ws, ss, id = 0;
-    p = read_int(p, &ws);
+//     p = read_int(p, &ws);
-    p = read_int(p, &ss);
+//     p = read_int(p, &ss);
-    printf("%d %d\n", ws, ss);
+//     printf("%d %d\n", ws, ss);
-    opt->set_para("threads", ws);
+//     opt->set_para("threads", ws);
-    configure_name = new vec<char*>[ws];
+//     configure_name = new vec<char*>[ws];
-    configure_val = new vec<double>[ws];
+//     configure_val = new vec<double>[ws];
-    while (fin.getline(buf, 1000)) {
+//     while (fin.getline(buf, 1000)) {
-        p = strtok(buf, " ");
+//         p = strtok(buf, " ");
-        printf("%s\n", p);
+//         printf("%s\n", p);
-        solver_type.push(0);
+//         solver_type.push(0);
-        while (p) {
+//         while (p) {
-            p = strtok(NULL, " ");
+//             p = strtok(NULL, " ");
-            printf("%s\n", p);
+//             printf("%s\n", p);
-            if (!p) break;
+//             if (!p) break;
-            int l = strlen(p), pos = 0;
+//             int l = strlen(p), pos = 0;
-            for (int i = 1; i < l; i++)
+//             for (int i = 1; i < l; i++)
-                if (p[i] == '=') pos = i;
+//                 if (p[i] == '=') pos = i;
-            char *name = new char[pos];
+//             char *name = new char[pos];
-            strncpy(name, p, pos);
+//             strncpy(name, p, pos);
-            printf("%s\n", name);
+//             printf("%s\n", name);
-            configure_name[id].push(name);
+//             configure_name[id].push(name);
-            char *val = p + pos + 1;
+//             char *val = p + pos + 1;
-            double v = atof(val);
+//             double v = atof(val);
-            printf("%.2lf\n", v);
+//             printf("%.2lf\n", v);
-            configure_val[id].push(v);
+//             configure_val[id].push(v);
-        }
+//         }
-        printf("out\n");
+//         printf("out\n");
-        id++;
+//         id++;
-    }
+//     }
-}
+// }
 
 void light::arg_parse(int argc, char **argv) {
     cmdline::parser parser;
@@ -95,6 +95,4 @@ void light::arg_parse(int argc, char **argv) {
     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());
 }

src/light.hpp

@@ -36,7 +36,7 @@ struct light
 public:
     light();
     ~light();
-    paras *opt;
+    // paras *opt;
     preprocess *pre;
     vec<int> solver_type;
     vec<basesolver *> workers;
@@ -73,7 +73,6 @@ public:
         return winner_period;
     }
     void arg_parse(int argc, char **argv);
-    void configure_from_file(const char* file);
     void init_workers();
     void diversity_workers();
     void parse_input();
@@ -82,6 +81,7 @@ public:
     int  solve();
     void terminate_workers();
     void print_model();
+    
 };
 
 #endif

src/paras.cpp

@@ -2,46 +2,9 @@
 #include <cstdio>
 #include <iostream>
 #include <string>
+
+paras __global_paras;
  
-void paras::init_paras() {
-#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, S, M, D, C) \
-    map_string[#N] = D; 
-    STR_PARAS 
-#undef STR_PARA
-}
-
-void paras::sync_paras() {
-#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, S, M, D, C) \
-    N = map_string[#N];
-    STR_PARAS 
-#undef STR_PARAs
-}
-
-
-void paras::set_para(char *name, int val) {
-    map_int[name] = val;
-}
-
-void paras::set_para(char *name, double val) {
-    map_double[name] = val;
-}
-
-void paras::set_para(char *name, char* val) {
-    map_string[name] = val;
-}
-
-
 void paras::print_change() {
     printf("c ------------------- Paras list -------------------\n");
     printf("c %-20s\t %-10s\t %-10s\t %-10s\t %s\n",
@@ -59,4 +22,4 @@ void paras::print_change() {
 #undef STR_PARA
 
     printf("c --------------------------------------------------\n");
-}
+}

src/paras.hpp

@@ -43,15 +43,11 @@ struct paras
     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)
+extern paras __global_paras;
+
+#define OPT(N) (__global_paras.N)
 
 #endif

src/solve.cpp

@@ -29,7 +29,7 @@ void * solve_worker(void *arg) {
    basesolver * sq = (basesolver *)arg;
    while (!terminated) {
         int res = sq->solve();
-        if (sq->controller->opt->DPS) {
+        if (OPT(DPS)) {
             //printf("c %d solved, res is %d\n", sq->id, res);
             if (res) {
                 terminated = 1;

src/workers/basekissat.cpp

@@ -101,13 +101,13 @@ basekissat::basekissat(int id, light* light) : basesolver(id, light) {
     solver -> cbkImportClause = NULL;
     solver -> cbkExportClause = NULL;
     solver -> cbk_start_new_period  = NULL;
-    if (light->opt->share) {
+    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                   = light->opt->DPS;
+        solver -> dps                   = OPT(DPS);
-        solver -> dps_period            = light->opt->DPS_period;
+        solver -> dps_period            = OPT(DPS_period);
     }
 }
 

src/workers/sharer.cpp

@@ -16,12 +16,12 @@ std::vector<std::pair<MPI_Request*, int*>> send_data_struct;
 MPI_Request receive_request;
 int buf[BUF_SIZE];
 
-int num_received_clauses_by_network = 0;
+// int num_received_clauses_by_network = 0;
-int num_skip_clauses_by_network = 0;
+// int num_skip_clauses_by_network = 0;
 
-// 记录子句是否已经导入过
+// // 记录子句是否已经导入过
 
-std::unordered_map<int, bool> clause_imported;
+// std::unordered_map<int, bool> clause_imported;
 
 void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_store>> &cls) {
 
@@ -99,7 +99,7 @@ bool receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &claus
         from = buf[index++];
 
         while(index < count) {
-            num_received_clauses_by_network++;
+            //num_received_clauses_by_network++;
 
             shared_ptr<clause_store> cl = std::make_shared<clause_store>(buf[index++]);
 
@@ -108,11 +108,11 @@ bool receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &claus
                 cl->data[i] = buf[index++];
             }
 
-            if(clause_imported[cl->hash_code()]) {
+            // if(clause_imported[cl->hash_code()]) {
 
-                num_skip_clauses_by_network++;
+            //     num_skip_clauses_by_network++;
-                continue;
+            //     continue;
-            }
+            // }
 
             clauses.push_back(cl);
         }
@@ -138,9 +138,9 @@ void sharer::clause_sharing_init() {
 
 void sharer::clause_sharing_end() {
     printf("c sharing nums: %d\nc sharing time: %.2lf\n", nums, share_time);
-    printf("c sharing received_num_by_network: %d\n", num_received_clauses_by_network);
+    // printf("c sharing received_num_by_network: %d\n", num_received_clauses_by_network);
-    printf("c sharing skip_num_by_network: %d\n", num_skip_clauses_by_network);
+    // printf("c sharing skip_num_by_network: %d\n", num_skip_clauses_by_network);
-    printf("c sharing unique reduce percentage: %.2f%%\n", (double) num_skip_clauses_by_network / num_received_clauses_by_network * 100);
+    // printf("c sharing unique reduce percentage: %.2f%%\n", (double) num_skip_clauses_by_network / num_received_clauses_by_network * 100);
 }
 
 void sharer::do_clause_sharing() {
@@ -163,9 +163,9 @@ void sharer::do_clause_sharing() {
             consumers[j]->import_clauses_from(clauses);
         }
 
-        for (int k = 0; k < clauses.size(); k++) {
+        // for (int k = 0; k < clauses.size(); k++) {
-            clause_imported[clauses[k]->hash_code()] = true;
+        //     clause_imported[clauses[k]->hash_code()] = true;
-        }
+        // }
 
         // 传递外部网络传输的子句给下个节点
         share_clauses_to_next_node(from, clauses);
@@ -177,14 +177,14 @@ void sharer::do_clause_sharing() {
         producers[i]->export_clauses_to(cls);
 
         // 删除掉重复的学习子句
-        int t_size = cls.size();
+        // int t_size = cls.size();
-        for(int i=0; i<t_size; i++) {
+        // for(int i=0; i<t_size; i++) {
-            if(clause_imported[cls[i]->hash_code()]) {
+        //     if(clause_imported[cls[i]->hash_code()]) {
-                std::swap(cls[i], cls[t_size-1]);
+        //         std::swap(cls[i], cls[t_size-1]);
-                t_size--;
+        //         t_size--;
-            }
+        //     }
-        }
+        // }
-        cls.resize(t_size);
+        // cls.resize(t_size);
 
         //分享当前节点产生的子句
         if(cls.size() > 0) share_clauses_to_next_node(rank, cls);
@@ -205,9 +205,9 @@ void sharer::do_clause_sharing() {
             if (producers[i]->id == consumers[j]->id) continue;
             consumers[j]->import_clauses_from(cls);
         }
-        for (int k = 0; k < cls.size(); k++) {
+        // for (int k = 0; k < cls.size(); k++) {
-            clause_imported[cls[k]->hash_code()] = true;
+        //     clause_imported[cls[k]->hash_code()] = true;
-        }
+        // }
     }
 
     auto clk_ed = std::chrono::high_resolution_clock::now();