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.

8 files changed, 150 insertions, 0 deletions

diff --git a/contrib/alttheoryskel/Makefile b/contrib/alttheoryskel/Makefile
new file mode 100644
index 000000000..2aeda0cf8
--- /dev/null
+++ b/contrib/alttheoryskel/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/$dir
+
+include $(topdir)/Makefile.subdir
diff --git a/contrib/alttheoryskel/Makefile.am b/contrib/alttheoryskel/Makefile.am
new file mode 100644
index 000000000..2f36e8fc1
--- /dev/null
+++ b/contrib/alttheoryskel/Makefile.am
@@ -0,0 +1,14 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = lib$dir.la
+
+lib$dir_la_SOURCES = \
+	theory_$dir.h \
+	theory_$dir.cpp
+
+EXTRA_DIST = \
+	kinds \
+	options_handlers.h
diff --git a/contrib/alttheoryskel/README.WHATS-NEXT b/contrib/alttheoryskel/README.WHATS-NEXT
new file mode 100644
index 000000000..c6ad91c3f
--- /dev/null
+++ b/contrib/alttheoryskel/README.WHATS-NEXT
@@ -0,0 +1,25 @@
+Congratulations, you now have a new theory of $dir !
+
+Your next steps will likely be:
+
+* to implement a decision procedure for your theory by implementing
+  Theory$camel::check() in theory_$dir.cpp. Before writing the actual
+  code, you will need :
+
+  * 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://cvc4.cs.nyu.edu/wiki/
+
+...and in particular the Developer's Guide:
+
+  http://cvc4.cs.nyu.edu/wiki/Developer%27s_Guide
+
+which contains coding guidelines for the CVC4 project.
+
+Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance
+should you need it!
diff --git a/contrib/alttheoryskel/kinds b/contrib/alttheoryskel/kinds
new file mode 100644
index 000000000..44efe1698
--- /dev/null
+++ b/contrib/alttheoryskel/kinds
@@ -0,0 +1,8 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+alternate THEORY_$alt_id "$dir" ::CVC4::theory::$dir::Theory$camel "theory/$dir/theory_$dir.h"
+
diff --git a/contrib/alttheoryskel/options b/contrib/alttheoryskel/options
new file mode 100644
index 000000000..f627dc4a0
--- /dev/null
+++ b/contrib/alttheoryskel/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/alttheoryskel/options_handlers.h b/contrib/alttheoryskel/options_handlers.h
new file mode 100644
index 000000000..d384e84d9
--- /dev/null
+++ b/contrib/alttheoryskel/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/alttheoryskel/theory_DIR.cpp b/contrib/alttheoryskel/theory_DIR.cpp
new file mode 100644
index 000000000..eca07e909
--- /dev/null
+++ b/contrib/alttheoryskel/theory_DIR.cpp
@@ -0,0 +1,42 @@
+#include "theory/$dir/theory_$dir.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace $dir {
+
+/** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */
+Theory$camel::Theory$camel(context::Context* c,
+                           context::UserContext* u,
+                           OutputChannel& out,
+                           Valuation valuation,
+                           const LogicInfo& logicInfo,
+                           QuantifiersEngine* qe) :
+  Theory(THEORY_$alt_id, c, u, out, valuation, logicInfo, qe) {
+}/* Theory$camel::Theory$camel() */
+
+void Theory$camel::check(Effort level) {
+
+  while(!done()) {
+    // Get all the assertions
+    Assertion assertion = get();
+    TNode fact = assertion.assertion;
+
+    Debug("$dir") << "Theory$camel::check(): processing " << fact << std::endl;
+
+    // Do the work
+    switch(fact.getKind()) {
+
+    /* cases for all the theory's kinds go here... */
+
+    default:
+      Unhandled(fact.getKind());
+    }
+  }
+
+}/* Theory$camel::check() */
+
+}/* CVC4::theory::$dir namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/contrib/alttheoryskel/theory_DIR.h b/contrib/alttheoryskel/theory_DIR.h
new file mode 100644
index 000000000..9dfb3e614
--- /dev/null
+++ b/contrib/alttheoryskel/theory_DIR.h
@@ -0,0 +1,35 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__$id__THEORY_$id_H
+#define __CVC4__THEORY__$id__THEORY_$id_H
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace $dir {
+
+class Theory$camel : public Theory {
+public:
+
+  /** 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,
+               const LogicInfo& logicInfo,
+               QuantifiersEngine* qe);
+
+  void check(Effort);
+
+  std::string identify() const {
+    return "THEORY_$id";
+  }
+
+};/* class Theory$camel */
+
+}/* CVC4::theory::$dir namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__$id__THEORY_$id_H */