Adding general support for SMT2 set-info command

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) {