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.

1 files changed, 51 insertions, 3 deletions

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