Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

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"