add timeout keyword to set-option in the smt2 frontend (#527)

* add timeout keyword to set-option in the smt2 frontend

* add timeout example

src/frontend/smt2/smt2_commands.c

@@ -6283,6 +6283,10 @@ void smt2_set_option(const char *name, aval_t value) {
     set_boolean_option(g, name, value, &g->dump_models);
     break;
 
+  case SMT2_KW_TIMEOUT:
+    set_uint32_option(g, name, value, &g->timeout);
+    break;
+
   case SMT2_KW_PRODUCE_UNSAT_ASSUMPTIONS:
     // optional: if true, get-unsat-assumptions can be used
     if (option_can_be_set(name)) {

src/frontend/smt2/smt2_commands.h

@@ -402,7 +402,7 @@ typedef struct smt2_globals_s {
   uint32_t nthreads;           // default = 0 (single threaded)
 
   // timeout
-  uint32_t timeout;           // default = 0 (no timeout)
+  uint32_t timeout;           // default = 0 (no timeout); global timeout used for every check-sat
   timeout_t *to;              // initially NULL. Non-NULL once init_timeout is called
   bool interrupted;           // true if the most recent call to check_sat timed out
 

src/frontend/smt2/smt2_keywords.txt

@@ -37,4 +37,5 @@ struct keyword_s;
 :category,                    SMT2_KW_CATEGORY
 :difficulty,                  SMT2_KW_DIFFICULTY
 :notes,                       SMT2_KW_NOTES
-:dump-models,                 SMT2_KW_DUMP_MODELS
+:dump-models,                 SMT2_KW_DUMP_MODELS
+:timeout,                     SMT2_KW_TIMEOUT

src/frontend/smt2/smt2_lexer.c

@@ -116,6 +116,7 @@ static const char * const smt2_keyword_string[NUM_SMT2_KEYWORDS] = {
   ":reproducible-resource-limit",  // SMT2_KW_REPRODUCIBLE_RESOURCE_LIMIT
   ":verbosity",               // SMT2_KW_VERBOSITY
   ":dump-models",             // SMT2_KW_DUMP_MODELS
+  ":timeout",                 // SMT2_KW_TIMEOUT
 
   ":all-statistics",          // SMT2_KW_ALL_STATISTICS
   ":assertion-stack-levesl",  // SMT2_KM_ASSERTIONS_STACK_LEVELS

src/frontend/smt2/smt2_lexer.h

@@ -136,6 +136,7 @@ enum smt2_keyword {
   SMT2_KW_REPRODUCIBLE_RESOURCE_LIMIT,
   SMT2_KW_VERBOSITY,
   SMT2_KW_DUMP_MODELS,
+  SMT2_KW_TIMEOUT,
 
   // Predefined keywords for (get-info ...)
   SMT2_KW_ALL_STATISTICS,

tests/regress/set-timeout.smt2

@@ -0,0 +1,3 @@
+ (set-option :timeout 1)
+ (set-logic QF_UF)
+ (exit)