4 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
5 # Copyright (c) 2010-2013 The CVC4 Project
7 # The purpose of this script is to create rewriter_tables.h from a template
8 # and a list of theory kinds.
12 # mkrewriter template-file theory-kind-files...
14 # Output is to standard out.
20 /********************* */
23 ** Copyright $copyright New York University and The University of Iowa,
26 ** This header file automatically generated by:
30 ** for the CVC4 project.
44 pre_rewrite_get_cache
=
45 pre_rewrite_set_cache
=
48 post_rewrite_get_cache
=
49 post_rewrite_set_cache
=
51 pre_rewrite_attribute_ids
=
52 post_rewrite_attribute_ids
=
55 seen_theory_builtin
=false
60 lineno
=${BASH_LINENO[0]}
63 echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
67 # this script doesn't care about the theory class information, but
68 # makes does make sure it's there
70 if [ "$1" = THEORY_BUILTIN
]; then
71 if $seen_theory_builtin; then
72 echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
75 seen_theory_builtin
=true
76 elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
77 echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
79 elif ! expr "$2" : '\(::*\)' >/dev
/null
; then
80 echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
81 elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev
/null
; then
82 echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
89 # alternate ID name T header
91 lineno
=${BASH_LINENO[0]}
94 echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
102 function properties
{
104 lineno
=${BASH_LINENO[0]}
110 lineno
=${BASH_LINENO[0]}
115 function enumerator
{
116 # enumerator KIND enumerator-class header
117 lineno
=${BASH_LINENO[0]}
121 function typechecker
{
123 lineno
=${BASH_LINENO[0]}
128 # typerule OPERATOR typechecking-class
129 lineno
=${BASH_LINENO[0]}
134 # construle OPERATOR isconst-checking-class
135 lineno
=${BASH_LINENO[0]}
140 # rewriter class header
144 rewriter_includes
="${rewriter_includes}#include \"$header\"
146 rewrite_init
="${rewrite_init} ${class}::init();
148 rewrite_shutdown
="${rewrite_shutdown} ${class}::shutdown();
150 pre_rewrite_attribute_ids
="${pre_rewrite_attribute_ids} preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::pre_rewrite()));
152 post_rewrite_attribute_ids
="${post_rewrite_attribute_ids} postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::post_rewrite()));
155 pre_rewrite_calls
="${pre_rewrite_calls} case ${theory_id}: return ${class}::preRewrite(node);
157 pre_rewrite_get_cache
="${pre_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node);
159 pre_rewrite_set_cache
="${pre_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache);
162 post_rewrite_calls
="${post_rewrite_calls} case ${theory_id}: return ${class}::postRewrite(node);
164 post_rewrite_get_cache
="${post_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node);
166 post_rewrite_set_cache
="${post_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache);
169 lineno
=${BASH_LINENO[0]}
174 # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
175 lineno
=${BASH_LINENO[0]}
179 function cardinality
{
180 # cardinality TYPE cardinality-computer [header]
181 lineno
=${BASH_LINENO[0]}
185 function well-founded
{
186 # well-founded TYPE wellfoundedness-computer [header]
187 lineno
=${BASH_LINENO[0]}
192 # variable K ["comment"]
193 lineno
=${BASH_LINENO[0]}
198 # operator K #children ["comment"]
199 lineno
=${BASH_LINENO[0]}
203 function parameterized
{
204 # parameterized K1 K2 #children ["comment"]
205 lineno
=${BASH_LINENO[0]}
210 # constant K T Hasher header ["comment"]
211 lineno
=${BASH_LINENO[0]}
215 function nullaryoperator
{
216 # nullaryoperator K ["comment"]
217 lineno
=${BASH_LINENO[0]}
221 function check_theory_seen
{
222 if $seen_endtheory; then
223 echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
226 if ! $seen_theory; then
227 echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
232 function check_builtin_theory_seen
{
233 if ! $seen_theory_builtin; then
234 echo "$me: warning: no declaration for the builtin theory found" >&2
238 while [ $# -gt 0 ]; do
242 b
=$
(basename $
(dirname "$kf"))
244 if ! $seen_theory; then
245 echo "$kf: error: no theory content found in file!" >&2
248 if ! $seen_endtheory; then
249 echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
254 check_builtin_theory_seen
258 # generate warnings about incorrect #line annotations in templates
259 nl -ba -s' ' "$template" |
grep '^ *[0-9][0-9]* # *line' |
260 awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
262 text
=$
(cat "$template")
267 pre_rewrite_get_cache \
268 post_rewrite_get_cache \
269 pre_rewrite_set_cache \
270 post_rewrite_set_cache \
271 rewrite_init rewrite_shutdown \
272 pre_rewrite_attribute_ids \
273 post_rewrite_attribute_ids \
276 eval text
="\${text//\\\$\\{$var\\}/\${$var}}"
278 error
=`expr "$text" : '.*\${\([^}]*\)}.*'`
279 if [ -n "$error" ]; then
280 echo "$template:0: error: undefined replacement \${$error}" >&2