Wall-clock timeout

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);
 }
 

src/api/MainSolver.cc

@@ -23,8 +23,37 @@
 #include <tsolvers/RDLTHandler.h>
 #include <unsatcores/UnsatCoreBuilder.h>
 
+#include <condition_variable>
+#include <thread>
+
 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<Theory> th, std::unique_ptr<TermMapper> t
     initialize();
 }
 
+MainSolver::~MainSolver() = default;
+
 void MainSolver::initialize() {
+    timeLimitImplPtr = std::make_unique<TimeLimitImpl>(*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<SimpSMTSolver> 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<Theory> 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<PTRef const> MainSolver::Preprocessor::getPreprocessedFormulas() const {
     return {preprocessedFormulas.data(), static_cast<uint32_t>(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

src/api/MainSolver.h

@@ -19,6 +19,7 @@
 #include <smtsolvers/SimpSMTSolver.h>
 #include <unsatcores/UnsatCore.h>
 
+#include <chrono>
 #include <memory>
 
 namespace opensmt {
@@ -63,7 +64,7 @@ class MainSolver {
     MainSolver(std::unique_ptr<Theory> th, std::unique_ptr<TermMapper> tm, std::unique_ptr<THandler> thd,
                std::unique_ptr<SimpSMTSolver> 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<Theory> createTheory(Logic & logic, SMTConfig & config);
 
 protected:
@@ -324,6 +335,9 @@ class MainSolver {
     vec<PTRef> frameTerms;
     std::size_t firstNotSimplifiedFrame = 0;
     unsigned int insertedFormulasCount = 0;
+
+    class TimeLimitImpl;
+    std::unique_ptr<TimeLimitImpl> timeLimitImplPtr;
 };
 
 bool MainSolver::trackPartitions() const {

src/bin/opensmt.cc

@@ -33,6 +33,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #include <getopt.h>
 #include <iostream>
 #include <unistd.h>
+#include <string>
 
 #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<typename Enum>
@@ -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] <ms>          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;
 }
 

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";

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<int>(i)) {}
+      SMTOption(long long i)  : SMTOption(static_cast<long>(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 {