From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 15 Aug 2018 16:37:00 +0000 (-0700)
Subject: Fix dumping of get-unsat-assumptions (#2302)
X-Git-Tag: cvc5-1.0.0~4784
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e09be1045fc6cc8c5373f9eb96137add66b8d5d5;p=cvc5.git

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()`.
---

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
@@ -283,6 +283,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.
    */