satore: robust confluence — one-literal critical pairs and max-steps=1

[PratikDhanave]

Summary

Two fixes in the rewrite-tree confluence code (satore/rewrite-tree.rkt).

1. find-critical-pairs crashes on a one-literal critical pair

The bounded-size filter hard-codes two literals:

(> (max (literal-size (first cl)) (literal-size (second cl))) max-size)

But cl is (clause-normalize (substitute (list to-lit1 to-lit2) s)), and safe-factoring (inside clause-normalize) can collapse the two to literals into a single literal — e.g. rules p(X) -> q(X) and ~p(Y) -> q(Y) produce the resolvent [q(Y) q(Y)], which normalizes to [q(Y)]. (second cl) then raises an index error.

Fix — take the max literal-size over the whole clause (identical to the old behavior for two-literal clauses, and matching the docstring "a literal heavier than a from literal"):

(> (apply max 0 (map literal-size cl)) max-size)

2. rewrite-tree-confluence! drops the final step's change from its result

The terminating branch returns any-change?, which never OR-s in the current iteration's changed?. When the loop stops because of max-steps (e.g. max-steps = 1) after a step that did add a rule, it wrongly returns #false, contradicting the docstring "Returns whether any change has been made." Fixed with (or any-change? changed?).

Testing

Verified by static tracing (clause-normalize/safe-factoring can reduce a 2-literal resolvent to 1 literal; the max-steps = 1 boundary returns before OR-ing the change). No Racket toolchain available locally; reviewers can run raco test satore/tests/.

[polarbe]

Dooray! 메일 발송 실패 안내 메일 발송 실패 안내 ***@***.***) 님께 보낸 메일이 전송되지 못하였습니다. 실패 사유를 확인해보세요. * 받는 사람 :  ***@***.***) * 발송 시간 :  2026-07-25T15:21:24 * 메일 제목 :  [google-deepmind/deepmind-research] satore: robust confluence — one-literal critical pairs and max-steps=1 (PR #741) * 실패 사유 :  받는 사람이 현재 메일 수신을 제한하고 있습니다. 이 설정은 개인 또는 조직의 메일 수신 정책에 의해 적용되었습니다. 이 메일은 발신전용으로 회신되지 않습니다. 더 궁금하신 사항은 ***@***.*** 으로 문의해 주시기 바랍니다. © Dooray!.

[PratikDhanave]

satore: makes confluence robust (one-literal critical pairs, max-steps=1). CI green — ready for review.

[polarbe]

Dooray! 메일 발송 실패 안내 메일 발송 실패 안내 ***@***.***) 님께 보낸 메일이 전송되지 못하였습니다. 실패 사유를 확인해보세요. * 받는 사람 :  ***@***.***) * 발송 시간 :  2026-08-21T14:39:20 * 메일 제목 :  Re: [google-deepmind/deepmind-research] satore: robust confluence — one-literal critical pairs and max-steps=1 (PR #741) * 실패 사유 :  받는 사람이 현재 메일 수신을 제한하고 있습니다. 이 설정은 개인 또는 조직의 메일 수신 정책에 의해 적용되었습니다. 이 메일은 발신전용으로 회신되지 않습니다. 더 궁금하신 사항은 ***@***.*** 으로 문의해 주시기 바랍니다. © Dooray!.