diff options
author | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
commit | 2ba8bb701ce289ba60afec01b653b0930cc59298 (patch) | |
tree | 46df365b7b41ce662a0f94de5b11c3ed20829851 /src/parser/smt2 | |
parent | 42b665f2a00643c81b42932fab1441987628c5a5 (diff) |
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}.
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 9 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 5 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 15 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 5 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.h | 2 | ||||
-rw-r--r-- | src/parser/smt2/sygus_input.cpp | 5 |
6 files changed, 31 insertions, 10 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7f639762a..8be9ad2dd 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -40,6 +40,10 @@ options { @lexer::includes { +// This should come immediately after #include <antlr3.h> 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 @@ -75,6 +79,11 @@ using namespace CVC4::parser; }/* @lexer::postinclude */ @parser::includes { + +// This should come immediately after #include <antlr3.h> in the generated +// files. See the documentation in "parser/antlr_undefines.h" for more details. +#include "parser/antlr_undefines.h" + #include "parser/parser.h" #include "parser/antlr_tracing.h" #include "smt_util/command.h" diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 355b58067..3b1467b5e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -20,6 +20,7 @@ #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/smt1/smt1.h" +#include "parser/smt2/smt2_input.h" #include "smt_util/command.h" #include "util/bitvector.h" @@ -40,6 +41,10 @@ Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn } } +void Smt2::setLanguage(InputLanguage lang) { + ((Smt2Input*) getInput())->setLanguage(lang); +} + void Smt2::addArithmeticOperators() { Parser::addOperator(kind::PLUS); Parser::addOperator(kind::MINUS); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index c8b89799c..7cf92f008 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -19,16 +19,15 @@ #ifndef __CVC4__PARSER__SMT2_H #define __CVC4__PARSER__SMT2_H +#include <sstream> +#include <stack> +#include <string> +#include <utility> + #include "parser/parser.h" #include "parser/smt1/smt1.h" #include "theory/logic_info.h" #include "util/abstract_value.h" -#include "parser/smt2/smt2_input.h" - -#include <string> -#include <sstream> -#include <utility> -#include <stack> namespace CVC4 { @@ -115,9 +114,7 @@ public: return getInput()->getLanguage() == language::input::LANG_SYGUS; } - void setLanguage(InputLanguage lang) { - ((Smt2Input*) getInput())->setLanguage(lang); - } + void setLanguage(InputLanguage lang); void setInfo(const std::string& flag, const SExpr& sexpr); diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 9f1fae16f..cea6db278 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -14,9 +14,14 @@ ** [[ 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 <antlr3.h> +#include "parser/antlr_undefines.h" + #include "parser/smt2/smt2_input.h" + #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 0eb4a504b..9a07ddc08 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -26,7 +26,7 @@ // extern void Smt2ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); namespace CVC4 { - + class Command; class Expr; class ExprManager; diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp index 086a04d27..e4f36b3df 100644 --- a/src/parser/smt2/sygus_input.cpp +++ b/src/parser/smt2/sygus_input.cpp @@ -14,9 +14,14 @@ ** [[ 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 <antlr3.h> +#include "parser/antlr_undefines.h" + #include "parser/smt2/sygus_input.h" + #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" |