1 files changed, 242 insertions, 0 deletions
diff --git a/src/theory/mkinstantiator b/src/theory/mkinstantiator
new file mode 100755
index 000000000..1908d2e96
--- /dev/null
+++ b/src/theory/mkinstantiator
@@ -0,0 +1,242 @@
+#!/bin/bash
+#
+# mkinstantiator
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010-2012  The CVC4 Project
+#
+# The purpose of this script is to create rewriter_tables.h from a template
+# and a list of theory kinds.
+#
+# Invocation:
+#
+#   mkinstantiator template-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+copyright=2010-2012
+
+cat <<EOF
+/*********************                                                        */
+/** instantiator_tables.h
+ **
+ ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ **
+ ** This header file automatically generated by:
+ **
+ **     $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+EOF
+
+me=$(basename "$0")
+
+template=$1; shift
+
+instantiator_includes=
+instantiator_class=
+theory_id=
+theory_class=
+theory_header=
+
+make_instantiator_cases=
+instantiator=
+
+seen_theory=false
+seen_theory_builtin=false
+
+function theory {
+  # theory id T header
+
+  lineno=${BASH_LINENO[0]}
+
+  if $seen_theory; then
+    echo "$kf:$lineno: theory declaration can only appear once" >&2
+    exit 1;
+  fi
+
+  seen_theory=true
+  if [ "$1" = THEORY_BUILTIN ]; then
+    if $seen_theory_builtin; then
+      echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
+      exit 1
+    fi
+    seen_theory_builtin=true
+  elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
+    echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
+    exit 1
+  elif ! expr "$2" : '\(::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
+  elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
+  fi
+
+  theory_id="$1"
+  theory_class="$2"
+  theory_header="$3"
+
+  instantiator_class=
+  instantiator=NULL
+}
+
+function instantiator {
+  # instantiator class header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+
+  if [ -n "$instantiator_class" ]; then
+    echo "$kf:$lineno: error: cannot have two \"instantiator\" directives" >&2
+    exit 1
+  fi
+
+  instantiator_class="$1"
+  instantiator_header="$2"
+
+  if [ -z "$instantiator_class" -o -z "$instantiator_header" ]; then
+    echo "$kf:$lineno: error: \"instantiator\" directive missing class or header argument" >&2
+    exit 1
+  fi
+
+  instantiator_includes="${instantiator_includes}#include \"$theory_header\"
+#line $lineno \"$kf\"
+#include \"$instantiator_header\"
+"
+  instantiator="new $instantiator_class(c, qe, static_cast< $theory_class* >(this))";
+}
+
+function properties {
+  # properties prop*
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function endtheory {
+  # endtheory
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  seen_endtheory=true
+
+  make_instantiator_cases="${make_instantiator_cases}
+#line $lineno \"$kf\"
+  case $theory_id:
+    return $instantiator;
+"
+}
+
+function typechecker {
+  # typechecker header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function typerule {
+  # typerule OPERATOR typechecking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function rewriter {
+  # rewriter class header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function sort {
+  # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function cardinality {
+  # cardinality TYPE cardinality-computer [header]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function well-founded {
+  # well-founded TYPE wellfoundedness-computer [header]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function variable {
+  # variable K ["comment"]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function operator {
+  # operator K #children ["comment"]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function parameterized {
+  # parameterized K1 K2 #children ["comment"]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function constant {
+  # constant K T Hasher header ["comment"]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function check_theory_seen {
+  if $seen_endtheory; then
+    echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
+    exit 1
+  fi
+  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
+  seen_endtheory=false
+  b=$(basename $(dirname "$kf"))
+  source "$kf"
+  if ! $seen_theory; then
+    echo "$kf: error: no theory content found in file!" >&2
+    exit 1
+  fi
+  if ! $seen_endtheory; then
+    echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
+    exit 1
+  fi
+  shift
+done
+check_builtin_theory_seen
+
+## output
+
+# 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
+
+text=$(cat "$template")
+for var in \
+    instantiator_includes \
+    make_instantiator_cases \
+    template \
+    ; 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"