src/theory/mktheorytraits

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