diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-15 09:37:00 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-15 09:37:00 -0700 |
commit | e09be1045fc6cc8c5373f9eb96137add66b8d5d5 (patch) | |
tree | b7e7b133524287aba7fda1cdda195df039f46e70 | |
parent | 4a3bde6335f676a28f4aa5f872c213e0ec8bbaa7 (diff) |
Fix dumping of get-unsat-assumptions (#2302)
When dumping a `get-unsat-assumptions` command, CVC4 was instead dumping
two `get-unsat-cores` commands. This commit splits
`SmtEngine::getUnsatCores()` into a part that does the dumping and an
internal part that actually gets the unsat core without dumping.
`SmtEngine::getUnsatAssumptions()` now calls the internal version to
avoid the redundant dumping of a `get-unsat-cores` command and changes
the command that gets dumped in `SmtEngine::getUnsatAssumptions()`.
-rw-r--r-- | src/smt/smt_engine.cpp | 47 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 8 |
2 files changed, 36 insertions, 19 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bcb5c58b4..38f6a2d5e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4826,9 +4826,9 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void) finalOptionsAreSet(); if (Dump.isOn("benchmark")) { - Dump("benchmark") << GetUnsatCoreCommand(); + Dump("benchmark") << GetUnsatAssumptionsCommand(); } - UnsatCore core = getUnsatCore(); + UnsatCore core = getUnsatCoreInternal(); vector<Expr> res; for (const Expr& e : d_assumptions) { @@ -5191,6 +5191,31 @@ Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } +UnsatCore SmtEngine::getUnsatCoreInternal() +{ +#if IS_PROOFS_BUILD + if (!options::unsatCores()) + { + throw ModalException( + "Cannot get an unsat core when produce-unsat-cores option is off."); + } + if (d_status.isNull() || d_status.asSatisfiabilityResult() != Result::UNSAT + || d_problemExtended) + { + throw RecoverableModalException( + "Cannot get an unsat core unless immediately preceded by UNSAT/VALID " + "response."); + } + + d_proofManager->traceUnsatCore(); // just to trigger core creation + return UnsatCore(this, d_proofManager->extractUnsatCore()); +#else /* IS_PROOFS_BUILD */ + throw ModalException( + "This build of CVC4 doesn't have proof support (required for unsat " + "cores)."); +#endif /* IS_PROOFS_BUILD */ +} + void SmtEngine::checkUnsatCore() { Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off"); @@ -5549,23 +5574,7 @@ UnsatCore SmtEngine::getUnsatCore() { if(Dump.isOn("benchmark")) { Dump("benchmark") << GetUnsatCoreCommand(); } -#if IS_PROOFS_BUILD - if(!options::unsatCores()) { - throw ModalException("Cannot get an unsat core when produce-unsat-cores option is off."); - } - if(d_status.isNull() || - d_status.asSatisfiabilityResult() != Result::UNSAT || - d_problemExtended) { - throw RecoverableModalException( - "Cannot get an unsat core unless immediately preceded by UNSAT/VALID " - "response."); - } - - d_proofManager->traceUnsatCore();// just to trigger core creation - return UnsatCore(this, d_proofManager->extractUnsatCore()); -#else /* IS_PROOFS_BUILD */ - throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores)."); -#endif /* IS_PROOFS_BUILD */ + return getUnsatCoreInternal(); } // TODO(#1108): Simplify the error reporting of this method. diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index dc5a5e703..599087cb0 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -284,6 +284,14 @@ class CVC4_PUBLIC SmtEngine { void checkProof(); /** + * Internal method to get an unsatisfiable core (only if immediately preceded + * by an UNSAT or VALID query). Only permitted if CVC4 was built with + * unsat-core support and produce-unsat-cores is on. Does not dump the + * command. + */ + UnsatCore getUnsatCoreInternal(); + + /** * Check that an unsatisfiable core is indeed unsatisfiable. */ void checkUnsatCore(); |