diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
commit | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (patch) | |
tree | 8db12e260b24978bbbed3363846f6daf7c0da04f /src/expr/command.h | |
parent | 5e2f381b26d683691d9a040589536dc39c5831e0 (diff) |
parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
Diffstat (limited to 'src/expr/command.h')
-rw-r--r-- | src/expr/command.h | 334 |
1 files changed, 126 insertions, 208 deletions
diff --git a/src/expr/command.h b/src/expr/command.h index 388ad62e6..0c78dd1c6 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -39,7 +39,7 @@ namespace CVC4 { class SmtEngine; class Command; -inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; /** The status an SMT benchmark can have */ @@ -52,115 +52,203 @@ enum BenchmarkStatus { SMT_UNKNOWN }; -inline std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) - CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, + BenchmarkStatus status) CVC4_PUBLIC; class CVC4_PUBLIC Command { public: - virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; + virtual void invoke(SmtEngine* smtEngine) = 0; + virtual void invoke(SmtEngine* smtEngine, std::ostream& out); virtual ~Command() {}; virtual void toStream(std::ostream&) const = 0; std::string toString() const; + virtual void printResult(std::ostream& out) const; };/* class Command */ +/** + * EmptyCommands (and its subclasses) are the residue of a command + * after the parser handles them (and there's nothing left to do). + */ class CVC4_PUBLIC EmptyCommand : public Command { +protected: + std::string d_name; public: EmptyCommand(std::string name = ""); - void invoke(CVC4::SmtEngine* smtEngine); + void invoke(SmtEngine* smtEngine); void toStream(std::ostream& out) const; -private: - std::string d_name; };/* class EmptyCommand */ class CVC4_PUBLIC AssertCommand : public Command { +protected: + BoolExpr d_expr; public: AssertCommand(const BoolExpr& e); - void invoke(CVC4::SmtEngine* smtEngine); + void invoke(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 invoke(SmtEngine* smtEngine); void toStream(std::ostream& out) const; };/* class PushCommand */ class CVC4_PUBLIC PopCommand : public Command { public: - void invoke(CVC4::SmtEngine* smtEngine); + void invoke(SmtEngine* smtEngine); void toStream(std::ostream& out) const; };/* class PopCommand */ - class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { -public: - DeclarationCommand(const std::string& id, const Type& t); - DeclarationCommand(const std::vector<std::string>& ids, const Type& t); - void toStream(std::ostream& out) const; protected: std::vector<std::string> d_declaredSymbols; Type d_type; -}; +public: + DeclarationCommand(const std::string& id, Type t); + DeclarationCommand(const std::vector<std::string>& ids, Type t); + void toStream(std::ostream& out) const; +};/* class DeclarationCommand */ -class CVC4_PUBLIC CheckSatCommand : public Command { +class CVC4_PUBLIC DefineFunctionCommand : public Command { +protected: + std::string d_name; + std::vector<std::pair<std::string, Type> > d_args; + Type d_type; + Expr d_formula; public: - CheckSatCommand(const BoolExpr& expr); - void invoke(SmtEngine* smt); - Result getResult(); + DefineFunctionCommand(const std::string& name, + const std::vector<std::pair<std::string, Type> >& args, + Type type, Expr formula); + void invoke(SmtEngine* smtEngine); void toStream(std::ostream& out) const; +};/* class DefineFunctionCommand */ + +class CVC4_PUBLIC CheckSatCommand : public Command { protected: BoolExpr d_expr; Result d_result; +public: + CheckSatCommand(const BoolExpr& expr); + void invoke(SmtEngine* smtEngine); + Result getResult() const; + void printResult(std::ostream& out) const; + void toStream(std::ostream& out) const; };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { -public: - QueryCommand(const BoolExpr& e); - void invoke(SmtEngine* smt); - Result getResult(); - void toStream(std::ostream& out) const; protected: BoolExpr d_expr; Result d_result; +public: + QueryCommand(const BoolExpr& e); + void invoke(SmtEngine* smtEngine); + Result getResult() const; + void printResult(std::ostream& out) const; + void toStream(std::ostream& out) const; };/* class QueryCommand */ -class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { +class CVC4_PUBLIC GetValueCommand : public Command { +protected: + Expr d_term; + Expr d_result; public: - SetBenchmarkStatusCommand(BenchmarkStatus status); - void invoke(SmtEngine* smt); + GetValueCommand(Expr term); + void invoke(SmtEngine* smtEngine); + Expr getResult() const; + void printResult(std::ostream& out) const; + void toStream(std::ostream& out) const; +};/* class GetValueCommand */ + +class CVC4_PUBLIC GetAssertionsCommand : public Command { +protected: + std::string d_result; +public: + GetAssertionsCommand(); + void invoke(SmtEngine* smtEngine); + std::string getResult() const; + void printResult(std::ostream& out) const; void toStream(std::ostream& out) const; +};/* class GetAssertionsCommand */ + +class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { protected: BenchmarkStatus d_status; +public: + SetBenchmarkStatusCommand(BenchmarkStatus status); + void invoke(SmtEngine* smtEngine); + void toStream(std::ostream& out) const; };/* class SetBenchmarkStatusCommand */ - class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { +protected: + std::string d_logic; public: SetBenchmarkLogicCommand(std::string logic); - void invoke(SmtEngine* smt); + void invoke(SmtEngine* smtEngine); void toStream(std::ostream& out) const; -protected: - std::string d_logic; };/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC SetInfoCommand : public Command { +protected: + std::string d_flag; + SExpr d_sexpr; + std::string d_result; public: SetInfoCommand(std::string flag, SExpr& sexpr); - void invoke(SmtEngine* smt); + void invoke(SmtEngine* smtEngine); void toStream(std::ostream& out) const; + std::string getResult() const; + void printResult(std::ostream& out) const; +};/* class SetInfoCommand */ + +class CVC4_PUBLIC GetInfoCommand : public Command { +protected: + std::string d_flag; + std::string d_result; +public: + GetInfoCommand(std::string flag); + void invoke(SmtEngine* smtEngine); + void toStream(std::ostream& out) const; + std::string getResult() const; + void printResult(std::ostream& out) const; +};/* class GetInfoCommand */ + +class CVC4_PUBLIC SetOptionCommand : public Command { protected: std::string d_flag; SExpr d_sexpr; -};/* class SetInfoCommand */ + std::string d_result; +public: + SetOptionCommand(std::string flag, SExpr& sexpr); + void invoke(SmtEngine* smtEngine); + void toStream(std::ostream& out) const; + std::string getResult() const; + void printResult(std::ostream& out) const; +};/* class SetOptionCommand */ + +class CVC4_PUBLIC GetOptionCommand : public Command { +protected: + std::string d_flag; + std::string d_result; +public: + GetOptionCommand(std::string flag); + void invoke(SmtEngine* smtEngine); + void toStream(std::ostream& out) const; + std::string getResult() const; + void printResult(std::ostream& out) const; +};/* class GetOptionCommand */ class CVC4_PUBLIC CommandSequence : public Command { +private: + /** All the commands to be executed (in sequence) */ + std::vector<Command*> d_commandSequence; + /** Next command to be executed */ + unsigned int d_index; public: CommandSequence(); ~CommandSequence(); - void invoke(SmtEngine* smt); + void invoke(SmtEngine* smtEngine); + void invoke(SmtEngine* smtEngine, std::ostream& out); void addCommand(Command* cmd); void toStream(std::ostream& out) const; @@ -172,178 +260,8 @@ public: iterator begin() { return d_commandSequence.begin(); } iterator end() { return d_commandSequence.end(); } - -private: - /** All the commands to be executed (in sequence) */ - std::vector<Command*> d_commandSequence; - /** Next command to be executed */ - unsigned int d_index; };/* class CommandSequence */ }/* CVC4 namespace */ -/* =========== inline function definitions =========== */ - -#include "smt/smt_engine.h" - -namespace CVC4 { - -inline std::ostream& operator<<(std::ostream& out, const Command& c) { - c.toStream(out); - return out; -} - -/* class Command */ - -inline std::string Command::toString() const { - std::stringstream ss; - toStream(ss); - return ss.str(); -} - -/* class EmptyCommand */ - -inline EmptyCommand::EmptyCommand(std::string name) : - d_name(name) { -} - -inline void EmptyCommand::invoke(SmtEngine* smtEngine) { -} - -inline void EmptyCommand::toStream(std::ostream& out) const { - out << "EmptyCommand(" << d_name << ")"; -} - -/* class AssertCommand */ - -inline AssertCommand::AssertCommand(const BoolExpr& e) : - d_expr(e) { -} - -inline void AssertCommand::invoke(SmtEngine* smtEngine) { - smtEngine->assertFormula(d_expr); -} - -inline void AssertCommand::toStream(std::ostream& out) const { - out << "Assert(" << d_expr << ")"; -} - -/* class CheckSatCommand */ - -inline CheckSatCommand::CheckSatCommand(const BoolExpr& expr) : - d_expr(expr) { -} - -inline void CheckSatCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->checkSat(d_expr); -} - -inline Result CheckSatCommand::getResult() { - return d_result; -} - -/* class QueryCommand */ - -inline QueryCommand::QueryCommand(const BoolExpr& e) : - d_expr(e) { -} - -inline void QueryCommand::invoke(CVC4::SmtEngine* smtEngine) { - d_result = smtEngine->query(d_expr); -} - -inline Result QueryCommand::getResult() { - return d_result; -} - -inline void QueryCommand::toStream(std::ostream& out) const { - out << "Query("; - d_expr.printAst(out, 0); - out << ")"; -} - -/* class CommandSequence */ - -inline CommandSequence::CommandSequence() : - d_index(0) { -} - -inline void CommandSequence::addCommand(Command* cmd) { - d_commandSequence.push_back(cmd); -} - -/* class DeclarationCommand */ - -inline DeclarationCommand::DeclarationCommand(const std::string& id, const Type& t) : - d_type(t) -{ - d_declaredSymbols.push_back(id); -} - -inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, const Type& t) : - d_declaredSymbols(ids), - d_type(t) -{ -} - -/* class SetBenchmarkStatusCommand */ - -inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : - d_status(status) { -} - -inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) { - // FIXME: TODO: something to be done with the status -} - -inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const { - out << "SetBenchmarkStatus(" << d_status << ")"; -} - -/* class SetBenchmarkLogicCommand */ - -inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) : - d_logic(logic) { -} - -inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) { - // FIXME: TODO: something to be done with the logic -} - -inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { - out << "SetBenchmarkLogic(" << d_logic << ")"; -} - -inline SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) : - d_flag(flag), - d_sexpr(sexpr) { -} - -inline void SetInfoCommand::invoke(SmtEngine* smt) { } - -inline void SetInfoCommand::toStream(std::ostream& out) const { - out << "SetInfo(" << d_flag << ", " << d_sexpr << ")"; -} - -/* output stream insertion operator for benchmark statuses */ -inline std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) { - switch(status) { - - case SMT_SATISFIABLE: - return out << "sat"; - - case SMT_UNSATISFIABLE: - return out << "unsat"; - - case SMT_UNKNOWN: - return out << "unknown"; - - default: - return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]"; - } -} - -}/* CVC4 namespace */ - #endif /* __CVC4__COMMAND_H */ |