KCFG optimisation-on-creation

[PetarMax]

This PR introduces an optional optimisation that performs, as the KCFG is created, the already implemented edge minimisation procedure, in which two consecutive edges are subsumed into one.

In this way, we generate much smaller KCFGs, speeding up very large proofs.

[ehildenb]

@PetarMax this needs to be a new KCFGExtendResult type, not something modifying the signature of commit, since that function is used for different proof types too. KCFG minimization has tobe its own routine that isn't done in conjunction with other things, to keep synchronization across threads working nicely.

[PetarMax]

This works perfectly across threads. Understood re signature of commit, will adapt.

[PetarMax]

Also, I am not sure that we can do anything beyond this edge subsumption in the context of branch parallelisation. The leaf node identifiers do get preserved, though...

[PetarMax]

@ehildenb Is it looking better now?

[PetarMax]

I can confirm that this change decreases the running time of our longest, most intensive engagement test by ~20%.

[tothtamas28]

I can confirm that this change decreases the running time of our longest, most intensive engagement test by ~20%.

20% is pretty significant, and it indicates that somehow maintaining a proof becomes more and more expensive as the number of nodes (or the depth of the tree) grows. What operation could be the cause of this?

[PetarMax]

It could be the KCFG traversal, understanding pending nodes, understanding next steps, and then doing all this in parallel for a number of threads...

[ehildenb]

It would be worth it to profile it and see where the expensive routines are. I bet we can get a lot of that 20% shaved off with some targeted optimizations.

That being said, periodic minimization seems useful. But maybe we should just always minimize if the user asks? Basically, when we get a Step result here, and if minimization is turend on, we check if the prior edge was an Edge, and if so just extend that prior edge (remove it, and put in a longer edge with the union of the rules list and the addition of the depth counters to the new state). So we don't need to minmiize the whole KCFG every time, we instead just use Step to extend Edge when they are entered into the KCFG, rather than create a new one. I see now that this is basically what we're doing here!

We still need to be able to maintain the old behavior for Simbolik, which relies on being able to see every node that is stored for opcode cuts. Minimization basically doesn't play nicely with cut-rules.

[PetarMax]

I see now that this is basically what we're doing here!

We still need to be able to maintain the old behavior for Simbolik, which relies on being able to see every node that is stored for opcode cuts. Minimization basically doesn't play nicely with cut-rules.

Yes, this is what we're doing :) and yes, this behaviour wouldn't be forced, it would be non-default and activated with a switch. Hmm, could we have a minimize-for-symbolik variant of minimization, which leaves the cut-rules but compresses others?

[ehildenb]

This may cause problems in the future if the same node is referenced by a merged edge somewhere, for example. Maybe best to just keep the node? But that also could cause problems with how we display the KCFG....

So maybe best to just note that this could be a source of issues if the nodes is already referred to somewhere else. It may also warrant making a safe_remove_node option, which checks that there aren't any references to the node before removing it. Can you make an issue about that and link it back to this comment?

[ehildenb]

I assume this final version was tested downstream to work with the examples we care about. Looks good.