diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser_state.cpp | 10 | ||||
-rw-r--r-- | src/parser/parser_state.h | 37 | ||||
-rw-r--r-- | src/parser/smtlib.ypp | 40 | ||||
-rw-r--r-- | src/parser/smtlib_scanner.lpp | 4 |
4 files changed, 40 insertions, 51 deletions
diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp index 74def84cb..25f1cfd78 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser_state.cpp @@ -62,6 +62,10 @@ void ParserState::setPromptNextLine() void ParserState::increaseLineNumber() { ++d_input_line; + if (d_interactive) { + std::cout << getCurrentPrompt(); + setPromptNextLine(); + } } int ParserState::getLineNumber() const @@ -74,12 +78,6 @@ std::string ParserState::getFileName() const return d_file_name; } -void ParserState::getParsedCommands(vector<Command*>& commands_vector) -{ - d_commands.swap(commands_vector); - d_commands.clear(); -} - } // End namespace parser } // End namespace CVC3 diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index fbb0afe70..8b18ff22f 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -19,14 +19,11 @@ #include <vector> #include <iostream> -#include <util/command.h> +#include "cvc4.h" namespace CVC4 { -class Expr; -class ExprManager; - namespace parser { @@ -80,17 +77,6 @@ class ParserState int read(char* buffer, int size); /** - * Returns the vector of parsed commands in the given vector (and forgets - * about them in the local state. - */ - void getParsedCommands(std::vector<CVC4::Command*>& commands_vector); - - /** - * Adds the commands in the given vector. - */ - void addCommands(std::vector<CVC4::Command*>& commands_vector); - - /** * Makes room for a new string literal (empties the buffer). */ void newStringLiteral(); @@ -118,11 +104,6 @@ class ParserState std::string getBenchmarkName() const; /** - * Add the command to the list of commands. - */ - void addCommand(const Command* cmd); - - /** * Set the status of the parsed benchmark. */ void setBenchmarkStatus(BenchmarkStatus status); @@ -145,7 +126,7 @@ class ParserState /** * Creates a new expression, given the kind and the children */ - CVC4::Expr* newExpression(CVC4::Kind kind, std::vector<CVC4::Expr*>& children); + CVC4::Expr* newExpression(CVC4::Kind kind, std::vector<CVC4::Expr>& children); /** * Returns a new TRUE Boolean constant. @@ -162,6 +143,17 @@ class ParserState */ CVC4::Expr* getNewVariableByName(const std::string var_name) const; + /** + * Sets the command that is the result of the parser. + */ + void setCommand(CVC4::Command* cmd); + + /** + * Sets the interactive flag on/off. If on, every time we go to a new line + * (via increaseLineNumber()) the prompt will be printed to stdout. + */ + void setInteractive(bool interactive = true); + private: /** Counter for uniqueID of bound variables */ @@ -190,9 +182,6 @@ class ParserState /** The name of the benchmark if any */ std::string d_benchmark_name; - - /** The vector of parsed commands if parsed as a whole */ - std::vector<CVC4::Command*> d_commands; }; }/* CVC4::parser namespace */ diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index 8e6d99f6e..b1aeaa570 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -11,9 +11,8 @@ ** commands in SMT-LIB language. **/ -#include "cvc4_expr.h" -#include "parser/parser_state.h" -#include "util/command.h" +#include "cvc4.h" +#include "parser_state.h" // Exported shared data namespace CVC4 { @@ -43,13 +42,13 @@ int smtliberror(const char *s) { return _global_parser_state->parseError(s); } %union { std::string *p_string; - std::vector<std::string*> *p_string_vector; + std::vector<std::string> *p_string_vector; CVC4::Expr *p_expression; - std::vector<CVC4::Expr*> *p_expression_vector; + std::vector<CVC4::Expr> *p_expression_vector; CVC4::Command *p_command; - std::vector<CVC4::Command*> *p_command_vector; + CVC4::CommandSequence *p_command_sequence; CVC4::parser::ParserState::BenchmarkStatus d_bench_status; @@ -57,8 +56,6 @@ int smtliberror(const char *s) { return _global_parser_state->parseError(s); } }; -%start benchmark - %token <p_string> NUMERAL_TOK %token <p_string> SYM_TOK %token <p_string> STRING_TOK @@ -104,29 +101,34 @@ int smtliberror(const char *s) { return _global_parser_state->parseError(s); } %type <p_expression> an_formula an_atom prop_atom %type <p_expression_vector> an_formulas; %type <d_kind> connective; +%type <p_command> bench_attribute +%type <p_command_sequence> bench_attributes +%start benchmark + %% benchmark: LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK { _global_parser_state->setBenchmarkName(*$3); + _global_parser_state->setCommand($4); } - | EOF_TOK + | EOF_TOK { _global_parser_state->setCommand(new EmptyCommand()); } ; bench_name: SYM_TOK; bench_attributes: - bench_attribute - | bench_attributes bench_attribute + bench_attribute { $$ = new CommandSequence($1); } + | bench_attributes bench_attribute { $$ = $1; $$->addCommand($2); } ; - + bench_attribute: - | COLON_TOK FORMULA_TOK an_formula { _global_parser_state->addCommand(new CheckSatCommand(*$3)); delete $3; } - | COLON_TOK STATUS_TOK status { _global_parser_state->setBenchmarkStatus($3); } - | COLON_TOK LOGIC_TOK logic_name { _global_parser_state->setBenchmarkLogic(*$3); delete $3; } - | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK - | annotation + COLON_TOK FORMULA_TOK an_formula { $$ = new CheckSatCommand(*$3); delete $3; } + | COLON_TOK STATUS_TOK status { $$ = new EmptyCommand(); _global_parser_state->setBenchmarkStatus($3); } + | COLON_TOK LOGIC_TOK logic_name { $$ = new EmptyCommand(); _global_parser_state->setBenchmarkLogic(*$3); delete $3; } + | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK { $$ = new EmptyCommand(); } + | annotation { $$ = new EmptyCommand(); } ; logic_name: SYM_TOK; @@ -152,8 +154,8 @@ pred_sig: ; an_formulas: - an_formula { $$ = new vector<Expr*>; $$->push_back($1); delete $1; } - | an_formulas an_formula { $$ = $1; $$->push_back($2); delete $2; } + an_formula { $$ = new vector<Expr>; $$->push_back(*$1); delete $1; } + | an_formulas an_formula { $$ = $1; $$->push_back(*$2); delete $2; } ; an_formula: diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp index 4d9cb8213..70026bd4c 100644 --- a/src/parser/smtlib_scanner.lpp +++ b/src/parser/smtlib_scanner.lpp @@ -17,8 +17,8 @@ %option noyymore %option yylineno %option prefix="smtlib" - -%{ + +%{ #include <iostream> #include "parser_state.h" |