diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-04 03:31:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-04 03:31:38 +0000 |
commit | fc14c009e8e9d2274368b54c12f3580a9ec8f718 (patch) | |
tree | 853fdc64b8f6f29dc106e581dfe8ed8e4c569778 /src/expr/command.h | |
parent | 33988bd64b92960f7bed5c68d1266adc4183454b (diff) |
src/expr/kind.h is now automatically generated.
Build src/expr before src/util.
Moved CVC4::Command to the expr package.
Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).
Added file-level documentation to Antlr sources
When built for debug, spin on SEGV instead of aborting. Really useful
for debugging problems that crop up only on long runs. Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.
Updated src/main/about.h for 2010.
Diffstat (limited to 'src/expr/command.h')
-rw-r--r-- | src/expr/command.h | 297 |
1 files changed, 297 insertions, 0 deletions
diff --git a/src/expr/command.h b/src/expr/command.h new file mode 100644 index 000000000..dedefb782 --- /dev/null +++ b/src/expr/command.h @@ -0,0 +1,297 @@ +/********************* -*- C++ -*- */ +/** command.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** 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 <iostream> +#include <sstream> +#include <string> +#include <vector> + +#include "cvc4_config.h" +#include "expr/expr.h" +#include "util/result.h" + +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; + +class CVC4_PUBLIC Command { +public: + virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; + virtual ~Command() {}; + virtual void toStream(std::ostream&) const = 0; + std::string toString() const; +};/* class Command */ + +class CVC4_PUBLIC EmptyCommand : public Command { +public: + EmptyCommand(std::string name = ""); + void invoke(CVC4::SmtEngine* smt_engine); + void toStream(std::ostream& out) const; +private: + std::string d_name; +};/* class EmptyCommand */ + +class CVC4_PUBLIC AssertCommand : public Command { +public: + AssertCommand(const BoolExpr& e); + void invoke(CVC4::SmtEngine* smt_engine); + void toStream(std::ostream& out) const; +protected: + BoolExpr d_expr; +};/* class AssertCommand */ + +class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { +public: + DeclarationCommand(const std::vector<std::string>& ids); + void toStream(std::ostream& out) const; +protected: + std::vector<std::string> d_declaredSymbols; +}; + +class CVC4_PUBLIC CheckSatCommand : public Command { +public: + 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 */ + enum BenchmarkStatus { + /** Benchmark is satisfiable */ + SMT_SATISFIABLE, + /** Benchmark is unsatisfiable */ + SMT_UNSATISFIABLE, + /** The status of the benchmark is unknown */ + SMT_UNKNOWN + }; + SetBenchmarkStatusCommand(BenchmarkStatus status); + void invoke(SmtEngine* smt); + void toStream(std::ostream& out) const; +protected: + BenchmarkStatus d_status; +};/* class SetBenchmarkStatusCommand */ + +inline std::ostream& operator<<(std::ostream& out, + SetBenchmarkStatusCommand::BenchmarkStatus bs) + CVC4_PUBLIC; + +class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { +public: + SetBenchmarkLogicCommand(std::string logic); + void invoke(SmtEngine* smt); + void toStream(std::ostream& out) const; +protected: + std::string d_logic; +};/* class SetBenchmarkLogicCommand */ + +class CVC4_PUBLIC CommandSequence : public Command { +public: + CommandSequence(); + ~CommandSequence(); + void invoke(SmtEngine* smt); + void addCommand(Command* cmd); + void toStream(std::ostream& out) const; + + typedef std::vector<Command*>::iterator iterator; + typedef std::vector<Command*>::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<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* 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(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<std::string>& 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 */ |