From e5bbc45d20caf51e7df8288d51f20eb12da72aba Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 8 Nov 2021 16:17:58 -0800 Subject: [PATCH] Remove command-verbosity option (#7581) This PR removes the command-verbosity option. It is implemented as a weird special case, and nobody seems to use it anyway. --- src/main/command_executor.cpp | 7 -- src/smt/command.cpp | 102 ++++++++---------- src/smt/command.h | 40 +++---- src/smt/solver_engine.cpp | 79 +------------- src/smt/solver_engine.h | 5 - .../regress0/options/ast-and-sexpr.smt2 | 9 -- .../regress0/options/set-and-get-options.smt2 | 6 -- 7 files changed, 64 insertions(+), 184 deletions(-) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index be3652dd4..ae4dc1e9c 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -213,13 +213,6 @@ bool solverInvoke(api::Solver* solver, } cmd->invoke(solver, sm, out); - // ignore the error if the command-verbosity is 0 for this command - std::string commandName = - std::string("command-verbosity:") + cmd->getCommandName(); - if (solver->getOption(commandName) == "0") - { - return true; - } return !cmd->fail(); } diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 419167e7e..83f761428 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -208,9 +208,7 @@ void Command::invoke(api::Solver* solver, SymbolManager* sm, std::ostream& out) invoke(solver, sm); if (!(isMuted() && ok())) { - printResult( - out, - std::stoul(solver->getOption("command-verbosity:" + getCommandName()))); + printResult(out); } } @@ -226,14 +224,11 @@ void CommandStatus::toStream(std::ostream& out, Language language) const Printer::getPrinter(language)->toStream(out, this); } -void Command::printResult(std::ostream& out, uint32_t verbosity) const +void Command::printResult(std::ostream& out) const { - if (d_commandStatus != NULL) + if (d_commandStatus != nullptr) { - if ((!ok() && verbosity >= 1) || verbosity >= 2) - { - out << *d_commandStatus; - } + out << *d_commandStatus; } } @@ -320,9 +315,7 @@ void EchoCommand::invoke(api::Solver* solver, Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~" << std::endl; d_commandStatus = CommandSuccess::instance(); - printResult( - out, - std::stoul(solver->getOption("command-verbosity:" + getCommandName()))); + printResult(out); } Command* EchoCommand::clone() const { return new EchoCommand(d_output); } @@ -460,11 +453,11 @@ void CheckSatCommand::invoke(api::Solver* solver, SymbolManager* sm) api::Result CheckSatCommand::getResult() const { return d_result; } -void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const +void CheckSatCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -531,12 +524,11 @@ api::Result CheckSatAssumingCommand::getResult() const return d_result; } -void CheckSatAssumingCommand::printResult(std::ostream& out, - uint32_t verbosity) const +void CheckSatAssumingCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -586,11 +578,11 @@ void QueryCommand::invoke(api::Solver* solver, SymbolManager* sm) } api::Result QueryCommand::getResult() const { return d_result; } -void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const +void QueryCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -895,11 +887,11 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm) } api::Result CheckSynthCommand::getResult() const { return d_result; } -void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const +void CheckSynthCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -1514,11 +1506,11 @@ void SimplifyCommand::invoke(api::Solver* solver, SymbolManager* sm) } api::Term SimplifyCommand::getResult() const { return d_result; } -void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const +void SimplifyCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -1593,11 +1585,11 @@ void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm) } api::Term GetValueCommand::getResult() const { return d_result; } -void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const +void GetValueCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -1671,12 +1663,11 @@ void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm) } api::Term GetAssignmentCommand::getResult() const { return d_result; } -void GetAssignmentCommand::printResult(std::ostream& out, - uint32_t verbosity) const +void GetAssignmentCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -1732,11 +1723,11 @@ void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const +void GetModelCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -1883,7 +1874,7 @@ void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const +void GetProofCommand::printResult(std::ostream& out) const { if (ok()) { @@ -1891,7 +1882,7 @@ void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const } else { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } } @@ -1937,12 +1928,11 @@ void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetInstantiationsCommand::printResult(std::ostream& out, - uint32_t verbosity) const +void GetInstantiationsCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -2016,12 +2006,11 @@ void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetInterpolCommand::printResult(std::ostream& out, - uint32_t verbosity) const +void GetInterpolCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -2106,11 +2095,11 @@ void GetAbductCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const +void GetAbductCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -2187,12 +2176,11 @@ api::Term GetQuantifierEliminationCommand::getResult() const { return d_result; } -void GetQuantifierEliminationCommand::printResult(std::ostream& out, - uint32_t verbosity) const +void GetQuantifierEliminationCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -2250,12 +2238,11 @@ std::vector GetUnsatAssumptionsCommand::getResult() const return d_result; } -void GetUnsatAssumptionsCommand::printResult(std::ostream& out, - uint32_t verbosity) const +void GetUnsatAssumptionsCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -2307,12 +2294,11 @@ void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetUnsatCoreCommand::printResult(std::ostream& out, - uint32_t verbosity) const +void GetUnsatCoreCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -2384,12 +2370,11 @@ void GetDifficultyCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetDifficultyCommand::printResult(std::ostream& out, - uint32_t verbosity) const +void GetDifficultyCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -2464,12 +2449,11 @@ void GetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm) } std::string GetAssertionsCommand::getResult() const { return d_result; } -void GetAssertionsCommand::printResult(std::ostream& out, - uint32_t verbosity) const +void GetAssertionsCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else { @@ -2618,11 +2602,11 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) } std::string GetInfoCommand::getResult() const { return d_result; } -void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const +void GetInfoCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else if (d_result != "") { @@ -2719,11 +2703,11 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) } std::string GetOptionCommand::getResult() const { return d_result; } -void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const +void GetOptionCommand::printResult(std::ostream& out) const { if (!ok()) { - this->Command::printResult(out, verbosity); + this->Command::printResult(out); } else if (d_result != "") { diff --git a/src/smt/command.h b/src/smt/command.h index 5733eb3e5..6ca5a7fc8 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -253,7 +253,7 @@ class CVC5_EXPORT Command /** Get the command status (it's NULL if we haven't run yet). */ const CommandStatus* getCommandStatus() const { return d_commandStatus; } - virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const; + virtual void printResult(std::ostream& out) const; /** * Clone this Command (make a shallow copy). @@ -595,7 +595,7 @@ class CVC5_EXPORT CheckSatCommand : public Command CheckSatCommand(); api::Result getResult() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -621,7 +621,7 @@ class CVC5_EXPORT CheckSatAssumingCommand : public Command const std::vector& getTerms() const; api::Result getResult() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -646,7 +646,7 @@ class CVC5_EXPORT QueryCommand : public Command api::Term getTerm() const; api::Result getResult() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -825,7 +825,7 @@ class CVC5_EXPORT CheckSynthCommand : public Command /** returns the result of the check-synth call */ api::Result getResult() const; /** prints the result of the check-synth-call */ - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; /** invokes this command * * This invocation makes the SMT engine build a synthesis conjecture based on @@ -867,7 +867,7 @@ class CVC5_EXPORT SimplifyCommand : public Command api::Term getTerm() const; api::Term getResult() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -889,7 +889,7 @@ class CVC5_EXPORT GetValueCommand : public Command const std::vector& getTerms() const; api::Term getResult() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -908,7 +908,7 @@ class CVC5_EXPORT GetAssignmentCommand : public Command api::Term getResult() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -922,7 +922,7 @@ class CVC5_EXPORT GetModelCommand : public Command public: GetModelCommand(); void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -977,7 +977,7 @@ class CVC5_EXPORT GetProofCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; @@ -998,7 +998,7 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command static bool isEnabled(api::Solver* solver, const api::Result& res); void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -1035,7 +1035,7 @@ class CVC5_EXPORT GetInterpolCommand : public Command api::Term getResult() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -1085,7 +1085,7 @@ class CVC5_EXPORT GetAbductCommand : public Command api::Term getResult() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -1121,7 +1121,7 @@ class CVC5_EXPORT GetQuantifierEliminationCommand : public Command bool getDoFull() const; void invoke(api::Solver* solver, SymbolManager* sm) override; api::Term getResult() const; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1137,7 +1137,7 @@ class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command GetUnsatAssumptionsCommand(); void invoke(api::Solver* solver, SymbolManager* sm) override; std::vector getResult() const; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -1156,7 +1156,7 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command const std::vector& getUnsatCore() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1179,7 +1179,7 @@ class CVC5_EXPORT GetDifficultyCommand : public Command const std::map& getDifficultyMap() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1205,7 +1205,7 @@ class CVC5_EXPORT GetAssertionsCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; std::string getResult() const; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -1266,7 +1266,7 @@ class CVC5_EXPORT GetInfoCommand : public Command std::string getResult() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, @@ -1309,7 +1309,7 @@ class CVC5_EXPORT GetOptionCommand : public Command std::string getResult() const; void invoke(api::Solver* solver, SymbolManager* sm) override; - void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + void printResult(std::ostream& out) const override; Command* clone() const override; std::string getCommandName() const override; void toStream(std::ostream& out, diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 6dc40ac8b..a10f3210f 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1829,34 +1829,7 @@ void SolverEngine::printStatisticsDiff() const void SolverEngine::setOption(const std::string& key, const std::string& value) { Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; - - if (key == "command-verbosity") - { - size_t fstIndex = value.find(" "); - size_t sndIndex = value.find(" ", fstIndex + 1); - if (sndIndex == std::string::npos) - { - string c = value.substr(1, fstIndex - 1); - int v = - std::stoi(value.substr(fstIndex + 1, value.length() - fstIndex - 1)); - 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)"); - } - - if (value.find(" ") != std::string::npos) - { - throw OptionException("bad value for :" + key); - } - - std::string optionarg = value; - options::set(getOptions(), key, optionarg); + options::set(getOptions(), key, value); } void SolverEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } @@ -1865,57 +1838,7 @@ bool SolverEngine::isInternalSubsolver() const { return d_isInternalSubsolver; } std::string SolverEngine::getOption(const std::string& key) const { - NodeManager* nm = d_env->getNodeManager(); - Trace("smt") << "SMT getOption(" << key << ")" << endl; - - if (key.find("command-verbosity:") == 0) - { - auto it = - d_commandVerbosity.find(key.substr(std::strlen("command-verbosity:"))); - if (it != d_commandVerbosity.end()) - { - return std::to_string(it->second); - } - it = d_commandVerbosity.find("*"); - if (it != d_commandVerbosity.end()) - { - return std::to_string(it->second); - } - return "2"; - } - - if (key == "command-verbosity") - { - vector result; - Node defaultVerbosity; - for (const auto& verb : d_commandVerbosity) - { - // treat the command name as a variable name as opposed to a string - // constant to avoid printing double quotes around the name - Node name = nm->mkBoundVar(verb.first, nm->integerType()); - Node value = nm->mkConst(Rational(verb.second)); - if (verb.first == "*") - { - // put the default at the end of the SExpr - defaultVerbosity = nm->mkNode(Kind::SEXPR, name, value); - } - else - { - result.push_back(nm->mkNode(Kind::SEXPR, name, value)); - } - } - // ensure the default is always listed - if (defaultVerbosity.isNull()) - { - defaultVerbosity = nm->mkNode(Kind::SEXPR, - nm->mkBoundVar("*", nm->integerType()), - nm->mkConst(Rational(2))); - } - result.push_back(defaultVerbosity); - return nm->mkNode(Kind::SEXPR, result).toString(); - } - return options::get(getOptions(), key); } diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 7096aec92..d7df78f08 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -1086,11 +1086,6 @@ class CVC5_EXPORT SolverEngine /** Whether this is an internal subsolver. */ bool d_isInternalSubsolver; - /** - * Verbosity of various commands. - */ - std::map d_commandVerbosity; - /** The statistics class */ std::unique_ptr d_stats; diff --git a/test/regress/regress0/options/ast-and-sexpr.smt2 b/test/regress/regress0/options/ast-and-sexpr.smt2 index 41012f888..edd3a2341 100644 --- a/test/regress/regress0/options/ast-and-sexpr.smt2 +++ b/test/regress/regress0/options/ast-and-sexpr.smt2 @@ -1,18 +1,9 @@ -; EXPECT: (SEXPR (SEXPR check-sat (CONST_RATIONAL 2)) (SEXPR * (CONST_RATIONAL 1))) ; EXPECT: (:status unknown) ; This regression tests uses of s-expressions when the output-language is AST (set-option :output-language ast) -; Set the verbosity of all commands to 1 -(set-option :command-verbosity (* 1)) -; Set the verbosity of (check-sat) command to 2 -(set-option :command-verbosity (check-sat 2)) -; Get the verbosity of all commands -(get-option :command-verbosity) -; There is no SMT option to get the verbosity of a specific command - (set-info :source (true false (- 15) 15 15.0 #b00001111 #x0f x |x "| "" """")) (get-info :status) diff --git a/test/regress/regress0/options/set-and-get-options.smt2 b/test/regress/regress0/options/set-and-get-options.smt2 index 24e05ec2a..afa779b05 100644 --- a/test/regress/regress0/options/set-and-get-options.smt2 +++ b/test/regress/regress0/options/set-and-get-options.smt2 @@ -1,14 +1,8 @@ -; EXPECT: ((* 2)) -; EXPECT: ((check-sat 1) (* 1)) ; EXPECT: true ; EXPECT: false ; EXPECT: 15 ; EXPECT: none -(get-option :command-verbosity) -(set-option :command-verbosity (* 1)) -(set-option :command-verbosity (check-sat 1)) -(get-option :command-verbosity) (set-option :check-models true) (get-option :check-models) (set-option :check-models false) -- 2.30.2