summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/Makefile.am2
-rw-r--r--src/parser/antlr_input.cpp7
-rw-r--r--src/parser/bounded_token_buffer.cpp3
-rw-r--r--src/parser/bounded_token_factory.cpp12
-rw-r--r--src/parser/bounded_token_factory.h20
-rw-r--r--src/parser/cvc/Cvc.g8
-rw-r--r--src/parser/cvc/Makefile.am14
-rw-r--r--src/parser/cvc/cvc_input.cpp12
-rw-r--r--src/parser/cvc/cvc_input.h18
-rw-r--r--src/parser/input.cpp2
-rw-r--r--src/parser/input.h11
-rw-r--r--src/parser/memory_mapped_input_buffer.cpp9
-rw-r--r--src/parser/memory_mapped_input_buffer.h17
-rw-r--r--src/parser/parser_exception.h6
-rw-r--r--src/parser/parser_options.h35
-rw-r--r--src/parser/smt/Makefile.am14
-rw-r--r--src/parser/smt/Smt.g6
-rw-r--r--src/parser/smt/smt_input.cpp12
-rw-r--r--src/parser/smt/smt_input.h44
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback