2023-03-26 19:15:17 +08:00
|
|
|
|
|
|
|
#include <chrono>
|
|
|
|
#include <thread>
|
|
|
|
#include <fstream>
|
2023-03-29 07:12:33 +00:00
|
|
|
#include <mpi.h>
|
2023-03-26 19:15:17 +08:00
|
|
|
|
2023-03-27 15:44:39 +08:00
|
|
|
#include "light.hpp"
|
2023-03-26 19:15:17 +08:00
|
|
|
#include "utils/cmdline.h"
|
2023-03-27 15:44:39 +08:00
|
|
|
#include "paras.hpp"
|
|
|
|
|
2023-03-29 07:12:33 +00:00
|
|
|
int main(int argc, char **argv) {
|
|
|
|
|
|
|
|
int num_procs, rank;
|
|
|
|
|
|
|
|
MPI_Init(&argc, &argv);
|
|
|
|
MPI_Comm_size(MPI_COMM_WORLD, &num_procs);
|
|
|
|
MPI_Comm_rank(MPI_COMM_WORLD, &rank);
|
|
|
|
|
|
|
|
printf("num_procs: %d, rank: %d\n", num_procs, rank);
|
|
|
|
|
|
|
|
return 0;
|
|
|
|
|
2023-03-27 15:44:39 +08:00
|
|
|
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);
|
2023-03-26 19:15:17 +08:00
|
|
|
|
2023-03-29 07:12:33 +00:00
|
|
|
MPI_Finalize();
|
|
|
|
|
2023-03-26 19:15:17 +08:00
|
|
|
return 0;
|
|
|
|
}
|