Two fatal errors on same TPTP problem, with non-default options
mdesharnais opened this issue · 2 comments
We recently updated Metis to 2.4 in Isabelle. Things ran smoothly on thousands of proof goals, but we ran into two regressions, where Metis suddenly gave "KeyMap.delete: element not found" errors. We translated one of the two problems to TPTP and modified metis.sml to use the same options as in Isabelle (see attachments), without which the bug didn't arise in a reasonable time. Playing with the options, we obtained a different error outcome ("Active.simplify: clause should have been simplified away"). Details on these errors and how to reproduce them can be found in the attached patch for metis.sml.
Let us know if you need any further information. This is not a showstopper for us.
Martin & Jasmin
Thank you very much for isolating this bug and submitting the report. I can reproduce both defects and will work on root-causing the issue(s).
I believe I understand the two bugs and will commit a fix for them shortly.
The first bug (crashing in KeyMap.delete) can occur when mutually rewriting the disequality literals in a clause, for example rewriting
|- ~(a = f (g b)) \/ ~(f a = f $x) \/ ~(f (g b) = g c) \/ ~(g c = f $x) \/
~(g c = f a)
to
|- ~(a = f $x) \/ ~(a = f a) \/ ~(a = f (g b)) \/ ~(g c = a)
This is the smallest example I could find that triggered the crash. During rewriting there is a collision and an extra disequality literal is simplified away, but a later step assumed the literal was present in the theorem and tried (and failed) to do a resolution step on it. I fixed this by checking the literal still exists in the theorem before performing the resolution step.
The second bug was a faulty assumption in the code that prevented clauses from being fully simplified. After rewriting a clause with its disequality literals and then instantiating variables according to literals of the form ~($x = <term-not-containing-$x>), this can enable another round of rewriting with disequality literals:
~(X = f(X)) \/ ~(g(Y) = f(X)) \/ ~(c = f(X))
---------------------------------------------- rewrite
~(X = f(X)) \/ ~(g(Y) = X) \/ ~(c = X)
---------------------------------------------- simplify
~(g(Y) = f(g(Y))) \/ ~(c = g(Y))
---------------------------------------------- rewrite
~(c = f(c)) \/ ~(c = g(Y))
The code now attempts another round of rewriting if simplification changed anything.
Thank you again for the bug report.