Make data structures in relevance manager SAT-context dependent (#7733)

Make data structures in relevance manager SAT-context dependent (#7733)

This PR significantly improves the quality of values in get-difficulty. It fixes several bugs related to get-difficulty, including over-pruning values in ProofManager, and not tracking explanations for certain literals. It also improves performance by tracking justifications in relevance manager in a SAT-context dependent manner.

This is to support difficulty measurements based on lemmas sent at STANDARD effort.

It also adds 2 simple regressions.

A further PR will further improve the quality by being more careful about the relationships between literals and the assertions that entail that they are relevant.