1 files changed, 17 insertions, 0 deletions
diff --git a/src/theory/options_handlers.h b/src/theory/options_handlers.h
index 268fd46fd..def304d8b 100644
--- a/src/theory/options_handlers.h
+++ b/src/theory/options_handlers.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__THEORY__OPTIONS_HANDLERS_H
 #define __CVC4__THEORY__OPTIONS_HANDLERS_H
 
+#include "expr/metakind.h"
+
 namespace CVC4 {
 namespace theory {
 
@@ -46,6 +48,21 @@ inline TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg,
   }
 }
 
+inline void useTheory(std::string option, std::string optarg, SmtEngine* smt) {
+  if(optarg == "help") {
+    puts(useTheoryHelp);
+    exit(1);
+  }
+  if(useTheoryValidate(optarg)) {
+    std::map<std::string, bool> m = options::theoryAlternates();
+    m[optarg] = true;
+    options::theoryAlternates.set(m);
+  } else {
+    throw OptionException(std::string("unknown option for ") + option + ": `" +
+                          optarg + "'.  Try --use-theory help.");
+  }
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */