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, 35 insertions, 1 deletions

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();
 }