From 1c4d70e81e2acd9c53a117dcedea4a039b5c2fa1 Mon Sep 17 00:00:00 2001
From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com>
Date: Tue, 3 Sep 2024 13:00:35 -0700
Subject: [PATCH] add timeout keyword to set-option in the smt2 frontend

---
 src/frontend/smt2/smt2_commands.c   | 4 ++++
 src/frontend/smt2/smt2_commands.h   | 2 +-
 src/frontend/smt2/smt2_keywords.txt | 3 ++-
 src/frontend/smt2/smt2_lexer.c      | 1 +
 src/frontend/smt2/smt2_lexer.h      | 1 +
 tests/regress/set-timeout.smt2      | 3 +++
 tests/regress/set-timeout.smt2.gold | 0
 7 files changed, 12 insertions(+), 2 deletions(-)
 create mode 100644 tests/regress/set-timeout.smt2
 create mode 100644 tests/regress/set-timeout.smt2.gold

diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c
index 9b7f90307..f6a038f23 100644
--- a/src/frontend/smt2/smt2_commands.c
+++ b/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)) {
diff --git a/src/frontend/smt2/smt2_commands.h b/src/frontend/smt2/smt2_commands.h
index 3f5570859..9fea4ee96 100644
--- a/src/frontend/smt2/smt2_commands.h
+++ b/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
 
diff --git a/src/frontend/smt2/smt2_keywords.txt b/src/frontend/smt2/smt2_keywords.txt
index 20ad58844..e78a4c15f 100644
--- a/src/frontend/smt2/smt2_keywords.txt
+++ b/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
\ No newline at end of file
+:dump-models,                 SMT2_KW_DUMP_MODELS
+:timeout,                     SMT2_KW_TIMEOUT
diff --git a/src/frontend/smt2/smt2_lexer.c b/src/frontend/smt2/smt2_lexer.c
index 3efb06a6c..ae3faacd5 100644
--- a/src/frontend/smt2/smt2_lexer.c
+++ b/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
diff --git a/src/frontend/smt2/smt2_lexer.h b/src/frontend/smt2/smt2_lexer.h
index 865fd48fc..d555972fd 100644
--- a/src/frontend/smt2/smt2_lexer.h
+++ b/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,
diff --git a/tests/regress/set-timeout.smt2 b/tests/regress/set-timeout.smt2
new file mode 100644
index 000000000..227d74dc6
--- /dev/null
+++ b/tests/regress/set-timeout.smt2
@@ -0,0 +1,3 @@
+ (set-option :timeout 1)
+ (set-logic QF_UF)
+ (exit)
\ No newline at end of file
diff --git a/tests/regress/set-timeout.smt2.gold b/tests/regress/set-timeout.smt2.gold
new file mode 100644
index 000000000..e69de29bb