Implemented timeout set via command line

Author: Tomaqa

src/api/Interpret.cc

@@ -1375,22 +1375,25 @@ void Interpret::getInterpolants(const ASTNode& n)
 }
 
 bool Interpret::setTimeLimit(ASTNode const & n) {
-    int64_t limit;
     try {
-        limit = std::stoll(n.getValue());
-        if (limit <= 0) { throw std::out_of_range{"The value must be positive."}; }
+        int64_t limit = std::stoll(n.getValue());
+        setTimeLimit(limit);
     } catch (std::out_of_range const & e) {
         notify_formatted(true, "Invalid argument of set-time-limit: %s", e.what());
         return false;
     }
 
+    return true;
+}
+
+void Interpret::setTimeLimit(int64_t limit) {
+    if (limit <= 0) { throw std::out_of_range{"Time limit must be positive."}; }
+
     if (main_solver) {
         main_solver->setTimeLimit(std::chrono::milliseconds{limit});
     } else {
         optTimeLimit = limit;
     }
-
-    return true;
 }
 
 bool Interpret::is_top_level_assertion(PTRef ref) {

src/api/Interpret.h

@@ -196,6 +196,9 @@ class Interpret {
 
     ~Interpret();
 
+    // may throw std::out_of_range
+    void setTimeLimit(int64_t limit);
+
     int interpFile(FILE* in);
     int interpFile(char *content);
     int interpPipe();

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,13 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 
 namespace opensmt {
 
-inline bool pipeExecution = false;
+using namespace std::string_literals;
+
+namespace {
+    std::optional<int64_t> optTimeLimit;
+
+    bool pipeExecution = false;
+}
 
 SMTConfig parseCMDLineArgs(int argc, char * argv[ ]);
 
@@ -85,8 +92,13 @@ int main( int argc, char * argv[] )
     FILE * fin = NULL;
 
     SMTConfig c = parseCMDLineArgs(argc,argv);
+
     Interpret interpreter(c);
 
+    if (optTimeLimit) {
+        interpreter.setTimeLimit(*optTimeLimit);
+    }
+
     if (argc - optind == 0) {
         c.setInstanceName("stdin");
         if (pipeExecution) {
@@ -225,6 +237,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;
 }
@@ -247,14 +260,15 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
             {"minimal-unsat-cores", no_argument, &selectedLongOpt, minUcoreLongOpt},
             {"print-cores-full", no_argument, &selectedLongOpt, fullUcoreLongOpt},
             {"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) {
         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) {
@@ -289,6 +303,15 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
             case 'i':
                 res.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
                 break;
+            case 't': {
+                try {
+                    optTimeLimit = std::stoll(optarg);
+                } catch (std::out_of_range const & e) {
+                    throw std::invalid_argument{"Invalid argument of time-limit: "s + e.what()};
+                }
+
+                break;
+            }
             case 'p':
                 pipeExecution = true;
                 break;