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.

4 files changed, 100 insertions, 3 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 */
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}}"