Implemented time-limit-per-query

Author: Tomaqa

src/api/MainSolver.cc

@@ -89,6 +89,7 @@ MainSolver::~MainSolver() = default;
 
 void MainSolver::initialize() {
     timeLimitImplPtr = std::make_unique<TimeLimitImpl>(*this);
+    timeLimitPerQueryImplPtr = std::make_unique<TimeLimitImpl>(*this);
 
     frames.push();
     frameTerms.push(logic.getTerm_true());
@@ -383,6 +384,11 @@ sstat MainSolver::check() {
         timeLimitImplPtr->setLimitIfNotRunning(std::chrono::milliseconds{option.getValue().numval});
     }
 
+    if (auto option = config.getOption(SMTConfig::o_time_limit_per_query); not option.isEmpty()) {
+        assert(option.getValue().type == O_NUM);
+        timeLimitPerQueryImplPtr->setLimit(std::chrono::milliseconds{option.getValue().numval});
+    }
+
     sstat rval = simplifyFormulas();
 
     if (config.dump_query()) printCurrentAssertionsAsQuery();

src/api/MainSolver.h

@@ -331,6 +331,7 @@ class MainSolver {
 
     class TimeLimitImpl;
     std::unique_ptr<TimeLimitImpl> timeLimitImplPtr;
+    std::unique_ptr<TimeLimitImpl> timeLimitPerQueryImplPtr;
 };
 
 bool MainSolver::trackPartitions() const {

src/bin/opensmt.cc

@@ -52,6 +52,9 @@ namespace opensmt {
 
 using namespace std::string_literals;
 
+template <typename...>
+constexpr bool falseTp = false;
+
 namespace {
     bool pipeExecution = false;
 }
@@ -244,11 +247,27 @@ 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"
+          "  --time-limit [-t] <ms>          sets wall-clock time limit in milliseconds since first query\n"
+          "  --time-limit-per-query <ms>     sets wall-clock time limit in milliseconds per each query\n"
           "  --pipe [-p]                     for execution within a pipe\n";
     std::cerr << help_string;
 }
 
+template <typename IntT>
+IntT parseInt(std::string const & msg) try {
+    if constexpr (std::is_same_v<IntT, int>) {
+        return std::stoi(optarg);
+    } else if constexpr (std::is_same_v<IntT, long>) {
+        return std::stol(optarg);
+    } else if constexpr (std::is_same_v<IntT, long long>) {
+        return std::stoll(optarg);
+    } else {
+        static_assert(falseTp<IntT>);
+    }
+} catch (std::logic_error const & e) {
+    throw std::invalid_argument{msg + e.what()};
+}
+
 SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
 {
     enum class LongOpt {
@@ -258,6 +277,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
         getUcore,
         minUcore,
         fullUcore,
+        timeLimitPerQuery,
     };
 
     SMTConfig res;
@@ -278,6 +298,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
             {"print-cores-full", no_argument, &selectedLongOpt, to_underlying(LongOpt::fullUcore)},
             {"produce-interpolants", no_argument, nullptr, 'i'},
             {"time-limit", required_argument, nullptr, 't'},
+            {"time-limit-per-query", required_argument, &selectedLongOpt, to_underlying(LongOpt::timeLimitPerQuery)},
             {"pipe", no_argument, nullptr, 'p'},
             {0, 0, 0, 0}
         };
@@ -310,6 +331,10 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
                     case LongOpt::fullUcore:
                         res.setOption(SMTConfig::o_print_cores_full, SMTOption(true), msg);
                         break;
+                    case LongOpt::timeLimitPerQuery:
+                        auto timeLimit = parseInt<int64_t>("Invalid argument of time-limit-per-query: ");
+                        ok &= res.setOption(SMTConfig::o_time_limit_per_query, SMTOption{timeLimit}, msg);
+                        break;
                 }
                 break;
             case 'h':
@@ -334,13 +359,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
                 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()};
-                }
-
+                auto timeLimit = parseInt<int64_t>("Invalid argument of time-limit: ");
                 ok &= res.setOption(SMTConfig::o_time_limit, SMTOption{timeLimit}, msg);
                 break;
             }

src/options/SMTConfig.cc

@@ -415,7 +415,7 @@ namespace opensmt {
           { msg = s_err_unknown_units; return false; }
       }
 
-      if (strcmp(name, o_time_limit) == 0) {
+      if (strcmp(name, o_time_limit) == 0 || strcmp(name, o_time_limit_per_query) == 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; }
       }
@@ -535,6 +535,7 @@ namespace opensmt {
   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";
+  const char* SMTConfig::o_time_limit_per_query = ":time-limit-per-query";
 
   char* SMTConfig::server_host=NULL;
   uint16_t SMTConfig::server_port = 0;

src/options/SMTConfig.h

@@ -329,6 +329,7 @@ namespace opensmt {
 
     // Wall-clock time limit for the solver in miliseconds
     static const char* o_time_limit;
+    static const char* o_time_limit_per_query;
   private:
 
     static const char* s_err_not_str;