LRS updates and fixes

[quickbeam123]

This is a result of some cleanup / refactoring / inspection efforts of LRS and the related code mostly around the PassiveContainer and its descendants.

(Ultimately, the goal was to create AWPassiveContainer as a generic, templated blend of two single queue AgeBasedPassiveClauseContainer : public SingleQueuePassiveClauseContainer<AgeQueue> and WeightBasedPassiveClauseContainer : public SingleQueuePassiveClauseContainer<WeightQueue>, which are now provided, and later use such CompositePassiveClauseContainer<C1,C2> for further experiments. However, this ambitious bit is not achieved, yet.)

Major things done:

• (1) fixed a bug in functions called in master fulfilsAgeLimit/fulfilsWeightLimit where the buggy pattern of

return age <= _ageSelectionMaxAge || (age == _ageSelectionMaxAge && weightForClauseSelection <= _ageSelectionMaxWeight);

meant that the second half of the condition never triggered and the corresponding computation was useless.

• funnily, making the above check more precise for fulfilsWeightLimit lead to a performance degradation and so I instead kicked out _weightSelectionMaxAge and we no longer maintain the age tie breaker in the stored limit on the weight queue
• removed awr shapes (as my brain was not large enough to comprehend and update LRS logic with them around; also we agreed with @MichaelRawson they are probably not worth having around); also from Schedules and samplers
• (2) the prover initialization (until the start the main loop) is ignored in the LRS "speed of processing" estimate, which is thus more precise
• (3) introduced the SingleQueuePassiveClauseContainer (and specialized if for AgeQueue and WeightQueue) which meant the AWPassiveContainer code could be simplified quite a bit
• added awr 0:1 and 1:0 to the samplers so that they become eligible strategies
• however, the plain age and plain weight strategies mostly suck (and counter-intuitively suck even more when properly adhering to the LRS principles - I observed several regressions when "fixing" the code made the performance worse. Mostly one is better off with otter for these, but the code is, hopefully a good learning example on what's going on
• refined the LRS api of PassiveClauseContainer (mostly just renamed things) so that the functions are (hopefully) more intuitive and added plenty of comments
• (4) half of the LRS API is concerned with deleting already accepted passive (and also active) clauses when the limits get tighter; from passive, we then try to delete clauses that are beyond the new limit or whose only children would only be beyond the limit and from active, we try to delete clauses whose only children would be beyond the limit. This "retroactive deletion" effort does not seem to pay off in general, in fact, tends to be rather detrimental, and so it's now guarded by a new option)

I renamed a file in the process, so the part of the diff is not very useful, sorry! However, I will soon add some performance results to compensate.

[quickbeam123]

FOF TPTP run with -i 5000 (approx 2.0-2.5s per problem)

Sort by UNS
8297 ['problemsSTD_master8750_default_i5000.pkl']
8426 ['problemsSTD_mlf8761_default_i5000.pkl'] (1)
8427 ['problemsSTD_mlf8755_default_i5000.pkl'] (2)
8447 ['problemsSTD_mlf8771_default_i5000.pkl'] (3)
8452 ['problemsSTD_mlf8777_default_i5000.pkl'] (4) - retroactive deletion false now, by default

plot.pdf

[MichaelRawson]

This is much nicer code. Big experimental improvements, too! Can we treat lrd with suspicion and eventually delete if it doesn't give any benefit?

[MichaelRawson]

What are the semantics of andThatsIt? The container only discriminates by age?

[quickbeam123]

Yes, it's the weird -arw 1:0 corner case.

I agree we could simplify things here if we agreed that pure age container is not worth extra fancyness in the code.

Otherwise, I was just trying to do my homework to the end ;)

[MichaelRawson]

'A' for the homework! OK - I was just thinking if so that you could have a member function isPureAgeContainer() const or even a static (if the inheritance stuff works out) that does that bit, and thereby remove the need for the out-parameter here.

[quickbeam123]

It's definitely to the effect of isPureAgeContainer. But I think we would need another virtual function in the interface for this, don't you?

I guess I can still easily kick this out, check how much we lose in the -awr 1:0 case and if it's bearable, simplify, but leave a comment on how the homework should have been done?

[MichaelRawson]

Please don't kick it out, it seems like the nice way of doing things! I intended adding another virtual function to the interface like you say, but if you don't like that solution this one seems fine to me. :-)

[quickbeam123]

Yes, it would be nice if we could spider-out lrd=true completely. The interface could then be made much simpler again.

A potential explanation for why retroactive deletions are not so good is that it takes extra effort to remove these clauses and we have "already payed for" them (through inter-reductions on entering passive) so might just keep them for chance of leading to a "luck proof" trough reductions. (As LRS is deleting clauses on the grounds they will most likely not be feasible parents for GENERATING inferences only.)

[quickbeam123]

Adding one more boost - Unprocessed doing FIFO instead of LIFO, moves us up by ~30 problems here:

8452 ['problemsSTD_mlf8777_default_i5000.pkl']
8483 ['problemsSTD_mlf8780_default_i5000.pkl']

[
plot.pdf
](url)