src/options/mkoptions

   1 #!/bin/bash
   2 #
   3 # mkoptions
   4 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
   5 # Copyright (c) 2011-2014  The CVC4 Project
   6 #
   7 # The purpose of this script is to create options.{h,cpp}
   8 # from template files and a list of options.
   9 #
  10 # Invocation:
  11 #
  12 #   mkoptions (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+
  13 #
  14
  15 copyright=2011-2014
  16
  17 me=$(basename "$0")
  18
  19 function usage {
  20   echo "usage: $me (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+" >&2
  21 }
  22
  23 progress_char=/
  24 if [ -t 1 ]; then r="\r"; else r=""; fi
  25 function progress {
  26   file="$(expr "$1" : '.*\(.................................................................\)')"
  27   if [ -z "$file" ]; then file="$1"; else file="[...]$file"; fi
  28   [ -t 1 ] && printf "$r%c %-70s (%3d%%)" "$progress_char" "$file" "$(($2*100/$3))"
  29   progress_char="`echo "$progress_char" | tr -- '-\\\\|/' '\\\\|/-'`"
  30 }
  31
  32 function NOTE {
  33   printf "$r%-80s\n" "$kf:$lineno: note: $@"
  34 }
  35
  36 function WARN {
  37   printf "$r%-80s\n" "$kf:$lineno: warning: $@"
  38 }
  39
  40 function ERR {
  41   printf "$r%-80s\n" "$kf:$lineno: error: $@"
  42   exit 1
  43 }
  44
  45 declare -a templates
  46 declare -a outputs
  47
  48 while [ "$1" != -t ]; do
  49   if [ "$#" -lt 2 ]; then
  50     echo "$me: error: expected -t on command line" >&2
  51     usage
  52     exit 1
  53   fi
  54   templates[${#templates[@]}]="$1"; shift
  55   if [ "$1" = -t ]; then
  56     echo "$me: error: mismatched number of templates and output files (before -t)" >&2
  57     usage
  58     exit 1
  59   fi
  60   outputs[${#outputs[@]}]="$1"; shift
  61 done
  62
  63 shift
  64 if [ "$#" -lt 3 ]; then
  65   echo "$me: error: not enough arguments" >&2
  66   usage
  67   exit 1
  68 fi
  69
  70 options_h_template="$1"; shift
  71 options_cpp_template="$1"; shift
  72
  73 all_modules_defaults=
  74 all_modules_short_options=
  75 all_modules_long_options=
  76 all_modules_smt_options=
  77 all_modules_option_handlers=
  78 all_modules_get_options=
  79 smt_getoption_handlers=
  80 smt_setoption_handlers=
  81 include_all_option_headers=
  82 all_modules_contributions=
  83 option_handler_includes=
  84 all_custom_handlers=
  85 common_documentation=
  86 remaining_documentation=
  87 common_manpage_documentation=
  88 remaining_manpage_documentation=
  89 common_manpage_smt_documentation=
  90 remaining_manpage_smt_documentation=
  91 common_manpage_internals_documentation=
  92 remaining_manpage_internals_documentation=
  93
  94 seen_module=false
  95 seen_endmodule=false
  96 expect_doc=false
  97 expect_doc_alternate=false
  98 seen_doc=false
  99 n_long=256
 100
 101 internal=
 102 smtname=
 103 short_option=
 104 short_option_alternate=
 105 long_option=
 106 long_option_alternate=
 107 long_option_alternate_set=
 108 type=
 109 predicates=
 110
 111 # just for duplicates-checking
 112 all_declared_internal_options=
 113 all_declared_long_options=
 114 all_declared_short_options=
 115 all_declared_smt_options=
 116
 117 long_option_value_begin=$n_long
 118
 119 function module {
 120   # module id name
 121
 122   module_id=
 123   module_name=
 124   module_includes=
 125   module_optionholder_spec=
 126   module_decls=
 127   module_specializations=
 128   module_inlines=
 129   module_accessors=
 130   module_global_definitions=
 131
 132   seen_module=true
 133   if [ $# -lt 3 -o -z "$1" -o -z "$2" -o -z "$3" ]; then
 134     ERR "\"module\" directive requires exactly three arguments"
 135   fi
 136
 137   module_id="$1"; shift
 138   include="$1"; shift
 139   module_name="$@"
 140   include_all_option_headers="${include_all_option_headers}
 141 #line $lineno \"$kf\"
 142 #include $(check_include "$include")"
 143   all_modules_contributions="${all_modules_contributions}
 144   CVC4_OPTIONS__${module_id}__FOR_OPTION_HOLDER"
 145   module_optionholder_spec="#define CVC4_OPTIONS__${module_id}__FOR_OPTION_HOLDER"
 146
 147   previous_remaining_documentation="${remaining_documentation}"
 148   remaining_documentation="${remaining_documentation}\\n\\n\"
 149 #line $lineno \"$kf\"
 150 \"From the $module_name module:"
 151   remaining_documentation_at_start_of_module="${remaining_documentation}"
 152
 153   previous_remaining_manpage_documentation="${remaining_manpage_documentation}"
 154   remaining_manpage_documentation="${remaining_manpage_documentation}
 155 .SH `echo "$module_name" | tr a-z A-Z` OPTIONS
 156 "
 157   remaining_manpage_documentation_at_start_of_module="${remaining_manpage_documentation}"
 158
 159   previous_remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}"
 160   remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
 161 .TP
 162 .I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\"
 163 "
 164   remaining_manpage_smt_documentation_at_start_of_module="${remaining_manpage_smt_documentation}"
 165
 166   previous_remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}"
 167   remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
 168 .TP
 169 .I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\"
 170 "
 171   remaining_manpage_internals_documentation_at_start_of_module="${remaining_manpage_internals_documentation}"
 172 }
 173
 174 function endmodule {
 175   # endmodule
 176   check_module_seen
 177   check_doc
 178   seen_endmodule=true
 179   if [ $# -ne 0 ]; then
 180     ERR "endmodule takes no arguments"
 181   fi
 182
 183   # check, and if no documented options, remove the headers
 184
 185   if [ "$remaining_documentation" = "$remaining_documentation_at_start_of_module" ]; then
 186     remaining_documentation="$previous_remaining_documentation"
 187   fi
 188
 189   if [ "$remaining_manpage_documentation" = "$remaining_manpage_documentation_at_start_of_module" ]; then
 190     remaining_manpage_documentation="$previous_remaining_manpage_documentation"
 191   fi
 192
 193   if [ "$remaining_manpage_smt_documentation" = "$remaining_manpage_smt_documentation_at_start_of_module" ]; then
 194     remaining_manpage_smt_documentation="$previous_remaining_manpage_smt_documentation"
 195   fi
 196
 197   if [ "$remaining_manpage_internals_documentation" = "$remaining_manpage_internals_documentation_at_start_of_module" ]; then
 198     remaining_manpage_internals_documentation="$previous_remaining_manpage_internals_documentation"
 199   fi
 200 }
 201
 202 function common-option {
 203   # common-option option-args...
 204   handle_option COMMON "$@"
 205 }
 206
 207 function option {
 208   # option option-args...
 209   handle_option STANDARD "$@"
 210 }
 211
 212 function expert-option {
 213   # expert-option option-args...
 214   handle_option EXPERT "$@"
 215 }
 216
 217 function undocumented-option {
 218   # undocumented-option option-args...
 219   handle_option UNDOCUMENTED "$@"
 220 }
 221
 222 function handle_option {
 223   check_module_seen
 224   check_doc
 225
 226   args=("$@")
 227
 228   category="${args[0]}"
 229   internal="${args[1]}"
 230   smtname=
 231   short_option=
 232   short_option_alternate=
 233   long_option=
 234   long_option_alternate=
 235   long_option_alternate_set=
 236   type=
 237   readOnly=true
 238   required_argument=false
 239   default_value=
 240   handlers=
 241   predicates=
 242   links=
 243   links_alternate=
 244   smt_links=
 245
 246   options_already_documented=false
 247   alternate_options_already_documented=false
 248
 249   if [ "$category" = UNDOCUMENTED ]; then
 250     expect_doc=false
 251   else
 252     expect_doc=true
 253   fi
 254   expect_doc_alternate=false
 255   seen_doc=false
 256
 257   # scan ahead to see where the type is
 258   type_pos=2
 259   while [ $(($type_pos+1)) -lt ${#args[@]} ] && ! expr "${args[$(($type_pos+1))]}" : '\:' &>/dev/null; do
 260     let ++type_pos
 261   done
 262
 263   type="${args[$type_pos]}"
 264
 265   if [ "$type" = argument ]; then
 266     type=void
 267     required_argument=true
 268   fi
 269
 270   if [ $type_pos -eq 2 ]; then
 271     expect_doc=false
 272     readOnly=false
 273   else
 274     i=2
 275     while [ $i -lt $type_pos ]; do
 276       if expr "${args[$i]}" : '\--' &>/dev/null || expr "${args[$i]}" : '/--' &>/dev/null; then
 277         if [ -n "$long_option" -o -n "$long_option_alternate" ]; then
 278           ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
 279         fi
 280         long_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
 281         if [ -n "$long_option" ]; then
 282           if ! expr "$long_option" : '\--.' &>/dev/null; then
 283             ERR "bad long option \`$long_option': expected something like \`--foo'"
 284           fi
 285           long_option="$(echo "$long_option" | sed 's,^--,,')"
 286         fi
 287         if expr "${args[$i]}" : '.*/' &>/dev/null; then
 288           long_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
 289           long_option_alternate_set=set
 290           if [ -n "$long_option_alternate" ]; then
 291             if ! expr "$long_option_alternate" : '\--.' &>/dev/null; then
 292               ERR "bad alternate long option \`$long_option_alternate': expected something like \`--foo'"
 293             fi
 294             long_option_alternate="$(echo "$long_option_alternate" | sed 's,^--,,')"
 295           fi
 296         fi
 297       elif expr "${args[$i]}" : '\-' &>/dev/null || expr "${args[$i]}" : '/-' &>/dev/null; then
 298         if [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
 299           ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
 300         fi
 301         short_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
 302         if [ -n "$short_option" ]; then
 303           if ! expr "$short_option" : '\-.$' &>/dev/null; then
 304             ERR "bad short option \`$short_option': expected something like \`-x'"
 305           fi
 306           short_option="$(echo "$short_option" | sed 's,^-,,')"
 307         fi
 308         if expr "${args[$i]}" : '.*/' &>/dev/null; then
 309           short_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
 310           if expr "$short_option_alternate" : '\-' &>/dev/null; then
 311             if ! expr "$short_option_alternate" : '\-.$' &>/dev/null; then
 312               ERR "bad alternate short option \`$short_option_alternate': expected something like \`-x'"
 313             fi
 314             short_option_alternate="$(echo "$short_option_alternate" | sed 's,^-,,')"
 315           fi
 316         fi
 317       else
 318         if [ -n "$smtname" -o -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
 319           ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
 320         fi
 321         smtname="${args[$i]}"
 322       fi
 323       let ++i
 324     done
 325   fi
 326
 327   if [ "$type" = void -a "$internal" != - ]; then
 328     ERR "$internal cannot be void-typed; use \`-' as the name if its to be void"
 329   elif [ "$type" != void -a "$internal" = - ]; then
 330     ERR "cannot use an unnamed option if its type is not void"
 331   fi
 332
 333   if [ "$type" = bool -a -n "$long_option$short_option" -a "$category" != UNDOCUMENTED ]; then
 334     if [ -n "$short_option_alternate" -o -n "$long_option_alternate" ]; then
 335       expect_doc_alternate=true
 336     fi
 337   fi
 338   if [ "$type" = bool -a -n "$long_option" -a -z "$long_option_alternate" -a -z "$long_option_alternate_set" ]; then
 339     long_option_alternate="no-$(echo "$long_option" | sed 's,^--,,')"
 340   fi
 341   if [ "$type" != bool -a -n "$short_option_alternate" ]; then
 342     ERR "cannot use alternate short option -$short_option_alternate for \`$internal' because it's not of bool type"
 343   elif [ "$type" != bool -a -n "$long_option_alternate" ]; then
 344     ERR "cannot use alternate long option --$long_option_alternate for \`$internal' because it's not of bool type"
 345   fi
 346
 347   # check that normal options are accessible via SmtEngine too
 348   if [ -n "$long_option$short_option$long_option_alternate$short_option_alternate" -a -z "$smtname" -a "$internal" != - ]; then
 349     if [ -n "$long_option" ]; then
 350       smtname="$long_option"
 351     else
 352       WARN "$internal is inaccessible via SmtEngine (no smt name for option) but can be set via command-line: $long_option $short_option $long_option_alternate $short_option_alternate"
 353     fi
 354   fi
 355
 356   # check for duplicates
 357   if [ "$internal" != - ]; then
 358     if echo " $all_declared_internal_options " | grep -q " $internal "; then
 359       ERR "internal option name \`$internal' previously declared"
 360     fi
 361     all_declared_internal_options="$all_declared_internal_options $internal"
 362   fi
 363   if [ -n "$long_option" ]; then
 364     if echo " $all_declared_long_options " | grep -q " $long_option "; then
 365       ERR "long option name \`--$long_option' previously declared"
 366     fi
 367     all_declared_long_options="$all_declared_long_options $long_option"
 368   fi
 369   if [ -n "$long_option_alternate" ]; then
 370     if echo " $all_declared_long_options " | grep -q " $long_option_alternate "; then
 371       ERR "long option name \`--$long_option_alternate' previously declared"
 372     fi
 373     all_declared_long_options="$all_declared_long_options $long_option_alternate"
 374   fi
 375   if [ -n "$short_option" ]; then
 376     if echo " $all_declared_short_options " | grep -q " $short_option "; then
 377       ERR "short option name \`-$short_option' previously declared"
 378     fi
 379     all_declared_short_options="$all_declared_short_options $short_option"
 380   fi
 381   if [ -n "$short_option_alternate" ]; then
 382     if echo " $all_declared_short_options " | grep -q " $short_option_alternate "; then
 383       ERR "short option name \`-$short_option_alternate' previously declared"
 384     fi
 385     all_declared_short_options="$all_declared_short_options $short_option_alternate"
 386   fi
 387   if [ -n "$smtname" ]; then
 388     if echo " $all_declared_smt_options " | grep -q " $smtname "; then
 389       ERR "SMT option name \`$smtname' previously declared"
 390     fi
 391     all_declared_smt_options="$all_declared_smt_options $smtname"
 392   fi
 393
 394   # parse attributes
 395   i=$(($type_pos+1))
 396   while [ $i -lt ${#args[@]} ]; do
 397     attribute="${args[$i]}"
 398     case "$attribute" in
 399     :default)
 400        let ++i
 401        default_value="${args[$i]}"
 402        ;;
 403     :handler)
 404        let ++i
 405        if [ -n "$handlers" ]; then
 406          ERR "cannot specify more than one handler; maybe you want a :handler and a :predicate"
 407        fi
 408        handlers="${args[$i]}"
 409        ;;
 410     :predicate)
 411        while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
 412          let ++i
 413          predicates="${predicates} ${args[$i]}"
 414        done
 415        ;;
 416     :link)
 417        while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
 418          let ++i
 419          link="${args[$i]}"
 420          if expr "${args[$i]}" : '.*/' &>/dev/null; then
 421            links="${links} $(echo "${args[$i]}" | sed 's,/.*,,')"
 422            links_alternate="${links_alternate} $(echo "${args[$i]}" | sed 's,[^/]*/,,')"
 423          else
 424            links="${links} ${args[$i]}"
 425          fi
 426        done
 427        ;;
 428     :link-smt)
 429        j=0
 430        while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
 431          let ++i
 432          let ++j
 433          if [ $j -eq 3 ]; then
 434            echo "$kf:$lineno: error: attribute :link-smt can only take two arguments" >&2
 435            exit 1
 436          fi
 437          if expr "${args[$i]}" : '.*/' &>/dev/null; then
 438            echo "$kf:$lineno: error: attribute :link-smt cannot take alternates" >&2
 439            exit 1
 440          fi
 441          smt_links="${smt_links} ${args[$i]}"
 442        done
 443        if [ $j -eq 1 ]; then
 444          smt_links="${smt_links} \"true\""
 445        fi
 446        ;;
 447     :include)
 448        while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
 449          let ++i
 450          module_includes="${module_includes}
 451 #line $lineno \"$kf\"
 452 #include $(check_include "${args[$i]}")"
 453        done
 454        ;;
 455     :handler-include|:predicate-include)
 456        while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
 457          let ++i
 458          option_handler_includes="${option_handler_includes}
 459 #line $lineno \"$kf\"
 460 #include $(check_include "${args[$i]}")"
 461        done
 462        ;;
 463     :read-write)
 464        readOnly=false
 465        ;;
 466     :read-only)
 467        readOnly=true
 468        ;;
 469     *)
 470        ERR "error in option \`$internal': bad attribute \`$attribute'"
 471     esac
 472     let ++i
 473   done
 474
 475   # set up structures
 476   if [ "$internal" != - ]; then
 477     # set up a field in the options_holder
 478     module_optionholder_spec="${module_optionholder_spec} \\
 479   ${internal}__option_t::type $internal; \\
 480   bool ${internal}__setByUser__;"
 481     all_modules_defaults="${all_modules_defaults:+${all_modules_defaults},}
 482 #line $lineno \"$kf\"
 483   $internal($default_value),
 484 #line $lineno \"$kf\"
 485   ${internal}__setByUser__(false)"
 486     if $readOnly; then
 487       module_decls="${module_decls}
 488 #line $lineno \"$kf\"
 489 extern struct CVC4_PUBLIC ${internal}__option_t { typedef $type type; type operator()() const; bool wasSetByUser() const; } $internal CVC4_PUBLIC;"
 490       module_inlines="${module_inlines}
 491 #line $lineno \"$kf\"
 492 inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return Options::current()[*this]; }
 493 #line $lineno \"$kf\"
 494 inline bool ${internal}__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
 495 "
 496     else
 497       module_decls="${module_decls}
 498 #line $lineno \"$kf\"
 499 extern struct CVC4_PUBLIC ${internal}__option_t { typedef $type type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } $internal CVC4_PUBLIC;"
 500       module_inlines="${module_inlines}
 501 #line $lineno \"$kf\"
 502 inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return Options::current()[*this]; }
 503 #line $lineno \"$kf\"
 504 inline bool ${internal}__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
 505 #line $lineno \"$kf\"
 506 inline void ${internal}__option_t::set(const ${internal}__option_t::type& v) { Options::current().set(*this, v); }
 507 "
 508       module_specializations="${module_specializations}
 509 #line $lineno \"$kf\"
 510 template <> void Options::set(options::${internal}__option_t, const options::${internal}__option_t::type& x);"
 511       module_accessors="${module_accessors}
 512 #line $lineno \"$kf\"
 513 template <> void Options::set(options::${internal}__option_t, const options::${internal}__option_t::type& x) { d_holder->$internal = x; }"
 514     fi
 515     module_global_definitions="${module_global_definitions}
 516 #line $lineno \"$kf\"
 517 struct ${internal}__option_t $internal;"
 518     module_specializations="${module_specializations}
 519 #line $lineno \"$kf\"
 520 template <> const options::${internal}__option_t::type& Options::operator[](options::${internal}__option_t) const;
 521 #line $lineno \"$kf\"
 522 template <> bool Options::wasSetByUser(options::${internal}__option_t) const;"
 523     if [ "$type" = bool ]; then
 524       module_specializations="${module_specializations}
 525 #line $lineno \"$kf\"
 526 template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, SmtEngine* smt);"
 527     elif [ "$internal" != - ]; then
 528       module_specializations="${module_specializations}
 529 #line $lineno \"$kf\"
 530 template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt);"
 531     fi
 532
 533     module_accessors="${module_accessors}
 534 #line $lineno \"$kf\"
 535 template <> const options::${internal}__option_t::type& Options::operator[](options::${internal}__option_t) const { return d_holder->$internal; }
 536 #line $lineno \"$kf\"
 537 template <> bool Options::wasSetByUser(options::${internal}__option_t) const { return d_holder->${internal}__setByUser__; }"
 538   fi
 539
 540   if $required_argument || [ "$type" != bool -a "$type" != void ]; then
 541     expect_arg=:
 542     expect_arg_long=required_argument
 543   else
 544     expect_arg=
 545     expect_arg_long=no_argument
 546   fi
 547   cases=
 548   cases_alternate=
 549   if [ -n "$short_option" ]; then
 550     all_modules_short_options="${all_modules_short_options}$short_option$expect_arg"
 551     cases="${cases}
 552     case '$short_option':"
 553   fi
 554   if [ -n "$short_option_alternate" ]; then
 555     all_modules_short_options="${all_modules_short_options}$short_option_alternate$expect_arg"
 556     cases_alternate="${cases_alternate}
 557     case '$short_option_alternate':"
 558   fi
 559   if [ -n "$long_option" ]; then
 560     all_modules_long_options="${all_modules_long_options}
 561   { \"$(echo "$long_option" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long },"
 562     cases="${cases}
 563     case $n_long:// --$long_option"
 564     let ++n_long
 565   fi
 566   if [ -n "$long_option_alternate" ]; then
 567     all_modules_long_options="${all_modules_long_options}
 568   { \"$(echo "$long_option_alternate" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long },"
 569     cases_alternate="${cases_alternate}
 570     case $n_long:// --$long_option_alternate"
 571     let ++n_long
 572   fi
 573   run_links=
 574   run_links_alternate=
 575   run_smt_links=
 576   if [ -n "$links" -a -z "$smt_links" -a -n "$smtname" ]; then
 577     WARN "$smtname has no :link-smt, but equivalent command-line has :link"
 578   elif [ -n "$smt_links" -a -z "$links" ] && [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o "$long_option_alternate" ]; then
 579     WARN "$smtname has a :link-smt, but equivalent command-line has no :link"
 580   fi
 581   if [ -n "$links" ]; then
 582     # command-line links
 583     for link in $links; do
 584       run_links="$run_links
 585 #line $lineno \"$kf\"
 586       preemptGetopt(extra_argc, extra_argv, \"$link\");"
 587     done
 588   fi
 589   if [ -n "$smt_links" ]; then
 590     # smt links
 591     smt_links=($smt_links)
 592     i=0
 593     while [ $i -lt ${#smt_links[@]} ]; do
 594       run_smt_links="$run_smt_links
 595 #line $lineno \"$kf\"
 596     smt->setOption(std::string(\"${smt_links[$i]}\"), SExpr(${smt_links[$(($i+1))]}));"
 597       i=$((i+2))
 598     done
 599   fi
 600   if [ -n "$links_alternate" ]; then
 601     # command-line links
 602     for link in $links_alternate; do
 603       run_links_alternate="$run_links_alternate
 604 #line $lineno \"$kf\"
 605       preemptGetopt(extra_argc, extra_argv, \"$link\");"
 606     done
 607   fi
 608   if [ "$type" = bool ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then
 609     run_handlers=
 610     if [ -n "$handlers" ]; then
 611       ERR "bool-valued options cannot have handlers"
 612     fi
 613     if [ -n "$predicates" ]; then
 614       for predicate in $predicates; do
 615         run_handlers="$run_handlers
 616 #line $lineno \"$kf\"
 617   $predicate(option, b, smt);"
 618       done
 619     fi
 620     if [ -n "$run_handlers" ]; then
 621       all_custom_handlers="${all_custom_handlers}
 622 #line $lineno \"$kf\"
 623 template <> void runBoolPredicates(options::${internal}__option_t, std::string option, bool b, SmtEngine* smt) {
 624   $run_handlers
 625 }"
 626     fi
 627   fi
 628   if [ -n "$cases" ]; then
 629     if [ "$type" = bool ]; then
 630       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 631 #line $lineno \"$kf\"
 632       assignBool(options::$internal, option, true, NULL);$run_links
 633       break;
 634 "
 635     elif [ -n "$expect_arg" -a "$internal" != - ]; then
 636       run_handlers=
 637       if [ -n "$handlers" ]; then
 638         for handler in $handlers; do
 639           run_handlers="$run_handlers
 640 #line $lineno \"$kf\"
 641   $handler(option, optionarg, smt);"
 642         done
 643       else
 644         run_handlers="
 645 #line $lineno \"$kf\"
 646   handleOption<$type>(option, optionarg);"
 647       fi
 648       if [ -n "$predicates" ]; then
 649         for predicate in $predicates; do
 650           run_handlers="$run_handlers
 651 #line $lineno \"$kf\"
 652   $predicate(option, retval, smt);"
 653         done
 654       fi
 655       all_custom_handlers="${all_custom_handlers}
 656 #line $lineno \"$kf\"
 657 template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optionarg, SmtEngine* smt) {
 658 #line $lineno \"$kf\"
 659   options::${internal}__option_t::type retval = $run_handlers
 660 #line $lineno \"$kf\"
 661   return retval;
 662 }"
 663       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 664 #line $lineno \"$kf\"
 665       assign(options::$internal, option, optionarg, NULL);$run_links
 666       break;
 667 "
 668     elif [ -n "$expect_arg" ]; then
 669       run_handlers=
 670       if [ -n "$predicates" ]; then
 671         ERR "void-valued options cannot have predicates"
 672       fi
 673       if [ -n "$handlers" ]; then
 674         for handler in $handlers; do
 675           run_handlers="$run_handlers
 676 #line $lineno \"$kf\"
 677       $handler(option, optionarg, smt);"
 678         done
 679       fi
 680       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 681 #line $lineno \"$kf\"
 682       $run_handlers$run_links
 683       break;
 684 "
 685     else
 686       run_handlers=
 687       if [ -n "$predicates" ]; then
 688         ERR "void-valued options cannot have predicates"
 689       fi
 690       if [ -n "$handlers" ]; then
 691         for handler in $handlers; do
 692           run_handlers="$run_handlers
 693 #line $lineno \"$kf\"
 694       $handler(option, smt);"
 695         done
 696       fi
 697       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 698 #line $lineno \"$kf\"
 699       $run_handlers$run_links
 700       break;
 701 "
 702     fi
 703   fi
 704   if [ -n "$cases_alternate" ]; then
 705     if [ "$type" = bool ]; then
 706       all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate}
 707 #line $lineno \"$kf\"
 708       assignBool(options::$internal, option, false, NULL);$run_links_alternate
 709       break;
 710 "
 711     else
 712       ERR "internal error: expected BOOL-typed option in alternate handler"
 713     fi
 714   fi
 715
 716   if [ -n "$smtname" ]; then
 717     all_modules_smt_options="${all_modules_smt_options:+$all_modules_smt_options,}
 718 #line $lineno \"$kf\"
 719   \"$smtname\""
 720     if [ "$internal" != - ]; then
 721       case "$type" in
 722       bool)
 723         all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
 724 #line $lineno \"$kf\"
 725   }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(SExpr::Keyword(d_holder->$internal ? \"true\" : \"false\")); opts.push_back(v); }"
 726         smt_getoption_handlers="${smt_getoption_handlers}
 727 #line $lineno \"$kf\"
 728   if(key == \"$smtname\") {
 729 #line $lineno \"$kf\"
 730     return SExprKeyword(options::$internal() ? \"true\" : \"false\");
 731   }";;
 732       int|unsigned|int*_t|uint*_t|unsigned\ long|long|CVC4::Integer)
 733         all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
 734 #line $lineno \"$kf\"
 735   }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(d_holder->$internal); opts.push_back(v); }"
 736         smt_getoption_handlers="${smt_getoption_handlers}
 737 #line $lineno \"$kf\"
 738   if(key == \"$smtname\") {
 739 #line $lineno \"$kf\"
 740     return SExpr(Integer(options::$internal()));
 741   }";;
 742       float|double)
 743         all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
 744 #line $lineno \"$kf\"
 745   }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(Rational::fromDouble(d_holder->$internal)); opts.push_back(v); }"
 746         smt_getoption_handlers="${smt_getoption_handlers}
 747 #line $lineno \"$kf\"
 748   if(key == \"$smtname\") {
 749 #line $lineno \"$kf\"
 750     stringstream ss; ss << std::fixed << options::$internal();
 751     return SExpr(Rational::fromDecimal(ss.str()));
 752   }";;
 753       CVC4::Rational)
 754         all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
 755 #line $lineno \"$kf\"
 756   }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(d_holder->$internal); opts.push_back(v); }"
 757         smt_getoption_handlers="${smt_getoption_handlers}
 758 #line $lineno \"$kf\"
 759   if(key == \"$smtname\") {
 760 #line $lineno \"$kf\"
 761     return SExpr(options::$internal());
 762   }";;
 763       *)
 764         all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
 765 #line $lineno \"$kf\"
 766   }{ std::stringstream ss; ss << d_holder->$internal; std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(ss.str()); opts.push_back(v); }"
 767         smt_getoption_handlers="${smt_getoption_handlers}
 768 #line $lineno \"$kf\"
 769   if(key == \"$smtname\") {
 770 #line $lineno \"$kf\"
 771     stringstream ss; ss << options::$internal();
 772     return SExpr(ss.str());
 773   }";;
 774       esac
 775     fi
 776
 777     if [ "$type" = bool ]; then
 778       smt_setoption_handlers="${smt_setoption_handlers}
 779 #line $lineno \"$kf\"
 780   if(key == \"$smtname\") {
 781 #line $lineno \"$kf\"
 782     Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_smt_links
 783     return;
 784   }"
 785     elif [ -n "$expect_arg" -a "$internal" != - ]; then
 786       run_handlers=
 787       if [ -n "$handlers" ]; then
 788         for handler in $handlers; do
 789           run_handlers="$run_handlers
 790 #line $lineno \"$kf\"
 791     $handler(\"$smtname\", optionarg, smt);
 792 "
 793         done
 794       fi
 795       smt_setoption_handlers="${smt_setoption_handlers}
 796 #line $lineno \"$kf\"
 797   if(key == \"$smtname\") {
 798 #line $lineno \"$kf\"
 799     Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_smt_links
 800     return;
 801   }"
 802     elif [ -n "$expect_arg" ]; then
 803       run_handlers=
 804       for handler in $handlers; do
 805         run_handlers="$run_handlers
 806 #line $lineno \"$kf\"
 807     $handler(\"$smtname\", optionarg, smt);
 808 "
 809       done
 810       smt_setoption_handlers="${smt_setoption_handlers}
 811 #line $lineno \"$kf\"
 812   if(key == \"$smtname\") {
 813 #line $lineno \"$kf\"
 814     $run_handlers$run_smt_links
 815     return;
 816   }"
 817     else
 818       run_handlers=
 819       for handler in $handlers; do
 820         run_handlers="$run_handlers
 821 #line $lineno \"$kf\"
 822     $handler(\"$smtname\", smt);
 823 "
 824       done
 825       smt_setoption_handlers="${smt_setoption_handlers}
 826 #line $lineno \"$kf\"
 827   if(key == \"$smtname\") {
 828 #line $lineno \"$kf\"
 829     $run_handlers$run_smt_links
 830     return;
 831   }"
 832     fi
 833   elif [ -n "$long_option" -o "$long_option_alternate" ] && [ "$internal" != - ]; then
 834     case "$type" in
 835     bool)
 836       getoption_name="$long_option"
 837       inv=
 838       # case where we have a --disable but no corresponding --enable
 839       if [ -z "$getoption_name" ]; then
 840         getoption_name="$long_option_alternate"
 841         inv='!'
 842       fi
 843       all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
 844 #line $lineno \"$kf\"
 845   }{ std::vector<SExpr> v; v.push_back(\"$getoption_name\"); v.push_back(SExpr::Keyword((${inv}d_holder->$internal) ? \"true\" : \"false\")); opts.push_back(v); }";;
 846     int|unsigned|int*_t|uint*_t|unsigned\ long|long|CVC4::Integer)
 847         all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
 848 #line $lineno \"$kf\"
 849   }{ std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(d_holder->$internal); opts.push_back(v); }";;
 850     float|double)
 851       all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
 852 #line $lineno \"$kf\"
 853   }{ std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(Rational::fromDouble(d_holder->$internal)); opts.push_back(v); }";;
 854     CVC4::Rational)
 855       all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
 856 #line $lineno \"$kf\"
 857   }{ std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(d_holder->$internal); opts.push_back(v); }";;
 858     *)
 859       all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
 860 #line $lineno \"$kf\"
 861   }{ std::stringstream ss; ss << d_holder->$internal; std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(ss.str()); opts.push_back(v); }";;
 862     esac
 863   fi
 864
 865   if [ "$type" = bool ]; then
 866     # emit assignBool/assign
 867     all_custom_handlers="${all_custom_handlers}
 868 #line $lineno \"$kf\"
 869 template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, SmtEngine* smt) {
 870 #line $lineno \"$kf\"
 871   runBoolPredicates(options::$internal, option, value, smt);
 872 #line $lineno \"$kf\"
 873   d_holder->$internal = value;
 874 #line $lineno \"$kf\"
 875   d_holder->${internal}__setByUser__ = true;
 876 #line $lineno \"$kf\"
 877   Trace(\"options\") << \"user assigned option $internal\" << std::endl;
 878 }"
 879   elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then
 880     all_custom_handlers="${all_custom_handlers}
 881 #line $lineno \"$kf\"
 882 template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt) {
 883 #line $lineno \"$kf\"
 884   d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, smt);
 885 #line $lineno \"$kf\"
 886   d_holder->${internal}__setByUser__ = true;
 887 #line $lineno \"$kf\"
 888   Trace(\"options\") << \"user assigned option $internal\" << std::endl;
 889 }"
 890   fi
 891 }
 892
 893 function common-alias {
 894   # common-alias -option[=arg] = (-option[=arg])+
 895   handle_alias COMMON "$@"
 896 }
 897
 898 function alias {
 899   # alias -option[=arg] = (-option[=arg])+
 900   handle_alias STANDARD "$@"
 901 }
 902
 903 function expert-alias {
 904   # expert-alias -option[=arg] = (-option[=arg])+
 905   handle_alias EXPERT "$@"
 906 }
 907
 908 function undocumented-alias {
 909   # undocumented-alias -option[=arg] = (-option[=arg])+
 910   handle_alias UNDOCUMENTED "$@"
 911 }
 912
 913 function handle_alias {
 914   # handle_alias CATEGORY -option[=arg] = (-option[=arg])+
 915   check_module_seen
 916   check_doc
 917
 918   category="$1"
 919   shift
 920
 921   internal=-
 922   smtname=
 923   short_option=
 924   short_option_alternate=
 925   long_option=
 926   long_option_alternate=
 927   long_option_alternate_set=
 928   type=void
 929   readOnly=true
 930   required_argument=false
 931   default_value=
 932   handlers=
 933   predicates=
 934   links=
 935   links_alternate=
 936
 937   options_already_documented=false
 938   alternate_options_already_documented=false
 939
 940   if [ "$category" = UNDOCUMENTED ]; then
 941     expect_doc=false
 942   else
 943     expect_doc=true
 944   fi
 945   expect_doc_alternate=false
 946
 947   if [ $# -lt 3 ]; then
 948     ERR "malformed \"alias\" command; expected more arguments"
 949   fi
 950   if [ "$1" = '=' ]; then
 951     ERR "malformed \"alias\" command; expected option name"
 952   fi
 953   option="$1"
 954   shift
 955   if [ "$1" != '=' ]; then
 956     ERR "malformed \"alias\" command; expected \`='"
 957   fi
 958   shift
 959   if [ $# -eq 0 ]; then
 960     ERR "malformed \"alias\" command; expected more arguments"
 961   fi
 962   cases=
 963   if ! expr "$option" : '\-' &>/dev/null; then
 964     ERR "alias for SMT options not yet supported"
 965   fi
 966   if expr "$option" : '\--' &>/dev/null; then
 967     if expr "$option" : '.*=' &>/dev/null; then
 968       expect_arg_long=required_argument
 969       arg="$(echo "$option" | sed 's,[^=]*=\(.*\),\1,')"
 970       option="$(echo "$option" | sed 's,--,,;s,=.*,,')"
 971     else
 972       expect_arg_long=no_argument
 973       arg=
 974       option="$(echo "$option" | sed 's,--,,')"
 975     fi
 976     all_modules_long_options="${all_modules_long_options}
 977   { \"$(echo "$option" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long },"
 978       cases="${cases}
 979     case $n_long:// --$option"
 980     let ++n_long
 981     long_option="${long_option:+$long_option | --}$option"
 982   else
 983     if ! expr "$option" : '\-.$' &>/dev/null; then
 984       if ! expr "$option" : '\-.=' &>/dev/null; then
 985         ERR "expected short option specification, got \`$option'"
 986       fi
 987       expect_arg=:
 988       arg="$(echo "$option" | sed 's,[^=]*=,,')"
 989       option="$(echo "$option" | sed 's,-\(.\)=.*,\1,')"
 990     else
 991       expect_arg=
 992       arg=
 993       option="$(echo "$option" | sed 's,-,,')"
 994     fi
 995     all_modules_short_options="${all_modules_short_options}$option$expect_arg"
 996       cases="${cases}
 997     case '$option':"
 998     short_option="${short_option:+$short_option | -}$option"
 999   fi
1000
1001   while [ $# -gt 0 ]; do
1002     linkopt="$1"
1003     # on the RHS, we're looking for =ARG, where "ARG" is *exactly* what
1004     # was given on the LHS
1005     if expr "$linkopt" : '.*=' &>/dev/null; then
1006       linkarg="$(echo "$linkopt" | sed 's,[^=]*=,,')"
1007       if [ "$linkarg" = "$arg" ]; then
1008         # we found =ARG
1009         linkopt="$(echo "$linkopt" | sed 's,=.*,,')"
1010       else
1011         # false positive: =SOMETHING, where SOMETHING != ARG
1012         linkarg=
1013       fi
1014     else
1015       linkarg=
1016     fi
1017     links="$links
1018 #line $lineno \"$kf\"
1019       preemptGetopt(extra_argc, extra_argv, \"$linkopt\");"
1020     if [ "$linkarg" ]; then
1021       # include also the arg
1022       links="$links
1023 #line $lineno \"$kf\"
1024       preemptGetopt(extra_argc, extra_argv, optionarg.c_str());"
1025     fi
1026     shift
1027   done
1028   all_modules_option_handlers="$all_modules_option_handlers$cases$links
1029       break;
1030 "
1031 }
1032
1033 function warning {
1034   # warning message
1035   check_module_seen
1036   check_doc
1037
1038   WARN "$*"
1039 }
1040
1041 function doc {
1042   # doc text...
1043   check_module_seen
1044   expect_doc=false
1045   seen_doc=true
1046
1047   if [ -z "$short_option" -a -z "$long_option" ]; then
1048     if [ -n "$short_option_alternate" -o -n "$long_option_alternate" ]; then
1049       if [ -n "$smtname" ]; then
1050         expect_doc_alternate=true
1051       else
1052         if [ "$internal" != - ]; then
1053           if ! $alternate_options_already_documented; then
1054             if [ "$short_option_alternate" ]; then
1055               if [ "$long_option_alternate" ]; then
1056                 altopt="s -$short_option_alternate and --$long_option_alternate, each of"
1057               else
1058                 altopt=" -$short_option_alternate,"
1059               fi
1060             else
1061               altopt=" --$long_option_alternate,"
1062             fi
1063             if [ -z "$default_value" ]; then
1064               typedefault="($type)"
1065             else
1066               typedefault="($type, default = $default_value)"
1067             fi
1068             mansmtdoc="$@"
1069             if [ "$category" = EXPERT ]; then
1070               mansmtdoc="$mansmtdoc (EXPERTS only)"
1071             fi
1072             altmanopt="`echo "$altopt" | sed 's,-,\\\\\\-,g'`"
1073             mansmtdoc="`echo "$mansmtdoc" | sed 's,-,\\\\\\-,g'`"
1074             typedefault="`echo "$typedefault" | sed 's,-,\\\\\\-,g'`"
1075             if [ "$category" = COMMON ]; then
1076               common_manpage_internals_documentation="${common_manpage_internals_documentation}
1077 .TP
1078 .B \"$internal\"
1079 $typedefault
1080 .br
1081 .B \"This internal Boolean flag is undocumented; however, its alternate option$altmanopt which reverses the sense of the option, is documented thusly:\"
1082 $mansmtdoc"
1083             else
1084               remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
1085 .TP
1086 .B \"$internal\"
1087 $typedefault
1088 .br
1089 .B \"This internal Boolean flag is undocumented; however, its alternate option$altmanopt which reverses the sense of the option, is documented thusly:\"
1090 $mansmtdoc"
1091             fi
1092           else
1093             if [ "$category" = COMMON ]; then
1094               common_manpage_internals_documentation="${common_manpage_internals_documentation}
1095 $@"
1096             else
1097               remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
1098 $@"
1099             fi
1100           fi
1101         fi
1102         doc-alternate "$@"
1103         return
1104       fi
1105     fi
1106   fi
1107
1108   the_opt=
1109   if [ "$long_option" ]; then
1110     the_opt="--$long_option"
1111     if [ "$short_option" ]; then
1112       shortoptarg=
1113       if expr "$the_opt" : '.*=' &>/dev/null; then
1114         shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')"
1115       fi
1116       the_opt="$the_opt | -$short_option$shortoptarg"
1117     fi
1118   elif [ "$short_option" ]; then
1119     the_opt="-$short_option"
1120   fi
1121
1122   if ! $options_already_documented; then
1123     options_already_documented=true
1124
1125     the_doc="$@"
1126     mandoc="$@"
1127     mansmtdoc="$@"
1128     if [ "$category" = EXPERT ]; then
1129       the_doc="$the_doc (EXPERTS only)"
1130       mandoc="$mandoc (EXPERTS only)"
1131       mansmtdoc="$mansmtdoc (EXPERTS only)"
1132     fi
1133
1134     if [ "$type" = bool -a -n "$long_option" -a "$long_option_alternate" = "no-$long_option" ]; then
1135       the_doc="$the_doc [*]"
1136       mandoc="$mandoc [*]"
1137     fi
1138
1139     # in man, minus sign is \-, different from hyphen
1140     the_manopt="`echo "$the_opt" | sed 's,-,\\\\\\-,g'`"
1141     mandoc="`echo "$mandoc" | sed 's,-,\\\\\\-,g'`"
1142     mansmtdoc="`echo "$mansmtdoc" | sed 's,-,\\\\\\-,g'`"
1143
1144     if [ "$the_opt" ]; then
1145       doc_line=
1146       while [ -n "$the_doc" ]; do
1147         remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')"
1148         the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')"
1149         if [ -z "$doc_line" ]; then
1150           if expr "$the_opt" : '.\{23\}' &>/dev/null; then
1151             # break into two lines
1152             doc_line="$(printf '  %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")"
1153           else
1154             doc_line="$(printf '  %-22s %s' "$the_opt" "$the_doc")"
1155           fi
1156         else
1157           doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")"
1158         fi
1159         the_doc="$(expr "$remaining_doc" : '\(.*\) ')"
1160       done
1161
1162       if [ "$category" = COMMON ]; then
1163         common_documentation="${common_documentation}\\n\"
1164 #line $lineno \"$kf\"
1165 \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
1166         common_manpage_documentation="${common_manpage_documentation}
1167 .IP \"$the_manopt\"
1168 $mandoc"
1169       elif [ "$category" != UNDOCUMENTED ]; then
1170         remaining_documentation="${remaining_documentation}\\n\"
1171 #line $lineno \"$kf\"
1172 \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
1173         remaining_manpage_documentation="${remaining_manpage_documentation}
1174 .IP \"$the_manopt\"
1175 $mandoc"
1176       fi
1177     fi
1178
1179     if [ "$smtname" -a "$category" != UNDOCUMENTED ]; then
1180       if [ "$category" = COMMON ]; then
1181         common_manpage_smt_documentation="${common_manpage_smt_documentation}
1182 .TP
1183 .B \"$smtname\"
1184 ($type) $mansmtdoc"
1185       else
1186         remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
1187 .TP
1188 .B \"$smtname\"
1189 ($type) $mansmtdoc"
1190       fi
1191     fi
1192     if [ "$internal" != - ]; then
1193       if [ -z "$default_value" ]; then
1194         typedefault="($type)"
1195       else
1196         typedefault="($type, default = $default_value)"
1197       fi
1198       typedefault="`echo "$typedefault" | sed 's,-,\\\\\\-,g'`"
1199       if [ "$category" = COMMON ]; then
1200         common_manpage_internals_documentation="${common_manpage_internals_documentation}
1201 .TP
1202 .B \"$internal\"
1203 $typedefault
1204 .br
1205 $mansmtdoc"
1206       else
1207         remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
1208 .TP
1209 .B \"$internal\"
1210 $typedefault
1211 .br
1212 $mansmtdoc"
1213       fi
1214     fi
1215   else
1216     if [ "$the_opt" -a "$category" != UNDOCUMENTED ]; then
1217       if [ "$category" = COMMON ]; then
1218         common_manpage_documentation="${common_manpage_documentation}
1219 $@"
1220       else
1221         remaining_manpage_documentation="${remaining_manpage_documentation}
1222 $@"
1223       fi
1224     fi
1225
1226     if [ "$smtname" -a "$category" != UNDOCUMENTED ]; then
1227       if [ "$category" = COMMON ]; then
1228         common_manpage_smt_documentation="${common_manpage_smt_documentation}
1229 $@"
1230       else
1231         remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
1232 $@"
1233       fi
1234     fi
1235
1236     if [ "$internal" != - ]; then
1237       if [ "$category" = COMMON ]; then
1238         common_manpage_internals_documentation="${common_manpage_internals_documentation}
1239 $@"
1240       else
1241         remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
1242 $@"
1243       fi
1244     fi
1245   fi
1246 }
1247
1248 function doc-alternate {
1249   # doc-alternate text...
1250   check_module_seen
1251   expect_doc_alternate=false
1252
1253   if $expect_doc; then
1254     ERR "must provide documentation before alternate documentation"
1255   fi
1256
1257   if [ -z "$short_option_alternate" -a -z "$long_option_alternate" ]; then
1258     ERR "cannot document an alternative for option \`$internal'; one does not exist"
1259   fi
1260
1261   if [ "$category" = UNDOCUMENTED ]; then
1262     return
1263   fi
1264
1265   if ! $alternate_options_already_documented; then
1266     alternate_options_already_documented=true
1267     the_opt=
1268     if [ "$long_option_alternate" ]; then
1269       the_opt="--$long_option_alternate"
1270       shortoptarg=
1271       if expr "$the_opt" : '.*=' &>/dev/null; then
1272         shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')"
1273       fi
1274       if [ "$short_option_alternate" ]; then
1275         the_opt="$the_opt | -$short_option_alternate$shortoptarg"
1276       fi
1277     elif [ "$short_option_alternate" ]; then
1278       the_opt="-$short_option_alternate"
1279     fi
1280     if [ -z "$the_opt" ]; then
1281       # nothing to document
1282       return
1283     fi
1284
1285     the_doc="$@"
1286     if [ "$category" = EXPERT ]; then
1287       the_doc="$the_doc (EXPERTS only)"
1288     fi
1289
1290     doc_line=
1291     while [ -n "$the_doc" ]; do
1292       remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')"
1293       the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')"
1294       if [ -z "$doc_line" ]; then
1295         if expr "$the_opt" : '.\{23\}' &>/dev/null; then
1296           # break into two lines
1297           doc_line="$(printf '  %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")"
1298         else
1299           doc_line="$(printf '  %-22s %s' "$the_opt" "$the_doc")"
1300         fi
1301       else
1302         doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")"
1303       fi
1304       the_doc="$(expr "$remaining_doc" : '\(.*\) ')"
1305     done
1306
1307     # in man, minus sign is \-, different from hyphen
1308     the_manopt="`echo "$the_opt" | sed 's,-,\\\\\\-,g'`"
1309
1310     if [ "$category" = COMMON ]; then
1311       common_documentation="${common_documentation}\\n\"
1312 #line $lineno \"$kf\"
1313 \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
1314       common_manpage_documentation="${common_manpage_documentation}
1315 .IP \"$the_manopt\"
1316 $@"
1317     else
1318       remaining_documentation="${remaining_documentation}\\n\"
1319 #line $lineno \"$kf\"
1320 \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
1321       remaining_manpage_documentation="${remaining_manpage_documentation}
1322 .IP \"$the_manopt\"
1323 $@"
1324     fi
1325   else
1326     if [ "$category" = COMMON ]; then
1327       common_manpage_documentation="${common_manpage_documentation}
1328 $@"
1329     else
1330       remaining_manpage_documentation="${remaining_manpage_documentation}
1331 $@"
1332     fi
1333   fi
1334 }
1335
1336 function check_doc {
1337   if $expect_doc; then
1338     if [ "$internal" != - ]; then
1339       WARN "$internal is lacking documentation"
1340     elif [ -n "$long_option" ]; then
1341       WARN "option --$long_option is lacking documentation"
1342     elif [ -n "$short_option" ]; then
1343       WARN "option -$short_option is lacking documentation"
1344     elif [ -n "$smtname" ]; then
1345       WARN "SMT option $smtname is lacking documentation"
1346     fi
1347     expect_doc=false
1348   elif ! $seen_doc; then
1349     if [ -n "$internal" -a "$internal" != - ]; then
1350       if [ -z "$default_value" ]; then
1351         typedefault="($type)"
1352       else
1353         typedefault="($type, default = $default_value)"
1354       fi
1355       if [ "$category" = COMMON ]; then
1356         common_manpage_internals_documentation="${common_manpage_internals_documentation}
1357 .TP
1358 .B \"$internal\"
1359 $typedefault
1360 .br
1361 [undocumented]"
1362       else
1363         remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
1364 .TP
1365 .B \"$internal\"
1366 $typedefault
1367 .br
1368 [undocumented]"
1369       fi
1370     fi
1371   fi
1372
1373   if $expect_doc_alternate; then
1374     WARN "$internal is lacking documentation for the alternative option(s): $short_option_alternate $long_option_alternate"
1375     expect_doc_alternate=false
1376   fi
1377 }
1378
1379 function check_module_seen {
1380   if $seen_endmodule; then
1381     ERR "command after \"endmodule\" declaration (endmodule has to be last)"
1382   fi
1383   if ! $seen_module; then
1384     ERR "no \"module\" declaration found (it has to be first)"
1385   fi
1386 }
1387
1388 function check_include {
1389   if ! expr "$1" : '".*"$' &>/dev/null && ! expr "$1" : '<.*>$' &>/dev/null; then
1390     echo "\"$1\""
1391   else
1392     echo "$1"
1393   fi
1394 }
1395
1396 function output_module {
1397   template="$1"
1398   output="$2"
1399
1400   filename="$(basename "$output")"
1401
1402   #echo "generating module $output from $template"
1403
1404   # generate warnings about incorrect #line annotations in templates
1405   nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
1406     awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
1407
1408   mkdir -p "`dirname "$output"`"
1409   cp "$template" "$output.working"
1410   echo -n > "$output.sed"
1411   for var in \
1412       module_id \
1413       module_name \
1414       module_includes \
1415       module_optionholder_spec \
1416       module_decls \
1417       module_specializations \
1418       module_inlines \
1419       module_accessors \
1420       module_global_definitions \
1421       template \
1422       ; do
1423     progress "$output" $count $total
1424     repl="$(eval "echo \"\${$var}\"" | sed 's,\\,\\\\,g;s/,/\\,/g;s,&,\\\&,g;$!s,$,\\,g')"
1425     # a little nasty; for multi-line replacements, bash can eat a final
1426     # (blank) newline, and so we get a final \ on the final line, leading
1427     # to malformed replacements in the sed script
1428     repl2="$(echo "$repl" | sed '$s,\\*$,,')"
1429     while [ "$repl" != "$repl2" ]; do
1430       repl="$repl2"
1431       repl2="$(echo "$repl" | sed '$s,\\*$,,')"
1432     done
1433     repl="$repl2"
1434     echo -n ";s,$(eval echo "\$\{$var\}"),$repl,g" >>"$output.sed"
1435   done
1436   sed -f "$output.sed" "$output.working" >"$output.working2"
1437   mv -f "$output.working2" "$output.working"
1438   error="$(grep '.*\${[^}]*}.*' "$output.working" | head -n 1)"
1439   if [ -n "$error" ]; then
1440     error="$(echo "$error" | sed 's,.*\${\([^}]*\)}.*,\1,')"
1441     rm -f "$output.working"
1442     rm -f "$output.sed"
1443     kf="$template"
1444     lineno=0
1445     ERR "undefined replacement \${$error}"
1446   fi
1447
1448   (
1449
1450   # Output header (if this is a .cpp or .c or .h file) and then the
1451   # processed text
1452
1453   if expr "$output" : '.*\.cpp$' &>/dev/null || expr "$output" : '.*\.[ch]$' &>/dev/null; then
1454
1455   cat <<EOF
1456 /*********************                                                        */
1457 /** $filename
1458  **
1459  ** Copyright $copyright  New York University and The University of Iowa,
1460  ** and as below.
1461  **
1462  ** This file automatically generated by:
1463  **
1464  **     $0 $@
1465  **
1466  ** for the CVC4 project.
1467  **/
1468
1469 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1470 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1471 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1472 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1473 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1474 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1475
1476 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1477 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1478 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1479 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1480 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1481 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1482
1483 /* Edit the template file instead.                     */
1484
1485 EOF
1486   fi
1487
1488   cat "$output.working"
1489
1490   ) >"$output.tmp"
1491
1492   rm -f "$output.working"
1493   rm -f "$output.sed"
1494   if diff -q "$output" "$output.tmp" &>/dev/null; then
1495     rm -f "$output.tmp"
1496   else
1497     mv -f "$output.tmp" "$output"
1498     printf "${r}regenerated %-68s\n" "$output"
1499   fi
1500 }
1501
1502 total=$(($#/2+23*${#templates[@]}))
1503 count=0
1504 while [ $# -gt 0 ]; do
1505   kf="$1"; shift
1506   if [ $# -eq 0 ]; then
1507     echo "$me: error: mismatched number of templates and output files (after -t)" >&2
1508     usage
1509     exit 1
1510   fi
1511   outdir="$1"; shift
1512
1513   #echo "scanning $kf"
1514   let ++count
1515   progress "$kf" $count $total
1516
1517   seen_module=false
1518   seen_endmodule=false
1519   b=$(basename $(dirname "$kf"))
1520   lineno=0
1521   # IFS= forces read to read an entire line
1522   while IFS= read -r line; do
1523     let ++lineno
1524     # read any continuations of the line
1525     while expr "$line" : '.*\\$' &>/dev/null; do
1526       IFS= read -r line2
1527       line="$(echo "$line" | sed 's,\\$,,')$line2"
1528       let ++lineno
1529     done
1530     if expr "$line" : '[        ].*' &>/dev/null; then
1531       doc "$(echo "$line" | sed 's,^[   ],,')"
1532     elif expr "$line" : '\.[    ]*$' &>/dev/null; then
1533       doc ""
1534     elif expr "$line" : '\.' &>/dev/null; then
1535       ERR "malformed line during processing of option \`$internal': continuation lines should not have content"
1536     elif expr "$line" : '/.*' &>/dev/null; then
1537       doc-alternate "$(echo "$line" | sed 's,^/,,')"
1538     else
1539       line="$(echo "$line" | sed 's,\([<>&()!?*]\),\\\1,g')"
1540       progress "$kf" $count $total
1541       if ! eval "$line"; then
1542         ERR "error was due to evaluation of this line"
1543       fi
1544     fi
1545   done < "$kf"
1546   if ! $seen_module; then
1547     ERR "no module content found in file!"
1548   fi
1549   if ! $seen_endmodule; then
1550     ERR "no \"endmodule\" declaration found (it is required at the end)"
1551   fi
1552
1553   output_module "$options_h_template" "$outdir/$(basename "$kf").h"
1554   output_module "$options_cpp_template" "$outdir/$(basename "$kf").cpp"
1555 done
1556
1557 ## final outputs
1558
1559 regenerated=false
1560 i=0; while [ $i -lt ${#templates[@]} ]; do
1561
1562 template="${templates[$i]}"
1563 output="${outputs[$i]}"
1564
1565 progress "$output" $count $total
1566
1567 let ++i
1568
1569 filename="$(basename "$output")"
1570
1571 #echo "generating $output from $template"
1572
1573 # generate warnings about incorrect #line annotations in templates
1574 nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
1575   awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
1576
1577 long_option_value_end=$n_long
1578
1579 cp "$template" "$output.working"
1580 echo -n > "$output.sed"
1581 for var in \
1582     smt_getoption_handlers \
1583     smt_setoption_handlers \
1584     long_option_value_begin \
1585     long_option_value_end \
1586     template \
1587     option_handler_includes \
1588     all_modules_defaults \
1589     all_modules_short_options \
1590     all_modules_long_options \
1591     all_modules_smt_options \
1592     all_modules_option_handlers \
1593     all_modules_get_options \
1594     include_all_option_headers \
1595     all_modules_contributions \
1596     all_custom_handlers \
1597     common_documentation \
1598     remaining_documentation \
1599     common_manpage_documentation \
1600     remaining_manpage_documentation \
1601     common_manpage_smt_documentation \
1602     remaining_manpage_smt_documentation \
1603     common_manpage_internals_documentation \
1604     remaining_manpage_internals_documentation \
1605     ; do
1606   let ++count
1607   progress "$output" $count $total
1608   repl="$(eval "echo \"\${$var}\"" | sed 's,\\,\\\\,g;s/,/\\,/g;s,&,\\\&,g;$!s,$,\\,g')"
1609   # a little nasty; for multi-line replacements, bash can eat a final
1610   # (blank) newline, and so we get a final \ on the final line, leading
1611   # to malformed replacements in the sed script
1612   repl2="$(echo "$repl" | sed '$s,\\*$,,')"
1613   while [ "$repl" != "$repl2" ]; do
1614     repl="$repl2"
1615     repl2="$(echo "$repl" | sed '$s,\\*$,,')"
1616   done
1617   repl="$repl2"
1618   echo -n ";s,$(eval echo "\$\{$var\}"),$repl,g" >>"$output.sed"
1619 done
1620 sed -f "$output.sed" "$output.working" >"$output.working2"
1621 mv -f "$output.working2" "$output.working"
1622 error="$(grep '.*\${[^}]*}.*' "$output.working" | head -n 1)"
1623 if [ -n "$error" ]; then
1624   error="$(echo "$error" | sed 's,.*\${\([^}]*\)}.*,\1,')"
1625   echo "$template:0: error: undefined replacement \${$error}" >&2
1626   rm -f "$output.working"
1627   rm -f "$output.sed"
1628   exit 1
1629 fi
1630
1631 progress "$output" $count $total
1632
1633 (
1634
1635 # Output header (if this is a .cpp or .c or .h file) and then the
1636 # processed text
1637
1638 if expr "$output" : '.*\.cpp$' &>/dev/null || expr "$output" : '.*\.[ch]$' &>/dev/null; then
1639
1640 cat <<EOF
1641 /*********************                                                        */
1642 /** $filename
1643  **
1644  ** Copyright $copyright  New York University and The University of Iowa,
1645  ** and as below.
1646  **
1647  ** This file automatically generated by:
1648  **
1649  **     $0 $@
1650  **
1651  ** for the CVC4 project.
1652  **/
1653
1654 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1655 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1656 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1657 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1658 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1659 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1660
1661 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1662 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1663 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1664 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1665 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1666 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
1667
1668 /* Edit the template file instead:                     */
1669 /* $1 */
1670
1671 EOF
1672 fi
1673
1674 cat "$output.working"
1675
1676 ) >"$output.tmp"
1677
1678 rm -f "$output.working"
1679 rm -f "$output.sed"
1680 if diff -q "$output" "$output.tmp" &>/dev/null; then
1681   regenerated=false
1682 else
1683   mv -f "$output.tmp" "$output"
1684   printf "${r}regenerated %-68s\n" "$output"
1685   regenerated=true
1686 fi
1687 rm -f "$output.tmp"
1688
1689 done
1690
1691 if ! $regenerated; then
1692   [ -t 1 ] && printf "$r%-80s$r" ""
1693 fi