Proof format: DOT

Using the flag proof-format-mode=dot, cvc5 outputs proofs in the DOT format.

The DOT format is a graph description language (see e.g. this description). It can be used, among other things, for visualization.

We leverage this format for visualizing cvc5 proofs, in the internal calculus, as a graph. One can use a default dot visualizer or the dedicated proof visualizer available here. It suffices to upload the DOT proof outputted by cvc5, saved into a file. The visualizer offers several custom features, such as fold/unfold subproofs, coloring nodes, and stepwise expansion of let terms.