From 2b7a6d2f2bcb26c0b5641bf7d0258c9fc9796c17 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Mon, 8 Feb 2010 18:46:32 +0000 Subject: [PATCH] Push/Pop parsing and commands --- src/expr/command.cpp | 22 +++++++++++++-- src/expr/command.h | 55 ++++++++++++++++++++++--------------- src/parser/cvc/cvc_parser.g | 2 ++ 3 files changed, 54 insertions(+), 25 deletions(-) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index a7b15f05e..01f7205b2 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -20,11 +20,11 @@ using namespace std; namespace CVC4 { -ostream& operator<<(ostream& out, const Command* c) { - if (c == NULL) { +ostream& operator<<(ostream& out, const Command* command) { + if (command == NULL) { out << "null"; } else { - c->toStream(out); + command->toStream(out); } return out; } @@ -71,4 +71,20 @@ void DeclarationCommand::toStream(std::ostream& out) const { out << ")"; } +void PushCommand::invoke(SmtEngine* smtEngine) { + smtEngine->push(); +} + +void PushCommand::toStream(ostream& out) const { + out << "Push()"; +} + +void PopCommand::invoke(SmtEngine* smtEngine) { + smtEngine->pop(); +} + +void PopCommand::toStream(ostream& out) const { + out << "Pop()"; +} + }/* CVC4 namespace */ diff --git a/src/expr/command.h b/src/expr/command.h index b6f1987a2..3c42c153c 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -47,7 +47,7 @@ public: class CVC4_PUBLIC EmptyCommand : public Command { public: EmptyCommand(std::string name = ""); - void invoke(CVC4::SmtEngine* smt_engine); + void invoke(CVC4::SmtEngine* smtEngine); void toStream(std::ostream& out) const; private: std::string d_name; @@ -56,12 +56,25 @@ private: class CVC4_PUBLIC AssertCommand : public Command { public: AssertCommand(const BoolExpr& e); - void invoke(CVC4::SmtEngine* smt_engine); + void invoke(CVC4::SmtEngine* smtEngine); void toStream(std::ostream& out) const; protected: BoolExpr d_expr; };/* class AssertCommand */ +class CVC4_PUBLIC PushCommand : public Command { +public: + void invoke(CVC4::SmtEngine* smtEngine); + void toStream(std::ostream& out) const; +};/* class PushCommand */ + +class CVC4_PUBLIC PopCommand : public Command { +public: + void invoke(CVC4::SmtEngine* smtEngine); + void toStream(std::ostream& out) const; +};/* class PopCommand */ + + class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { public: DeclarationCommand(const std::vector& ids, const Type* t); @@ -72,7 +85,7 @@ protected: class CVC4_PUBLIC CheckSatCommand : public Command { public: - CheckSatCommand(const BoolExpr& e); + CheckSatCommand(const BoolExpr& expr); void invoke(SmtEngine* smt); Result getResult(); void toStream(std::ostream& out) const; @@ -111,7 +124,7 @@ protected: };/* class SetBenchmarkStatusCommand */ inline std::ostream& operator<<(std::ostream& out, - SetBenchmarkStatusCommand::BenchmarkStatus bs) + SetBenchmarkStatusCommand::BenchmarkStatus status) CVC4_PUBLIC; class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { @@ -174,7 +187,7 @@ inline EmptyCommand::EmptyCommand(std::string name) : d_name(name) { } -inline void EmptyCommand::invoke(SmtEngine* smt_engine) { +inline void EmptyCommand::invoke(SmtEngine* smtEngine) { } inline void EmptyCommand::toStream(std::ostream& out) const { @@ -187,8 +200,8 @@ inline AssertCommand::AssertCommand(const BoolExpr& e) : d_expr(e) { } -inline void AssertCommand::invoke(SmtEngine* smt_engine) { - smt_engine->assertFormula(d_expr); +inline void AssertCommand::invoke(SmtEngine* smtEngine) { + smtEngine->assertFormula(d_expr); } inline void AssertCommand::toStream(std::ostream& out) const { @@ -197,12 +210,12 @@ inline void AssertCommand::toStream(std::ostream& out) const { /* class CheckSatCommand */ -inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) : - d_expr(e) { +inline CheckSatCommand::CheckSatCommand(const BoolExpr& expr) : + d_expr(expr) { } -inline void CheckSatCommand::invoke(SmtEngine* smt_engine) { - d_result = smt_engine->checkSat(d_expr); +inline void CheckSatCommand::invoke(SmtEngine* smtEngine) { + d_result = smtEngine->checkSat(d_expr); } inline Result CheckSatCommand::getResult() { @@ -215,8 +228,8 @@ inline QueryCommand::QueryCommand(const BoolExpr& e) : d_expr(e) { } -inline void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) { - d_result = smt_engine->query(d_expr); +inline void QueryCommand::invoke(CVC4::SmtEngine* smtEngine) { + d_result = smtEngine->query(d_expr); } inline Result QueryCommand::getResult() { @@ -241,16 +254,14 @@ inline void CommandSequence::addCommand(Command* cmd) { /* class DeclarationCommand */ -inline -DeclarationCommand::DeclarationCommand(const std::vector& ids, - const Type* t) : +inline DeclarationCommand::DeclarationCommand(const std::vector& ids, const Type* t) : d_declaredSymbols(ids) { } /* class SetBenchmarkStatusCommand */ -inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus s) : - d_status(s) { +inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : + d_status(status) { } inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) { @@ -263,8 +274,8 @@ inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const { /* class SetBenchmarkLogicCommand */ -inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string l) : - d_logic(l) { +inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) : + d_logic(logic) { } inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) { @@ -277,8 +288,8 @@ inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { /* output stream insertion operator for benchmark statuses */ inline std::ostream& operator<<(std::ostream& out, - SetBenchmarkStatusCommand::BenchmarkStatus bs) { - switch(bs) { + SetBenchmarkStatusCommand::BenchmarkStatus status) { + switch(status) { case SetBenchmarkStatusCommand::SMT_SATISFIABLE: return out << "sat"; diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 30df2d439..7f4ce3c26 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -76,6 +76,8 @@ command returns [CVC4::Command* cmd = 0] | QUERY f = formula SEMICOLON { cmd = new QueryCommand(f); } | CHECKSAT f = formula SEMICOLON { cmd = new CheckSatCommand(f); } | CHECKSAT SEMICOLON { cmd = new CheckSatCommand(getTrueExpr()); } + | PUSH SEMICOLON { cmd = new PushCommand(); } + | POP SEMICOLON { cmd = new PopCommand(); } | cmd = declaration | EOF ; -- 2.30.2