Add the ability to "mute" commands, needed for SMT-LIB compliance.

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 9edc77e391ef94e3fd38d7ed9912fe73a8f796af..43679113c210d7f3cbcb9f8195240fdd28c20821 100644 (file)
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -74,11 +74,12 @@ ostream& operator<<(ostream& out, const CommandStatus* s) throw() {
 
 /* class Command */
 
-Command::Command() throw() : d_commandStatus(NULL) {
+Command::Command() throw() : d_commandStatus(NULL), d_muted(false) {
 }
 
 Command::Command(const Command& cmd) {
   d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone();
+  d_muted = cmd.d_muted;
 }
 
 Command::~Command() throw() {
@@ -98,7 +99,9 @@ bool Command::fail() const throw() {
 
 void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
   invoke(smtEngine);
-  printResult(out);
+  if(!(isMuted() && ok())) {
+    printResult(out);
+  }
 }
 
 std::string Command::toString() const throw() {

diff --git a/src/expr/command.h b/src/expr/command.h
index 9877044fb41141fee66dbe6e1b4ceb5a27de4409..8e59834031907c54bf28c93b3cee098a9bd72425 100644 (file)
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -193,6 +193,12 @@ protected:
    */
   const CommandStatus* d_commandStatus;
 
+  /**
+   * True if this command is "muted"---i.e., don't print "success" on
+   * successful execution.
+   */
+  bool d_muted;
+
 public:
   typedef CommandPrintSuccess printsuccess;
 
@@ -209,6 +215,16 @@ public:
 
   std::string toString() const throw();
 
+  /**
+   * If false, instruct this Command not to print a success message.
+   */
+  void setMuted(bool muted) throw() { d_muted = muted; }
+
+  /**
+   * Determine whether this Command will print a success message.
+   */
+  bool isMuted() throw() { return d_muted; }
+
   /**
    * Either the command hasn't run yet, or it completed successfully
    * (CommandSuccess, not CommandUnsupported or CommandFailure).

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a390cf4527d55d0bc0597fa35a190c7a00ddde05..387a24fe1142c9e360df9971e9d8f1186f0c0c0c 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -952,6 +952,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       std::string attr_name = attr;
       attr_name.erase( attr_name.begin() );
       Command* c = new SetUserAttributeCommand( attr_name, expr );
+      c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     } else {
       PARSER_STATE->attributeNotSupported(attr);
@@ -979,6 +980,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       // bind name to expr with define-fun
       Command* c =
         new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
+      c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     }
   ;

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index e1f977890380a10694f3c2797d047bcb3267d73e..5d104531fe1bf210490db6f7bfaec5d1d5b12064 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -290,7 +290,9 @@ void Smt2::checkThatLogicIsSet() {
 
       setLogic("ALL_SUPPORTED");
 
-      preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED"));
+      Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
+      c->setMuted(true);
+      preemptCommand(c);
     }
   }
 }