diff --git a/build.sh b/build.sh deleted file mode 100755 index 2d46fad..0000000 --- a/build.sh +++ /dev/null @@ -1,20 +0,0 @@ -#!/bin/bash - - -COMPILE_THREADS=16 - - -# build kissat - -# cd kissat-inc -# ./configure -# make -j $COMPILE_THREADS -# cd .. - -# build and copy light-solver - -make -C src-light-solver -j $COMPILE_THREADS - -# build and copy light-master - -make -C src-light-master -j $COMPILE_THREADS \ No newline at end of file diff --git a/src/distributed/leader.hpp b/src/distributed/leader.hpp index f212d08..f54b45d 100644 --- a/src/distributed/leader.hpp +++ b/src/distributed/leader.hpp @@ -79,6 +79,9 @@ void leader_main(light* S, int num_procs, int rank) { MPI_Request solved; MPI_Status status; MPI_Irecv(&is_sat, 1, MPI_INT, MPI_ANY_SOURCE, SOLVED_REPORT_TAG, MPI_COMM_WORLD, &solved); + int* sol; + + int res = 0; // waiting for results: while(true) { @@ -107,23 +110,43 @@ void leader_main(light* S, int num_procs, int rank) { // send signal for getting solution(model) when sat if(is_sat) { + res = 10; LOGGER->info("recived model size: %v", pre->vars); LOGGER->info("SAT!!!!!!"); MPI_Send(NULL, 0, MPI_INT, status.MPI_SOURCE, MODEL_REPORT_TAG, MPI_COMM_WORLD); - int* sol = new int[pre->vars]; + sol = new int[pre->vars]; MPI_Recv(sol, pre->vars, MPI_INT, status.MPI_SOURCE, MODEL_REPORT_TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE); - - for(int i=0; ivars; i++) { - printf("%d ", sol[i]); - } - printf("\n"); - - delete []sol; } else { + res = 20; LOGGER->info("UNSAT!!!!!!"); } break; } } + + MPI_Barrier(MPI_COMM_WORLD); + + if(res == 10) { + printf("s SAT\n"); + for(int i=0; ivars; i++) { + printf("%d ", sol[i]); + } + printf("\n"); + + for (int i = 1; i <= pre->orivars; i++) + if (pre->mapto[i]) pre->mapval[i] = (sol[abs(pre->mapto[i])-1] > 0 ? 1 : -1) * (pre->mapto[i] > 0 ? 1 : -1); + + pre->get_complete_model(); + for (int i = 1; i <= pre->orivars; i++) { + printf("%d ", i * pre->mapval[i]); + } + printf("\n"); + } else if(res == 20) { + printf("s UNSAT\n"); + } else { + printf("s UNKNOWN\n"); + } + + delete []sol; } \ No newline at end of file diff --git a/src/distributed/worker.hpp b/src/distributed/worker.hpp index c3161ef..08e2f16 100644 --- a/src/distributed/worker.hpp +++ b/src/distributed/worker.hpp @@ -97,4 +97,6 @@ void worker_main(light* S, int num_procs, int rank) { } delete(S); + + MPI_Barrier(MPI_COMM_WORLD); } \ No newline at end of file diff --git a/src/main.cpp b/src/main.cpp index dd26bc7..a94ba9e 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -26,7 +26,6 @@ int main(int argc, char **argv) { if(rank == 0) leader_main(S, num_procs, rank); else worker_main(S, num_procs, rank); - MPI_Barrier(MPI_COMM_WORLD); MPI_Finalize(); diff --git a/src/solve.cpp b/src/solve.cpp index 44d88a2..af5898b 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -198,17 +198,7 @@ int light::run() { parse_input(); if (OPT(share)) share(); int res = solve(); - - // if (res == 10 && OPT(simplify)) { - // for (int i = 1; i <= pre->orivars; i++) - // if (pre->mapto[i]) pre->mapval[i] = (model[abs(pre->mapto[i])-1] > 0 ? 1 : -1) * (pre->mapto[i] > 0 ? 1 : -1); - // pre->get_complete_model(); - // model.clear(); - // for (int i = 1; i <= pre->orivars; i++) { - // model.push(i * pre->mapval[i]); - // } - // } - + return res; } diff --git a/src/utils/easylogging++.cc b/src/utils/easylogging++.cpp similarity index 100% rename from src/utils/easylogging++.cc rename to src/utils/easylogging++.cpp