1 files changed, 22 insertions, 0 deletions
diff --git a/src/util/options.h b/src/util/options.h
index 7fcf35f00..c79bc93b1 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -47,6 +47,12 @@ struct CVC4_PUBLIC Options {
   /** The input language */
   parser::InputLanguage lang;
 
+  /** Enumeration of UF implementation choices */
+  typedef enum { TIM, MORGAN } UfImplementation;
+
+  /** Which implementation of uninterpreted function theory to use */
+  UfImplementation uf_implementation;
+
   /** Should we exit after parsing? */
   bool parseOnly;
 
@@ -65,6 +71,7 @@ struct CVC4_PUBLIC Options {
               err(0),
               verbosity(0),
               lang(parser::LANG_AUTO),
+              uf_implementation(MORGAN),
               parseOnly(false),
               semanticChecks(true),
               memoryMap(false),
@@ -72,6 +79,21 @@ struct CVC4_PUBLIC Options {
   {}
 };/* struct Options */
 
+inline std::ostream& operator<<(std::ostream& out, Options::UfImplementation uf) {
+  switch(uf) {
+  case Options::TIM:
+    out << "TIM";
+    break;
+  case Options::MORGAN:
+    out << "MORGAN";
+    break;
+  default:
+    out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]";
+  }
+
+  return out;
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__OPTIONS_H */