FMB max sort size detection via X = t_1 | ... | X = t_n

[quickbeam123]

As Andrei pointed out, the check in SortInference.cpp could be stronger:

(2) If some of the t_i's are unifiable, the bound can be made lower.
You discussed below an example: X = Y | X = c, for which the bound is
1 since one can derive X = c from it.

However, this is further complicated by the fact that SortInference sees the FMB-proprocessed clauses. Often general splitting destroys the necessary structure as with, e.g.
cnf(a,axiom,Y = Z | e = Z | f(X) = Z ).
which may reach the relevant place as, e.g.,
16. f(X0) = X1 | sP0(X1) [general splitting component introduction]
and
17. e = X0 | X0 = X1 | ~sP0(X0) [general splitting 1,16]

[easychair]

As Andrei pointed out, the check in SortInference.cpp could be stronger: (2) If some of the t_i's are unifiable, the bound can be made lower. You discussed below an example: X = Y | X = c, for which the bound is 1 since one can derive X = c from it. However, this is further complicated by the fact that SortInference sees the FMB-proprocessed clauses. Often general splitting destroys the necessary structure as in:

I am not sure what it means, you forgot to include the example.

[quickbeam123]

I just pressed Enter too early. Now, the example is in there. Sure the main trick will be to move upper bound detection after clausification but before general splitting, but with that I kind of wanted to pass the ball to @selig who knows the FMB pipeline better than me.

[easychair]

The example is not there but the solution seems to be right. Not sure though if this is likely to occur in real problems. A

…

On Wed, 20 Jul 2022 at 14:18, Martin Suda ***@***.***> wrote: I just pressed Enter too early. Now, the example is in there. Sure the main trick will be to move upper bound detection after clausification by before general splitting, but with that I kind of wanted to pass the ball to @selig <https://github.com/selig> who knows the FMB pipeline better than me. — Reply to this email directly, view it on GitHub <#398 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABVY4BN5SKQE4DSHRBHUFMLVU7VB5ANCNFSM54C76E6A> . You are receiving this because you commented.Message ID: ***@***.***>

[selig]

I agree it could be stronger but the current implementation should at least capture the common case, which is an explicit domain axiom using constants (e.g. X = a | X = b | X = c). Previously I tried to write a general solution and there was a bug and we removed it, leaving us without support for this simple common case (for many years).

Before we make changes I'd want to do an analysis of some real problems to see if the more general case actually occurs with any frequency.