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, 263 insertions, 0 deletions

diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
new file mode 100755
index 000000000..58e5e4381
--- /dev/null
+++ b/src/theory/mktheorytraits
@@ -0,0 +1,263 @@
+#!/bin/bash
+#
+# mktheorytraits
+# 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
+/*********************                                                        */
+/** theory_traits.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
+
+theory_traits=
+theory_includes=
+theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\
+"
+
+theory_has_check="false"
+theory_has_propagate="false"
+theory_has_static_learning="false"
+theory_has_presolve="false"
+
+theory_stable_infinite="false"
+theory_finite="false"
+theory_polite="false"
+
+rewriter_class=
+rewriter_header=
+  
+theory_id=
+theory_class=
+
+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"
+  theory_class="$2"
+  
+  theory_includes="${theory_includes}#include \"$3\"
+"
+  theory_for_each_macro="${theory_for_each_macro} CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::${theory_id}) \\
+"
+}
+
+function rewriter {
+  # rewriter class header
+  lineno=${BASH_LINENO[0]}
+  
+  rewriter_class="$1"
+  rewriter_header="$2"
+  
+  theory_includes="${theory_includes}#include \"$2\"
+"
+
+}
+
+function endtheory {
+  # endtheory
+  
+  theory_traits="${theory_traits}
+template<>
+struct TheoryTraits<${theory_id}> {
+    typedef ${theory_class} theory_class;
+    typedef ${rewriter_class} rewriter_class;
+    
+    static const bool isStableInfinite = ${theory_stable_infinite};
+    static const bool isFinite = ${theory_finite};
+    static const bool isPolite = ${theory_polite};
+    
+    static const bool hasCheck = ${theory_has_check};
+    static const bool hasPropagate = ${theory_has_propagate};
+    static const bool hasStaticLearning = ${theory_has_static_learning};
+    static const bool hasPresolve = ${theory_has_presolve};
+};
+"
+
+  theory_has_check="false"
+  theory_has_propagate="false"
+  theory_has_static_learning="false"
+  theory_has_presolve="false"
+
+  theory_stable_infinite="false"
+  theory_finite="false"
+  theory_polite="false"
+
+  rewriter_class=
+  rewriter_header=
+  
+  theory_id=
+  theory_class=
+  
+  lineno=${BASH_LINENO[0]}
+}
+
+
+function properties {
+  # properties property*
+  lineno=${BASH_LINENO[0]}
+  while (( $# )); 
+  do
+    property="$1"
+    case "$property" in 
+       finite) theory_finite="true";;
+       stable-infinite) theory_stable_infinite="true";;
+       polite) theory_polite="true";;
+       check) theory_has_check="true";;
+       propagate) theory_has_propagate="true";;
+       staticLearning) theory_has_static_learning="true";;
+       presolve) theory_has_presolve="true";
+    esac
+    shift
+  done;  
+}
+
+function sort {
+  # sort TYPE ["comment"]
+  
+  lineno=${BASH_LINENO[0]}
+  
+  check_theory_seen
+  register_sort "$1" "$2"
+}
+
+function variable {
+  # variable K ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_kind "$1" 0 "$2"
+}
+
+function operator {
+  # operator K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_kind "$1" "$2" "$3"
+}
+
+function parameterized {
+  # parameterized K1 K2 #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_kind "$1" "$3" "$4"
+}
+
+function constant {
+  # constant K T Hasher header ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_kind "$1" 0 "$5"
+}
+
+function register_sort {
+  id=$1
+  comment=$2
+  type_constant_to_theory_id="${type_constant_to_theory_id}   case $id: return $theory_id; break;
+" 
+}
+
+function register_kind {
+  r=$1
+  nc=$2
+  comment=$3
+  kind_to_theory_id="${kind_to_theory_id}   case kind::$r: return $theory_id; break;
+"
+}
+
+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"))
+  kind_decls="${kind_decls}
+  /* from $b */
+"
+  kind_printers="${kind_printers}
+  /* from $b */
+"
+  source "$kf"
+  check_theory_seen
+  shift
+done
+check_builtin_theory_seen
+
+## output
+
+text=$(cat "$template")
+for var in theory_traits theory_for_each_macro theory_includes; 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"