Help for options about vampire HOT 2 CLOSED

Also, how about renaming it to --help, rather than --show_options? Plus an alias to -h. It seems to be the most common naming. I don't know how is it possible to discover --show_options option without knowing in advance that it exists.

from vampire.

I began work on this feature, which has also been useful in starting to properly understand what options there are and what they mean.

It's in branch https://github.com/easychair/vampire/tree/show_options

I've done more than originally intended. I'm not sure if it's the correct approach as it makes parsing options slightly more work. This can be reviewed.

The basic idea is that every option in Options.cpp is specified in the form

OptionName("sat_solver","sas",VAMPIRE_TAG,
"Select the SAT solver to be used throughout the solver. This will be used in AVATAR (for splitting) when the saturation algorithm is discount,lrs or otter and in instance generation for selection and global subsumption. The buf options are experimental (they add buffering).",
false, "vampire",OptionValues("buf_lingeling","buf_vampire",
"lingeling","vampire")),

Which gives a long name, short name, tag, description, experimental flag, default option and list of options. The tag can be used to filter the options so --show_options vampire will only show options related to vampire mode. This is then formatted as

--sat_solver (-sas)
Select the SAT solver to be used throughout the solver. This will be used
in AVATAR (for splitting) when the saturation algorithm is discount,lrs
or otter and in instance generation for selection and global subsumption.
The buf options are experimental (they add buffering).
values: buf_lingeling,buf_vampire,lingeling,vampire
default: vampire

I have also added a --help option that will (eventually) print some minimal usage help and tell the user about the show_options option.

This is still work in progress (and relatively low priority). It still needs lots of tidying and appropriate tags and descriptions adding to each option.

Hopefully this extension will

1. increase the usability of the tool
2. make adding new options and maintaining current options easier

from vampire.