Add support for minimal unsat cores (#4605)

This commit adds support for computing minimal unsat cores. The
algorithm implemented in this commit is just a trivial deletion-based
algorithm that tries to remove each assertion in the unsat core
individually.

7 files changed, 100 insertions, 2 deletions

diff --git a/NEWS b/NEWS
index 74ee86165..f01643643 100644
--- a/NEWS
+++ b/NEWS
@@ -23,6 +23,7 @@ New Features:
   * Support for `str.indexof_re(s, r, n)`, which returns the index of the first
     occurrence of a regular expression `r` in a string `s` after index `n` or
     -1 if `r` does not match a substring after `n`.
+* A new option to compute minimal unsat cores (`--minimal-unsat-cores`).
 
 Improvements:
 * New API: Added functions to retrieve the heap/nil term when using separation
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 9b5a93486..a97fe572f 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -195,6 +195,14 @@ name   = "SMT Layer"
   help = "Produce unsat cores using solving under assumptions and preprocessing proofs."
 
 [[option]]
+  name       = "minimalUnsatCores"
+  category   = "regular"
+  long       = "minimal-unsat-cores"
+  type       = "bool"
+  default    = "false"
+  help       = "if an unsat core is produced, it is reduced to a minimal unsat core"
+
+[[option]]
   name       = "checkUnsatCores"
   category   = "regular"
   long       = "check-unsat-cores"
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index bb104e98d..d5b3b7929 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -69,7 +69,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.driver.dumpUnsatCores = true;
   }
   if (options::checkUnsatCores() || options::dumpUnsatCores()
-      || options::unsatAssumptions()
+      || options::unsatAssumptions() || options::minimalUnsatCores()
       || options::unsatCoresMode() != options::UnsatCoresMode::OFF)
   {
     opts.smt.unsatCores = true;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9056e7c94..b09fdb4d7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1400,9 +1400,80 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
   std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts);
   std::vector<Node> core;
   d_ucManager->getUnsatCore(pfn, *d_asserts, core);
+  if (options::minimalUnsatCores())
+  {
+    core = reduceUnsatCore(core);
+  }
   return UnsatCore(core);
 }
 
+std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core)
+{
+  Assert(options::unsatCores())
+      << "cannot reduce unsat core if unsat cores are turned off";
+
+  Notice() << "SmtEngine::reduceUnsatCore(): reducing unsat core" << endl;
+  std::unordered_set<Node> removed;
+  for (const Node& skip : core)
+  {
+    std::unique_ptr<SmtEngine> coreChecker;
+    initializeSubsolver(coreChecker);
+    coreChecker->setLogic(getLogicInfo());
+    coreChecker->getOptions().smt.checkUnsatCores = false;
+    // disable all proof options
+    coreChecker->getOptions().smt.produceProofs = false;
+    coreChecker->getOptions().smt.checkProofs = false;
+    coreChecker->getOptions().proof.proofEagerChecking = false;
+
+    for (const Node& ucAssertion : core)
+    {
+      if (ucAssertion != skip && removed.find(ucAssertion) == removed.end())
+      {
+        Node assertionAfterExpansion = expandDefinitions(ucAssertion);
+        coreChecker->assertFormula(assertionAfterExpansion);
+      }
+    }
+    Result r;
+    try
+    {
+      r = coreChecker->checkSat();
+    }
+    catch (...)
+    {
+      throw;
+    }
+
+    if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+    {
+      removed.insert(skip);
+    }
+    else if (r.asSatisfiabilityResult().isUnknown())
+    {
+      Warning() << "SmtEngine::reduceUnsatCore(): could not reduce unsat core "
+                   "due to "
+                   "unknown result.";
+    }
+  }
+
+  if (removed.empty())
+  {
+    return core;
+  }
+  else
+  {
+    std::vector<Node> newUcAssertions;
+    for (const Node& n : core)
+    {
+      if (removed.find(n) == removed.end())
+      {
+        newUcAssertions.push_back(n);
+      }
+    }
+
+    return newUcAssertions;
+  }
+}
+
 void SmtEngine::checkUnsatCore() {
   Assert(d_env->getOptions().smt.unsatCores)
       << "cannot check unsat core if unsat cores are turned off";
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3128257e6..02e5c6b06 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1,6 +1,6 @@
 /******************************************************************************
  * Top contributors (to current version):
- *   Andrew Reynolds, Morgan Deters, Aina Niemetz
+
  *
  * This file is part of the cvc5 project.
  *
@@ -368,6 +368,11 @@ class CVC5_EXPORT SmtEngine
   Result assertFormula(const Node& formula, bool inUnsatCore = true);
 
   /**
+   * Reduce an unsatisfiable core to make it minimal.
+   */
+  std::vector<Node> reduceUnsatCore(const std::vector<Node>& core);
+
+  /**
    * Check if a given (set of) expression(s) is entailed with respect to the
    * current set of assertions. We check this by asserting the negation of
    * the (big AND over the) given (set of) expression(s).
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index db6a7ae48..6ebb91f9e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1649,6 +1649,7 @@ set(regress_1_tests
   regress1/issue5739-rtf-processed.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
+  regress1/minimal_unsat_core.smt2
   regress1/model-blocker-simple.smt2
   regress1/model-blocker-values.smt2
   regress1/nl/approx-sqrt.smt2
diff --git a/test/regress/regress1/minimal_unsat_core.smt2 b/test/regress/regress1/minimal_unsat_core.smt2
new file mode 100644
index 000000000..ef1d3ceef
--- /dev/null
+++ b/test/regress/regress1/minimal_unsat_core.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --minimal-unsat-cores
+(set-logic QF_NIA)
+(set-info :status unsat)
+(declare-fun n () Int)
+
+(assert (= n 0))
+(assert (= (div (div n n) n)
+           (div (div (div n n) n) n)))
+(assert (distinct (div (div n n) n)
+                  (div (div (div (div (div n n) n) n) n) n)))
+
+(check-sat)