Alexander Bentkamp
2020-04-27 8:48:47 (GMT)
I just got back the results for the lambda-free Sup eval. Unlike in 2018, our calculi now perform much worse than the first-order mode. It seems that this is due to polymorphic ArgCong. I think we need to slow it down significantly.
Petar Vukmirovic
2020-04-27 8:50:51 (GMT)
Ok send me the results and I will take a look
Alexander Bentkamp
2020-04-27 8:54:57 (GMT)
Don't worry about. I'll take care of it.
Petar Vukmirovic
2020-04-27 11:6:38 (GMT)
Ok send me the results and I will take a look
Alexander Bentkamp
2020-04-27 11:31:5 (GMT)
We could do it like this: https://github.com/sneeuwballen/zipperposition/commit/4c3027a0055bced8ac540e3887bb26a8f8dded68
Alexander Bentkamp
2020-04-27 11:31:36 (GMT)
I am not sure how this would influence superposition with lambdas, though.
Petar Vukmirovic
2020-04-27 11:42:11 (GMT)
Looks good
Petar Vukmirovic
2020-04-27 11:42:37 (GMT)
For your question I think we need to tune the parameters
Alexander Bentkamp
2020-04-27 11:43:5 (GMT)
How?
Petar Vukmirovic
2020-04-27 11:43:19 (GMT)
well putting the right values for penalty for sup with lams
Alexander Bentkamp
2020-04-27 11:43:54 (GMT)
but what is the right value?
Petar Vukmirovic
2020-04-27 11:44:36 (GMT)
we need to test that :slight_smile:
Petar Vukmirovic
2020-04-27 11:44:45 (GMT)
something lower than ArgCong for sure
Jasmin Blanchette
2020-04-27 11:50:59 (GMT)
I have the impression this is rather slow converging... Whatever you do, test it on five examples that fail today before running yet another multi-day round on StarExec...
Jasmin Blanchette
2020-04-27 11:52:13 (GMT)
That's usually how I tune(d) fudge factors.
Petar Vukmirovic
2020-04-27 12:6:45 (GMT)
Alex tested in on one example, maybe he can add 4 more and I can see if we destroyed anything :slight_smile:
Alexander Bentkamp
2020-04-27 12:11:32 (GMT)
Ok, I tested 4 more examples and they all work now.
Alexander Bentkamp
2020-04-27 12:12:31 (GMT)
Petar will test whether this new behavior of the streams hurts lambda-superposition.
Alexander Bentkamp
2020-04-27 12:14:6 (GMT)
And I will run the next eval in Iowa because apparently it is much faster?
Petar Vukmirovic
2020-04-27 12:22:52 (GMT)
Yes :slight_smile:
Petar Vukmirovic
2020-04-27 12:32:15 (GMT)
Tests are running
Petar Vukmirovic
2020-04-28 15:40:35 (GMT)
@Alexander Bentkamp : I found a bug with the rule I described last week. It makes issues only with the problems containing applied predicate variables, and if you do not have them you do not need to rerun your eval
Petar Vukmirovic
2020-04-28 15:40:56 (GMT)
I have also found a bug in lambda-lifting part of E interface module, which I am trying to fix now
Petar Vukmirovic
2020-04-28 15:41:6 (GMT)
again, if you do not use this feature you are safe
Alexander Bentkamp
2020-04-28 15:49:4 (GMT)
I don't use the E backend, but maybe I have applied predicate variables. Are those allowed in the lambda-free fragment check?
Alexander Bentkamp
2020-04-28 15:51:20 (GMT)
And what is the rule you described last week?
Petar Vukmirovic
2020-04-28 15:58:27 (GMT)
Petar Vukmirovic
2020-04-28 15:59:5 (GMT)
BoolEF rule...
And the E-related bug is in E, not in Zip, so it might influence both Leo and Satallax
Alexander Bentkamp
2020-04-28 16:32:6 (GMT)
Oh, so the bug was in Boolean.ml? That's no problem for me. That module is deactivated in lambda-free mode.
Petar Vukmirovic
2020-04-28 16:47:56 (GMT)
No no.. there is this one inference which is run from Superposition.ml and taps into normal equality factoring
Petar Vukmirovic
2020-04-28 16:48:36 (GMT)
But it concerns terms of the form where is a predicate variable
Petar Vukmirovic
2020-04-28 16:49:6 (GMT)
BoolEF(+/-)
Alexander Bentkamp
2020-04-28 17:42:42 (GMT)
Ok, I see. But luckily predicate variables are not allowed in the lambda-free fragment. So its' all good.