diff options
Diffstat (limited to 'src/theory/mkrewriter')
| -rwxr-xr-x | src/theory/mkrewriter | 70 |
1 files changed, 54 insertions, 16 deletions
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index a53da2022..78fc39984 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -35,16 +35,16 @@ me=$(basename "$0") template=$1; shift -rewriter_includes= +rewriter_includes= rewrite_init= rewrite_shutdown= -pre_rewrite_calls= -pre_rewrite_get_cache= +pre_rewrite_calls= +pre_rewrite_get_cache= pre_rewrite_set_cache= post_rewrite_calls= -post_rewrite_get_cache= +post_rewrite_get_cache= post_rewrite_set_cache= seen_theory=false @@ -55,6 +55,11 @@ function theory { lineno=${BASH_LINENO[0]} + if $seen_theory; then + echo "$kf:$lineno: theory declaration can only appear once" >&2 + exit 1; + fi + # this script doesn't care about the theory class information, but # makes does make sure it's there seen_theory=true @@ -72,8 +77,8 @@ function theory { 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_id="$1" } function properties { @@ -86,32 +91,33 @@ function endtheory { # endtheory lineno=${BASH_LINENO[0]} check_theory_seen + seen_endtheory=true } function rewriter { # rewriter class header - class="$1" + class="$1" header="$2" rewriter_includes="${rewriter_includes}#include \"$header\" " rewrite_init="${rewrite_init} ${class}::init(); " - rewrite_shutdown="${rewrite_shutdown} ${class}::shutdown(); + 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_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); + 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); + 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]} @@ -119,7 +125,13 @@ function rewriter { } function sort { - # sort TYPE ["comment"] + # sort TYPE cardinality ["comment"] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function cardinality { + # cardinality TYPE cardinality-computer [header] lineno=${BASH_LINENO[0]} check_theory_seen } @@ -149,6 +161,10 @@ function constant { } 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 @@ -164,17 +180,39 @@ function check_builtin_theory_seen { while [ $# -gt 0 ]; do kf=$1 seen_theory=false + seen_endtheory=false b=$(basename $(dirname "$kf")) source "$kf" - check_theory_seen + 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 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 +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 \ + template \ + ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` |