Adding listeners to Options.

- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.

- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.

- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.

- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.

- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.

- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.

- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.

1 files changed, 43 insertions, 29 deletions

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 05280baa8..ad8d7033f 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -115,6 +115,7 @@ long_option_alternate=
 long_option_alternate_set=
 type=
 predicates=
+notifications=
 
 # just for duplicates-checking
 all_declared_internal_options=
@@ -247,6 +248,7 @@ function handle_option {
   default_value=
   handlers=
   predicates=
+  notifications=
   links=
   links_alternate=
   smt_links=
@@ -425,6 +427,12 @@ function handle_option {
          predicates="${predicates} ${args[$i]}"
        done
        ;;
+    :notify)
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
+         let ++i
+         notifications="${notifications} ${args[$i]}"
+       done
+       ;;
     :link)
        while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
          let ++i
@@ -535,11 +543,11 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const;"
     if [ "$type" = bool ]; then
       module_specializations="${module_specializations}
 #line $lineno \"$kf\"
-template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, options::OptionsHandler* handler);"
+template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value);"
     elif [ "$internal" != - ]; then
       module_specializations="${module_specializations}
 #line $lineno \"$kf\"
-template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, options::OptionsHandler* handler);"
+template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value);"
     fi
 
     module_accessors="${module_accessors}
@@ -585,6 +593,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
   run_links=
   run_links_alternate=
   run_smt_links=
+  run_notifications=
   if [ -n "$links" -a -z "$smt_links" -a -n "$smtname" ]; then
     WARN "$smtname has no :link-smt, but equivalent command-line has :link"
   elif [ -n "$smt_links" -a -z "$links" ] && [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o "$long_option_alternate" ]; then
@@ -595,7 +604,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
     for link in $links; do
       run_links="$run_links
 #line $lineno \"$kf\"
-      preemptGetopt(extra_argc, extra_argv, \"$link\");"
+      argumentExtender.extend(extra_argc, extra_argv, \"$link\", allocated);"
     done
   fi
   if [ -n "$smt_links" ]; then
@@ -605,7 +614,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
     while [ $i -lt ${#smt_links[@]} ]; do
       run_smt_links="$run_smt_links
 #line $lineno \"$kf\"
-    handler->setOption(std::string(\"${smt_links[$i]}\"), (${smt_links[$(($i+1))]}));"
+    setOption(std::string(\"${smt_links[$i]}\"), (${smt_links[$(($i+1))]}));"
       i=$((i+2))
     done
   fi
@@ -614,7 +623,14 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
     for link in $links_alternate; do
       run_links_alternate="$run_links_alternate
 #line $lineno \"$kf\"
-      preemptGetopt(extra_argc, extra_argv, \"$link\");"
+      argumentExtender.extend(extra_argc, extra_argv, \"$link\", allocated);"
+    done
+  fi
+  if [ -n "$notifications" ]; then
+    for notification in $notifications; do
+      run_notifications="$run_notifications
+#line $lineno \"$kf\"
+  d_handler->$notification(option);"
     done
   fi
   if [ "$type" = bool ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then
@@ -626,7 +642,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
       for predicate in $predicates; do
         run_handlers="$run_handlers
 #line $lineno \"$kf\"
-  $predicate(option, b, handler);"
+  handler->$predicate(option, b);"
       done
     fi
     if [ -n "$run_handlers" ]; then
@@ -641,7 +657,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o
     if [ "$type" = bool ]; then
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 #line $lineno \"$kf\"
-      assignBool(options::$internal, option, true, handler);$run_links
+      assignBool(options::$internal, option, true);$run_links
       break;
 "
     elif [ -n "$expect_arg" -a "$internal" != - ]; then
@@ -650,7 +666,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-  $handler(option, optionarg, handler);"
+  handler->$handler(option, optionarg);"
         done
       else
         run_handlers="
@@ -661,7 +677,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o
         for predicate in $predicates; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-  $predicate(option, retval, handler);"
+  handler->$predicate(option, retval);"
         done
       fi
       all_custom_handlers="${all_custom_handlers}
@@ -674,7 +690,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 }"
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 #line $lineno \"$kf\"
-      assign(options::$internal, option, optionarg, handler);$run_links
+      assign(options::$internal, option, optionarg);$run_links
       break;
 "
     elif [ -n "$expect_arg" ]; then
@@ -686,7 +702,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-      $handler(option, optionarg, handler);"
+      handler->$handler(option, optionarg);"
         done
       fi
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
@@ -703,7 +719,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-      $handler(option, handler);"
+      handler->$handler(option);"
         done
       fi
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
@@ -712,12 +728,12 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
       break;
 "
     fi
-  fi
+  fi # ends if [ -n "$cases" ];
   if [ -n "$cases_alternate" ]; then
     if [ "$type" = bool ]; then
       all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate}
 #line $lineno \"$kf\"
-      assignBool(options::$internal, option, false, handler);$run_links_alternate
+      assignBool(options::$internal, option, false);$run_links_alternate
       break;
 "
     else
@@ -770,7 +786,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current()->assignBool(options::$internal, \"$smtname\", optionarg == \"true\", handler);$run_smt_links
+    Options::current()->assignBool(options::$internal, \"$smtname\", optionarg == \"true\");$run_smt_links
     return;
   }"
     elif [ -n "$expect_arg" -a "$internal" != - ]; then
@@ -779,7 +795,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-    $handler(\"$smtname\", optionarg, handler);
+    handler->$handler(\"$smtname\", optionarg);
 "
         done
       fi
@@ -787,7 +803,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current()->assign(options::$internal, \"$smtname\", optionarg, handler);$run_smt_links
+    Options::current()->assign(options::$internal, \"$smtname\", optionarg);$run_smt_links
     return;
   }"
     elif [ -n "$expect_arg" ]; then
@@ -795,7 +811,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
       for handler in $handlers; do
         run_handlers="$run_handlers
 #line $lineno \"$kf\"
-    $handler(\"$smtname\", optionarg, handler);
+    handler->$handler(\"$smtname\", optionarg);
 "
       done
       smt_setoption_handlers="${smt_setoption_handlers}
@@ -810,7 +826,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
       for handler in $handlers; do
         run_handlers="$run_handlers
 #line $lineno \"$kf\"
-    $handler(\"$smtname\", handler);
+    handler->$handler(\"$smtname\");
 "
       done
       smt_setoption_handlers="${smt_setoption_handlers}
@@ -849,26 +865,26 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
     # emit assignBool/assign
     all_custom_handlers="${all_custom_handlers}
 #line $lineno \"$kf\"
-template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, options::OptionsHandler* handler) {
+template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value) {
 #line $lineno \"$kf\"
-  runBoolPredicates(options::$internal, option, value, handler);
+  runBoolPredicates(options::$internal, option, value, d_handler);
 #line $lineno \"$kf\"
   d_holder->$internal = value;
 #line $lineno \"$kf\"
   d_holder->${internal}__setByUser__ = true;
 #line $lineno \"$kf\"
-  Trace(\"options\") << \"user assigned option $internal\" << std::endl;
+  Trace(\"options\") << \"user assigned option $internal\" << std::endl;$run_notifications
 }"
   elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then
     all_custom_handlers="${all_custom_handlers}
 #line $lineno \"$kf\"
-template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, options::OptionsHandler* handler) {
+template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value) {
 #line $lineno \"$kf\"
-  d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, handler);
+  d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, d_handler);
 #line $lineno \"$kf\"
   d_holder->${internal}__setByUser__ = true;
 #line $lineno \"$kf\"
-  Trace(\"options\") << \"user assigned option $internal\" << std::endl;
+  Trace(\"options\") << \"user assigned option $internal\" << std::endl;$run_notifications
 }"
   fi
 }
@@ -912,8 +928,6 @@ function handle_alias {
   readOnly=true
   required_argument=false
   default_value=
-  handlers=
-  predicates=
   links=
   links_alternate=
 
@@ -999,12 +1013,12 @@ function handle_alias {
     fi
     links="$links
 #line $lineno \"$kf\"
-      preemptGetopt(extra_argc, extra_argv, \"$linkopt\");"
+      argumentExtender.extend(extra_argc, extra_argv, \"$linkopt\", allocated);"
     if [ "$linkarg" ]; then
       # include also the arg
       links="$links
 #line $lineno \"$kf\"
-      preemptGetopt(extra_argc, extra_argv, optionarg.c_str());"
+      argumentExtender.extend(extra_argc, extra_argv, optionarg.c_str(), allocated);"
     fi
     shift
   done