New strategy randomization

[quickbeam123]

A new option for getting a randomly sampled strategy (--sample_strategy), which expects a filename for describing a distribution on the option space to sample from. This is similar in function to and arguably subsumes the two related --mode random_strategy and --random_strategy on/sat/nocheck, which could be scheduled for removal after this is approved. The PR also cleans up a bit in Options.cpp and reorganises things there a bit (e.g., new OptionTag for INDUCTION and THEORIES options).

Three example files for option space sampling are provided: samplerFOL.txt, samplerFNT.txt, samplerSMT.txt. The first two roughly correspond to the FOL and FNT divisions of CASC, the last should include theory reasoning, but is at this moment incomplete (as documented there). (Ahmed's new branch on HOL, which won CASC HOL this year, already contains most this PR's commits and a file samplerHOL.txt there.)

The format of the sampler files should be easy to understand. It describes a sequence of sampling rules (one on each line, barring empty lines and comment lines starting with a #), which are executed in order, and each rule (provided its preconditions are satisfied) triggers sampling of a value for a particular option from a specified distribution. The most common sampler is for the categorical distribution (~cat), which is specified by a list of values with corresponding integer frequencies. Other samplers include ratios, uniform floats and integers, and a (shifted) geometric distribution for potentially unbounded integers. A notable feature is the ability to sample also virtual (non-existent) options, by convention prefixed by a $ sign, whose value can later be reference in the conditions.

Example:

# naming
> $nm ~cat Z:1,NZ:5 
$nm=Z > nm ~cat 0:1
$nm=NZ > nm ~sgd 0.07,2

First samples a virtual option $nm with either a value Z (1 out of 6) or Nz (5 out of 6).
Then, if $nm is set to Z sample the (actual) naming option with value 0 (nm ~cat 0:1 is simply an assignment to the effect of nm := 0), and if $nm is set to NZ, we sample from a shifted geometric distribution with p=0.07 and a shift=2. (So 2 gets selected with a probability p, 3 with a probability p(1-p), ... and 2+i with a probability p(1-p)^i).

[MichaelRawson]

This is cool! I guess this supports spidering/snaking and other such randomised runs, right?

I've asked a few questions here or there, otherwise looks good to me. The nice documentation you wrote up for this merge - could it go as a comment in a suitable file or as part of the wiki?

[quickbeam123]

Michael, thank you for your careful review!

I sometimes disagreed with your suggestions, but hopefully with a good justification.

To make Options.cpp a bit smaller again, I don't mind the other randomization mechanism to scheduled for removal. (However, it actually implements something the one does not, and that's taking property into account when sampling. We can have a longer discussion about it elsewhere.)

[MichaelRawson]

I sometimes disagreed with your suggestions, but hopefully with a good justification.

Absolutely! I fully expect to be wrong, you're the expert. :-)

To make Options.cpp a bit smaller again, I don't mind the other randomization mechanism to scheduled for removal.

Good. We can discuss at some point, if we don't turn out to have a use for the other thing then let's remove it. Merging.