From b25991f4c2779c34b51cd51b943290a4a3d2a9fd Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 23 Apr 2013 23:03:37 -0400
Subject: 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.
---
 src/theory/theory_traits_template.h | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'src/theory/theory_traits_template.h')

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 */
-- 
cgit v1.2.3