diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/Makefile.am | 2 | ||||
-rw-r--r-- | src/parser/antlr_input.cpp | 7 | ||||
-rw-r--r-- | src/parser/bounded_token_buffer.cpp | 3 | ||||
-rw-r--r-- | src/parser/bounded_token_factory.cpp | 12 | ||||
-rw-r--r-- | src/parser/bounded_token_factory.h | 20 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 8 | ||||
-rw-r--r-- | src/parser/cvc/Makefile.am | 14 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.cpp | 12 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.h | 18 | ||||
-rw-r--r-- | src/parser/input.cpp | 2 | ||||
-rw-r--r-- | src/parser/input.h | 11 | ||||
-rw-r--r-- | src/parser/memory_mapped_input_buffer.cpp | 9 | ||||
-rw-r--r-- | src/parser/memory_mapped_input_buffer.h | 17 | ||||
-rw-r--r-- | src/parser/parser_exception.h | 6 | ||||
-rw-r--r-- | src/parser/parser_options.h | 35 | ||||
-rw-r--r-- | src/parser/smt/Makefile.am | 14 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 6 | ||||
-rw-r--r-- | src/parser/smt/smt_input.cpp | 12 | ||||
-rw-r--r-- | src/parser/smt/smt_input.h | 44 |
19 files changed, 108 insertions, 144 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index ee0a23c98..5d8b75f38 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -15,7 +15,7 @@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -fvisibility=hidden -Wno-deprecated +AM_CXXFLAGS = -Wall -fvisibility=hidden SUBDIRS = smt cvc diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 0c0006031..901735b1f 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -13,13 +13,6 @@ ** A super-class for ANTLR-generated input language parsers **/ -/* - * antlr_parser.cpp - * - * Created on: Nov 30, 2009 - * Author: dejan - */ - #include <iostream> #include <limits.h> #include <antlr3.h> diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index f53b6d548..1418e8f3c 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -35,8 +35,7 @@ #include <antlr3lexer.h> #include <antlr3tokenstream.h> -#include "bounded_token_buffer.h" -#include "cvc4_config.h" +#include "parser/bounded_token_buffer.h" #include "util/Assert.h" namespace CVC4 { diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp index dae2f46e5..0209eb172 100644 --- a/src/parser/bounded_token_factory.cpp +++ b/src/parser/bounded_token_factory.cpp @@ -1,10 +1,3 @@ -/* - * bounded_token_factory.cpp - * - * Created on: Mar 2, 2010 - * Author: dejan - */ - #include <antlr3input.h> #include <antlr3commontoken.h> #include <antlr3interfaces.h> @@ -130,5 +123,6 @@ setInputStream (pANTLR3_TOKEN_FACTORY factory, pANTLR3_INPUT_STREAM input) factory->unTruc.strFactory = NULL; } } -} -} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h index 6f8729c19..8f8177544 100644 --- a/src/parser/bounded_token_factory.h +++ b/src/parser/bounded_token_factory.h @@ -1,12 +1,7 @@ -/* - * bounded_token_factory.h - * - * Created on: Mar 2, 2010 - * Author: dejan - */ +#include "cvc4parser_private.h" -#ifndef BOUNDED_TOKEN_FACTORY_H_ -#define BOUNDED_TOKEN_FACTORY_H_ +#ifndef __CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H +#define __CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H namespace CVC4 { namespace parser { @@ -28,11 +23,10 @@ pANTLR3_TOKEN_FACTORY BoundedTokenFactoryNew(pANTLR3_INPUT_STREAM input,ANTLR3_UINT32 size); #ifdef __cplusplus -} +}/* extern "C" */ #endif -} -} - +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -#endif /* BOUNDED_TOKEN_FACTORY_H_ */ +#endif /* __CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 4cb4d577b..d2ac81167 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -74,6 +74,8 @@ using namespace CVC4::parser; #define EXPR_MANAGER ANTLR_INPUT->getExprManager() #undef MK_EXPR #define MK_EXPR EXPR_MANAGER->mkExpr +#undef MK_CONST +#define MK_CONST EXPR_MANAGER->mkConst } /** @@ -105,7 +107,7 @@ command returns [CVC4::Command* cmd = 0] : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); } | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f); } | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); } - | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_EXPR(CVC4::kind::TRUE)); } + | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_CONST(true)); } | PUSH_TOK SEMICOLON { cmd = new PushCommand(); } | POP_TOK SEMICOLON { cmd = new PopCommand(); } | declaration[cmd] @@ -369,8 +371,8 @@ term[CVC4::Expr& f] LPAREN formula[f] RPAREN /* constants */ - | TRUE_TOK { f = MK_EXPR(CVC4::kind::TRUE); } - | FALSE_TOK { f = MK_EXPR(CVC4::kind::FALSE); } + | TRUE_TOK { f = MK_CONST(true); } + | FALSE_TOK { f = MK_CONST(false); } | /* variable */ identifier[name,CHECK_DECLARED,SYM_VARIABLE] diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index f02c9345c..ade8d83e7 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -2,8 +2,10 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -fvisibility=hidden + # Compile generated C files using C++ compiler CC=$(CXX) +AM_CFLAGS = $(AM_CXXFLAGS) noinst_LTLIBRARIES = libparsercvc.la @@ -30,17 +32,17 @@ BUILT_SOURCES = $(ANTLR_STUFF) dist-hook: $(ANTLR_STUFF) MAINTAINERCLEANFILES = $(ANTLR_STUFF) maintainer-clean-local: - -rmdir @srcdir@/generated - -rm -f @srcdir@/stamp-generated + -$(AM_V_at)rmdir @srcdir@/generated + -$(AM_V_at)rm -f @srcdir@/stamp-generated @srcdir@/stamp-generated: - mkdir -p @srcdir@/generated - touch @srcdir@/stamp-generated + $(AM_V_at)mkdir -p @srcdir@/generated + $(AM_V_at)touch @srcdir@/stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/CvcLexer.h: Cvc.g @srcdir@/stamp-generated - -rm -f $(ANTLR_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/Cvc.g" + -$(AM_V_at)rm -f $(ANTLR_STUFF) + $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Cvc.g" # These don't actually depend on CvcLexer.h, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 1f1a602c5..241ce62f3 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -1,10 +1,3 @@ -/* - * cvc_parser.cpp - * - * Created on: Mar 5, 2010 - * Author: chris - */ - #include <antlr3.h> #include "expr/expr_manager.h" @@ -69,6 +62,5 @@ pANTLR3_LEXER CvcInput::getLexer() { } */ -} // namespace parser - -} // namespace CVC4 +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index a6117b4a9..9908a25aa 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -1,12 +1,7 @@ -/* - * cvc_parser.h - * - * Created on: Mar 5, 2010 - * Author: chris - */ +#include "cvc4parser_public.h" -#ifndef CVC_PARSER_H_ -#define CVC_PARSER_H_ +#ifndef __CVC4__PARSER__CVC_INPUT_H +#define __CVC4__PARSER__CVC_INPUT_H #include "parser/antlr_input.h" #include "parser/cvc/generated/CvcLexer.h" @@ -76,8 +71,7 @@ private: }; // class CvcInput -} // namespace parser +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -} // namespace CVC4 - -#endif /* CVC_PARSER_H_ */ +#endif /* __CVC4__PARSER__CVC_INPUT_H */ diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 01de4ea4f..0fd9a2628 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -1,5 +1,5 @@ /********************* */ -/** parser.cpp +/** input.cpp ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): cconway diff --git a/src/parser/input.h b/src/parser/input.h index 90cdc4e8d..a255ede12 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -1,8 +1,8 @@ /********************* */ -/** parser.h - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway +/** input.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -13,13 +13,14 @@ ** Parser abstraction. **/ +#include "cvc4parser_public.h" + #ifndef __CVC4__PARSER__PARSER_H #define __CVC4__PARSER__PARSER_H #include <string> #include <iostream> -#include "cvc4_config.h" #include "expr/expr.h" #include "expr/kind.h" #include "parser/parser_exception.h" diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index 6618ecebc..f1a7b5729 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -1,10 +1,3 @@ -/* - * memory_mapped_input_buffer.cpp - * - * Created on: Mar 3, 2010 - * Author: chris - */ - #include <fcntl.h> #include <stdio.h> #include <stdint.h> @@ -14,7 +7,7 @@ #include <sys/stat.h> #include <antlr3input.h> -#include "memory_mapped_input_buffer.h" +#include "parser/memory_mapped_input_buffer.h" #include "util/Assert.h" #include "util/exception.h" diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h index 88ba2183a..4146eec02 100644 --- a/src/parser/memory_mapped_input_buffer.h +++ b/src/parser/memory_mapped_input_buffer.h @@ -1,6 +1,8 @@ /********************* */ -/** memory_mapped_input_buffer.cpp +/** memory_mapped_input_buffer.h ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -11,6 +13,8 @@ ** ANTLR input buffer from a memory-mapped file. **/ +#include "cvc4parser_private.h" + #ifndef __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H #define __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H @@ -20,15 +24,18 @@ namespace CVC4 { namespace parser { +#ifdef __cplusplus extern "C" { +#endif pANTLR3_INPUT_STREAM MemoryMappedInputBufferNew(const std::string& filename); -} - -} -} +#ifdef __cplusplus +}/* extern "C" */ +#endif +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H */ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index ee02289ee..9bbe7d709 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -13,15 +13,17 @@ ** Exception class for parse errors. **/ +#include "cvc4parser_public.h" + #ifndef __CVC4__PARSER__PARSER_EXCEPTION_H #define __CVC4__PARSER__PARSER_EXCEPTION_H -#include "util/exception.h" -#include "cvc4_config.h" #include <iostream> #include <string> #include <sstream> +#include "util/exception.h" + namespace CVC4 { namespace parser { diff --git a/src/parser/parser_options.h b/src/parser/parser_options.h index ddba219a4..ae1d99542 100644 --- a/src/parser/parser_options.h +++ b/src/parser/parser_options.h @@ -1,27 +1,22 @@ -/* - * parser_options.h - * - * Created on: Mar 3, 2010 - * Author: chris - */ +#include "cvc4_public.h" -#ifndef CVC4__PARSER__PARSER_OPTIONS_H_ -#define CVC4__PARSER__PARSER_OPTIONS_H_ +#ifndef __CVC4__PARSER__PARSER_OPTIONS_H +#define __CVC4__PARSER__PARSER_OPTIONS_H namespace CVC4 { namespace parser { - /** The input language option */ - enum InputLanguage { - /** The SMTLIB input language */ - LANG_SMTLIB, - /** The CVC4 input language */ - LANG_CVC4, - /** Auto-detect the language */ - LANG_AUTO - }; +/** The input language option */ +enum InputLanguage { + /** The SMTLIB input language */ + LANG_SMTLIB, + /** The CVC4 input language */ + LANG_CVC4, + /** Auto-detect the language */ + LANG_AUTO +};/* enum InputLanguage */ -} -} +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -#endif /* CVC4__PARSER__PARSER_OPTIONS_H_ */ +#endif /* __CVC4__PARSER__PARSER_OPTIONS_H */ diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 3ea6dc940..f081f493f 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -2,7 +2,9 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -fvisibility=hidden + # Compile generated C files using C++ compiler +AM_CFLAGS = $(AM_CXXFLAGS) CC=$(CXX) noinst_LTLIBRARIES = libparsersmt.la @@ -30,17 +32,17 @@ BUILT_SOURCES = $(ANTLR_STUFF) dist-hook: $(ANTLR_STUFF) MAINTAINERCLEANFILES = $(ANTLR_STUFF) maintainer-clean-local: - -rmdir @srcdir@/generated - -rm -f @srcdir@/stamp-generated + -$(AM_V_at)rmdir @srcdir@/generated + -$(AM_V_at)rm -f @srcdir@/stamp-generated @srcdir@/stamp-generated: - mkdir -p @srcdir@/generated - touch @srcdir@/stamp-generated + $(AM_V_at)mkdir -p @srcdir@/generated + $(AM_V_at)touch @srcdir@/stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/SmtLexer.h: Smt.g @srcdir@/stamp-generated - -rm -f $(ANTLR_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/Smt.g" + -$(AM_V_at)rm -f $(ANTLR_STUFF) + $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Smt.g" # These don't actually depend on SmtLexer.h, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 789e01670..48a0eddef 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -74,6 +74,8 @@ using namespace CVC4::parser; #define EXPR_MANAGER ANTLR_INPUT->getExprManager() #undef MK_EXPR #define MK_EXPR EXPR_MANAGER->mkExpr +#undef MK_CONST +#define MK_CONST EXPR_MANAGER->mkConst } /** @@ -206,8 +208,8 @@ annotatedFormula[CVC4::Expr& expr] { expr = ANTLR_INPUT->getVariable(name); } /* constants */ - | TRUE_TOK { expr = MK_EXPR(CVC4::kind::TRUE); } - | FALSE_TOK { expr = MK_EXPR(CVC4::kind::FALSE); } + | TRUE_TOK { expr = MK_CONST(true); } + | FALSE_TOK { expr = MK_CONST(false); } /* TODO: let, flet, quantifiers, arithmetic constants */ ; diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp index db4d89860..cd62eec39 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -1,10 +1,3 @@ -/* - * smt_parser.cpp - * - * Created on: Mar 5, 2010 - * Author: chris - */ - #include <antlr3.h> #include "expr/expr_manager.h" @@ -65,6 +58,5 @@ Expr SmtInput::doParseExpr() throw (ParserException) { return d_pSmtParser->parseExpr(d_pSmtParser); } -} // namespace parser - -} // namespace CVC4 +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index 4795edc91..3e295d18a 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -1,12 +1,7 @@ -/* - * smt_parser.h - * - * Created on: Mar 5, 2010 - * Author: chris - */ +#include "cvc4parser_public.h" -#ifndef SMT_PARSER_H_ -#define SMT_PARSER_H_ +#ifndef __CVC4__PARSER__SMT_INPUT_H +#define __CVC4__PARSER__SMT_INPUT_H #include "parser/antlr_input.h" #include "parser/smt/generated/SmtLexer.h" @@ -32,7 +27,8 @@ class SmtInput : public AntlrInput { public: - /** Create a file input. + /** + * Create a file input. * * @param exprManager the manager to use when building expressions from the input * @param filename the path of the file to read @@ -41,7 +37,8 @@ public: */ SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap); - /** Create a string input. + /** + * Create a string input. * * @param exprManager the manager to use when building expressions from the input * @param input the string to read @@ -49,20 +46,22 @@ public: */ SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name); - /* Destructor. Frees the lexer and the parser. */ + /** Destructor. Frees the lexer and the parser. */ ~SmtInput(); protected: - /** Parse a command from the input. Returns <code>NULL</code> if there is - * no command there to parse. + /** + * Parse a command from the input. Returns <code>NULL</code> if + * there is no command there to parse. * * @throws ParserException if an error is encountered during parsing. */ Command* doParseCommand() throw(ParserException); - /** Parse an expression from the input. Returns a null <code>Expr</code> - * if there is no expression there to parse. + /** + * Parse an expression from the input. Returns a null + * <code>Expr</code> if there is no expression there to parse. * * @throws ParserException if an error is encountered during parsing. */ @@ -70,14 +69,15 @@ protected: private: - /** Initialize the class. Called from the constructors once the input stream - * is initialized. */ + /** + * Initialize the class. Called from the constructors once the input + * stream is initialized. + */ void init(); -}; // class SmtInput - -} // namespace parser +};/* class SmtInput */ -} // namespace CVC4 +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -#endif /* SMT_PARSER_H_ */ +#endif /* __CVC4__PARSER__SMT_INPUT_H */ |