void ParserState::increaseLineNumber()
{
++d_input_line;
+ if (d_interactive) {
+ std::cout << getCurrentPrompt();
+ setPromptNextLine();
+ }
}
int ParserState::getLineNumber() 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
#include <vector>
#include <iostream>
-#include <util/command.h>
+#include "cvc4.h"
namespace CVC4
{
-class Expr;
-class ExprManager;
-
namespace parser
{
*/
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).
*/
*/
std::string getBenchmarkName() const;
- /**
- * Add the command to the list of commands.
- */
- void addCommand(const Command* cmd);
-
/**
* Set the status of the parsed benchmark.
*/
/**
* 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.
*/
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 */
/** 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 */
** 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 {
%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;
};
-%start benchmark
-
%token <p_string> NUMERAL_TOK
%token <p_string> SYM_TOK
%token <p_string> STRING_TOK
%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;
;
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:
%option noyymore
%option yylineno
%option prefix="smtlib"
-
-%{
+
+%{
#include <iostream>
#include "parser_state.h"
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);
}
{
}
-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)
{
}
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);
+}
#ifndef __CVC4__COMMAND_H
#define __CVC4__COMMAND_H
-#include "expr/expr.h"
+#include "cvc4.h"
namespace CVC4
{
{
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
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<Command*> d_command_sequence;
+ /** Next command to be executed */
+ unsigned int d_last_index;
+};
+
}/* CVC4 namespace */
#endif /* __CVC4__COMMAND_H */
projects / cvc5.git / commitdiff