Engine: Meta

[shilangyu]

Introduces a Meta folder with all of the optimizations that sit on top of other engines.

[Aurele-Barriere]

Having this option nat as a configuration is very restrictive. It says that the only way we decide between using MemoBT or for instance PikeVM is by checking the peak memory usage. Why is this not a function, from regex and string to a choice of engine?
The correctness of the meta engine should not be depend on the heuristics we use to decide which engine to run

[shilangyu]

The idea was that a user provided heuristic in my opinion is not very useful. Indeed, the proof would barely change and its trivially true that it is correct (any choice of engine is correct). But since the Meta engine is much less abstract and actually wants to exploit the details of engines, I thought it would be good to essentially hardcode these decision procedures.

I can make it more abstract, and then write a specialization of it with the nat version for example, would you find that useful?

[Aurele-Barriere]

I think that's better to have the heuristics abstracted yes, we should be able to change the heuristics without changing anything in the proofs.

[shilangyu]

I experimented a bit with this abstraction. I feel like abstracting this is very leaky. For example, say we abstract the choice of choosing an anchored and unanchored engine. Then, this choice has to make a decision just based on the regex and input, without knowing what purpose the engine is being ran for. For instance, we might want to run the anchor engine for different purposes. It also gets a bit hairy with being precise about which regexes these heuristics that pick the engine support.

I can attempt more of this tomorrow, but I personally find it hard to do it in a way that is beneficial and well abstracted :/