Implement query caching

[mtzguido]

This PR introduces an internal cache of VCs that were already successfully discharged to Z3, to later avoid asking them again. This happens very often when working interactively over a file and making small edits. The way it works, roughly, is that any time before discharging a VC of shape G |= t, we first look up hash((G,t) in an RBSet, and if it's there, we report success without making the query. Otherwise we ask Z3, and if that works, we add the hash to the RBSet.

It is not meant to be bullet proof. For one, it is not handling hash collisions and second the hash is even ignoring some possibly relevant pieces (like effect definitions in the environment, they do not go into the hash).

It's also only enabled on IDE mode, the batch mode ignores it. For one it's a lot less useful there, but most importantly this means this new feature does not affect existing makefiles, CI, etc. It also has to be explicitly enabled with --query_cache.

The cache is always kept live and populated as long as F* lives. Even popping options does not clear it (which is not immediately a problem since pragmas like #push-options go into the environment and are hashed).

This feature is mostly motivated by Pulse, where we may do many small queries in program order, so this makes interactive editing of a program fragment a lot faster. For F*, it is mostly useful when there are no changes, since queries are usually monolithic.

[nikswamy]

This is super useful, especially for Pulse. Thanks Guido!