summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Makefile.am32
-rw-r--r--src/parser/options17
-rw-r--r--src/parser/parser.cpp2
-rw-r--r--src/parser/parser_builder.cpp12
-rw-r--r--src/parser/smt/Makefile.am30
-rw-r--r--src/parser/smt/Smt.g2
-rw-r--r--src/parser/smt2/Makefile.am30
-rw-r--r--src/parser/smt2/Smt2.g12
-rw-r--r--src/parser/tptp/Makefile.am30
9 files changed, 88 insertions, 79 deletions
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 15a572745..e5666b702 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -15,14 +15,14 @@ ANTLR_OPTS =
noinst_LTLIBRARIES = libparsercvc.la
ANTLR_TOKEN_STUFF = \
- @srcdir@/generated/Cvc.tokens
+ generated/Cvc.tokens
ANTLR_LEXER_STUFF = \
- @srcdir@/generated/CvcLexer.h \
- @srcdir@/generated/CvcLexer.c \
+ generated/CvcLexer.h \
+ generated/CvcLexer.c \
$(ANTLR_TOKEN_STUFF)
ANTLR_PARSER_STUFF = \
- @srcdir@/generated/CvcParser.h \
- @srcdir@/generated/CvcParser.c
+ generated/CvcParser.h \
+ generated/CvcParser.c
ANTLR_STUFF = \
$(ANTLR_LEXER_STUFF) \
$(ANTLR_PARSER_STUFF)
@@ -33,29 +33,27 @@ libparsercvc_la_SOURCES = \
cvc_input.cpp \
$(ANTLR_STUFF)
-BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+BUILT_SOURCES = $(ANTLR_STUFF) stamp-generated
-EXTRA_DIST = \
- @srcdir@/stamp-generated \
- README
+EXTRA_DIST = README
MAINTAINERCLEANFILES = $(ANTLR_STUFF)
maintainer-clean-local:
- -$(AM_V_at)rmdir @srcdir@/generated
- -$(AM_V_at)rm -f @srcdir@/stamp-generated
+ -$(AM_V_at)rmdir generated
+ -$(AM_V_at)rm -f stamp-generated
-@srcdir@/stamp-generated:
- $(AM_V_at)mkdir -p @srcdir@/generated
- $(AM_V_at)touch @srcdir@/stamp-generated
+stamp-generated:
+ $(AM_V_at)mkdir -p generated
+ $(AM_V_at)touch 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
+generated/CvcLexer.h: Cvc.g stamp-generated
-$(AM_V_at)rm -f $(ANTLR_STUFF)
@if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi
- $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Cvc.g"
+ $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "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
# from running in parallel (since the token files will be deleted &
# recreated)
-@srcdir@/generated/CvcLexer.c @srcdir@/generated/CvcParser.h @srcdir@/generated/CvcParser.c $(ANTLR_TOKEN_STUFF): @srcdir@/generated/CvcLexer.h
+generated/CvcLexer.c generated/CvcParser.h generated/CvcParser.c $(ANTLR_TOKEN_STUFF): generated/CvcLexer.h
diff --git a/src/parser/options b/src/parser/options
new file mode 100644
index 000000000..beae09823
--- /dev/null
+++ b/src/parser/options
@@ -0,0 +1,17 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module PARSER "parser/options.h" Parser
+
+common-option strictParsing --strict-parsing bool
+ be less tolerant of non-conforming inputs
+
+option memoryMap --mmap bool
+ memory map file input
+
+option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking
+ disable ALL semantic checks, including type checks
+
+endmodule
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 2265355f0..44148a7f1 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -29,7 +29,7 @@
#include "expr/kind.h"
#include "expr/type.h"
#include "util/output.h"
-#include "util/options.h"
+#include "options/options.h"
#include "util/Assert.h"
#include "parser/cvc/cvc_input.h"
#include "parser/smt/smt_input.h"
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index d9b7cf341..bd71f71e7 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -26,7 +26,7 @@
#include "tptp/tptp.h"
#include "expr/expr_manager.h"
-#include "util/options.h"
+#include "parser/options.h"
namespace CVC4 {
namespace parser {
@@ -146,11 +146,11 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
ParserBuilder& ParserBuilder::withOptions(const Options& options) {
return
- withInputLanguage(options.inputLanguage)
- .withMmap(options.memoryMap)
- .withChecks(options.semanticChecks)
- .withStrictMode(options.strictParsing)
- .withParseOnly(options.parseOnly);
+ withInputLanguage(options[options::inputLanguage])
+ .withMmap(options[options::memoryMap])
+ .withChecks(options[options::semanticChecks])
+ .withStrictMode(options[options::strictParsing])
+ .withParseOnly(options[options::parseOnly]);
}
ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 975a90b72..a74a6909c 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -15,14 +15,14 @@ ANTLR_OPTS =
noinst_LTLIBRARIES = libparsersmt.la
ANTLR_TOKEN_STUFF = \
- @srcdir@/generated/Smt.tokens
+ generated/Smt.tokens
ANTLR_LEXER_STUFF = \
- @srcdir@/generated/SmtLexer.h \
- @srcdir@/generated/SmtLexer.c \
+ generated/SmtLexer.h \
+ generated/SmtLexer.c \
$(ANTLR_TOKEN_STUFF)
ANTLR_PARSER_STUFF = \
- @srcdir@/generated/SmtParser.h \
- @srcdir@/generated/SmtParser.c
+ generated/SmtParser.h \
+ generated/SmtParser.c
ANTLR_STUFF = \
$(ANTLR_LEXER_STUFF) \
$(ANTLR_PARSER_STUFF)
@@ -35,27 +35,25 @@ libparsersmt_la_SOURCES = \
smt_input.cpp \
$(ANTLR_STUFF)
-BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
-
-EXTRA_DIST = @srcdir@/stamp-generated
+BUILT_SOURCES = $(ANTLR_STUFF) stamp-generated
MAINTAINERCLEANFILES = $(ANTLR_STUFF)
maintainer-clean-local:
- -$(AM_V_at)rmdir @srcdir@/generated
- -$(AM_V_at)rm -f @srcdir@/stamp-generated
+ -$(AM_V_at)rmdir generated
+ -$(AM_V_at)rm -f stamp-generated
-@srcdir@/stamp-generated:
- $(AM_V_at)mkdir -p @srcdir@/generated
- $(AM_V_at)touch @srcdir@/stamp-generated
+stamp-generated:
+ $(AM_V_at)mkdir -p generated
+ $(AM_V_at)touch 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
+generated/SmtLexer.h: Smt.g stamp-generated
-$(AM_V_at)rm -f $(ANTLR_STUFF)
@if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi
- $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Smt.g"
+ $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "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
# from running in parallel (since the token files will be deleted &
# recreated)
-@srcdir@/generated/SmtLexer.c @srcdir@/generated/SmtParser.h @srcdir@/generated/SmtParser.c $(ANTLR_TOKEN_STUFF): @srcdir@/generated/SmtLexer.h
+generated/SmtLexer.c generated/SmtParser.h generated/SmtParser.c $(ANTLR_TOKEN_STUFF): generated/SmtLexer.h
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 429adee0a..f9c38385f 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -565,7 +565,7 @@ annotation[CVC4::Command*& smt_command]
value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
value.erase(value.end() - 1);
value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), value.end());
- smt_command = new SetInfoCommand(key, value); }
+ smt_command = new SetInfoCommand(key.c_str() + 1, value); }
)?
{ if(smt_command == NULL) {
smt_command = new EmptyCommand(std::string("annotation: ") + key);
diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am
index 75ceec43a..8f7bf433c 100644
--- a/src/parser/smt2/Makefile.am
+++ b/src/parser/smt2/Makefile.am
@@ -15,14 +15,14 @@ ANTLR_OPTS =
noinst_LTLIBRARIES = libparsersmt2.la
ANTLR_TOKEN_STUFF = \
- @srcdir@/generated/Smt2.tokens
+ generated/Smt2.tokens
ANTLR_LEXER_STUFF = \
- @srcdir@/generated/Smt2Lexer.h \
- @srcdir@/generated/Smt2Lexer.c \
+ generated/Smt2Lexer.h \
+ generated/Smt2Lexer.c \
$(ANTLR_TOKEN_STUFF)
ANTLR_PARSER_STUFF = \
- @srcdir@/generated/Smt2Parser.h \
- @srcdir@/generated/Smt2Parser.c
+ generated/Smt2Parser.h \
+ generated/Smt2Parser.c
ANTLR_STUFF = \
$(ANTLR_LEXER_STUFF) \
$(ANTLR_PARSER_STUFF)
@@ -35,27 +35,25 @@ libparsersmt2_la_SOURCES = \
smt2_input.cpp \
$(ANTLR_STUFF)
-BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
-
-EXTRA_DIST = @srcdir@/stamp-generated
+BUILT_SOURCES = $(ANTLR_STUFF) stamp-generated
MAINTAINERCLEANFILES = $(ANTLR_STUFF)
maintainer-clean-local:
- -$(AM_V_at)rmdir @srcdir@/generated
- -$(AM_V_at)rm -f @srcdir@/stamp-generated
+ -$(AM_V_at)rmdir generated
+ -$(AM_V_at)rm -f stamp-generated
-@srcdir@/stamp-generated:
- $(AM_V_at)mkdir -p @srcdir@/generated
- $(AM_V_at)touch @srcdir@/stamp-generated
+stamp-generated:
+ $(AM_V_at)mkdir -p generated
+ $(AM_V_at)touch stamp-generated
# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first.
-@srcdir@/generated/Smt2Lexer.h: Smt2.g @srcdir@/stamp-generated
+generated/Smt2Lexer.h: Smt2.g stamp-generated
-$(AM_V_at)rm -f $(ANTLR_STUFF)
@if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi
- $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Smt2.g"
+ $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt2.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
# from running in parallel (since the token files will be deleted &
# recreated)
-@srcdir@/generated/Smt2Lexer.c @srcdir@/generated/Smt2Parser.h @srcdir@/generated/Smt2Parser.c $(ANTLR_TOKEN_STUFF): @srcdir@/generated/Smt2Lexer.h
+generated/Smt2Lexer.c generated/Smt2Parser.h generated/Smt2Parser.c $(ANTLR_TOKEN_STUFF): generated/Smt2Lexer.h
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 93d596264..dd0ccb0ad 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -183,19 +183,19 @@ command returns [CVC4::Command* cmd = NULL]
$cmd = new SetBenchmarkLogicCommand(name); }
| SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
{ name = AntlrInput::tokenText($KEYWORD);
- PARSER_STATE->setInfo(name,sexpr);
- cmd = new SetInfoCommand(name,sexpr); }
+ PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
+ cmd = new SetInfoCommand(name.c_str() + 1, sexpr); }
| /* get-info */
GET_INFO_TOK KEYWORD
- { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD)); }
+ { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
| /* set-option */
SET_OPTION_TOK KEYWORD symbolicExpr[sexpr]
{ name = AntlrInput::tokenText($KEYWORD);
- PARSER_STATE->setOption(name,sexpr);
- cmd = new SetOptionCommand(name,sexpr); }
+ PARSER_STATE->setOption(name.c_str() + 1, sexpr);
+ cmd = new SetOptionCommand(name.c_str() + 1, sexpr); }
| /* get-option */
GET_OPTION_TOK KEYWORD
- { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD)); }
+ { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
| /* sort declaration */
DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_SORT]
diff --git a/src/parser/tptp/Makefile.am b/src/parser/tptp/Makefile.am
index 4ec1717e9..3113a523c 100644
--- a/src/parser/tptp/Makefile.am
+++ b/src/parser/tptp/Makefile.am
@@ -15,14 +15,14 @@ ANTLR_OPTS =
noinst_LTLIBRARIES = libparsertptp.la
ANTLR_TOKEN_STUFF = \
- @srcdir@/generated/Tptp.tokens
+ generated/Tptp.tokens
ANTLR_LEXER_STUFF = \
- @srcdir@/generated/TptpLexer.h \
- @srcdir@/generated/TptpLexer.c \
+ generated/TptpLexer.h \
+ generated/TptpLexer.c \
$(ANTLR_TOKEN_STUFF)
ANTLR_PARSER_STUFF = \
- @srcdir@/generated/TptpParser.h \
- @srcdir@/generated/TptpParser.c
+ generated/TptpParser.h \
+ generated/TptpParser.c
ANTLR_STUFF = \
$(ANTLR_LEXER_STUFF) \
$(ANTLR_PARSER_STUFF)
@@ -35,27 +35,25 @@ libparsertptp_la_SOURCES = \
tptp_input.cpp \
$(ANTLR_STUFF)
-BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
-
-EXTRA_DIST = @srcdir@/stamp-generated
+BUILT_SOURCES = $(ANTLR_STUFF) stamp-generated
MAINTAINERCLEANFILES = $(ANTLR_STUFF)
maintainer-clean-local:
- -$(AM_V_at)rmdir @srcdir@/generated
- -$(AM_V_at)rm -f @srcdir@/stamp-generated
+ -$(AM_V_at)rmdir generated
+ -$(AM_V_at)rm -f stamp-generated
-@srcdir@/stamp-generated:
- $(AM_V_at)mkdir -p @srcdir@/generated
- $(AM_V_at)touch @srcdir@/stamp-generated
+stamp-generated:
+ $(AM_V_at)mkdir -p generated
+ $(AM_V_at)touch stamp-generated
# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first.
-@srcdir@/generated/TptpLexer.h: Tptp.g @srcdir@/stamp-generated
+generated/TptpLexer.h: Tptp.g stamp-generated
-$(AM_V_at)rm -f $(ANTLR_STUFF)
@if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi
- $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Tptp.g"
+ $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Tptp.g"
# These don't actually depend on TptpLexer.h, but if we're doing parallel
# make and the lexer needs to be rebuilt, we have to keep the rules
# from running in parallel (since the token files will be deleted &
# recreated)
-@srcdir@/generated/TptpLexer.c @srcdir@/generated/TptpParser.h @srcdir@/generated/TptpParser.c $(ANTLR_TOKEN_STUFF): @srcdir@/generated/TptpLexer.h
+generated/TptpLexer.c generated/TptpParser.h generated/TptpParser.c $(ANTLR_TOKEN_STUFF): generated/TptpLexer.h
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback