clean-up: check-all-sat feature

[Halbaroth]

This issue is a reminder to all things we have to do to get a clean check-all-sat feature.

• supporting check-all-sat with the solver FunSAT. As I explained in feat: check-all-sat support #846, the current output of the option --all-sat is strange when we use the solver FunSAT. Indeed, FunSAT isn't a CDCL solver. It didn't produce a partial boolean model of the clauses. In particular, it forgot every declared symbols in an abandoned branch.
• supporting check-all-sat in Dolmen.
• check-all-sat should work if we use (set-option :produce-models true) in the SMT-LIB language.
• Test check-all-sat with --dump-models.
• Improve the printer while using this command.
• Choose between --all-sat or --all-models. Both are weird. I suggest --produce-all-bool-models or adding a argument to the command --produce-models. We could do the same with --dump-models for the native input language.
• Add documentation about the feature and modify the change log.
• Producing new declaration in the module Frontend.ml isn't a neat design. We should add a new command to the SAT interface sig_sat.mli for check-all-sat.
• Add tests and cram tests.

[Halbaroth]

We decided to not support this feature in a near future.