1 files changed, 51 insertions, 2 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 9c438a5cd..a01237fd0 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -138,7 +138,11 @@ static const string optionsDescription = "\
    --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --disable-arithmetic-propagation turns on arithmetic propagation\n\
    --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\
-   --incremental | -i     enable incremental solving\n";
+   --incremental | -i     enable incremental solving\n\
+   --time-limit=MS        enable time limiting (give milliseconds)\n\
+   --time-limit-per=MS    enable time limiting per query (give milliseconds)\n\
+   --limit=N              enable resource limiting\n\
+   --limit-per=N          enable resource limiting per query\n";
 
 #warning "Change CL options as --disable-variable-removal cannot do anything currently."
 
@@ -296,7 +300,11 @@ enum OptionValue {
   ARITHMETIC_PROPAGATION,
   ARITHMETIC_PIVOT_THRESHOLD,
   ARITHMETIC_PROP_MAX_LENGTH,
-  DISABLE_SYMMETRY_BREAKER
+  DISABLE_SYMMETRY_BREAKER,
+  TIME_LIMIT,
+  TIME_LIMIT_PER,
+  LIMIT,
+  LIMIT_PER
 };/* enum OptionValue */
 
 /**
@@ -371,6 +379,10 @@ static struct option cmdlineOptions[] = {
   { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL },
   { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
   { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
+  { "time-limit" , required_argument, NULL, TIME_LIMIT  },
+  { "time-limit-per", required_argument, NULL, TIME_LIMIT_PER },
+  { "limit"      , required_argument, NULL, LIMIT       },
+  { "limit-per"  , required_argument, NULL, LIMIT_PER   },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -677,6 +689,43 @@ throw(OptionException) {
       ufSymmetryBreaker = false;
       break;
 
+    case TIME_LIMIT:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--time-limit requires a nonnegative argument.");
+        }
+        cumulativeMillisecondLimit = (unsigned long) i;
+      }
+      break;
+    case TIME_LIMIT_PER:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--time-limit-per requires a nonnegative argument.");
+        }
+        perCallMillisecondLimit = (unsigned long) i;
+      }
+      break;
+    case LIMIT:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--limit requires a nonnegative argument.");
+        }
+        cumulativeResourceLimit = (unsigned long) i;
+      }
+      break;
+    case LIMIT_PER:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--limit-per requires a nonnegative argument.");
+        }
+        perCallResourceLimit = (unsigned long) i;
+        break;
+      }
+
     case RANDOM_SEED:
       satRandomSeed = atof(optarg);
       break;