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, 28 insertions, 23 deletions

diff --git a/src/options/smt_options b/src/options/smt_options
index b99a8a83b..bc2586fe0 100644
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -5,15 +5,15 @@
 
 module SMT "options/smt_options.h" SMT layer
 
-common-option - dump --dump=MODE argument :handler CVC4::options::dumpMode :handler-include "options/options_handler_interface.h"
+common-option dumpModeString dump --dump=MODE std::string :default "" :notify notifyDumpMode
  dump preprocessed assertions, etc., see --dump=help
-common-option - dump-to --dump-to=FILE argument :handler CVC4::options::dumpToFile :handler-include "options/options_handler_interface.h"
+common-option dumpToFileName dump-to --dump-to=FILE std::string :notify notifyDumpToFile
  all dumping goes to FILE (instead of stdout)
 
-expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo* :include "options/logic_info_forward.h" :handler CVC4::options::stringToLogicInfo :handler-include "options/options_handler_interface.h" :default NULL
+expert-option forceLogicString force-logic --force-logic=LOGIC std::string :default "" :notify notifyForceLogic
  set the logic, and override all further user attempts to change it
 
-option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::options::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "options/simplification_mode.h" :handler-include "options/options_handler_interface.h"
+option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "options/simplification_mode.h"
  choose simplification mode, see --simplification=help
 alias --no-simplification = --simplification=none
  turn off all simplification (same as --simplification=none)
@@ -23,35 +23,35 @@ option doStaticLearning static-learning --static-learning bool :default true
 
 option expandDefinitions expand-definitions bool :default false
  always expand symbol definitions in output
-common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+common-option produceModels produce-models -m --produce-models bool :default false :notify notifyBeforeSearch
  support the get-value and get-model commands
-option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :notify notifyBeforeSearch
  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
-option dumpModels --dump-models bool :default false :link --produce-models
+option dumpModels --dump-models bool :default false :link --produce-models :link-smt produce-models
  output models after every SAT/INVALID/UNKNOWN response
-option proof produce-proofs --proof bool :default false :predicate CVC4::options::proofEnabledBuild CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+option proof produce-proofs --proof bool :default false :predicate proofEnabledBuild :notify notifyBeforeSearch
  turn on proof generation
-option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" :read-write
+option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :notify notifyBeforeSearch :read-write
  after UNSAT/VALID, machine-check the generated proof
-option dumpProofs --dump-proofs bool :default false :link --proof
+option dumpProofs --dump-proofs bool :default false :link --proof :link-smt produce-proofs
  output proofs after every UNSAT/VALID response
 option dumpInstantiations --dump-instantiations bool :default false
  output instantiations of quantified formulas after every UNSAT/VALID response
 option dumpSynth --dump-synth bool :read-write :default false
  output solution for synthesis conjectures after every UNSAT/VALID response
-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::options::proofEnabledBuild CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch
  turn on unsat core generation
 option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produce-unsat-cores :link-smt produce-unsat-cores :read-write
  after UNSAT/VALID, produce and check an unsat core (expensive)
-option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :notify notifyBeforeSearch
  output unsat cores after every UNSAT/VALID response
 
-option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch
  support the get-assignment command
 
-undocumented-option interactiveMode interactive-mode bool :predicate CVC4::options::beforeSearch CVC4::options::setProduceAssertions :predicate-include "options/options_handler_interface.h" :read-write
+undocumented-option interactiveMode interactive-mode bool :predicate setProduceAssertions :read-write :notify notifyBeforeSearch
  deprecated name for produce-assertions
-common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::options::beforeSearch CVC4::options::setProduceAssertions :predicate-include "options/options_handler_interface.h" :read-write
+common-option produceAssertions produce-assertions --produce-assertions bool :predicate setProduceAssertions :read-write :notify notifyBeforeSearch
  keep an assertions list (enables get-assertions command)
 
 option doITESimp --ite-simp bool :read-write
@@ -86,18 +86,18 @@ option abstractValues abstract-values --abstract-values bool :default false
 option modelUninterpDtEnum --model-u-dt-enum bool :default false
  in models, output uninterpreted sorts as datatype enumerations
 
-option - regular-output-channel argument :handler CVC4::options::setRegularOutputChannel :handler-include "options/options_handler_interface.h"
+option regularChannelName regular-output-channel std::string :notify notifySetRegularOutputChannel
  set the regular output channel of the solver
-option - diagnostic-output-channel argument :handler CVC4::options::setDiagnosticOutputChannel :handler-include "options/options_handler_interface.h"
+option diagnosticChannelName diagnostic-output-channel std::string :notify notifySetDiagnosticOutputChannel
  set the diagnostic output channel of the solver
 
-common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler CVC4::options::tlimitHandler :handler-include "options/options_handler_interface.h"
+common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler tlimitHandler :notify notifyTlimit
  enable time limiting (give milliseconds)
-common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long" :handler CVC4::options::tlimitPerHandler :handler-include "options/options_handler_interface.h"
+common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long" :handler tlimitPerHandler :notify notifyTlimitPer
  enable time limiting per query (give milliseconds)
-common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler CVC4::options::rlimitHandler :handler-include "options/options_handler_interface.h"
+common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler rlimitHandler :notify notifyRlimit
  enable resource limiting (currently, roughly the number of SAT conflicts)
-common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler CVC4::options::rlimitPerHandler :handler-include "options/options_handler_interface.h"
+common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler rlimitPerHandler :notify notifyRlimitPer
  enable resource limiting per query
 common-option hardLimit hard-limit --hard-limit bool :default false
  the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)
@@ -145,14 +145,19 @@ expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsi
 expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
  eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
 
+
 # --replay is currently broken; don't document it for 1.0
-undocumented-option replayFilename --replay=FILE std::string :handler CVC4::options::checkReplayFilename :handler-include "options/options_handler_interface.h"
+undocumented-option replayInputFilename --replay=FILE std::string :handler checkReplayFilename
  replay decisions from file
 
+# --replay is currently broken; don't document it for 1.0
+undocumented-option replayLogFilename --replay-log=FILE std::string :handler checkReplayFilename :notify notifySetReplayLogFilename :notify notifyBeforeSearch
+ replay decisions from file
 
 option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false
  Force no CPU limit when dumping models and proofs
 
-option solveIntAsBV --solve-int-as-bv uint32_t :default 0
+undocumented-option solveIntAsBV --solve-int-as-bv uint32_t :default 0
+ attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)
 
 endmodule