Black-sat

This is a feature release!
- New syntax for the CLI interface based on subcommands. Type `black solve <formula>` to solve the formula.
- A new trace checking feature under the command `black check` to check the satisfaction of a formula by a single model has been integrated in the test suite
- An important fix has been applied to fix a bug in the past operators encoding discovered with the new trace checking feature

Added support for printing the model of satisfiable formulas.
The `-m`/`--model` option asks to print the model if it exists.
The `-o`/`--output-format` option selects the output format. Accepted choices are `readable` (default) and `json`

Direct support for past operators, without a preliminary conversion to LTL (which is still available under the `--remove-past` option).

New feature release:
* Support for past LTL operators (thanks to Gabriele Venturato)
* Important bug fixes for CNF-based backends

Minor update w.r.t. the previous release:
* Everything's ready for binary RPM and DEB packages
* Black now knows its `--version`

This first proper release includes many improvements over the prototype available at the time of submission of the TABLEAUX paper, including:
* multiple backends, supported by an abstraction layer that includes CNF encoding by Tseitin algorithm:
* MiniSAT
* CryptoMiniSAT
* Glucose (turned on as default)
* Z3
* MathSAT
* Better command line interface
* Proper build system, supporting package creation
* Homebrew formula available, Debian and RPM packages coming soon...
* Multiple bug fixes and improvements