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, 17 insertions, 0 deletions

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 10b67b4d6..22d7baac3 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -325,6 +325,23 @@ ${metakind_ubchildren}
 
 }/* CVC4::kind::metakind namespace */
 }/* CVC4::kind namespace */
+
+#line 330 "${template}"
+
+namespace theory {
+
+static inline bool useTheoryValidate(std::string theory) {
+${use_theory_validations}
+  return false;
+}
+
+static const char *const useTheoryHelp = "\
+The following options are valid alternate implementations for use with\n\
+the --use-theory option:\n\
+\n\
+${theory_alternate_doc}";
+
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */