1 files changed, 0 insertions, 162 deletions
diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof
deleted file mode 100755
index 415668b49..000000000
--- a/src/theory/mktheoryof
+++ /dev/null
@@ -1,162 +0,0 @@
-#!/bin/bash
-#
-# mktheoryof
-# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010  The CVC4 Project
-#
-# The purpose of this script is to create theoryof_table.h from a
-# template and a list of theory kinds.
-#
-# Invocation:
-#
-#   mktheoryof template-file theory-kind-files...
-#
-# Output is to standard out.
-#
-
-copyright=2010
-
-cat <<EOF
-/*********************                                                        */
-/** theoryof_table.h
- **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
- **
- ** This header file automatically generated by:
- **
- **     $0 $@
- **
- ** for the CVC4 project.
- **/
-
-EOF
-
-template=$1; shift
-
-theoryof_table_forwards=
-theoryof_table_registers=
-
-seen_theory=false
-seen_theory_builtin=false
-
-function theory {
-  lineno=${BASH_LINENO[0]}
-
-  # this script doesn't care about the theory class information, but
-  # makes does make sure it's there
-  seen_theory=true
-  if [ "$1" = builtin ]; then
-    if $seen_theory_builtin; then
-      echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
-      exit 1
-    fi
-    seen_theory_builtin=true
-    shift
-  elif [ -z "$1" -o -z "$2" ]; then
-    echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
-    exit 1
-  elif ! expr "$1" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
-  elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
-  fi
-
-  decl=
-  last=
-  num=0
-  for ns in `echo "$1" | sed 's,::, ,g'`; do
-    if [ -n "$last" ]; then
-      decl="${decl}namespace $last { "
-      let ++num
-    fi
-    last="$ns"
-  done
-  decl="${decl}class $last;"
-  while [ $num -gt 0 ]; do
-    decl="${decl} }"
-    let --num
-  done
-
-  theoryof_table_forwards="${theoryof_table_forwards}$decl // #include \"theory/$b/$2\"
-"
-  theoryof_table_registers="${theoryof_table_registers}
-  /* from $b */
-  void registerTheory($1* th) {
-"
-}
-
-function variable {
-  # variable K ["comment"]
-
-  lineno=${BASH_LINENO[0]}
-
-  do_theoryof "$1"
-}
-
-function operator {
-  # operator K #children ["comment"]
-
-  lineno=${BASH_LINENO[0]}
-
-  do_theoryof "$1"
-}
-
-function parameterized {
-  # parameterized K #children ["comment"]
-
-  lineno=${BASH_LINENO[0]}
-
-  do_theoryof "$1"
-}
-
-function constant {
-  # constant K T Hasher header ["comment"]
-
-  lineno=${BASH_LINENO[0]}
-
-  do_theoryof "$1"
-}
-
-function do_theoryof {
-  check_theory_seen
-  theoryof_table_registers="${theoryof_table_registers}    d_table[::CVC4::kind::$1] = (Theory*)th;
-"
-}
-
-function check_theory_seen {
-  if ! $seen_theory; then
-    echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
-    exit 1
-  fi
-}
-
-function check_builtin_theory_seen {
-  if ! $seen_theory_builtin; then
-    echo "$me: warning: no declaration for the builtin theory found" >&2
-  fi
-}
-
-while [ $# -gt 0 ]; do
-  kf=$1
-  seen_theory=false
-  b=$(basename $(dirname "$kf"))
-  source "$kf"
-  check_theory_seen
-  theoryof_table_registers="${theoryof_table_registers}  }
-"
-  shift
-done
-check_builtin_theory_seen
-
-## output
-
-text=$(cat "$template")
-for var in theoryof_table_forwards theoryof_table_registers; do
-  eval text="\${text//\\\$\\{$var\\}/\${$var}}"
-done
-error=`expr "$text" : '.*\${\([^}]*\)}.*'`
-if [ -n "$error" ]; then
-  echo "$template:0: error: undefined replacement \${$error}" >&2
-  exit 1
-fi
-echo "$text"