Adding listeners to Options.
authorTim King <taking@google.com>
Thu, 28 Jan 2016 20:35:45 +0000 (12:35 -0800)
committerTim King <taking@google.com>
Thu, 28 Jan 2016 20:35:45 +0000 (12:35 -0800)
commit2ba8bb701ce289ba60afec01b653b0930cc59298
tree46df365b7b41ce662a0f94de5b11c3ed20829851
parent42b665f2a00643c81b42932fab1441987628c5a5
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}.
200 files changed:
contrib/alttheoryskel/theory_DIR.cpp
contrib/alttheoryskel/theory_DIR.h
contrib/theoryskel/theory_DIR.cpp
contrib/theoryskel/theory_DIR.h
examples/hashsmt/word.cpp
examples/nra-translate/normalize.cpp
examples/nra-translate/smt2info.cpp
examples/nra-translate/smt2todreal.cpp
examples/nra-translate/smt2toisat.cpp
examples/nra-translate/smt2tomathematica.cpp
examples/nra-translate/smt2toqepcad.cpp
examples/nra-translate/smt2toredlog.cpp
examples/sets-translate/sets_translate.cpp
examples/translator.cpp
src/Makefile.am
src/base/Makefile.am
src/base/configuration.cpp [new file with mode: 0644]
src/base/configuration.h [new file with mode: 0644]
src/base/configuration.i [new file with mode: 0644]
src/base/configuration_private.h [new file with mode: 0644]
src/base/exception.cpp
src/base/exception.h
src/base/listener.cpp
src/base/listener.h
src/base/mktagheaders [new file with mode: 0755]
src/base/mktags [new file with mode: 0755]
src/base/output.h
src/compat/cvc3_compat.cpp
src/cvc4.i
src/expr/Makefile.am
src/expr/expr_template.h
src/expr/node.h
src/expr/node_manager.cpp
src/expr/node_manager.h
src/expr/node_manager_listeners.cpp [new file with mode: 0644]
src/expr/node_manager_listeners.h [new file with mode: 0644]
src/include/cvc4.h
src/include/cvc4_private.h
src/include/cvc4_private_library.h
src/include/cvc4parser_private.h
src/lib/clock_gettime.c
src/lib/clock_gettime.h
src/main/command_executor.cpp
src/main/command_executor.h
src/main/command_executor_portfolio.cpp
src/main/command_executor_portfolio.h
src/main/driver_unified.cpp
src/main/interactive_shell.cpp
src/main/main.cpp
src/main/portfolio_util.cpp
src/main/portfolio_util.h
src/main/util.cpp
src/options/Makefile.am
src/options/argument_extender.cpp [new file with mode: 0644]
src/options/argument_extender.h [new file with mode: 0644]
src/options/arith_options
src/options/base_handlers.h
src/options/base_options
src/options/booleans_options
src/options/bv_options
src/options/decision_options
src/options/expr_options
src/options/logic_info_forward.h [deleted file]
src/options/main_options
src/options/mkoptions
src/options/mktagheaders [deleted file]
src/options/mktags [deleted file]
src/options/open_ostream.cpp [new file with mode: 0644]
src/options/open_ostream.h [new file with mode: 0644]
src/options/options.h
src/options/options_get_option_template.cpp [new file with mode: 0644]
src/options/options_handler.cpp [new file with mode: 0644]
src/options/options_handler.h [new file with mode: 0644]
src/options/options_handler_get_option_template.cpp [deleted file]
src/options/options_handler_interface.cpp [deleted file]
src/options/options_handler_interface.h [deleted file]
src/options/options_handler_interface.i [deleted file]
src/options/options_handler_set_option_template.cpp [deleted file]
src/options/options_public_functions.cpp [new file with mode: 0644]
src/options/options_set_option_template.cpp [new file with mode: 0644]
src/options/options_template.cpp
src/options/parser_options
src/options/printer_modes.h
src/options/printer_options
src/options/prop_options
src/options/quantifiers_options
src/options/smt_options
src/options/strings_options
src/options/theory_options
src/options/uf_options
src/options/ufss_mode.h
src/parser/Makefile.am
src/parser/antlr_input.cpp
src/parser/antlr_input.h
src/parser/antlr_input_imports.cpp
src/parser/antlr_line_buffered_input.cpp
src/parser/antlr_line_buffered_input.h
src/parser/antlr_undefines.h [new file with mode: 0644]
src/parser/cvc/Cvc.g
src/parser/cvc/cvc_input.cpp
src/parser/input.cpp
src/parser/input.h
src/parser/parser.cpp
src/parser/parser_builder.cpp
src/parser/smt1/Smt1.g
src/parser/smt1/smt1_input.cpp
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/parser/smt2/smt2_input.cpp
src/parser/smt2/smt2_input.h
src/parser/smt2/sygus_input.cpp
src/parser/tptp/Tptp.g
src/parser/tptp/tptp.cpp
src/parser/tptp/tptp.h
src/parser/tptp/tptp_input.cpp
src/printer/printer.h
src/proof/proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/prop/bvminisat/bvminisat.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/prop/theory_proxy.h
src/smt/managed_ostreams.cpp [new file with mode: 0644]
src/smt/managed_ostreams.h [new file with mode: 0644]
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/smt/smt_engine_check_proof.cpp
src/smt/smt_engine_scope.h
src/smt/smt_globals.cpp [deleted file]
src/smt/smt_globals.h [deleted file]
src/smt/smt_options_handler.cpp [deleted file]
src/smt/smt_options_handler.h [deleted file]
src/smt/update_ostream.h [new file with mode: 0644]
src/smt_util/Makefile.am
src/smt_util/boolean_simplification.h
src/smt_util/dump.cpp
src/smt_util/dump.h
src/smt_util/lemma_channels.cpp [new file with mode: 0644]
src/smt_util/lemma_channels.h [new file with mode: 0644]
src/theory/arith/constraint.h
src/theory/arith/cut_log.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/booleans/theory_bool.h
src/theory/builtin/theory_builtin.h
src/theory/bv/bitblaster_template.h
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/fp/theory_fp.cpp
src/theory/fp/theory_fp.h
src/theory/idl/theory_idl.cpp
src/theory/idl/theory_idl.h
src/theory/logic_info.cpp
src/theory/logic_info.h
src/theory/mktheorytraits
src/theory/quantifiers/theory_quantifiers.cpp
src/theory/quantifiers/theory_quantifiers.h
src/theory/sets/theory_sets.cpp
src/theory/sets/theory_sets.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
src/util/Makefile.am
src/util/cache.h
src/util/configuration.cpp [deleted file]
src/util/configuration.h [deleted file]
src/util/configuration.i [deleted file]
src/util/configuration_private.h [deleted file]
src/util/resource_manager.cpp
src/util/resource_manager.h
src/util/sexpr.cpp
test/system/smt2_compliance.cpp
test/unit/expr/attribute_black.h
test/unit/expr/expr_public.h
test/unit/expr/node_black.h
test/unit/prop/cnf_stream_white.h
test/unit/theory/theory_arith_white.h
test/unit/theory/theory_engine_white.h
test/unit/theory/theory_white.h
test/unit/util/configuration_black.h
test/unit/util/listener_black.h
test/unit/util/output_black.h