diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-30 20:22:33 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-30 20:22:33 +0000 |
commit | 8730e9320a833a9eb0e65074f9988950b7424c0c (patch) | |
tree | 1cb09404256743e208fece079ba473595e05edcd /src/expr/command.h | |
parent | 8c87c05ac56a5f29b2ae1e658f2d7d3b7b588163 (diff) |
Merging from branches/antlr3 (r246:354)
Diffstat (limited to 'src/expr/command.h')
-rw-r--r-- | src/expr/command.h | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/src/expr/command.h b/src/expr/command.h index 3c42c153c..e5994b3c7 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -36,6 +36,20 @@ class Command; inline 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 */ +enum BenchmarkStatus { + /** Benchmark is satisfiable */ + SMT_SATISFIABLE, + /** Benchmark is unsatisfiable */ + SMT_UNSATISFIABLE, + /** The status of the benchmark is unknown */ + SMT_UNKNOWN +}; + +inline std::ostream& operator<<(std::ostream& out, + BenchmarkStatus status) + CVC4_PUBLIC; + class CVC4_PUBLIC Command { public: virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; @@ -107,15 +121,6 @@ protected: 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; @@ -123,9 +128,6 @@ protected: BenchmarkStatus d_status; };/* class SetBenchmarkStatusCommand */ -inline std::ostream& operator<<(std::ostream& out, - SetBenchmarkStatusCommand::BenchmarkStatus status) - CVC4_PUBLIC; class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { public: @@ -288,16 +290,16 @@ inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { /* output stream insertion operator for benchmark statuses */ inline std::ostream& operator<<(std::ostream& out, - SetBenchmarkStatusCommand::BenchmarkStatus status) { + BenchmarkStatus status) { switch(status) { - case SetBenchmarkStatusCommand::SMT_SATISFIABLE: + case SMT_SATISFIABLE: return out << "sat"; - case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE: + case SMT_UNSATISFIABLE: return out << "unsat"; - case SetBenchmarkStatusCommand::SMT_UNKNOWN: + case SMT_UNKNOWN: return out << "unknown"; default: |