parallel,UNSAT: assign from global to thread status

When we find UNSAT during sync, e.g. by receiving clauses, make
sure this status is propagated to the thread status as well, as
this is used to then terminate search with the proper status as
well.

Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>

Author: conp-solutions

minisat/parallel/ParSolver.cc

@@ -1317,7 +1317,7 @@ bool ParSolver::sync_evaluate_state_deterministic(size_t threadnr, bool caller_h
                    "if unassigned, no assumptions should available anymore");
             assert(data->partitionAssumptions.size() == 0 && "if unassigned, no assumptions should available anymore");
             // signal that the overall tree might now be UNSAT
-            notifyEvaluatePartitions.store(true);
+            // notifyEvaluatePartitions.store(true);
         }
     }
 
@@ -1464,7 +1464,14 @@ bool ParSolver::sync_deterministic(size_t threadnr, bool caller_has_solution)
 
     // TODO: refactor into separate method
     if (threadnr == 0) {
-        if (notifyEvaluatePartitions.load()) evaluatePartitionTree();
+        if (true) { /* (notifyEvaluatePartitions.load()) */
+            if (!evaluatePartitionTree()) {
+                std::cout << "c found UNSAT during evaluating partition tree" << std::endl;
+                assert(solved_current_call != 10);
+                solverData[threadnr]->_status = l_False; /* use thread 0 to propagate status */
+                solved_current_call.store(20);
+            }
+        }
         /* thread 0 asignes new partitions to threads with an UNSAT current partition */
         if (!assignPartitionAndTasks(threadnr)) {
             assert(false && "implement failure of assigning extra task");
@@ -1516,6 +1523,11 @@ bool ParSolver::sync_deterministic(size_t threadnr, bool caller_has_solution)
     /* If unsat here, formula is unsat, so all need to stop */
     if (solverData[threadnr]->_status == l_False) {
         solved_current_call.store(20);
+    } else if (solved_current_call.load() == 20) {
+        solverData[threadnr]->_status = l_False;
+        if (verbosity > 1)
+            std::cout << "c set thread " << threadnr << " status to " << solverData[threadnr]->_status
+                      << " based on global status " << solved_current_call << std::endl;
     }
 
     /* block on the barrier; needs to sync 'solved_current_call' from unsat partitions */