diff options
Diffstat (limited to 'src/smt/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 334 |
1 files changed, 260 insertions, 74 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 040d87250..e61ea868f 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2,9 +2,9 @@ /*! \file command.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Francois Bobot + ** Tim King, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -104,7 +104,25 @@ ostream& operator<<(ostream& out, const CommandStatus* s) return out; } -/* class CommandPrintSuccess */ + +/* output stream insertion operator for benchmark statuses */ +std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) +{ + switch (status) + { + case SMT_SATISFIABLE: return out << "sat"; + + case SMT_UNSATISFIABLE: return out << "unsat"; + + case SMT_UNKNOWN: return out << "unknown"; + + default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]"; + } +} + +/* -------------------------------------------------------------------------- */ +/* class CommandPrintSuccess */ +/* -------------------------------------------------------------------------- */ void CommandPrintSuccess::applyPrintSuccess(std::ostream& out) { @@ -127,7 +145,9 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) return out; } -/* class Command */ +/* -------------------------------------------------------------------------- */ +/* class Command */ +/* -------------------------------------------------------------------------- */ Command::Command() : d_commandStatus(NULL), d_muted(false) {} Command::Command(const Command& cmd) @@ -208,7 +228,9 @@ void Command::printResult(std::ostream& out, uint32_t verbosity) const } } -/* class EmptyCommand */ +/* -------------------------------------------------------------------------- */ +/* class EmptyCommand */ +/* -------------------------------------------------------------------------- */ EmptyCommand::EmptyCommand(std::string name) : d_name(name) {} std::string EmptyCommand::getName() const { return d_name; } @@ -226,7 +248,10 @@ Command* EmptyCommand::exportTo(ExprManager* exprManager, Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); } std::string EmptyCommand::getCommandName() const { return "empty"; } -/* class EchoCommand */ + +/* -------------------------------------------------------------------------- */ +/* class EchoCommand */ +/* -------------------------------------------------------------------------- */ EchoCommand::EchoCommand(std::string output) : d_output(output) {} std::string EchoCommand::getOutput() const { return d_output; } @@ -254,7 +279,10 @@ Command* EchoCommand::exportTo(ExprManager* exprManager, Command* EchoCommand::clone() const { return new EchoCommand(d_output); } std::string EchoCommand::getCommandName() const { return "echo"; } -/* class AssertCommand */ + +/* -------------------------------------------------------------------------- */ +/* class AssertCommand */ +/* -------------------------------------------------------------------------- */ AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) : d_expr(e), d_inUnsatCore(inUnsatCore) @@ -292,7 +320,10 @@ Command* AssertCommand::clone() const } std::string AssertCommand::getCommandName() const { return "assert"; } -/* class PushCommand */ + +/* -------------------------------------------------------------------------- */ +/* class PushCommand */ +/* -------------------------------------------------------------------------- */ void PushCommand::invoke(SmtEngine* smtEngine) { @@ -319,7 +350,10 @@ Command* PushCommand::exportTo(ExprManager* exprManager, Command* PushCommand::clone() const { return new PushCommand(); } std::string PushCommand::getCommandName() const { return "push"; } -/* class PopCommand */ + +/* -------------------------------------------------------------------------- */ +/* class PopCommand */ +/* -------------------------------------------------------------------------- */ void PopCommand::invoke(SmtEngine* smtEngine) { @@ -346,7 +380,10 @@ Command* PopCommand::exportTo(ExprManager* exprManager, Command* PopCommand::clone() const { return new PopCommand(); } std::string PopCommand::getCommandName() const { return "pop"; } -/* class CheckSatCommand */ + +/* -------------------------------------------------------------------------- */ +/* class CheckSatCommand */ +/* -------------------------------------------------------------------------- */ CheckSatCommand::CheckSatCommand() : d_expr() {} CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) @@ -398,7 +435,90 @@ Command* CheckSatCommand::clone() const } std::string CheckSatCommand::getCommandName() const { return "check-sat"; } -/* class QueryCommand */ + +/* -------------------------------------------------------------------------- */ +/* class CheckSatAssumingCommand */ +/* -------------------------------------------------------------------------- */ + +CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term) : d_terms() +{ + d_terms.push_back(term); +} + +CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector<Expr>& terms, + bool inUnsatCore) + : d_terms(terms), d_inUnsatCore(inUnsatCore) +{ + PrettyCheckArgument( + terms.size() >= 1, terms, "cannot get-value of an empty set of terms"); +} + +const std::vector<Expr>& CheckSatAssumingCommand::getTerms() const +{ + return d_terms; +} + +void CheckSatAssumingCommand::invoke(SmtEngine* smtEngine) +{ + try + { + d_result = smtEngine->checkSat(d_terms); + d_commandStatus = CommandSuccess::instance(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Result CheckSatAssumingCommand::getResult() const +{ + return d_result; +} + +void CheckSatAssumingCommand::printResult(std::ostream& out, + uint32_t verbosity) const +{ + if (!ok()) + { + this->Command::printResult(out, verbosity); + } + else + { + out << d_result << endl; + } +} + +Command* CheckSatAssumingCommand::exportTo( + ExprManager* exprManager, ExprManagerMapCollection& variableMap) +{ + vector<Expr> exportedTerms; + for (const Expr& e : d_terms) + { + exportedTerms.push_back(e.exportTo(exprManager, variableMap)); + } + CheckSatAssumingCommand* c = + new CheckSatAssumingCommand(exportedTerms, d_inUnsatCore); + c->d_result = d_result; + return c; +} + +Command* CheckSatAssumingCommand::clone() const +{ + CheckSatAssumingCommand* c = + new CheckSatAssumingCommand(d_terms, d_inUnsatCore); + c->d_result = d_result; + return c; +} + +std::string CheckSatAssumingCommand::getCommandName() const +{ + return "check-sat-assuming"; +} + +/* -------------------------------------------------------------------------- */ +/* class QueryCommand */ +/* -------------------------------------------------------------------------- */ QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) : d_expr(e), d_inUnsatCore(inUnsatCore) @@ -449,7 +569,10 @@ Command* QueryCommand::clone() const } std::string QueryCommand::getCommandName() const { return "query"; } -/* class CheckSynthCommand */ + +/* -------------------------------------------------------------------------- */ +/* class CheckSynthCommand */ +/* -------------------------------------------------------------------------- */ CheckSynthCommand::CheckSynthCommand() : d_expr() {} CheckSynthCommand::CheckSynthCommand(const Expr& expr) : d_expr(expr) {} @@ -524,7 +647,10 @@ Command* CheckSynthCommand::clone() const } std::string CheckSynthCommand::getCommandName() const { return "check-synth"; } -/* class ResetCommand */ + +/* -------------------------------------------------------------------------- */ +/* class ResetCommand */ +/* -------------------------------------------------------------------------- */ void ResetCommand::invoke(SmtEngine* smtEngine) { @@ -547,7 +673,10 @@ Command* ResetCommand::exportTo(ExprManager* exprManager, Command* ResetCommand::clone() const { return new ResetCommand(); } std::string ResetCommand::getCommandName() const { return "reset"; } -/* class ResetAssertionsCommand */ + +/* -------------------------------------------------------------------------- */ +/* class ResetAssertionsCommand */ +/* -------------------------------------------------------------------------- */ void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) { @@ -578,7 +707,9 @@ std::string ResetAssertionsCommand::getCommandName() const return "reset-assertions"; } -/* class QuitCommand */ +/* -------------------------------------------------------------------------- */ +/* class QuitCommand */ +/* -------------------------------------------------------------------------- */ void QuitCommand::invoke(SmtEngine* smtEngine) { @@ -594,7 +725,10 @@ Command* QuitCommand::exportTo(ExprManager* exprManager, Command* QuitCommand::clone() const { return new QuitCommand(); } std::string QuitCommand::getCommandName() const { return "exit"; } -/* class CommentCommand */ + +/* -------------------------------------------------------------------------- */ +/* class CommentCommand */ +/* -------------------------------------------------------------------------- */ CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {} std::string CommentCommand::getComment() const { return d_comment; } @@ -612,7 +746,10 @@ Command* CommentCommand::exportTo(ExprManager* exprManager, Command* CommentCommand::clone() const { return new CommentCommand(d_comment); } std::string CommentCommand::getCommandName() const { return "comment"; } -/* class CommandSequence */ + +/* -------------------------------------------------------------------------- */ +/* class CommandSequence */ +/* -------------------------------------------------------------------------- */ CommandSequence::CommandSequence() : d_index(0) {} CommandSequence::~CommandSequence() @@ -712,9 +849,10 @@ CommandSequence::iterator CommandSequence::end() } std::string CommandSequence::getCommandName() const { return "sequence"; } -/* class DeclarationSequenceCommand */ -/* class DeclarationDefinitionCommand */ +/* -------------------------------------------------------------------------- */ +/* class DeclarationDefinitionCommand */ +/* -------------------------------------------------------------------------- */ DeclarationDefinitionCommand::DeclarationDefinitionCommand( const std::string& id) @@ -723,7 +861,10 @@ DeclarationDefinitionCommand::DeclarationDefinitionCommand( } std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; } -/* class DeclareFunctionCommand */ + +/* -------------------------------------------------------------------------- */ +/* class DeclareFunctionCommand */ +/* -------------------------------------------------------------------------- */ DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, @@ -781,7 +922,9 @@ std::string DeclareFunctionCommand::getCommandName() const return "declare-fun"; } -/* class DeclareTypeCommand */ +/* -------------------------------------------------------------------------- */ +/* class DeclareTypeCommand */ +/* -------------------------------------------------------------------------- */ DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, @@ -814,7 +957,9 @@ std::string DeclareTypeCommand::getCommandName() const return "declare-sort"; } -/* class DefineTypeCommand */ +/* -------------------------------------------------------------------------- */ +/* class DefineTypeCommand */ +/* -------------------------------------------------------------------------- */ DefineTypeCommand::DefineTypeCommand(const std::string& id, Type t) : DeclarationDefinitionCommand(id), d_params(), d_type(t) @@ -857,7 +1002,10 @@ Command* DefineTypeCommand::clone() const } std::string DefineTypeCommand::getCommandName() const { return "define-sort"; } -/* class DefineFunctionCommand */ + +/* -------------------------------------------------------------------------- */ +/* class DefineFunctionCommand */ +/* -------------------------------------------------------------------------- */ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, Expr func, @@ -927,7 +1075,9 @@ std::string DefineFunctionCommand::getCommandName() const return "define-fun"; } -/* class DefineNamedFunctionCommand */ +/* -------------------------------------------------------------------------- */ +/* class DefineNamedFunctionCommand */ +/* -------------------------------------------------------------------------- */ DefineNamedFunctionCommand::DefineNamedFunctionCommand( const std::string& id, @@ -967,7 +1117,9 @@ Command* DefineNamedFunctionCommand::clone() const return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); } -/* class DefineFunctionRecCommand */ +/* -------------------------------------------------------------------------- */ +/* class DefineFunctionRecCommand */ +/* -------------------------------------------------------------------------- */ DefineFunctionRecCommand::DefineFunctionRecCommand( Expr func, const std::vector<Expr>& formals, Expr formula) @@ -979,7 +1131,7 @@ DefineFunctionRecCommand::DefineFunctionRecCommand( DefineFunctionRecCommand::DefineFunctionRecCommand( const std::vector<Expr>& funcs, - const std::vector<std::vector<Expr> >& formals, + const std::vector<std::vector<Expr>>& formals, const std::vector<Expr>& formulas) { d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end()); @@ -992,7 +1144,7 @@ const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const return d_funcs; } -const std::vector<std::vector<Expr> >& DefineFunctionRecCommand::getFormals() +const std::vector<std::vector<Expr>>& DefineFunctionRecCommand::getFormals() const { return d_formals; @@ -1026,7 +1178,7 @@ Command* DefineFunctionRecCommand::exportTo( exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED); funcs.push_back(func); } - std::vector<std::vector<Expr> > formals; + std::vector<std::vector<Expr>> formals; for (unsigned i = 0, size = d_formals.size(); i < size; i++) { std::vector<Expr> formals_c; @@ -1055,7 +1207,9 @@ std::string DefineFunctionRecCommand::getCommandName() const return "define-fun-rec"; } -/* class SetUserAttribute */ +/* -------------------------------------------------------------------------- */ +/* class SetUserAttribute */ +/* -------------------------------------------------------------------------- */ SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, @@ -1122,7 +1276,9 @@ std::string SetUserAttributeCommand::getCommandName() const return "set-user-attribute"; } -/* class SimplifyCommand */ +/* -------------------------------------------------------------------------- */ +/* class SimplifyCommand */ +/* -------------------------------------------------------------------------- */ SimplifyCommand::SimplifyCommand(Expr term) : d_term(term) {} Expr SimplifyCommand::getTerm() const { return d_term; } @@ -1173,7 +1329,10 @@ Command* SimplifyCommand::clone() const } std::string SimplifyCommand::getCommandName() const { return "simplify"; } -/* class ExpandDefinitionsCommand */ + +/* -------------------------------------------------------------------------- */ +/* class ExpandDefinitionsCommand */ +/* -------------------------------------------------------------------------- */ ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) : d_term(term) {} Expr ExpandDefinitionsCommand::getTerm() const { return d_term; } @@ -1218,7 +1377,9 @@ std::string ExpandDefinitionsCommand::getCommandName() const return "expand-definitions"; } -/* class GetValueCommand */ +/* -------------------------------------------------------------------------- */ +/* class GetValueCommand */ +/* -------------------------------------------------------------------------- */ GetValueCommand::GetValueCommand(Expr term) : d_terms() { @@ -1240,15 +1401,13 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) vector<Expr> result; ExprManager* em = smtEngine->getExprManager(); NodeManager* nm = NodeManager::fromExprManager(em); - for (std::vector<Expr>::const_iterator i = d_terms.begin(); - i != d_terms.end(); - ++i) + for (const Expr& e : d_terms) { - Assert(nm == NodeManager::fromExprManager((*i).getExprManager())); + Assert(nm == NodeManager::fromExprManager(e.getExprManager())); smt::SmtScope scope(smtEngine); Node request = Node::fromExpr( - options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i); - Node value = Node::fromExpr(smtEngine->getValue(*i)); + options::expandDefinitions() ? smtEngine->expandDefinitions(e) : e); + Node value = Node::fromExpr(smtEngine->getValue(e)); if (value.getType().isInteger() && request.getType() == nm->realType()) { // Need to wrap in special marker so that output printers know this @@ -1314,14 +1473,17 @@ Command* GetValueCommand::clone() const } std::string GetValueCommand::getCommandName() const { return "get-value"; } -/* class GetAssignmentCommand */ + +/* -------------------------------------------------------------------------- */ +/* class GetAssignmentCommand */ +/* -------------------------------------------------------------------------- */ GetAssignmentCommand::GetAssignmentCommand() {} void GetAssignmentCommand::invoke(SmtEngine* smtEngine) { try { - std::vector<std::pair<Expr,Expr>> assignments = smtEngine->getAssignment(); + std::vector<std::pair<Expr, Expr>> assignments = smtEngine->getAssignment(); vector<SExpr> sexprs; for (const auto& p : assignments) { @@ -1388,7 +1550,9 @@ std::string GetAssignmentCommand::getCommandName() const return "get-assignment"; } -/* class GetModelCommand */ +/* -------------------------------------------------------------------------- */ +/* class GetModelCommand */ +/* -------------------------------------------------------------------------- */ GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {} void GetModelCommand::invoke(SmtEngine* smtEngine) @@ -1449,7 +1613,10 @@ Command* GetModelCommand::clone() const } std::string GetModelCommand::getCommandName() const { return "get-model"; } -/* class GetProofCommand */ + +/* -------------------------------------------------------------------------- */ +/* class GetProofCommand */ +/* -------------------------------------------------------------------------- */ GetProofCommand::GetProofCommand() : d_smtEngine(nullptr), d_result(nullptr) {} void GetProofCommand::invoke(SmtEngine* smtEngine) @@ -1506,7 +1673,10 @@ Command* GetProofCommand::clone() const } std::string GetProofCommand::getCommandName() const { return "get-proof"; } -/* class GetInstantiationsCommand */ + +/* -------------------------------------------------------------------------- */ +/* class GetInstantiationsCommand */ +/* -------------------------------------------------------------------------- */ GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {} void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) @@ -1557,7 +1727,9 @@ std::string GetInstantiationsCommand::getCommandName() const return "get-instantiations"; } -/* class GetSynthSolutionCommand */ +/* -------------------------------------------------------------------------- */ +/* class GetSynthSolutionCommand */ +/* -------------------------------------------------------------------------- */ GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {} void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) @@ -1606,7 +1778,9 @@ std::string GetSynthSolutionCommand::getCommandName() const return "get-instantiations"; } -/* class GetQuantifierEliminationCommand */ +/* -------------------------------------------------------------------------- */ +/* class GetQuantifierEliminationCommand */ +/* -------------------------------------------------------------------------- */ GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() : d_expr() {} GetQuantifierEliminationCommand::GetQuantifierEliminationCommand( @@ -1666,7 +1840,9 @@ std::string GetQuantifierEliminationCommand::getCommandName() const return d_doFull ? "get-qe" : "get-qe-disjunct"; } -/* class GetUnsatCoreCommand */ +/* -------------------------------------------------------------------------- */ +/* class GetUnsatCoreCommand */ +/* -------------------------------------------------------------------------- */ GetUnsatCoreCommand::GetUnsatCoreCommand() {} void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) @@ -1725,7 +1901,9 @@ std::string GetUnsatCoreCommand::getCommandName() const return "get-unsat-core"; } -/* class GetAssertionsCommand */ +/* -------------------------------------------------------------------------- */ +/* class GetAssertionsCommand */ +/* -------------------------------------------------------------------------- */ GetAssertionsCommand::GetAssertionsCommand() {} void GetAssertionsCommand::invoke(SmtEngine* smtEngine) @@ -1780,7 +1958,9 @@ std::string GetAssertionsCommand::getCommandName() const return "get-assertions"; } -/* class SetBenchmarkStatusCommand */ +/* -------------------------------------------------------------------------- */ +/* class SetBenchmarkStatusCommand */ +/* -------------------------------------------------------------------------- */ SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : d_status(status) @@ -1824,7 +2004,9 @@ std::string SetBenchmarkStatusCommand::getCommandName() const return "set-info"; } -/* class SetBenchmarkLogicCommand */ +/* -------------------------------------------------------------------------- */ +/* class SetBenchmarkLogicCommand */ +/* -------------------------------------------------------------------------- */ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) : d_logic(logic) @@ -1861,7 +2043,9 @@ std::string SetBenchmarkLogicCommand::getCommandName() const return "set-logic"; } -/* class SetInfoCommand */ +/* -------------------------------------------------------------------------- */ +/* class SetInfoCommand */ +/* -------------------------------------------------------------------------- */ SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) : d_flag(flag), d_sexpr(sexpr) @@ -1900,7 +2084,10 @@ Command* SetInfoCommand::clone() const } std::string SetInfoCommand::getCommandName() const { return "set-info"; } -/* class GetInfoCommand */ + +/* -------------------------------------------------------------------------- */ +/* class GetInfoCommand */ +/* -------------------------------------------------------------------------- */ GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {} std::string GetInfoCommand::getFlag() const { return d_flag; } @@ -1959,7 +2146,10 @@ Command* GetInfoCommand::clone() const } std::string GetInfoCommand::getCommandName() const { return "get-info"; } -/* class SetOptionCommand */ + +/* -------------------------------------------------------------------------- */ +/* class SetOptionCommand */ +/* -------------------------------------------------------------------------- */ SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) : d_flag(flag), d_sexpr(sexpr) @@ -1997,7 +2187,10 @@ Command* SetOptionCommand::clone() const } std::string SetOptionCommand::getCommandName() const { return "set-option"; } -/* class GetOptionCommand */ + +/* -------------------------------------------------------------------------- */ +/* class GetOptionCommand */ +/* -------------------------------------------------------------------------- */ GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {} std::string GetOptionCommand::getFlag() const { return d_flag; } @@ -2048,7 +2241,10 @@ Command* GetOptionCommand::clone() const } std::string GetOptionCommand::getCommandName() const { return "get-option"; } -/* class SetExpressionNameCommand */ + +/* -------------------------------------------------------------------------- */ +/* class SetExpressionNameCommand */ +/* -------------------------------------------------------------------------- */ SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name) : d_expr(expr), d_name(name) @@ -2080,7 +2276,9 @@ std::string SetExpressionNameCommand::getCommandName() const return "set-expr-name"; } -/* class DatatypeDeclarationCommand */ +/* -------------------------------------------------------------------------- */ +/* class DatatypeDeclarationCommand */ +/* -------------------------------------------------------------------------- */ DatatypeDeclarationCommand::DatatypeDeclarationCommand( const DatatypeType& datatype) @@ -2123,7 +2321,9 @@ std::string DatatypeDeclarationCommand::getCommandName() const return "declare-datatypes"; } -/* class RewriteRuleCommand */ +/* -------------------------------------------------------------------------- */ +/* class RewriteRuleCommand */ +/* -------------------------------------------------------------------------- */ RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, const std::vector<Expr>& guards, @@ -2235,7 +2435,9 @@ std::string RewriteRuleCommand::getCommandName() const return "rewrite-rule"; } -/* class PropagateRuleCommand */ +/* -------------------------------------------------------------------------- */ +/* class PropagateRuleCommand */ +/* -------------------------------------------------------------------------- */ PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, const std::vector<Expr>& guards, @@ -2366,20 +2568,4 @@ std::string PropagateRuleCommand::getCommandName() const { return "propagate-rule"; } - -/* output stream insertion operator for benchmark statuses */ -std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) -{ - switch (status) - { - case SMT_SATISFIABLE: return out << "sat"; - - case SMT_UNSATISFIABLE: return out << "unsat"; - - case SMT_UNKNOWN: return out << "unknown"; - - default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]"; - } -} - -} /* CVC4 namespace */ +} // namespace CVC4 |