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..58420308d 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -23,8 +23,37 @@ #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; + + // 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{}; + 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 +85,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 +100,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 +455,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 +634,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(); + waitToEnd(); +} + +void MainSolver::TimeLimitImpl::setLimit(std::chrono::milliseconds limit) { + assert(limit > std::chrono::milliseconds::zero()); + + // Override already running thread + if (isRunning()) { + requestEnd(); + waitToEnd(); + } + + 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) { + 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/bin/opensmt.cc b/src/bin/opensmt.cc index 1809de3f8..361fc3ff6 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) { @@ -306,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)); @@ -321,8 +333,19 @@ 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; + 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.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..a3b28d4f9 100644 --- a/src/options/SMTConfig.h +++ b/src/options/SMTConfig.h @@ -146,6 +146,9 @@ 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(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; } @@ -323,11 +326,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; @@ -953,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; 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..95d39249f --- /dev/null +++ b/test/unit/test_Timeout.cc @@ -0,0 +1,819 @@ +/* + * 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; + + char const * auxMsg = "ok"; + + void init() { + for (size_t i = 0; i < nSolvers; ++i) { + auto & config = configs[i]; + auto & logic = logics[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"); + 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(std::size_t solverIdx, bool useConfig = false) { + setTimeLimit(solverIdx, small_limit_ms, useConfig); + } + + void setLargeTimeLimit(std::size_t solverIdx, bool useConfig = false) { + setTimeLimit(solverIdx, large_limit_ms, useConfig); + } + + void setSmallTimeLimitAll(bool useConfig = false) { + for (size_t i = 0; i < nSolvers; ++i) { + setSmallTimeLimit(i, useConfig); + } + } + + void setLargeTimeLimitAll(bool useConfig = false) { + for (size_t i = 0; i < nSolvers; ++i) { + setLargeTimeLimit(i, useConfig); + } + } + + std::array joinAll() { + std::array results; + for (size_t i = 0; i < nSolvers; ++i) { + results[i] = join(i); + } + return results; + } + + std::array configs{SMTConfig{}, SMTConfig{}}; + std::array logics{Logic_t::QF_LRA, Logic_t::QF_LRA}; + 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(); + threads[idx] = std::thread{std::move(task)}; + } + + void solveOnBackground(size_t idx) { + runOnBackground(idx, [this, idx] { return solverPtrs[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(0); + solveAllOnBackground(); + waitReadyAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_PreSmallTimeout) { + init(); + + setSmallTimeLimit(0); + 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(0); + 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(0); + 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(0); + 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(0); + 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(0); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_False, s_False})); +} + +TEST_F(TimeoutTest, test_PostSmallTimeout) { + init(); + + solveAllOnBackground(); + waitReadyAll(); + setSmallTimeLimit(0); + 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(0); + 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(0); + 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(0); + 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(0); + 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(0); + 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(0); + 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(0); + 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(0); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +TEST_F(TimeoutTest, test_PreLargeThenAllPostLargeTimeout) { + init(); + + setLargeTimeLimit(0); + 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(0); + 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(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})); +} + +TEST_F(TimeoutTest, test_PreSmallThenAllPostSmallTimeout) { + init(); + + 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 + setSmallTimeLimitAll(); + reqContinue(); + auto results = joinAll(); + + ASSERT_EQ(results, std::to_array({s_Undef, s_Undef})); +} + +} // namespace opensmt