Add assumption-based unsat cores. (#6427)

This PR adds an assumption-based unsat cores option. If enabled it will
disable proof logging in the SAT solver and adds input assertions as
assumptions to the SAT solver. When an unsat core is requested we
extract the unsat core in terms of the unsat assumption in the SAT
solver. Assumption-based unsat cores use the proof infrastructure to map
the input assumptions back to the original assertions.

9 files changed, 169 insertions, 27 deletions

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 88e344b8a..432ff1f89 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -247,6 +247,14 @@ enum class PfRule : uint32_t
   // where F is an equality (= t t') that holds by a form of substitution that
   // could not be determined by the TrustSubstitutionMap.
   TRUST_SUBS_MAP,
+  // ========= SAT Refutation for assumption-based unsat cores
+  // Children: (P1, ..., Pn)
+  // Arguments: none
+  // ---------------------
+  // Conclusion: false
+  // Note: P1, ..., Pn correspond to the unsat core determined by the SAT
+  // solver.
+  SAT_REFUTATION,
 
   //================================================= Boolean rules
   // ======== Resolution
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 40274489b..19f1bff97 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -484,8 +484,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
       // If a literal is false at 0 level (both sat and user level) we also
       // ignore it, unless we are tracking the SAT solver's reasoning
       if (value(ps[i]) == l_False) {
-        if (!options::unsatCores() && !isProofEnabled()
-            && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0)
+        if (!options::unsatCores() && !needProof() && level(var(ps[i])) == 0
+            && user_level(var(ps[i])) == 0)
         {
           continue;
         }
@@ -527,7 +527,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
       // If all false, we're in conflict
       if (ps.size() == falseLiteralsCount) {
-        if (options::unsatCores() || isProofEnabled())
+        if (options::unsatCores() || needProof())
         {
           // Take care of false units here; otherwise, we need to
           // construct the clause below to give to the proof manager
@@ -549,7 +549,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
               ProofManager::getSatProof()->finalizeProof(
                   cvc5::Minisat::CRef_Lazy);
             }
-            if (isProofEnabled())
+            if (needProof())
             {
               d_pfManager->finalizeProof(ps[0], true);
             }
@@ -574,7 +574,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
         clauses_persistent.push(cr);
         attachClause(cr);
 
-        if (options::unsatCores() || isProofEnabled())
+        if (options::unsatCores() || needProof())
         {
           if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
           {
@@ -596,7 +596,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
             {
               ProofManager::getSatProof()->finalizeProof(cr);
             }
-            if (isProofEnabled())
+            if (needProof())
             {
               d_pfManager->finalizeProof(ca[cr], true);
             }
@@ -633,7 +633,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
             // already been registered, as the ProofCnfStream will not register
             // them and as they are not the result of propagation will be left
             // hanging in assumptions accumulator
-            if (isProofEnabled())
+            if (needProof())
             {
               d_pfManager->registerSatLitAssumption(ps[0]);
             }
@@ -654,7 +654,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
                 ProofManager::getSatProof()->finalizeProof(confl);
               }
             }
-            if (isProofEnabled())
+            if (needProof())
             {
               if (ca[confl].size() == 1)
               {
@@ -755,7 +755,7 @@ void Solver::removeClause(CRef cr) {
       // Solver::reason, if it appears in a resolution chain built lazily we
       // will be unable to do so after the step below. Thus we eagerly justify
       // this propagation here.
-      if (isProofEnabled())
+      if (needProof())
       {
         Trace("pf::sat")
             << "Solver::removeClause: eagerly compute propagation of " << c[0]
@@ -1001,7 +1001,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
   {
     ProofManager::getSatProof()->startResChain(confl);
     }
-    if (isProofEnabled())
+    if (needProof())
     {
       d_pfManager->startResChain(ca[confl]);
     }
@@ -1066,7 +1066,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
               {
                 ProofManager::getSatProof()->resolveOutUnit(q);
               }
-              if (isProofEnabled())
+              if (needProof())
               {
                 d_pfManager->addResolutionStep(q);
               }
@@ -1088,7 +1088,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
           {
             ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
           }
-          if (isProofEnabled())
+          if (needProof())
           {
             d_pfManager->addResolutionStep(ca[confl], p);
           }
@@ -1129,7 +1129,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
                 {
                   ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
                 }
-                if (isProofEnabled())
+                if (needProof())
                 {
                   Debug("newproof::sat")
                       << "Solver::analyze: redundant lit "
@@ -1677,7 +1677,7 @@ lbool Solver::search(int nof_conflicts)
         {
           ProofManager::getSatProof()->finalizeProof(confl);
         }
-        if (isProofEnabled())
+        if (needProof())
         {
           if (confl == CRef_Lazy)
           {
@@ -1704,7 +1704,7 @@ lbool Solver::search(int nof_conflicts)
         {
           ProofManager::getSatProof()->endResChain(learnt_clause[0]);
         }
-        if (isProofEnabled())
+        if (needProof())
         {
           d_pfManager->endResChain(learnt_clause[0]);
         }
@@ -1723,7 +1723,7 @@ lbool Solver::search(int nof_conflicts)
           ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
           ProofManager::getSatProof()->endResChain(id);
         }
-        if (isProofEnabled())
+        if (needProof())
         {
           d_pfManager->endResChain(ca[cr]);
         }
@@ -2219,7 +2219,7 @@ CRef Solver::updateLemmas() {
 
       // If it's an empty lemma, we have a conflict at zero level
       if (lemma.size() == 0) {
-        Assert(!options::unsatCores() && !isProofEnabled());
+        Assert(!options::unsatCores() && !needProof());
         conflict = CRef_Lazy;
         backtrackLevel = 0;
         Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
@@ -2249,7 +2249,7 @@ CRef Solver::updateLemmas() {
   // Last index in the trail
   int backtrack_index = trail.size();
 
-  Assert(!options::unsatCores() || isProofEnabled()
+  Assert(!options::unsatCores() || needProof()
          || lemmas.size() == (int)lemmas_cnf_assertion.size());
 
   // Attach all the clauses and enqueue all the propagations
@@ -2320,7 +2320,7 @@ CRef Solver::updateLemmas() {
             {
               ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
             }
-            if (isProofEnabled())
+            if (needProof())
             {
               d_pfManager->storeUnitConflict(lemma[0]);
             }
@@ -2334,7 +2334,7 @@ CRef Solver::updateLemmas() {
     }
   }
 
-  Assert(!options::unsatCores() || isProofEnabled()
+  Assert(!options::unsatCores() || needProof()
          || lemmas.size() == (int)lemmas_cnf_assertion.size());
   // Clear the lemmas
   lemmas.clear();
@@ -2400,5 +2400,11 @@ std::shared_ptr<ProofNode> Solver::getProof()
 
 bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
 
+bool Solver::needProof() const
+{
+  return isProofEnabled()
+         && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS;
+}
+
 }  // namespace Minisat
 }  // namespace cvc5
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index cd3f38c9e..a9ee25c11 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -160,6 +160,13 @@ public:
  /** Is proof enabled? */
  bool isProofEnabled() const;
 
+ /**
+  * Checks whether we need a proof.
+  *
+  * SAT proofs are not required for assumption-based unsat cores.
+  */
+ bool needProof() const;
+
  // Less than for literals in a lemma
  struct lemma_lt
  {
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 813292a21..611416dbc 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -32,7 +32,7 @@ namespace prop {
 //// DPllMinisatSatSolver
 
 MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry)
-    : d_minisat(NULL), d_context(NULL), d_statistics(registry)
+    : d_minisat(NULL), d_context(NULL), d_assumptions(), d_statistics(registry)
 {}
 
 MinisatSatSolver::~MinisatSatSolver()
@@ -193,6 +193,40 @@ SatValue MinisatSatSolver::solve() {
   return result;
 }
 
+SatValue MinisatSatSolver::solve(const std::vector<SatLiteral>& assumptions)
+{
+  setupOptions();
+  d_minisat->budgetOff();
+
+  d_assumptions.clear();
+  Minisat::vec<Minisat::Lit> assumps;
+
+  for (const SatLiteral& lit : assumptions)
+  {
+    Minisat::Lit mlit = toMinisatLit(lit);
+    assumps.push(mlit);
+    d_assumptions.emplace(lit);
+  }
+
+  SatValue result = toSatLiteralValue(d_minisat->solve(assumps));
+  d_minisat->clearInterrupt();
+  return result;
+}
+
+void MinisatSatSolver::getUnsatAssumptions(
+    std::vector<SatLiteral>& unsat_assumptions)
+{
+  for (size_t i = 0, size = d_minisat->d_conflict.size(); i < size; ++i)
+  {
+    Minisat::Lit mlit = d_minisat->d_conflict[i];
+    SatLiteral lit = ~toSatLiteral(mlit);
+    if (d_assumptions.find(lit) != d_assumptions.end())
+    {
+      unsat_assumptions.push_back(lit);
+    }
+  }
+}
+
 bool MinisatSatSolver::ok() const {
   return d_minisat->okay();
 }
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 42588080d..74b7ab749 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -58,6 +58,8 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
 
   SatValue solve() override;
   SatValue solve(long unsigned int&) override;
+  SatValue solve(const std::vector<SatLiteral>& assumptions) override;
+  void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions) override;
 
   bool ok() const override;
 
@@ -100,6 +102,14 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
   /** Context we will be using to synchronize the sat solver */
   context::Context* d_context;
 
+  /**
+   * Stores assumptions passed via last solve() call.
+   *
+   * It is used in getUnsatAssumptions() to determine which of the literals in
+   * the final conflict clause are assumptions.
+   */
+  std::unordered_set<SatLiteral, SatLiteralHashFunction> d_assumptions;
+
   void setupOptions();
 
   class Statistics {
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c4d929d35..23377cb0c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -82,7 +82,8 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_ppm(nullptr),
       d_interrupted(false),
       d_resourceManager(rm),
-      d_outMgr(outMgr)
+      d_outMgr(outMgr),
+      d_assumptions(userContext)
 {
   Debug("prop") << "Constructing the PropEngine" << std::endl;
 
@@ -262,7 +263,18 @@ void PropEngine::assertInternal(
   // Assert as (possibly) removable
   if (isProofEnabled())
   {
-    d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
+    if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS
+        && input)
+    {
+      Assert(!negated);
+      d_pfCnfStream->ensureLiteral(node);
+      d_assumptions.push_back(node);
+    }
+    else
+    {
+      d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
+    }
+
     // if input, register the assertion
     if (input)
     {
@@ -274,6 +286,7 @@ void PropEngine::assertInternal(
     d_cnfStream->convertAndAssert(node, removable, negated, input);
   }
 }
+
 void PropEngine::assertLemmasInternal(
     theory::TrustNode trn,
     const std::vector<theory::TrustNode>& ppLemmas,
@@ -358,7 +371,20 @@ Result PropEngine::checkSat() {
   d_interrupted = false;
 
   // Check the problem
-  SatValue result = d_satSolver->solve();
+  SatValue result;
+  if (d_assumptions.size() == 0)
+  {
+    result = d_satSolver->solve();
+  }
+  else
+  {
+    std::vector<SatLiteral> assumptions;
+    for (const Node& node : d_assumptions)
+    {
+      assumptions.push_back(d_cnfStream->getLiteral(node));
+    }
+    result = d_satSolver->solve(assumptions);
+  }
 
   if( result == SAT_VALUE_UNKNOWN ) {
 
@@ -628,5 +654,27 @@ std::shared_ptr<ProofNode> PropEngine::getProof()
 
 bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; }
 
+void PropEngine::getUnsatCore(std::vector<Node>& core)
+{
+  Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS);
+  std::vector<SatLiteral> unsat_assumptions;
+  d_satSolver->getUnsatAssumptions(unsat_assumptions);
+  for (const SatLiteral& lit : unsat_assumptions)
+  {
+    core.push_back(d_cnfStream->getNode(lit));
+  }
+}
+
+std::shared_ptr<ProofNode> PropEngine::getRefutation()
+{
+  Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS);
+  std::vector<Node> core;
+  getUnsatCore(core);
+  CDProof cdp(d_pnm);
+  Node fnode = NodeManager::currentNM()->mkConst(false);
+  cdp.addStep(fnode, PfRule::SAT_REFUTATION, core, {});
+  return cdp.getProofFor(fnode);
+}
+
 }  // namespace prop
 }  // namespace cvc5
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a0496a525..6812a6549 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -286,6 +286,13 @@ class PropEngine
 
   /** Is proof enabled? */
   bool isProofEnabled() const;
+
+  /** Retrieve unsat core from SAT solver for assumption-based unsat cores. */
+  void getUnsatCore(std::vector<Node>& core);
+
+  /** Return the prop engine proof for assumption-based unsat cores. */
+  std::shared_ptr<ProofNode> getRefutation();
+
  private:
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
@@ -370,6 +377,12 @@ class PropEngine
 
   /** Reference to the output manager of the smt engine */
   OutputManager& d_outMgr;
+
+  /**
+   * Stores assumptions added via assertInternal() if assumption-based unsat
+   * cores are enabled.
+   */
+  context::CDList<Node> d_assumptions;
 };
 
 }  // namespace prop
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8e8a1e062..09b3d64ab 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1419,9 +1419,19 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
   // generate with new proofs
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
-  Assert(pe->getProof() != nullptr);
-  std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(
-      pe->getProof(), *d_asserts, *d_definedFunctions);
+
+  std::shared_ptr<ProofNode> pepf;
+  if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS)
+  {
+    pepf = pe->getRefutation();
+  }
+  else
+  {
+    pepf = pe->getProof();
+  }
+  Assert(pepf != nullptr);
+  std::shared_ptr<ProofNode> pfn =
+      d_pfManager->getFinalProof(pepf, *d_asserts, *d_definedFunctions);
   std::vector<Node> core;
   d_ucManager->getUnsatCore(pfn, *d_asserts, core);
   return UnsatCore(core);
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index 256ccedce..8b2967fe6 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -74,6 +74,7 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::CNF_ITE_NEG1, this);
   pc->registerChecker(PfRule::CNF_ITE_NEG2, this);
   pc->registerChecker(PfRule::CNF_ITE_NEG3, this);
+  pc->registerTrustedChecker(PfRule::SAT_REFUTATION, this, 1);
 }
 
 Node BoolProofRuleChecker::checkInternal(PfRule id,
@@ -950,6 +951,11 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
         args[0], args[0][1].notNode(), args[0][2].notNode()};
     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
   }
+  if (id == PfRule::SAT_REFUTATION)
+  {
+    Assert(args.empty());
+    return NodeManager::currentNM()->mkConst(false);
+  }
   // no rule
   return Node::null();
 }