diff options
Diffstat (limited to 'src/expr/proof_rule.h')
| -rw-r--r-- | src/expr/proof_rule.h | 8 |
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 |