From b747578dee53489326bf53743cfc4f83c467cbfd Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 4 Sep 2013 20:29:24 -0400 Subject: Support per-command verbosity settings. --- src/expr/command.cpp | 195 ++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 163 insertions(+), 32 deletions(-) (limited to 'src/expr/command.cpp') 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& 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& 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() { -- cgit v1.2.3