From: Aina Niemetz Date: Mon, 5 Mar 2018 22:05:26 +0000 (-0800) Subject: Add support for check-sat-assuming. (#1637) X-Git-Tag: cvc5-1.0.0~5254 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d51c8347a3c6bf7857c474bd3493377f9fed58e5;p=cvc5.git 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)). --- diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 90b69b10a..a245d4890 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -2,9 +2,9 @@ /*! \file bitvectors.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Morgan Deters, Paul Meng + ** Liana Hadarean, 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 @@ -107,5 +107,10 @@ int main() { cout << " Expect valid. " << endl; cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl; + Expr x_neq_x = em.mkExpr(kind::EQUAL, x, x).notExpr(); + std::vector v{new_x_eq_new_x_, x_neq_x}; + cout << " Querying: " << v << endl; + cout << " Expect invalid. " << endl; + cout << " CVC4: " << smt.query(v) << endl; return 0; } diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 6bcd15027..010b36e94 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Kshitij Bansal, Dejan Jovanovic ** 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 diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 8cc87cfff..cb4534c08 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -2,9 +2,9 @@ /*! \file expr_template.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway + ** Morgan Deters, Dejan Jovanovic, 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 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b9a2a8805..889352299 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** 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 @@ -431,7 +431,7 @@ command [std::unique_ptr* cmd] } } | /* check-sat */ - CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } + CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support check-sat command."); } @@ -446,6 +446,16 @@ command [std::unique_ptr* cmd] | { expr = MK_CONST(bool(true)); } ) { cmd->reset(new CheckSatCommand(expr)); } + | /* check-sat-assuming */ + CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); } + ( LPAREN_TOK termList[terms,expr] RPAREN_TOK + { cmd->reset(new CheckSatAssumingCommand(terms)); } + | ~LPAREN_TOK + { PARSER_STATE->parseError("The check-sat-assuming command expects a " + "list of terms. Perhaps you forgot a pair of " + "parentheses?"); + } + ) | /* get-assertions */ GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new GetAssertionsCommand()); } @@ -1276,7 +1286,6 @@ smt25Command[std::unique_ptr* cmd] } cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs)); } - // CHECK_SAT_ASSUMING still being discussed // GET_UNSAT_ASSUMPTIONS ; @@ -1713,7 +1722,8 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] // } | symbol[s,CHECK_NONE,SYM_SORT] { sexpr = SExpr(SExpr::Keyword(s)); } - | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK + | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK + | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK @@ -3064,7 +3074,8 @@ selector[CVC4::DatatypeConstructor& ctor] // Base SMT-LIB tokens ASSERT_TOK : 'assert'; -CHECKSAT_TOK : 'check-sat'; +CHECK_SAT_TOK : 'check-sat'; +CHECK_SAT_ASSUMING_TOK : 'check-sat-assuming'; DECLARE_FUN_TOK : 'declare-fun'; DECLARE_SORT_TOK : 'declare-sort'; DEFINE_FUN_TOK : 'define-fun'; diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index be95c947d..31f9b9c41 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -147,6 +147,7 @@ void AstPrinter::toStream(std::ostream& out, tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || + tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || @@ -237,6 +238,14 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) } } +static void toStream(std::ostream& out, const CheckSatAssumingCommand* c) +{ + const vector& terms = c->getTerms(); + out << "CheckSatAssuming( << "; + copy(terms.begin(), terms.end(), ostream_iterator(out, ", ")); + out << ">> )"; +} + static void toStream(std::ostream& out, const QueryCommand* c) { out << "Query(" << c->getExpr() << ')'; @@ -333,7 +342,7 @@ static void toStream(std::ostream& out, const GetValueCommand* c) out << "GetValue( << "; const vector& terms = c->getTerms(); copy(terms.begin(), terms.end(), ostream_iterator(out, ", ")); - out << " >> )"; + out << ">> )"; } static void toStream(std::ostream& out, const GetModelCommand* c) diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 27105c3b4..d778ccc2b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -2,9 +2,9 @@ /*! \file cvc_printer.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds + ** Morgan Deters, Tim King, Dejan Jovanovic ** 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 @@ -955,6 +955,7 @@ void CvcPrinter::toStream(std::ostream& out, tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || @@ -1159,6 +1160,31 @@ static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode) } } +static void toStream(std::ostream& out, + const CheckSatAssumingCommand* c, + bool cvc3Mode) +{ + const vector& exprs = c->getTerms(); + if (cvc3Mode) + { + out << "PUSH; "; + } + out << "CHECKSAT"; + if (exprs.size() > 0) + { + out << " " << exprs[0]; + for (size_t i = 1, n = exprs.size(); i < n; ++i) + { + out << " AND " << exprs[i]; + } + } + out << ";"; + if (cvc3Mode) + { + out << " POP;"; + } +} + static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode) { Expr e = c->getExpr(); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e06f8c062..e025c64f1 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -2,9 +2,9 @@ /*! \file smt2_printer.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Martin Brain + ** 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 @@ -1191,7 +1191,8 @@ void Smt2Printer::toStream(std::ostream& out, if (tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) - || tryToStream(out, c) + || tryToStream(out, c) + || tryToStream(out, c, d_variant) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) @@ -1511,14 +1512,29 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) } } -static void toStream(std::ostream& out, const QueryCommand* c) +static void toStream(std::ostream& out, const CheckSatAssumingCommand* c) +{ + out << "(check-sat-assuming ( "; + const vector& terms = c->getTerms(); + copy(terms.begin(), terms.end(), ostream_iterator(out, " ")); + out << "))"; +} + +static void toStream(std::ostream& out, const QueryCommand* c, Variant v) { Expr e = c->getExpr(); if(!e.isNull()) { - out << PushCommand() << endl - << AssertCommand(BooleanSimplification::negate(e)) << endl - << CheckSatCommand() << endl - << PopCommand(); + if (v == smt2_0_variant) + { + out << PushCommand() << endl + << AssertCommand(BooleanSimplification::negate(e)) << endl + << CheckSatCommand() << endl + << PopCommand(); + } + else + { + out << CheckSatAssumingCommand(e.notExpr()) << endl; + } } else { out << "(check-sat)"; } 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 diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 06225dfb6..b78c48549 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -39,7 +39,8 @@ BUG_TESTS = \ inc-define.smt2 \ bug691.smt2 \ simple_unsat_cores.smt2 \ - bug821.smt2 + bug821.smt2 \ + bug821-check_sat_assuming.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 b/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 new file mode 100644 index 000000000..50e440689 --- /dev/null +++ b/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +(set-logic UF) +(declare-fun _substvar_4_ () Bool) +(check-sat-assuming (_substvar_4_ _substvar_4_)) +(check-sat-assuming (_substvar_4_ false)) +(check-sat-assuming ((= _substvar_4_ _substvar_4_)))