This component can be useful when creating implementations of `Solver`,
as some
SAT solvers require the input to be in 3-CNF.
As part of making `CNFFormula` externally accessible, I have moved some
member
variables out of it that aren't really part of the representation of a
3-CNF
formula and thus live better elsewhere:
* `WatchedHead` and `NextWatched` have been moved to
`WatchedLiteralsSolverImpl`, as they're part of the specific algorithm
used
by that SAT solver.
* `Atomics` has become an output parameter of `buildCNF()` because it
has to do
with the relationship between a `CNFFormula` and the set of `Formula`s
it is
derived from rather than being an integral part of the representation of
a
3-CNF formula.
I have also made all member variables private and added appropriate
accessors.
