From: Aina Niemetz Date: Fri, 9 Mar 2018 19:40:59 +0000 (-0800) Subject: Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653) X-Git-Tag: cvc5-1.0.0~5241 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6085d9b70beb9a2be5a26a3c085b4f1a1758410;p=cvc5.git Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653) --- diff --git a/src/options/smt_options b/src/options/smt_options index 72189ea13..811cc5a71 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -54,6 +54,9 @@ option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-uns option dumpUnsatCoresFull dump-unsat-cores-full --dump-unsat-cores-full bool :default false :link --dump-unsat-cores :link-smt dump-unsat-cores :notify notifyBeforeSearch dump the full unsat core, including unlabeled assertions +option unsatAssumptions produce-unsat-assumptions --produce-unsat-assumptions bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate proofEnabledBuild :notify notifyBeforeSearch + turn on unsat assumptions generation + option checkSynthSol --check-synth-sol bool :default false checks whether produced solutions to functions-to-synthesize satisfy the conjecture diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 889352299..2c26c824f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -462,6 +462,9 @@ command [std::unique_ptr* cmd] | /* get-proof */ GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new GetProofCommand()); } + | /* get-unsat-assumptions */ + GET_UNSAT_ASSUMPTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { cmd->reset(new GetUnsatAssumptionsCommand); } | /* get-unsat-core */ GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new GetUnsatCoreCommand); } @@ -1286,7 +1289,6 @@ smt25Command[std::unique_ptr* cmd] } cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs)); } - // GET_UNSAT_ASSUMPTIONS ; extendedCommand[std::unique_ptr* cmd] @@ -1726,7 +1728,8 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] | 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 + | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_ASSUMPTIONS_TOK + | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK @@ -3086,6 +3089,7 @@ GET_VALUE_TOK : 'get-value'; GET_ASSIGNMENT_TOK : 'get-assignment'; GET_ASSERTIONS_TOK : 'get-assertions'; GET_PROOF_TOK : 'get-proof'; +GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions'; GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset'; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e025c64f1..8c9680a74 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1210,6 +1210,7 @@ void Smt2Printer::toStream(std::ostream& out, || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) + || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c, d_variant) || tryToStream(out, c, d_variant) @@ -1803,6 +1804,11 @@ static void toStream(std::ostream& out, const GetProofCommand* c) out << "(get-proof)"; } +static void toStream(std::ostream& out, const GetUnsatAssumptionsCommand* c) +{ + out << "(get-unsat-assumptions)"; +} + static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) { out << "(get-unsat-core)"; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index e61ea868f..c77c4ed02 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1840,6 +1840,67 @@ std::string GetQuantifierEliminationCommand::getCommandName() const return d_doFull ? "get-qe" : "get-qe-disjunct"; } +/* -------------------------------------------------------------------------- */ +/* class GetUnsatAssumptionsCommand */ +/* -------------------------------------------------------------------------- */ + +GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {} + +void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine) +{ + try + { + d_result = smtEngine->getUnsatAssumptions(); + d_commandStatus = CommandSuccess::instance(); + } + catch (RecoverableModalException& e) + { + d_commandStatus = new CommandRecoverableFailure(e.what()); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +std::vector GetUnsatAssumptionsCommand::getResult() const +{ + return d_result; +} + +void GetUnsatAssumptionsCommand::printResult(std::ostream& out, + uint32_t verbosity) const +{ + if (!ok()) + { + this->Command::printResult(out, verbosity); + } + else + { + out << d_result << endl; + } +} + +Command* GetUnsatAssumptionsCommand::exportTo( + ExprManager* exprManager, ExprManagerMapCollection& variableMap) +{ + GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand; + c->d_result = d_result; + return c; +} + +Command* GetUnsatAssumptionsCommand::clone() const +{ + GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand; + c->d_result = d_result; + return c; +} + +std::string GetUnsatAssumptionsCommand::getCommandName() const +{ + return "get-unsat-assumptions"; +} + /* -------------------------------------------------------------------------- */ /* class GetUnsatCoreCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 19bf9fddd..08f83e7a9 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -809,6 +809,21 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command std::string getCommandName() const override; }; /* class GetQuantifierEliminationCommand */ +class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command +{ + public: + GetUnsatAssumptionsCommand(); + void invoke(SmtEngine* smtEngine) override; + std::vector getResult() const; + 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; + protected: + std::vector d_result; +}; /* class GetUnsatAssumptionsCommand */ + class CVC4_PUBLIC GetUnsatCoreCommand : public Command { public: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ae00b4caf..d3489b301 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2144,6 +2144,12 @@ void SmtEngine::setDefaults() { } } +void SmtEngine::setProblemExtended(bool value) +{ + d_problemExtended = value; + if (value) { d_assumptions.clear(); } +} + void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) { SmtScope smts(this); @@ -4693,25 +4699,25 @@ void SmtEngine::ensureBoolean(const Expr& e) } } -Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) +Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) { - return checkSatisfiability(ex, inUnsatCore, false); + return checkSatisfiability(assumption, inUnsatCore, false); } -Result SmtEngine::checkSat(const vector& exprs, bool inUnsatCore) +Result SmtEngine::checkSat(const vector& assumptions, bool inUnsatCore) { - return checkSatisfiability(exprs, inUnsatCore, false); + return checkSatisfiability(assumptions, inUnsatCore, false); } -Result SmtEngine::query(const Expr& ex, bool inUnsatCore) +Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) { - Assert(!ex.isNull()); - return checkSatisfiability(ex, inUnsatCore, true); + Assert(!assumption.isNull()); + return checkSatisfiability(assumption, inUnsatCore, true); } -Result SmtEngine::query(const vector& exprs, bool inUnsatCore) +Result SmtEngine::query(const vector& assumptions, bool inUnsatCore) { - return checkSatisfiability(exprs, inUnsatCore, true); + return checkSatisfiability(assumptions, inUnsatCore, true); } Result SmtEngine::checkSatisfiability(const Expr& expr, @@ -4724,7 +4730,7 @@ Result SmtEngine::checkSatisfiability(const Expr& expr, isQuery); } -Result SmtEngine::checkSatisfiability(const vector& exprs, +Result SmtEngine::checkSatisfiability(const vector& assumptions, bool inUnsatCore, bool isQuery) { @@ -4735,7 +4741,7 @@ Result SmtEngine::checkSatisfiability(const vector& exprs, doPendingPops(); Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" - << exprs << ")" << endl; + << assumptions << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { throw ModalException("Cannot make multiple queries unless " @@ -4755,29 +4761,31 @@ Result SmtEngine::checkSatisfiability(const vector& exprs, bool didInternalPush = false; - vector t_exprs; + setProblemExtended(true); + if (isQuery) { - size_t size = exprs.size(); + size_t size = assumptions.size(); if (size > 1) { - /* Assume: not (BIGAND exprs) */ - t_exprs.push_back(d_exprManager->mkExpr(kind::AND, exprs).notExpr()); + /* Assume: not (BIGAND assumptions) */ + d_assumptions.push_back( + d_exprManager->mkExpr(kind::AND, assumptions).notExpr()); } else if (size == 1) { /* Assume: not expr */ - t_exprs.push_back(exprs[0].notExpr()); + d_assumptions.push_back(assumptions[0].notExpr()); } } else { - /* Assume: BIGAND exprs */ - t_exprs = exprs; + /* Assume: BIGAND assumptions */ + d_assumptions = assumptions; } Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - for (Expr e : t_exprs) + for (Expr e : d_assumptions) { // Substitute out any abstract values in ex. e = d_private->substituteAbstractValues(Node::fromExpr(e)).toExpr(); @@ -4788,7 +4796,6 @@ Result SmtEngine::checkSatisfiability(const vector& exprs, /* Add assumption */ internalPush(); didInternalPush = true; - d_problemExtended = true; if (d_assertionList != NULL) { d_assertionList->push_back(e); @@ -4832,13 +4839,14 @@ Result SmtEngine::checkSatisfiability(const vector& exprs, if (Dump.isOn("benchmark")) { // the expr already got dumped out if assertion-dumping is on - if (isQuery && exprs.size() == 1) + if (isQuery && assumptions.size() == 1) { - Dump("benchmark") << QueryCommand(exprs[0]); + Dump("benchmark") << QueryCommand(assumptions[0]); } else { - Dump("benchmark") << CheckSatAssumingCommand(t_exprs, inUnsatCore); + Dump("benchmark") << CheckSatAssumingCommand(d_assumptions, + inUnsatCore); } } @@ -4851,10 +4859,10 @@ Result SmtEngine::checkSatisfiability(const vector& exprs, // Remember the status d_status = r; - d_problemExtended = false; + setProblemExtended(false); Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" - << exprs << ") => " << r << endl; + << assumptions << ") => " << r << endl; // Check that SAT results generate a model correctly. if(options::checkModels()) { @@ -4893,6 +4901,38 @@ Result SmtEngine::checkSatisfiability(const vector& exprs, } } +vector SmtEngine::getUnsatAssumptions(void) +{ + Trace("smt") << "SMT getUnsatAssumptions()" << endl; + SmtScope smts(this); + if (!options::unsatAssumptions()) + { + throw ModalException( + "Cannot get unsat assumptions when produce-unsat-assumptions option " + "is off."); + } + if (d_status.isNull() + || d_status.asSatisfiabilityResult() != Result::UNSAT + || d_problemExtended) + { + throw RecoverableModalException( + "Cannot get unsat assumptions unless immediately preceded by " + "UNSAT/VALID response."); + } + finalOptionsAreSet(); + if (Dump.isOn("benchmark")) + { + Dump("benchmark") << GetUnsatCoreCommand(); + } + UnsatCore core = getUnsatCore(); + vector res; + for (const Expr& e : d_assumptions) + { + if (find(core.begin(), core.end(), e) != core.end()) { res.push_back(e); } + } + return res; +} + Result SmtEngine::checkSynth(const Expr& e) { SmtScope smts(this); @@ -5890,7 +5930,7 @@ void SmtEngine::push() // The problem isn't really "extended" yet, but this disallows // get-model after a push, simplifying our lives somewhat and // staying symmtric with pop. - d_problemExtended = true; + setProblemExtended(true); d_userLevels.push_back(d_userContext->getLevel()); internalPush(); @@ -5924,7 +5964,7 @@ void SmtEngine::pop() { // but also it would be weird to have a legally-executed (get-model) // that only returns a subset of the assignment (because the rest // is no longer in scope!). - d_problemExtended = true; + setProblemExtended(true); AlwaysAssert(d_userContext->getLevel() > 0); AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index bba6b1cef..377888a5a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -158,6 +158,14 @@ class CVC4_PUBLIC SmtEngine { */ AssertionList* d_assertionList; + /** + * The list of assumptions from the previous call to checkSatisfiability. + * Note that if the last call to checkSatisfiability was a validity check, + * i.e., a call to query(a1, ..., an), then d_assumptions contains one single + * assumption ~(a1 AND ... AND an). + */ + std::vector d_assumptions; + /** * List of items for which to retrieve values using getAssignment(). */ @@ -317,6 +325,13 @@ class CVC4_PUBLIC SmtEngine { */ void setDefaults(); + /** + * Sets d_problemExtended to the given value. + * If d_problemExtended is set to true, the list of assumptions from the + * previous call to checkSatisfiability is cleared. + */ + void setProblemExtended(bool value); + /** * Create theory engine, prop engine, decision engine. Called by * finalOptionsAreSet() @@ -400,10 +415,10 @@ class CVC4_PUBLIC SmtEngine { SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED; //check satisfiability (for query and check-sat) - Result checkSatisfiability(const Expr& expr, + Result checkSatisfiability(const Expr& assumption, bool inUnsatCore, bool isQuery); - Result checkSatisfiability(const std::vector& exprs, + Result checkSatisfiability(const std::vector& assumptions, bool inUnsatCore, bool isQuery); @@ -540,20 +555,32 @@ 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 = Expr(), + Result query(const Expr& assumption = Expr(), bool inUnsatCore = true) /* throw(Exception) */; - Result query(const std::vector& exprs, + Result query(const std::vector& assumptions, bool inUnsatCore = true) /* throw(Exception) */; /** * Assert a formula (if provided) to the current context and call * check(). Returns sat, unsat, or unknown result. */ - Result checkSat(const Expr& e = Expr(), + Result checkSat(const Expr& assumption = Expr(), bool inUnsatCore = true) /* throw(Exception) */; - Result checkSat(const std::vector& exprs, + Result checkSat(const std::vector& assumptions, bool inUnsatCore = true) /* throw(Exception) */; + /** + * Returns a set of so-called "failed" assumptions. + * + * The returned set is a subset of the set of assumptions of a previous + * (unsatisfiable) call to checkSatisfiability. Calling checkSatisfiability + * with this set of failed assumptions still produces an unsat answer. + * + * Note that the returned set of failed assumptions is not necessarily + * minimal. + */ + std::vector getUnsatAssumptions(void); + /** * Assert a synthesis conjecture to the current context and call * check(). Returns sat, unsat, or unknown result. diff --git a/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 b/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 index 50e440689..5a01e44f8 100644 --- a/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 +++ b/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 @@ -1,9 +1,14 @@ ; COMMAND-LINE: --incremental -; EXPECT: sat -; EXPECT: unsat -; EXPECT: sat (set-logic UF) +(set-option :produce-unsat-assumptions true) (declare-fun _substvar_4_ () Bool) -(check-sat-assuming (_substvar_4_ _substvar_4_)) +(check-sat-assuming (_substvar_4_ (= _substvar_4_ _substvar_4_))) +; EXPECT: sat (check-sat-assuming (_substvar_4_ false)) -(check-sat-assuming ((= _substvar_4_ _substvar_4_))) +; EXPECT: unsat +(get-unsat-assumptions) +; EXPECT: [false] +(check-sat-assuming ((= _substvar_4_ _substvar_4_) (distinct _substvar_4_ _substvar_4_))) +; EXPECT: unsat +(get-unsat-assumptions) +; EXPECT: [(distinct _substvar_4_ _substvar_4_)]