From 67a3ba16218ca0a936a6f2430dce721a076885f3 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 4 May 2010 19:31:24 +0000 Subject: Adding general support for SMT2 set-info command --- src/expr/command.h | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'src/expr/command.h') 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) { -- cgit v1.2.3