summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/smt_options3
-rw-r--r--src/parser/smt2/Smt2.g8
-rw-r--r--src/printer/smt2/smt2_printer.cpp6
-rw-r--r--src/smt/command.cpp61
-rw-r--r--src/smt/command.h15
-rw-r--r--src/smt/smt_engine.cpp94
-rw-r--r--src/smt/smt_engine.h39
-rw-r--r--test/regress/regress0/push-pop/bug821-check_sat_assuming.smt215
8 files changed, 201 insertions, 40 deletions
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<CVC4::Command>* 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<CVC4::Command>* cmd]
}
cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs));
}
- // GET_UNSAT_ASSUMPTIONS
;
extendedCommand[std::unique_ptr<CVC4::Command>* 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<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)
@@ -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
@@ -1841,6 +1841,67 @@ std::string GetQuantifierEliminationCommand::getCommandName() const
}
/* -------------------------------------------------------------------------- */
+/* 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 */
/* -------------------------------------------------------------------------- */
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<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:
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<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,
@@ -4724,7 +4730,7 @@ 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)
{
@@ -4735,7 +4741,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& 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<Expr>& exprs,
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();
@@ -4788,7 +4796,6 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& 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<Expr>& 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<Expr>& 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<Expr>& exprs,
}
}
+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);
@@ -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
@@ -159,6 +159,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<Expr> d_assumptions;
+
+ /**
* List of items for which to retrieve values using getAssignment().
*/
AssignmentSet* d_assignments;
@@ -318,6 +326,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<Expr>& exprs,
+ Result checkSatisfiability(const std::vector<Expr>& assumptions,
bool inUnsatCore,
bool isQuery);
@@ -540,21 +555,33 @@ 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<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.
*/
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_)]
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback