1 files changed, 165 insertions, 0 deletions
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
new file mode 100755
index 000000000..8eb29bb15
--- /dev/null
+++ b/src/theory/mkrewriter
@@ -0,0 +1,165 @@
+#!/bin/bash
+#
+# mkrewriter
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010  The CVC4 Project
+#
+# The purpose of this script is to create kind.h from a template and a
+# list of theory kinds.
+#
+# Invocation:
+#
+#   mkkind template-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+copyright=2010
+
+cat <<EOF
+/*********************                                                        */
+/** kind.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
+
+rewriter_includes= 
+rewrite_init=
+rewrite_shutdown=
+
+pre_rewrite_calls= 
+pre_rewrite_get_cache= 
+pre_rewrite_set_cache=
+
+post_rewrite_calls=
+post_rewrite_get_cache= 
+post_rewrite_set_cache=
+
+seen_theory=false
+seen_theory_builtin=false
+
+function theory {
+  # theory T header
+
+  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" = 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"  
+}
+
+function properties {
+  # properties prop*
+  lineno=${BASH_LINENO[0]}
+}
+
+function endtheory {
+  # endtheory
+  lineno=${BASH_LINENO[0]}
+}
+
+function rewriter {
+  # rewriter class header
+  class="$1" 
+  header="$2"
+  
+  rewriter_includes="${rewriter_includes}#include \"$header\"
+"
+  rewrite_init="${rewrite_init}   ${class}::init();
+"
+  rewrite_shutdown="${rewrite_shutdown}    ${class}::shutdown(); 
+"
+
+  pre_rewrite_calls="${pre_rewrite_calls}    case ${theory_id}: return ${class}::preRewrite(node);
+"
+  pre_rewrite_get_cache="${pre_rewrite_get_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node); 
+"
+  pre_rewrite_set_cache="${pre_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache); 
+"
+
+  post_rewrite_calls="${post_rewrite_calls}    case ${theory_id}: return ${class}::postRewrite(node);
+"
+  post_rewrite_get_cache="${post_rewrite_get_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node); 
+" 
+  post_rewrite_set_cache="${post_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache); 
+"
+
+  lineno=${BASH_LINENO[0]}
+  
+}
+
+function sort {
+  # sort TYPE ["comment"]  
+  lineno=${BASH_LINENO[0]}
+}
+
+function variable {
+  # variable K ["comment"]
+  lineno=${BASH_LINENO[0]}
+}
+
+function operator {
+  # operator K #children ["comment"]
+  lineno=${BASH_LINENO[0]}
+}
+
+function parameterized {
+  # parameterized K1 K2 #children ["comment"]
+  lineno=${BASH_LINENO[0]}
+}
+
+function constant {
+  # constant K T Hasher header ["comment"]
+  lineno=${BASH_LINENO[0]}
+}
+
+while [ $# -gt 0 ]; do
+  kf=$1
+  seen_theory=false
+  b=$(basename $(dirname "$kf"))
+  source "$kf"
+  check_theory_seen
+  shift
+done
+check_builtin_theory_seen
+
+## output
+
+text=$(cat "$template")
+for var in rewriter_includes pre_rewrite_calls post_rewrite_calls pre_rewrite_get_cache post_rewrite_get_cache pre_rewrite_set_cache post_rewrite_set_cache rewrite_init rewrite_shutdown; 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"