From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 24 Apr 2013 03:03:37 +0000 (-0400)
Subject: Theory "alternates" support
X-Git-Tag: cvc5-1.0.0~7314
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b25991f4c2779c34b51cd51b943290a4a3d2a9fd;p=cvc5.git

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.
---

diff --git a/configure.ac b/configure.ac
index c29d0f75a..2a48f4b13 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1179,7 +1179,7 @@ AC_SUBST(MAN_DATE)
 AC_CONFIG_FILES([
   Makefile.builds
   Makefile]
-  m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | sort | sed 's,\.am$,,'])
+  m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
 )
 
 if test $cvc4_has_threads = yes; then
diff --git a/contrib/Makefile.am b/contrib/Makefile.am
index b2147b19a..702bfe7fa 100644
--- a/contrib/Makefile.am
+++ b/contrib/Makefile.am
@@ -22,3 +22,9 @@ EXTRA_DIST = \
 	theoryskel/theory_DIR.h \
 	theoryskel/theory_DIR_rewriter.h \
 	theoryskel/theory_DIR_type_rules.h
+	alttheoryskel/kinds \
+	alttheoryskel/Makefile \
+	alttheoryskel/Makefile.am \
+	alttheoryskel/README.WHATS-NEXT \
+	alttheoryskel/theory_DIR.cpp \
+	alttheoryskel/theory_DIR.h
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 */
diff --git a/contrib/new-theory b/contrib/new-theory
index 4aedd7c0f..4649e5943 100755
--- a/contrib/new-theory
+++ b/contrib/new-theory
@@ -1,6 +1,6 @@
 #!/bin/bash
 #
-# usage: new-theory theory-directory-name
+# usage: new-theory [--alternate existing-theory] new-theory-dir-name
 #
 
 cd "`dirname "$0"`/.."
@@ -11,23 +11,39 @@ if [ ! -e src/theory/theory_engine.h ]; then
   exit 1
 fi
 
+if [ $# -ge 1 -a "$1" = --alternate ]; then
+  shift
+  alternate=true
+  alttheory="$1"
+  shift
+else
+  alternate=false
+fi
+
 if [ $# -ne 1 ]; then
-  echo "usage: new-theory theory-directory-name" >&2
-  echo "e.g.:  new-theory arith" >&2
+  echo "usage: new-theory [--alternate existing-theory] new-theory-dir-name" >&2
   echo "e.g.:  new-theory arrays" >&2
   echo "e.g.:  new-theory sets" >&2
   echo "e.g.:  new-theory rewrite_rules" >&2
+  echo "e.g.:  new-theory --alternate arith difference-logic" >&2
   echo >&2
-  echo "This tool will create a new src/theory/<theory-directory-name>" >&2
+  echo "This tool will create a new src/theory/<new-theory-dir-name>" >&2
   echo "directory and fill in some infrastructural files in that directory." >&2
   echo "It also will incorporate that directory into the build process." >&2
   echo "Please refer to the file README.WHATS-NEXT file created in that" >&2
-  echo "directory for tips on what to do next."
-  echo
+  echo "directory for tips on what to do next." >&2
+  echo >&2
   echo "Theories with multiple words (e.g. \"rewrite_rules\") should have" >&2
   echo "directories and namespaces separated by an underscore (_).  The" >&2
   echo "resulting class names created by this script will be in CamelCase" >&2
   echo "(e.g. RewriteRules) if that convention is followed." >&2
+  echo >&2
+  echo "With --alternate, create a new theory directory that is declared as" >&2
+  echo "an alternate implementation of an existing host theory.  Such" >&2
+  echo "\"alternates\" share preprocessing, typechecking, rewriting (i.e.," >&2
+  echo "normal form), and expression kinds with their host theories, but" >&2
+  echo "differ in decision procedure implementation.  They are selectable" >&2
+  echo "at runtime with --use-theory." >&2
   exit 1
 fi
 
@@ -36,6 +52,9 @@ dir="$1"
 if [ -e "src/theory/$dir" ]; then
   echo "ERROR: Theory \"$dir\" already exists." >&2
   echo "ERROR: Please choose a new directory name (or move that one aside)." >&2
+  echo "ERROR: Or, if you'd like to create an alternate implementation of" >&2
+  echo "ERROR: $dir, use this program this way:" >&2
+  echo "ERROR:     new-theory --alternate $dir new-implementation-name" >&2
   exit 1
 fi
 
@@ -49,6 +68,17 @@ if ! expr "$dir" : '[a-zA-Z][a-zA-Z0-9_]*$' &>/dev/null ||
   exit 1
 fi
 
+if $alternate; then
+  if ! [ -d "src/theory/$alttheory" -a -f "src/theory/$alttheory/kinds" ]; then
+    echo "ERROR: Theory \"$alttheory\" doesn't exist, or cannot read its kinds file." >&2
+    exit 1
+  fi
+  alt_id="$(
+    function theory() { echo $1 | sed 's,^THEORY_,,'; exit; }
+    source "src/theory/$alttheory/kinds"
+  )"
+fi
+
 id="`echo "$dir" | tr a-z A-Z`"
 # convoluted, but should be relatively portable and give a CamelCase
 # representation for a string.  (e.g. "foo_bar" becomes "FooBar")
@@ -62,6 +92,7 @@ fi
 echo "Theory of $dir"
 echo "Theory directory: src/theory/$dir"
 echo "Theory id: THEORY_$id"
+$alternate && echo "Alternate for theory id: THEORY_$alt_id"
 echo "Theory class: CVC4::theory::$dir::Theory$camel"
 echo
 
@@ -74,13 +105,28 @@ function copyskel {
     > "src/theory/$dir/$dest"
 }
 
+function copyaltskel {
+  src="$1"
+  dest="`echo "$src" | sed "s/DIR/$dir/g"`"
+  echo "Creating src/theory/$dir/$dest..."
+  sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \
+    contrib/alttheoryskel/$src \
+    > "src/theory/$dir/$dest"
+}
+
 # copy files from the skeleton, with proper replacements
-for file in `ls contrib/theoryskel`; do
-  copyskel "$file"
-done
+if $alternate; then
+  for file in `ls contrib/alttheoryskel`; do
+    copyaltskel "$file"
+  done
+else
+  for file in `ls contrib/theoryskel`; do
+    copyskel "$file"
+  done
+fi
 
 echo
-echo "Adding $dir to SUBDIRS in src/theory/Makefile.am..."
+echo "Adding $dir to SUBDIRS to src/theory/Makefile.am..."
 if grep -q '^SUBDIRS = .*[^a-zA-Z0-9_]'"$dir"'\([^a-zA-Z0-9_]\|$\)' src/theory/Makefile.am &>/dev/null; then
   echo "NOTE: src/theory/Makefile.am already descends into dir $dir"
 else
@@ -95,9 +141,9 @@ else
   fi
 fi
 
-echo "Adding lib$theory.la to LIBADD in src/theory/Makefile.am..."
+echo "Adding lib$dir.la to LIBADD to src/theory/Makefile.am..."
 if grep -q '^	@builddir@/'"$dir"'/lib'"$dir"'\.la\>' src/theory/Makefile.am &>/dev/null; then
-  echo "NOTE: src/theory/Makefile.am already seems to include lib$theory.la"
+  echo "NOTE: src/theory/Makefile.am already seems to include lib$dir.la"
 else
   awk '!/^libtheory_la_LIBADD = / {print$0} /^libtheory_la_LIBADD = / {while(/\\ *$/){print $0;getline} print $0,"\\";print "\t@builddir@/'"$dir"'/lib'"$dir"'.la"}' src/theory/Makefile.am > src/theory/Makefile.am.new-theory
   if ! cp -f src/theory/Makefile.am src/theory/Makefile.am~; then
@@ -110,6 +156,22 @@ else
   fi
 fi
 
+echo "Adding ../theory/$dir/options.cpp to OPTIONS_FILES_SRCS"
+echo "  and nodist_liboptions_la_SOURCES to src/options/Makefile.am..."
+if grep -q '^	\.\./theory/'"$dir"'/options\.cpp\>' src/options/Makefile.am &>/dev/null; then
+  echo "NOTE: src/options/Makefile.am already seems to link to $dir option files"
+else
+  awk '!/^OPTIONS_FILES_SRCS = \\|^nodist_liboptions_la_SOURCES = / {print$0} /^OPTIONS_FILES_SRCS = \\|^nodist_liboptions_la_SOURCES = / {while(/\\ *$/){print $0;getline} print $0,"\\";print "\t../theory/'"$dir"'/options.cpp","\\";print "\t../theory/'"$dir"'/options.h";}' src/options/Makefile.am > src/options/Makefile.am.new-theory
+  if ! cp -f src/options/Makefile.am src/options/Makefile.am~; then
+    echo "ERROR: cannot copy src/options/Makefile.am !" >&2
+    exit 1
+  fi
+  if ! mv -f src/options/Makefile.am.new-theory src/options/Makefile.am; then
+    echo "ERROR: cannot replace src/options/Makefile.am !" >&2
+    exit 1
+  fi
+fi
+
 echo
 echo "Rerunning autogen.sh..."
 ./autogen.sh
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);
 
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 */
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index ca89dfc91..8c94db3cc 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -70,10 +70,15 @@ seen_theory=false
 seen_theory_builtin=false
 
 function theory {
-  # theory T header
+  # theory ID T header
 
   lineno=${BASH_LINENO[0]}
 
+  if $seen_theory; then
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
+  fi
+
   # this script doesn't care about the theory class information, but
   # makes does make sure it's there
   seen_theory=true
@@ -93,6 +98,20 @@ function theory {
   fi
 }
 
+function alternate {
+  # alternate ID name T header
+
+  lineno=${BASH_LINENO[0]}
+
+  if $seen_theory; then
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
+  fi
+
+  seen_theory=true
+  seen_endtheory=true
+}
+
 function rewriter {
   # rewriter class header
   lineno=${BASH_LINENO[0]}
diff --git a/src/expr/mkkind b/src/expr/mkkind
index f8432466d..02e0f50bf 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -77,10 +77,15 @@ theory_enum=
 theory_descriptions=
 
 function theory {
-  # theory T header
+  # theory ID T header
 
   lineno=${BASH_LINENO[0]}
 
+  if $seen_theory; then
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
+  fi
+
   # this script doesn't care about the theory class information, but
   # makes does make sure it's there
   seen_theory=true
@@ -106,6 +111,20 @@ function theory {
 "
 }
 
+function alternate {
+  # alternate ID name T header
+
+  lineno=${BASH_LINENO[0]}
+
+  if $seen_theory; then
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
+  fi
+
+  seen_theory=true
+  seen_endtheory=true
+}
+
 function properties {
   # rewriter class header
   lineno=${BASH_LINENO[0]}
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 160a74eac..d8192e432 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -50,14 +50,22 @@ metakind_ubchildren=
 metakind_lbchildren=
 metakind_operatorKinds=
 
+use_theory_validations=
+theory_alternate_doc=
+
 seen_theory=false
 seen_theory_builtin=false
 
 function theory {
-  # theory T header
+  # theory ID T header
 
   lineno=${BASH_LINENO[0]}
 
+  if $seen_theory; then
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
+  fi
+
   # this script doesn't care about the theory class information, but
   # makes does make sure it's there
   seen_theory=true
@@ -81,6 +89,34 @@ function theory {
 // #include \"theory/$b/$2\""
 }
 
+function alternate {
+  # alternate ID name T header
+
+  lineno=${BASH_LINENO[0]}
+
+  if $seen_theory; then
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
+  fi
+
+  seen_theory=true
+  seen_endtheory=true
+
+  theory_id="$1"
+  name="$2"
+  theory_class="$3"
+  theory_header="$4"
+  theory_includes="${theory_includes}#include \"$theory_header\"
+"
+
+  use_theory_validations="${use_theory_validations}
+  if(theory == \"$name\") {
+    return true;
+  }"
+  theory_alternate_doc="$theory_alternate_doc$name - alternate implementation for $theory_id\\n\\
+"
+}
+
 function properties {
   # properties prop*
   lineno=${BASH_LINENO[0]}
@@ -366,6 +402,10 @@ check_builtin_theory_seen
 nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
   awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
 
+if [ -z "$theory_alternate_doc" ]; then
+  theory_alternate_doc="[none defined]"
+fi
+
 text=$(cat "$template")
 for var in \
     metakind_includes \
@@ -378,6 +418,8 @@ for var in \
     metakind_ubchildren \
     metakind_lbchildren \
     metakind_operatorKinds \
+    use_theory_validations \
+    theory_alternate_doc \
     template \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 864b444df..cc11147ed 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -603,12 +603,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic));
 
   // Add the theories
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-    d_theoryEngine->addTheory<TheoryTraits<THEORY>::theory_class>(THEORY);
-  CVC4_FOR_EACH_THEORY;
+  for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
+    TheoryConstructor::addTheory(d_theoryEngine, id);
+  }
 
   // global push/pop around everything, to ensure proper destruction
   // of context-dependent data structures
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 2d8012bfb..084a624f7 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -52,13 +52,13 @@ seen_theory=false
 seen_theory_builtin=false
 
 function theory {
-  # theory T header
+  # theory ID T header
 
   lineno=${BASH_LINENO[0]}
 
   if $seen_theory; then
-    echo "$kf:$lineno: theory declaration can only appear once" >&2
-    exit 1;
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
   fi
 
   # this script doesn't care about the theory class information, but
@@ -82,6 +82,20 @@ function theory {
   theory_id="$1"
 }
 
+function alternate {
+  # alternate ID name T header
+
+  lineno=${BASH_LINENO[0]}
+
+  if $seen_theory; then
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
+  fi
+
+  seen_theory=true
+  seen_endtheory=true
+}
+
 function properties {
   # properties prop*
   lineno=${BASH_LINENO[0]}
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 3edc7c140..97ede32d5 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -40,6 +40,7 @@ template=$1; shift
 
 theory_traits=
 theory_includes=
+theory_constructors=
 theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\
 "
 
@@ -72,13 +73,13 @@ seen_theory=false
 seen_theory_builtin=false
 
 function theory {
-  # theory T header
+  # theory ID T header
 
   lineno=${BASH_LINENO[0]}
 
   if $seen_theory; then
-    echo "$kf:$lineno: theory declaration can only appear once" >&2
-    exit 1;
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
   fi
 
   # this script doesn't care about the theory class information, but
@@ -109,6 +110,30 @@ function theory {
 "
 }
 
+function alternate {
+  # alternate ID name T header
+
+  lineno=${BASH_LINENO[0]}
+
+  if $seen_theory; then
+    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+    exit 1
+  fi
+
+  seen_theory=true
+  seen_endtheory=true
+
+  theory_header="$4"
+  theory_includes="${theory_includes}#include \"$theory_header\"
+"
+
+  eval "alternate_for_$1=\"\${alternate_for_$1}
+      if(options::theoryAlternates()[\\\"$2\\\"]) {
+        engine->addTheory< $3 >($1);
+        return;
+      }\""
+}
+
 function rewriter {
   # rewriter class header
   lineno=${BASH_LINENO[0]}
@@ -128,10 +153,17 @@ function endtheory {
 
   seen_endtheory=true
 
+  theory_constructors="${theory_constructors}
+    case $theory_id:
+\$alternate_for_$theory_id
+      engine->addTheory< $theory_class >($theory_id);
+      return;
+"
+
   theory_traits="${theory_traits}
 template<>
 struct TheoryTraits<${theory_id}> {
-    typedef ${theory_class} theory_class;
+    // typedef ${theory_class} theory_class;
     typedef ${rewriter_class} rewriter_class;
 
     static const bool isStableInfinite = ${theory_stable_infinite};
@@ -368,6 +400,8 @@ check_builtin_theory_seen
 
 ## output
 
+eval "theory_constructors=\"$theory_constructors\""
+
 # generate warnings about incorrect #line annotations in templates
 nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
   awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
@@ -377,6 +411,7 @@ for var in \
     theory_traits \
     theory_for_each_macro \
     theory_includes \
+    theory_constructors \
     template \
     type_enumerator_includes \
     mk_type_enumerator_type_constant_cases \
diff --git a/src/theory/options b/src/theory/options
index 5a523f0fa..5d752fca1 100644
--- a/src/theory/options
+++ b/src/theory/options
@@ -8,4 +8,8 @@ module THEORY "theory/options.h" Theory layer
 expert-option theoryOfMode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::theory::stringToTheoryOfMode :handler-include "theory/options_handlers.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "theory/theoryof_mode.h"
  mode for theoryof
 
+option - use-theory --use-theory=NAME argument :handler CVC4::theory::useTheory :handler-include "theory/options_handlers.h"
+ use alternate theory implementation NAME (--use-theory=help for a list)
+option theoryAlternates ::std::map<std::string,bool> :include <map> :read-write
+
 endmodule
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 */
 
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 */