diff options
Diffstat (limited to 'src/theory/mkinstantiator')
| -rwxr-xr-x | src/theory/mkinstantiator | 254 |
1 files changed, 0 insertions, 254 deletions
diff --git a/src/theory/mkinstantiator b/src/theory/mkinstantiator deleted file mode 100755 index 73fc6706d..000000000 --- a/src/theory/mkinstantiator +++ /dev/null @@ -1,254 +0,0 @@ -#!/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 enumerator { - # enumerator KIND enumerator-class header - lineno=${BASH_LINENO[0]} - check_theory_seen -} - -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 construle { - # construle OPERATOR isconst-checking-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" |