From dff2298c59f3550b1c3873b0d9fe9691f6f658d4 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sat, 28 Nov 2009 02:59:11 +0000 Subject: [PATCH] Added an EmptyCommand and a CommandSequence commands and changed the parser a bit. --- src/parser/parser_state.cpp | 10 ++++---- src/parser/parser_state.h | 37 +++++++++++------------------ src/parser/smtlib.ypp | 40 ++++++++++++++++--------------- src/parser/smtlib_scanner.lpp | 4 ++-- src/util/command.cpp | 44 ++++++++++++++++++++++++++++++----- src/util/command.h | 25 ++++++++++++++++++-- 6 files changed, 101 insertions(+), 59 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& 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 #include -#include +#include "cvc4.h" namespace CVC4 { -class Expr; -class ExprManager; - namespace parser { @@ -79,17 +76,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& commands_vector); - - /** - * Adds the commands in the given vector. - */ - void addCommands(std::vector& commands_vector); - /** * Makes room for a new string literal (empties the buffer). */ @@ -117,11 +103,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. */ @@ -145,7 +126,7 @@ class ParserState /** * Creates a new expression, given the kind and the children */ - CVC4::Expr* newExpression(CVC4::Kind kind, std::vector& children); + CVC4::Expr* newExpression(CVC4::Kind kind, std::vector& 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 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 *p_string_vector; + std::vector *p_string_vector; CVC4::Expr *p_expression; - std::vector *p_expression_vector; + std::vector *p_expression_vector; CVC4::Command *p_command; - std::vector *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 NUMERAL_TOK %token SYM_TOK %token STRING_TOK @@ -104,29 +101,34 @@ int smtliberror(const char *s) { return _global_parser_state->parseError(s); } %type an_formula an_atom prop_atom %type an_formulas; %type connective; +%type bench_attribute +%type 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; $$->push_back($1); delete $1; } - | an_formulas an_formula { $$ = $1; $$->push_back($2); delete $2; } + an_formula { $$ = new vector; $$->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 #include "parser_state.h" diff --git a/src/util/command.cpp b/src/util/command.cpp index b728a2228..35db79a0d 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -9,12 +9,14 @@ using namespace CVC4; +void EmptyCommand::invoke(SmtEngine* smt_engine) { } + AssertCommand::AssertCommand(const Expr& e) : d_expr(e) { } -void AssertCommand::invoke(CVC4::SmtEngine* smt_engine) +void AssertCommand::invoke(SmtEngine* smt_engine) { smt_engine->assert(d_expr); } @@ -23,18 +25,18 @@ CheckSatCommand::CheckSatCommand() { } -CheckSatCommand::CheckSatCommand(const Expr& e): - d_expr(e) +CheckSatCommand::CheckSatCommand(const Expr& e) : + d_expr(e) { } -void CheckSatCommand::invoke(CVC4::SmtEngine* smt_engine) +void CheckSatCommand::invoke(SmtEngine* smt_engine) { smt_engine->checkSat(d_expr); } -QueryCommand::QueryCommand(const Expr& e): - d_expr(e) +QueryCommand::QueryCommand(const Expr& e) : + d_expr(e) { } @@ -43,3 +45,33 @@ void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) smt_engine->query(d_expr); } +CommandSequence::CommandSequence() : + d_last_index(0) +{ +} + +CommandSequence::CommandSequence(Command* cmd) : + d_last_index(0) +{ + addCommand(cmd); +} + + +CommandSequence::~CommandSequence() +{ + for (unsigned i = d_last_index; i < d_command_sequence.size(); i++) + delete d_command_sequence[i]; +} + +void CommandSequence::invoke(SmtEngine* smt_engine) +{ + for (; d_last_index < d_command_sequence.size(); d_last_index++) { + d_command_sequence[d_last_index]->invoke(smt_engine); + delete d_command_sequence[d_last_index]; + } +} + +void CommandSequence::addCommand(Command* cmd) +{ + d_command_sequence.push_back(cmd); +} diff --git a/src/util/command.h b/src/util/command.h index 745f6f5e2..c6778f34a 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -12,7 +12,7 @@ #ifndef __CVC4__COMMAND_H #define __CVC4__COMMAND_H -#include "expr/expr.h" +#include "cvc4.h" namespace CVC4 { @@ -23,7 +23,13 @@ class Command { public: virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; - virtual ~Command() {} + virtual ~Command() {}; +}; + +class EmptyCommand : public Command +{ + public: + virtual void invoke(CVC4::SmtEngine* smt_engine); }; class AssertCommand: public Command @@ -54,6 +60,21 @@ class QueryCommand: public Command Expr d_expr; }; +class CommandSequence: public Command +{ + public: + CommandSequence(); + CommandSequence(Command* cmd); + ~CommandSequence(); + void invoke(CVC4::SmtEngine* smt); + void addCommand(Command* cmd); + private: + /** All the commands to be executed (in sequence) */ + std::vector d_command_sequence; + /** Next command to be executed */ + unsigned int d_last_index; +}; + }/* CVC4 namespace */ #endif /* __CVC4__COMMAND_H */ -- 2.30.2