From 64d530e5b9096e66398f92d93cf7bc4268df0e70 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 3 Feb 2010 22:20:25 +0000 Subject: Addressed many of the concerns of bug 10 (build system code review). Some parts split into other bugs: 19, 20, 21. Addressed concerns of bug 11 (util package code review). Slight parser source file modifications: file comments, #included headers in generated parsers/lexers Added CVC4::Result propagation back through MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when verbosity is not requested. --- src/util/command.h | 198 ++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 181 insertions(+), 17 deletions(-) (limited to 'src/util/command.h') diff --git a/src/util/command.h b/src/util/command.h index 57edfea01..15104a5ea 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -10,26 +10,30 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Implementation of the command pattern on SmtEngines. Generated by - ** the parser. + ** Implementation of the command pattern on SmtEngines. Command + ** objects are generated by the parser (typically) to implement the + ** commands in parsed input (see Parser::parseNextCommand()), or by + ** client code. **/ #ifndef __CVC4__COMMAND_H #define __CVC4__COMMAND_H #include +#include +#include +#include #include "cvc4_config.h" #include "expr/expr.h" +#include "util/result.h" namespace CVC4 { - class SmtEngine; - class Command; -}/* CVC4 namespace */ -namespace CVC4 { +class SmtEngine; +class Command; -std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; class CVC4_PUBLIC Command { @@ -49,7 +53,6 @@ private: std::string d_name; };/* class EmptyCommand */ - class CVC4_PUBLIC AssertCommand : public Command { public: AssertCommand(const BoolExpr& e); @@ -59,7 +62,6 @@ protected: BoolExpr d_expr; };/* class AssertCommand */ - class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { public: DeclarationCommand(const std::vector& ids); @@ -73,22 +75,24 @@ public: CheckSatCommand(); CheckSatCommand(const BoolExpr& e); void invoke(SmtEngine* smt); + Result getResult(); void toStream(std::ostream& out) const; protected: BoolExpr d_expr; + Result d_result; };/* 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; };/* class QueryCommand */ - class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { public: /** The status an SMT benchmark can have */ @@ -105,7 +109,11 @@ public: void toStream(std::ostream& out) const; protected: BenchmarkStatus d_status; -};/* class QueryCommand */ +};/* class SetBenchmarkStatusCommand */ + +inline std::ostream& operator<<(std::ostream& out, + SetBenchmarkStatusCommand::BenchmarkStatus bs) + CVC4_PUBLIC; class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { public: @@ -114,9 +122,7 @@ public: void toStream(std::ostream& out) const; protected: std::string d_logic; -};/* class QueryCommand */ - - +};/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC CommandSequence : public Command { public: @@ -125,13 +131,171 @@ public: void invoke(SmtEngine* smt); void addCommand(Command* cmd); void toStream(std::ostream& out) const; + + typedef std::vector::iterator iterator; + typedef std::vector::const_iterator const_iterator; + + const_iterator begin() const { return d_commandSequence.begin(); } + const_iterator end() const { return d_commandSequence.end(); } + + iterator begin() { return d_commandSequence.begin(); } + iterator end() { return d_commandSequence.end(); } + private: /** All the commands to be executed (in sequence) */ - std::vector d_command_sequence; + std::vector d_commandSequence; /** Next command to be executed */ - unsigned int d_last_index; + 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* smt_engine) { +} + +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* smt_engine) { + smt_engine->assertFormula(d_expr); +} + +inline void AssertCommand::toStream(std::ostream& out) const { + out << "Assert(" << d_expr << ")"; +} + +/* class CheckSatCommand */ + +inline CheckSatCommand::CheckSatCommand() { +} + +inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) : + d_expr(e) { +} + +inline void CheckSatCommand::invoke(SmtEngine* smt_engine) { + d_result = smt_engine->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* smt_engine) { + d_result = smt_engine->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::vector& ids) : + d_declaredSymbols(ids) { +} + +/* class SetBenchmarkStatusCommand */ + +inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus s) : + d_status(s) { +} + +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 l) : + d_logic(l) { +} + +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 << ")"; +} + +/* output stream insertion operator for benchmark statuses */ +inline std::ostream& operator<<(std::ostream& out, + SetBenchmarkStatusCommand::BenchmarkStatus bs) { + switch(bs) { + + case SetBenchmarkStatusCommand::SMT_SATISFIABLE: + return out << "sat"; + + case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE: + return out << "unsat"; + + case SetBenchmarkStatusCommand::SMT_UNKNOWN: + return out << "unknown"; + + default: + return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]"; + } +} + +}/* CVC4 namespace */ + #endif /* __CVC4__COMMAND_H */ -- cgit v1.2.3