Connect difficulty manager to TheoryEngine (#7161)

Connect difficulty manager to TheoryEngine (#7161)

This also introduces the produceDifficulty option which is analogous to produceUnsatCores.

It requires another unsat cores mode PP_ONLY, indicating that we are only tracking proofs of preprocessing. This option should perhaps be renamed to proofMode instead of unsatCoresMode, since its use is more general than for unsat cores. This will be addressed in a future refactoring.