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.

6 files changed, 38 insertions, 11 deletions

diff --git a/contrib/theoryskel/Makefile.am b/contrib/theoryskel/Makefile.am
index d6b41ac03..000544d98 100644
--- a/contrib/theoryskel/Makefile.am
+++ b/contrib/theoryskel/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = lib$dir.la
@@ -12,4 +12,5 @@ lib$dir_la_SOURCES = \
 	theory_$dir_type_rules.h
 
 EXTRA_DIST = \
-	kinds
+	kinds \
+	options_handlers.h
diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT
index 6e090b984..ede8054ed 100644
--- a/contrib/theoryskel/README.WHATS-NEXT
+++ b/contrib/theoryskel/README.WHATS-NEXT
@@ -19,18 +19,18 @@ and finally:
   Theory$camel::check() in theory_$dir.cpp. Before writing the actual
   code, you will need :
 
-  * to determine which datastructures are context dependent and use for them
-    context dependent datastructures (context/cd*.h)
+  * to determine which data structures are context dependent and use for
+    them context-dependent data structures (context/cd*.h)
   * to choose which work will be done at QUICK_CHECK, STANDARD or at
     FULL_EFFORT.
 
 You'll probably find the Developer's wiki useful:
 
-  http://church.cims.nyu.edu/wiki/CVC_Portal
+  http://cvc4.cs.nyu.edu/wiki/
 
-...and in particular the Deverloper's Guide:
+...and in particular the Developer's Guide:
 
-  http://church.cims.nyu.edu/wiki/Developer%27s_Guide
+  http://cvc4.cs.nyu.edu/wiki/Developer%27s_Guide
 
 which contains coding guidelines for the CVC4 project.
 
diff --git a/contrib/theoryskel/options b/contrib/theoryskel/options
new file mode 100644
index 000000000..f627dc4a0
--- /dev/null
+++ b/contrib/theoryskel/options
@@ -0,0 +1,8 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module $id "theory/$dir/options.h" $camel
+
+endmodule
diff --git a/contrib/theoryskel/options_handlers.h b/contrib/theoryskel/options_handlers.h
new file mode 100644
index 000000000..d384e84d9
--- /dev/null
+++ b/contrib/theoryskel/options_handlers.h
@@ -0,0 +1,14 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__$id__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__$id__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+namespace $dir {
+
+}/* CVC4::theory::$dir namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__$id__OPTIONS_HANDLERS_H */
diff --git a/contrib/theoryskel/theory_DIR.cpp b/contrib/theoryskel/theory_DIR.cpp
index e885cb9c7..aefa0a2af 100644
--- a/contrib/theoryskel/theory_DIR.cpp
+++ b/contrib/theoryskel/theory_DIR.cpp
@@ -10,8 +10,10 @@ namespace $dir {
 Theory$camel::Theory$camel(context::Context* c,
                            context::UserContext* u,
                            OutputChannel& out,
-                           Valuation valuation) :
-  Theory(THEORY_$id, c, u, out, valuation) {
+                           Valuation valuation,
+                           const LogicInfo& logicInfo,
+                           QuantifiersEngine* qe) :
+  Theory(THEORY_$id, c, u, out, valuation, logicInfo, qe) {
 }/* Theory$camel::Theory$camel() */
 
 void Theory$camel::check(Effort level) {
diff --git a/contrib/theoryskel/theory_DIR.h b/contrib/theoryskel/theory_DIR.h
index f8151ae42..9dfb3e614 100644
--- a/contrib/theoryskel/theory_DIR.h
+++ b/contrib/theoryskel/theory_DIR.h
@@ -12,11 +12,13 @@ namespace $dir {
 class Theory$camel : public Theory {
 public:
 
-  /** Constructs a new instance of Theory$camel w.r.t. the provided context.*/
+  /** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */
   Theory$camel(context::Context* c,
                context::UserContext* u,
                OutputChannel& out,
-               Valuation valuation);
+               Valuation valuation,
+               const LogicInfo& logicInfo,
+               QuantifiersEngine* qe);
 
   void check(Effort);