Add support for CVC4 and Boolector

[jamesbornholt]

This PR adds support for the CVC4 and Boolector SMT solvers.

Since this is the first time we've had multiple SMT backends, we also have to make a few wider changes:

• Different solvers support different SMT logics and features (e.g., unsat cores, optimization), so add solver-features to get the supported features of a solver.
• Annotate the test suite with the required features for each test, so that they aren't run on solvers that don't support them.
• Refactor SMT generation and model parsing to support the quirks of different SMT solvers.
• Since we're not going to install CVC4 or Boolector by default, add support for manually specifying their locations, via a #:path argument to their constructors (and add the same argument to the Z3 constructor, too).

As an added bonus, we also add a new output-smt global parameter that can be set to #t to dump all generated SMT to temporary files for inspection or reuse.

---

Here's an example of how to use a different solver for queries:

#lang rosette

(require rosette/solver/smt/cvc4)
(current-solver (cvc4 #:path "/path/to/cvc4"))

(define-symbolic x (bitvector 5))
(solve (assert (bvsge x (bv 4 5))))

[pmatos]

@jamesbornholt Great job. Thanks for this!

[emina]

Thank you @jamesbornholt!