summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--NEWS2
-rw-r--r--src/expr/command.cpp195
-rw-r--r--src/expr/command.h60
-rw-r--r--src/parser/smt2/Smt2.g12
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/smt/smt_engine.h5
-rw-r--r--src/smt/smt_options_template.cpp62
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<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() {
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<Expr>& 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
@@ -239,6 +239,11 @@ class CVC4_PUBLIC SmtEngine {
std::string d_filename;
/**
+ * Verbosity of various commands.
+ */
+ std::map<std::string, Integer> d_commandVerbosity;
+
+ /**
* A private utility class to SmtEngine.
*/
smt::SmtEnginePrivate* d_private;
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<SExpr>& 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<SExpr> result;
+ SExpr defaultVerbosity;
+ for(map<string, Integer>::const_iterator i = d_commandVerbosity.begin();
+ i != d_commandVerbosity.end();
+ ++i) {
+ vector<SExpr> 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<SExpr> 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<string, Integer>::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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback