[proofs] [cnf] Utilities to notify and track proofs of optimized SAT clauses in the...

[proofs] [cnf] Utilities to notify and track proofs of optimized SAT clauses in the ProofCnfStream (#8388)

Adds functionality for the TheoryProxy and ProofCnfStream modules to be notified of clauses that were asserted in lower levels than the current one. These clauses have their proofs tracked in the ProofCnfStream via an OptimizedClausesManager object.

Since the SAT solver may optimize the assertion level of propagation
explanations and of added clauses, we need to be able to maintain proofs across
context-popping. Not doing this can lead to open proofs. To do this the Proof
cnf stream uses an OptClausesManager to re-add proofs of facts inserted at
optimized levels.

Future PRs will change the SAT solver to use these notifications.