diff options
Diffstat (limited to 'src/theory/mktheorytraits')
| -rwxr-xr-x | src/theory/mktheorytraits | 263 |
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" |