diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-03-10 18:33:41 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-10 13:33:41 -0800 |
| commit | f4519b17b6738cf959877c0e0b37000fc7bb0d88 (patch) | |
| tree | fe1928ff1ab5f06912e2ad3447310a2c412c23c0 | |
| parent | c81140e9ab5db8bc95eb15145641be9d909d0618 (diff) | |
[proof-new] Clarifying doc (#6108)
| -rw-r--r-- | src/expr/proof_rule.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 2759a3c9e..e2933e012 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -302,8 +302,8 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: C2 // where - // Set representations of C1 and C2 is the same but the number of literals in - // C2 is the same of that of C1 + // Set representations of C1 and C2 are the same and the number of literals + // in C2 is the same of that of C1 REORDERING, // ======== N-ary Resolution + Factoring + Reordering // Children: (P1:C_1, ..., Pm:C_n) |