Defines interface between the simulator and terms that are sent to the
SAT or SMT solver. The simulator can use a richer set of types, but
the symbolic values must be representable by types supported by this
interface.
A solver backend is defined in terms of a type parameter
sym,
which is the type that tracks whatever state or context is needed by
that particular backend. To instantiate the solver interface, one must
provide several type family definitions and class instances for
sym:
The canonical implementation of these interface classes is found in
What4.Expr.Builder.