Skip to content

frame_instances: revise priorities for uses in "linear" bi

Note: For the purposes of this MR, "linear bi" includes those where BiAffine instances aren't available to proof search.

The new workings are documented in the code. Today, instead, frame_here_absorbing | 0 will seldom succeed, so frame_here | 1, but after other hints like frame_exist | 1. So, to frame R in R, where R is an existential, iFrame will first try to pull the existential apart before framing R as a whole, which might be expensive (especially for overly large Rs). The same applies to other connectives.

  • For each instance, I added either an explicit priority or a comment, but I'm sure you might have different preferences.

Please count this as a Bedrock contribution — we've hit this in practice (and we've also sealed the offending R).

Edited by Paolo G. Giarrusso

Merge request reports