Open Halbaroth opened 5 months ago
In my opinion there are two issues here:
id
can flood the SAT solver with useless monomorphization of itself isn't a desired behaviour. Matching
. So we could keep all the triggers generated by Alt-Ergo, sort them with an appropriate weight function and try to match them in this order until we reach the maximal number of instantiations.
I don't know if we should use a different limitation per axiom or the same one for all of them.Does the problem also happen with the Tableaux solver? I remember that it seemed to behave better wrt instantiation in some tests I made while looking at the differences a while back.
Limiting the number of triggers per axiom is indeed a bit weird, and your proposed solution of limiting the number of instantiations per axiom looks better, but the devil's in the details (for instance we should probably do some sort of round-robin strategy on the triggers we use for a given axiom, to ensure all triggers ultimately have a chance to be checked in some later matching round). It is likely a deep rabbit hole that'll lead to a game of whack-a-mole with regressions, so it's probably safer to explore post-release (realistically as part of the matching/instantiation cleanup that is on the TODO list).
for instance we should probably do some sort of round-robin strategy on the triggers we use for a given axiom, to ensure all triggers ultimately have a chance to be checked in some later matching round
It's exactly what I had in mind but I didn't find a way to explain it. Basically, we have to be fair with both triggers and axioms.
realistically as part of the matching/instantiation cleanup that is on the TODO list
Don't worry. I don't plan to work on it before the release. I open this issue as a remainder. Actually, I use the mechanism of GitHub to pin issues to releases.
Does the problem also happen with the Tableaux solver? I remember that it seemed to behave better wrt instantiation in some tests I made while looking at the differences a while back.
Good catch! It works with the option --sat-solver Tableaux
.
Good catch! It works with the option
--sat-solver Tableaux
.
Ha! That confirms an intuition I had that we should be looking precisely at the difference in the way the Tableaux and CDCL solver do matching/instantiation and see if we can reproduce the behavior of the Tableaux solver in the CDCL solver.
(For context, after #1041 I expected that disabling dynamic variable ordering in the CDCL-Tableaux solver would provide identical behavior to the Tableaux solver, but it was not the case in particular due to different instantiation strategies. I have hopes we can reduce the gap between the two solvers by looking at the difference between their behavior wrt instantiation and having the CDCL-Tableaux solver match the behavior of the Tableaux solver — unless it drastically slows the solver, which is a possibility)
While looking for a minimal example that triggers a regression introduced by my patch in #1102, I ran into another issue (as always...) with our instantiation strategy. A relatively short example:
(It's not easy to simplify further this example, I tried hard).
If you run AE on this file, you'll got a
Valid
answer quickly, and indeed, the goal is valid. But if you uncomment thebad
axiom, AE loops infinitely, producing new monomorphization of the termid
with typesa t, a t t, a t t t, ...
.It's a bit sad that a completely useless axiom produces an infinitely loop so easily.
While generating new multi-triggers, Alt-Ergo filters the multi-triggers to limit their number. In particular, AE produces at most
nb_triggers
multi-triggers per axiom wherenb_triggers
is a field of the matching environment (defined inUtil.ml
). The initial value ofnb_triggers
is given byOptions.get_nb_triggers ()
and its default value is2
.The limit
nb_triggers
is adaptive and can be increased with a factor depending of the matching mode (normal
,greedy
andgreedier
). In fact, this limit increases if the solver cannot progress after some matching rounds.Before any filtering, the multi-triggers generated by AE for the axioms are:
bad
, we got the multi-triggersid
andh(id)
.good1
, we gotx
andrename(x, id)
.good2
, we goti
,x
,rename(x, id)
,p(x, i, x)
,f(p(x, i, rename(x, id)))
.Now AE removes the variables and keep only two multi-triggers, so we got:
bad
, we got the multi-triggersh(id)
andid
.good1
, we gotrename(x, id)
.good2
, we gotrename(x, id)
,f(p(x, i, rename(x, id)))
.Unfortunately, AE threw the crucial multi-trigger
p(x, i, x)
. Since it keeps the multi-triggerid
, the matching will progress with useless new terms and so the adaptive limitnb_triggers
will never increase. If you call AE with the option--nb_triggers 3
, it succeeds!Another way to solve the issue consists in removing the
ite
in theAuto
strategy (seeSatml_frontend
).