Reimplement QAlpha internals and expand benchmarking

[edenfrenkel]

This pull request performs the following changes.

In inference:

• Reimplement and reorganize the QAlpha code:
  • Rename subsume.rs -> language.rs, lemma.rs -> frame.rs, weaken.rs -> lemmas.rs, and move all QAlpha-related code into inference/src/qalpha.
  • Remove the Not language constructor and add dedicated constructors for And, Or, and quantification.
  • Define weakening recursively together with language construction.
  • Use the total order over canonical formulas to minimize sets.
• Implement a custom parallelism scheme in parallel.rs:
  • Actually run threads / solvers simultaneously (with rayon this was often not the case). This also lead to some changes in solver/src/basics.rs, namely replacing rayon with standard library threading.
  • Allow prioritization of tasks, as well as adding tasks / cancelling remaining tasks mid-run.

In bounded:

• In simulator.rs, implement two bounded simulators, one based on explicit-state (using set.rs) and another on SAT solving (using sat.rs), which given a universe size can produce all initial states, as well as all successors of a given state.
• Implement dynamic solvers which can handle multiple universe sizes.
• Expand the preprocessing in fly/src/rets.rs by implementing flattening to eliminate nested function applications.
• Perform some minor changes, mainly to do with typing / lifetimes, to enable the above.
• Use the above to replace the SMT-based simulations in QAlpha.

In benchmarking:

• Add QAlpha benchmarks.
• Add more detailed reporting, and save the stdout and stderr of each run.

[tchajed]

If this is at a stable point, let's merge it. It's too big to review at this point so I'd rather merge it now and start splitting up future features when possible.

[edenfrenkel]

I agree, you can go ahead and merge