From d51c8347a3c6bf7857c474bd3493377f9fed58e5 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 5 Mar 2018 14:05:26 -0800 Subject: Add support for check-sat-assuming. (#1637) This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input formula) under assumption (not (or a b)). --- src/smt/command.cpp | 334 ++++++++++++++++++++++++++++++++++++++----------- src/smt/command.h | 45 +++++-- src/smt/smt_engine.cpp | 116 ++++++++++++----- src/smt/smt_engine.h | 14 ++- 4 files changed, 392 insertions(+), 117 deletions(-) (limited to 'src/smt') 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& 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& 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 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& formals, Expr formula) @@ -979,7 +1131,7 @@ DefineFunctionRecCommand::DefineFunctionRecCommand( DefineFunctionRecCommand::DefineFunctionRecCommand( const std::vector& funcs, - const std::vector >& formals, + const std::vector>& formals, const std::vector& formulas) { d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end()); @@ -992,7 +1144,7 @@ const std::vector& DefineFunctionRecCommand::getFunctions() const return d_funcs; } -const std::vector >& DefineFunctionRecCommand::getFormals() +const std::vector>& 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 > formals; + std::vector> formals; for (unsigned i = 0, size = d_formals.size(); i < size; i++) { std::vector 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 result; ExprManager* em = smtEngine->getExprManager(); NodeManager* nm = NodeManager::fromExprManager(em); - for (std::vector::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> assignments = smtEngine->getAssignment(); + std::vector> assignments = smtEngine->getAssignment(); vector 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& vars, const std::vector& guards, @@ -2235,7 +2435,9 @@ std::string RewriteRuleCommand::getCommandName() const return "rewrite-rule"; } -/* class PropagateRuleCommand */ +/* -------------------------------------------------------------------------- */ +/* class PropagateRuleCommand */ +/* -------------------------------------------------------------------------- */ PropagateRuleCommand::PropagateRuleCommand(const std::vector& vars, const std::vector& 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 diff --git a/src/smt/command.h b/src/smt/command.h index 9573e1c22..19bf9fddd 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -2,9 +2,9 @@ /*! \file command.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Andres Noetzli + ** Tim King, Morgan Deters, Andrew Reynolds ** 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 @@ -544,13 +544,12 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command const std::string d_str_value; }; /* class SetUserAttributeCommand */ +/** + * The command when parsing check-sat. + * This command will check satisfiability of the input formula. + */ class CVC4_PUBLIC CheckSatCommand : public Command { - protected: - Expr d_expr; - Result d_result; - bool d_inUnsatCore; - public: CheckSatCommand(); CheckSatCommand(const Expr& expr, bool inUnsatCore = true); @@ -563,8 +562,40 @@ class CVC4_PUBLIC CheckSatCommand : public Command ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; + + private: + Expr d_expr; + Result d_result; + bool d_inUnsatCore; }; /* class CheckSatCommand */ +/** + * The command when parsing check-sat-assuming. + * This command will assume a set of formulas and check satisfiability of the + * input formula under these assumptions. + */ +class CVC4_PUBLIC CheckSatAssumingCommand : public Command +{ + public: + CheckSatAssumingCommand(Expr term); + CheckSatAssumingCommand(const std::vector& terms, + bool inUnsatCore = true); + + const std::vector& getTerms() const; + Result getResult() const; + void invoke(SmtEngine* smtEngine) override; + void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) override; + Command* clone() const override; + std::string getCommandName() const override; + + private: + std::vector d_terms; + Result d_result; + bool d_inUnsatCore; +}; /* class CheckSatAssumingCommand */ + class CVC4_PUBLIC QueryCommand : public Command { protected: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 19236f881..6e90ab152 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2,9 +2,9 @@ /*! \file smt_engine.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds + ** Morgan Deters, Andrew Reynolds, Tim King ** 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 @@ -4683,22 +4683,46 @@ void SmtEngine::ensureBoolean(const Expr& e) Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) { return checkSatisfiability(ex, inUnsatCore, false); -} /* SmtEngine::checkSat() */ +} + +Result SmtEngine::checkSat(const vector& exprs, bool inUnsatCore) +{ + return checkSatisfiability(exprs, inUnsatCore, false); +} Result SmtEngine::query(const Expr& ex, bool inUnsatCore) { Assert(!ex.isNull()); return checkSatisfiability(ex, inUnsatCore, true); -} /* SmtEngine::query() */ +} -Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQuery) { - try { - Assert(ex.isNull() || ex.getExprManager() == d_exprManager); +Result SmtEngine::query(const vector& exprs, bool inUnsatCore) +{ + return checkSatisfiability(exprs, inUnsatCore, true); +} + +Result SmtEngine::checkSatisfiability(const Expr& expr, + bool inUnsatCore, + bool isQuery) +{ + return checkSatisfiability( + expr.isNull() ? vector() : vector{expr}, + inUnsatCore, + isQuery); +} + +Result SmtEngine::checkSatisfiability(const vector& exprs, + bool inUnsatCore, + bool isQuery) +{ + try + { SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << ex << ")" << endl; + Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" + << exprs << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { throw ModalException("Cannot make multiple queries unless " @@ -4706,45 +4730,64 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ "(try --incremental)"); } - Expr e; - if(!ex.isNull()) { - // Substitute out any abstract values in ex. - e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - // Ensure expr is type-checked at this point. - ensureBoolean(e); - } - // check to see if a postsolve() is pending if(d_needPostsolve) { d_theoryEngine->postsolve(); d_needPostsolve = false; } - // Note that a query has been made d_queryMade = true; - // reset global negation d_globalNegation = false; bool didInternalPush = false; - // Add the formula - if(!e.isNull()) { - // Push the context + + vector t_exprs; + if (isQuery) + { + size_t size = exprs.size(); + if (size > 1) + { + /* Assume: not (BIGAND exprs) */ + t_exprs.push_back(d_exprManager->mkExpr(kind::AND, exprs).notExpr()); + } + else if (size == 1) + { + /* Assume: not expr */ + t_exprs.push_back(exprs[0].notExpr()); + } + } + else + { + /* Assume: BIGAND exprs */ + t_exprs = exprs; + } + + Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + for (Expr e : t_exprs) + { + // Substitute out any abstract values in ex. + e = d_private->substituteAbstractValues(Node::fromExpr(e)).toExpr(); + Assert(e.getExprManager() == d_exprManager); + // Ensure expr is type-checked at this point. + ensureBoolean(e); + + /* Add assumption */ internalPush(); didInternalPush = true; - d_problemExtended = true; - Expr ea = isQuery ? e.notExpr() : e; - if(d_assertionList != NULL) { - d_assertionList->push_back(ea); + if (d_assertionList != NULL) + { + d_assertionList->push_back(e); } - d_private->addFormula(ea.getNode(), inUnsatCore); + d_private->addFormula(e.getNode(), inUnsatCore); } - Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult(); - if ( ( options::solveRealAsInt() || options::solveIntAsBV() > 0 ) && r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) + && r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); } // flipped if we did a global negation @@ -4773,12 +4816,16 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ d_needPostsolve = true; // Dump the query if requested - if(Dump.isOn("benchmark")) { + if (Dump.isOn("benchmark")) + { // the expr already got dumped out if assertion-dumping is on - if( isQuery ){ - Dump("benchmark") << QueryCommand(ex); - }else{ - Dump("benchmark") << CheckSatCommand(ex); + if (isQuery && exprs.size() == 1) + { + Dump("benchmark") << QueryCommand(exprs[0]); + } + else + { + Dump("benchmark") << CheckSatAssumingCommand(t_exprs, inUnsatCore); } } @@ -4793,7 +4840,8 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ d_problemExtended = false; - Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << e << ") => " << r << endl; + Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" + << exprs << ") => " << r << endl; // Check that SAT results generate a model correctly. if(options::checkModels()) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 16cf90de1..bba6b1cef 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -400,7 +400,12 @@ class CVC4_PUBLIC SmtEngine { SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED; //check satisfiability (for query and check-sat) - Result checkSatisfiability(const Expr& e, bool inUnsatCore, bool isQuery); + Result checkSatisfiability(const Expr& expr, + bool inUnsatCore, + bool isQuery); + Result checkSatisfiability(const std::vector& exprs, + bool inUnsatCore, + bool isQuery); /** * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is @@ -535,7 +540,10 @@ class CVC4_PUBLIC SmtEngine { * of assertions by asserting the query expression's negation and * calling check(). Returns valid, invalid, or unknown result. */ - Result query(const Expr& e, bool inUnsatCore = true) /* throw(Exception) */; + Result query(const Expr& e = Expr(), + bool inUnsatCore = true) /* throw(Exception) */; + Result query(const std::vector& exprs, + bool inUnsatCore = true) /* throw(Exception) */; /** * Assert a formula (if provided) to the current context and call @@ -543,6 +551,8 @@ class CVC4_PUBLIC SmtEngine { */ Result checkSat(const Expr& e = Expr(), bool inUnsatCore = true) /* throw(Exception) */; + Result checkSat(const std::vector& exprs, + bool inUnsatCore = true) /* throw(Exception) */; /** * Assert a synthesis conjecture to the current context and call -- cgit v1.2.3