From 206872d902c5ccb12e08e6231a59246af3ad53b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Sun, 20 Jul 2025 19:52:21 +0200 Subject: [PATCH 1/6] Implemented timeout set via API or smt2 file --- src/api/Interpret.cc | 10 +++- src/api/MainSolver.cc | 101 +++++++++++++++++++++++++++++++++++++++ src/api/MainSolver.h | 16 ++++++- src/options/SMTConfig.cc | 8 ++++ src/options/SMTConfig.h | 5 ++ 5 files changed, 138 insertions(+), 2 deletions(-) diff --git a/src/api/Interpret.cc b/src/api/Interpret.cc index c46549922..bd49cbaa6 100644 --- a/src/api/Interpret.cc +++ b/src/api/Interpret.cc @@ -107,8 +107,16 @@ void Interpret::setOption(ASTNode& n) { SMTOption value(n); const char* msg = "ok"; bool rval = config.setOption(name, value, msg); - if (rval == false) + if (rval == false) { notify_formatted(true, "set-option failed for %s: %s", name, msg); + } else if (main_solver) { + const SMTOption& stored_value = config.getOption(name); + assert(not stored_value.isEmpty()); + + if (strcmp(name, SMTConfig::o_time_limit) == 0) { + main_solver->setTimeLimit(std::chrono::milliseconds{stored_value.getValue().numval}); + } + } free(name); } diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 781602091..b668117da 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -23,8 +23,36 @@ #include #include +#include +#include + namespace opensmt { +class MainSolver::TimeLimitImpl { +public: + TimeLimitImpl(MainSolver & s) : solver(s) {} + ~TimeLimitImpl(); + + void setLimit(std::chrono::milliseconds); + void setLimitIfNotRunning(std::chrono::milliseconds); + +protected: + bool isRunning() const noexcept; + + void requestEnd(); + void waitToEnd(); + +private: + MainSolver & solver; + + std::jthread thread{}; + + // See https://en.cppreference.com/w/cpp/thread/condition_variable.html + std::mutex mtx{}; + std::condition_variable condVar{}; + bool endReq{false}; +}; + MainSolver::MainSolver(Logic & logic, SMTConfig & conf, std::string name) : theory(createTheory(logic, conf)), term_mapper(new TermMapper(logic)), @@ -56,7 +84,11 @@ MainSolver::MainSolver(std::unique_ptr th, std::unique_ptr t initialize(); } +MainSolver::~MainSolver() = default; + void MainSolver::initialize() { + timeLimitImplPtr = std::make_unique(*this); + frames.push(); frameTerms.push(logic.getTerm_true()); preprocessor.initialize(); @@ -67,6 +99,11 @@ void MainSolver::initialize() { smt_solver->addOriginalSMTClause({~term_mapper->getOrCreateLit(logic.getTerm_false())}, iorefs); if (iorefs.first != CRef_Undef) { pmanager.addClauseClassMask(iorefs.first, 1); } + + if (auto option = config.getOption(SMTConfig::o_time_limit); not option.isEmpty()) { + assert(option.getValue().type == O_NUM); + timeLimitImplPtr->setLimit(std::chrono::milliseconds{option.getValue().numval}); + } } void MainSolver::push() { @@ -417,6 +454,18 @@ std::unique_ptr MainSolver::createInnerSolver(SMTConfig & config, } } +void MainSolver::setTimeLimit(std::chrono::milliseconds limit, TimeLimitConf const & conf) { + if (limit <= std::chrono::milliseconds::zero()) { + throw std::invalid_argument{"MainSolver::setTimeLimit: The value must be positive."}; + } + + if (conf.override) { + timeLimitImplPtr->setLimit(limit); + } else { + timeLimitImplPtr->setLimitIfNotRunning(limit); + } +} + std::unique_ptr MainSolver::createTheory(Logic & logic, SMTConfig & config) { Logic_t logicType = logic.getLogic(); Theory * theory = nullptr; @@ -584,4 +633,56 @@ void MainSolver::Preprocessor::addPreprocessedFormula(PTRef fla) { span MainSolver::Preprocessor::getPreprocessedFormulas() const { return {preprocessedFormulas.data(), static_cast(preprocessedFormulas.size())}; } + +MainSolver::TimeLimitImpl::~TimeLimitImpl() { + if (not isRunning()) { return; } + + requestEnd(); + // no need to wait in destructor (thanks to std::jthread) +} + +void MainSolver::TimeLimitImpl::setLimit(std::chrono::milliseconds limit) { + assert(limit > std::chrono::milliseconds::zero()); + + // Override already running thread + if (isRunning()) { + requestEnd(); + waitToEnd(); + } + + thread = std::jthread([this, limit] { + std::unique_lock lock(mtx); + // Abort if a further future end request has already been sent + if (endReq) { return; } + // Releases the lock and suspends the thread, waiting on a notification or timeout + // Notification must be sent *after* the wait, otherwise could be missed - hence checking `endReq` above + if (condVar.wait_for(lock, limit) == std::cv_status::timeout) { solver.notifyStop(); } + }); +} + +void MainSolver::TimeLimitImpl::setLimitIfNotRunning(std::chrono::milliseconds limit) { + if (isRunning()) { return; } + setLimit(limit); +} + +bool MainSolver::TimeLimitImpl::isRunning() const noexcept { + return thread.joinable(); +} + +void MainSolver::TimeLimitImpl::requestEnd() { + assert(isRunning()); + { + std::lock_guard lock(mtx); + endReq = true; + } + condVar.notify_all(); + assert(isRunning()); +} + +void MainSolver::TimeLimitImpl::waitToEnd() { + assert(isRunning()); + thread.join(); + endReq = false; + assert(not isRunning()); +} } // namespace opensmt diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index 8cc3fc2ed..b296fbc76 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -19,6 +19,7 @@ #include #include +#include #include namespace opensmt { @@ -63,7 +64,7 @@ class MainSolver { MainSolver(std::unique_ptr th, std::unique_ptr tm, std::unique_ptr thd, std::unique_ptr ss, Logic & logic, SMTConfig & conf, std::string name); - virtual ~MainSolver() = default; + virtual ~MainSolver(); MainSolver(MainSolver const &) = delete; MainSolver & operator=(MainSolver const &) = delete; MainSolver(MainSolver &&) = default; @@ -149,6 +150,16 @@ class MainSolver { // For stopping at the global scope, refer to GlobalStop.h void notifyStop() { smt_solver->notifyStop(); } + // Set wall-clock time limit for the solver in miliseconds + // When it expires, the solving is terminated gracefully and unknown is returned + // Overrides previously set and still running limit + void setTimeLimit(std::chrono::milliseconds limit) { setTimeLimit(limit, {}); } + struct TimeLimitConf { + // override by default, otherwise do not set the limit + bool override = true; + }; + void setTimeLimit(std::chrono::milliseconds, TimeLimitConf const &); + static std::unique_ptr createTheory(Logic & logic, SMTConfig & config); protected: @@ -324,6 +335,9 @@ class MainSolver { vec frameTerms; std::size_t firstNotSimplifiedFrame = 0; unsigned int insertedFormulasCount = 0; + + class TimeLimitImpl; + std::unique_ptr timeLimitImplPtr; }; bool MainSolver::trackPartitions() const { diff --git a/src/options/SMTConfig.cc b/src/options/SMTConfig.cc index df63494dd..3a5c6ca88 100644 --- a/src/options/SMTConfig.cc +++ b/src/options/SMTConfig.cc @@ -414,6 +414,12 @@ namespace opensmt { strcmp(val, spts_search_counter) != 0) { msg = s_err_unknown_units; return false; } } + + if (strcmp(name, o_time_limit) == 0) { + if (value.getValue().type != O_NUM) { msg = s_err_not_num; return false; } + if (value.getValue().numval <= 0) { msg = s_err_not_positive; return false; } + } + if (optionTable.has(name)) optionTable.remove(name); insertOption(name, new SMTOption(value)); @@ -528,6 +534,7 @@ namespace opensmt { const char* SMTConfig::o_sat_picky_w = ":picky_w"; const char* SMTConfig::o_global_declarations = ":global-declarations"; const char* SMTConfig::o_sat_split_mode = ":split-mode"; + const char* SMTConfig::o_time_limit = ":time-limit"; char* SMTConfig::server_host=NULL; uint16_t SMTConfig::server_port = 0; @@ -538,6 +545,7 @@ namespace opensmt { const char* SMTConfig::s_err_not_str = "expected string"; const char* SMTConfig::s_err_not_bool = "expected Boolean"; const char* SMTConfig::s_err_not_num = "expected number"; + const char* SMTConfig::s_err_not_positive = "expected positive value"; const char* SMTConfig::s_err_seed_zero = "seed cannot be 0"; const char* SMTConfig::s_err_unknown_split = "unknown split type"; const char* SMTConfig::s_err_unknown_units = "unknown split units"; diff --git a/src/options/SMTConfig.h b/src/options/SMTConfig.h index 59b4c1cb3..c4d3035e2 100644 --- a/src/options/SMTConfig.h +++ b/src/options/SMTConfig.h @@ -323,11 +323,16 @@ namespace opensmt { static const char* o_global_declarations; static const char* o_sat_split_mode; + + // Wall-clock time limit for the solver in miliseconds + // MainSolver implicitly sets the limit *only* when initializing! + static const char* o_time_limit; private: static const char* s_err_not_str; static const char* s_err_not_bool; static const char* s_err_not_num; + static const char* s_err_not_positive; static const char* s_err_seed_zero; static const char* s_err_unknown_split; static const char* s_err_unknown_units; From 16ffa9073554eee12909a62232c9b12ec0255426 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Tue, 21 Oct 2025 16:50:10 +0200 Subject: [PATCH 2/6] Unit tests on time limits --- test/unit/CMakeLists.txt | 8 + test/unit/test_Timeout.cc | 509 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 517 insertions(+) create mode 100644 test/unit/test_Timeout.cc diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index b580291a5..63833cf0d 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -251,3 +251,11 @@ target_sources(StopTest target_link_libraries(StopTest OpenSMT gtest gtest_main) gtest_add_tests(TARGET StopTest) + +add_executable(TimeoutTest) +target_sources(TimeoutTest + PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/test_Timeout.cc" + ) + +target_link_libraries(TimeoutTest OpenSMT gtest gtest_main) +gtest_add_tests(TARGET TimeoutTest) diff --git a/test/unit/test_Timeout.cc b/test/unit/test_Timeout.cc new file mode 100644 index 000000000..d90e778d6 --- /dev/null +++ b/test/unit/test_Timeout.cc @@ -0,0 +1,509 @@ +/* + * Copyright (c) 2025, Kolarik Tomas + * + * SPDX-License-Identifier: MIT + * + */ + +// Builds on "test_Stop.cc" + +#include + +#include +#include + +#include +#include +#include +#include +#include +#include + +// Pre-timeout checks if setting the time limit prior to solving works as expected +// Post-timeout checks if setting the time limit during solving works as expected + +// Small pre-timeouts followed by large post-timeouts are unstable - we cannot anticipate preprocessing time +// These cases work only if the machine is fast enough - unusable for CI of user machines +// #define FAST_MACHINE + +namespace opensmt { + +std::mutex mutex; +std::condition_variable condVar; +size_t ackReadyCnt{0}; +bool reqContinueFlag{false}; + +constexpr std::chrono::milliseconds computation_time_ms{50}; +// Must be large enough to at least allow setting another consecutive time limit +constexpr std::chrono::milliseconds small_limit_ms{5}; +// Must be large enough +constexpr std::chrono::milliseconds large_limit_ms{10000}; + +// Ensure that the computation takes more than small_limit_ms but less than large_limit_ms +static_assert(computation_time_ms >= small_limit_ms * 5); +static_assert(computation_time_ms * 10 <= large_limit_ms); + +class TestMainSolver : public MainSolver { +public: + using MainSolver::MainSolver; + +protected: + sstat solve_(vec const & enabledFrames) override { + std::unique_lock lock(mutex); + ++ackReadyCnt; + lock.unlock(); + condVar.notify_all(); + lock.lock(); + condVar.wait(lock, [] { return reqContinueFlag; }); + lock.unlock(); + + std::this_thread::sleep_for(computation_time_ms); + + return MainSolver::solve_(enabledFrames); + } +}; + +class TimeoutTest : public ::testing::Test { +public: + + ~TimeoutTest() { + ackReadyCnt = 0; + reqContinueFlag = false; + } +protected: + static constexpr size_t nSolvers = 2; + + void init() { + for (size_t i = 0; i < nSolvers; ++i) { + auto & logic = logics[i]; + auto & solver = solvers[i]; + + PTRef x = logic.mkRealVar("x"); + PTRef y = logic.mkRealVar("y"); + PTRef z = logic.mkRealVar("z"); + PTRef w = logic.mkRealVar("w"); + PTRef v = logic.mkRealVar("v"); + + // This at least ensures that it is not solved just during the preprocessing phase + + solver.addAssertion(logic.mkOr(logic.mkEq(x, y), logic.mkEq(x, z))); + solver.addAssertion(logic.mkOr(logic.mkEq(y, w), logic.mkEq(y, v))); + solver.addAssertion(logic.mkOr(logic.mkEq(z, w), logic.mkEq(z, v))); + + solver.addAssertion(logic.mkLt(x, w)); + solver.addAssertion(logic.mkLt(x, v)); + } + } + + void solveAllOnBackground() { + for (size_t i = 0; i < nSolvers; ++i) { + solveOnBackground(i); + } + } + + void waitReadyAll() { + std::unique_lock lock(mutex); + condVar.wait(lock, [] { return ackReadyCnt == nSolvers; }); + } + + void reqContinue() { + { + std::lock_guard lock(mutex); + reqContinueFlag = true; + } + condVar.notify_all(); + } + + void setSmallTimeLimit(TestMainSolver & solver) { + solver.setTimeLimit(small_limit_ms); + } + + void setLargeTimeLimit(TestMainSolver & solver) { + solver.setTimeLimit(large_limit_ms); + } + + void setSmallTimeLimitAll() { + for (size_t i = 0; i < nSolvers; ++i) { + setSmallTimeLimit(solvers[i]); + } + } + + void setLargeTimeLimitAll() { + for (size_t i = 0; i < nSolvers; ++i) { + setLargeTimeLimit(solvers[i]); + } + } + + std::array joinAll() { + std::array results; + for (size_t i = 0; i < nSolvers; ++i) { + results[i] = join(i); + } + return results; + } + + SMTConfig config{}; + std::array logics{Logic_t::QF_LRA, Logic_t::QF_LRA}; + std::array solvers{TestMainSolver{logics[0], config, "solver 1"}, + TestMainSolver{logics[1], config, "solver 2"}}; + + std::array threads; + std::array, nSolvers> futures; + +private: + void runOnBackground(size_t idx, auto f) { + std::packaged_task task{std::move(f)}; + futures[idx] = task.get_future(); + threads[idx] = std::thread{std::move(task)}; + } + + void solveOnBackground(size_t idx) { + runOnBackground(idx, [this, idx] { return solvers[idx].check(); }); + } + + sstat join(size_t idx) { + threads[idx].join(); + return futures[idx].get(); + } +}; + +TEST_F(TimeoutTest, test_NoTimeout) { + init(); + + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_PreLargeTimeout) { + init(); + + setLargeTimeLimit(solvers.front()); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_PreSmallTimeout) { + init(); + + setSmallTimeLimit(solvers.front()); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreLargeTimeout) { + init(); + + setLargeTimeLimitAll(); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreSmallTimeout) { + init(); + + setSmallTimeLimitAll(); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_AllPreLargeThenOnePreLargeTimeout) { + init(); + + // also tests overriding already existing time limit thread + setLargeTimeLimitAll(); + setLargeTimeLimit(solvers.front()); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreLargeThenOnePreSmallTimeout) { + init(); + + // also tests overriding already existing time limit thread + setLargeTimeLimitAll(); + setSmallTimeLimit(solvers.front()); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreSmallThenOnePreLargeTimeout) { + init(); + + // also tests overriding already existing time limit thread + setSmallTimeLimitAll(); + setLargeTimeLimit(solvers.front()); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_Undef})); +} + +TEST_F(TimeoutTest, test_AllPreSmallThenOnePreSmallTimeout) { + init(); + + // also tests overriding already existing time limit thread + setSmallTimeLimitAll(); + setSmallTimeLimit(solvers.front()); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +// Post-timeouts at least ensure the functionality of returning unknown after the solving is already trigerred + +TEST_F(TimeoutTest, test_PostLargeTimeout) { + init(); + + solveAllOnBackground(); + waitReadyAll(); + setLargeTimeLimit(solvers.front()); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_PostSmallTimeout) { + init(); + + solveAllOnBackground(); + waitReadyAll(); + setSmallTimeLimit(solvers.front()); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_False})); +} + +TEST_F(TimeoutTest, test_AllPostLargeTimeout) { + init(); + + solveAllOnBackground(); + waitReadyAll(); + setLargeTimeLimitAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_AllPostSmallTimeout) { + init(); + + solveAllOnBackground(); + waitReadyAll(); + setSmallTimeLimitAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_AllPostLargeThenOnePostLargeTimeout) { + init(); + + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setLargeTimeLimitAll(); + setLargeTimeLimit(solvers.front()); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_AllPostLargeThenOnePostSmallTimeout) { + init(); + + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setLargeTimeLimitAll(); + setSmallTimeLimit(solvers.front()); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_False})); +} + +TEST_F(TimeoutTest, test_AllPostSmallThenOnePostLargeTimeout) { + init(); + + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setSmallTimeLimitAll(); + setLargeTimeLimit(solvers.front()); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_Undef})); +} + +TEST_F(TimeoutTest, test_AllPostSmallThenOnePostSmallTimeout) { + init(); + + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setSmallTimeLimitAll(); + setSmallTimeLimit(solvers.front()); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +// Combinations of pre- and post-timeouts + +TEST_F(TimeoutTest, test_AllPreLargeThenOnePostLargeTimeout) { + init(); + + setLargeTimeLimitAll(); + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setLargeTimeLimit(solvers.front()); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreLargeThenOnePostSmallTimeout) { + init(); + + setLargeTimeLimitAll(); + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setSmallTimeLimit(solvers.front()); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_False})); +} + +#ifdef FAST_MACHINE +TEST_F(TimeoutTest, test_AllPreSmallThenOnePostLargeTimeout) { + init(); + + setSmallTimeLimitAll(); + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setLargeTimeLimit(solvers.front()); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_Undef})); +} +#endif + +TEST_F(TimeoutTest, test_AllPreSmallThenOnePostSmallTimeout) { + init(); + + setSmallTimeLimitAll(); + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setSmallTimeLimit(solvers.front()); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_PreLargeThenAllPostLargeTimeout) { + init(); + + setLargeTimeLimit(solvers.front()); + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setLargeTimeLimitAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +#ifdef FAST_MACHINE +TEST_F(TimeoutTest, test_PreSmallThenAllPostLargeTimeout) { + init(); + + setSmallTimeLimit(solvers.front()); + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setLargeTimeLimitAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} +#endif + +TEST_F(TimeoutTest, test_PreLargeThenAllPostSmallTimeout) { + init(); + + setLargeTimeLimit(solvers.front()); + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setSmallTimeLimitAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_PreSmallThenAllPostSmallTimeout) { + init(); + + setSmallTimeLimit(solvers.front()); + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setSmallTimeLimitAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +} // namespace opensmt From ecaa6d4a00ce880bc728d0a3fa4ef20a4d828c0a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Mon, 21 Jul 2025 16:04:38 +0200 Subject: [PATCH 3/6] Implemented timeout set via command line --- src/bin/opensmt.cc | 35 +++++++++++++++++++++++++++++++---- src/options/SMTConfig.h | 2 ++ 2 files changed, 33 insertions(+), 4 deletions(-) diff --git a/src/bin/opensmt.cc b/src/bin/opensmt.cc index 1809de3f8..d7475f415 100644 --- a/src/bin/opensmt.cc +++ b/src/bin/opensmt.cc @@ -33,6 +33,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include #include #include +#include #define opensmt_error_() { std::cerr << "# Error (triggered at " << __FILE__ << ", " << __LINE__ << ")" << std::endl; assert(false); ::exit( 1 ); } #define opensmt_error( S ) { std::cerr << "; Error: " << S << " (triggered at " << __FILE__ << ", " << __LINE__ << ")" << std::endl; ::exit( 1 ); } @@ -49,7 +50,11 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. namespace opensmt { -inline bool pipeExecution = false; +using namespace std::string_literals; + +namespace { + bool pipeExecution = false; +} // Replace this with std::to_underlying once we move to C++23 template @@ -72,7 +77,7 @@ void interpretInteractive(Interpret & interpret); } int main( int argc, char * argv[] ) -{ +try { using namespace opensmt; signal( SIGTERM, catcher ); @@ -131,6 +136,10 @@ int main( int argc, char * argv[] ) return exit_status; } +catch (std::exception const & e) { + std::cerr << "Terminated with exception:\n" << e.what() << std::endl; + return 1; +} namespace opensmt { @@ -237,6 +246,7 @@ void printHelp() " --minimal-unsat-cores produced unsat cores must be irreducible\n" " --print-cores-full produced unsat cores are agnostic to the smt2 attribute ':named'\n" " --produce-interpolants [-i] enables interpolant computation\n" + " --time-limit [-t] sets wall-clock time limit in milliseconds\n" " --pipe [-p] for execution within a pipe\n"; std::cerr << help_string; } @@ -269,14 +279,16 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] ) {"minimal-unsat-cores", no_argument, &selectedLongOpt, to_underlying(LongOpt::minUcore)}, {"print-cores-full", no_argument, &selectedLongOpt, to_underlying(LongOpt::fullUcore)}, {"produce-interpolants", no_argument, nullptr, 'i'}, + {"time-limit", required_argument, nullptr, 't'}, {"pipe", no_argument, nullptr, 'p'}, {0, 0, 0, 0} }; const char* msg; - while (true) { + bool ok = true; + while (ok) { int option_index = 0; - int c = getopt_long(argc, argv, "r:hdivp", long_options, &option_index); + int c = getopt_long(argc, argv, "r:hdivpt:", long_options, &option_index); if (c == -1) { break; } switch (c) { @@ -323,6 +335,17 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] ) case 'i': res.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); break; + case 't': { + int64_t timeLimit; + try { + timeLimit = std::stoll(optarg); + } catch (std::logic_error const & e) { + throw std::invalid_argument{"Invalid argument of time-limit: "s + e.what()}; + } + + ok &= res.setOption(SMTConfig::o_time_limit, SMTOption(timeLimit), msg); + break; + } case 'p': pipeExecution = true; break; @@ -332,6 +355,10 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] ) } } + if (not ok) { + throw std::invalid_argument{"Invalid command-line argument: "s + msg}; + } + return res; } diff --git a/src/options/SMTConfig.h b/src/options/SMTConfig.h index c4d3035e2..7ff2c6be1 100644 --- a/src/options/SMTConfig.h +++ b/src/options/SMTConfig.h @@ -146,6 +146,8 @@ namespace opensmt { SMTOption(ASTNode const & n); SMTOption() {} SMTOption(int i) : value(i) {} + //+ Should also support long representation + SMTOption(long i) : SMTOption(static_cast(i)) {} SMTOption(double i): value(i) {} SMTOption(const char* s) : value(s) {} inline bool isEmpty() const { return value.type == O_EMPTY; } From dea6bbc3f18f4e322cb009ae494fa3609465bc86 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Mon, 4 Aug 2025 18:29:04 +0200 Subject: [PATCH 4/6] Used std::thread instead of std::jthread which is not supported in MacOS --- src/api/MainSolver.cc | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index b668117da..58420308d 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -45,7 +45,8 @@ class MainSolver::TimeLimitImpl { private: MainSolver & solver; - std::jthread thread{}; + // not using std::jthread since MacOS does not support it + std::thread thread{}; // See https://en.cppreference.com/w/cpp/thread/condition_variable.html std::mutex mtx{}; @@ -638,7 +639,7 @@ MainSolver::TimeLimitImpl::~TimeLimitImpl() { if (not isRunning()) { return; } requestEnd(); - // no need to wait in destructor (thanks to std::jthread) + waitToEnd(); } void MainSolver::TimeLimitImpl::setLimit(std::chrono::milliseconds limit) { @@ -650,14 +651,14 @@ void MainSolver::TimeLimitImpl::setLimit(std::chrono::milliseconds limit) { waitToEnd(); } - thread = std::jthread([this, limit] { + thread = decltype(thread){[this, limit] { std::unique_lock lock(mtx); // Abort if a further future end request has already been sent if (endReq) { return; } // Releases the lock and suspends the thread, waiting on a notification or timeout // Notification must be sent *after* the wait, otherwise could be missed - hence checking `endReq` above if (condVar.wait_for(lock, limit) == std::cv_status::timeout) { solver.notifyStop(); } - }); + }}; } void MainSolver::TimeLimitImpl::setLimitIfNotRunning(std::chrono::milliseconds limit) { From ad8891ace5388354b5a07d60b6a076d50d935a65 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Mon, 4 Aug 2025 18:38:15 +0200 Subject: [PATCH 5/6] Preferring brace initialization of SMTOption-s and avoiding narrowing conversions --- src/bin/opensmt.cc | 10 +++++----- src/options/SMTConfig.h | 3 ++- src/parallel/opensmtSplitter.cc | 6 +++--- src/unsatcores/UnsatCoreBuilder.cc | 2 +- 4 files changed, 11 insertions(+), 10 deletions(-) diff --git a/src/bin/opensmt.cc b/src/bin/opensmt.cc index d7475f415..361fc3ff6 100644 --- a/src/bin/opensmt.cc +++ b/src/bin/opensmt.cc @@ -318,13 +318,13 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] ) printHelp(); exit(0); case 'v': - res.setOption(SMTConfig::o_verbosity, SMTOption(true), msg); + res.setOption(SMTConfig::o_verbosity, SMTOption{true}, msg); break; case 'd': - res.setOption(SMTConfig::o_dryrun, SMTOption(true), msg); + res.setOption(SMTConfig::o_dryrun, SMTOption{true}, msg); break; case 'r': - if (!res.setOption(SMTConfig::o_random_seed, SMTOption(atoi(optarg)), msg)) + if (!res.setOption(SMTConfig::o_random_seed, SMTOption{atoi(optarg)}, msg)) fprintf(stderr, "Error setting random seed: %s\n", msg); else fprintf(stderr, "; Using random seed %d\n", atoi(optarg)); @@ -333,7 +333,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] ) res.setOption(SMTConfig::o_produce_models, SMTOption(true), msg); break; case 'i': - res.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); + res.setOption(SMTConfig::o_produce_inter, SMTOption{true}, msg); break; case 't': { int64_t timeLimit; @@ -343,7 +343,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] ) throw std::invalid_argument{"Invalid argument of time-limit: "s + e.what()}; } - ok &= res.setOption(SMTConfig::o_time_limit, SMTOption(timeLimit), msg); + ok &= res.setOption(SMTConfig::o_time_limit, SMTOption{timeLimit}, msg); break; } case 'p': diff --git a/src/options/SMTConfig.h b/src/options/SMTConfig.h index 7ff2c6be1..a3b28d4f9 100644 --- a/src/options/SMTConfig.h +++ b/src/options/SMTConfig.h @@ -148,6 +148,7 @@ namespace opensmt { SMTOption(int i) : value(i) {} //+ Should also support long representation SMTOption(long i) : SMTOption(static_cast(i)) {} + SMTOption(long long i) : SMTOption(static_cast(i)) {} SMTOption(double i): value(i) {} SMTOption(const char* s) : value(s) {} inline bool isEmpty() const { return value.type == O_EMPTY; } @@ -960,7 +961,7 @@ namespace opensmt { void setSimplifyInterpolant(int val) { const char* msg; - setOption(o_simplify_inter, SMTOption(val), msg); + setOption(o_simplify_inter, SMTOption{val}, msg); } int getSimplifyInterpolant() const { diff --git a/src/parallel/opensmtSplitter.cc b/src/parallel/opensmtSplitter.cc index f920ba898..6fca95986 100644 --- a/src/parallel/opensmtSplitter.cc +++ b/src/parallel/opensmtSplitter.cc @@ -80,16 +80,16 @@ int main( int argc, char * argv[] ) break; case 'd': const char* msg; - c.setOption(SMTConfig::o_dryrun, SMTOption(true), msg); + c.setOption(SMTConfig::o_dryrun, SMTOption{true}, msg); break; case 'r': - if (!c.setOption(SMTConfig::o_random_seed, SMTOption(atoi(optarg)), msg)) + if (!c.setOption(SMTConfig::o_random_seed, SMTOption{atoi(optarg)}, msg)) fprintf(stderr, "Error setting random seed: %s\n", msg); else fprintf(stderr, "; Using random seed %d\n", atoi(optarg)); break; case 'i': - c.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); + c.setOption(SMTConfig::o_produce_inter, SMTOption{true}, msg); break; case 'p': pipe = true; diff --git a/src/unsatcores/UnsatCoreBuilder.cc b/src/unsatcores/UnsatCoreBuilder.cc index c8655b887..a18a05491 100644 --- a/src/unsatcores/UnsatCoreBuilder.cc +++ b/src/unsatcores/UnsatCoreBuilder.cc @@ -157,7 +157,7 @@ SMTConfig UnsatCoreBuilder::Minimize::makeSmtSolverConfig() const { assert(not newConfig.produce_inter()); char const * msg = "ok"; - newConfig.setOption(SMTConfig::o_produce_models, SMTOption(false), msg); + newConfig.setOption(SMTConfig::o_produce_models, SMTOption{false}, msg); assert(not newConfig.produce_models()); return newConfig; From 41da79d042efede3d710b4e9b022641e9f0382b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Tue, 4 Nov 2025 10:43:20 +0100 Subject: [PATCH 6/6] Unit tests on time limits when set via SMTConfig --- test/unit/test_Timeout.cc | 378 ++++++++++++++++++++++++++++++++++---- 1 file changed, 344 insertions(+), 34 deletions(-) diff --git a/test/unit/test_Timeout.cc b/test/unit/test_Timeout.cc index d90e778d6..95d39249f 100644 --- a/test/unit/test_Timeout.cc +++ b/test/unit/test_Timeout.cc @@ -65,18 +65,25 @@ class TestMainSolver : public MainSolver { class TimeoutTest : public ::testing::Test { public: - ~TimeoutTest() { ackReadyCnt = 0; reqContinueFlag = false; } + protected: static constexpr size_t nSolvers = 2; + char const * auxMsg = "ok"; + void init() { for (size_t i = 0; i < nSolvers; ++i) { + auto & config = configs[i]; auto & logic = logics[i]; - auto & solver = solvers[i]; + + auto & solverPtr = solverPtrs[i]; + std::string name = "solver " + std::to_string(i); + solverPtr = std::make_unique(logic, config, name.c_str()); + auto & solver = *solverPtr; PTRef x = logic.mkRealVar("x"); PTRef y = logic.mkRealVar("y"); @@ -114,23 +121,23 @@ class TimeoutTest : public ::testing::Test { condVar.notify_all(); } - void setSmallTimeLimit(TestMainSolver & solver) { - solver.setTimeLimit(small_limit_ms); + void setSmallTimeLimit(std::size_t solverIdx, bool useConfig = false) { + setTimeLimit(solverIdx, small_limit_ms, useConfig); } - void setLargeTimeLimit(TestMainSolver & solver) { - solver.setTimeLimit(large_limit_ms); + void setLargeTimeLimit(std::size_t solverIdx, bool useConfig = false) { + setTimeLimit(solverIdx, large_limit_ms, useConfig); } - void setSmallTimeLimitAll() { + void setSmallTimeLimitAll(bool useConfig = false) { for (size_t i = 0; i < nSolvers; ++i) { - setSmallTimeLimit(solvers[i]); + setSmallTimeLimit(i, useConfig); } } - void setLargeTimeLimitAll() { + void setLargeTimeLimitAll(bool useConfig = false) { for (size_t i = 0; i < nSolvers; ++i) { - setLargeTimeLimit(solvers[i]); + setLargeTimeLimit(i, useConfig); } } @@ -142,15 +149,26 @@ class TimeoutTest : public ::testing::Test { return results; } - SMTConfig config{}; + std::array configs{SMTConfig{}, SMTConfig{}}; std::array logics{Logic_t::QF_LRA, Logic_t::QF_LRA}; - std::array solvers{TestMainSolver{logics[0], config, "solver 1"}, - TestMainSolver{logics[1], config, "solver 2"}}; + std::array, nSolvers> solverPtrs{}; std::array threads; std::array, nSolvers> futures; private: + void setTimeLimit(std::size_t solverIdx, std::chrono::milliseconds limit_ms, bool useConfig = false) { + if (not useConfig) { + TestMainSolver & solver = *solverPtrs[solverIdx]; + solver.setTimeLimit(limit_ms); + } else { + auto & config = configs[solverIdx]; + [[maybe_unused]] + bool rval = config.setOption(SMTConfig::o_time_limit, SMTOption(limit_ms.count()), auxMsg); + assert(rval); + } + } + void runOnBackground(size_t idx, auto f) { std::packaged_task task{std::move(f)}; futures[idx] = task.get_future(); @@ -158,7 +176,7 @@ class TimeoutTest : public ::testing::Test { } void solveOnBackground(size_t idx) { - runOnBackground(idx, [this, idx] { return solvers[idx].check(); }); + runOnBackground(idx, [this, idx] { return solverPtrs[idx]->check(); }); } sstat join(size_t idx) { @@ -181,7 +199,7 @@ TEST_F(TimeoutTest, test_NoTimeout) { TEST_F(TimeoutTest, test_PreLargeTimeout) { init(); - setLargeTimeLimit(solvers.front()); + setLargeTimeLimit(0); solveAllOnBackground(); waitReadyAll(); reqContinue(); @@ -193,7 +211,7 @@ TEST_F(TimeoutTest, test_PreLargeTimeout) { TEST_F(TimeoutTest, test_PreSmallTimeout) { init(); - setSmallTimeLimit(solvers.front()); + setSmallTimeLimit(0); solveAllOnBackground(); waitReadyAll(); reqContinue(); @@ -231,7 +249,7 @@ TEST_F(TimeoutTest, test_AllPreLargeThenOnePreLargeTimeout) { // also tests overriding already existing time limit thread setLargeTimeLimitAll(); - setLargeTimeLimit(solvers.front()); + setLargeTimeLimit(0); solveAllOnBackground(); waitReadyAll(); reqContinue(); @@ -245,7 +263,7 @@ TEST_F(TimeoutTest, test_AllPreLargeThenOnePreSmallTimeout) { // also tests overriding already existing time limit thread setLargeTimeLimitAll(); - setSmallTimeLimit(solvers.front()); + setSmallTimeLimit(0); solveAllOnBackground(); waitReadyAll(); reqContinue(); @@ -259,7 +277,7 @@ TEST_F(TimeoutTest, test_AllPreSmallThenOnePreLargeTimeout) { // also tests overriding already existing time limit thread setSmallTimeLimitAll(); - setLargeTimeLimit(solvers.front()); + setLargeTimeLimit(0); solveAllOnBackground(); waitReadyAll(); reqContinue(); @@ -273,7 +291,7 @@ TEST_F(TimeoutTest, test_AllPreSmallThenOnePreSmallTimeout) { // also tests overriding already existing time limit thread setSmallTimeLimitAll(); - setSmallTimeLimit(solvers.front()); + setSmallTimeLimit(0); solveAllOnBackground(); waitReadyAll(); reqContinue(); @@ -289,7 +307,7 @@ TEST_F(TimeoutTest, test_PostLargeTimeout) { solveAllOnBackground(); waitReadyAll(); - setLargeTimeLimit(solvers.front()); + setLargeTimeLimit(0); reqContinue(); auto results = joinAll(); @@ -301,7 +319,7 @@ TEST_F(TimeoutTest, test_PostSmallTimeout) { solveAllOnBackground(); waitReadyAll(); - setSmallTimeLimit(solvers.front()); + setSmallTimeLimit(0); reqContinue(); auto results = joinAll(); @@ -339,7 +357,7 @@ TEST_F(TimeoutTest, test_AllPostLargeThenOnePostLargeTimeout) { waitReadyAll(); // also tests overriding already existing time limit thread setLargeTimeLimitAll(); - setLargeTimeLimit(solvers.front()); + setLargeTimeLimit(0); reqContinue(); auto results = joinAll(); @@ -353,7 +371,7 @@ TEST_F(TimeoutTest, test_AllPostLargeThenOnePostSmallTimeout) { waitReadyAll(); // also tests overriding already existing time limit thread setLargeTimeLimitAll(); - setSmallTimeLimit(solvers.front()); + setSmallTimeLimit(0); reqContinue(); auto results = joinAll(); @@ -367,7 +385,7 @@ TEST_F(TimeoutTest, test_AllPostSmallThenOnePostLargeTimeout) { waitReadyAll(); // also tests overriding already existing time limit thread setSmallTimeLimitAll(); - setLargeTimeLimit(solvers.front()); + setLargeTimeLimit(0); reqContinue(); auto results = joinAll(); @@ -381,7 +399,7 @@ TEST_F(TimeoutTest, test_AllPostSmallThenOnePostSmallTimeout) { waitReadyAll(); // also tests overriding already existing time limit thread setSmallTimeLimitAll(); - setSmallTimeLimit(solvers.front()); + setSmallTimeLimit(0); reqContinue(); auto results = joinAll(); @@ -397,7 +415,7 @@ TEST_F(TimeoutTest, test_AllPreLargeThenOnePostLargeTimeout) { solveAllOnBackground(); waitReadyAll(); // also tests overriding already existing time limit thread - setLargeTimeLimit(solvers.front()); + setLargeTimeLimit(0); reqContinue(); auto results = joinAll(); @@ -411,7 +429,7 @@ TEST_F(TimeoutTest, test_AllPreLargeThenOnePostSmallTimeout) { solveAllOnBackground(); waitReadyAll(); // also tests overriding already existing time limit thread - setSmallTimeLimit(solvers.front()); + setSmallTimeLimit(0); reqContinue(); auto results = joinAll(); @@ -426,7 +444,7 @@ TEST_F(TimeoutTest, test_AllPreSmallThenOnePostLargeTimeout) { solveAllOnBackground(); waitReadyAll(); // also tests overriding already existing time limit thread - setLargeTimeLimit(solvers.front()); + setLargeTimeLimit(0); reqContinue(); auto results = joinAll(); @@ -441,7 +459,7 @@ TEST_F(TimeoutTest, test_AllPreSmallThenOnePostSmallTimeout) { solveAllOnBackground(); waitReadyAll(); // also tests overriding already existing time limit thread - setSmallTimeLimit(solvers.front()); + setSmallTimeLimit(0); reqContinue(); auto results = joinAll(); @@ -451,7 +469,7 @@ TEST_F(TimeoutTest, test_AllPreSmallThenOnePostSmallTimeout) { TEST_F(TimeoutTest, test_PreLargeThenAllPostLargeTimeout) { init(); - setLargeTimeLimit(solvers.front()); + setLargeTimeLimit(0); solveAllOnBackground(); waitReadyAll(); // also tests overriding already existing time limit thread @@ -466,7 +484,7 @@ TEST_F(TimeoutTest, test_PreLargeThenAllPostLargeTimeout) { TEST_F(TimeoutTest, test_PreSmallThenAllPostLargeTimeout) { init(); - setSmallTimeLimit(solvers.front()); + setSmallTimeLimit(0); solveAllOnBackground(); waitReadyAll(); // also tests overriding already existing time limit thread @@ -481,7 +499,7 @@ TEST_F(TimeoutTest, test_PreSmallThenAllPostLargeTimeout) { TEST_F(TimeoutTest, test_PreLargeThenAllPostSmallTimeout) { init(); - setLargeTimeLimit(solvers.front()); + setLargeTimeLimit(0); solveAllOnBackground(); waitReadyAll(); // also tests overriding already existing time limit thread @@ -495,7 +513,299 @@ TEST_F(TimeoutTest, test_PreLargeThenAllPostSmallTimeout) { TEST_F(TimeoutTest, test_PreSmallThenAllPostSmallTimeout) { init(); - setSmallTimeLimit(solvers.front()); + setSmallTimeLimit(0); + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setSmallTimeLimitAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +// Now using SMTConfig which only makes sense when called even before init + +TEST_F(TimeoutTest, test_PreInitLargeTimeoutConfig) { + setLargeTimeLimit(0, true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_PreInitSmallTimeoutConfig) { + setSmallTimeLimit(0, true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreInitLargeTimeoutConfig) { + setLargeTimeLimitAll(true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreInitSmallTimeoutConfig) { + setSmallTimeLimitAll(true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_AllPreInitLargeThenOnePreInitLargeTimeoutConfig) { + setLargeTimeLimitAll(true); + setLargeTimeLimit(0, true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreInitLargeThenOnePreInitSmallTimeoutConfig) { + setLargeTimeLimitAll(true); + setSmallTimeLimit(0, true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreInitSmallThenOnePreInitLargeTimeoutConfig) { + setSmallTimeLimitAll(true); + setLargeTimeLimit(0, true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_Undef})); +} + +TEST_F(TimeoutTest, test_AllPreInitSmallThenOnePreInitSmallTimeoutConfig) { + setSmallTimeLimitAll(true); + setSmallTimeLimit(0, true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +// Combinations of preinit- and pre-/post-timeouts + +TEST_F(TimeoutTest, test_AllPreInitLargeThenOnePreLargeTimeoutConfig) { + setLargeTimeLimitAll(true); + + init(); + + // also tests overriding already existing time limit thread + setLargeTimeLimit(0); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreInitLargeThenOnePostLargeTimeoutConfig) { + setLargeTimeLimitAll(true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setLargeTimeLimit(0); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreInitLargeThenOnePreSmallTimeoutConfig) { + setLargeTimeLimitAll(true); + + init(); + + // also tests overriding already existing time limit thread + setSmallTimeLimit(0); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreInitLargeThenOnePostSmallTimeoutConfig) { + setLargeTimeLimitAll(true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setSmallTimeLimit(0); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_False})); +} + +TEST_F(TimeoutTest, test_AllPreInitSmallThenOnePreSmallTimeoutConfig) { + setSmallTimeLimitAll(true); + + init(); + + // also tests overriding already existing time limit thread + setSmallTimeLimit(0); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_AllPreInitSmallThenOnePostSmallTimeoutConfig) { + setSmallTimeLimitAll(true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setSmallTimeLimit(0); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_PreInitLargeThenAllPreLargeTimeoutConfig) { + setLargeTimeLimit(0, true); + + init(); + + // also tests overriding already existing time limit thread + setLargeTimeLimitAll(); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_PreInitLargeThenAllPostLargeTimeoutConfig) { + setLargeTimeLimit(0, true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setLargeTimeLimitAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_PreInitLargeThenAllPreSmallTimeoutConfig) { + setLargeTimeLimit(0, true); + + init(); + + // also tests overriding already existing time limit thread + setSmallTimeLimitAll(); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_PreInitLargeThenAllPostSmallTimeoutConfig) { + setLargeTimeLimit(0, true); + + init(); + + solveAllOnBackground(); + waitReadyAll(); + // also tests overriding already existing time limit thread + setSmallTimeLimitAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_PreInitSmallThenAllPreSmallTimeoutConfig) { + setSmallTimeLimit(0, true); + + init(); + + // also tests overriding already existing time limit thread + setSmallTimeLimitAll(); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_PreInitSmallThenAllPostSmallTimeoutConfig) { + setSmallTimeLimit(0, true); + + init(); + solveAllOnBackground(); waitReadyAll(); // also tests overriding already existing time limit thread