SYNTHESIZER: Allow goto-synthesizer accept all CBMC options

[qinheping]

With this PR, goto-synthesizer will accept all of CBMC options so that we don't need to update the backend options in goto-synthesizer when they are updated in CBMC_OPTION.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

All modified lines are covered by tests ✅

Comparison is base (faa3144) 78.62% compared to head (31b22af) 78.62%.

❗ Current head 31b22af differs from pull request most recent head b1e19b9. Consider uploading reports for the commit b1e19b9 to get more accurate results

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7900   +/-   ##
========================================
  Coverage    78.62%   78.62%           
========================================
  Files         1701     1700    -1     
  Lines       195974   195974           
========================================
  Hits        154086   154086           
  Misses       41888    41888           

Files	Coverage Δ
...oto-synthesizer/goto_synthesizer_parse_options.cpp	76.19% <100.00%> (+0.94%)	⬆️

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[zhassan-aws]

I don't have much background, but why not make the option --cbmc-options instead to remove the need to specify cbmc (which seems redundant?).

[qinheping]

goto-synthesizer checks its arguments of that start with -- against the SYNTHEZIER_OPT, and errors out if the argument is not matched any defined option. It will happen if some CBMC option is not one of the synthesizer options.
So we let the argument start with cbmc instead to avoid the check.

[tautschnig]

Doing string tokenisation and possibly having to deal with quoting/unquoting feels fragile. Could we please try a rather different approach:

1. Move the implementation of goto_synthesizer_parse_optionst::goto_synthesizer_parse_optionst(int argc, const char **argv) to goto_synthesizer_parse_options.cpp.
2. Keep #include <cbmc/cbmc_parse_options.h> as proposed in the current commit.
3. Use GOTO_SYNTHESIZER_OPTIONS CBMC_OPTIONS (no operator required between these) as the first argument to goto_synthesizer_parse_optionst::goto_synthesizer_parse_optionst.
4. Now goto-synthesizer should just accept all of CBMC's options, and will continue to do so even when those change. We just need to find some good solution for the --help output, perhaps just say "Accepts all of cbmc's options plus the following: ..."

[qinheping]

Doing string tokenisation and possibly having to deal with quoting/unquoting feels fragile. Could we please try a rather different approach:

1. Move the implementation of `goto_synthesizer_parse_optionst::goto_synthesizer_parse_optionst(int argc, const char **argv)` to `goto_synthesizer_parse_options.cpp`.

2. Keep `#include <cbmc/cbmc_parse_options.h>` as proposed in the current commit.

3. Use `GOTO_SYNTHESIZER_OPTIONS CBMC_OPTIONS` (no operator required between these) as the first argument to `goto_synthesizer_parse_optionst::goto_synthesizer_parse_optionst`.

4. Now `goto-synthesizer` should just accept all of CBMC's options, and will continue to do so even when those change. We just need to find some good solution for the `--help` output, perhaps just say "Accepts all of cbmc's options plus the following: ..."

Thank you! I also updated the title and description of this PR.

[tautschnig]

Could you please re-add a test, if that's at all possible (i.e., if there is any new behaviour observable)?