1#!/usr/bin/env bash 2# 3# mktheorytraits 4# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 5# Copyright (c) 2010-2013 The CVC4 Project 6# 7# The purpose of this script is to create theory_traits.h from a template 8# and a list of theory kinds. 9# 10# Invocation: 11# 12# mktheorytraits template-file theory-kind-files... 13# 14# Output is to standard out. 15# 16 17copyright=2010-2014 18 19filename=`basename "$1" | sed 's,_template,,'` 20 21cat <<EOF 22/********************* */ 23/** $filename 24 ** 25 ** Copyright $copyright New York University and The University of Iowa, 26 ** and as below. 27 ** 28 ** This header file automatically generated by: 29 ** 30 ** $0 $@ 31 ** 32 ** for the CVC4 project. 33 **/ 34 35EOF 36 37me=$(basename "$0") 38 39template=$1; shift 40 41theory_traits= 42theory_includes= 43theory_constructors= 44theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\ 45" 46 47type_enumerator_includes= 48mk_type_enumerator_cases= 49 50theory_has_check="false" 51theory_has_propagate="false" 52theory_has_ppStaticLearn="false" 53theory_has_notifyRestart="false" 54theory_has_presolve="false" 55theory_has_postsolve="false" 56 57theory_stable_infinite="false" 58theory_finite="false" 59theory_polite="false" 60theory_parametric="false" 61 62rewriter_class= 63rewriter_header= 64 65theory_id= 66theory_class= 67 68type_constants= 69type_kinds= 70 71seen_theory=false 72seen_theory_builtin=false 73 74function theory { 75 # theory ID T header 76 77 lineno=${BASH_LINENO[0]} 78 79 if $seen_theory; then 80 echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2 81 exit 1 82 fi 83 84 # this script doesn't care about the theory class information, but 85 # makes does make sure it's there 86 seen_theory=true 87 if [ "$1" = THEORY_BUILTIN ]; then 88 if $seen_theory_builtin; then 89 echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2 90 exit 1 91 fi 92 seen_theory_builtin=true 93 elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then 94 echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 95 exit 1 96 elif ! expr "$2" : '\(::*\)' >/dev/null; then 97 echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2 98 elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then 99 echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 100 fi 101 102 theory_id="$1" 103 theory_class="$2" 104 105 theory_header="$3" 106 theory_includes="${theory_includes}#include \"$theory_header\" 107" 108 theory_for_each_macro="${theory_for_each_macro} CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::${theory_id}) \\ 109" 110} 111 112function alternate { 113 # alternate ID name T header 114 115 lineno=${BASH_LINENO[0]} 116 117 if $seen_theory; then 118 echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2 119 exit 1 120 fi 121 122 seen_theory=true 123 seen_endtheory=true 124 125 theory_header="$4" 126 theory_includes="${theory_includes}#include \"$theory_header\" 127" 128 129 eval "alternate_for_$1=\"\${alternate_for_$1} 130 if(engine->useTheoryAlternative(\\\"$2\\\")) { 131 engine->addTheory< $3 >($1); 132 return; 133 }\"" 134} 135 136function rewriter { 137 # rewriter class header 138 lineno=${BASH_LINENO[0]} 139 check_theory_seen 140 141 rewriter_class="$1" 142 rewriter_header="$2" 143 144 theory_includes="${theory_includes}#include \"$2\" 145" 146} 147 148function endtheory { 149 # endtheory 150 lineno=${BASH_LINENO[0]} 151 check_theory_seen 152 153 seen_endtheory=true 154 155 theory_constructors="${theory_constructors} 156 case $theory_id: 157\$alternate_for_$theory_id 158 engine->addTheory< $theory_class >($theory_id); 159 return; 160" 161 162 theory_traits="${theory_traits} 163template<> 164struct TheoryTraits<${theory_id}> { 165 // typedef ${theory_class} theory_class; 166 typedef ${rewriter_class} rewriter_class; 167 168 static const bool isStableInfinite = ${theory_stable_infinite}; 169 static const bool isFinite = ${theory_finite}; 170 static const bool isPolite = ${theory_polite}; 171 static const bool isParametric = ${theory_parametric}; 172 173 static const bool hasCheck = ${theory_has_check}; 174 static const bool hasPropagate = ${theory_has_propagate}; 175 static const bool hasPpStaticLearn = ${theory_has_ppStaticLearn}; 176 static const bool hasNotifyRestart = ${theory_has_notifyRestart}; 177 static const bool hasPresolve = ${theory_has_presolve}; 178 static const bool hasPostsolve = ${theory_has_postsolve}; 179};/* struct TheoryTraits<${theory_id}> */ 180" 181 182 # warnings about theory content and properties 183 dir="$(dirname "$kf")/../../" 184 if [ -e "$dir/$theory_header" ]; then 185 for function in check propagate ppStaticLearn notifyRestart presolve postsolve; do 186 if eval "\$theory_has_$function"; then 187 grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' || 188 echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2 189 else 190 grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' && 191 echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2 192 fi 193 done 194 else 195 echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2 196 fi 197 198 theory_has_check="false" 199 theory_has_propagate="false" 200 theory_has_ppStaticLearn="false" 201 theory_has_notifyRestart="false" 202 theory_has_presolve="false" 203 theory_has_postsolve="false" 204 205 theory_stable_infinite="false" 206 theory_finite="false" 207 theory_polite="false" 208 theory_parametric="false" 209 210 rewriter_class= 211 rewriter_header= 212 213 theory_id= 214 theory_class= 215 216 type_constants= 217 type_kinds= 218 219 lineno=${BASH_LINENO[0]} 220} 221 222function enumerator { 223 # enumerator KIND enumerator-class header 224 lineno=${BASH_LINENO[0]} 225 check_theory_seen 226 type_enumerator_includes="${type_enumerator_includes} 227#line $lineno \"$kf\" 228#include \"$3\"" 229 if expr "$type_constants" : '.* '"$1"' ' &>/dev/null; then 230 mk_type_enumerator_type_constant_cases="${mk_type_enumerator_type_constant_cases} 231#line $lineno \"$kf\" 232 case $1: 233#line $lineno \"$kf\" 234 return new $2(type, tep); 235" 236 elif expr "$type_kinds" : '.* '"$1"' ' &>/dev/null; then 237 mk_type_enumerator_cases="${mk_type_enumerator_cases} 238#line $lineno \"$kf\" 239 case kind::$1: 240#line $lineno \"$kf\" 241 return new $2(type, tep); 242" 243 else 244 echo "$kf:$lineno: error: don't know anything about $1; enumerator must appear after definition" >&2 245 echo "type_constants: $type_constants" >&2 246 echo "type_kinds : $type_kinds" >&2 247 exit 1 248 fi 249} 250 251function typechecker { 252 # typechecker header 253 lineno=${BASH_LINENO[0]} 254 check_theory_seen 255} 256 257function typerule { 258 # typerule OPERATOR typechecking-class 259 lineno=${BASH_LINENO[0]} 260 check_theory_seen 261} 262 263function construle { 264 # construle OPERATOR isconst-checking-class 265 lineno=${BASH_LINENO[0]} 266 check_theory_seen 267} 268 269function properties { 270 # properties property* 271 lineno=${BASH_LINENO[0]} 272 check_theory_seen 273 while (( $# )); 274 do 275 property="$1" 276 case "$property" in 277 finite) theory_finite="true";; 278 stable-infinite) theory_stable_infinite="true";; 279 parametric) theory_parametric="true";; 280 polite) theory_polite="true";; 281 check) theory_has_check="true";; 282 propagate) theory_has_propagate="true";; 283 ppStaticLearn) theory_has_ppStaticLearn="true";; 284 presolve) theory_has_presolve="true";; 285 postsolve) theory_has_postsolve="true";; 286 notifyRestart) theory_has_notifyRestart="true";; 287 *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;; 288 esac 289 shift 290 done 291} 292 293function sort { 294 # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"] 295 lineno=${BASH_LINENO[0]} 296 check_theory_seen 297 if [ "$3" = well-founded ]; then 298 register_sort "$1" "$2" "$6" 299 else 300 register_sort "$1" "$2" "$4" 301 fi 302} 303 304function cardinality { 305 # cardinality TYPE cardinality-computer [header] 306 lineno=${BASH_LINENO[0]} 307 check_theory_seen 308} 309 310function well-founded { 311 # well-founded TYPE wellfoundedness-computer [header] 312 lineno=${BASH_LINENO[0]} 313 check_theory_seen 314} 315 316function variable { 317 # variable K ["comment"] 318 lineno=${BASH_LINENO[0]} 319 check_theory_seen 320 register_kind "$1" 0 "$2" 321} 322 323function operator { 324 # operator K #children ["comment"] 325 lineno=${BASH_LINENO[0]} 326 check_theory_seen 327 register_kind "$1" "$2" "$3" 328} 329 330function parameterized { 331 # parameterized K1 K2 #children ["comment"] 332 lineno=${BASH_LINENO[0]} 333 check_theory_seen 334 register_kind "$1" "$3" "$4" 335} 336 337function constant { 338 # constant K T Hasher header ["comment"] 339 lineno=${BASH_LINENO[0]} 340 check_theory_seen 341 register_kind "$1" 0 "$5" 342} 343 344function nullaryoperator { 345 # nullaryoperator K ["comment"] 346 lineno=${BASH_LINENO[0]} 347 check_theory_seen 348 register_kind "$1" 0 "$2" 349} 350 351function register_sort { 352 id=$1 353 cardinality=$2 354 comment=$3 355 type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; 356" 357 type_constants="${type_constants} $1 " 358} 359 360function register_kind { 361 r=$1 362 nc=$2 363 comment=$3 364 kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; 365" 366 type_kinds="${type_kinds} $1 " 367} 368 369function check_theory_seen { 370 if $seen_endtheory; then 371 echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 372 exit 1 373 fi 374 if ! $seen_theory; then 375 echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 376 exit 1 377 fi 378} 379 380function check_builtin_theory_seen { 381 if ! $seen_theory_builtin; then 382 echo "$me: warning: no declaration for the builtin theory found" >&2 383 fi 384} 385 386while [ $# -gt 0 ]; do 387 kf=$1 388 seen_theory=false 389 seen_endtheory=false 390 b=$(basename $(dirname "$kf")) 391 source "$kf" 392 if ! $seen_theory; then 393 echo "$kf: error: no theory content found in file!" >&2 394 exit 1 395 fi 396 if ! $seen_endtheory; then 397 echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 398 exit 1 399 fi 400 shift 401done 402check_builtin_theory_seen 403 404## output 405 406eval "theory_constructors=\"$theory_constructors\"" 407 408# generate warnings about incorrect #line annotations in templates 409nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | 410 awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2 411 412text=$(cat "$template") 413for var in \ 414 theory_traits \ 415 theory_for_each_macro \ 416 theory_includes \ 417 theory_constructors \ 418 template \ 419 type_enumerator_includes \ 420 mk_type_enumerator_type_constant_cases \ 421 mk_type_enumerator_cases \ 422 ; do 423 eval text="\${text//\\\$\\{$var\\}/\${$var}}" 424done 425error=`expr "$text" : '.*\${\([^}]*\)}.*'` 426if [ -n "$error" ]; then 427 echo "$template:0: error: undefined replacement \${$error}" >&2 428 exit 1 429fi 430echo "$text" 431