src/theory/mktheorytraits

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