From b747578dee53489326bf53743cfc4f83c467cbfd Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 4 Sep 2013 20:29:24 -0400 Subject: [PATCH] Support per-command verbosity settings. --- NEWS | 2 + src/expr/command.cpp | 195 ++++++++++++++++++++++++++----- src/expr/command.h | 60 +++++++--- src/parser/smt2/Smt2.g | 12 +- src/smt/smt_engine.cpp | 2 +- src/smt/smt_engine.h | 5 + src/smt/smt_options_template.cpp | 62 +++++++++- 7 files changed, 287 insertions(+), 51 deletions(-) diff --git a/NEWS b/NEWS index bd7347a75..983491b1b 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,8 @@ Changes since 1.2 intervening push/pop. * Increased compliance to SMT-LIBv2, numerous bugs and usability issues resolved. +* New :command-verbosity SMT option to silence success and error messages + on a per-command basis. API changes to Command infrastructure to support. Changes since 1.1 ================= 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() { diff --git a/src/expr/command.h b/src/expr/command.h index 38a8b1efa..a3d58e5dd 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -215,6 +215,8 @@ public: std::string toString() const throw(); + virtual std::string getCommandName() const throw() = 0; + /** * If false, instruct this Command not to print a success message. */ @@ -240,7 +242,7 @@ public: /** Get the command status (it's NULL if we haven't run yet). */ const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; } - virtual void printResult(std::ostream& out) const throw(); + virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); /** * Maps this Command into one for a different ExprManager, using @@ -287,6 +289,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class EmptyCommand */ class CVC4_PUBLIC EchoCommand : public Command { @@ -300,6 +303,7 @@ public: void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class EchoCommand */ class CVC4_PUBLIC AssertCommand : public Command { @@ -312,6 +316,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class AssertCommand */ class CVC4_PUBLIC PushCommand : public Command { @@ -320,6 +325,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class PushCommand */ class CVC4_PUBLIC PopCommand : public Command { @@ -328,6 +334,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class PopCommand */ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { @@ -352,6 +359,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class DeclareFunctionCommand */ class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { @@ -366,6 +374,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class DeclareTypeCommand */ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { @@ -381,6 +390,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class DefineTypeCommand */ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { @@ -399,6 +409,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class DefineFunctionCommand */ /** @@ -433,6 +444,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class SetUserAttributeCommand */ @@ -447,9 +459,10 @@ public: Expr getExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); Result getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { @@ -462,9 +475,10 @@ public: Expr getExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); Result getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class QueryCommand */ // this is TRANSFORM in the CVC presentation language @@ -478,9 +492,10 @@ public: Expr getTerm() const throw(); void invoke(SmtEngine* smtEngine) throw(); Expr getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class SimplifyCommand */ class CVC4_PUBLIC ExpandDefinitionsCommand : public Command { @@ -493,9 +508,10 @@ public: Expr getTerm() const throw(); void invoke(SmtEngine* smtEngine) throw(); Expr getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class ExpandDefinitionsCommand */ class CVC4_PUBLIC GetValueCommand : public Command { @@ -509,9 +525,10 @@ public: const std::vector& getTerms() const throw(); void invoke(SmtEngine* smtEngine) throw(); Expr getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class GetValueCommand */ class CVC4_PUBLIC GetAssignmentCommand : public Command { @@ -522,9 +539,10 @@ public: ~GetAssignmentCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); SExpr getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class GetAssignmentCommand */ class CVC4_PUBLIC GetModelCommand : public Command { @@ -537,9 +555,10 @@ public: void invoke(SmtEngine* smtEngine) throw(); // Model is private to the library -- for now //Model* getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class GetModelCommand */ class CVC4_PUBLIC GetProofCommand : public Command { @@ -550,9 +569,10 @@ public: ~GetProofCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); Proof* getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class GetProofCommand */ class CVC4_PUBLIC GetUnsatCoreCommand : public Command { @@ -562,9 +582,10 @@ public: GetUnsatCoreCommand() throw(); ~GetUnsatCoreCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class GetUnsatCoreCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command { @@ -575,9 +596,10 @@ public: ~GetAssertionsCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); std::string getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class GetAssertionsCommand */ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { @@ -590,6 +612,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class SetBenchmarkStatusCommand */ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { @@ -602,6 +625,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC SetInfoCommand : public Command { @@ -616,6 +640,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class SetInfoCommand */ class CVC4_PUBLIC GetInfoCommand : public Command { @@ -628,9 +653,10 @@ public: std::string getFlag() const throw(); void invoke(SmtEngine* smtEngine) throw(); std::string getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class GetInfoCommand */ class CVC4_PUBLIC SetOptionCommand : public Command { @@ -645,6 +671,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class SetOptionCommand */ class CVC4_PUBLIC GetOptionCommand : public Command { @@ -657,9 +684,10 @@ public: std::string getFlag() const throw(); void invoke(SmtEngine* smtEngine) throw(); std::string getResult() const throw(); - void printResult(std::ostream& out) const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class GetOptionCommand */ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { @@ -673,6 +701,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class DatatypeDeclarationCommand */ class CVC4_PUBLIC RewriteRuleCommand : public Command { @@ -703,6 +732,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class RewriteRuleCommand */ class CVC4_PUBLIC PropagateRuleCommand : public Command { @@ -738,6 +768,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class PropagateRuleCommand */ @@ -748,6 +779,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class QuitCommand */ class CVC4_PUBLIC CommentCommand : public Command { @@ -759,6 +791,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class CommentCommand */ class CVC4_PUBLIC CommandSequence : public Command { @@ -788,6 +821,7 @@ public: Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; + std::string getCommandName() const throw(); };/* class CommandSequence */ class CVC4_PUBLIC DeclarationSequence : public CommandSequence { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f047bc88e..23f0fb9fa 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -242,9 +242,8 @@ command returns [CVC4::Command* cmd = NULL] GET_INFO_TOK KEYWORD { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); } | /* set-option */ - SET_OPTION_TOK KEYWORD symbolicExpr[sexpr] - { name = AntlrInput::tokenText($KEYWORD); - PARSER_STATE->setOption(name.c_str() + 1, sexpr); + SET_OPTION_TOK keyword[name] symbolicExpr[sexpr] + { PARSER_STATE->setOption(name.c_str() + 1, sexpr); cmd = new SetOptionCommand(name.c_str() + 1, sexpr); } | /* get-option */ GET_OPTION_TOK KEYWORD @@ -701,6 +700,8 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] { sexpr = SExpr(s); } | symbol[s,CHECK_NONE,SYM_SORT] { sexpr = SExpr(SExpr::Keyword(s)); } + | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) + { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } | builtinOp[k] { std::stringstream ss; ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k); @@ -708,6 +709,11 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] } ; +keyword[std::string& s] + : KEYWORD + { s = AntlrInput::tokenText($KEYWORD); } + ; + simpleSymbolicExpr[CVC4::SExpr& sexpr] : simpleSymbolicExprNoKeyword[sexpr] | KEYWORD diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 603e82c3e..810715885 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1172,7 +1172,7 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const return stats; } else if(key == "error-behavior") { // immediate-exit | continued-execution - return SExpr::Keyword("immediate-exit"); + return SExpr::Keyword("continued-execution"); } else if(key == "name") { return Configuration::getName(); } else if(key == "version") { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 9f00fad6b..1da8d26da 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -238,6 +238,11 @@ class CVC4_PUBLIC SmtEngine { */ std::string d_filename; + /** + * Verbosity of various commands. + */ + std::map d_commandVerbosity; + /** * A private utility class to SmtEngine. */ diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp index 638cf2f83..228c18adb 100644 --- a/src/smt/smt_options_template.cpp +++ b/src/smt/smt_options_template.cpp @@ -44,11 +44,29 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) Dump("benchmark") << SetOptionCommand(key, value); } + if(key == "command-verbosity") { + if(!value.isAtom()) { + const vector& cs = value.getChildren(); + if(cs.size() == 2 && + (cs[0].isKeyword() || cs[0].isString()) && + cs[1].isInteger()) { + string c = cs[0].getValue(); + const Integer& v = cs[1].getIntegerValue(); + if(v < 0 || v > 2) { + throw OptionException("command-verbosity must be 0, 1, or 2"); + } + d_commandVerbosity[c] = v; + return; + } + } + throw OptionException("command-verbosity value must be a tuple (command-name, integer)"); + } + string optionarg = value.getValue(); ${smt_setoption_handlers} -#line 52 "${template}" +#line 70 "${template}" throw UnrecognizedOptionException(key); } @@ -63,9 +81,49 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const Dump("benchmark") << GetOptionCommand(key); } + if(key == "command-verbosity") { + vector result; + SExpr defaultVerbosity; + for(map::const_iterator i = d_commandVerbosity.begin(); + i != d_commandVerbosity.end(); + ++i) { + vector v; + v.push_back((*i).first); + v.push_back((*i).second); + if((*i).first == "*") { + // put the default at the end of the SExpr + defaultVerbosity = v; + } else { + result.push_back(v); + } + } + // put the default at the end of the SExpr + if(!defaultVerbosity.isAtom()) { + result.push_back(defaultVerbosity); + } else { + // ensure the default is always listed + vector v; + v.push_back("*"); + v.push_back(Integer(2)); + result.push_back(v); + } + return result; + } else if(key.length() >= 18 && + key.compare(0, 18, "command-verbosity:") == 0) { + map::const_iterator i = d_commandVerbosity.find(key.c_str() + 18); + if(i != d_commandVerbosity.end()) { + return (*i).second; + } + i = d_commandVerbosity.find("*"); + if(i != d_commandVerbosity.end()) { + return (*i).second; + } + return Integer(2); + } + ${smt_getoption_handlers} -#line 69 "${template}" +#line 127 "${template}" throw UnrecognizedOptionException(key); } -- 2.30.2