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