Implemented timeout set via command line

Author: Tomaqa

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;
+}
 
 SMTConfig parseCMDLineArgs(int argc, char * argv[ ]);
 
@@ -66,7 +71,7 @@ void interpretInteractive(Interpret & interpret);
 }
 
 int main( int argc, char * argv[] )
-{
+try {
     using namespace opensmt;
 
     signal( SIGTERM, catcher );
@@ -123,6 +128,10 @@ int main( int argc, char * argv[] )
 
     return 0;
 }
+catch (std::exception const & e) {
+    std::cerr << "Terminated with exception:\n" << e.what() << std::endl;
+    return 1;
+}
 
 namespace opensmt {
 
@@ -225,6 +234,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 +257,16 @@ 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) {
+    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) {
@@ -289,6 +301,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;
@@ -298,6 +321,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.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<int>(i)) {}
       SMTOption(double i): value(i) {}
       SMTOption(const char* s) : value(s) {}
       inline bool isEmpty() const { return value.type == O_EMPTY; }