Pullrequest

.gitignore

@@ -0,0 +1 @@
+build/*

src/trusted/main_check.c

@@ -12,9 +12,11 @@ int main(int argc, char *argv[]) {
 
     const char *fifo_directives = "", *fifo_feedback = "";
     bool check_model = false, lenient = false;
+    u64 num_solvers = 0;
     for (int i = 1; i < argc; i++) {
         trusted_utils_try_match_arg(argv[i], "-fifo-directives=", &fifo_directives);
         trusted_utils_try_match_arg(argv[i], "-fifo-feedback=", &fifo_feedback);
+        trusted_utils_try_match_num(argv[i], "-num-solvers=", &num_solvers);
         trusted_utils_try_match_flag(argv[i], "-check-model", &check_model);
         trusted_utils_try_match_flag(argv[i], "-lenient", &lenient);
     }
@@ -25,7 +27,7 @@ int main(int argc, char *argv[]) {
     writer_init(output_path);
 #endif
 
-    tc_init(fifo_directives, fifo_feedback);
+    tc_init(fifo_directives, fifo_feedback, num_solvers);
     int res = tc_run(check_model, lenient);
     fflush(stdout);
     return res;

src/trusted/trusted_checker.c

@@ -25,6 +25,7 @@ FILE* input; // named pipe
 FILE* output; // named pipe
 int nb_vars; // # variables in formula
 signature formula_sig; // formula signature
+u64 nb_solvers; // number of solvers
 
 bool do_logging = true;
 
@@ -55,13 +56,14 @@ void read_hints(int nb_hints) {
     trusted_utils_read_uls(buf_hints->data, nb_hints, input);
 }
 
-void tc_init(const char* fifo_in, const char* fifo_out) {
+void tc_init(const char* fifo_in, const char* fifo_out, u64 num_solvers) {
     input = fopen(fifo_in, "r");
     if (!input) trusted_utils_exit_eof();
     output = fopen(fifo_out, "w");
     if (!output) trusted_utils_exit_eof();
     buf_lits = int_vec_init(1 << 14);
     buf_hints = u64_vec_init(1 << 14);
+    nb_solvers = num_solvers;
 }
 
 void tc_end() {
@@ -182,7 +184,7 @@ int tc_run(bool check_model, bool lenient) {
     }
 
     float elapsed = (float) (clock() - start) / CLOCKS_PER_SEC;
-    snprintf(trusted_utils_msgstr, 512, "cpu:%.3f prod:%lu imp:%lu del:%lu", elapsed, nb_produced, nb_imported, nb_deleted);
+    snprintf(trusted_utils_msgstr, 512, "cpu:%.3f prod:%lu imp:%lu del:%lu n_s:%lu", elapsed, nb_produced, nb_imported, nb_deleted, nb_solvers);
     trusted_utils_log(trusted_utils_msgstr);
 
     return 0;

src/trusted/trusted_checker.h

@@ -3,6 +3,6 @@
 
 #include <stdbool.h>
 
-void tc_init(const char* fifo_in, const char* fifo_out);
+void tc_init(const char* fifo_in, const char* fifo_out, unsigned long num_solvers);
 void tc_end();
 int tc_run(bool check_model, bool lenient);

src/trusted/trusted_utils.c

@@ -36,9 +36,16 @@ bool begins_with(const char* str, const char* prefix) {
         i++;
     }
 }
+
 void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** out) {
-    if (begins_with(arg, opt)) *out = arg+strlen(opt);
+    if (begins_with(arg, opt)) *out = arg + strlen(opt);
+}
+
+void trusted_utils_try_match_num(const char* arg, const char* opt, u64* out) {
+    const char* start_of_number = arg + strlen(opt);
+    if (begins_with(arg, opt)) *out = strtol(start_of_number, NULL, 10);
 }
+
 void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out) {
     if (begins_with(arg, opt)) *out = true;
 }

src/trusted/trusted_utils.h

@@ -35,6 +35,7 @@ void trusted_utils_log_err(const char* msg);
 void trusted_utils_exit_eof();
 
 void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** out);
+void trusted_utils_try_match_num(const char* arg, const char* opt, u64* out);
 void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out);
 
 void trusted_utils_copy_bytes(u8* to, const u8* from, u64 nb_bytes);