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, 8 insertions, 0 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