add an implementation of std::variant<...>

[kroening]

This appears to require update 3 of MSVC 2015, which may be an issue.

• 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.
• n/a 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).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[kroening]

I don't usually like introducing dependencies, but this one will disappear by itself with time.

[tautschnig]

I'm not particularly convinced we need this, but should there genuinely be a use case we need tests (cf. unit/util/optional.cpp), and possibly documentation, though tests would also serve as such. As is, we have no idea whether this passes CI.

[LAJW]

😱 👍 🥕 Let's make it happen!

[allredj]

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 83f53a7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98995273
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: b10a24e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99566510

[thomasspriggs]

Looks really useful. I notice that the upstream repository for this includes tests. Maybe we should copy over the tests as well, so this can be tested on CI.

[thk123]

I had a quick look at the upstream tests - they are written in GTest - I think rewriting them in catch would be time consuming and error prone. Instead - I suggest including this as a submodule so we can trust that the tests are run by the upstream CI. Alternatively, we could run the tests on our CI - but would involve adding a dependency on gtest for CI. (closed by mistake!)

@tautschnig for motivation - I think if this had existed when symbolt or goto_trace_stept had existed their design would be more robust. Can encode the different types of symbol (e.g. function symbols have a code_typet rather than a typet) but keep the value semantics, don't have awkward class hierarchies.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: ffca144).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102486684

[kroening]

goto_trace_stept is certainly an obvious "customer"; should we use that as trial?

[thk123]

@kroening in principle yes, I worried in practise that something that central would be a very large undertaking. I proposed it as a "motivating example" to demonstrated there are use cases on the assumption that other uses cases that are less entwined was also crop up.

[thk123]

Added as a submodule in #4344 if people would like to review that as well.

[TGWDB]

This PR appears like it could be useful if rebased, any chance of this being revisited (or should we consider closing as too old and out of date)?

[codecov]

Codecov Report

Merging #3962 (0208d01) into develop (ea82b03) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #3962   +/-   ##
========================================
  Coverage    75.90%   75.90%           
========================================
  Files         1515     1515           
  Lines       163990   163989    -1     
========================================
+ Hits        124473   124474    +1     
+ Misses       39517    39515    -2     

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.cpp	94.92% <100.00%> (-0.01%)	⬇️
src/goto-instrument/contracts/assigns.cpp	96.66% <0.00%> (+2.22%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 7435884...0208d01. Read the comment docs.

[TGWDB]

@tautschnig This PR now passes all CI and is waiting only on your requested change, can you please have a look?

[TGWDB]

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.