Correcting command line argument for '--max_time'

[aytey]

It seems that the max_conflicts and max_time option had the same short name:

./stp -g 10
terminate called after throwing an instance of 'boost::exception_detail::clone_impl<boost::exception_detail::error_info_injector<boost::program_options::ambiguous_option> >'
  what():  option '-g' is ambiguous and matches '--max_num_confl', and '--max_time'
Aborted (core dumped)

This PR changes that to make sure the have different short names.

The larger changes are due to git-clang-format.

Signed-off-by: Andrew V. Jones andrew.jones@vector.com

[rgov]

Do -g and -k match the options for any other solver? Would be nice to know what CVC4 or whatever uses. They don't make a lot of sense to me and it makes the command line a bit hard to read if you cannot guess what the abbreviations stand for.

[aytey]

I'm genuinely fine to remove these short options all together (I'm pretty sure I added them; at least I did the timeout one!).

To answer your question:

• CVC4 uses --tlimit=MS and --rlimit=N (rlimit for conflicts)

• Z3 uses -T and -t (hard vs. soft, respectively) ... however STP already has a -t for "print quick statistics"

[rgov]

First, I'm for deprecating -t for statistics and encouraging the use of --stats. Then if we want to reclaim -t with a timeout argument, it won't be horrible to update any old workflows that use the flag without an argument.

Then --tlimit and --rlimit sound good to me (not sure what r stands for), with perhaps -T or -t aliasing to --tlimit according to which one matches Z3's behavior best.

My goal isn't to replicate the entire interface (though that might be nice, as Clang replicated GCC's interface) but just make it a little more readable to people coming from other solvers.

[TrevorHansen]

Sorry for the slow merge. This looks good.