5 files changed, 92 insertions, 7 deletions
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 2d8012bfb..084a624f7 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -52,13 +52,13 @@ seen_theory=false
 seen_theory_builtin=false
 
 function theory {
-  # theory T header
+  # theory ID T header
 
   lineno=${BASH_LINENO[0]}
 
   if $seen_theory; then
-    echo "$kf:$lineno: theory declaration can only appear once" >&2
-    exit 1;
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
   fi
 
   # this script doesn't care about the theory class information, but
@@ -82,6 +82,20 @@ function theory {
   theory_id="$1"
 }
 
+function alternate {
+  # alternate ID name T header
+
+  lineno=${BASH_LINENO[0]}
+
+  if $seen_theory; then
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
+  fi
+
+  seen_theory=true
+  seen_endtheory=true
+}
+
 function properties {
   # properties prop*
   lineno=${BASH_LINENO[0]}
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 3edc7c140..97ede32d5 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -40,6 +40,7 @@ template=$1; shift
 
 theory_traits=
 theory_includes=
+theory_constructors=
 theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\
 "
 
@@ -72,13 +73,13 @@ seen_theory=false
 seen_theory_builtin=false
 
 function theory {
-  # theory T header
+  # theory ID T header
 
   lineno=${BASH_LINENO[0]}
 
   if $seen_theory; then
-    echo "$kf:$lineno: theory declaration can only appear once" >&2
-    exit 1;
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
   fi
 
   # this script doesn't care about the theory class information, but
@@ -109,6 +110,30 @@ function theory {
 "
 }
 
+function alternate {
+  # alternate ID name T header
+
+  lineno=${BASH_LINENO[0]}
+
+  if $seen_theory; then
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
+  fi
+
+  seen_theory=true
+  seen_endtheory=true
+
+  theory_header="$4"
+  theory_includes="${theory_includes}#include \"$theory_header\"
+"
+
+  eval "alternate_for_$1=\"\${alternate_for_$1}
+      if(options::theoryAlternates()[\\\"$2\\\"]) {
+        engine->addTheory< $3 >($1);
+        return;
+      }\""
+}
+
 function rewriter {
   # rewriter class header
   lineno=${BASH_LINENO[0]}
@@ -128,10 +153,17 @@ function endtheory {
 
   seen_endtheory=true
 
+  theory_constructors="${theory_constructors}
+    case $theory_id:
+\$alternate_for_$theory_id
+      engine->addTheory< $theory_class >($theory_id);
+      return;
+"
+
   theory_traits="${theory_traits}
 template<>
 struct TheoryTraits<${theory_id}> {
-    typedef ${theory_class} theory_class;
+    // typedef ${theory_class} theory_class;
     typedef ${rewriter_class} rewriter_class;
 
     static const bool isStableInfinite = ${theory_stable_infinite};
@@ -368,6 +400,8 @@ check_builtin_theory_seen
 
 ## output
 
+eval "theory_constructors=\"$theory_constructors\""
+
 # generate warnings about incorrect #line annotations in templates
 nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
   awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
@@ -377,6 +411,7 @@ for var in \
     theory_traits \
     theory_for_each_macro \
     theory_includes \
+    theory_constructors \
     template \
     type_enumerator_includes \
     mk_type_enumerator_type_constant_cases \
diff --git a/src/theory/options b/src/theory/options
index 5a523f0fa..5d752fca1 100644
--- a/src/theory/options
+++ b/src/theory/options
@@ -8,4 +8,8 @@ module THEORY "theory/options.h" Theory layer
 expert-option theoryOfMode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::theory::stringToTheoryOfMode :handler-include "theory/options_handlers.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "theory/theoryof_mode.h"
  mode for theoryof
 
+option - use-theory --use-theory=NAME argument :handler CVC4::theory::useTheory :handler-include "theory/options_handlers.h"
+ use alternate theory implementation NAME (--use-theory=help for a list)
+option theoryAlternates ::std::map<std::string,bool> :include <map> :read-write
+
 endmodule
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 */
 
diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h
index d4f961eb7..326c6c913 100644
--- a/src/theory/theory_traits_template.h
+++ b/src/theory/theory_traits_template.h
@@ -21,6 +21,7 @@
 
 #include "cvc4_private.h"
 #include "theory/theory.h"
+#include "theory/options.h"
 
 ${theory_includes}
 
@@ -34,5 +35,19 @@ ${theory_traits}
 
 ${theory_for_each_macro}
 
+#line 39 "${template}"
+
+struct TheoryConstructor {
+  static void addTheory(TheoryEngine* engine, TheoryId id) {
+    switch(id) {
+
+${theory_constructors}
+
+    default:
+      Unhandled(id);
+    }
+  }
+};/* struct CVC4::theory::TheoryConstructor */
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */