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