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
| /* 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); }
}
cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs));
}
- // GET_UNSAT_ASSUMPTIONS
;
extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
| 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
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';
|| tryToStream<GetAssignmentCommand>(out, c)
|| tryToStream<GetAssertionsCommand>(out, c)
|| tryToStream<GetProofCommand>(out, c)
+ || tryToStream<GetUnsatAssumptionsCommand>(out, c)
|| tryToStream<GetUnsatCoreCommand>(out, c)
|| tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant)
|| tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant)
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)";
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<Expr> 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 */
/* -------------------------------------------------------------------------- */
std::string getCommandName() const override;
}; /* class GetQuantifierEliminationCommand */
+class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
+{
+ public:
+ GetUnsatAssumptionsCommand();
+ void invoke(SmtEngine* smtEngine) override;
+ std::vector<Expr> 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<Expr> d_result;
+}; /* class GetUnsatAssumptionsCommand */
+
class CVC4_PUBLIC GetUnsatCoreCommand : public Command
{
public:
}
}
+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);
}
}
-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<Expr>& exprs, bool inUnsatCore)
+Result SmtEngine::checkSat(const vector<Expr>& 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<Expr>& exprs, bool inUnsatCore)
+Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore)
{
- return checkSatisfiability(exprs, inUnsatCore, true);
+ return checkSatisfiability(assumptions, inUnsatCore, true);
}
Result SmtEngine::checkSatisfiability(const Expr& expr,
isQuery);
}
-Result SmtEngine::checkSatisfiability(const vector<Expr>& exprs,
+Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
bool inUnsatCore,
bool isQuery)
{
doPendingPops();
Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "("
- << exprs << ")" << endl;
+ << assumptions << ")" << endl;
if(d_queryMade && !options::incrementalSolving()) {
throw ModalException("Cannot make multiple queries unless "
bool didInternalPush = false;
- vector<Expr> 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();
/* Add assumption */
internalPush();
didInternalPush = true;
- d_problemExtended = true;
if (d_assertionList != NULL)
{
d_assertionList->push_back(e);
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);
}
}
// 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()) {
}
}
+vector<Expr> 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<Expr> 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);
// 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();
// 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());
*/
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<Expr> d_assumptions;
+
/**
* List of items for which to retrieve values using getAssignment().
*/
*/
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()
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<Expr>& exprs,
+ Result checkSatisfiability(const std::vector<Expr>& assumptions,
bool inUnsatCore,
bool isQuery);
* 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<Expr>& exprs,
+ Result query(const std::vector<Expr>& 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<Expr>& exprs,
+ Result checkSat(const std::vector<Expr>& 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<Expr> getUnsatAssumptions(void);
+
/**
* Assert a synthesis conjecture to the current context and call
* check(). Returns sat, unsat, or unknown result.
; 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_)]
projects / cvc5.git / commitdiff