1 files changed, 21 insertions, 1 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index ed196ac45..b15f4ae66 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -69,7 +69,8 @@ enum OptionValue {
   SHOW_CONFIG,
   STRICT_PARSING,
   DEFAULT_EXPR_DEPTH,
-  PRINT_EXPR_TYPES
+  PRINT_EXPR_TYPES,
+  UF_THEORY
 };/* enum OptionValue */
 
 /**
@@ -115,6 +116,7 @@ static struct option cmdlineOptions[] = {
   { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
   { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
   { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
+  { "uf"         , required_argument, NULL, UF_THEORY },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -248,6 +250,24 @@ throw(OptionException) {
       }
       break;
 
+    case UF_THEORY:
+      {
+        if(!strcmp(optarg, "tim")) {
+          opts->uf_implementation = Options::TIM;
+        } else if(!strcmp(optarg, "morgan")) {
+          opts->uf_implementation = Options::MORGAN;
+        } else if(!strcmp(optarg, "help")) {
+          printf("UF implementations available:\n");
+          printf("tim\n");
+          printf("morgan\n");
+          exit(1);
+        } else {
+          throw OptionException(string("unknown language for --uf: `") +
+                                optarg + "'.  Try --uf help.");
+        }
+      }
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");