diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_input.cpp | 15 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 6 | ||||
-rw-r--r-- | src/parser/antlr_line_buffered_input.cpp | 2 | ||||
-rw-r--r-- | src/parser/antlr_tracing.h | 3 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 17 | ||||
-rw-r--r-- | src/parser/input.cpp | 5 | ||||
-rw-r--r-- | src/parser/input.h | 4 | ||||
-rw-r--r-- | src/parser/memory_mapped_input_buffer.cpp | 2 | ||||
-rw-r--r-- | src/parser/options | 34 | ||||
-rw-r--r-- | src/parser/parser.cpp | 24 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 11 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 3 | ||||
-rw-r--r-- | src/parser/parser_exception.h | 2 | ||||
-rw-r--r-- | src/parser/smt1/Smt1.g | 9 | ||||
-rw-r--r-- | src/parser/smt1/smt1.cpp | 2 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 26 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 8 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 13 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 11 |
19 files changed, 83 insertions, 114 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 1d2dbd736..21e48b19e 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -18,23 +18,22 @@ #include <antlr3.h> #include <stdint.h> +#include "base/output.h" +#include "expr/type.h" #include "parser/antlr_input.h" -#include "parser/input.h" +#include "parser/antlr_line_buffered_input.h" #include "parser/bounded_token_buffer.h" #include "parser/bounded_token_factory.h" -#include "parser/antlr_line_buffered_input.h" +#include "parser/cvc/cvc_input.h" +#include "parser/input.h" #include "parser/memory_mapped_input_buffer.h" -#include "parser/parser_exception.h" #include "parser/parser.h" - -#include "expr/command.h" -#include "expr/type.h" -#include "parser/cvc/cvc_input.h" +#include "parser/parser_exception.h" #include "parser/smt1/smt1_input.h" #include "parser/smt2/smt2_input.h" #include "parser/smt2/sygus_input.h" #include "parser/tptp/tptp_input.h" -#include "util/output.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 2086db714..baec46e6f 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -36,14 +36,14 @@ #include <vector> #include <cassert> +#include "base/output.h" #include "parser/bounded_token_buffer.h" -#include "parser/parser_exception.h" #include "parser/input.h" - +#include "parser/parser_exception.h" #include "util/bitvector.h" #include "util/integer.h" #include "util/rational.h" -#include "util/output.h" + namespace CVC4 { diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp index 33589110f..cc1d499fb 100644 --- a/src/parser/antlr_line_buffered_input.cpp +++ b/src/parser/antlr_line_buffered_input.cpp @@ -29,7 +29,7 @@ #include <string> #include <cassert> -#include "util/output.h" +#include "base/output.h" #include "parser/antlr_line_buffered_input.h" namespace CVC4 { diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h index a94cd4f2f..1709e99a2 100644 --- a/src/parser/antlr_tracing.h +++ b/src/parser/antlr_tracing.h @@ -23,7 +23,8 @@ #include <iostream> #include <string> -#include "util/output.h" + +#include "base/output.h" /* The ANTLR lexer generator, as of v3.2, puts Java trace commands * into our beautiful generated C lexer! How awful! This is clearly diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 0c356ca57..460b1ee03 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -476,10 +476,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { # define ANTLR3_INLINE_INPUT_8BIT #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ -#include "parser/antlr_tracing.h" -#include "util/integer.h" #include "parser/antlr_input.h" +#include "parser/antlr_tracing.h" #include "parser/parser.h" +#include "util/integer.h" }/* @lexer::includes */ @@ -487,10 +487,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { #include <stdint.h> #include <cassert> -#include "expr/command.h" +#include "parser/antlr_tracing.h" #include "parser/parser.h" +#include "smt_util/command.h" #include "util/subrange_bound.h" -#include "parser/antlr_tracing.h" namespace CVC4 { class Expr; @@ -541,16 +541,17 @@ namespace CVC4 { @parser::postinclude { +#include <sstream> +#include <string> +#include <vector> + +#include "base/output.h" #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" -#include "util/output.h" -#include <vector> -#include <string> -#include <sstream> #define REPEAT_COMMAND(k, CommandCtor) \ ({ \ diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 09f71800b..82b6dd32f 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -18,10 +18,11 @@ #include "parser/parser_exception.h" #include "parser/parser.h" -#include "expr/command.h" +#include "base/output.h" +#include "smt_util/command.h" #include "expr/type.h" #include "parser/antlr_input.h" -#include "util/output.h" + using namespace std; using namespace CVC4; diff --git a/src/parser/input.h b/src/parser/input.h index 312bc92f1..dcb54d256 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -20,14 +20,14 @@ #define __CVC4__PARSER__INPUT_H #include <iostream> -#include <string> #include <stdio.h> +#include <string> #include <vector> +#include "options/language.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "parser/parser_exception.h" -#include "util/language.h" namespace CVC4 { diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index 9dcab2085..7be1c9aba 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -28,8 +28,8 @@ #endif /* _WIN32 */ +#include "base/exception.h" #include "parser/memory_mapped_input_buffer.h" -#include "util/exception.h" namespace CVC4 { namespace parser { diff --git a/src/parser/options b/src/parser/options deleted file mode 100644 index 66e95889f..000000000 --- a/src/parser/options +++ /dev/null @@ -1,34 +0,0 @@ -# -# 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 - -option globalDeclarations global-declarations bool :default false - force all declarations and definitions to be global - -# this is to support security in the online version, and in other similar contexts -# (--no-include-file disables filesystem access in TPTP and SMT2 parsers) -# the name --no-include-file is legacy: it also now limits any filesystem access -# (read or write) for example by using --dump-to (or the equivalent set-option) or -# set-option :regular-output-channel/:diagnostic-output-channel. However, the main -# driver is still permitted to read the input file given on the command-line if any. -# creation/use of temp files are still permitted (but the paths aren't given by the -# user). Also note this is only safe for the version invoked through the main driver, -# there are ways via the API to get the CVC4 library to open a file for reading or -# writing and thus leak information from an existing file, or overwrite an existing -# file with malicious content. -undocumented-option filesystemAccess /--no-filesystem-access bool :default true -undocumented-alias --no-include-file = --no-filesystem-access - -endmodule diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index d17d5d141..0e8a9e241 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -14,24 +14,26 @@ ** Parser state implementation. **/ -#include <iostream> -#include <fstream> -#include <sstream> -#include <iterator> +#include "parser/parser.h" + #include <stdint.h> + #include <cassert> +#include <fstream> +#include <iostream> +#include <iterator> +#include <sstream> -#include "parser/input.h" -#include "parser/parser.h" -#include "parser/parser_exception.h" -#include "expr/command.h" +#include "base/output.h" #include "expr/expr.h" #include "expr/kind.h" +#include "expr/resource_manager.h" #include "expr/type.h" -#include "util/output.h" -#include "util/resource_manager.h" #include "options/options.h" -#include "smt/options.h" +#include "options/smt_options.h" +#include "parser/input.h" +#include "parser/parser_exception.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4::kind; diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index a2faec704..08e0232aa 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -13,20 +13,19 @@ ** ** A builder for parsers. **/ +#include "parser/parser_builder.h" #include <string> -#include "parser/parser_builder.h" +#include "expr/expr_manager.h" +#include "options/parser_options.h" +#include "options/smt_options.h" #include "parser/input.h" #include "parser/parser.h" #include "smt1/smt1.h" #include "smt2/smt2.h" #include "tptp/tptp.h" -#include "expr/expr_manager.h" -#include "parser/options.h" -#include "smt/options.h" - namespace CVC4 { namespace parser { @@ -168,7 +167,7 @@ ParserBuilder& ParserBuilder::withOptions(const Options& options) { .withParseOnly(options[options::parseOnly]) .withIncludeFile(options[options::filesystemAccess]); if(options.wasSetByUser(options::forceLogic)) { - retval = retval.withForcedLogic(options[options::forceLogic].getLogicString()); + retval = retval.withForcedLogic(options[options::forceLogic]->getLogicString()); } return retval; } diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 71810bf7c..fe652286b 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -21,10 +21,9 @@ #include <string> +#include "options/language.h" #include "parser/input.h" -#include "util/language.h" - namespace CVC4 { class ExprManager; diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 3b211371c..de47767c9 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -23,7 +23,7 @@ #include <string> #include <sstream> -#include "util/exception.h" +#include "base/exception.h" namespace CVC4 { namespace parser { diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index a885fe990..98825f1c3 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -63,7 +63,7 @@ options { #include <stdint.h> -#include "expr/command.h" +#include "smt_util/command.h" #include "parser/parser.h" #include "parser/antlr_tracing.h" @@ -101,6 +101,9 @@ namespace CVC4 { @parser::postinclude { +#include <vector> + +#include "base/output.h" #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" @@ -108,9 +111,7 @@ namespace CVC4 { #include "parser/parser.h" #include "parser/smt1/smt1.h" #include "util/integer.h" -#include "util/output.h" #include "util/rational.h" -#include <vector> using namespace CVC4; using namespace CVC4::parser; @@ -573,7 +574,7 @@ annotation[CVC4::Command*& smt_command] annotatedFormulas[pats,pat] '}' | attribute[key] ( userValue[value] - { smt_command = new SetInfoCommand(key.c_str() + 1, value); } + { smt_command = new SetInfoCommand(key.c_str() + 1, SExpr(value)); } | { smt_command = new EmptyCommand(std::string("annotation: ") + key); } ) ; diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index 8d827b17e..01bc8901e 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -18,7 +18,7 @@ namespace std { } #include "expr/type.h" -#include "expr/command.h" +#include "smt_util/command.h" #include "parser/parser.h" #include "parser/smt1/smt1.h" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d2409ba15..8ac1fa34c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -75,9 +75,9 @@ using namespace CVC4::parser; }/* @lexer::postinclude */ @parser::includes { -#include "expr/command.h" #include "parser/parser.h" #include "parser/antlr_tracing.h" +#include "smt_util/command.h" namespace CVC4 { class Expr; @@ -102,21 +102,22 @@ namespace CVC4 { @parser::postinclude { +#include <set> +#include <sstream> +#include <string> +#include <vector> + +#include "base/output.h" #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/smt2/smt2.h" +#include "util/floatingpoint.h" +#include "util/hash.h" #include "util/integer.h" -#include "util/output.h" #include "util/rational.h" -#include "util/hash.h" -#include "util/floatingpoint.h" -#include <vector> -#include <set> -#include <string> -#include <sstream> // \todo Review the need for this header #include "math.h" @@ -995,10 +996,7 @@ smt25Command[CVC4::Command*& cmd] /* echo */ | ECHO_TOK ( simpleSymbolicExpr[sexpr] - { std::stringstream ss; - ss << sexpr; - cmd = new EchoCommand(ss.str()); - } + { cmd = new EchoCommand(sexpr.toString()); } | { cmd = new EchoCommand(); } ) @@ -1446,12 +1444,12 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] | HEX_LITERAL { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); - sexpr = Integer(hexString, 16); + sexpr = SExpr(Integer(hexString, 16)); } | BINARY_LITERAL { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); - sexpr = Integer(binString, 2); + sexpr = SExpr(Integer(binString, 2)); } | str[s,false] { sexpr = SExpr(s); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index d3af9143a..355b58067 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -13,14 +13,14 @@ ** ** Definitions of SMT2 constants. **/ +#include "parser/smt2/smt2.h" + #include "expr/type.h" -#include "expr/command.h" +#include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/smt1/smt1.h" -#include "parser/smt2/smt2.h" -#include "parser/antlr_input.h" - +#include "smt_util/command.h" #include "util/bitvector.h" // ANTLR defines these, which is really bad! diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 62dcc70f5..a2bad4988 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -83,7 +83,7 @@ using namespace CVC4::parser; }/* @lexer::postinclude */ @parser::includes { -#include "expr/command.h" +#include "smt_util/command.h" #include "parser/parser.h" #include "parser/tptp/tptp.h" #include "parser/antlr_tracing.h" @@ -92,6 +92,11 @@ using namespace CVC4::parser; @parser::postinclude { +#include <algorithm> +#include <iterator> +#include <vector> + +#include "base/output.h" #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" @@ -99,11 +104,7 @@ using namespace CVC4::parser; #include "parser/parser.h" #include "parser/tptp/tptp.h" #include "util/integer.h" -#include "util/output.h" #include "util/rational.h" -#include <vector> -#include <iterator> -#include <algorithm> using namespace CVC4; using namespace CVC4::parser; @@ -203,7 +204,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] filename = filename.substr(0, filename.length() - 2); } CommandSequence* seq = new CommandSequence(); - seq->addCommand(new SetInfoCommand("name", filename)); + seq->addCommand(new SetInfoCommand("name", SExpr(filename))); if(PARSER_STATE->hasConjecture()) { seq->addCommand(new QueryCommand(MK_CONST(bool(false)))); } else { diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 2cd8f4339..4fdbc236d 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -19,13 +19,14 @@ #ifndef __CVC4__PARSER__TPTP_H #define __CVC4__PARSER__TPTP_H -#include "parser/parser.h" -#include "expr/command.h" -#include "util/hash.h" -#include <ext/hash_set> #include <cassert> -#include "parser/options.h" +#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" namespace CVC4 { |