From 2ba8bb701ce289ba60afec01b653b0930cc59298 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 28 Jan 2016 12:35:45 -0800 Subject: 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}. --- src/parser/cvc/Cvc.g | 8 ++++++++ src/parser/cvc/cvc_input.cpp | 6 +++++- 2 files changed, 13 insertions(+), 1 deletion(-) (limited to 'src/parser/cvc') diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 21e01e7ed..08fba893e 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -463,6 +463,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { @lexer::includes { +// This should come immediately after #include in the generated +// files. See the documentation in "parser/antlr_undefines.h" for more details. +#include "parser/antlr_undefines.h" + /** This suppresses warnings about the redefinition of token symbols between different * parsers. The redefinitions should be harmless as long as no client: (a) #include's * the lexer headers for two grammars AND (b) uses the token symbol definitions. */ @@ -487,6 +491,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { @parser::includes { +// This should come immediately after #include in the generated +// files. See the documentation in "parser/antlr_undefines.h" for more details. +#include "parser/antlr_undefines.h" + #include #include #include "options/set_language.h" diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 69920403f..2370109ef 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -14,12 +14,16 @@ ** [[ Add file-specific comments here ]] **/ +// These headers should be the first two included. +// See the documentation in "parser/antlr_undefines.h" for more details. #include +#include "parser/antlr_undefines.h" + +#include "parser/cvc/cvc_input.h" #include "expr/expr_manager.h" #include "parser/antlr_input.h" #include "parser/parser_exception.h" -#include "parser/cvc/cvc_input.h" #include "parser/cvc/CvcLexer.h" #include "parser/cvc/CvcParser.h" -- cgit v1.2.3