diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-04 19:31:24 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-04 19:31:24 +0000 |
commit | 67a3ba16218ca0a936a6f2430dce721a076885f3 (patch) | |
tree | dff41999a0fb7a043c3421272e451cb2718010a4 /src/expr/command.h | |
parent | 437686e2050a622a3f7e68077aff46fd6af83cbd (diff) |
Adding general support for SMT2 set-info command
Diffstat (limited to 'src/expr/command.h')
-rw-r--r-- | src/expr/command.h | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/expr/command.h b/src/expr/command.h index 3be957feb..5061722f6 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -29,6 +29,7 @@ #include "expr/expr.h" #include "expr/type.h" #include "util/result.h" +#include "util/sexpr.h" namespace CVC4 { @@ -142,6 +143,16 @@ protected: std::string d_logic; };/* class SetBenchmarkLogicCommand */ +class CVC4_PUBLIC SetInfoCommand : public Command { +public: + SetInfoCommand(std::string flag, SExpr& sexpr); + void invoke(SmtEngine* smt); + void toStream(std::ostream& out) const; +protected: + std::string d_flag; + SExpr d_sexpr; +};/* class SetInfoCommand */ + class CVC4_PUBLIC CommandSequence : public Command { public: CommandSequence(); @@ -300,6 +311,17 @@ 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) { |