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 | |
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')
-rw-r--r-- | src/parser/Makefile.am | 21 | ||||
-rw-r--r-- | src/parser/antlr_input.cpp | 8 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 23 | ||||
-rw-r--r-- | src/parser/antlr_input_imports.cpp | 6 | ||||
-rw-r--r-- | src/parser/antlr_line_buffered_input.cpp | 16 | ||||
-rw-r--r-- | src/parser/antlr_line_buffered_input.h | 7 | ||||
-rw-r--r-- | src/parser/antlr_undefines.h | 69 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 8 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.cpp | 6 | ||||
-rw-r--r-- | src/parser/input.cpp | 10 | ||||
-rw-r--r-- | src/parser/input.h | 4 | ||||
-rw-r--r-- | src/parser/parser.cpp | 10 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 25 | ||||
-rw-r--r-- | src/parser/smt1/Smt1.g | 9 | ||||
-rw-r--r-- | src/parser/smt1/smt1_input.cpp | 4 | ||||
-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 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 9 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 5 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 4 | ||||
-rw-r--r-- | src/parser/tptp/tptp_input.cpp | 4 |
25 files changed, 217 insertions, 72 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index c8a8cc941..18e77fab3 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -37,25 +37,26 @@ libcvc4parser_la_LIBADD += \ endif libcvc4parser_la_SOURCES = \ - antlr_input.h \ antlr_input.cpp \ + antlr_input.h \ antlr_input_imports.cpp \ - antlr_line_buffered_input.h \ antlr_line_buffered_input.cpp \ - bounded_token_buffer.h \ + antlr_line_buffered_input.h \ + antlr_tracing.h \ + antlr_undefines.h \ bounded_token_buffer.cpp \ - bounded_token_factory.h \ + bounded_token_buffer.h \ bounded_token_factory.cpp \ - input.h \ + bounded_token_factory.h \ input.cpp \ - memory_mapped_input_buffer.h \ + input.h \ memory_mapped_input_buffer.cpp \ - parser.h \ + memory_mapped_input_buffer.h \ parser.cpp \ - parser_builder.h \ + parser.h \ parser_builder.cpp \ - parser_exception.h \ - antlr_tracing.h + parser_builder.h \ + parser_exception.h EXTRA_DIST = \ Makefile.antlr_tracing \ diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 21e48b19e..6428017f5 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -14,13 +14,17 @@ ** A super-class for ANTLR-generated input language parsers **/ +#include "parser/antlr_input.h" +// We rely on the inclusion of #include <antlr3.h> in "parser/antlr_input.h". +// This is avoid having to undefine the symbols in <antlr3.h>. +// See the documentation in "parser/antlr_undefines.h" for more +// details. + #include <limits.h> -#include <antlr3.h> #include <stdint.h> #include "base/output.h" #include "expr/type.h" -#include "parser/antlr_input.h" #include "parser/antlr_line_buffered_input.h" #include "parser/bounded_token_buffer.h" #include "parser/bounded_token_factory.h" diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index baec46e6f..241d1bc83 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -14,21 +14,17 @@ ** Base for ANTLR parser classes. **/ -#include <antlr3.h> +#ifndef __CVC4__PARSER__ANTLR_INPUT_H +#define __CVC4__PARSER__ANTLR_INPUT_H -// ANTLR3 headers define these in our space :( -// undef them so that we don't get multiple-definition warnings -#undef PACKAGE_BUGREPORT -#undef PACKAGE_NAME -#undef PACKAGE_STRING -#undef PACKAGE_TARNAME -#undef PACKAGE_VERSION +// These headers must be included first. See the documentation +// in parser/antlr_undefines.h for an explanation. +// Also while unusual this must also be within the #ifdef guard. +#include <antlr3.h> +#include "parser/antlr_undefines.h" #include "cvc4parser_private.h" -#ifndef __CVC4__PARSER__ANTLR_INPUT_H -#define __CVC4__PARSER__ANTLR_INPUT_H - #include <iostream> #include <sstream> #include <stdexcept> @@ -72,10 +68,11 @@ private: pANTLR3_UINT8 inputString); /* This is private and unimplemented, because you should never use it. */ - AntlrInputStream(const AntlrInputStream& inputStream) CVC4_UNUSED; + AntlrInputStream(const AntlrInputStream& inputStream) CVC4_UNDEFINED; /* This is private and unimplemented, because you should never use it. */ - AntlrInputStream& operator=(const AntlrInputStream& inputStream) CVC4_UNUSED; + AntlrInputStream& operator=(const AntlrInputStream& inputStream) + CVC4_UNDEFINED; public: diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index f50dd5879..e74d83882 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -51,7 +51,13 @@ // (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF // THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + +// These headers must 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 <sstream> #include "parser/antlr_input.h" diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp index cc1d499fb..99b4a3068 100644 --- a/src/parser/antlr_line_buffered_input.cpp +++ b/src/parser/antlr_line_buffered_input.cpp @@ -15,22 +15,19 @@ ** \todo document this file **/ -#include <antlr3.h> +// We rely on the inclusion of #include <antlr3.h> in +// "parser/antlr_line_buffered_input.h". +// This is avoid having to undefine the symbols in <antlr3.h>. +// See the documentation in "parser/antlr_undefines.h" for more +// details. -// ANTLR3 headers define these in our space :( -// undef them so that we don't get multiple-definition warnings -#undef PACKAGE_BUGREPORT -#undef PACKAGE_NAME -#undef PACKAGE_STRING -#undef PACKAGE_TARNAME -#undef PACKAGE_VERSION +#include "parser/antlr_line_buffered_input.h" #include <iostream> #include <string> #include <cassert> #include "base/output.h" -#include "parser/antlr_line_buffered_input.h" namespace CVC4 { namespace parser { @@ -380,4 +377,3 @@ antlr3CreateLineBufferedStream(std::istream& in) }/* CVC4::parser namespace */ }/* CVC4 namespace */ - diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h index 13a6486cd..c47ab324f 100644 --- a/src/parser/antlr_line_buffered_input.h +++ b/src/parser/antlr_line_buffered_input.h @@ -15,12 +15,17 @@ ** \todo document this file **/ +// 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 "cvc4parser_private.h" #ifndef __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H #define __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H -#include <antlr3.h> +#include <istream> namespace CVC4 { namespace parser { diff --git a/src/parser/antlr_undefines.h b/src/parser/antlr_undefines.h new file mode 100644 index 000000000..35a6c7e12 --- /dev/null +++ b/src/parser/antlr_undefines.h @@ -0,0 +1,69 @@ +/********************* */ +/*! \file antlr_undefines.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Every usage undefines standard autotools macro names. + ** + ** This header is very sensitive and it should be understood *in full* before + ** it is used or *moved* in position relative to other headers. + ** + ** Including this header runs #undef on the following identifiers: + ** - PACKAGE_BUGREPORT, + ** - PACKAGE_NAME + ** - PACKAGE_STRING + ** - PACKAGE_TARNAME + ** - PACKAGE_VERSION + ** + ** This is to solves a problem caused by antlr and cvc4 both defining these + ** symbols. This has to do with both packages using autotools in a slightly + ** dicey way. This was reported by us a long time ago, but most versions + ** of libantlr are quite old (3.2). + ** http://www.antlr3.org/pipermail/antlr-interest/2010-March/037859.html + ** + ** The source of both of these two definitions are given below. + ** + ** From antlr, the autogenerated antlr lexers and parsers include antlr3.h. + ** The chain of inclusions is: + ** Lang{Lexer,Parser}.h -> <antlr3.h> -> <antlr3config.h> -> <antlr3defs.h> + ** + ** where Lang is in {Smt1,Smt2,Tptp,Cvc}. + ** + ** From CVC4, the parsers use Debug("...") and other features from + ** "base/output.h". This is a cvc4_private_library.h header file. This means + ** the files is usable while building the driver and parsers, but is otherwise + ** conceptually the same as a cvc4_private.h header. (If that sounds sketchy, + ** it is sure is! [See src/DESIGN.txt for more details].) + ** The include chain is then + ** "base/output.h" -> "cvc4_private_library.h" -> "cvc4_private.h" -> + ** "cvc4autoconfig.h". + ** The file cvc4autoconfig.h is autogenerated by autotools and can be found in + ** builds/<arch>/<target>/cvc4autoconfig.h + ** + ** Thus a working solution is to include this header immediately after all + ** locations of #include <antlr3.h>. This includes all autogenerated files. + ** This potentially has to be repeated so this header should not be guarded. + ** + ** To ensure that we do not remove cvc4's versions and use antlr's by mistake + ** #include <antlr3.h> needs to proceed any other includes like + ** #include "cvc4parser_private.h". + ** + ** It is worth noting that future version of antlr can both not define these + ** macros and may generate different code. This is at best a stop gap + ** solution. + ** + ** Every location this header is included needs to be documented. + ** When in doubt do not move this header! + **/ + +#undef PACKAGE_BUGREPORT +#undef PACKAGE_NAME +#undef PACKAGE_STRING +#undef PACKAGE_TARNAME +#undef PACKAGE_VERSION 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 <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 token symbol definitions. */ @@ -487,6 +491,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { @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 <stdint.h> #include <cassert> #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 <antlr3.h> +#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" diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 82b6dd32f..7cc5ac0ca 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -14,14 +14,16 @@ ** A super-class for input language parsers **/ +// This must be included first. +#include "parser/antlr_input.h" + #include "parser/input.h" -#include "parser/parser_exception.h" -#include "parser/parser.h" #include "base/output.h" -#include "smt_util/command.h" #include "expr/type.h" -#include "parser/antlr_input.h" +#include "parser/parser.h" +#include "parser/parser_exception.h" +#include "smt_util/command.h" using namespace std; diff --git a/src/parser/input.h b/src/parser/input.h index dcb54d256..4ff37409c 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -94,8 +94,8 @@ class CVC4_PUBLIC Input { * copy construction and assignment. Mark them private and do not define * them. */ - Input(const Input& input) CVC4_UNUSED; - Input& operator=(const Input& input) CVC4_UNUSED; + Input(const Input& input) CVC4_UNDEFINED; + Input& operator=(const Input& input) CVC4_UNDEFINED; public: diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index adbeaabd3..3cfe78145 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -30,7 +30,6 @@ #include "expr/kind.h" #include "expr/type.h" #include "options/options.h" -#include "options/smt_options.h" #include "parser/input.h" #include "parser/parser_exception.h" #include "smt_util/command.h" @@ -500,17 +499,20 @@ Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) Debug("parser") << "nextCommand() => " << cmd << std::endl; if (cmd != NULL && dynamic_cast<SetOptionCommand*>(cmd) == NULL && - dynamic_cast<QuitCommand*>(cmd) == NULL) { + dynamic_cast<QuitCommand*>(cmd) == NULL) + { // don't count set-option commands as to not get stuck in an infinite // loop of resourcing out - d_resourceManager->spendResource(d_exprManager->getOptions()[options::parseStep]); + const Options& options = d_exprManager->getOptions(); + d_resourceManager->spendResource(options.getParseStep()); } return cmd; } Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) { Debug("parser") << "nextExpression()" << std::endl; - d_resourceManager->spendResource(d_exprManager->getOptions()[options::parseStep]); + const Options& options = d_exprManager->getOptions(); + d_resourceManager->spendResource(options.getParseStep()); Expr result; if(!done()) { try { diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index f473ae178..e095d208b 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -13,16 +13,18 @@ ** ** A builder for parsers. **/ + +// This must be included first. +#include "parser/antlr_input.h" + #include "parser/parser_builder.h" #include <string> #include "expr/expr_manager.h" -#include "options/base_options.h" -#include "options/parser_options.h" -#include "options/smt_options.h" #include "parser/input.h" #include "parser/parser.h" +#include "options/options.h" #include "smt1/smt1.h" #include "smt2/smt2.h" #include "tptp/tptp.h" @@ -161,14 +163,15 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) { ParserBuilder& ParserBuilder::withOptions(const Options& options) { ParserBuilder& retval = *this; retval = - retval.withInputLanguage(options[options::inputLanguage]) - .withMmap(options[options::memoryMap]) - .withChecks(options[options::semanticChecks]) - .withStrictMode(options[options::strictParsing]) - .withParseOnly(options[options::parseOnly]) - .withIncludeFile(options[options::filesystemAccess]); - if(options.wasSetByUser(options::forceLogic)) { - retval = retval.withForcedLogic(options[options::forceLogic]->getLogicString()); + retval.withInputLanguage(options.getInputLanguage()) + .withMmap(options.getMemoryMap()) + .withChecks(options.getSemanticChecks()) + .withStrictMode(options.getStrictParsing()) + .withParseOnly(options.getParseOnly()) + .withIncludeFile(options.getFilesystemAccess()); + if(options.wasSetByUserForceLogicString()) { + LogicInfo tmp(options.getForceLogicString()); + retval = retval.withForcedLogic(tmp.getLogicString()); } return retval; } diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index 98825f1c3..e8b7d5b9b 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -39,6 +39,11 @@ options { }/* @header */ @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 @@ -61,6 +66,10 @@ options { @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 <stdint.h> #include "smt_util/command.h" diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp index 1391c7e85..8a8aa577e 100644 --- a/src/parser/smt1/smt1_input.cpp +++ b/src/parser/smt1/smt1_input.cpp @@ -14,9 +14,13 @@ ** [[ Add file-specific comments here ]] **/ +// These headers must 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/smt1/smt1_input.h" + #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" 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" diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index a2bad4988..52951dd38 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -41,6 +41,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 @@ -83,6 +87,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 "smt_util/command.h" #include "parser/parser.h" #include "parser/tptp/tptp.h" diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index b674b12dc..9d3bd4b1c 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -14,10 +14,11 @@ ** Definitions of TPTP constants. **/ +// Do not #include "parser/antlr_input.h" directly. Rely on the header. +#include "parser/tptp/tptp.h" + #include "expr/type.h" #include "parser/parser.h" -#include "parser/tptp/tptp.h" -#include "parser/antlr_input.h" // ANTLR defines these, which is really bad! #undef true diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 4fdbc236d..5e00ea1ce 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -14,6 +14,8 @@ ** Definitions of TPTP constants. **/ +#include "parser/antlr_input.h" // Needs to go first. + #include "cvc4parser_private.h" #ifndef __CVC4__PARSER__TPTP_H @@ -22,8 +24,6 @@ #include <cassert> #include <ext/hash_set> -#include "options/parser_options.h" -#include "parser/antlr_input.h" #include "parser/parser.h" #include "smt_util/command.h" #include "util/hash.h" diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index e41a539bb..5a393a58c 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -14,7 +14,11 @@ ** [[ 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/tptp/tptp_input.h" #include "expr/expr_manager.h" |