Allow specifying the oracle to use in an oracle ranking

[kevinmorio]

Oracle rankings in a top-level heuristic specification or in lemma
attributes now allow the specification of independent oracles:

heuristic: o "/path/to/oracle"`

or

lemma example [heuristic=o "/path/to/oracle"]:
  ...

This PR indirectly fixes #372 since the heuristic can now be completely specified in the spthy file.

[rsasse]

Cool stuff! Just to make sure, does this also work for the heuristic "O" (using smart as base) or only for "o" (using consecutive)? It should be possible for both. Looking at the code it seems to do both. Great! Probably best to have a test set up for both cases though.

[kevinmorio]

Yes, it works for both the "o" and "O" heuristic. I added a minimal example for this feature. Should this also be included in the regression tests?

We might also consider changing the starting directory for relative paths given in an oracle ranking. Currently, they are relative to the current working directory which means that we have to cd into the directory containing the model file.
Instead, the paths could be relative to the directory of the model file.

[rkunnema]

Hi! We talked about this change and @kevinmorio wants to try to compute the path relative to the curred WD from the path relative to the spthy file and the spthy's location relative to the current WD.

[rsasse]

This sounds good in theory, and great if it works in practice across different OSes used. Please check at least on Linux+macos. Not necessarily on Windows, even though that would be good in case we support that again.

Thanks both for your work on this! :-)

[kevinmorio]

Oracles in model files are now relative to the directory containing the model file. I verified that it works as intended on Linux and macOS, but I see no reason why it shouldn't also work on Windows, since Haskell's System.FilePath library supports all three. (Since there is no version of Maude for Windows, I cannot test there. WSL would work, but should be similar to Linux.)

As part of this PR, I also revised the precedence handling of heuristics which is now:

1. Command line
2. Lemma attribute
3. Top-level
4. Default ("s")

This allows specifying heuristics in the model file, but also allows overriding all heuristics using the command line flag.

[deejaydarvin]

Anyone want to try with Windows?

[rkunnema]

Looks good to me. Waiting for @kevinmorio to document this, then I'll merge.