src/theory/mktheorytraits

   1 #!/bin/bash
   2 #
   3 # mktheorytraits
   4 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
   5 # Copyright (c) 2010-2011  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-2011
  18
  19 cat <<EOF
  20 /*********************                                                        */
  21 /** theory_traits.h
  22  **
  23  ** Copyright $copyright  The AcSys Group, New York University, and as below.
  24  **
  25  ** This header file automatically generated by:
  26  **
  27  **     $0 $@
  28  **
  29  ** for the CVC4 project.
  30  **/
  31
  32 EOF
  33
  34 me=$(basename "$0")
  35
  36 template=$1; shift
  37
  38 theory_traits=
  39 theory_includes=
  40 theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\
  41 "
  42
  43 theory_has_check="false"
  44 theory_has_propagate="false"
  45 theory_has_staticLearning="false"
  46 theory_has_notifyRestart="false"
  47 theory_has_presolve="false"
  48 theory_has_postsolve="false"
  49
  50 theory_stable_infinite="false"
  51 theory_finite="false"
  52 theory_polite="false"
  53 theory_parametric="false"
  54
  55 rewriter_class=
  56 rewriter_header=
  57
  58 theory_id=
  59 theory_class=
  60
  61 seen_theory=false
  62 seen_theory_builtin=false
  63
  64 function theory {
  65   # theory T header
  66
  67   lineno=${BASH_LINENO[0]}
  68
  69   if $seen_theory; then
  70     echo "$kf:$lineno: theory declaration can only appear once" >&2
  71     exit 1;
  72   fi
  73
  74   # this script doesn't care about the theory class information, but
  75   # makes does make sure it's there
  76   seen_theory=true
  77   if [ "$1" = THEORY_BUILTIN ]; then
  78     if $seen_theory_builtin; then
  79       echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
  80       exit 1
  81     fi
  82     seen_theory_builtin=true
  83   elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
  84     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
  85     exit 1
  86   elif ! expr "$2" : '\(::*\)' >/dev/null; then
  87     echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
  88   elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
  89     echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
  90   fi
  91
  92   theory_id="$1"
  93   theory_class="$2"
  94
  95   theory_header="$3"
  96   theory_includes="${theory_includes}#include \"$theory_header\"
  97 "
  98   theory_for_each_macro="${theory_for_each_macro} CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::${theory_id}) \\
  99 "
 100 }
 101
 102 function rewriter {
 103   # rewriter class header
 104   lineno=${BASH_LINENO[0]}
 105   check_theory_seen
 106
 107   rewriter_class="$1"
 108   rewriter_header="$2"
 109
 110   theory_includes="${theory_includes}#include \"$2\"
 111 "
 112 }
 113
 114 function endtheory {
 115   # endtheory
 116   lineno=${BASH_LINENO[0]}
 117   check_theory_seen
 118
 119   seen_endtheory=true
 120
 121   theory_traits="${theory_traits}
 122 template<>
 123 struct TheoryTraits<${theory_id}> {
 124     typedef ${theory_class} theory_class;
 125     typedef ${rewriter_class} rewriter_class;
 126
 127     static const bool isStableInfinite = ${theory_stable_infinite};
 128     static const bool isFinite = ${theory_finite};
 129     static const bool isPolite = ${theory_polite};
 130     static const bool isParametric = ${theory_parametric};
 131
 132     static const bool hasCheck = ${theory_has_check};
 133     static const bool hasPropagate = ${theory_has_propagate};
 134     static const bool hasStaticLearning = ${theory_has_staticLearning};
 135     static const bool hasNotifyRestart = ${theory_has_notifyRestart};
 136     static const bool hasPresolve = ${theory_has_presolve};
 137     static const bool hasPostsolve = ${theory_has_postsolve};
 138 };/* struct TheoryTraits<${theory_id}> */
 139 "
 140
 141   # warnings about theory content and properties
 142   # TODO: fix, not corresponding to staticLearning anymore
 143   # dir="$(dirname "$kf")/../../"
 144   # if [ -e "$dir/$theory_header" ]; then
 145   #   for function in check propagate staticLearning notifyRestart presolve postsolve; do
 146   #      if eval "\$theory_has_$function"; then
 147   #        grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' ||
 148   #          echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2
 149   #      else
 150   #        grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' &&
 151   #          echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2
 152   #      fi
 153   #    done
 154   # else
 155   #   echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2
 156   # fi
 157
 158   theory_has_check="false"
 159   theory_has_propagate="false"
 160   theory_has_staticLearning="false"
 161   theory_has_notifyRestart="false"
 162   theory_has_presolve="false"
 163   theory_has_postsolve="false"
 164
 165   theory_stable_infinite="false"
 166   theory_finite="false"
 167   theory_polite="false"
 168   theory_parametric="false"
 169
 170   rewriter_class=
 171   rewriter_header=
 172
 173   theory_id=
 174   theory_class=
 175
 176   lineno=${BASH_LINENO[0]}
 177 }
 178
 179 function typechecker {
 180   # typechecker header
 181   lineno=${BASH_LINENO[0]}
 182   check_theory_seen
 183 }
 184
 185 function typerule {
 186   # typerule OPERATOR typechecking-class
 187   lineno=${BASH_LINENO[0]}
 188   check_theory_seen
 189 }
 190
 191 function properties {
 192   # properties property*
 193   lineno=${BASH_LINENO[0]}
 194   check_theory_seen
 195   while (( $# ));
 196   do
 197     property="$1"
 198     case "$property" in
 199        finite) theory_finite="true";;
 200        stable-infinite) theory_stable_infinite="true";;
 201        parametric) theory_parametric="true";;
 202        polite) theory_polite="true";;
 203        check) theory_has_check="true";;
 204        propagate) theory_has_propagate="true";;
 205        staticLearning) theory_has_staticLearning="true";;
 206        presolve) theory_has_presolve="true";;
 207        postsolve) theory_has_postsolve="true";;
 208        notifyRestart) theory_has_notifyRestart="true";;
 209        *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;;
 210     esac
 211     shift
 212   done
 213 }
 214
 215 function sort {
 216   # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
 217   lineno=${BASH_LINENO[0]}
 218   check_theory_seen
 219   if [ "$3" = well-founded ]; then
 220     register_sort "$1" "$2" "$6"
 221   else
 222     register_sort "$1" "$2" "$4"
 223   fi
 224 }
 225
 226 function cardinality {
 227   # cardinality TYPE cardinality-computer [header]
 228   lineno=${BASH_LINENO[0]}
 229   check_theory_seen
 230 }
 231
 232 function well-founded {
 233   # well-founded TYPE wellfoundedness-computer [header]
 234   lineno=${BASH_LINENO[0]}
 235   check_theory_seen
 236 }
 237
 238 function variable {
 239   # variable K ["comment"]
 240   lineno=${BASH_LINENO[0]}
 241   check_theory_seen
 242   register_kind "$1" 0 "$2"
 243 }
 244
 245 function operator {
 246   # operator K #children ["comment"]
 247   lineno=${BASH_LINENO[0]}
 248   check_theory_seen
 249   register_kind "$1" "$2" "$3"
 250 }
 251
 252 function parameterized {
 253   # parameterized K1 K2 #children ["comment"]
 254   lineno=${BASH_LINENO[0]}
 255   check_theory_seen
 256   register_kind "$1" "$3" "$4"
 257 }
 258
 259 function constant {
 260   # constant K T Hasher header ["comment"]
 261   lineno=${BASH_LINENO[0]}
 262   check_theory_seen
 263   register_kind "$1" 0 "$5"
 264 }
 265
 266 function register_sort {
 267   id=$1
 268   cardinality=$2
 269   comment=$3
 270   type_constant_to_theory_id="${type_constant_to_theory_id}   case $id: return $theory_id; break;
 271 "
 272 }
 273
 274 function register_kind {
 275   r=$1
 276   nc=$2
 277   comment=$3
 278   kind_to_theory_id="${kind_to_theory_id}   case kind::$r: return $theory_id; break;
 279 "
 280 }
 281
 282 function check_theory_seen {
 283   if $seen_endtheory; then
 284     echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
 285     exit 1
 286   fi
 287   if ! $seen_theory; then
 288     echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
 289     exit 1
 290   fi
 291 }
 292
 293 function check_builtin_theory_seen {
 294   if ! $seen_theory_builtin; then
 295     echo "$me: warning: no declaration for the builtin theory found" >&2
 296   fi
 297 }
 298
 299 while [ $# -gt 0 ]; do
 300   kf=$1
 301   seen_theory=false
 302   seen_endtheory=false
 303   b=$(basename $(dirname "$kf"))
 304   source "$kf"
 305   if ! $seen_theory; then
 306     echo "$kf: error: no theory content found in file!" >&2
 307     exit 1
 308   fi
 309   if ! $seen_endtheory; then
 310     echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
 311     exit 1
 312   fi
 313   shift
 314 done
 315 check_builtin_theory_seen
 316
 317 ## output
 318
 319 # generate warnings about incorrect #line annotations in templates
 320 nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
 321   awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
 322
 323 text=$(cat "$template")
 324 for var in \
 325     theory_traits \
 326     theory_for_each_macro \
 327     theory_includes \
 328     template \
 329     ; do
 330   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 331 done
 332 error=`expr "$text" : '.*\${\([^}]*\)}.*'`
 333 if [ -n "$error" ]; then
 334   echo "$template:0: error: undefined replacement \${$error}" >&2
 335   exit 1
 336 fi
 337 echo "$text"