Support per-command verbosity settings.

1 files changed, 163 insertions, 32 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 423bf3234..d0bd02c8a 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -100,7 +100,7 @@ bool Command::fail() const throw() {
 void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
   invoke(smtEngine);
   if(!(isMuted() && ok())) {
-    printResult(out);
+    printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
   }
 }
 
@@ -119,9 +119,11 @@ void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const t
   Printer::getPrinter(language)->toStream(out, this);
 }
 
-void Command::printResult(std::ostream& out) const throw() {
+void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(d_commandStatus != NULL) {
-    out << *d_commandStatus;
+    if((!ok() && verbosity >= 1) || verbosity >= 2) {
+      out << *d_commandStatus;
+    }
   }
 }
 
@@ -148,6 +150,10 @@ Command* EmptyCommand::clone() const {
   return new EmptyCommand(d_name);
 }
 
+std::string EmptyCommand::getCommandName() const throw() {
+  return "empty";
+}
+
 /* class EchoCommand */
 
 EchoCommand::EchoCommand(std::string output) throw() :
@@ -166,7 +172,7 @@ void EchoCommand::invoke(SmtEngine* smtEngine) throw() {
 void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
   out << d_output << std::endl;
   d_commandStatus = CommandSuccess::instance();
-  printResult(out);
+  printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
 }
 
 Command* EchoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
@@ -177,6 +183,10 @@ Command* EchoCommand::clone() const {
   return new EchoCommand(d_output);
 }
 
+std::string EchoCommand::getCommandName() const throw() {
+  return "echo";
+}
+
 /* class AssertCommand */
 
 AssertCommand::AssertCommand(const Expr& e) throw() :
@@ -204,6 +214,11 @@ Command* AssertCommand::clone() const {
   return new AssertCommand(d_expr);
 }
 
+std::string AssertCommand::getCommandName() const throw() {
+  return "assert";
+}
+
+
 /* class PushCommand */
 
 void PushCommand::invoke(SmtEngine* smtEngine) throw() {
@@ -223,6 +238,10 @@ Command* PushCommand::clone() const {
   return new PushCommand();
 }
 
+std::string PushCommand::getCommandName() const throw() {
+  return "push";
+}
+
 /* class PopCommand */
 
 void PopCommand::invoke(SmtEngine* smtEngine) throw() {
@@ -242,6 +261,10 @@ Command* PopCommand::clone() const {
   return new PopCommand();
 }
 
+std::string PopCommand::getCommandName() const throw() {
+  return "pop";
+}
+
 /* class CheckSatCommand */
 
 CheckSatCommand::CheckSatCommand() throw() :
@@ -269,9 +292,9 @@ Result CheckSatCommand::getResult() const throw() {
   return d_result;
 }
 
-void CheckSatCommand::printResult(std::ostream& out) const throw() {
+void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else {
     out << d_result << endl;
   }
@@ -289,6 +312,10 @@ Command* CheckSatCommand::clone() const {
   return c;
 }
 
+std::string CheckSatCommand::getCommandName() const throw() {
+  return "check-sat";
+}
+
 /* class QueryCommand */
 
 QueryCommand::QueryCommand(const Expr& e) throw() :
@@ -312,9 +339,9 @@ Result QueryCommand::getResult() const throw() {
   return d_result;
 }
 
-void QueryCommand::printResult(std::ostream& out) const throw() {
+void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else {
     out << d_result << endl;
   }
@@ -332,6 +359,10 @@ Command* QueryCommand::clone() const {
   return c;
 }
 
+std::string QueryCommand::getCommandName() const throw() {
+  return "query";
+}
+
 /* class QuitCommand */
 
 QuitCommand::QuitCommand() throw() {
@@ -350,6 +381,10 @@ Command* QuitCommand::clone() const {
   return new QuitCommand();
 }
 
+std::string QuitCommand::getCommandName() const throw() {
+  return "exit";
+}
+
 /* class CommentCommand */
 
 CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
@@ -372,6 +407,10 @@ Command* CommentCommand::clone() const {
   return new CommentCommand(d_comment);
 }
 
+std::string CommentCommand::getCommandName() const throw() {
+  return "comment";
+}
+
 /* class CommandSequence */
 
 CommandSequence::CommandSequence() throw() :
@@ -422,10 +461,6 @@ void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
-CommandSequence::const_iterator CommandSequence::begin() const throw() {
-  return d_commandSequence.begin();
-}
-
 Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
   CommandSequence* seq = new CommandSequence();
   for(iterator i = begin(); i != end(); ++i) {
@@ -446,6 +481,10 @@ Command* CommandSequence::clone() const {
   return seq;
 }
 
+CommandSequence::const_iterator CommandSequence::begin() const throw() {
+  return d_commandSequence.begin();
+}
+
 CommandSequence::const_iterator CommandSequence::end() const throw() {
   return d_commandSequence.end();
 }
@@ -458,6 +497,10 @@ CommandSequence::iterator CommandSequence::end() throw() {
   return d_commandSequence.end();
 }
 
+std::string CommandSequence::getCommandName() const throw() {
+  return "sequence";
+}
+
 /* class DeclarationSequenceCommand */
 
 /* class DeclarationDefinitionCommand */
@@ -500,6 +543,10 @@ Command* DeclareFunctionCommand::clone() const {
   return new DeclareFunctionCommand(d_symbol, d_func, d_type);
 }
 
+std::string DeclareFunctionCommand::getCommandName() const throw() {
+  return "declare-fun";
+}
+
 /* class DeclareTypeCommand */
 
 DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() :
@@ -530,6 +577,10 @@ Command* DeclareTypeCommand::clone() const {
   return new DeclareTypeCommand(d_symbol, d_arity, d_type);
 }
 
+std::string DeclareTypeCommand::getCommandName() const throw() {
+  return "declare-sort";
+}
+
 /* class DefineTypeCommand */
 
 DefineTypeCommand::DefineTypeCommand(const std::string& id,
@@ -571,6 +622,10 @@ Command* DefineTypeCommand::clone() const {
   return new DefineTypeCommand(d_symbol, d_params, d_type);
 }
 
+std::string DefineTypeCommand::getCommandName() const throw() {
+  return "define-sort";
+}
+
 /* class DefineFunctionCommand */
 
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
@@ -628,6 +683,10 @@ Command* DefineFunctionCommand::clone() const {
   return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula);
 }
 
+std::string DefineFunctionCommand::getCommandName() const throw() {
+  return "define-fun";
+}
+
 /* class DefineNamedFunctionCommand */
 
 DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
@@ -695,6 +754,10 @@ Command* SetUserAttributeCommand::clone() const{
   return new SetUserAttributeCommand( d_attr, d_expr );
 }
 
+std::string SetUserAttributeCommand::getCommandName() const throw() {
+  return "set-user-attribute";
+}
+
 /* class SimplifyCommand */
 
 SimplifyCommand::SimplifyCommand(Expr term) throw() :
@@ -718,9 +781,9 @@ Expr SimplifyCommand::getResult() const throw() {
   return d_result;
 }
 
-void SimplifyCommand::printResult(std::ostream& out) const throw() {
+void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else {
     out << d_result << endl;
   }
@@ -738,6 +801,10 @@ Command* SimplifyCommand::clone() const {
   return c;
 }
 
+std::string SimplifyCommand::getCommandName() const throw() {
+  return "simplify";
+}
+
 /* class ExpandDefinitionsCommand */
 
 ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() :
@@ -757,9 +824,9 @@ Expr ExpandDefinitionsCommand::getResult() const throw() {
   return d_result;
 }
 
-void ExpandDefinitionsCommand::printResult(std::ostream& out) const throw() {
+void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else {
     out << d_result << endl;
   }
@@ -777,6 +844,10 @@ Command* ExpandDefinitionsCommand::clone() const {
   return c;
 }
 
+std::string ExpandDefinitionsCommand::getCommandName() const throw() {
+  return "expand-definitions";
+}
+
 /* class GetValueCommand */
 
 GetValueCommand::GetValueCommand(Expr term) throw() :
@@ -816,9 +887,9 @@ Expr GetValueCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetValueCommand::printResult(std::ostream& out) const throw() {
+void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else {
     Expr::dag::Scope scope(out, false);
     out << d_result << endl;
@@ -841,6 +912,10 @@ Command* GetValueCommand::clone() const {
   return c;
 }
 
+std::string GetValueCommand::getCommandName() const throw() {
+  return "get-value";
+}
+
 /* class GetAssignmentCommand */
 
 GetAssignmentCommand::GetAssignmentCommand() throw() {
@@ -859,9 +934,9 @@ SExpr GetAssignmentCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetAssignmentCommand::printResult(std::ostream& out) const throw() {
+void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else {
     out << d_result << endl;
   }
@@ -879,6 +954,10 @@ Command* GetAssignmentCommand::clone() const {
   return c;
 }
 
+std::string GetAssignmentCommand::getCommandName() const throw() {
+  return "get-assignment";
+}
+
 /* class GetModelCommand */
 
 GetModelCommand::GetModelCommand() throw() {
@@ -900,9 +979,9 @@ Model* GetModelCommand::getResult() const throw() {
 }
 */
 
-void GetModelCommand::printResult(std::ostream& out) const throw() {
+void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else {
     out << *d_result;
   }
@@ -922,6 +1001,10 @@ Command* GetModelCommand::clone() const {
   return c;
 }
 
+std::string GetModelCommand::getCommandName() const throw() {
+  return "get-model";
+}
+
 /* class GetProofCommand */
 
 GetProofCommand::GetProofCommand() throw() {
@@ -940,9 +1023,9 @@ Proof* GetProofCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetProofCommand::printResult(std::ostream& out) const throw() {
+void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else {
     d_result->toStream(out);
   }
@@ -960,6 +1043,10 @@ Command* GetProofCommand::clone() const {
   return c;
 }
 
+std::string GetProofCommand::getCommandName() const throw() {
+  return "get-proof";
+}
+
 /* class GetUnsatCoreCommand */
 
 GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
@@ -977,9 +1064,9 @@ void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = new CommandUnsupported();
 }
 
-void GetUnsatCoreCommand::printResult(std::ostream& out) const throw() {
+void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else {
     //do nothing -- unsat cores not yet supported
     // d_result->toStream(out);
@@ -998,6 +1085,10 @@ Command* GetUnsatCoreCommand::clone() const {
   return c;
 }
 
+std::string GetUnsatCoreCommand::getCommandName() const throw() {
+  return "get-unsat-core";
+}
+
 /* class GetAssertionsCommand */
 
 GetAssertionsCommand::GetAssertionsCommand() throw() {
@@ -1021,9 +1112,9 @@ std::string GetAssertionsCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetAssertionsCommand::printResult(std::ostream& out) const throw() {
+void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else {
     out << d_result;
   }
@@ -1041,6 +1132,10 @@ Command* GetAssertionsCommand::clone() const {
   return c;
 }
 
+std::string GetAssertionsCommand::getCommandName() const throw() {
+  return "get-assertions";
+}
+
 /* class SetBenchmarkStatusCommand */
 
 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
@@ -1071,6 +1166,10 @@ Command* SetBenchmarkStatusCommand::clone() const {
   return new SetBenchmarkStatusCommand(d_status);
 }
 
+std::string SetBenchmarkStatusCommand::getCommandName() const throw() {
+  return "set-info";
+}
+
 /* class SetBenchmarkLogicCommand */
 
 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
@@ -1098,6 +1197,10 @@ Command* SetBenchmarkLogicCommand::clone() const {
   return new SetBenchmarkLogicCommand(d_logic);
 }
 
+std::string SetBenchmarkLogicCommand::getCommandName() const throw() {
+  return "set-logic";
+}
+
 /* class SetInfoCommand */
 
 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
@@ -1133,6 +1236,10 @@ Command* SetInfoCommand::clone() const {
   return new SetInfoCommand(d_flag, d_sexpr);
 }
 
+std::string SetInfoCommand::getCommandName() const throw() {
+  return "set-info";
+}
+
 /* class GetInfoCommand */
 
 GetInfoCommand::GetInfoCommand(std::string flag) throw() :
@@ -1163,9 +1270,9 @@ std::string GetInfoCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetInfoCommand::printResult(std::ostream& out) const throw() {
+void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else if(d_result != "") {
     out << d_result << endl;
   }
@@ -1183,6 +1290,10 @@ Command* GetInfoCommand::clone() const {
   return c;
 }
 
+std::string GetInfoCommand::getCommandName() const throw() {
+  return "get-info";
+}
+
 /* class SetOptionCommand */
 
 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
@@ -1217,6 +1328,10 @@ Command* SetOptionCommand::clone() const {
   return new SetOptionCommand(d_flag, d_sexpr);
 }
 
+std::string SetOptionCommand::getCommandName() const throw() {
+  return "set-option";
+}
+
 /* class GetOptionCommand */
 
 GetOptionCommand::GetOptionCommand(std::string flag) throw() :
@@ -1245,9 +1360,9 @@ std::string GetOptionCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetOptionCommand::printResult(std::ostream& out) const throw() {
+void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
-    this->Command::printResult(out);
+    this->Command::printResult(out, verbosity);
   } else if(d_result != "") {
     out << d_result << endl;
   }
@@ -1265,6 +1380,10 @@ Command* GetOptionCommand::clone() const {
   return c;
 }
 
+std::string GetOptionCommand::getCommandName() const throw() {
+  return "get-option";
+}
+
 /* class DatatypeDeclarationCommand */
 
 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
@@ -1294,6 +1413,10 @@ Command* DatatypeDeclarationCommand::clone() const {
   return new DatatypeDeclarationCommand(d_datatypes);
 }
 
+std::string DatatypeDeclarationCommand::getCommandName() const throw() {
+  return "declare-datatypes";
+}
+
 /* class RewriteRuleCommand */
 
 RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
@@ -1394,6 +1517,10 @@ Command* RewriteRuleCommand::clone() const {
   return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers);
 }
 
+std::string RewriteRuleCommand::getCommandName() const throw() {
+  return "rewrite-rule";
+}
+
 /* class PropagateRuleCommand */
 
 PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
@@ -1511,6 +1638,10 @@ Command* PropagateRuleCommand::clone() const {
   return new PropagateRuleCommand(d_vars, d_guards, d_heads, d_body, d_triggers);
 }
 
+std::string PropagateRuleCommand::getCommandName() const throw() {
+  return "propagate-rule";
+}
+
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out,
                          BenchmarkStatus status) throw() {