Theory "alternates" support

* This is a feature that Dejan and I want for the upcoming tutorial.
  It allows rapid prototyping of new decision procedure implementations
  (which we may choose to demonstrate), and a new --use-theory command-line
  option to select from different available implementations.  It has no
  affect on the current set of theories, as no "alternates" are defined.

* Also update the new-theory script, which was broken and incomplete.

1 files changed, 15 insertions, 0 deletions

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 */