Unified stopping of solvers

Used dedicated functions at global and local scope to notify the stop.
Used the flags in okContinue() function (not used in ScatterSplitter though)

Author: Tomaqa

.clang-files

@@ -1,3 +1,5 @@
+./src/api/GlobalStop.cc
+./src/api/GlobalStop.h
 ./src/api/MainSolver.cc
 ./src/api/MainSolver.h
 ./src/api/Opensmt.cc

src/api/CMakeLists.txt

@@ -20,12 +20,14 @@ $<TARGET_OBJECTS:unsatcores>
 add_library(api OBJECT)
 
 set(PRIVATE_SOURCES_TO_ADD
+    "${CMAKE_CURRENT_SOURCE_DIR}/GlobalStop.cc"
     "${CMAKE_CURRENT_SOURCE_DIR}/MainSolver.cc"
     "${CMAKE_CURRENT_SOURCE_DIR}/PartitionManager.cc"
     "${CMAKE_CURRENT_SOURCE_DIR}/Interpret.cc"
 )
 
 set(PUBLIC_SOURCES_TO_ADD
+    "${CMAKE_CURRENT_SOURCE_DIR}/GlobalStop.h"
     "${CMAKE_CURRENT_SOURCE_DIR}/MainSolver.h"
     "${CMAKE_CURRENT_SOURCE_DIR}/PartitionManager.h"
     "${CMAKE_CURRENT_SOURCE_DIR}/smt2tokens.h"
@@ -99,6 +101,7 @@ endif()
 install(FILES
     Opensmt.h
     smt2tokens.h
+    GlobalStop.h
     MainSolver.h
     PartitionManager.h
     Interpret.h

src/api/GlobalStop.cc

@@ -0,0 +1,22 @@
+/*
+ *  Copyright (c) 2025, Tomas Kolarik <tomaqa@gmail.com>
+ *
+ *  SPDX-License-Identifier: MIT
+ *
+ */
+
+namespace opensmt {
+
+namespace {
+    bool globalStopFlag{false};
+}
+
+void notifyGlobalStop() {
+    globalStopFlag = true;
+}
+
+bool globallyStopped() {
+    return globalStopFlag;
+}
+
+} // namespace opensmt

src/api/GlobalStop.h

@@ -0,0 +1,15 @@
+/*
+ *  Copyright (c) 2025, Tomas Kolarik <tomaqa@gmail.com>
+ *
+ *  SPDX-License-Identifier: MIT
+ *
+ */
+
+namespace opensmt {
+
+// Notify all solvers in the application to stop
+void notifyGlobalStop();
+// Check if a global stop flag for all solvers has been triggered
+bool globallyStopped();
+
+} // namespace opensmt

src/api/MainSolver.cc

@@ -25,8 +25,6 @@
 
 namespace opensmt {
 
-bool stop;
-
 MainSolver::MainSolver(Logic & logic, SMTConfig & conf, std::string name)
     : theory(createTheory(logic, conf)),
       term_mapper(new TermMapper(logic)),

src/api/MainSolver.h

@@ -9,6 +9,7 @@
 #ifndef MAINSOLVER_H
 #define MAINSOLVER_H
 
+#include "GlobalStop.h"
 #include "PartitionManager.h"
 
 #include <cnfizers/Tseitin.h>
@@ -145,7 +146,9 @@ class MainSolver {
     }
     TermNames const & getTermNames() const { return termNames; }
 
-    void stop() { smt_solver->stop = true; }
+    // Notify this particular solver to stop the computation
+    // For stopping at the global scope, refer to GlobalStop.h
+    void notifyStop() { smt_solver->notifyStop(); }
 
     static std::unique_ptr<Theory> createTheory(Logic & logic, SMTConfig & config);
 

src/parallel/ScatterSplitter.cc

@@ -133,6 +133,8 @@ bool ScatterSplitter::excludeAssumptions(vec<Lit> && neg_constrs) {
 
 bool ScatterSplitter::okContinue() const {
 
+    // ignores SimpSMTSolver::okContinue and hence ignores stopped() and globallyStopped()
+
     if (splitContext.solverLimit() and splitContext.solverLimit() == search_counter and not config.sat_split_mode()) {
         return false;
     } else if (getChannel().shouldStop()) {

src/smtsolvers/CoreSMTSolver.cc

@@ -46,6 +46,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "CoreSMTSolver.h"
 
+#include <api/GlobalStop.h>
 #include <common/InternalException.h>
 #include <common/Random.h>
 #include <common/ReportUtils.h>
@@ -60,16 +61,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 namespace opensmt {
 
-extern bool stop;
-
 //=================================================================================================
 // Constructor/Destructor:
 
 CoreSMTSolver::CoreSMTSolver(SMTConfig & c, THandler& t )
     : config           (c)
     , theory_handler   (t)
     , verbosity        (c.verbosity())
-    , stop             (false)
     // Parameters: (formerly in 'SearchParams')
     , var_decay        (c.sat_var_decay())
     , clause_decay     (c.sat_clause_decay())
@@ -115,7 +113,6 @@ CoreSMTSolver::CoreSMTSolver(SMTConfig & c, THandler& t )
 #endif
     , conflict_budget       (-1)
     , propagation_budget    (-1)
-    , asynch_interrupt      (false)
     , learnt_t_lemmata      (0)
     , perm_learnt_t_lemmata (0)
     , luby_i                (0)
@@ -1346,7 +1343,7 @@ void CoreSMTSolver::popBacktrackPoint()
 
 bool CoreSMTSolver::okContinue() const
 {
-    return not opensmt::stop;
+    return not stopped() and not globallyStopped();
 }
 
 void CoreSMTSolver::learntSizeAdjust() {
@@ -1705,9 +1702,11 @@ lbool CoreSMTSolver::solve_()
 
     // Search:
 
-    if (config.dryrun())
-        stop = true;
-    while (status == l_Undef && okContinue() && !this->stop) {
+    if (config.dryrun()) {
+        notifyStop();
+    }
+
+    while (status == l_Undef && okContinue()) {
         // Print some information. At every restart for
         // standard mode or any 2^n intervarls for luby
         // restarts
@@ -1737,7 +1736,7 @@ lbool CoreSMTSolver::solve_()
             model[i] = value(i);
         }
     } else {
-        assert(not okContinue() || status == l_False || this->stop);
+        assert(not okContinue() || status == l_False);
     }
 
     // We terminate

src/smtsolvers/CoreSMTSolver.h

@@ -82,8 +82,8 @@ class CoreSMTSolver
     bool      verbosity;
     enum class ConsistencyAction { BacktrackToZero, ReturnUndef, SkipToSearchBegin, NoOp };
     int search_counter;
+    bool stopFlag{false};
 public:
-    bool stop = false;
 
     // Constructor/Destructor:
     //
@@ -92,9 +92,13 @@ class CoreSMTSolver
     void     initialize       ();
     void     clearSearch      ();  // Backtrack SAT solver and theories to decision level 0
 
+    void notifyStop() { stopFlag = true; }
+
     // Problem specification:
     //
 protected:
+    bool stopped() const { return stopFlag; }
+
     void  addVar_    (Var v); // Ensure that var v exists in the solver
     virtual Var newVar(bool dvar); // Add a new variable with parameters specifying variable mode.
 public:
@@ -150,8 +154,6 @@ class CoreSMTSolver
     void    setConfBudget(int64_t x);
     void    setPropBudget(int64_t x);
     void    budgetOff();
-    void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
-    void    clearInterrupt();     // Clear interrupt indicator flag.
 
     // Memory management:
     //
@@ -350,7 +352,6 @@ class CoreSMTSolver
     //
     int64_t             conflict_budget;    // -1 means no budget.
     int64_t             propagation_budget; // -1 means no budget.
-    bool                asynch_interrupt;
 
     // Main internal methods:
     //
@@ -706,12 +707,10 @@ inline void     CoreSMTSolver::setDecisionVar(Var v, bool b)
 }
 inline void     CoreSMTSolver::setConfBudget(int64_t x)                   { conflict_budget    = conflicts    + x; }
 inline void     CoreSMTSolver::setPropBudget(int64_t x)                   { propagation_budget = propagations + x; }
-inline void     CoreSMTSolver::interrupt()                                { asynch_interrupt = true; }
-inline void     CoreSMTSolver::clearInterrupt()                           { asynch_interrupt = false; }
 inline void     CoreSMTSolver::budgetOff()                                { conflict_budget = propagation_budget = -1; }
 inline bool     CoreSMTSolver::withinBudget() const
 {
-    return !asynch_interrupt &&
+    return !stopped() &&
            (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
            (propagation_budget < 0 || propagations < (uint64_t)propagation_budget);
 }

src/smtsolvers/LookaheadSMTSolver.cc

@@ -44,7 +44,7 @@ lbool LookaheadSMTSolver::solve_() {
             model[i] = value(i);
         }
     } else {
-        assert(not okContinue() || res == LALoopRes::unsat || this->stop);
+        assert(not okContinue() || res == LALoopRes::unsat);
     }
     switch (res) {
         case LALoopRes::unknown_final: